NaturalTopology.lean

def zcCompletedDifferentialModuleStageProjectionAdd
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ZCCompletedDifferentialModule C ψ →+
      ZCCompletedDifferentialModuleStage C ψ i

theorem zcCompletedDifferentialModuleStageProjectionAdd_apply
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (a : ZCCompletedDifferentialModule C ψ) :
    zcCompletedDifferentialModuleStageProjectionAdd C ψ i a =
      zcCompletedDifferentialModuleStageProjection C ψ i a

theorem zcCompletedDifferentialModuleStageProjectionAdd_universal
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageProjectionAdd C ψ i
        (zcUniversalDifferential C ψ g) =
      zcCompletedDifferentialModuleStageDifferential C ψ i g

def zcCompletedDifferentialModuleStageProjectionProduct :
    ZCCompletedDifferentialModule C ψ →
      ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        ZCCompletedDifferentialModuleStage C ψ i

theorem zcCompletedDifferentialModuleStageProjectionProduct_apply
    (a : ZCCompletedDifferentialModule C ψ)
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcCompletedDifferentialModuleStageProjectionProduct C ψ a i =
      zcCompletedDifferentialModuleStageProjectionAdd C ψ i a

def zcCompletedDifferentialModuleNaturalTopology :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ)

theorem continuous_zcCompletedDifferentialModuleStageProjectionProduct_naturalTopology :
    @Continuous (ZCCompletedDifferentialModule C ψ)
      (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        ZCCompletedDifferentialModuleStage C ψ i)
      (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
      (zcCompletedDifferentialModuleStageProjectionProduct C ψ)

theorem continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    @Continuous (ZCCompletedDifferentialModule C ψ)
      (ZCCompletedDifferentialModuleStage C ψ i)
      (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
      (zcCompletedDifferentialModuleStageProjectionAdd C ψ i)

theorem continuous_zcCompletedDifferentialModuleStageProjection_naturalTopology
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    @Continuous (ZCCompletedDifferentialModule C ψ)
      (ZCCompletedDifferentialModuleStage C ψ i)
      (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
      (zcCompletedDifferentialModuleStageProjection C ψ i)

def zcCompletedDifferentialModuleStageProjectionsSeparate : Prop

def zcCompletedDifferentialModulePreStageProjectionsSeparate : Prop

def zcCompletedDifferentialModulePreStageKernel
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    Submodule (ZCCompletedGroupAlgebra C H)
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

theorem mem_zcCompletedDifferentialModulePreStageKernel_iff
    {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}
    {i : ZCCompletedDifferentialModuleIndex C ψ}
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G} :
    x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i ↔
      crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H)
        (zcCompletedDifferentialModuleStageDifferential C ψ i) x = 0

theorem mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule
    {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}
    {i : ZCCompletedDifferentialModuleIndex C ψ}
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G} :
    x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i ↔
      zcCompletedDifferentialModulePreStageMap C ψ i x ∈
        crossedDifferentialRelationSubmodule
          (zcCompletedDifferentialModuleStageScalar C ψ i)

theorem crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) ≤
      zcCompletedDifferentialModulePreStageKernel C ψ i

theorem zcCompletedDifferentialModulePreStageMap_mem_relationSubmodule_of_mem
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}
    (hx : x ∈ crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)) :
    zcCompletedDifferentialModulePreStageMap C ψ i x ∈
      crossedDifferentialRelationSubmodule
        (zcCompletedDifferentialModuleStageScalar C ψ i)

def zcCompletedDifferentialModulePreStageKernelIntersection :
    Submodule (ZCCompletedGroupAlgebra C H)
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

theorem mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff
    {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G} :
    x ∈ zcCompletedDifferentialModulePreStageKernelIntersection C ψ ↔
      ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        zcCompletedDifferentialModulePreStageMap C ψ i x ∈
          crossedDifferentialRelationSubmodule
            (zcCompletedDifferentialModuleStageScalar C ψ i)

abbrev zcCompletedDifferentialRelationFiniteClosedSubmodule :
    Submodule (ZCCompletedGroupAlgebra C H)
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

abbrev ZCSeparatedCompletedDifferentialModule : Type u

abbrev ZCApsi : Type u

theorem crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule :
    crossedDifferentialRelationSubmodule
      (zcCompletedGroupAlgebraScalar C ψ) ≤
    zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ

def zcSeparatedUniversalDifferential :
    ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
      (ZCSeparatedCompletedDifferentialModule C ψ) where
  toFun g :=
    (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
      (Finsupp.single g 1)
  map_mul' := by
    intro g h
    let δ : G → ZCSeparatedCompletedDifferentialModule C ψ := fun x =>
      (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
        (Finsupp.single x 1)
    change δ (g * h) = δ g + zcCompletedGroupAlgebraScalar C ψ g • δ h
    have hzero :
        (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
            (crossedDifferentialRelationElement
              (zcCompletedGroupAlgebraScalar C ψ) g h) = 0 := by
      exact
        (Submodule.Quotient.mk_eq_zero
          (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
          (x := crossedDifferentialRelationElement
            (zcCompletedGroupAlgebraScalar C ψ) g h)).2
          (crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule C ψ
            (crossedDifferentialRelationElement_mem
              (zcCompletedGroupAlgebraScalar C ψ) g h))
    have hzero' :
        δ (g * h) -
            (δ g +
              (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
                (zcCompletedGroupAlgebraScalar C ψ g • Finsupp.single h 1)) = 0 := by
      simpa [δ, crossedDifferentialRelationElement] using hzero
    have hsmul :
        (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
            (zcCompletedGroupAlgebraScalar C ψ g • Finsupp.single h 1) =
          zcCompletedGroupAlgebraScalar C ψ g • δ h := by
      simpa [δ, Submodule.mkQ_apply] using
        (Submodule.Quotient.mk_smul
          (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
          (r := zcCompletedGroupAlgebraScalar C ψ g)
          (x := Finsupp.single h 1))
    rw [hsmul] at hzero'
    exact sub_eq_zero.mp hzero'

theorem zcSeparatedUniversalDifferential_commutator_right_kernel
    (g h : G) (hh : ψ h = 1) :
    zcSeparatedUniversalDifferential C ψ ⁅g, h⁆ =
      (zcGroupLike C H (ψ g) - 1) •
        zcSeparatedUniversalDifferential C ψ h

theorem zcSeparatedCompletedDifferentialModule_mk_eq_zero_iff
    {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G} :
    (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x =
        (0 : ZCSeparatedCompletedDifferentialModule C ψ) ↔
      ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        zcCompletedDifferentialModulePreStageMap C ψ i x ∈
          crossedDifferentialRelationSubmodule
            (zcCompletedDifferentialModuleStageScalar C ψ i)

def zcSeparatedCompletedDifferentialModuleStageProjectionAdd
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedDifferentialModuleStage C ψ i

theorem zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
    zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i
        ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x) =
      crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H)
        (zcCompletedDifferentialModuleStageDifferential C ψ i) x

theorem zcSeparatedCompletedDifferentialModuleStageProjectionAdd_universal
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i
        (zcSeparatedUniversalDifferential C ψ g) =
      zcCompletedDifferentialModuleStageDifferential C ψ i g

def zcSeparatedCompletedDifferentialModuleStageProjectionProduct :
    ZCSeparatedCompletedDifferentialModule C ψ →
      ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        ZCCompletedDifferentialModuleStage C ψ i

theorem zcSeparatedCompletedDifferentialModuleStageProjectionProduct_apply
    (a : ZCSeparatedCompletedDifferentialModule C ψ)
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ a i =
      zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a

theorem zcSeparatedCompletedDifferentialModuleStageProjectionsSeparate :
    ∀ x : ZCSeparatedCompletedDifferentialModule C ψ,
      (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x = 0) →
      x = 0

theorem zcSeparatedCompletedDifferentialModuleStageProjectionProduct_injective :
    Function.Injective
      (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ)

theorem zcSeparatedCompletedDifferentialModuleStageProjection_ext
    {a b : ZCSeparatedCompletedDifferentialModule C ψ}
    (h : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
      zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a =
        zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i b) :
    a = b

def zcCompletedDifferentialModuleToSeparated :
    ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
      ZCSeparatedCompletedDifferentialModule C ψ

theorem zcCompletedDifferentialModuleToSeparated_universal (g : G) :
    zcCompletedDifferentialModuleToSeparated C ψ
      (zcUniversalDifferential C ψ g) =
    zcSeparatedUniversalDifferential C ψ g

theorem crossedDifferentialBoundaryLiftLinear_kills_finiteClosedSubmodule
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψc : ContinuousMonoidHom G H)
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}
    (hx : x ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψc.toMonoidHom) :
    crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H)
        (zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x = 0

def zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψc : ContinuousMonoidHom G H) :
    ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
      ZCCompletedGroupAlgebra C H

theorem zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_universal
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψc : ContinuousMonoidHom G H)
    (g : G) :
    zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC ψc
        (zcSeparatedUniversalDifferential C ψc.toMonoidHom g) =
      zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom g

theorem zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_comp_toSeparated
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψc : ContinuousMonoidHom G H) :
    (zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC ψc).comp
      (zcCompletedDifferentialModuleToSeparated C ψc.toMonoidHom) =
    zcToCompletedGroupAlgebra C ψc.toMonoidHom

def zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations : Prop

def zcCompletedDifferentialPreModuleNaturalTopology :
    TopologicalSpace (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)

theorem continuous_zcCompletedDifferentialModulePreStageMap_naturalTopology
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ i)
        (zcCompletedDifferentialModuleStageSource C ψ i))
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      (⊥ : TopologicalSpace
        (CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψ i)
          (zcCompletedDifferentialModuleStageSource C ψ i)))
      (zcCompletedDifferentialModulePreStageMap C ψ i)

def zcSeparatedCompletedDifferentialModuleNaturalTopology :
    TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ)

theorem continuous_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology :
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (ZCSeparatedCompletedDifferentialModule C ψ)
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
      (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

theorem isQuotientMap_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology :
    letI : TopologicalSpace
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
      zcCompletedDifferentialPreModuleNaturalTopology C ψ
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
    Topology.IsQuotientMap (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ := by
  let : TopologicalSpace
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
    zcCompletedDifferentialPreModuleNaturalTopology C ψ
  let : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
    zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
  rw [Topology.isQuotientMap_iff]
  constructor
  · exact ⟨rfl⟩
  · exact
      Submodule.Quotient.mk_surjective
        (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)

theorem continuous_zcSeparatedCompletedDifferentialModule_iff_comp_mkQ
    {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}
    {A : Type u} [TopologicalSpace A]
    {f : ZCSeparatedCompletedDifferentialModule C ψ → A} :
    @Continuous
        (ZCSeparatedCompletedDifferentialModule C ψ) A
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ) inferInstance f ↔
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) A
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance
        (fun x => f ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x)) := by
  let : TopologicalSpace
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
    zcCompletedDifferentialPreModuleNaturalTopology C ψ
  let : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
    zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
  simpa [Function.comp_def] using
    (isQuotientMap_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology
      C ψ).continuous_iff (g := f)

theorem continuous_zcSepDiffModuleStageProjAdd_naturalTopology
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    @Continuous
      (ZCSeparatedCompletedDifferentialModule C ψ)
      (ZCCompletedDifferentialModuleStage C ψ i)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
      inferInstance
      (zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i)

theorem continuous_zcSepDiffModuleStageProjProduct_naturalTopology :
    @Continuous
      (ZCSeparatedCompletedDifferentialModule C ψ)
      (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        ZCCompletedDifferentialModuleStage C ψ i)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
      inferInstance
      (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ)

theorem t2Space_zcSeparatedCompletedDifferentialModuleNaturalTopology :
    @T2Space
      (ZCSeparatedCompletedDifferentialModule C ψ)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)

theorem zcSepDiffModuleNaturalTopology_eq_induced_stageProjProduct
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ)) :
    zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ =
      TopologicalSpace.induced
        (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstance

theorem continuous_zcCompletedDifferentialPreModule_single_one_naturalTopology :
    @Continuous G
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      inferInstance
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      (fun g : G => Finsupp.single g (1 : ZCCompletedGroupAlgebra C H)) := by
  rw [continuous_induced_rng]
  let S := zcCompletedDifferentialPreModuleStageSystem C ψ
  let preSingle :
      ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        G →
          CrossedDifferentialPreModule
            (zcCompletedDifferentialModuleStageRing C ψ i)
            (zcCompletedDifferentialModuleStageSource C ψ i) := fun i g =>
        zcCompletedDifferentialModulePreStageMap C ψ i
          (Finsupp.single g (1 : ZCCompletedGroupAlgebra C H))
  have hpreSingle_continuous :
      ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        @Continuous G
          (CrossedDifferentialPreModule
            (zcCompletedDifferentialModuleStageRing C ψ i)
            (zcCompletedDifferentialModuleStageSource C ψ i))
          inferInstance
          ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)
          (preSingle i) := by
    intro i
    have hsource :
        Continuous (zcCompletedDifferentialModuleStageSourceProj C ψ i) := by
      exact QuotientGroup.continuous_mk
    have hsingle :
        @Continuous
          (zcCompletedDifferentialModuleStageSource C ψ i)
          (CrossedDifferentialPreModule
            (zcCompletedDifferentialModuleStageRing C ψ i)
            (zcCompletedDifferentialModuleStageSource C ψ i))
          inferInstance
          ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)
          (fun q => Finsupp.single q
            (1 : zcCompletedDifferentialModuleStageRing C ψ i)) :=
      @continuous_of_discreteTopology
        (zcCompletedDifferentialModuleStageSource C ψ i)
        inferInstance inferInstance
        (CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψ i)
          (zcCompletedDifferentialModuleStageSource C ψ i))
        ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)
        (fun q => Finsupp.single q
          (1 : zcCompletedDifferentialModuleStageRing C ψ i))
    have hcomp :
        @Continuous G
          (CrossedDifferentialPreModule
            (zcCompletedDifferentialModuleStageRing C ψ i)
            (zcCompletedDifferentialModuleStageSource C ψ i))
          inferInstance
          ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)
          ((fun q => Finsupp.single q
              (1 : zcCompletedDifferentialModuleStageRing C ψ i)) ∘
            zcCompletedDifferentialModuleStageSourceProj C ψ i) :=
      @Continuous.comp
        G
        (zcCompletedDifferentialModuleStageSource C ψ i)
        (CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψ i)
          (zcCompletedDifferentialModuleStageSource C ψ i))
        inferInstance inferInstance
        ((zcCompletedDifferentialPreModuleStageSystem C ψ).topologicalSpace i)
        (f := zcCompletedDifferentialModuleStageSourceProj C ψ i)
        (g := fun q => Finsupp.single q
          (1 : zcCompletedDifferentialModuleStageRing C ψ i))
        hsingle hsource
    have hfun :
        ((fun q => Finsupp.single q
            (1 : zcCompletedDifferentialModuleStageRing C ψ i)) ∘
          zcCompletedDifferentialModuleStageSourceProj C ψ i) =
            preSingle i := by
      funext g
      simp only [Function.comp_apply, preSingle,
        zcCompletedDifferentialModulePreStageMap_single,
        zcCompletedGroupAlgebraProjection_one]
    exact hfun ▸ hcomp
  have hpreSingle_compat : S.CompatibleMaps preSingle := by
    intro i j hij
    funext g
    exact
      congrFun
        (zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap C ψ i j hij)
        (Finsupp.single g (1 : ZCCompletedGroupAlgebra C H))
  have hLift : Continuous (S.inverseLimitLift preSingle hpreSingle_compat) :=
    S.continuous_inverseLimitLift preSingle hpreSingle_continuous hpreSingle_compat
  have hEq :
      zcCompletedDifferentialPreModuleStageFamilyMap C ψ ∘
          (fun g : G => Finsupp.single g (1 : ZCCompletedGroupAlgebra C H)) =
        S.inverseLimitLift preSingle hpreSingle_compat := by
    apply S.inverseLimitLift_unique preSingle hpreSingle_compat
    intro i
    funext g
    rfl
  rw [hEq]
  exact hLift

theorem continuous_zcSeparatedUniversalDifferential_naturalTopology :
    @Continuous G
      (ZCSeparatedCompletedDifferentialModule C ψ)
      inferInstance
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
      (zcSeparatedUniversalDifferential C ψ)

theorem continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A]
    (delta : G → A)
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (L :
      CrossedDifferentialPreModule
        (zcCompletedDifferentialModuleStageRing C ψ i)
        (zcCompletedDifferentialModuleStageSource C ψ i) → A)
    (hfactor :
      ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
        crossedDifferentialModuleLiftLinear
            (R := ZCCompletedGroupAlgebra C H) delta x =
          L (zcCompletedDifferentialModulePreStageMap C ψ i x)) :
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      A
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      inferInstance
      (crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H) delta)

theorem continuous_crossedDifferentialModuleLiftLinear_stageDifferential
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (ZCCompletedDifferentialModuleStage C ψ i)
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      inferInstance
      (crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H)
        (zcCompletedDifferentialModuleStageDifferential C ψ i))

def zcCompletedDifferentialModuleRelationSubmoduleClosed : Prop

theorem zcDiffModuleRelSubmoduleClosed_of_inj_continuous_comp_mkQ
    {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
    [TopologicalSpace M] [T1Space M]
    (L :
      ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] M)
    (hLinj : Function.Injective L)
    (hcont :
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        M
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
        inferInstance
        (fun x =>
          L
            ((crossedDifferentialRelationSubmodule
              (zcCompletedGroupAlgebraScalar C ψ)).mkQ x))) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ := by
  let : TopologicalSpace
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
    zcCompletedDifferentialPreModuleNaturalTopology C ψ
  change IsClosed
    ((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :
      Submodule (ZCCompletedGroupAlgebra C H)
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
      Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))
  have hpreimage :
      ((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :
        Submodule (ZCCompletedGroupAlgebra C H)
          (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
        Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =
      (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
        L
          ((crossedDifferentialRelationSubmodule
            (zcCompletedGroupAlgebraScalar C ψ)).mkQ x)) ⁻¹' ({0} : Set M) := by
    ext x
    constructor
    · intro hx
      have hq :
          ((crossedDifferentialRelationSubmodule
            (zcCompletedGroupAlgebraScalar C ψ)).mkQ x :
              ZCCompletedDifferentialModule C ψ) = 0 :=
        (Submodule.Quotient.mk_eq_zero
          (p := crossedDifferentialRelationSubmodule
            (zcCompletedGroupAlgebraScalar C ψ))
          (x := x)).2 hx
      change
        L
          ((crossedDifferentialRelationSubmodule
            (zcCompletedGroupAlgebraScalar C ψ)).mkQ x) = 0
      rw [hq]
      exact map_zero L
    · intro hx
      have hq :
          ((crossedDifferentialRelationSubmodule
            (zcCompletedGroupAlgebraScalar C ψ)).mkQ x :
              ZCCompletedDifferentialModule C ψ) = 0 := by
        apply hLinj
        simpa using hx
      exact
        (Submodule.Quotient.mk_eq_zero
          (p := crossedDifferentialRelationSubmodule
            (zcCompletedGroupAlgebraScalar C ψ))
          (x := x)).1 hq
  rw [hpreimage]
  exact isClosed_singleton.preimage hcont

theorem continuous_zcCompletedDifferentialModule_mkQ_naturalTopology :
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (ZCCompletedDifferentialModule C ψ)
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      (zcCompletedDifferentialModuleNaturalTopology C ψ)
      (crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)).mkQ

theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_of_t1_naturalTopology
    (hT1 :
      @T1Space (ZCCompletedDifferentialModule C ψ)
        (zcCompletedDifferentialModuleNaturalTopology C ψ)) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ

theorem zcDiffModuleRelSubmoduleClosed_of_inj_continuous_naturalTopology
    {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
    [TopologicalSpace M] [T1Space M]
    (L :
      ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] M)
    (hLinj : Function.Injective L)
    (hcont :
      @Continuous
        (ZCCompletedDifferentialModule C ψ) M
        (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
        L) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ

theorem zcDiffModuleFiniteRelationReductions_mem_closure_relSubmodule
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
    (hx : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
      zcCompletedDifferentialModulePreStageMap C ψ i x ∈
        crossedDifferentialRelationSubmodule
          (zcCompletedDifferentialModuleStageScalar C ψ i)) :
    x ∈ @closure
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      ((crossedDifferentialRelationSubmodule
        (zcCompletedGroupAlgebraScalar C ψ) :
          Submodule (ZCCompletedGroupAlgebra C H)
            (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set
              (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))

theorem isClosed_zcCompletedDifferentialModulePreStageKernel_naturalTopology
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    @IsClosed
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      ((zcCompletedDifferentialModulePreStageKernel C ψ i :
        Submodule (ZCCompletedGroupAlgebra C H)
          (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
        Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))

theorem isClosed_zcCompletedDifferentialRelationFiniteClosedSubmodule_naturalTopology :
    @IsClosed
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ :
        Submodule (ZCCompletedGroupAlgebra C H)
          (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
        Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))

theorem isClosed_zero_zcSeparatedCompletedDifferentialModuleNaturalTopology :
    @IsClosed (ZCSeparatedCompletedDifferentialModule C ψ)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
      ({0} : Set (ZCSeparatedCompletedDifferentialModule C ψ))

theorem closure_crossedDifferentialRelationSubmodule_eq_finiteClosedSubmodule
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ)) :
    @closure
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      ((crossedDifferentialRelationSubmodule
        (zcCompletedGroupAlgebraScalar C ψ) :
          Submodule (ZCCompletedGroupAlgebra C H)
            (CrossedDifferentialPreModule
              (ZCCompletedGroupAlgebra C H) G)) :
        Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =
    (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ :
      Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))

theorem crossedDifferentialModuleLiftLinear_kills_finiteClosedSubmodule_of_continuous
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont :
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        A
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H) delta))
    {x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G}
    (hx : x ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ) :
    crossedDifferentialModuleLiftLinear
      (R := ZCCompletedGroupAlgebra C H) delta x = 0

def zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont :
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        A
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H) delta)) :
    ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A

theorem zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_universal
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont :
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        A
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H) delta))
    (g : G) :
    zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
        C ψ hdir delta hcont
        (zcSeparatedUniversalDifferential C ψ g) =
      delta g

theorem zcSeparatedCompletedDifferentialModuleHom_ext
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    {f h : ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A}
    (hfh : ∀ g, f (zcSeparatedUniversalDifferential C ψ g) =
      h (zcSeparatedUniversalDifferential C ψ g)) :
    f = h

theorem zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_unique
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont :
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        A
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H) delta))
    (f : ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A)
    (hf : ∀ g, f (zcSeparatedUniversalDifferential C ψ g) = delta g) :
    f =
      zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
        C ψ hdir delta hcont

def zcSeparatedCompletedDifferentialModuleLiftContinuousLinearMapOfContinuousPrelift
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont :
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        A
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H) delta)) :
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
    ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A := by
  letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
    zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
  refine
    { toLinearMap :=
        zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
          C ψ hdir delta hcont
      cont := ?_ }
  rw [continuous_coinduced_dom]
  change
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      A
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      inferInstance
      (fun x =>
        zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
          C ψ hdir delta hcont
          ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x))
  have hcomp :
      (fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
        zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
          C ψ hdir delta hcont
          ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x)) =
      crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H) delta := by
    funext x
    rw [zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift,
      Submodule.mkQ_apply, Submodule.liftQ_apply]
  rw [hcomp]
  exact hcont

theorem zcSepDiffModuleLiftContinuousLinearMapOfContinuousPrelift_apply
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
    (hcont :
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        A
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
        inferInstance
        (crossedDifferentialModuleLiftLinear
          (R := ZCCompletedGroupAlgebra C H) delta))
    (m : ZCSeparatedCompletedDifferentialModule C ψ) :
    zcSeparatedCompletedDifferentialModuleLiftContinuousLinearMapOfContinuousPrelift
        C ψ hdir delta hcont m =
      zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
        C ψ hdir delta hcont m

def zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (hprelift :
      ∀ (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A),
        Continuous delta →
          @Continuous
            (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
            A
            (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
            inferInstance
            (crossedDifferentialModuleLiftLinear
              (R := ZCCompletedGroupAlgebra C H) delta)) :
    {delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A //
        Continuous delta} ≃
      (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
      ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) where
  toFun delta :=
    zcSeparatedCompletedDifferentialModuleLiftContinuousLinearMapOfContinuousPrelift
      C ψ hdir delta.1 (hprelift delta.1 delta.2)
  invFun f := by
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
    exact
      ⟨(zcSeparatedUniversalDifferential C ψ).mapLinear f.toLinearMap,
        f.cont.comp (continuous_zcSeparatedUniversalDifferential_naturalTopology C ψ)⟩
  left_inv delta := by
    apply Subtype.ext
    apply CrossedHom.ext
    intro g
    exact
      zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_universal
        C ψ hdir delta.1 (hprelift delta.1 delta.2) g
  right_inv f := by
    let : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
    let delta :=
      (zcSeparatedUniversalDifferential C ψ).mapLinear f.toLinearMap
    have hcontinuous_delta : Continuous delta :=
      f.cont.comp (continuous_zcSeparatedUniversalDifferential_naturalTopology C ψ)
    have hlin :
        f.toLinearMap =
          zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
            C ψ hdir delta (hprelift delta hcontinuous_delta) := by
      apply zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_unique
        C ψ hdir
      intro g
      rfl
    apply ContinuousLinearMap.ext
    intro m
    exact congrFun (congrArg DFunLike.coe hlin.symm) m

def zcSepContCrossedDiffEquivCLM
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (ψc : ContinuousMonoidHom G H)
    (hprelift :
      ∀ (delta : ScalarCrossedHom
          (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A),
        Continuous delta →
          @Continuous
            (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
            A
            (zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom)
            inferInstance
            (crossedDifferentialModuleLiftLinear
              (R := ZCCompletedGroupAlgebra C H) delta)) :
    {delta : ScalarCrossedHom
        (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A //
        Continuous delta} ≃
      (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom
      ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →L[ZCCompletedGroupAlgebra C H] A)
          := by
  letI : Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom) :=
    nonempty_zcCompletedDifferentialModuleIndex C hC ψc
  exact
    zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap
      C ψc.toMonoidHom
      (directed_zcCompletedDifferentialModuleIndex C hForm hC ψc)
      hprelift

def zcSepCompletedContCrossedDiffEquivContinuousLinearMapOfFiniteStageFactorization
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (hfactor :
      ∀ (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A),
        Continuous delta →
          ∃ i : ZCCompletedDifferentialModuleIndex C ψ,
            ∃ L :
              CrossedDifferentialPreModule
                (zcCompletedDifferentialModuleStageRing C ψ i)
                (zcCompletedDifferentialModuleStageSource C ψ i) → A,
              ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
                crossedDifferentialModuleLiftLinear
                    (R := ZCCompletedGroupAlgebra C H) delta x =
                  L (zcCompletedDifferentialModulePreStageMap C ψ i x)) :
    {delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A //
        Continuous delta} ≃
      (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
      ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) := by
  refine
    zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap
      C ψ hdir ?_
  intro delta hcont
  rcases hfactor delta hcont with ⟨i, L, hL⟩
  exact
    continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor
      C ψ delta i L hL

def zcSepContCrossedDiffEquivCLMOfFiniteStage
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [T1Space A]
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (ψc : ContinuousMonoidHom G H)
    (hfactor :
      ∀ (delta : ScalarCrossedHom
          (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A),
        Continuous delta →
          ∃ i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom,
            ∃ L :
              CrossedDifferentialPreModule
                (zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i)
                (zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i) → A,
              ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
                crossedDifferentialModuleLiftLinear
                    (R := ZCCompletedGroupAlgebra C H) delta x =
                  L (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) :
    {delta : ScalarCrossedHom
        (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A //
        Continuous delta} ≃
      (letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom
      ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →L[ZCCompletedGroupAlgebra C H] A)
          := by
  letI : Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom) :=
    nonempty_zcCompletedDifferentialModuleIndex C hC ψc
  exact
    zcSepCompletedContCrossedDiffEquivContinuousLinearMapOfFiniteStageFactorization
      C ψc.toMonoidHom
      (directed_zcCompletedDifferentialModuleIndex C hForm hC ψc)
      hfactor

theorem zcCompletedGroupAlgebra_smul_factor_through_finite_stage
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [Finite A] [DiscreteTopology A]
    [ContinuousSMul (ZCCompletedGroupAlgebra C H) A]
    (hForm : ProCGroups.FiniteGroupClass.Formation C) :
    ∃ j : ZCCompletedGroupAlgebraIndex C H,
      ∃ act : ZCCompletedGroupAlgebraStage C H j → A → A,
        ∀ (r : ZCCompletedGroupAlgebra C H) (a : A),
          act (zcCompletedGroupAlgebraProjection C H j r) a = r • a

theorem crossedDifferentialModuleLiftLinear_factors_finite_discrete
    {A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
    [TopologicalSpace A] [Finite A] [DiscreteTopology A]
    [ContinuousSMul (ZCCompletedGroupAlgebra C H) A]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (ψc : ContinuousMonoidHom G H)
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G)
    (delta : ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) A)
    (hcont : Continuous delta) :
    ∃ i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom,
      ∃ L :
        CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i)
          (zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i) → A,
        ∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
          crossedDifferentialModuleLiftLinear
              (R := ZCCompletedGroupAlgebra C H) delta x =
            L (zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)

theorem continuous_crossedDifferentialModuleLiftLinear_of_profiniteTarget
    {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
    [TopologicalSpace M]
    [IsTopologicalRing (ZCCompletedGroupAlgebra C H)]
    [CompactSpace (ZCCompletedGroupAlgebra C H)]
    [IsTopologicalAddGroup M] [ContinuousSMul (ZCCompletedGroupAlgebra C H) M]
    [CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (ψc : ContinuousMonoidHom G H)
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G)
    (delta : ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) M)
    (hcont : Continuous delta) :
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      M
      (zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom)
      inferInstance
      (crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H) delta)

def zcApsiContinuousCrossedDifferentialEquivContinuousLinearMapOfProfiniteTarget
    {M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
    [TopologicalSpace M]
    [IsTopologicalRing (ZCCompletedGroupAlgebra C H)]
    [CompactSpace (ZCCompletedGroupAlgebra C H)]
    [IsTopologicalAddGroup M] [ContinuousSMul (ZCCompletedGroupAlgebra C H) M]
    [CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M]
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (ψc : ContinuousMonoidHom G H)
    (hG : ProCGroups.ProC.HasOpenNormalBasisInClass C G) :
    {delta : ScalarCrossedHom
        (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) M //
        Continuous delta} ≃
      (letI : TopologicalSpace (ZCApsi C ψc.toMonoidHom) :=
        zcSeparatedCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom
      ZCApsi C ψc.toMonoidHom →L[ZCCompletedGroupAlgebra C H] M) := by
  letI : T1Space M := inferInstance
  letI : ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C :=
    hForm.containsTrivialQuotients
  letI : Nonempty (ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom) :=
    nonempty_zcCompletedDifferentialModuleIndex C hC ψc
  exact
    zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap
      C ψc.toMonoidHom
      (directed_zcCompletedDifferentialModuleIndex C hForm hC ψc)
      (fun delta hcont =>
        continuous_crossedDifferentialModuleLiftLinear_of_profiniteTarget
          C hC hForm ψc hG delta hcont)

theorem zcDiffModuleFiniteRelationReductionsReflectRelations_of_isClosed_relSubmodule
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (hclosed :
      @IsClosed
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
        ((crossedDifferentialRelationSubmodule
          (zcCompletedGroupAlgebraScalar C ψ) :
            Submodule (ZCCompletedGroupAlgebra C H)
              (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set
                (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))) :
    zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ

theorem zcDiffModuleFiniteRelationReductionsReflectRelations_of_relSubmoduleClosed
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ))
    (hclosed : zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ) :
    zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ

theorem zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations
    (C : ProCGroups.FiniteGroupClass.{u}) (ψ : G →* H) :
    zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ ↔
      zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ

theorem zcDiffModulePreStageProjsSeparate_iff_relSubmodule_eq_iInf_kernel
    (C : ProCGroups.FiniteGroupClass.{u}) (ψ : G →* H) :
    zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ ↔
      crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =
        zcCompletedDifferentialModulePreStageKernelIntersection C ψ

theorem zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate
    (hpre : zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ) :
    zcCompletedDifferentialModuleStageProjectionsSeparate C ψ

theorem zcDiffModuleStageProjsSeparate_of_relSubmodule_eq_iInf_kernel
    (hker :
      crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =
        zcCompletedDifferentialModulePreStageKernelIntersection C ψ) :
    zcCompletedDifferentialModuleStageProjectionsSeparate C ψ

theorem zcCompletedDifferentialModuleStageProjection_ext_of_separating
    (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ)
    {a b : ZCCompletedDifferentialModule C ψ}
    (h : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
      zcCompletedDifferentialModuleStageProjectionAdd C ψ i a =
        zcCompletedDifferentialModuleStageProjectionAdd C ψ i b) :
    a = b

theorem t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating
    (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :
    @T2Space (ZCCompletedDifferentialModule C ψ)
      (zcCompletedDifferentialModuleNaturalTopology C ψ)

theorem t2Space_zcDiffModuleNaturalTopology_of_relSubmodule_eq_iInf_kernel
    (hker :
      crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =
        zcCompletedDifferentialModulePreStageKernelIntersection C ψ) :
    @T2Space (ZCCompletedDifferentialModule C ψ)
      (zcCompletedDifferentialModuleNaturalTopology C ψ)

theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_of_stageProjsSeparate
    (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ

theorem zcDiffModuleRelSubmoduleClosed_of_finiteRelationReductionsReflectRelations
    (hreflect :
      zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ

theorem zcDiffModuleFiniteRelationReductionsReflectRelations_iff_relSubmodule_eq_iInf_kernel
    (C : ProCGroups.FiniteGroupClass.{u}) (ψ : G →* H) :
    zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ ↔
      crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =
        zcCompletedDifferentialModulePreStageKernelIntersection C ψ

theorem zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
    {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ)) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ ↔
      zcCompletedDifferentialModuleStageProjectionsSeparate C ψ

theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_iff_t2_naturalTopology
    {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}
    [Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
    (hdir : Directed (· ≤ ·)
      (id : ZCCompletedDifferentialModuleIndex C ψ →
        ZCCompletedDifferentialModuleIndex C ψ)) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ ↔
      @T2Space (ZCCompletedDifferentialModule C ψ)
        (zcCompletedDifferentialModuleNaturalTopology C ψ)

theorem continuous_add_zcCompletedDifferentialModuleNaturalTopology :
    letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
      zcCompletedDifferentialModuleNaturalTopology C ψ
    Continuous (fun p : ZCCompletedDifferentialModule C ψ ×
        ZCCompletedDifferentialModule C ψ => p.1 + p.2) := by
  let : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
    zcCompletedDifferentialModuleNaturalTopology C ψ
  rw [continuous_induced_rng]
  change Continuous
    (fun p : ZCCompletedDifferentialModule C ψ ×
        ZCCompletedDifferentialModule C ψ =>
      fun i : ZCCompletedDifferentialModuleIndex C ψ =>
        zcCompletedDifferentialModuleStageProjectionAdd C ψ i (p.1 + p.2))
  simpa [map_add] using
    (continuous_pi fun i =>
      ((continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ i).comp
          continuous_fst).add
        ((continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ i).comp
          continuous_snd))

theorem continuous_neg_zcCompletedDifferentialModuleNaturalTopology :
    letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
      zcCompletedDifferentialModuleNaturalTopology C ψ
    Continuous (fun a : ZCCompletedDifferentialModule C ψ => -a) := by
  let : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
    zcCompletedDifferentialModuleNaturalTopology C ψ
  rw [continuous_induced_rng]
  change Continuous
    (fun a : ZCCompletedDifferentialModule C ψ =>
      fun i : ZCCompletedDifferentialModuleIndex C ψ =>
        zcCompletedDifferentialModuleStageProjectionAdd C ψ i (-a))
  simpa [map_neg] using
    (continuous_pi fun i =>
      (continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ i).neg)

theorem isTopologicalAddGroup_zcCompletedDifferentialModuleNaturalTopology :
    @IsTopologicalAddGroup (ZCCompletedDifferentialModule C ψ)
      (zcCompletedDifferentialModuleNaturalTopology C ψ) _

theorem continuous_zcCompletedDifferentialModuleStageDifferential
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    Continuous (zcCompletedDifferentialModuleStageDifferential C ψ i)

theorem continuous_zcUniversalDifferential_naturalTopology :
    @Continuous G (ZCCompletedDifferentialModule C ψ) inferInstance
      (zcCompletedDifferentialModuleNaturalTopology C ψ)
      (zcUniversalDifferential C ψ)

theorem zcUniversalDifferentialFinalTopology_le_naturalTopology :
    zcUniversalDifferentialFinalTopology C ψ ≤
      zcCompletedDifferentialModuleNaturalTopology C ψ

theorem continuous_zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    Continuous (zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψ i)

theorem continuous_zcToCompletedGroupAlgebra_naturalTopology
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψc : ContinuousMonoidHom G H) :
    @Continuous (ZCCompletedDifferentialModule C ψc.toMonoidHom)
      (ZCCompletedGroupAlgebra C H)
      (zcCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom) inferInstance
      (zcToCompletedGroupAlgebra C ψc.toMonoidHom)

theorem continuousSMul_zcCompletedDifferentialModuleNaturalTopology :
    @ContinuousSMul (ZCCompletedGroupAlgebra C H)
      (ZCCompletedDifferentialModule C ψ)
      inferInstance inferInstance (zcCompletedDifferentialModuleNaturalTopology C ψ)