Profinite integers, profinite powers, and continuous automorphisms

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe continuous automorphisms of a pro-p group acting trivially on its Frattini quotient form a pro-p group#

For a compact pro-p group G, the kernel of ContinuousAut G →* MulAut (G ⧸ proPFrattini p G) is pro-p for the congruence topology.

TauCeti.IsProP.isProP_ker_mapQuotient_proPFrattini.{u_1} {G : Type u_1} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ} [Fact (Nat.Prime p)]
  (hG : TauCeti.IsProP p G) : TauCeti.IsProP p ↥(TauCeti.ContinuousAut.mapQuotient ⋯).ker
Lean

Formalized in Tau Ceti as TauCeti.IsProP.isProP_ker_mapQuotient_proPFrattini.

Sources
LeanTauCeti.IsProP.isProP_ker_mapQuotient_proPFrattini
Uses 1
Proof usesTauCeti.profiniteFrattini

TheoremTauCeti.ContinuousAut.isOpen_ker_mapQuotient_proPFrattini#

For a topologically finitely generated compact group, the continuous automorphisms acting trivially on the pro-p Frattini quotient form an open subgroup for the congruence topology: the pro-p Frattini subgroup is open and topologically characteristic.

TauCeti.ContinuousAut.isOpen_ker_mapQuotient_proPFrattini.{u_1} {G : Type u_1} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  (hG : TauCeti.IsTopologicallyFinitelyGenerated G) (p : ℕ) :
  IsOpen ↑(TauCeti.ContinuousAut.mapQuotient ⋯).ker
Lean

Formalized in Tau Ceti as TauCeti.ContinuousAut.isOpen_ker_mapQuotient_proPFrattini.

Sources
LeanTauCeti.ContinuousAut.isOpen_ker_mapQuotient_proPFrattini

TheoremThe kernel on the Frattini quotient is the inverse limit of the finite kernels#

For a topologically finitely generated pro-p group G, the coordinates on the quotients G ⧸ N by the topologically characteristic open normal subgroups N ≤ proPFrattini p G identify the kernel of ContinuousAut G →* MulAut (G ⧸ proPFrattini p G) with the families of automorphisms σ N of the finite p-groups G ⧸ N that act trivially on the Frattini quotients of G ⧸ N and are compatible with the quotient maps G ⧸ N → G ⧸ M for N ≤ M. The coordinate map is injective and a topological embedding by ContinuousAut.isEmbedding_pi_mapQuotient_ker_proPFrattini.

TauCeti.IsProP.range_pi_mapQuotient_ker_proPFrattini.{u_1} {G : Type u_1} [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ}
  [Fact (Nat.Prime p)] (hG : TauCeti.IsProP p G)
  (hfg : TauCeti.IsTopologicallyFinitelyGenerated G) :
  (Set.range fun φ N => (TauCeti.ContinuousAut.mapQuotient ⋯) ↑φ) =
    {σ |
      (∀
          (N :
            { N //
              TauCeti.IsTopCharacteristic G ↑N.toOpenSubgroup ∧
                ↑N.toOpenSubgroup ≤ TauCeti.proPFrattini p G }),
          σ N ∈ (MulAut.mapQuotient (frattini (G ⧸ ↑(↑N).toOpenSubgroup))).ker) ∧
        ∀
          ⦃N M :
            { N //
              TauCeti.IsTopCharacteristic G ↑N.toOpenSubgroup ∧
                ↑N.toOpenSubgroup ≤ TauCeti.proPFrattini p G }⦄
          (hle : ↑N ≤ ↑M) (q : G ⧸ ↑(↑N).toOpenSubgroup),
          (TauCeti.QuotientGroup.mapOfLE hle) ((σ N) q) =
            (σ M) ((TauCeti.QuotientGroup.mapOfLE hle) q)}
Lean

Formalized in Tau Ceti as TauCeti.IsProP.range_pi_mapQuotient_ker_proPFrattini.

Sources
LeanTauCeti.IsProP.range_pi_mapQuotient_ker_proPFrattini
Uses 1
Proof usesTauCeti.profiniteFrattini

Definitiongr_1 of a free pro-p group is the exterior square of gr_0#

For the free pro-p group F on a finite type, the graded bracket induces an isomorphism of ℤ_p-modules ⋀²gr_0(F) ≃ gr_1(F), x ∧ y ↦ [x, y] (exteriorSquareEquivLcsGradedPieceOne_ιMulti).

TauCeti.freeProP.exteriorSquareEquivLcsGradedPieceOne.{u} (p : ℕ) [Fact (Nat.Prime p)] (X : Type u)
  [Fintype X] :
  ↥(⋀[ℤ_[p]]^2 (TauCeti.lcsGradedPiece (TauCeti.freeProP p X) 0)) ≃ₗ[ℤ_[p]]
    TauCeti.lcsGradedPiece (TauCeti.freeProP p X) 1
Lean

Formalized in Tau Ceti as TauCeti.freeProP.exteriorSquareEquivLcsGradedPieceOne.

Sources
LeanTauCeti.freeProP.exteriorSquareEquivLcsGradedPieceOne
Uses 1 · Used by 1
Statement usesThe ℤ_p-basis of gr_1 of a free pro-p group of finite rank
Used byTauCeti.freeProP.finrank_lcsGradedPiece_one

DefinitionThe ℤ_p-basis of gr_1 of a free pro-p group of finite rank#

The ℤ_p-basis of gr_1 of a free pro-p group of finite rank, formed by the brackets [x_i, x_j] of the generator classes for i < j (TauCeti.lcsGradedPiece_one_freeProP_bijective).

TauCeti.freeProP.lcsDegreeOneBasis.{u} (p : ℕ) [Fact (Nat.Prime p)] (X : Type u) [Fintype X]
  [LinearOrder X] :
  Module.Basis { ij // ij.1 < ij.2 } ℤ_[p] (TauCeti.lcsGradedPiece (TauCeti.freeProP p X) 1)
Lean

Formalized in Tau Ceti as TauCeti.freeProP.lcsDegreeOneBasis.

Sources
LeanTauCeti.freeProP.lcsDegreeOneBasis
Used by 1
Used bygr_1 of a free pro-p group is the exterior square of gr_0

TheoremTauCeti.freeProP.finrank_lcsGradedPiece_one#

gr_1 of the free pro-p group on X has rank #X choose 2 over ℤ_p.

TauCeti.freeProP.finrank_lcsGradedPiece_one.{u} (p : ℕ) [Fact (Nat.Prime p)] (X : Type u)
  [Fintype X] :
  Module.finrank ℤ_[p] (TauCeti.lcsGradedPiece (TauCeti.freeProP p X) 1) = (Fintype.card X).choose 2
Lean

Formalized in Tau Ceti as TauCeti.freeProP.finrank_lcsGradedPiece_one.

Sources
LeanTauCeti.freeProP.finrank_lcsGradedPiece_one
Uses 1
Proof usesgr_1 of a free pro-p group is the exterior square of gr_0

DefinitionTauCeti.outerAction#

The outer action of E ⧸ N on a normal subgroup N: the class of e acts by the outer class of conjugation by e (outerAction_mk). It is well defined because conjugation by an element of N is inner.

TauCeti.outerAction.{u_1} {E : Type u_1} [Group E] [TopologicalSpace E] (N : Subgroup E) [N.Normal]
  [SeparatelyContinuousMul E] : E ⧸ N →* TauCeti.ContinuousOut ↥N
Lean

Formalized in Tau Ceti as TauCeti.outerAction.

Sources
LeanTauCeti.outerAction
Used by 1
Used byTauCeti.continuous_outerAction

TheoremTauCeti.continuous_outerAction#

For compact N, the outer action E ⧸ N → ContinuousOut N is continuous for the quotient topologies.

TauCeti.continuous_outerAction.{u_1} {E : Type u_1} [Group E] [TopologicalSpace E] {N : Subgroup E}
  [N.Normal] [IsTopologicalGroup E] [CompactSpace ↥N] : Continuous ⇑(TauCeti.outerAction N)
Lean

Formalized in Tau Ceti as TauCeti.continuous_outerAction.

Sources
LeanTauCeti.continuous_outerAction
Uses 1
Statement usesTauCeti.outerAction

DefinitionThe product decomposition of the profinite integers#

The ring homomorphism from Additive zHat to ∀ ℓ : Nat.Primes, ℤ_[ℓ] with components the ℓ-adic components zHat.component ℓ is a ring isomorphism: injective by zHat.ext_of_component and surjective by zHat.exists_forall_component_eq. It is a homeomorphism (zHat.continuous_ringEquivPiPadicInt, zHat.continuous_ringEquivPiPadicInt_symm), so an isomorphism of topological rings.

TauCeti.zHat.ringEquivPiPadicInt.{u} :
  Additive ↑TauCeti.zHat.toProfinite.toTop ≃+* ((ℓ : Nat.Primes) → ℤ_[↑ℓ])
Lean

Formalized in Tau Ceti as TauCeti.zHat.ringEquivPiPadicInt.

Sources
LeanTauCeti.zHat.ringEquivPiPadicInt
Used by 2
Used byThe section of the exponent over the principal units · The unit-group decomposition of the profinite integers

DefinitionThe unit-group decomposition of the profinite integers#

The product decomposition Additive zHat ≃+* ∀ ℓ, ℤ_[ℓ] restricts to an isomorphism of topological groups on units.

TauCeti.zHat.unitsEquivPiPadicInt.{u} :
  (Additive ↑TauCeti.zHat.toProfinite.toTop)ˣ ≃ₜ* ((ℓ : Nat.Primes) → ℤ_[↑ℓ]ˣ)
Lean

Formalized in Tau Ceti as TauCeti.zHat.unitsEquivPiPadicInt.

Sources
LeanTauCeti.zHat.unitsEquivPiPadicInt
Uses 1
Statement usesThe product decomposition of the profinite integers

TheoremEvery invertible matrix over 𝔽_p comes from a continuous automorphism of the free pro-p group of finite rank#

the automorphism of the Frattini quotient it defines lifts.

TauCeti.freeProP.continuousAutToGL_surjective.{u} {p : ℕ} [Fact (Nat.Prime p)] {X : Type u}
  [Fintype X] [DecidableEq X] : Function.Surjective ⇑(TauCeti.freeProP.continuousAutToGL p X)
Lean

Formalized in Tau Ceti as TauCeti.freeProP.continuousAutToGL_surjective.

Sources
LeanTauCeti.freeProP.continuousAutToGL_surjective
Uses 1
Proof usesBurnside's basis theorem, cardinal form

DefinitionThe profinite power#

The profinite power x ^ᶻ a of an element x of a profinite group by a profinite integer a: the value at a, read multiplicatively, of the continuous homomorphism zHat.lift x from the profinite integers to G that sends the generator to x.

TauCeti.zpowHat.{u, v} {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [TotallyDisconnectedSpace G] (x : G)
  (a : Additive ↑TauCeti.zHat.toProfinite.toTop) : G
Lean

Formalized in Tau Ceti as TauCeti.zpowHat.

Sources
LeanTauCeti.zpowHat
Used by 3
Used byIwasawa's theorem · The section of the exponent over the principal units · The ℓ-adic comparison

TheoremThe ℓ-adic comparison#

On a pro-ℓ group, the profinite power by a is Tau Ceti's ℓ-adic power by the ℓ-adic component of a.

TauCeti.zpowHat_eq_padicPow_component.{u, v} {G : Type v} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {ℓ : ℕ} [Fact (Nat.Prime ℓ)]
  (hG : TauCeti.IsProP ℓ G) (x : G) (a : Additive ↑TauCeti.zHat.toProfinite.toTop) :
  TauCeti.zpowHat x a = hG.padicPow x ((TauCeti.zHat.component ℓ) a)
Lean

Formalized in Tau Ceti as TauCeti.zpowHat_eq_padicPow_component.

Sources
LeanTauCeti.zpowHat_eq_padicPow_component
Uses 1 · Used by 1
Statement usesThe profinite power
Used byThe section of the exponent over the principal units

DefinitionThe graded Lie homomorphism of a continuous homomorphism f : G →* H#

the graded maps TauCeti.gradedMap p f hf k of all degrees, assembled into a homomorphism of graded Lie algebras ⨁ k, gr_k(G) →ₗ⁅ZMod p⁆ ⨁ k, gr_k(H). Its value on homogeneous elements is TauCeti.gradedLieHom_of.

TauCeti.gradedLieHom.{u, v} (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
  (f : G →* H) (hf : Continuous ⇑f) :
  (DirectSum ℕ fun k => TauCeti.gradedPiece p G k) →ₗ⁅ZMod p⁆
    DirectSum ℕ fun k => TauCeti.gradedPiece p H k
Lean

Formalized in Tau Ceti as TauCeti.gradedLieHom.

Sources
LeanTauCeti.gradedLieHom
Uses 1
Proof usesThe Jacobi identity

DefinitionThe ℤ_ℓ-Lie algebra of a pro-ℓ group#

For a pro-ℓ group G, the graded Lie ring ⨁ k, gr_k(G) of the lower p-series is a Lie algebra over ℤ_ℓ, for the ℤ_ℓ-module structure which in each degree is TauCeti.IsProP.gradedPieceModule: the graded bracket is ℤ_ℓ-bilinear. For p = 0 this is the ℤ_ℓ-Lie algebra of the closed lower central series.

TauCeti.IsProP.gradedLieAlgebra.{u} (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] [CompactSpace G] [TotallyDisconnectedSpace G]
  (hG : TauCeti.IsProP ℓ G) : LieAlgebra ℤ_[ℓ] (DirectSum ℕ fun k => TauCeti.gradedPiece p G k)
Lean

Formalized in Tau Ceti as TauCeti.IsProP.gradedLieAlgebra.

Sources
LeanTauCeti.IsProP.gradedLieAlgebra
Uses 1
Proof usesThe Jacobi identity

TheoremTauCeti.ContinuousAut.compactSpace#

For a topologically finitely generated profinite group, the congruence topology on the continuous automorphisms is compact: ContinuousAut G is a closed subspace of the product of the finite automorphism groups of the characteristic open quotients.

TauCeti.ContinuousAut.compactSpace.{u_1} {G : Type u_1} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
  (hG : TauCeti.IsTopologicallyFinitelyGenerated G) : CompactSpace (TauCeti.ContinuousAut G)
Lean

Formalized in Tau Ceti as TauCeti.ContinuousAut.compactSpace.

Sources
LeanTauCeti.ContinuousAut.compactSpace
Used by 1
Used byThe section of the exponent over the principal units

AbbreviationTauCeti.ClosedSubgroupConjClasses#

The closed subgroups of G up to conjugacy: the orbits of the conjugation action of G on ClosedSubgroup G.

TauCeti.ClosedSubgroupConjClasses.{u_1} (G : Type u_1) [Group G] [TopologicalSpace G]
  [SeparatelyContinuousMul G] : Type u_1
Lean

Formalized in Tau Ceti as TauCeti.ClosedSubgroupConjClasses.

Sources
LeanTauCeti.ClosedSubgroupConjClasses

TheoremThe Jacobi identity#

The Jacobi identity, with the three terms transported to the degree i + j + k + 2.

TauCeti.gradedBracket_jacobi.{u} {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G] {i j k : ℕ} (x : TauCeti.gradedPiece p G i) (y : TauCeti.gradedPiece p G j)
  (z : TauCeti.gradedPiece p G k) :
  TauCeti.gradedCast p G ⋯
          (((TauCeti.gradedBracket p G (i + j + 1) k) (((TauCeti.gradedBracket p G i j) x) y)) z) +
        TauCeti.gradedCast p G ⋯
          (((TauCeti.gradedBracket p G (j + k + 1) i) (((TauCeti.gradedBracket p G j k) y) z)) x) +
      TauCeti.gradedCast p G ⋯
        (((TauCeti.gradedBracket p G (k + i + 1) j) (((TauCeti.gradedBracket p G k i) z) x)) y) =
    0
Lean

Formalized in Tau Ceti as TauCeti.gradedBracket_jacobi.

Sources
LeanTauCeti.gradedBracket_jacobi
Used by 2
Used byThe graded Lie homomorphism of a continuous homomorphism f : G →* H · The ℤ_ℓ-Lie algebra of a pro-ℓ group

TheoremThe pro-p Nielsen–Schreier theorem#

A closed subgroup U of the free pro-p group on any type X is free pro-p on a pointed profinite space: some subset s of U converging to 1 has a topological isomorphism F_p(insert 1 s, 1) ≃ₜ* U sending the generator attached to each point of insert 1 s to that point, so that s is a basis of U converging to 1.

TauCeti.freeProP.exists_convergesToOne_continuousMulEquiv_of_isClosed.{u} {p : ℕ} {X : Type u}
  [Fact (Nat.Prime p)] {U : Subgroup (TauCeti.freeProP p X)} (hU : IsClosed ↑U) :
  ∃ s,
    TauCeti.ConvergesToOne s ∧
      ∃ e,
        ∀ (x : ↑(insert 1 s)),
          e (TauCeti.freeProCPointed.of (TauCeti.finiteGroupClassP p) ⟨1, ⋯⟩ x) = ↑x
Lean

Formalized in Tau Ceti as TauCeti.freeProP.exists_convergesToOne_continuousMulEquiv_of_isClosed.

Other forms

The pro-p Nielsen–Schreier theorem for open subgroups. Formalized in Tau Ceti as TauCeti.freeProP.nonempty_continuousMulEquiv_freeProP_openSubgroup_index.

TauCeti.freeProP.nonempty_continuousMulEquiv_freeProP_openSubgroup_index.{u} {p : ℕ} {X : Type u}
  [hp : Fact (Nat.Prime p)] [Finite X] [Nonempty X] (U : OpenSubgroup (TauCeti.freeProP p X))
  (Y : Type u) [Finite Y] (hY : Nat.card Y = 1 + (↑U).index * (Nat.card X - 1)) :
  Nonempty (↥↑U ≃ₜ* TauCeti.freeProP p Y)
Sources
LeanTauCeti.freeProP.exists_convergesToOne_continuousMulEquiv_of_isClosed · TauCeti.freeProP.nonempty_continuousMulEquiv_freeProP_openSubgroup_index
Uses 5
Proof usesDimension shifting in every positive degree · The first isomorphism theorem for a surjective strict homomorphism of topological groups · The Schreier index formula for open subgroups · Serre's theorem at arbitrary rank, as an equivalence · Shapiro's lemma in degree one

TheoremThe Schreier index formula for open subgroups#

For an open subgroup U of index m in the free pro-p group on a nonempty finite type X of cardinality n, d(U) = 1 + m * (n - 1).

TauCeti.freeProP.topologicalGeneratorRankNat_openSubgroup.{u} {p : ℕ} {X : Type u}
  [hp : Fact (Nat.Prime p)] [Finite X] [Nonempty X] (U : OpenSubgroup (TauCeti.freeProP p X)) :
  TauCeti.topologicalGeneratorRankNat ↥↑U ⋯ = 1 + (↑U).index * (Nat.card X - 1)
Lean

Formalized in Tau Ceti as TauCeti.freeProP.topologicalGeneratorRankNat_openSubgroup.

Other forms

The Schreier index formula for open subgroups, additive form. Formalized in Tau Ceti as TauCeti.freeProP.topologicalGeneratorRankNat_add_index.

TauCeti.freeProP.topologicalGeneratorRankNat_add_index.{u} {p : ℕ} {X : Type u}
  [hp : Fact (Nat.Prime p)] [Finite X] (U : OpenSubgroup (TauCeti.freeProP p X)) :
  TauCeti.topologicalGeneratorRankNat ↥↑U ⋯ + (↑U).index = 1 + (↑U).index * Nat.card X
Sources
LeanTauCeti.freeProP.topologicalGeneratorRankNat_openSubgroup · TauCeti.freeProP.topologicalGeneratorRankNat_add_index
Uses 3 · Used by 1
Proof usesBurnside's basis theorem, cardinal form · The first isomorphism theorem for a surjective strict homomorphism of topological groups · The two-term Euler formula
Used byThe pro-p Nielsen–Schreier theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.