Module

KernelInjectivity.lean

Nyll.ProCGroups.CrowellExactSequence.Profinite.KernelInjectivity

13 declarations indexed from sourceView source ↗

Module documentation

Injectivity criteria from the profinite kernel

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.

Imports1

Nyll.ProCGroups.CrowellExactSequence.Profinite.KernelBoundary

Imported by3

def

profiniteKernelAbelianizationBoundaryHomProCInteger

L33 ↗

CrowellExactSequence.profiniteKernelAbelianizationBoundaryHomProCInteger

Documentation

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

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

def

profiniteKernelAbelianizationBoundaryAddProCInteger

L45 ↗

CrowellExactSequence.profiniteKernelAbelianizationBoundaryAddProCInteger

Documentation

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

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

profiniteKernelAbelianizationBoundaryAddProCInteger_of

L59 ↗

CrowellExactSequence.profiniteKernelAbelianizationBoundaryAddProCInteger_of

Documentation

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

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

def

profiniteKernelAbelianizationBoundaryHomProCIntegerSep

L77 ↗

CrowellExactSequence.profiniteKernelAbelianizationBoundaryHomProCIntegerSep

Documentation

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.

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def profiniteKernelAbelianizationBoundaryHomProCIntegerSep
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
    ProfiniteKernelAbelianization psi →*
      Multiplicative
        (FoxDifferential.ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom)

def

profiniteKernelAbelianizationBoundaryAddProCIntegerSep

L88 ↗

CrowellExactSequence.profiniteKernelAbelianizationBoundaryAddProCIntegerSep

Documentation

Additive separated boundary from the topological kernel abelianization.

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of

L100 ↗

CrowellExactSequence.profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of

Documentation

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

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

zcDiffModuleToSep_profKerAbBoundaryAddZC

L115 ↗

CrowellExactSequence.zcDiffModuleToSep_profKerAbBoundaryAddZC

Documentation

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

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

presentedCompletedToZC_profiniteKernelAbelianizationBoundaryAdd

L155 ↗

CrowellExactSequence.presentedCompletedToZC_profiniteKernelAbelianizationBoundaryAdd

Documentation

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

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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

theorem

profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator

L188 ↗

CrowellExactSequence.profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator

Documentation

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.

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

profKerAbBoundaryAddZCSep_inj_of_kernel_le_closedCommutator

L239 ↗

CrowellExactSequence.profKerAbBoundaryAddZCSep_inj_of_kernel_le_closedCommutator

Documentation

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

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

kernel_le_closedCommutator_of_profKerAbBoundaryAddZC_inj

L294 ↗

CrowellExactSequence.kernel_le_closedCommutator_of_profKerAbBoundaryAddZC_inj

Documentation

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]}\).

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

profKerAbBoundaryAddZC_inj_iff_kernel_le_closedCommutator

L336 ↗

CrowellExactSequence.profKerAbBoundaryAddZC_inj_iff_kernel_le_closedCommutator

Documentation

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

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

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)

theorem

profKerAbBoundaryAddZC_inj_of_continuous_zcUnivDiff_kernel_le_closedCommutator

L360 ↗

CrowellExactSequence.profKerAbBoundaryAddZC_inj_of_continuous_zcUnivDiff_kernel_le_closedCommutator

Documentation

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.

Source context 7 commands

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

namespace CrowellExactSequence
noncomputable section
open ProCGroups.ProC
universe u
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

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) := by
  let hwell_dN :=
    completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff
      (G := G) (H := H) C psi hD
  exact
    profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
      (G := G) (H := H) C psi hwell_dN hker

Module documentation

Injectivity criteria from the profinite kernel

Declarations