TopologicalGeneration.lean

theorem eq_of_continuous_of_topologicallyGenerates
    (delta epsilon : CrossedHom action)
    (hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
    {s : Set G} (hsgen : TopologicallyGenerates (G := G) s)
    (hs : Set.EqOn delta epsilon s) :
    delta = epsilon

theorem eq_of_freeProC_of_continuous
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    {action : F →* Multiplicative (AddAut A)} (delta epsilon : CrossedHom action)
    (hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
    (hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
    delta = epsilon

theorem zcUniversalDifferential_kernel_le_closedCommutator_of_crossedDifferential
    (ψ : G →ₜ* H)
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
    (hkerD :
      ∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
        n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) :
    ∀ n : ProfiniteKernelSubgroup ψ,
      zcUniversalDifferential C ψ.toMonoidHom n.1 = 0 →
        n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)

instance instT1SpaceMultiplicativeTarget : T1Space (Multiplicative A)

def zcCrossedDifferentialKernelHom
    (ψ : G →ₜ* H)
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A) :
    ProfiniteKernelSubgroup ψ →* Multiplicative A where
  toFun n := Multiplicative.ofAdd (D n.1)
  map_one' := by
    rw [Submonoid.coe_one]
    exact congrArg Multiplicative.ofAdd (ScalarCrossedHom.map_one D)
  map_mul' n m := by
    apply Multiplicative.ext
    change D ((n * m : ProfiniteKernelSubgroup ψ) : G) = D n.1 + D m.1
    rw [Submonoid.coe_mul, ScalarCrossedHom.map_mul D n.1 m.1]
    have hn : ψ n.1 = 1 := n.2
    simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedGroupAlgebraScalar_apply,
        MonoidHom.coe_ofClass, hn,
  map_one, one_smul]

theorem continuous_zcCrossedDifferentialKernelHom
    (ψ : G →ₜ* H)
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
    (hcont : Continuous D) :
    Continuous (zcCrossedDifferentialKernelHom (C := C) ψ D)

def zcCrossedDifferentialProfiniteKernelAbelianizationHom
    (ψ : G →ₜ* H)
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
    (hcont : Continuous D) :
    ProfiniteKernelAbelianization ψ →* Multiplicative A

def zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
    (ψ : G →ₜ* H)
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
    (hcont : Continuous D) :
    ProfiniteKernelAbelianizationAdd ψ →+ A

theorem zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom_mk
    (ψ : G →ₜ* H)
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
    (hcont : Continuous D) (n : ProfiniteKernelSubgroup ψ) :
    zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
      (C := C) ψ D hcont
        (Additive.ofMul (QuotientGroup.mk' (Subgroup.closedCommutator _) n)) =
      D n.1

theorem zcCrossedDifferential_eq_zero_of_mem_closedCommutator
    (ψ : G →ₜ* H)
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
    (hcont : Continuous D) {n : ProfiniteKernelSubgroup ψ}
    (hn : n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) :
    D n.1 = 0

theorem zcCrossedDiffProfiniteKernelAbelianizationAddMonoidHom_inj_of_kernel_le_closedCommutator
    (ψ : G →ₜ* H)
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
    (hcont : Continuous D)
    (hker :
      ∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
        n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) :
    Function.Injective
      (zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
        (C := C) ψ D hcont)

theorem zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom_injective_iff
    {ψ : G →ₜ* H}
    (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
    (hcont : Continuous D) :
    Function.Injective
        (zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
          (C := C) ψ D hcont) ↔
      ∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
        n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)

theorem freeProCZCBoundary_of_topologicalGeneration
    {ι : X → G}
    (hgen : TopologicallyGenerates (G := G) (Set.range ι))
    (ψ : G →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
    (hbasis :
      ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (g : G) :
    freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)) (delta g) =
      zcCompletedGroupAlgebraBoundary C ψ g := by
  let beta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCCompletedGroupAlgebra C H) :=
    delta.mapLinear
      (freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)))
  have hbeta_continuous : Continuous beta :=
    (continuous_freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x))).comp hdelta_continuous
  have hboundary_continuous : Continuous (zcCompletedGroupAlgebraBoundary C ψ) :=
    continuous_zcCompletedGroupAlgebraBoundary (C := C) (G := H) ψ hψ_continuous
  have hEqOn :
      Set.EqOn beta (zcCompletedGroupAlgebraBoundary C ψ) (Set.range ι) := by
    intro y hy
    rcases hy with ⟨x, rfl⟩
    change
      freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)) (delta (ι x)) =
        zcGroupLike C H (ψ (ι x)) - 1
    rw [hbasis x, freeProCZCCompletedFoxBoundary_single]
  have hEq :=
    CrossedHom.eq_of_continuous_of_topologicallyGenerates
      beta (zcCompletedGroupAlgebraBoundary C ψ)
      hbeta_continuous hboundary_continuous hgen hEqOn
  exact congrArg
    (fun d : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCCompletedGroupAlgebra C H) => d g) hEq

theorem exact_zcCrossedDiffKernelAddMonoidHom_freeProCZCCompletedFoxBoundary_of_surj_semi
    (φ : X → H)
    (ψ : G →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hboundary :
      ∀ g : G,
        freeProCZCCompletedFoxBoundary C φ (delta g) =
          zcCompletedGroupAlgebraBoundary C ψ g)
    (hgraph :
      Function.Surjective
        (fun g : G =>
          ({ left := delta g, right := ψ g } :
            ZCCompletedFoxSemidirect C X H))) :
    Function.Exact
      (ScalarCrossedHom.restrictTrivialSubgroupAddMonoidHom
        delta ψ.ker
        (zcCompletedGroupAlgebraScalar_subtype_ker (C := C) (ψ := ψ)))
      (freeProCZCCompletedFoxBoundary C φ) := by
  intro v
  constructor
  · intro hv
    rcases hgraph
        ({ left := v, right := 1 } :
          ZCCompletedFoxSemidirect C X H) with
      ⟨g, hg⟩
    have hdelta_g : delta g = v := congrArg ZCCompletedFoxSemidirect.left hg
    have hψ_g : ψ g = 1 := congrArg ZCCompletedFoxSemidirect.right hg
    refine ⟨Additive.ofMul (⟨g, hψ_g⟩ : ψ.ker), ?_⟩
    simp only [ScalarCrossedHom.restrictTrivialSubgroupAddMonoidHom_apply, hdelta_g]
  · rintro ⟨n, hn⟩
    rw [← hn]
    change
      freeProCZCCompletedFoxBoundary C φ
        (delta (((Additive.toMul n : ψ.ker) : G))) = 0
    rw [hboundary (((Additive.toMul n : ψ.ker) : G))]
    exact zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
      (C := C) (ψ := ψ) (g := ((Additive.toMul n : ψ.ker) : G))
      (Additive.toMul n).2

theorem zcCompletedFoxSemidirect_surjective_forces_generator_boundary_zero
    (φ : X → H)
    (ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
    (hboundary :
      ∀ g : G,
        freeProCZCCompletedFoxBoundary C φ (delta g) =
          zcCompletedGroupAlgebraBoundary C ψ g)
    (hgraph :
      Function.Surjective
        (fun g : G =>
          ({ left := delta g, right := ψ g } :
            ZCCompletedFoxSemidirect C X H))) (x : X) :
    zcGroupLike C H (φ x) - 1 = 0 := by
  classical
  rcases hgraph
      ({ left := Pi.single x (1 : ZCCompletedGroupAlgebra C H), right := 1 } :
        ZCCompletedFoxSemidirect C X H) with
    ⟨g, hg⟩
  have hdelta_g : delta g = Pi.single x (1 : ZCCompletedGroupAlgebra C H) :=
    congrArg ZCCompletedFoxSemidirect.left hg
  have hψ_g : ψ g = 1 := congrArg ZCCompletedFoxSemidirect.right hg
  calc
    zcGroupLike C H (φ x) - 1 =
        freeProCZCCompletedFoxBoundary C φ
          (Pi.single x (1 : ZCCompletedGroupAlgebra C H)) := by
      rw [freeProCZCCompletedFoxBoundary_single]
    _ = freeProCZCCompletedFoxBoundary C φ (delta g) := by rw [hdelta_g]
    _ = zcCompletedGroupAlgebraBoundary C ψ g := hboundary g
    _ = 0 := zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker C ψ hψ_g

theorem exact_zcKernelAdd_freeProCZCFoxBoundary_of_topGen
    {ι : X → G}
    (hgen : TopologicallyGenerates (G := G) (Set.range ι))
    (ψ : G →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
    (hbasis :
      ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (hgraph :
      Function.Surjective
        (fun g : G =>
          ({ left := delta g, right := ψ g } :
            ZCCompletedFoxSemidirect C X H))) :
    Function.Exact
      (ScalarCrossedHom.restrictTrivialSubgroupAddMonoidHom
        delta ψ.ker
        (zcCompletedGroupAlgebraScalar_subtype_ker (C := C) (ψ := ψ)))
      (freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x))) := by
  exact
    exact_zcCrossedDiffKernelAddMonoidHom_freeProCZCCompletedFoxBoundary_of_surj_semi
      (C := C) (X := X) (G := G) (H := H)
      (fun x : X => ψ (ι x)) ψ delta
      (freeProCZCBoundary_of_topologicalGeneration
        (C := C) (X := X) (G := G) (H := H)
        hgen ψ delta hdelta_continuous hψ_continuous hbasis)
      hgraph

theorem freeProCZCFundamentalFormula_of_topologicalGeneration
    {ι : X → G}
    (hgen : TopologicallyGenerates (G := G) (Set.range ι))
    (ψ : G →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
    (hbasis :
      ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (g : G) :
    zcCompletedGroupAlgebraBoundary C ψ g =
      ∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1)

theorem freeProCZCFundamentalFormula_stage_of_topologicalGeneration
    {ι : X → G}
    (hgen : TopologicallyGenerates (G := G) (Set.range ι))
    (ψ : G →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
    (hbasis :
      ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (j : ZCCompletedGroupAlgebraIndex C H) (g : G) :
    zcCompletedGroupAlgebraProjection C H j
        (zcCompletedGroupAlgebraBoundary C ψ g) =
      zcCompletedGroupAlgebraProjection C H j
        (∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1))

theorem freeProCZCEulerFormula_of_topologicalGeneration
    {ι : X → G}
    (hgen : TopologicallyGenerates (G := G) (Set.range ι))
    (ψ : G →* H)
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
    (hbasis :
      ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
    (g : G) :
    zcGroupLike C H (ψ g) - 1 =
      ∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1)

theorem freeProCZCCompletedCrossedDifferential_ext_of_continuous
    {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
    (ψ : F →* H)
    (delta epsilon :
      ScalarCrossedHom
        (zcCompletedGroupAlgebraScalar C ψ)
        (ZCFreeFoxCoordinates C (X := X) (H := H)))
    (hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
    (hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
    delta = epsilon