Structure theorem for… to The two-term Euler formula

TheoremStructure theorem for torsion-free topologically finitely generated abelian pro-`p` groups #

Such a group is topologically isomorphic to ℤ_p ^ r.

TauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt.{u_1} {p : ℕ} [Fact (Nat.Prime p)]
  {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A]
  [TotallyDisconnectedSpace A] [IsMulTorsionFree A] (hA : TauCeti.IsProP p A)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated A) :
  ∃ r, Nonempty (A ≃ₜ* Multiplicative (Fin r → ℤ_[p]))

Lean

Formalized in Tau Ceti as TauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt.

Sources

LeanTauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt

Uses 1

Proof usesStructure theorem for topologically finitely generated abelian pro-p groups

TheoremThe successive-approximation theorem with tails #

Let r, w ∈ λ_1(F) be relators of the free pro-p group F on a finite linearly ordered type with the same class ρ ∈ gr_1(F), let S be a set of generators and l₁, l₂ disjoint duplicate-free lists of generators containing S, and suppose gr_{m+1}(F) = Im δ_ρ + ⟨π^{m+1} ξ_i : i ∈ S⟩ for every m ≥ 1. Then a continuous automorphism e of F carries r to (∏_{i ∈ l₁} t_i) * w * (∏_{i ∈ l₂} t_i) for tail elements t_i of the closed procyclic subgroups ⟨x_i⟩, all lying in λ_2(F).

TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_sup_gradedPowIterSpan_eq_top.{u}
  {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] [LinearOrder X]
  (r w : ↥(TauCeti.pLowerCentralSeries p (TauCeti.freeProP p X) 1))
  (h :
    TauCeti.gradedMk p (TauCeti.freeProP p X) 1 r = TauCeti.gradedMk p (TauCeti.freeProP p X) 1 w)
  (S : Set X) (l₁ l₂ : List X) (hnd : (l₁ ++ l₂).Nodup) (hl : ∀ i ∈ S, i ∈ l₁ ++ l₂)
  (hspan :
    ∀ (m : ℕ) (hm : 1 ≤ m),
      ((TauCeti.freeProP.basisModificationDelta p X hm)
              (TauCeti.gradedMk p (TauCeti.freeProP p X) 1 r)).range ⊔
          TauCeti.freeProP.gradedPowIterSpan p X S (m + 1) =
        ⊤) :
  ∃ e t,
    (∀ (i : X), t i ∈ (Subgroup.closure {TauCeti.freeProP.of i}).topologicalClosure) ∧
      (∀ (i : X), t i ∈ TauCeti.pLowerCentralSeries p (TauCeti.freeProP p X) 2) ∧
        e ↑r = (List.map t l₁).prod * ↑w * (List.map t l₂).prod

Lean

Formalized in Tau Ceti as TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_sup_gradedPowIterSpan_eq_top.

Sources

LeanTauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_sup_gradedPowIterSpan_eq_top

Used by 6

Used byThe marked presentation of G_{ℚ₂}(2) · Labute's Theorem 2 at the even-rank dyadic endpoint · Labute's Theorem 2 · Labute's Theorem 2 for odd rank · The necessity half of the existence theorem for q ≠ 2 (Labute, Theorem 1) · Uniqueness of the dyadic Demushkin groups of even rank with image {±1} × U^(f) (Labute, Theorem 6)

TheoremTate's criterion for the cohomological dimension of a pro-`p` group #

Let G be a profinite pro-p group. If for every short exact sequence 0 → A → B → C → 0 of finite discrete G-modules killed by p the map Hⁿ(G, B) → Hⁿ(G, C) is surjective, then cd_p G ≤ n: right exactness kills Hⁿ⁺¹ on those modules, and dévissage extends the vanishing to every finite discrete p-primary module.

TauCeti.IsProP.cohomologicalDimensionAt_le_of_forall_coeffMap_proj_surjective.{u} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] (hG : TauCeti.IsProP p G) [TotallyDisconnectedSpace G] (n : ℕ)
  (h :
    ∀ (A B C : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A]
      [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A]
      [inst_6 : AddCommGroup B] [inst_7 : TopologicalSpace B] [inst_8 : DiscreteTopology B]
      [inst_9 : DistribMulAction G B] [ContinuousSMul G B] [Finite B] [inst_12 : AddCommGroup C]
      [inst_13 : TopologicalSpace C] [inst_14 : DiscreteTopology C] [inst_15 : DistribMulAction G C]
      [ContinuousSMul G C] [Finite C] (S : TauCeti.ContCohomology.DiscreteShortExact G A B C),
      (∀ (a : A), p • a = 0) →
        (∀ (b : B), p • b = 0) →
          (∀ (c : C), p • c = 0) →
            Function.Surjective
              ⇑(CategoryTheory.ConcreteCategory.hom
                  (TauCeti.ContinuousCohomology.coeffMap
                    (TauCeti.ofDiscreteModuleMap S.proj.toIntLinearMap ⋯) n))) :
  TauCeti.cohomologicalDimensionAt p G ≤ ↑n

Lean

Formalized in Tau Ceti as TauCeti.IsProP.cohomologicalDimensionAt_le_of_forall_coeffMap_proj_surjective.

Sources

LeanTauCeti.IsProP.cohomologicalDimensionAt_le_of_forall_coeffMap_proj_surjective

Uses 2 · Used by 1

Proof usesDimension shifting in every positive degree · Shapiro's lemma in degree one

Used byTate's duality criterion for cd_p G ≤ 2

TheoremTate's duality criterion for `cd_p G ≤ 2`#

Let G be a profinite pro-p group and N a discrete G-module. If Tate's duality map in degree two, α₂ : H²(G, M) → Hom(H⁰(G, InternalHom G M N), H²(G, N)), is bijective for every finite discrete G-module M killed by p, then cd_p G ≤ 2: duality makes H²(G, -) right exact on those modules (TauCeti.ContCohomology.DiscreteShortExact.coeffMap_proj_surjective_of_dualityMap2), and right exactness bounds the dimension. For an infinite Demushkin group and N = 𝔽_p the hypothesis is Tate's perfect duality, and the conclusion is the upper bound in cd_p G = 2.

TauCeti.IsProP.cohomologicalDimensionAt_le_two_of_forall_dualityMap2_bijective.{u, v} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] (hG : TauCeti.IsProP p G) [TotallyDisconnectedSpace G] (N : Type v)
  [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N]
  [ContinuousSMul G N]
  (h :
    ∀ (M : Type u) [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
      [inst_2 : DiscreteTopology M] [inst_3 : DistribMulAction G M] [inst_4 : ContinuousSMul G M]
      [Finite M],
      (∀ (m : M), p • m = 0) → Function.Bijective ⇑(TauCeti.ContCohomology.dualityMap2 G M N)) :
  TauCeti.cohomologicalDimensionAt p G ≤ 2

Lean

Formalized in Tau Ceti as TauCeti.IsProP.cohomologicalDimensionAt_le_two_of_forall_dualityMap2_bijective.

Sources

LeanTauCeti.IsProP.cohomologicalDimensionAt_le_two_of_forall_dualityMap2_bijective

Uses 1 · Used by 2

Proof usesTate's criterion for the cohomological dimension of a pro-p group

Used byTate's theorem: an infinite Demushkin group has p-cohomological dimension exactly 2 · The isomorphism type of an open subgroup of a Demushkin group

TheoremThe three-term Euler formula #

Let G be a topologically finitely generated profinite pro-p group whose canonical H³ vanishes on the discrete modules of order p with trivial action, with H²(G, 𝔽_p) finite, and let U be an open subgroup. Then, in ℤ,

dim H⁰(U) - dim H¹(U) + dim H²(U) = [G : U] * (dim H⁰(G) - dim H¹(G) + dim H²(G)),

for the cohomology with trivial coefficients 𝔽_p. The six spaces are finite-dimensional: H⁰ always, H¹ because G and U are topologically finitely generated, and H²(U, 𝔽_p) by TauCeti.IsProP.finite_cohomFp_openSubgroup.

TauCeti.IsProP.finrank_cohomFp_zero_sub_finrank_cohomFp_one_add_finrank_cohomFp_two_openSubgroup.{u}
  {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G)
  (h3 :
    ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A]
      [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A],
      Nat.card A = p →
        (∀ (g : G) (a : A), g • a = a) →
          Subsingleton ↑(continuousCohomology 3 (TauCeti.ofDiscreteModule ℤ G A)).toModuleCat)
  [Finite ↑(TauCeti.cohomFp p G 2).toModuleCat] (U : OpenSubgroup G) :
  ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 0).toModuleCat) -
        ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 1).toModuleCat) +
      ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 2).toModuleCat) =
    ↑(↑U).index *
      (↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 0).toModuleCat) -
          ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 1).toModuleCat) +
        ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 2).toModuleCat))

Lean

Formalized in Tau Ceti as TauCeti.IsProP.finrank_cohomFp_zero_sub_finrank_cohomFp_one_add_finrank_cohomFp_two_openSubgroup.

Other forms

The three-term Euler formula. Formalized in Tau Ceti as TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_add_finrank_H2.

TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_add_finrank_H2.{u} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)]
  [ContinuousSMul G (ZMod p)] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x)
  (h3 :
    ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A]
      [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A],
      Nat.card A = p →
        (∀ (g : G) (a : A), g • a = a) →
          Subsingleton ↑(continuousCohomology 3 (TauCeti.ofDiscreteModule ℤ G A)).toModuleCat)
  (U : OpenSubgroup G) [Finite (TauCeti.ContCohomology.H2 G (ZMod p))] :
  1 - ↑(TauCeti.topologicalGeneratorRankNat ↥↑U ⋯) +
      ↑(Module.finrank (ZMod p) (TauCeti.ContCohomology.H2 (↥↑U) (ZMod p))) =
    ↑(↑U).index *
      (1 - ↑(TauCeti.topologicalGeneratorRankNat G hfg) +
        ↑(Module.finrank (ZMod p) (TauCeti.ContCohomology.H2 G (ZMod p))))

The three-term Euler formula under cd_p G ≤ 2. Formalized in Tau Ceti as TauCeti.CohomologicalDimensionLE.finrank_cohomFp_zero_sub_finrank_cohomFp_one_add_finrank_cohomFp_two_openSubgroup.

TauCeti.CohomologicalDimensionLE.finrank_cohomFp_zero_sub_finrank_cohomFp_one_add_finrank_cohomFp_two_openSubgroup.{u}
  {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) (hcd : TauCeti.CohomologicalDimensionLE p G 2)
  [Finite ↑(TauCeti.cohomFp p G 2).toModuleCat] (U : OpenSubgroup G) :
  ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 0).toModuleCat) -
        ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 1).toModuleCat) +
      ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 2).toModuleCat) =
    ↑(↑U).index *
      (↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 0).toModuleCat) -
          ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 1).toModuleCat) +
        ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 2).toModuleCat))

The three-term Euler formula under cd_p G ≤ 2. Formalized in Tau Ceti as TauCeti.CohomologicalDimensionLE.one_sub_topologicalGeneratorRankNat_add_finrank_H2.

TauCeti.CohomologicalDimensionLE.one_sub_topologicalGeneratorRankNat_add_finrank_H2.{u} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)]
  [ContinuousSMul G (ZMod p)] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x)
  (hcd : TauCeti.CohomologicalDimensionLE p G 2) (U : OpenSubgroup G)
  [Finite (TauCeti.ContCohomology.H2 G (ZMod p))] :
  1 - ↑(TauCeti.topologicalGeneratorRankNat ↥↑U ⋯) +
      ↑(Module.finrank (ZMod p) (TauCeti.ContCohomology.H2 (↥↑U) (ZMod p))) =
    ↑(↑U).index *
      (1 - ↑(TauCeti.topologicalGeneratorRankNat G hfg) +
        ↑(Module.finrank (ZMod p) (TauCeti.ContCohomology.H2 G (ZMod p))))

Sources

LeanTauCeti.IsProP.finrank_cohomFp_zero_sub_finrank_cohomFp_one_add_finrank_cohomFp_two_openSubgroup · TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_add_finrank_H2 · TauCeti.CohomologicalDimensionLE.finrank_cohomFp_zero_sub_finrank_cohomFp_one_add_finrank_cohomFp_two_openSubgroup · TauCeti.CohomologicalDimensionLE.one_sub_topologicalGeneratorRankNat_add_finrank_H2

Uses 3 · Used by 1

Proof usesBurnside's basis theorem, cardinal form · Shapiro's lemma in degree one · The three-term Euler identity under cd_p G ≤ 2

Used byThe isomorphism type of an open subgroup of a Demushkin group

TheoremThe three-term Euler identity under `cd_p G ≤ 2`#

For a topologically finitely generated profinite pro-p group G with cd_p G ≤ 2, the trivial action on 𝔽_p, and a finite discrete G-module M of order p ^ k, |H⁰(G, M)| * |H²(G, M)| * p ^ (k * d(G)) = |H¹(G, M)| * p ^ k * |H²(G, 𝔽_p)| ^ k.

TauCeti.CohomologicalDimensionLE.natCard_H0_mul_natCard_H2_mul_pow.{u} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)]
  [ContinuousSMul G (ZMod p)] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x)
  (hcd : TauCeti.CohomologicalDimensionLE p G 2) (M : Type u) [AddCommGroup M] [TopologicalSpace M]
  [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] {k : ℕ}
  (hk : Nat.card M = p ^ k) :
  Nat.card ↥(TauCeti.ContCohomology.H0 G M) * Nat.card (TauCeti.ContCohomology.H2 G M) *
      p ^ (k * TauCeti.topologicalGeneratorRankNat G hfg) =
    Nat.card (TauCeti.ContCohomology.H1 G M) * p ^ k *
      Nat.card (TauCeti.ContCohomology.H2 G (ZMod p)) ^ k

Lean

Formalized in Tau Ceti as TauCeti.CohomologicalDimensionLE.natCard_H0_mul_natCard_H2_mul_pow.

Other forms

The three-term Euler identity for an open subgroup under cd_p G ≤ 2. Formalized in Tau Ceti as TauCeti.CohomologicalDimensionLE.natCard_H2_openSubgroup_mul_pow.

TauCeti.CohomologicalDimensionLE.natCard_H2_openSubgroup_mul_pow.{u} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)]
  [ContinuousSMul G (ZMod p)] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) (htriv : ∀ (g : G) (x : ZMod p), g • x = x)
  (hcd : TauCeti.CohomologicalDimensionLE p G 2) (U : OpenSubgroup G) :
  p * Nat.card (TauCeti.ContCohomology.H2 (↥↑U) (ZMod p)) *
      p ^ ((↑U).index * TauCeti.topologicalGeneratorRankNat G hfg) =
    p ^ TauCeti.topologicalGeneratorRankNat ↥↑U ⋯ * p ^ (↑U).index *
      Nat.card (TauCeti.ContCohomology.H2 G (ZMod p)) ^ (↑U).index

The three-term Euler identity for the permutation module of an open subgroup, read through Shapiro's lemma. Formalized in Tau Ceti as TauCeti.IsProP.natCard_H2_openSubgroup_mul_pow.

TauCeti.IsProP.natCard_H2_openSubgroup_mul_pow.{u} {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)]
  (hG : TauCeti.IsProP p G) (hfg : TauCeti.IsTopologicallyFinitelyGenerated G)
  (htriv : ∀ (g : G) (x : ZMod p), g • x = x)
  (h3 :
    ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A]
      [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A],
      Nat.card A = p →
        (∀ (g : G) (a : A), g • a = a) →
          Subsingleton ↑(continuousCohomology 3 (TauCeti.ofDiscreteModule ℤ G A)).toModuleCat)
  (U : OpenSubgroup G) :
  p * Nat.card (TauCeti.ContCohomology.H2 (↥↑U) (ZMod p)) *
      p ^ ((↑U).index * TauCeti.topologicalGeneratorRankNat G hfg) =
    p ^ TauCeti.topologicalGeneratorRankNat ↥↑U ⋯ * p ^ (↑U).index *
      Nat.card (TauCeti.ContCohomology.H2 G (ZMod p)) ^ (↑U).index

Sources

LeanTauCeti.CohomologicalDimensionLE.natCard_H0_mul_natCard_H2_mul_pow · TauCeti.CohomologicalDimensionLE.natCard_H2_openSubgroup_mul_pow · TauCeti.IsProP.natCard_H2_openSubgroup_mul_pow

Uses 2 · Used by 1

Proof usesBurnside's basis theorem, cardinal form · Shapiro's lemma in degree one

Used byThe three-term Euler formula

TheoremThe topological first isomorphism theorem for rings #

A ring homomorphism that is a quotient map presents its target as the quotient of its source by its kernel, topologically as well as algebraically.

A continuous surjection is not enough on its own. Surjectivity of f makes the lift bijective and continuity of f makes it continuous, but a continuous bijection is open only when the topology it lands in is no coarser than the one it carries; that f is a quotient map is exactly the statement that it is not coarser.

IsHomeomorph.homeomorph turns this into R ⧸ ker f ≃ₜ S. What it bundles is RingHom.kerLift, which is a ring homomorphism, so a consumer needing the isomorphism of rings has it already — RingHom.quotientKerEquivOfSurjective is that same map.

RingHom.isHomeomorph_kerLift.{u_1, u_2} {R : Type u_1} {S : Type u_2} [TopologicalSpace R]
  [CommRing R] [TopologicalSpace S] [Semiring S] {f : R →+* S} (hq : Topology.IsQuotientMap ⇑f) :
  IsHomeomorph ⇑f.kerLift

Lean

Formalized in Tau Ceti as RingHom.isHomeomorph_kerLift.

Other forms

Topological first isomorphism theorem for the module topology. Formalized in Tau Ceti as LinearMap.quotKerContinuousLinearEquivOfSurjective.

LinearMap.quotKerContinuousLinearEquivOfSurjective.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2}
  {N : Type u_3} [Ring R] [TopologicalSpace R] [AddCommGroup M] [_root_.Module R M]
  [TopologicalSpace M] [IsModuleTopology R M] [AddCommGroup N] [_root_.Module R N]
  [TopologicalSpace N] [IsModuleTopology R N] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) :
  (M ⧸ f.ker) ≃L[R] N

Sources

LeanRingHom.isHomeomorph_kerLift · LinearMap.quotKerContinuousLinearEquivOfSurjective

TheoremThe topological Nakayama lemma #

Let I be a finitely generated ideal of topologically nilpotent elements. If P is a compact submodule and N a closed submodule of a topological module with P ≤ N ⊔ I • P, then P ≤ N. Compactness of P replaces the finite generation hypothesis of Submodule.le_of_le_smul_of_le_jacobson.

Submodule.le_of_le_smul_of_isCompact.{u_1, u_2} {R : Type u_1} {M : Type u_2} [CommSemiring R]
  [TopologicalSpace R] [AddCommGroup M] [_root_.Module R M] [TopologicalSpace M]
  [IsTopologicalAddGroup M] [ContinuousSMul R M] {I : Ideal R} {N P : Submodule R M} (hI : I.FG)
  (hInil : ∀ a ∈ I, IsTopologicallyNilpotent a) (hN : IsClosed ↑N) (hP : IsCompact ↑P)
  (hNP : P ≤ N ⊔ I • P) : P ≤ N

Lean

Formalized in Tau Ceti as Submodule.le_of_le_smul_of_isCompact.

Other forms

The topological Nakayama lemma, vanishing form. Formalized in Tau Ceti as Submodule.eq_bot_of_le_smul_of_isCompact.

Submodule.eq_bot_of_le_smul_of_isCompact.{u_1, u_2} {R : Type u_1} {M : Type u_2} [CommSemiring R]
  [TopologicalSpace R] [AddCommGroup M] [_root_.Module R M] [TopologicalSpace M]
  [IsTopologicalAddGroup M] [ContinuousSMul R M] [T1Space M] {I : Ideal R} {N : Submodule R M}
  (hI : I.FG) (hInil : ∀ a ∈ I, IsTopologicallyNilpotent a) (hN : IsCompact ↑N) (hIN : N ≤ I • N) :
  N = ⊥

Sources

LeanSubmodule.le_of_le_smul_of_isCompact · Submodule.eq_bot_of_le_smul_of_isCompact

TheoremThe torsion-free case of the structure theorem #

The coordinate q of the exponent vector exponentSum r = q • w, w x₀ = 1, of the relator vanishes exactly when r lies in the closed commutator subgroup of the free pro-p group; then the factor ℤ_p ⧸ q ℤ_p of oneRelatorAbelianizationEquiv is ℤ_p and G^{ab} ≅ ℤ_p^X is torsion-free.

TauCeti.presentedProP.oneRelator_q_eq_zero_iff_mem_topologicalClosure_commutator.{u} {p : ℕ}
  [Fact (Nat.Prime p)] {X : Type u} (r : TauCeti.freeProP p X) (x₀ : X) (w : X → ℤ_[p])
  (hw : w x₀ = 1) (q : ℤ_[p])
  (hr : Multiplicative.toAdd ((TauCeti.freeProP.exponentSum p X) r) = q • w) [Finite X] :
  q = 0 ↔ r ∈ (commutator (TauCeti.freeProP p X)).topologicalClosure

Lean

Formalized in Tau Ceti as TauCeti.presentedProP.oneRelator_q_eq_zero_iff_mem_topologicalClosure_commutator.

Sources

LeanTauCeti.presentedProP.oneRelator_q_eq_zero_iff_mem_topologicalClosure_commutator

TheoremThe trivial-filtration theorem #

A finite discrete p-primary additive group M with a continuous action of a pro-p group G has a G-stable increasing chain of subgroups N 0 = ⊥ ≤ N 1 ≤ … reaching ⊤ after padicValNat p (Nat.card M) steps, the composition length of M, and constant at ⊤ from there on, with |N i| = p ^ i along the way. Each step adjoins an element x with x ∉ N i, p • x ∈ N i and g • x - x ∈ N i for every g, so every factor N (i + 1) ⧸ N i is a copy of 𝔽_p with trivial G-action.

TauCeti.exists_filtration_of_isProP.{u_1, u_2} {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1}
  [Group G] [TopologicalSpace G] {M : Type u_2} [AddCommGroup M] [TopologicalSpace M]
  [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M]
  (hG : TauCeti.IsProP p G) (htors : IsAddPGroup p M) :
  ∃ N,
    N 0 = ⊥ ∧
      Monotone N ∧
        (∀ (i : ℕ), padicValNat p (Nat.card M) ≤ i → N i = ⊤) ∧
          (∀ (i : ℕ) (g : G), ∀ x ∈ N i, g • x ∈ N i) ∧
            (∀ i ≤ padicValNat p (Nat.card M), Nat.card ↥(N i) = p ^ i) ∧
              ∀ i < padicValNat p (Nat.card M),
                ∃ x,
                  N (i + 1) = N i ⊔ AddSubgroup.zmultiples x ∧
                    x ∉ N i ∧ p • x ∈ N i ∧ ∀ (g : G), g • x - x ∈ N i

Lean

Formalized in Tau Ceti as TauCeti.exists_filtration_of_isProP.

Other forms

The trivial-filtration theorem, first form. Formalized in Tau Ceti as TauCeti.exists_ne_zero_invariant_of_isProP.

TauCeti.exists_ne_zero_invariant_of_isProP.{u, v} {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u}
  [Group G] [TopologicalSpace G] {M : Type v} [AddGroup M] [DistribMulAction G M] [Finite M]
  [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] (hG : TauCeti.IsProP p G)
  [Nontrivial M] (htors : IsAddPGroup p M) : ∃ m, m ≠ 0 ∧ ∀ (g : G), g • m = m

The trivial-filtration theorem, relative form. Formalized in Tau Ceti as TauCeti.exists_notMem_nsmul_mem_smul_sub_mem_of_isProP.

TauCeti.exists_notMem_nsmul_mem_smul_sub_mem_of_isProP.{u, v} {p : ℕ} [hp : Fact (Nat.Prime p)]
  {G : Type u} [Group G] [TopologicalSpace G] {M : Type v} [AddCommGroup M] [TopologicalSpace M]
  [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M]
  (hG : TauCeti.IsProP p G) (htors : IsAddPGroup p M) {N : AddSubgroup M}
  (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) (hN' : N ≠ ⊤) : ∃ x ∉ N, p • x ∈ N ∧ ∀ (g : G), g • x - x ∈ N

Sources

LeanTauCeti.exists_filtration_of_isProP · TauCeti.exists_ne_zero_invariant_of_isProP · TauCeti.exists_notMem_nsmul_mem_smul_sub_mem_of_isProP

TheoremThe two-term Euler formula #

Let G be a topologically finitely generated profinite pro-p group whose explicit H² vanishes on the discrete modules of order p with trivial action, and let U be an open subgroup. Then, in ℤ,

dim H⁰(U, 𝔽_p) - dim H¹(U, 𝔽_p) = [G : U] * (dim H⁰(G, 𝔽_p) - dim H¹(G, 𝔽_p)).

The four spaces are finite-dimensional: H⁰ always, and H¹ because G and U are topologically finitely generated (TauCeti.IsProP.finite_cohomFp_one_iff).

TauCeti.IsProP.finrank_cohomFp_zero_sub_finrank_cohomFp_one_openSubgroup.{u} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G)
  (h2 :
    ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A]
      [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [inst_4 : ContinuousSMul G A]
      [Finite A],
      Nat.card A = p →
        (∀ (g : G) (a : A), g • a = a) → Subsingleton (TauCeti.ContCohomology.H2 G A))
  (U : OpenSubgroup G) :
  ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 0).toModuleCat) -
      ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 1).toModuleCat) =
    ↑(↑U).index *
      (↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 0).toModuleCat) -
        ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 1).toModuleCat))

Lean

Formalized in Tau Ceti as TauCeti.IsProP.finrank_cohomFp_zero_sub_finrank_cohomFp_one_openSubgroup.

Other forms

The two-term Euler formula. Formalized in Tau Ceti as TauCeti.IsProP.topologicalGeneratorRankNat_add_index.

TauCeti.IsProP.topologicalGeneratorRankNat_add_index.{u} {p : ℕ} [hp : Fact (Nat.Prime p)]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G)
  (h2 :
    ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A]
      [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [inst_4 : ContinuousSMul G A]
      [Finite A],
      Nat.card A = p →
        (∀ (g : G) (a : A), g • a = a) → Subsingleton (TauCeti.ContCohomology.H2 G A))
  (U : OpenSubgroup G) :
  TauCeti.topologicalGeneratorRankNat ↥↑U ⋯ + (↑U).index =
    1 + (↑U).index * TauCeti.topologicalGeneratorRankNat G hfg

The two-term Euler formula under cd_p G ≤ 1. Formalized in Tau Ceti as TauCeti.CohomologicalDimensionLE.finrank_cohomFp_zero_sub_finrank_cohomFp_one_openSubgroup.

TauCeti.CohomologicalDimensionLE.finrank_cohomFp_zero_sub_finrank_cohomFp_one_openSubgroup.{u}
  {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) (hcd : TauCeti.CohomologicalDimensionLE p G 1)
  (U : OpenSubgroup G) :
  ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 0).toModuleCat) -
      ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p (↥↑U) 1).toModuleCat) =
    ↑(↑U).index *
      (↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 0).toModuleCat) -
        ↑(Module.finrank (ZMod p) ↑(TauCeti.cohomFp p G 1).toModuleCat))

The two-term Euler formula under cd_p G ≤ 1. Formalized in Tau Ceti as TauCeti.CohomologicalDimensionLE.topologicalGeneratorRankNat_add_index.

TauCeti.CohomologicalDimensionLE.topologicalGeneratorRankNat_add_index.{u} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) (hcd : TauCeti.CohomologicalDimensionLE p G 1)
  (U : OpenSubgroup G) :
  TauCeti.topologicalGeneratorRankNat ↥↑U ⋯ + (↑U).index =
    1 + (↑U).index * TauCeti.topologicalGeneratorRankNat G hfg

The two-term Euler formula under cd_p G ≤ 1, in ℤ. Formalized in Tau Ceti as TauCeti.CohomologicalDimensionLE.one_sub_topologicalGeneratorRankNat_eq.

TauCeti.CohomologicalDimensionLE.one_sub_topologicalGeneratorRankNat_eq.{u} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) (hcd : TauCeti.CohomologicalDimensionLE p G 1)
  (U : OpenSubgroup G) :
  1 - ↑(TauCeti.topologicalGeneratorRankNat ↥↑U ⋯) =
    ↑(↑U).index * (1 - ↑(TauCeti.topologicalGeneratorRankNat G hfg))

The two-term Euler formula, in ℤ. Formalized in Tau Ceti as TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_eq.

TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_eq.{u} {p : ℕ} [hp : Fact (Nat.Prime p)]
  {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G)
  (h2 :
    ∀ (A : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A]
      [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [inst_4 : ContinuousSMul G A]
      [Finite A],
      Nat.card A = p →
        (∀ (g : G) (a : A), g • a = a) → Subsingleton (TauCeti.ContCohomology.H2 G A))
  (U : OpenSubgroup G) :
  1 - ↑(TauCeti.topologicalGeneratorRankNat ↥↑U ⋯) =
    ↑(↑U).index * (1 - ↑(TauCeti.topologicalGeneratorRankNat G hfg))

Sources

LeanTauCeti.IsProP.finrank_cohomFp_zero_sub_finrank_cohomFp_one_openSubgroup · TauCeti.IsProP.topologicalGeneratorRankNat_add_index · TauCeti.CohomologicalDimensionLE.finrank_cohomFp_zero_sub_finrank_cohomFp_one_openSubgroup · TauCeti.CohomologicalDimensionLE.topologicalGeneratorRankNat_add_index · TauCeti.CohomologicalDimensionLE.one_sub_topologicalGeneratorRankNat_eq · TauCeti.IsProP.one_sub_topologicalGeneratorRankNat_eq

Uses 2 · Used by 1

Proof usesBurnside's basis theorem, cardinal form · Shapiro's lemma in degree one

Used byThe Schreier index formula for open subgroups

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Structure theorem for… to The two-term Euler formula

TheoremStructure theorem for torsion-free topologically finitely generated abelian pro-p groups#

Lean

Sources

TheoremThe successive-approximation theorem with tails#

Lean

Sources

TheoremTate's criterion for the cohomological dimension of a pro-p group#

Lean

Sources

TheoremTate's duality criterion for cd_p G ≤ 2#

Lean

Sources

TheoremThe three-term Euler formula#

Lean

Other forms

Sources

TheoremThe three-term Euler identity under cd_p G ≤ 2#

Lean

Other forms

Sources

TheoremThe topological first isomorphism theorem for rings#

Lean

Other forms

Sources

TheoremThe topological Nakayama lemma#

Lean

Other forms

Sources

TheoremThe torsion-free case of the structure theorem#

Lean

Sources

TheoremThe trivial-filtration theorem#

Lean

Other forms

Sources

TheoremThe two-term Euler formula#

Lean

Other forms

Sources

TheoremStructure theorem for torsion-free topologically finitely generated abelian pro-`p` groups #

TheoremThe successive-approximation theorem with tails #

TheoremTate's criterion for the cohomological dimension of a pro-`p` group #

TheoremTate's duality criterion for `cd_p G ≤ 2`#

TheoremThe three-term Euler formula #

TheoremThe three-term Euler identity under `cd_p G ≤ 2`#

TheoremThe topological first isomorphism theorem for rings #

TheoremThe topological Nakayama lemma #

TheoremThe torsion-free case of the structure theorem #

TheoremThe trivial-filtration theorem #

TheoremThe two-term Euler formula #