Naturality.lean

def zcCompletedGroupAlgebraMapStage
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
    ZCCompletedGroupAlgebraStage C H
        (i.1, completedGroupAlgebraComapIndexInClass
          (G := H) (H := K) C hC φ i.2) →+*
      ZCCompletedGroupAlgebraStage C K i

theorem zcCompletedGroupAlgebraMapStage_of
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
    (q : CompletedGroupAlgebraQuotientInClass H C
      (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)) :
    zcCompletedGroupAlgebraMapStage C hC φ i
        (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _ q) =
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _
        (completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2 q)

theorem zcCompletedGroupAlgebraMapStage_single
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
    (q : CompletedGroupAlgebraQuotientInClass H C
      (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
    (a : ModNCompletedCoeff i.1.modulus) :
    zcCompletedGroupAlgebraMapStage C hC φ i (MonoidAlgebra.single q a) =
      MonoidAlgebra.single
        (completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2 q) a

theorem zcCompletedGroupAlgebraMapStage_surjective_of_surjective
    (φ : H →ₜ* K) (hφ : Function.Surjective φ)
    (i : ZCCompletedGroupAlgebraIndex C K) :
    Function.Surjective (zcCompletedGroupAlgebraMapStage C hC φ i)

theorem zcCompletedGroupAlgebraMapStage_smul
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
    (a : ModNCompletedCoeff i.1.modulus)
    (x :
      ZCCompletedGroupAlgebraStage C H
        (i.1, completedGroupAlgebraComapIndexInClass
          (G := H) (H := K) C hC φ i.2)) :
    zcCompletedGroupAlgebraMapStage C hC φ i (a • x) =
      a • zcCompletedGroupAlgebraMapStage C hC φ i x

def zcCompletedGroupAlgebraMapStageKernelIdeal
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
    Ideal
      (ZCCompletedGroupAlgebraStage C H
        (i.1, completedGroupAlgebraComapIndexInClass
          (G := H) (H := K) C hC φ i.2))

theorem mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff
    {C : ProCGroups.FiniteGroupClass.{u}} {hC : C.Hereditary}
    {φ : H →ₜ* K} {i : ZCCompletedGroupAlgebraIndex C K}
    {x :
      ZCCompletedGroupAlgebraStage C H
        (i.1, completedGroupAlgebraComapIndexInClass
          (G := H) (H := K) C hC φ i.2)} :
    x ∈ zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i ↔
      zcCompletedGroupAlgebraMapStage C hC φ i x = 0

def zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
    (q :
      (completedGroupAlgebraComapQuotientMapInClass
        (G := H) (H := K) C hC φ i.2).ker) :
    ZCCompletedGroupAlgebraStage C H
      (i.1, completedGroupAlgebraComapIndexInClass
        (G := H) (H := K) C hC φ i.2)

def zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
    Ideal
      (ZCCompletedGroupAlgebraStage C H
        (i.1, completedGroupAlgebraComapIndexInClass
          (G := H) (H := K) C hC φ i.2))

theorem zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator_mem_kernelIdeal
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
    (q :
      (completedGroupAlgebraComapQuotientMapInClass
        (G := H) (H := K) C hC φ i.2).ker) :
    zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC φ i q ∈
      zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i

theorem zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal_le_kernelIdeal
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
    zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i ≤
      zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i

def zcCompletedGroupAlgebraMapStageTargetSection
    (φ : H →ₜ* K) (hφ : Function.Surjective φ)
    (i : ZCCompletedGroupAlgebraIndex C K) :
    ZCCompletedGroupAlgebraStage C K i →ₗ[ModNCompletedCoeff i.1.modulus]
      ZCCompletedGroupAlgebraStage C H
        (i.1, completedGroupAlgebraComapIndexInClass
          (G := H) (H := K) C hC φ i.2)

theorem zcCompletedGroupAlgebraMapStageTargetSection_of
    (φ : H →ₜ* K) (hφ : Function.Surjective φ)
    (i : ZCCompletedGroupAlgebraIndex C K)
    (q : CompletedGroupAlgebraQuotientInClass K C i.2) :
    zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
        (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass K C i.2) q) =
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C
          (completedGroupAlgebraComapIndexInClass
            (G := H) (H := K) C hC φ i.2))
        (Function.surjInv
          (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
            (G := H) (H := K) C hC φ hφ i.2) q)

theorem zcCompletedGroupAlgebraMapStage_targetSection
    (φ : H →ₜ* K) (hφ : Function.Surjective φ)
    (i : ZCCompletedGroupAlgebraIndex C K)
    (y : ZCCompletedGroupAlgebraStage C K i) :
    zcCompletedGroupAlgebraMapStage C hC φ i
        (zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i y) = y

theorem zcCompletedGAMapStage_sourceBasis_sub_targetSection_mem_relationAugmentationIdeal
    (φ : H →ₜ* K) (hφ : Function.Surjective φ)
    (i : ZCCompletedGroupAlgebraIndex C K)
    (s :
      CompletedGroupAlgebraQuotientInClass H C
        (completedGroupAlgebraComapIndexInClass
          (G := H) (H := K) C hC φ i.2)) :
    MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
        (CompletedGroupAlgebraQuotientInClass H C
          (completedGroupAlgebraComapIndexInClass
            (G := H) (H := K) C hC φ i.2)) s -
      zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
        (zcCompletedGroupAlgebraMapStage C hC φ i
          (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass H C
              (completedGroupAlgebraComapIndexInClass
                (G := H) (H := K) C hC φ i.2)) s)) ∈
      zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i

theorem zcCompletedGAMapStage_sub_targetSection_map_mem_relationAugmentationIdeal
    (φ : H →ₜ* K) (hφ : Function.Surjective φ)
    (i : ZCCompletedGroupAlgebraIndex C K)
    (x :
      ZCCompletedGroupAlgebraStage C H
        (i.1, completedGroupAlgebraComapIndexInClass
          (G := H) (H := K) C hC φ i.2)) :
    x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
        (zcCompletedGroupAlgebraMapStage C hC φ i x) ∈
      zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i

theorem zcCompletedGAMapStageKernelIdeal_eq_relationAugmentationIdeal_of_surj
    (φ : H →ₜ* K) (hφ : Function.Surjective φ)
    (i : ZCCompletedGroupAlgebraIndex C K) :
    zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i =
      zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i

theorem zcCompletedGroupAlgebraMapStage_compatible
    (φ : H →ₜ* K)
    {i j : ZCCompletedGroupAlgebraIndex C K} (hij : i ≤ j) :
    (zcCompletedGroupAlgebraTransition C K hij).comp
        (zcCompletedGroupAlgebraMapStage C hC φ j) =
      (zcCompletedGroupAlgebraMapStage C hC φ i).comp
        (zcCompletedGroupAlgebraTransition C H
          (show
            (i.1, completedGroupAlgebraComapIndexInClass
                (G := H) (H := K) C hC φ i.2) ≤
              (j.1, completedGroupAlgebraComapIndexInClass
                (G := H) (H := K) C hC φ j.2) from
            ⟨hij.1,
              completedGroupAlgebraComapIndexInClass_mono
                (G := H) (H := K) C hC φ hij.2⟩)) := by
  let : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
  let : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
  apply RingHom.ext
  intro x
  refine MonoidAlgebra.induction_on
    (motive := fun x =>
      ((zcCompletedGroupAlgebraTransition C K hij).comp
          (zcCompletedGroupAlgebraMapStage C hC φ j)) x =
        ((zcCompletedGroupAlgebraMapStage C hC φ i).comp
          (zcCompletedGroupAlgebraTransition C H
            (show
              (i.1, completedGroupAlgebraComapIndexInClass
                  (G := H) (H := K) C hC φ i.2) ≤
                (j.1, completedGroupAlgebraComapIndexInClass
                  (G := H) (H := K) C hC φ j.2) from
              ⟨hij.1,
                completedGroupAlgebraComapIndexInClass_mono
                  (G := H) (H := K) C hC φ hij.2⟩))) x)
    x ?_ ?_ ?_
  · intro q
    rw [RingHom.comp_apply, RingHom.comp_apply,
      zcCompletedGroupAlgebraMapStage_of, zcCompletedGroupAlgebraTransition_of,
      zcCompletedGroupAlgebraTransition_of]
    change
      MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass K C i.2)
          ((OpenNormalSubgroupInClass.map
            (C := C) (G := K)
            (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
            (completedGroupAlgebraComapQuotientMapInClass
              (G := H) (H := K) C hC φ j.2 q)) =
        zcCompletedGroupAlgebraMapStage C hC φ i
          (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
            (CompletedGroupAlgebraQuotientInClass H C
              (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
            ((OpenNormalSubgroupInClass.map
              (C := C) (G := H)
              (U := OrderDual.ofDual
                (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
              (V := OrderDual.ofDual
                (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2))
              (completedGroupAlgebraComapIndexInClass_mono
                (G := H) (H := K) C hC φ hij.2)) q))
    erw [zcCompletedGroupAlgebraMapStage_of]
    exact congrArg (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
      (CompletedGroupAlgebraQuotientInClass K C i.2))
      (congrFun
        (congrArg DFunLike.coe
          (completedGroupAlgebraComapQuotientMapInClass_compatible
            (G := H) (H := K) C hC φ hij.2)) q)
  · intro x y hx hy
    rw [map_add, map_add, hx, hy]
  · intro a x hx
    rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
    rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
    simp only [zcCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMapInClass,
  modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, zcCompletedGroupAlgebraMapStage,
      map_intCast,
  RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply]

def zcCompletedGroupAlgebraMap (φ : H →ₜ* K) :
    ZCCompletedGroupAlgebra C H →+* ZCCompletedGroupAlgebra C K where
  toFun x := ⟨fun i =>
      zcCompletedGroupAlgebraMapStage C hC φ i
        (zcCompletedGroupAlgebraProjection C H
          (i.1, completedGroupAlgebraComapIndexInClass
            (G := H) (H := K) C hC φ i.2) x), by
    intro i j hij
    let hsource :
        (i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2) ≤
          (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) :=
      ⟨hij.1, completedGroupAlgebraComapIndexInClass_mono
        (G := H) (H := K) C hC φ hij.2⟩
    have hx := x.2
      (i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)
      (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2)
      hsource
    have hcompat := congrFun
      (congrArg DFunLike.coe
        (zcCompletedGroupAlgebraMapStage_compatible C hC φ hij))
      (zcCompletedGroupAlgebraProjection C H
        (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x)
    rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
    rw [hx] at hcompat
    simpa using hcompat⟩
  map_zero' := by
    apply Subtype.ext
    funext i
    simp only [zcCompletedGroupAlgebraMapStage, zcCompletedGroupAlgebraProjection_zero,
      MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_zero]
  map_add' := by
    intro x y
    apply Subtype.ext
    funext i
    simp only [zcCompletedGroupAlgebraProjection_add, map_add]
  map_one' := by
    apply Subtype.ext
    funext i
    simp only [zcCompletedGroupAlgebraMapStage, zcCompletedGroupAlgebraProjection_one,
  MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_one]
  map_mul' := by
    intro x y
    apply Subtype.ext
    funext i
    simp only [zcCompletedGroupAlgebraProjection_mul, map_mul]

theorem zcCompletedGroupAlgebraProjection_map
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
    (x : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraProjection C K i (zcCompletedGroupAlgebraMap C hC φ x) =
      zcCompletedGroupAlgebraMapStage C hC φ i
        (zcCompletedGroupAlgebraProjection C H
          (i.1, completedGroupAlgebraComapIndexInClass
            (G := H) (H := K) C hC φ i.2) x)

theorem mem_zcCompletedGroupAlgebraMap_ker_iff_stageKernelIdeal
    {C : ProCGroups.FiniteGroupClass.{u}} {hC : C.Hereditary}
    {φ : H →ₜ* K} {x : ZCCompletedGroupAlgebra C H} :
    x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC φ) ↔
      ∀ i : ZCCompletedGroupAlgebraIndex C K,
        zcCompletedGroupAlgebraProjection C H
            (i.1, completedGroupAlgebraComapIndexInClass
              (G := H) (H := K) C hC φ i.2) x ∈
          zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i

theorem mem_zcCompletedGAMap_ker_iff_stageRelationAugmentationIdeal_of_surj
    {C : ProCGroups.FiniteGroupClass.{u}} {hC : C.Hereditary}
    {φ : H →ₜ* K} (hφ : Function.Surjective φ)
    {x : ZCCompletedGroupAlgebra C H} :
    x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC φ) ↔
      ∀ i : ZCCompletedGroupAlgebraIndex C K,
        zcCompletedGroupAlgebraProjection C H
            (i.1, completedGroupAlgebraComapIndexInClass
              (G := H) (H := K) C hC φ i.2) x ∈
          zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i

theorem zcCompletedGroupAlgebraMap_groupLike
    (φ : H →ₜ* K) (h : H) :
    zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H h) =
      zcGroupLike C K (φ h)

theorem zcCompletedGroupAlgebraMap_scalar
    {G : Type v} [Group G] (φ : H →ₜ* K) (ψ : G →* H) (g : G) :
    zcCompletedGroupAlgebraMap C hC φ (zcCompletedGroupAlgebraScalar C ψ g) =
      zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) g

theorem zcCompletedGroupAlgebraMap_boundary
    {G : Type v} [Group G] (φ : H →ₜ* K) (ψ : G →* H) (g : G) :
    zcCompletedGroupAlgebraMap C hC φ (zcCompletedGroupAlgebraBoundary C ψ g) =
      zcCompletedGroupAlgebraBoundary C (φ.toMonoidHom.comp ψ) g

theorem zcCompletedGroupAlgebraMapStage_augmentation
    (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
    (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus K C i.2).comp
        (zcCompletedGroupAlgebraMapStage C hC φ i) =
      modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C
        (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)

theorem zcCompletedGroupAlgebraAugmentation_map
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (φ : H →ₜ* K) (x : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraAugmentation C K (zcCompletedGroupAlgebraMap C hC φ x) =
      zcCompletedGroupAlgebraAugmentation C H x

theorem zcCompletedGroupAlgebraMap_id :
    zcCompletedGroupAlgebraMap C hC (ContinuousMonoidHom.id H) =
      RingHom.id (ZCCompletedGroupAlgebra C H)

theorem zcCompletedGroupAlgebraMap_comp
    {L : Type u} [Group L] [TopologicalSpace L] [IsTopologicalGroup L]
    (φ : H →ₜ* K) (ψ : K →ₜ* L) :
    zcCompletedGroupAlgebraMap C hC (ψ.comp φ) =
      (zcCompletedGroupAlgebraMap C hC ψ).comp
        (zcCompletedGroupAlgebraMap C hC φ)

def zcUniversalDifferentialTargetCrossedHom
    (ψ : G →* H) (φ : H →ₜ* K) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) := by
  letI : Module (ZCCompletedGroupAlgebra C H)
      (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
    Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
  exact
    { toFun := fun g => zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g
      map_mul' := by
        intro g h
        change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) (g * h) =
          zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
            zcCompletedGroupAlgebraScalar C ψ g •
              zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
        rw [ScalarCrossedHom.map_mul
          (zcUniversalDifferential C (φ.toMonoidHom.comp ψ)) g h]
        change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
            zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) g •
              zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h =
          zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
            zcCompletedGroupAlgebraMap C hC φ
                (zcCompletedGroupAlgebraScalar C ψ g) •
              zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
        rw [zcCompletedGroupAlgebraMap_scalar] }

def zcCompletedDifferentialModuleTargetMap
    (ψ : G →* H) (φ : H →ₜ* K) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
    ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ) := by
  letI : Module (ZCCompletedGroupAlgebra C H)
      (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
    Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
  exact
    crossedHomModuleLift
      (A := ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ))
      (zcCompletedGroupAlgebraScalar C ψ)
      (zcUniversalDifferentialTargetCrossedHom C hC ψ φ)

theorem zcCompletedDifferentialModuleTargetMap_universal
    (ψ : G →* H) (φ : H →ₜ* K) (g : G) :
    letI : Module (ZCCompletedGroupAlgebra C H)
        (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
      Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
    zcCompletedDifferentialModuleTargetMap C hC ψ φ
        (zcUniversalDifferential C ψ g) =
      zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g := by
  let : Module (ZCCompletedGroupAlgebra C H)
      (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
    Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
  exact
    crossedHomModuleLift_universal
      (A := ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ))
      (zcCompletedGroupAlgebraScalar C ψ)
      (zcUniversalDifferentialTargetCrossedHom C hC ψ φ) g

theorem zcUniversalDifferential_eq_zero_of_target
    (ψ : G →* H) (φ : H →ₜ* K) {g : G}
    (hg : zcUniversalDifferential C ψ g = 0) :
    zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g = 0

theorem zcUniversalDifferential_eq_zero_of_source_target
    (ψ : G →* H) (ψ' : G' →* K) (f : G →* G') (φ : H →ₜ* K)
    (hcomm : ψ'.comp f = φ.toMonoidHom.comp ψ) {g : G}
    (hg : zcUniversalDifferential C ψ g = 0) :
    zcUniversalDifferential C ψ' (f g) = 0

def zcFreeFoxCoordinatesMap (φ : H →ₜ* K) :
    ZCFreeFoxCoordinates C (X := X) (H := H) →
      ZCFreeFoxCoordinates C (X := X) (H := K)

theorem zcFreeFoxCoordinatesMap_apply
    (φ : H →ₜ* K) (a : ZCFreeFoxCoordinates C (X := X) (H := H)) (x : X) :
    zcFreeFoxCoordinatesMap (X := X) C hC φ a x =
      zcCompletedGroupAlgebraMap C hC φ (a x)

theorem zcFreeFoxCoordinatesMap_id
    (a : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcFreeFoxCoordinatesMap (X := X) C hC (ContinuousMonoidHom.id H) a = a

theorem zcFreeFoxCoordinatesMap_comp
    {L : Type v} [Group L] [TopologicalSpace L] [IsTopologicalGroup L]
    (φ : H →ₜ* K) (ψ : K →ₜ* L)
    (a : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcFreeFoxCoordinatesMap (X := X) C hC (ψ.comp φ) a =
      zcFreeFoxCoordinatesMap (X := X) C hC ψ
        (zcFreeFoxCoordinatesMap (X := X) C hC φ a)

theorem zcFreeGroupFoxDerivativeVector_mapTarget
    (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
    zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) w =
      zcFreeFoxCoordinatesMap (X := X) C hC φ (zcFreeGroupFoxDerivativeVector C ψ w)

theorem zcFreeGroupFoxDerivative_mapTarget
    (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) (x : X) :
    zcFreeGroupFoxDerivative C (φ.toMonoidHom.comp ψ) x w =
      zcCompletedGroupAlgebraMap C hC φ (zcFreeGroupFoxDerivative C ψ x w)

theorem zcFreeGroupFoxBoundary_mapTarget
    (ψ : FreeGroup X →* H) (φ : H →ₜ* K)
    (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
    zcCompletedGroupAlgebraMap C hC φ (zcFreeGroupFoxBoundary C ψ v) =
      zcFreeGroupFoxBoundary C (φ.toMonoidHom.comp ψ)
        (zcFreeFoxCoordinatesMap (X := X) C hC φ v)

theorem zcFreeGroupFoxBoundary_derivativeVector_mapTarget
    (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
    zcCompletedGroupAlgebraMap C hC φ
        (zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w)) =
      zcFreeGroupFoxBoundary C (φ.toMonoidHom.comp ψ)
        (zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) w)

theorem zcFreeGroupFoxDerivative_euler_formula_mapTarget
    (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
    zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H (ψ w) - 1) =
      ∑ i : X,
        zcFreeGroupFoxDerivative C (φ.toMonoidHom.comp ψ) i w *
          (zcGroupLike C K ((φ.toMonoidHom.comp ψ) (FreeGroup.of i)) - 1)