Exactness.lean

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

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

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] (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) := by
  let dN :=
    profiniteKernelAbelianizationBoundaryAddProCIntegerSep
      (G := G) (H := H) C psi
  let delta :=
    presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
      (G := G) (H := H) C hC psi
  let blDelta :=
    blanchfieldLyndonFiniteFamilyMap
      (R := ZCCompletedGroupAlgebra C H)
      (fun i : X =>
        presentedCompletedDifferentialBoundaryProCInteger
          (G := G) (H := H) C psi (family i))
  have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
    rw [hcoords_symm]
    exact
      presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
        (G := G) (H := H) C hC psi family
  have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
    have h := congrArg (fun f => f y) hblDelta_comp
    change delta (coords.symm y) = blDelta y at h
    exact h.symm
  change Function.Exact dN delta
  intro a
  constructor
  · intro ha
    have hcoord_cycle : blDelta (coords a) = 0 := by
      calc
        blDelta (coords a) = delta (coords.symm (coords a)) := hblDelta_apply (coords a)
        _ = delta a := by rw [coords.symm_apply_apply]
        _ = 0 := ha
    rcases hcycle_lift (coords a) hcoord_cycle with ⟨n, hncoords⟩
    refine ⟨Additive.ofMul
      (QuotientGroup.mk'
        (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n), ?_⟩
    apply coords.injective
    calc
      coords
          (dN (Additive.ofMul
            (QuotientGroup.mk'
              (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
          coords (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) := by
            rw [profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of]
      _ = Dcoords n.1 := (hDcoords_kernel n).symm
      _ = coords a := hncoords
  · rintro ⟨x, hx⟩
    rw [← hx]
    exact
      presentedSepToZC_profiniteKernelAbelianizationBoundaryAddSep
        (G := G) (H := H) C hC psi x

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 := by
  let Dclosed : G → ZCFreeFoxCoordinates C (X := X) (H := H) :=
    fun g =>
      freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
        (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
  refine
    completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords_fintype
      (G := G) (H := H) C psi family hbasis_A Dclosed ?_ ?_
  · simpa [Dclosed] using
      continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
        (C := C) X H hfree (fun i : X => psi (family i)) htarget hφconv
  · intro n
    exact hleft_graph_eq n.1