Yamaguchi Lean 4 Library
ProCGroups.CrowellExactSequence.Applications.FiniteRank
ProCGroups/CrowellExactSequence/Applications/FiniteRank

ProCGroups.CrowellExactSequence.Applications.FiniteRank

1 Theorem | 1 Definition

Crowell exact sequences / Applications / Finite Rank.

This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.

imports
Imported by

Declarations

Definition CrowellExactSequence.finiteRank_topologicalAbelianization_sepCoordinateMap 
noncomputable def finiteRank_topologicalAbelianization_sepCoordinateMap
    {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
    (hFree : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
      (Fin r) F X) := by
  letI :
      ProCGroups.FiniteGroupClass.ContainsTrivialQuotients
        (ProCGroups.FiniteGroupClass.sigmaGroup sigma) :=
    (ProCGroups.FiniteGroupClass.sigmaGroup_fullFormation sigma).containsTrivialQuotients
  letI : TotallyDisconnectedSpace (TopologicalAbelianization F) :=
    ProCGroups.totallyDisconnectedSpace_quotient_closedNormal
      (Subgroup.closedCommutator F) (Subgroup.isClosed_closedCommutator F)
  exact
    freeProCChosenULift_sepCoordinateMap
      (H := TopologicalAbelianization F)
      (C := ProCGroups.FiniteGroupClass.sigmaGroup sigma)
      (ProCGroups.FiniteGroupClass.sigmaGroup_fullFormation sigma)
      (finiteRank_epimorphicallyFreeProCSourceData (F := F) X hFree)
      (finiteRank_epimorphicallyFreeProCSourceData_basis_card (F := F) X hFree)
      (TopologicalAbelianization.mkₜ F)
      (by
        change Function.Surjective (TopologicalAbelianization.mk F)
        exact TopologicalAbelianization.surjective_mk F)

The separated coordinate map for the topological abelianization of a finite-rank free pro-\(\Sigma\) group.

Theorem CrowellExactSequence.mem_topDerivedTop_two_of_finiteRank_topologicalAbelianization_sepCoordinateMap_eq_zero 
theorem mem_topDerivedTop_two_of_finiteRank_topologicalAbelianization_sepCoordinateMap_eq_zero
    {sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
    (hFree : ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := (ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
      (Fin r) F X)
    {a : F}
    (haψ : TopologicalAbelianization.mkₜ F a = 1)
    (hzero :
      finiteRank_topologicalAbelianization_sepCoordinateMap (F := F) X hFree
        (FoxDifferential.zcSeparatedUniversalDifferential
          (ProCGroups.FiniteGroupClass.sigmaGroup sigma)
          (TopologicalAbelianization.mkₜ F).toMonoidHom a) = 0) :
    a ∈ topDerivedTop F 2

If the separated abelianized Crowell exact-sequence coordinate vector of a kernel element vanishes, the element lies in the second closed derived subgroup.

Show Lean proof