Yamaguchi Lean 4 Library
ProCGroups.CrowellExactSequence.Profinite.KernelInjectivity
ProCGroups/CrowellExactSequence/Profinite/KernelInjectivity

ProCGroups.CrowellExactSequence.Profinite.KernelInjectivity

9 Theorems | 4 Definitions

This file factors the completed Crowell boundary through the topological abelianization of the kernel. It proves that the resulting boundary is annihilated by the completed differential map and records the Magnus-kernel criteria used to establish injectivity in the profinite sequence.

import
Imported by

Declarations

Definition CrowellExactSequence.profiniteKernelAbelianizationBoundaryHomProCInteger 
def profiniteKernelAbelianizationBoundaryHomProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (hwell_dN :
      CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
    ProfiniteKernelAbelianization psi →*
      Multiplicative (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom) :=
  QuotientGroup.lift
    (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)))
    (completedKernelBoundaryProCInteger (G := G) (H := H) C psi)
    hwell_dN

Boundary from the topological kernel abelianization to \(A_{\psi}(C)\), assuming the displayed boundary kills \(\overline{[N,N]}\).

Definition CrowellExactSequence.profiniteKernelAbelianizationBoundaryAddProCInteger 
def profiniteKernelAbelianizationBoundaryAddProCInteger
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (hwell_dN :
      CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
    ProfiniteKernelAbelianizationAdd psi →+
      FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom :=
  (profiniteKernelAbelianizationBoundaryHomProCInteger
    (G := G) (H := H) C psi hwell_dN).toAdditiveLeft

Additive boundary from the topological kernel abelianization to \(A_{\psi}(C)\).

Theorem CrowellExactSequence.profiniteKernelAbelianizationBoundaryAddProCInteger_of 
@[simp]
theorem profiniteKernelAbelianizationBoundaryAddProCInteger_of
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (hwell_dN :
      CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
    (n : ProfiniteKernelSubgroup psi) :
    profiniteKernelAbelianizationBoundaryAddProCInteger
        (G := G) (H := H) C psi hwell_dN
        (Additive.ofMul
          (QuotientGroup.mk'
            (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
      FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1

The \(\mathbb{Z}_C\)-coefficient boundary map is obtained from the profinite kernel abelianization boundary construction.

Show Lean proof
Definition CrowellExactSequence.profiniteKernelAbelianizationBoundaryHomProCIntegerSep 
def profiniteKernelAbelianizationBoundaryHomProCIntegerSep
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    ProfiniteKernelAbelianization psi →*
      Multiplicative
        (FoxDifferential.ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
  QuotientGroup.lift
    (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)))
    (separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi)
    (separatedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)

Separated boundary from the topological kernel abelianization to the finite-stage separated completed differential module. Unlike the algebraic target, this map is well-defined without a separate closedness or continuity hypothesis.

Definition CrowellExactSequence.profiniteKernelAbelianizationBoundaryAddProCIntegerSep 
def profiniteKernelAbelianizationBoundaryAddProCIntegerSep
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    ProfiniteKernelAbelianizationAdd psi →+
      FoxDifferential.ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
  (profiniteKernelAbelianizationBoundaryHomProCIntegerSep
    (G := G) (H := H) C psi).toAdditiveLeft

Additive separated boundary from the topological kernel abelianization.

Theorem CrowellExactSequence.profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of 
@[simp]
theorem profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (n : ProfiniteKernelSubgroup psi) :
    profiniteKernelAbelianizationBoundaryAddProCIntegerSep
        (G := G) (H := H) C psi
        (Additive.ofMul
          (QuotientGroup.mk'
            (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
      FoxDifferential.zcSeparatedUniversalDifferential C psi.toMonoidHom n.1

The separated \(\mathbb{Z}_C\)-coefficient boundary map is obtained from the profinite kernel abelianization boundary construction.

Show Lean proof
Theorem CrowellExactSequence.zcDiffModuleToSep_profKerAbBoundaryAddZC 
theorem zcDiffModuleToSep_profKerAbBoundaryAddZC
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (hwell_dN :
      CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
    (x : ProfiniteKernelAbelianizationAdd psi) :
    FoxDifferential.zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom
        (profiniteKernelAbelianizationBoundaryAddProCInteger
          (G := G) (H := H) C psi hwell_dN x) =
      profiniteKernelAbelianizationBoundaryAddProCIntegerSep
        (G := G) (H := H) C psi x

The map from the completed differential module to its separated quotient carries the kernel-abelianization boundary to its separated version.

Show Lean proof
Theorem CrowellExactSequence.presentedCompletedToZC_profiniteKernelAbelianizationBoundaryAdd 
theorem presentedCompletedToZC_profiniteKernelAbelianizationBoundaryAdd
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (hwell_dN :
      CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
    (x : ProfiniteKernelAbelianizationAdd psi) :
    presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
        (profiniteKernelAbelianizationBoundaryAddProCInteger
          (G := G) (H := H) C psi hwell_dN x) =
      0

The completed Crowell differential map vanishes on the image of the profinite-kernel abelianization boundary.

Show Lean proof
Theorem CrowellExactSequence.profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator 
theorem profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (hwell_dN :
      CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
    (hker :
      ∀ n : ProfiniteKernelSubgroup psi,
        FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
          n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
    Function.Injective
      (profiniteKernelAbelianizationBoundaryAddProCInteger
        (G := G) (H := H) C psi hwell_dN)

Magnus-kernel criterion form of injectivity for the genuine topological kernel boundary. In paper language this is the step \(ker(D|_N) = \overline{[N,N]} \mapsto d_N: N^{\mathrm{ab}}(C) \to A_{\psi}(C)\) is injective.

Show Lean proof
Theorem CrowellExactSequence.profKerAbBoundaryAddZCSep_inj_of_kernel_le_closedCommutator 
theorem profKerAbBoundaryAddZCSep_inj_of_kernel_le_closedCommutator
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (hker :
      ∀ n : ProfiniteKernelSubgroup psi,
        FoxDifferential.zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = 0 →
          n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
    Function.Injective
      (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
        (G := G) (H := H) C psi)

Magnus-kernel criterion form of injectivity for the separated topological kernel boundary.

Show Lean proof
Theorem CrowellExactSequence.kernel_le_closedCommutator_of_profKerAbBoundaryAddZC_inj 
theorem kernel_le_closedCommutator_of_profKerAbBoundaryAddZC_inj
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    (hwell_dN :
      CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
    (hinj :
      Function.Injective
        (profiniteKernelAbelianizationBoundaryAddProCInteger
          (G := G) (H := H) C psi hwell_dN)) :
    ∀ n : ProfiniteKernelSubgroup psi,
      FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
        n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)

Injectivity of the genuine topological kernel boundary is exactly the Magnus-kernel criterion in the reverse direction. In paper language this says that once \(d_N: N^{\mathrm{ab}}(C) \to A_{\psi}(C)\) is known to be injective, an element of ker \(\psi\) whose completed Fox differential vanishes is already in \(\overline{[N,N]}\).

Show Lean proof
Theorem CrowellExactSequence.profKerAbBoundaryAddZC_inj_iff_kernel_le_closedCommutator 
theorem profKerAbBoundaryAddZC_inj_iff_kernel_le_closedCommutator
    {C : ProCGroups.FiniteGroupClass.{u}} {psi : ContinuousMonoidHom G H}
    (hwell_dN :
      CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
    Function.Injective
        (profiniteKernelAbelianizationBoundaryAddProCInteger
          (G := G) (H := H) C psi hwell_dN) ↔
      ∀ n : ProfiniteKernelSubgroup psi,
        FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
          n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)

Injectivity of \(d_N: N^{\mathrm{ab}}(C) \to A_{\psi}(C)\) is equivalent to the continuous Magnus-kernel criterion.

Show Lean proof
Theorem CrowellExactSequence.profKerAbBoundaryAddZC_inj_of_continuous_zcUnivDiff_kernel_le_closedCommutator 
theorem profKerAbBoundaryAddZC_inj_of_continuous_zcUnivDiff_kernel_le_closedCommutator
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    [TopologicalSpace (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom)]
    [T1Space (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom)]
    (hD : Continuous
      (fun g : G => FoxDifferential.zcUniversalDifferential C psi.toMonoidHom g))
    (hker :
      ∀ n : ProfiniteKernelSubgroup psi,
        FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
          n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
    let hwell_dN :=
      completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff
        (G := G) (H := H) C psi hD
    Function.Injective
      (profiniteKernelAbelianizationBoundaryAddProCInteger
        (G := G) (H := H) C psi hwell_dN)

Continuous-boundary version of the Magnus-kernel injectivity criterion. This packages the two paper steps that \(d_N\) is well-defined and that \(\ker D|_N \leq \overline{[N,N]}\): continuity of the completed universal differential supplies well-definedness, and the kernel criterion supplies injectivity of the resulting genuine boundary map.

Show Lean proof