NYLL
Module

FiniteRank.lean

Nyll.ProCGroups.CrowellExactSequence.Applications.FiniteRank
2 declarations indexed from sourceView source ↗

Module documentation

ProCGroups.CrowellExactSequence.Applications.FiniteRank

Crowell exact sequences / Applications / Finite Rank.

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

Imports4
Imported by1

Declarations

def

finiteRank_topologicalAbelianization_sepCoordinateMap

L37 ↗
CrowellExactSequence.finiteRank_topologicalAbelianization_sepCoordinateMap
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CrowellExactSequence
open ProCGroups.Abelian
open ProCGroups.FiniteStepSolvableQuotients
universe u
variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
Lean source · statement
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)
theorem

mem_topDerivedTop_two_of_finiteRank_topologicalAbelianization_sepCoordinateMap_eq_zero

L65 ↗
CrowellExactSequence.mem_topDerivedTop_two_of_finiteRank_topologicalAbelianization_sepCoordinateMap_eq_zero
Documentation

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

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CrowellExactSequence
open ProCGroups.Abelian
open ProCGroups.FiniteStepSolvableQuotients
universe u
variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
Lean source · statement
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

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.