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

ProCGroups.CrowellExactSequence.Profinite.Exactness

4 Theorems

This file reduces exactness at the separated completed differential module to integration of coordinate cycles. It derives the middle image/kernel equality from finite-stage lifts and proves the required boundary vanishing under the closed-generator graph hypothesis.

imports
Imported by

Declarations

Theorem CrowellExactSequence.presentedSepToZC_profiniteKernelAbelianizationBoundaryAddSep 
theorem presentedSepToZC_profiniteKernelAbelianizationBoundaryAddSep
    (C : ProCGroups.FiniteGroupClass.{u})
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    (x : ProfiniteKernelAbelianizationAdd psi) :
    presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
        (G := G) (H := H) C hC psi
        (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
          (G := G) (H := H) C psi x) =
      0

The separated displayed boundary kills the separated kernel boundary.

Show Lean proof
Theorem CrowellExactSequence.exact_boundaryAddZC_sep_iff_delta_cycles_integrate 
theorem exact_boundaryAddZC_sep_iff_delta_cycles_integrate
    {C : ProCGroups.FiniteGroupClass.{u}}
    {hC : ProCGroups.FiniteGroupClass.Hereditary C}
    {psi : ContinuousMonoidHom G H} :
    Function.Exact
        (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
          (G := G) (H := H) C psi)
        (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
          (G := G) (H := H) C hC psi) ↔
      ∀ a : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom,
        presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
            (G := G) (H := H) C hC psi a = 0 →
          ∃ n : ProfiniteKernelSubgroup psi,
            zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = a

Exactness of the separated additive boundary is equivalent to integrability of all separated delta cycles.

Show Lean proof
Theorem CrowellExactSequence.exact_boundaryAddZC_sep_of_coord_cycle_lift 
theorem exact_boundaryAddZC_sep_of_coord_cycle_lift
    (C : ProCGroups.FiniteGroupClass.{u})
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (psi : ContinuousMonoidHom G H)
    {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
    (coords :
      ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom ≃ₗ[
        ZCCompletedGroupAlgebra C H]
        ZCFreeFoxCoordinates C (X := X) (H := H))
    (hcoords_symm :
      coords.symm.toLinearMap =
        presentedSeparatedDifferentialFamilyMapProCInteger
          (G := G) (H := H) C psi family)
    (Dcoords : G → ZCFreeFoxCoordinates C (X := X) (H := H))
    (hDcoords_kernel :
      ∀ n : ProfiniteKernelSubgroup psi,
        Dcoords n.1 =
          coords (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1))
    (hcycle_lift :
      ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
        blanchfieldLyndonFiniteFamilyMap
            (R := ZCCompletedGroupAlgebra C H)
            (fun i : X =>
              presentedCompletedDifferentialBoundaryProCInteger
                (G := G) (H := H) C psi (family i)) v = 0 →
          ∃ n : ProfiniteKernelSubgroup psi, Dcoords n.1 = v) :
    Function.Exact
      (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
        (G := G) (H := H) C psi)
      (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
        (G := G) (H := H) C hC psi)

A coordinate lift for each cycle gives exactness of the separated additive boundary sequence.

Show Lean proof
Theorem CrowellExactSequence.completedBoundaryKillsTopCommZC_of_closedGen_leftGraph 
theorem completedBoundaryKillsTopCommZC_of_closedGen_leftGraph
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
    {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
    [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
    (hbasis_A :
      IsPresentedCompletedDifferentialFamilyBasisProCInteger
        (G := G) (H := H) C psi family)
    (hfree :
      ProCGroups.FreeProC.IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) X G family)
    (htarget :
      HasOpenNormalBasisInClass C
        (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
          (C := C) (fun i : X => psi (family i)) : Subgroup
            (ZCCompletedFoxSemidirect C X H)))
    (hφconv :
      ProCGroups.FreeProC.FamilyConvergesToOneAlongOpenSubgroups
        (G :=
          (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
            (C := C) (fun i : X => psi (family i)) : Subgroup
              (ZCCompletedFoxSemidirect C X H)))
        (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
          (C := C) (fun i : X => psi (family i))))
    (hleft_graph_eq :
      ∀ g : G,
        freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
            (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g =
          presentedCompletedDifferentialFamilyCoordinatesProCInteger
            (G := G) (H := H) C psi family hbasis_A
            (zcUniversalDifferential C psi.toMonoidHom g)) :
    CompletedBoundaryKillsTopologicalCommutatorProCInteger
      (G := G) (H := H) C psi

Agreement of the closed-generated Magnus coordinates with the presented differential coordinates forces the completed kernel boundary to kill the closed commutator subgroup.

Show Lean proof