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.