def zcCompletedDifferentialModuleStageProjectionAdd
(i : ZCCompletedDifferentialModuleIndex C ψ) :
ZCCompletedDifferentialModule C ψ →+
ZCCompletedDifferentialModuleStage C ψ i :=
(zcCompletedDifferentialModuleStageProjection C ψ i).toAddMonoidHomThe additive finite-stage projection from the algebraic completed differential module.
theorem zcCompletedDifferentialModuleStageProjectionAdd_apply
(i : ZCCompletedDifferentialModuleIndex C ψ)
(a : ZCCompletedDifferentialModule C ψ) :
zcCompletedDifferentialModuleStageProjectionAdd C ψ i a =
zcCompletedDifferentialModuleStageProjection C ψ i aApplying the projection map to a completed element returns its corresponding finite-stage coordinate.
Show proof
rflProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcCompletedDifferentialModuleStageProjectionAdd_universal
(i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
zcCompletedDifferentialModuleStageProjectionAdd C ψ i
(zcUniversalDifferential C ψ g) =
zcCompletedDifferentialModuleStageDifferential C ψ i gShow proof
zcCompletedDifferentialModuleStageProjection_universal C ψ i gProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcCompletedDifferentialModuleStageProjectionProduct :
ZCCompletedDifferentialModule C ψ →
∀ i : ZCCompletedDifferentialModuleIndex C ψ,
ZCCompletedDifferentialModuleStage C ψ i :=
fun a i => zcCompletedDifferentialModuleStageProjectionAdd C ψ i aThe product of all finite source/target/coefficient projections of the algebraic quotient.
theorem zcCompletedDifferentialModuleStageProjectionProduct_apply
(a : ZCCompletedDifferentialModule C ψ)
(i : ZCCompletedDifferentialModuleIndex C ψ) :
zcCompletedDifferentialModuleStageProjectionProduct C ψ a i =
zcCompletedDifferentialModuleStageProjectionAdd C ψ i aApplying the projection map to a completed element returns its corresponding finite-stage coordinate.
Show proof
rflProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcCompletedDifferentialModuleNaturalTopology :
TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
TopologicalSpace.induced
(zcCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstanceThe finite-stage completed topology on the algebraic completed differential module. This topology is named deliberately: it is not installed as a global instance.
theorem continuous_zcCompletedDifferentialModuleStageProjectionProduct_naturalTopology :
@Continuous (ZCCompletedDifferentialModule C ψ)
(∀ i : ZCCompletedDifferentialModuleIndex C ψ,
ZCCompletedDifferentialModuleStage C ψ i)
(zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
(zcCompletedDifferentialModuleStageProjectionProduct C ψ)The product map defining the finite-stage completed topology is continuous.
Show proof
continuous_induced_domProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology
(i : ZCCompletedDifferentialModuleIndex C ψ) :
@Continuous (ZCCompletedDifferentialModule C ψ)
(ZCCompletedDifferentialModuleStage C ψ i)
(zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
(zcCompletedDifferentialModuleStageProjectionAdd C ψ i)Show proof
by
have hprod :=
continuous_zcCompletedDifferentialModuleStageProjectionProduct_naturalTopology C ψ
simpa [zcCompletedDifferentialModuleStageProjectionProduct, Function.comp_def] using
(@Continuous.comp
(ZCCompletedDifferentialModule C ψ)
(∀ i : ZCCompletedDifferentialModuleIndex C ψ,
ZCCompletedDifferentialModuleStage C ψ i)
(ZCCompletedDifferentialModuleStage C ψ i)
(zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance inferInstance
(f := zcCompletedDifferentialModuleStageProjectionProduct C ψ)
(g := fun x => x i)
(continuous_apply i) hprod)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcCompletedDifferentialModuleStageProjection_naturalTopology
(i : ZCCompletedDifferentialModuleIndex C ψ) :
@Continuous (ZCCompletedDifferentialModule C ψ)
(ZCCompletedDifferentialModuleStage C ψ i)
(zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
(zcCompletedDifferentialModuleStageProjection C ψ i)Continuity of the completed differential-module stage projection is characterized by the natural topology.
Show proof
by
simpa using
continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ iProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcCompletedDifferentialModuleStageProjectionsSeparate : Prop :=
Function.Injective (zcCompletedDifferentialModuleStageProjectionProduct C ψ)A named predicate for the algebraic separation still needed to make the natural topology Hausdorff. It is false for arbitrary sources without a residual finite-stage hypothesis.
def zcCompletedDifferentialModulePreStageProjectionsSeparate : Prop :=
∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
(∀ i : ZCCompletedDifferentialModuleIndex C ψ,
crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H)
(zcCompletedDifferentialModuleStageDifferential C ψ i) x = 0) →
x ∈ crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)def zcCompletedDifferentialModulePreStageKernel
(i : ZCCompletedDifferentialModuleIndex C ψ) :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
LinearMap.ker
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H)
(zcCompletedDifferentialModuleStageDifferential C ψ i))theorem mem_zcCompletedDifferentialModulePreStageKernel_iff
(i : ZCCompletedDifferentialModuleIndex C ψ)
(x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i ↔
crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H)
(zcCompletedDifferentialModuleStageDifferential C ψ i) x = 0Membership in a completed differential-module pre-stage kernel is equivalent to vanishing of the corresponding finite-stage coordinate.
Show proof
Iff.rflProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule
(i : ZCCompletedDifferentialModuleIndex C ψ)
(x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i ↔
zcCompletedDifferentialModulePreStageMap C ψ i x ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)Show proof
by
constructor
· intro hx
have hq :
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i x) = 0 := by
rw [zcCompletedDifferentialModulePreStageMap_mkQ]
exact hx
exact
(Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i))
(x := zcCompletedDifferentialModulePreStageMap C ψ i x)).1 hq
· intro hx
have hq :
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i x) = 0 :=
(Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i))
(x := zcCompletedDifferentialModulePreStageMap C ψ i x)).2 hx
rw [mem_zcCompletedDifferentialModulePreStageKernel_iff]
rw [← zcCompletedDifferentialModulePreStageMap_mkQ]
exact hqProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel
(i : ZCCompletedDifferentialModuleIndex C ψ) :
crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) ≤
zcCompletedDifferentialModulePreStageKernel C ψ iEvery defining crossed-differential relation is killed by every finite stage.
Show proof
by
simpa [zcCompletedDifferentialModulePreStageKernel] using
crossedDifferentialRelationSubmodule_le_ker
(A := ZCCompletedDifferentialModuleStage C ψ i)
(zcCompletedGroupAlgebraScalar C ψ)
(zcCompletedDifferentialModuleStageDifferential C ψ i)
(zcCompletedDifferentialModuleStageDifferential_isCrossedDifferential C ψ i)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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)Show proof
(mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule
C ψ i x).1
(crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel
(C := C) (ψ := ψ) i hx)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcCompletedDifferentialModulePreStageKernelIntersection :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
⨅ i : ZCCompletedDifferentialModuleIndex C ψ,
zcCompletedDifferentialModulePreStageKernel C ψ iThe common finite-stage kernel on the pre-module.
theorem mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff
(x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
x ∈ zcCompletedDifferentialModulePreStageKernelIntersection C ψ ↔
∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcCompletedDifferentialModulePreStageMap C ψ i x ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)Membership in the intersection of completed differential-module pre-stage kernels is equivalent to vanishing of the corresponding finite-stage coordinate.
Show proof
by
rw [zcCompletedDifferentialModulePreStageKernelIntersection, Submodule.mem_iInf]
constructor
· intro hx i
exact
(mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule
C ψ i x).1 (hx i)
· intro hx i
exact
(mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule
C ψ i x).2 (hx i)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□abbrev zcCompletedDifferentialRelationFiniteClosedSubmodule :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialModulePreStageKernelIntersection C ψThe finite-stage closed relation submodule defining the separated completed \(\psi\)-differential module.
abbrev ZCSeparatedCompletedDifferentialModule : Type u :=
CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G ⧸
zcCompletedDifferentialRelationFiniteClosedSubmodule C ψThe separated completed \(\psi\)-differential module. This is the finite-stage separated quotient used for the profinite Crowell middle term.
abbrev ZCApsi : Type u :=
ZCSeparatedCompletedDifferentialModule C ψMathematical Crowell module \(A_{\psi}(C)\). By convention in this development, \(A_{\psi}(C)\) is the closed/separated finite-stage quotient, not the algebraic quotient of the \(\mathbb{Z}_C\)-completed differential module.
theorem crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule :
crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ) ≤
zcCompletedDifferentialRelationFiniteClosedSubmodule C ψAlgebraic crossed-differential relations vanish in the finite-stage separated quotient.
Show proof
by
intro x hx
rw [zcCompletedDifferentialRelationFiniteClosedSubmodule,
mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff]
intro i
exact zcCompletedDifferentialModulePreStageMap_mem_relationSubmodule_of_mem C ψ i hxProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcSeparatedUniversalDifferential (g : G) :
ZCSeparatedCompletedDifferentialModule C ψ :=
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
(Finsupp.single g 1)The universal differential into the separated completed quotient.
theorem zcSeparatedUniversalDifferential_mul (g h : G) :
zcSeparatedUniversalDifferential C ψ (g * h) =
zcSeparatedUniversalDifferential C ψ g +
zcCompletedGroupAlgebraScalar C ψ g •
zcSeparatedUniversalDifferential C ψ hThe separated universal differential satisfies the crossed product rule.
Show proof
by
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' :
zcSeparatedUniversalDifferential C ψ (g * h) -
(zcSeparatedUniversalDifferential C ψ g +
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
(zcCompletedGroupAlgebraScalar C ψ g • Finsupp.single h 1)) = 0 := by
simpa [zcSeparatedUniversalDifferential, crossedDifferentialRelationElement] using hzero
have hsmul :
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
(zcCompletedGroupAlgebraScalar C ψ g • Finsupp.single h 1) =
zcCompletedGroupAlgebraScalar C ψ g •
zcSeparatedUniversalDifferential C ψ h := by
simpa [zcSeparatedUniversalDifferential, Submodule.mkQ_apply] using
(Submodule.Quotient.mk_smul
(p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
(r := zcCompletedGroupAlgebraScalar C ψ g)
(x := Finsupp.single h 1))
have hzero'' :
zcSeparatedUniversalDifferential C ψ (g * h) -
(zcSeparatedUniversalDifferential C ψ g +
zcCompletedGroupAlgebraScalar C ψ g •
zcSeparatedUniversalDifferential C ψ h) = 0 := by
rw [hsmul] at hzero'
exact hzero'
exact sub_eq_zero.mp hzero''Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcSeparatedUniversalDifferential_isCrossed :
IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C ψ)
(zcSeparatedUniversalDifferential C ψ)The separated universal differential is a crossed differential.
Show proof
by
intro g h
exact zcSeparatedUniversalDifferential_mul C ψ g hProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcSeparatedUniversalDifferential_commutator_right_kernel
(g h : G) (hh : ψ h = 1) :
zcSeparatedUniversalDifferential C ψ ⁅g, h⁆ =
(zcGroupLike C H (ψ g) - 1) •
zcSeparatedUniversalDifferential C ψ hCommutator formula for the separated universal differential when the right factor lies in the kernel of the target homomorphism.
Show proof
by
let δ := zcSeparatedUniversalDifferential C ψ
let coeff := zcCompletedGroupAlgebraScalar C ψ
have hcross :
IsCrossedDifferential coeff δ :=
zcSeparatedUniversalDifferential_isCrossed C ψ
have hcomm := IsCrossedDifferential.commutator hcross g h
have hconj : ψ (g * h * g⁻¹) = 1 := by
simp only [map_mul, hh, mul_one, map_inv, mul_inv_cancel]
have hcommKer : ψ ⁅g, h⁆ = 1 := by
simp only [commutatorElement_def, map_mul, hh, mul_one, map_inv, mul_inv_cancel, inv_one]
calc
δ ⁅g, h⁆ =
δ g + zcGroupLike C H (ψ g) • δ h - δ g - δ h := by
simpa only [δ, coeff, zcCompletedGroupAlgebraScalar_apply, hconj,
hcommKer, map_one, one_smul] using hcomm
_ = zcGroupLike C H (ψ g) • δ h - δ h := by
abel
_ = (zcGroupLike C H (ψ g) - 1) • δ h := by
rw [sub_smul, one_smul]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcSeparatedCompletedDifferentialModule_mk_eq_zero_iff
(x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x =
(0 : ZCSeparatedCompletedDifferentialModule C ψ) ↔
∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcCompletedDifferentialModulePreStageMap C ψ i x ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)A representative is zero in the separated quotient exactly when all finite reductions are finite crossed-differential relations.
Show proof
by
constructor
· intro hx
exact
(mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff C ψ x).1
((Submodule.Quotient.mk_eq_zero
(p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
(x := x)).1 hx)
· intro hx
exact
(Submodule.Quotient.mk_eq_zero
(p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
(x := x)).2
((mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff C ψ x).2 hx)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcSeparatedCompletedDifferentialModuleStageProjectionAdd
(i : ZCCompletedDifferentialModuleIndex C ψ) :
ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedDifferentialModuleStage C ψ i :=
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).liftQ
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H)
(zcCompletedDifferentialModuleStageDifferential C ψ i))
(by
intro x hx
rw [LinearMap.mem_ker]
have hxstage :
zcCompletedDifferentialModulePreStageMap C ψ i x ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i) :=
(mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff C ψ x).1
(by
simpa [zcCompletedDifferentialRelationFiniteClosedSubmodule] using hx) i
have hq :
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i x) = 0 :=
(Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i))
(x := zcCompletedDifferentialModulePreStageMap C ψ i x)).2 hxstage
rw [zcCompletedDifferentialModulePreStageMap_mkQ] at hq
exact hq)Finite-stage projection from the separated completed quotient.
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) xThe separated finite-stage projection of a quotient representative is the finite-stage crossed-differential lift of that representative.
Show proof
by
rw [zcSeparatedCompletedDifferentialModuleStageProjectionAdd, Submodule.mkQ_apply,
Submodule.liftQ_apply]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcSeparatedCompletedDifferentialModuleStageProjectionAdd_universal
(i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i
(zcSeparatedUniversalDifferential C ψ g) =
zcCompletedDifferentialModuleStageDifferential C ψ i gShow proof
by
rw [zcSeparatedUniversalDifferential,
zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ]
simp only [crossedDifferentialModuleLiftLinear_single, one_smul]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcSeparatedCompletedDifferentialModuleStageProjectionProduct :
ZCSeparatedCompletedDifferentialModule C ψ →
∀ i : ZCCompletedDifferentialModuleIndex C ψ,
ZCCompletedDifferentialModuleStage C ψ i :=
fun a i => zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i aThe product of all finite-stage projections from the separated completed quotient.
theorem zcSeparatedCompletedDifferentialModuleStageProjectionProduct_apply
(a : ZCSeparatedCompletedDifferentialModule C ψ)
(i : ZCCompletedDifferentialModuleIndex C ψ) :
zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ a i =
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i aApplying the projection map to a completed element returns its corresponding finite-stage coordinate.
Show proof
rflProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcSeparatedCompletedDifferentialModuleStageProjectionsSeparate :
∀ x : ZCSeparatedCompletedDifferentialModule C ψ,
(∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x = 0) →
x = 0The finite-stage projections separate points of the separated completed quotient.
Show proof
by
intro x
refine Submodule.Quotient.induction_on
(p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
(C := fun x =>
(∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x = 0) →
x = 0)
x ?_
intro y hy
apply
(Submodule.Quotient.mk_eq_zero
(p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
(x := y)).2
exact
(mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff C ψ y).2
(by
intro i
have hlin :
crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H)
(zcCompletedDifferentialModuleStageDifferential C ψ i) y = 0 := by
simpa using hy i
have hq :
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i y) = 0 := by
rw [zcCompletedDifferentialModulePreStageMap_mkQ]
exact hlin
exact
(Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i))
(x := zcCompletedDifferentialModulePreStageMap C ψ i y)).1 hq)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcSeparatedCompletedDifferentialModuleStageProjectionProduct_injective :
Function.Injective
(zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ)The finite-stage projection product is injective on the separated completed quotient.
Show proof
by
intro x y hxy
apply sub_eq_zero.mp
apply zcSeparatedCompletedDifferentialModuleStageProjectionsSeparate C ψ
intro i
have hi :
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x =
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i y := by
simpa [zcSeparatedCompletedDifferentialModuleStageProjectionProduct] using congrFun hxy i
rw [map_sub, hi, sub_self]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcSeparatedCompletedDifferentialModuleStageProjection_ext
{a b : ZCSeparatedCompletedDifferentialModule C ψ}
(h : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a =
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i b) :
a = bExtensionality for the separated completed quotient by finite-stage projections.
Show proof
zcSeparatedCompletedDifferentialModuleStageProjectionProduct_injective C ψ
(funext h)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcCompletedDifferentialModuleToSeparated :
ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
ZCSeparatedCompletedDifferentialModule C ψ :=
(crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ)).liftQ
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
(by
intro x hx
rw [LinearMap.mem_ker]
exact
(Submodule.Quotient.mk_eq_zero
(p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
(x := x)).2
(crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule C ψ hx))The natural map from the algebraic quotient to the finite-stage separated quotient.
theorem zcCompletedDifferentialModuleToSeparated_universal (g : G) :
zcCompletedDifferentialModuleToSeparated C ψ
(zcUniversalDifferential C ψ g) =
zcSeparatedUniversalDifferential C ψ gThe quotient map to the separated completed module sends the universal differential to the separated universal differential.
Show proof
by
simp only [zcCompletedDifferentialModuleToSeparated, zcUniversalDifferential, universalCrossedDifferential,
Submodule.mkQ_apply, Submodule.liftQ_apply, zcSeparatedUniversalDifferential]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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 = 0The pre-quotient completed boundary kills the finite-stage closed relation submodule. This is the descent input for the separated boundary \(A_{\psi}(C)_{\mathrm{sep}} \to \mathbb{Z}_C\llbracket H\rrbracket\).
Show proof
by
apply zcCompletedGroupAlgebraProjection_ext
intro j
let i := zcCompletedDifferentialModuleComapIndex C hC ψc j
have hxall :
∀ i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom,
zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i) := by
rw [zcCompletedDifferentialRelationFiniteClosedSubmodule] at hx
exact
(mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff
C ψc.toMonoidHom x).1 hx
have hxstage :
zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i) :=
hxall i
have hstage_zero :
zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
((crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) = 0 := by
have hq :
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x) = 0 :=
(Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i))
(x := zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)).2 hxstage
rw [hq, map_zero]
have hcompat :=
congrArg
(fun f =>
f
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x))
(zcDiffModuleStageBoundaryCompletedLinearMap_comp_stageProj
C ψc.toMonoidHom i)
have hstage_proj :
zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x) =
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x) := by
simpa [zcCompletedDifferentialModuleStageProjection,
zcCompletedDifferentialModuleLift, crossedDifferentialModuleLift] using
(zcCompletedDifferentialModulePreStageMap_mkQ C ψc.toMonoidHom i x).symm
have hboundary_quot :
zcToCompletedGroupAlgebra C ψc.toMonoidHom
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x) =
crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x := by
rfl
have hproj_eq :
zcCompletedGroupAlgebraProjection C H j
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x) =
zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
((crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) := by
calc
zcCompletedGroupAlgebraProjection C H j
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom) x) =
zcCompletedGroupAlgebraProjection C H i.target
(zcToCompletedGroupAlgebra C ψc.toMonoidHom
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x)) := by
rw [hboundary_quot]
simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedDifferentialModuleComapIndex, i]
_ =
zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
(zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψc.toMonoidHom)).mkQ x)) := by
simpa [LinearMap.comp_apply] using hcompat.symm
_ =
zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
((crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψc.toMonoidHom i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψc.toMonoidHom i x)) := by
rw [hstage_proj]
rw [hproj_eq, hstage_zero]
simp only [zcCompletedGroupAlgebraProjection_zero]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
(ψc : ContinuousMonoidHom G H) :
ZCSeparatedCompletedDifferentialModule C ψc.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
ZCCompletedGroupAlgebra C H :=
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψc.toMonoidHom).liftQ
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H)
(zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom))
(by
intro x hx
rw [LinearMap.mem_ker]
exact crossedDifferentialBoundaryLiftLinear_kills_finiteClosedSubmodule
C hC ψc hx)The completed boundary descends to the separated completed differential module.
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 gThe universal completed Fox map from the separated completed differential module to the completed group algebra is characterized by finite-stage Fox coordinate formulas.
Show proof
by
rw [zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra,
zcSeparatedUniversalDifferential, Submodule.mkQ_apply, Submodule.liftQ_apply]
simp only [ContinuousMonoidHom.coe_toMonoidHom, crossedDifferentialModuleLiftLinear_single, smul_eq_mul,
one_mul]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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.toMonoidHomThe completed Fox map to the completed group algebra agrees with the separated quotient map on finite-stage coordinates.
Show proof
by
apply zcCompletedDifferentialModuleHom_ext C ψc.toMonoidHom
intro g
rw [LinearMap.comp_apply, zcCompletedDifferentialModuleToSeparated_universal,
zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_universal,
zcToCompletedGroupAlgebra_universal]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations : Prop :=
∀ x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G,
(∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcCompletedDifferentialModulePreStageMap C ψ i x ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)) →
x ∈ crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)Algebraic relation-reflection form of finite-stage separation: if every finite source, target, and coefficient reduction of a completed pre-module element is a finite crossed-differential relation, then the original element is already in the raw completed crossed-differential relation submodule. This is an algebraic compatibility predicate for the \(\mathbb{Z}_C\)-completed differential module, not an input for the final separated profinite Crowell middle term.
def zcCompletedDifferentialPreModuleNaturalTopology :
TopologicalSpace (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
TopologicalSpace.induced
(zcCompletedDifferentialPreModuleStageFamilyMap C ψ) inferInstanceThe finite-stage topology on the completed pre-module, before quotienting by the crossed-differential relations.
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)Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
let S := zcCompletedDifferentialPreModuleStageSystem C ψ
have hfamily :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(ZCCompletedDifferentialPreModuleStageFamily C ψ)
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(zcCompletedDifferentialPreModuleStageFamilyMap C ψ) :=
continuous_induced_dom
have hproj := (S.continuous_projection i).comp hfamily
simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using hprojProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcSeparatedCompletedDifferentialModuleNaturalTopology :
TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
TopologicalSpace.coinduced
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)The separated completed module carries the quotient topology induced from the finite-stage topology on the completed pre-module.
theorem continuous_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(ZCSeparatedCompletedDifferentialModule C ψ)
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
(zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQThe quotient map to the separated completed module is continuous for the finite-stage pre-module topology and the separated quotient topology.
Show proof
continuous_coinduced_rngProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem isQuotientMap_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology :
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)The quotient map defining the separated completed module is a quotient map for the finite-stage pre-module topology.
Show proof
zcCompletedDifferentialPreModuleNaturalTopology C ψ
letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
Topology.IsQuotientMap (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ := by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
rw [Topology.isQuotientMap_iff]
constructor
· exact
Submodule.Quotient.mk_surjective
(p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
· intro s
rflProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcSeparatedCompletedDifferentialModule_iff_comp_mkQ
{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))Continuity out of the separated completed module can be tested after precomposing with the defining quotient map.
Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
simpa [Function.comp_def] using
(isQuotientMap_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology
C ψ).continuous_iff (g := f)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcSepDiffModuleStageProjAdd_naturalTopology
(i : ZCCompletedDifferentialModuleIndex C ψ) :
@Continuous
(ZCSeparatedCompletedDifferentialModule C ψ)
(ZCCompletedDifferentialModuleStage C ψ i)
(zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
inferInstance
(zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i)Each finite-stage projection from the separated completed quotient is continuous for the separated quotient topology.
Show proof
by
letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
rw [continuous_coinduced_dom]
change
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(ZCCompletedDifferentialModuleStage C ψ i)
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(fun x =>
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i
((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x))
letI : TopologicalSpace
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⊥
letI : DiscreteTopology
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⟨rfl⟩
have hpre :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i))
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(zcCompletedDifferentialModulePreStageMap C ψ i) :=
continuous_zcCompletedDifferentialModulePreStageMap_naturalTopology C ψ i
letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
have hq :
Continuous
(fun y :
CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i) =>
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ y) :=
continuous_of_discreteTopology
have hcoord :
(fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i
((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x)) =
(fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i x)) := by
funext x
rw [zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ,
← zcCompletedDifferentialModulePreStageMap_mkQ]
rw [hcoord]
exact hq.comp hpreProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcSepDiffModuleStageProjProduct_naturalTopology :
@Continuous
(ZCSeparatedCompletedDifferentialModule C ψ)
(∀ i : ZCCompletedDifferentialModuleIndex C ψ,
ZCCompletedDifferentialModuleStage C ψ i)
(zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
inferInstance
(zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ)The separated finite-stage projection product is continuous for the separated quotient topology.
Show proof
by
letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
exact
continuous_pi fun i =>
by
simpa [zcSeparatedCompletedDifferentialModuleStageProjectionProduct] using
continuous_zcSepDiffModuleStageProjAdd_naturalTopology C ψ iProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem t2Space_zcSeparatedCompletedDifferentialModuleNaturalTopology :
@T2Space
(ZCSeparatedCompletedDifferentialModule C ψ)
(zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)The separated completed quotient is Hausdorff for the separated finite-stage quotient topology.
Show proof
by
letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
exact T2Space.of_injective_continuous
(zcSeparatedCompletedDifferentialModuleStageProjectionProduct_injective C ψ)
(continuous_zcSepDiffModuleStageProjProduct_naturalTopology C ψ)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcSepDiffModuleNaturalTopology_eq_induced_stageProjProduct
[Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
(hdir : Directed (· ≤ ·)
(id : ZCCompletedDifferentialModuleIndex C ψ →
ZCCompletedDifferentialModuleIndex C ψ)) :
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ =
TopologicalSpace.induced
(zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstanceShow proof
by
ext U
constructor
· intro hU
let Tind : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
TopologicalSpace.induced
(zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstance
rw [@isOpen_iff_forall_mem_open
(ZCSeparatedCompletedDifferentialModule C ψ) Tind U]
intro x hxU
refine Submodule.Quotient.induction_on
(p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
(C := fun x =>
x ∈ U → ∃ t, t ⊆ U ∧ @IsOpen
(ZCSeparatedCompletedDifferentialModule C ψ) Tind t ∧ x ∈ t)
x ?_ hxU
intro a haU
let q :
CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G →
ZCSeparatedCompletedDifferentialModule C ψ :=
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
have hpreOpen :
@IsOpen
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
(q ⁻¹' U) := by
simpa [q, zcSeparatedCompletedDifferentialModuleNaturalTopology] using hU
rcases isOpen_induced_iff.mp hpreOpen with ⟨V, hVopen, hVeq⟩
have haV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ a ∈ V := by
have haU' : a ∈ q ⁻¹' U := haU
rwa [← hVeq] at haU'
let S := zcCompletedDifferentialPreModuleStageSystem C ψ
rcases S.exists_projection_preimage_subset hdir hVopen haV with
⟨i, W, hWopen, haW, hWV⟩
let t : Set (ZCSeparatedCompletedDifferentialModule C ψ) :=
{z | zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i z =
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q a)}
refine ⟨t, ?_, ?_, ?_⟩
· intro z hz
refine Submodule.Quotient.induction_on
(p := zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)
(C := fun z => z ∈ t → z ∈ U) z ?_ hz
intro b hb
have hcoord :
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q b) =
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q a) := hb
have hstageRel :
zcCompletedDifferentialModulePreStageMap C ψ i (b - a) ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i) := by
apply (Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i))
(x := zcCompletedDifferentialModulePreStageMap C ψ i (b - a))).1
have hq :
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i (b - a)) = 0 := by
have hbq :
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i b) =
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i a) := by
rw [zcCompletedDifferentialModulePreStageMap_mkQ,
zcCompletedDifferentialModulePreStageMap_mkQ]
simpa [q] using hcoord
have hzero :
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i b) -
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i a) = 0 :=
sub_eq_zero.mpr hbq
simpa [map_sub] using hzero
exact hq
rcases zcCompletedDifferentialModulePreStageMap_relationSubmodule_surjective
C ψ i hstageRel with
⟨r, hr, hrstage⟩
have hqa : q (b - r) = q b := by
have hrclosed : r ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ :=
crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule C ψ hr
apply (Submodule.Quotient.eq
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ)).2
change (b - r) - b ∈ zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ
have hdiff : (b - r) - b = -r := by
abel
rw [hdiff]
exact (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).neg_mem hrclosed
have hpre_eq :
zcCompletedDifferentialModulePreStageMap C ψ i (b - r) =
zcCompletedDifferentialModulePreStageMap C ψ i a := by
have hcalc :
zcCompletedDifferentialModulePreStageMap C ψ i (b - a) =
zcCompletedDifferentialModulePreStageMap C ψ i r := hrstage.symm
have hsub :
zcCompletedDifferentialModulePreStageMap C ψ i b -
zcCompletedDifferentialModulePreStageMap C ψ i a =
zcCompletedDifferentialModulePreStageMap C ψ i r := by
simpa [map_sub] using hcalc
rw [map_sub]
rw [← hsub]
abel
have hbW : S.projection i
(zcCompletedDifferentialPreModuleStageFamilyMap C ψ (b - r)) ∈ W := by
change zcCompletedDifferentialModulePreStageMap C ψ i (b - r) ∈ W
rw [hpre_eq]
simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using haW
have hbV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ (b - r) ∈ V := hWV hbW
have hbU : q (b - r) ∈ U := by
have hbV' :
(b - r) ∈ zcCompletedDifferentialPreModuleStageFamilyMap C ψ ⁻¹' V := hbV
rwa [hVeq] at hbV'
rwa [hqa] at hbU
· letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) := Tind
have hprod :
Continuous (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ) :=
continuous_induced_dom
have hcoord :
Continuous (fun z : ZCSeparatedCompletedDifferentialModule C ψ =>
zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i z) := by
simpa [zcSeparatedCompletedDifferentialModuleStageProjectionProduct] using
(continuous_apply i).comp hprod
haveI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
exact (isOpen_discrete
({zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i (q a)} :
Set (ZCCompletedDifferentialModuleStage C ψ i))).preimage hcoord
· exact rfl
· intro hU
letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVU⟩
rw [← hVU]
exact hVopen.preimage
(continuous_zcSepDiffModuleStageProjProduct_naturalTopology C ψ)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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))Show proof
by
rw [continuous_induced_rng]
let S := zcCompletedDifferentialPreModuleStageSystem C ψ
let preSingle :
∀ i : ZCCompletedDifferentialModuleIndex C ψ, G → S.X i := fun i g =>
zcCompletedDifferentialModulePreStageMap C ψ i
(Finsupp.single g (1 : ZCCompletedGroupAlgebra C H))
have hpreSingle_continuous : ∀ i, Continuous (preSingle i) := by
intro i
letI : TopologicalSpace
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⊥
letI : DiscreteTopology
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⟨rfl⟩
have hsource :
Continuous (zcCompletedDifferentialModuleStageSourceProj C ψ i) := by
simpa [zcCompletedDifferentialModuleStageSourceProj] using
(continuous_quotient_mk' : Continuous (fun g : G =>
QuotientGroup.mk' (i.source.1 : Subgroup G) g))
have hsingle :
Continuous (fun q : zcCompletedDifferentialModuleStageSource C ψ i =>
Finsupp.single q (1 : zcCompletedDifferentialModuleStageRing C ψ i)) :=
continuous_of_discreteTopology
simpa [preSingle, zcCompletedDifferentialModulePreStageMap_single] using
hsingle.comp hsource
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 hLiftProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcSeparatedUniversalDifferential_naturalTopology :
@Continuous G
(ZCSeparatedCompletedDifferentialModule C ψ)
inferInstance
(zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
(zcSeparatedUniversalDifferential C ψ)The separated universal differential is continuous for the separated finite-stage quotient topology.
Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
exact
(continuous_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology C ψ).comp
(continuous_zcCompletedDifferentialPreModule_single_one_naturalTopology C ψ)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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)Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
letI : TopologicalSpace
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⊥
letI : DiscreteTopology
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⟨rfl⟩
have hpre :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i))
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(zcCompletedDifferentialModulePreStageMap C ψ i) :=
continuous_zcCompletedDifferentialModulePreStageMap_naturalTopology C ψ i
have hL : Continuous L := continuous_of_discreteTopology
have hfun :
(fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta x) =
fun x => L (zcCompletedDifferentialModulePreStageMap C ψ i x) := by
funext x
exact hfactor x
change
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
A
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(fun x =>
crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta x)
rw [hfun]
exact hL.comp hpreProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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))Show proof
by
exact
continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor
C ψ
(zcCompletedDifferentialModuleStageDifferential C ψ i)
i
(fun y =>
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ y)
(by
intro x
exact (zcCompletedDifferentialModulePreStageMap_mkQ C ψ i x).symm)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcCompletedDifferentialModuleRelationSubmoduleClosed : Prop :=
@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))The raw algebraic crossed-differential relation submodule is closed for the finite-stage topology on the completed pre-module. This closedness condition makes the algebraic quotient separated; the separated quotient construction records this condition structurally.
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 ψA useful non-circular closedness criterion. If a Hausdorff/\(T_1\) target receives an injective linear map from the algebraic completed differential module, and the composite from the completed pre-module is continuous for the finite-stage pre-module topology, then the defining crossed-differential relation submodule is closed. In applications the target is usually a finite coordinate module \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\). The formulation isolates the real topological input: continuity of the pre-quotient coordinate map.
Show proof
by
letI : 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 hcontProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcCompletedDifferentialModule_mkQ_naturalTopology :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(ZCCompletedDifferentialModule C ψ)
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
(zcCompletedDifferentialModuleNaturalTopology C ψ)
(crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ)).mkQThe quotient map from the completed pre-module to the algebraic quotient is continuous for the finite-stage topologies.
Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleNaturalTopology C ψ
rw [continuous_induced_rng]
change Continuous
(fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
fun i : ZCCompletedDifferentialModuleIndex C ψ =>
zcCompletedDifferentialModuleStageProjectionAdd C ψ i
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ)).mkQ x))
refine continuous_pi fun i => ?_
let S := zcCompletedDifferentialPreModuleStageSystem C ψ
letI : TopologicalSpace
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⊥
letI : DiscreteTopology
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⟨rfl⟩
have hpre :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i))
(zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance
(zcCompletedDifferentialModulePreStageMap C ψ i) := by
have hfamily :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(ZCCompletedDifferentialPreModuleStageFamily C ψ)
(zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance
(zcCompletedDifferentialPreModuleStageFamilyMap C ψ) :=
continuous_induced_dom
have hproj := (S.continuous_projection i).comp hfamily
simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using hproj
letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ i) := inferInstance
have hq :
Continuous
(fun y :
CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i) =>
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ y) :=
continuous_of_discreteTopology
have hcomp := hq.comp hpre
have hcoord :
(fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
zcCompletedDifferentialModuleStageProjectionAdd C ψ i
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ)).mkQ x)) =
(fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
(crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)).mkQ
(zcCompletedDifferentialModulePreStageMap C ψ i x)) := by
funext x
rw [zcCompletedDifferentialModuleStageProjectionAdd_apply,
zcCompletedDifferentialModuleStageProjection_mkQ,
← zcCompletedDifferentialModulePreStageMap_mkQ]
rw [hcoord]
exact hcompProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_of_t1_naturalTopology
(hT1 :
@T1Space (ZCCompletedDifferentialModule C ψ)
(zcCompletedDifferentialModuleNaturalTopology C ψ)) :
zcCompletedDifferentialModuleRelationSubmoduleClosed C ψIf the finite-stage natural topology on the algebraic quotient is already \(T_1\), then the defining crossed-differential relation submodule is closed in the completed pre-module finite-stage topology. This is the quotient-topology reflection statement: the relation submodule is the preimage of \({0}\) under the continuous algebraic quotient map.
Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleNaturalTopology C ψ
letI : T1Space (ZCCompletedDifferentialModule C ψ) := hT1
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 =>
(crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ)).mkQ x) ⁻¹'
({0} : Set (ZCCompletedDifferentialModule C ψ)) := by
ext x
simp only [SetLike.mem_coe, Submodule.mkQ_apply, Set.mem_preimage, Set.mem_singleton_iff,
Submodule.Quotient.mk_eq_zero]
rw [hpreimage]
exact isClosed_singleton.preimage
(continuous_zcCompletedDifferentialModule_mkQ_naturalTopology C ψ)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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 ψA quotient-level non-circular closedness criterion. If the algebraic completed differential module admits an injective continuous map from its finite-stage natural topology to a \(T_1\) target, then the defining crossed-differential relation submodule is closed in the pre-module finite-stage topology. This packages the topological reflection step through the continuous algebraic quotient map from the pre-module.
Show proof
zcDiffModuleRelSubmoduleClosed_of_inj_continuous_comp_mkQ
C ψ L hLinj
(@Continuous.comp
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(ZCCompletedDifferentialModule C ψ) M
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
(zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
(f := (crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ)).mkQ)
(g := L) hcont
(continuous_zcCompletedDifferentialModule_mkQ_naturalTopology C ψ))Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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))Finite relation-valued reductions put a pre-module element in the finite-stage closure of the completed crossed-differential relation submodule.
Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
rw [mem_closure_iff]
intro U hU hxU
rcases isOpen_induced_iff.mp hU with ⟨V, hVopen, hVeq⟩
have hxV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ x ∈ V := by
rw [← hVeq] at hxU
exact hxU
let S := zcCompletedDifferentialPreModuleStageSystem C ψ
rcases S.exists_projection_preimage_subset hdir hVopen hxV with
⟨i, W, hWopen, hxW, hWU⟩
rcases zcCompletedDifferentialModuleFiniteRelationReductions_finiteStageApproximation
C ψ hdir ({i} : Finset (ZCCompletedDifferentialModuleIndex C ψ)) x hx with
⟨r, hr, hrstage⟩
refine ⟨r, ?_, hr⟩
have hri : zcCompletedDifferentialModulePreStageMap C ψ i r =
zcCompletedDifferentialModulePreStageMap C ψ i x := by
exact hrstage i (by simp only [Finset.mem_singleton])
have hrW :
S.projection i (zcCompletedDifferentialPreModuleStageFamilyMap C ψ r) ∈ W := by
change zcCompletedDifferentialModulePreStageMap C ψ i r ∈ W
rw [hri]
simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using hxW
have hrV : zcCompletedDifferentialPreModuleStageFamilyMap C ψ r ∈ V := hWU hrW
rw [← hVeq]
exact hrVProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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))Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
let S := zcCompletedDifferentialPreModuleStageSystem C ψ
letI : TopologicalSpace
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⊥
letI : DiscreteTopology
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)) :=
⟨rfl⟩
have hpre :
Continuous (zcCompletedDifferentialModulePreStageMap C ψ i) := by
have hfamily :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
(ZCCompletedDifferentialPreModuleStageFamily C ψ)
(zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance
(zcCompletedDifferentialPreModuleStageFamilyMap C ψ) :=
continuous_induced_dom
have hproj := (S.continuous_projection i).comp hfamily
simpa [S, zcCompletedDifferentialPreModuleStageFamilyMap_projection] using hproj
have hpreimage :
IsClosed
((zcCompletedDifferentialModulePreStageMap C ψ i) ⁻¹'
(((crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)) :
Submodule
(zcCompletedDifferentialModuleStageRing C ψ i)
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i))) :
Set (CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)))) := by
exact
(isClosed_discrete
(((crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)) :
Submodule
(zcCompletedDifferentialModuleStageRing C ψ i)
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i))) :
Set (CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)))).preimage hpre
have hset :
((zcCompletedDifferentialModulePreStageKernel C ψ i :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) =
((zcCompletedDifferentialModulePreStageMap C ψ i) ⁻¹'
(((crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i)) :
Submodule
(zcCompletedDifferentialModuleStageRing C ψ i)
(CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i))) :
Set (CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψ i)
(zcCompletedDifferentialModuleStageSource C ψ i)))) := by
ext x
exact
mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule
C ψ i x
simpa [hset] using hpreimageProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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))Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
change IsClosed
((zcCompletedDifferentialModulePreStageKernelIntersection C ψ :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G))
rw [zcCompletedDifferentialModulePreStageKernelIntersection]
simpa [Submodule.coe_iInf] using
(isClosed_iInter
(fun i =>
isClosed_zcCompletedDifferentialModulePreStageKernel_naturalTopology
C ψ i))Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem isClosed_zero_zcSeparatedCompletedDifferentialModuleNaturalTopology :
@IsClosed (ZCSeparatedCompletedDifferentialModule C ψ)
(zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
({0} : Set (ZCSeparatedCompletedDifferentialModule C ψ))Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
rw [zcSeparatedCompletedDifferentialModuleNaturalTopology, isClosed_coinduced]
have hpreimage :
((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ ⁻¹'
({0} : Set (ZCSeparatedCompletedDifferentialModule C ψ))) =
((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
ext x
simp only [Set.mem_preimage, Submodule.mkQ_apply, Set.mem_singleton_iff, Submodule.Quotient.mk_eq_zero,
SetLike.mem_coe]
rw [hpreimage]
exact isClosed_zcCompletedDifferentialRelationFiniteClosedSubmodule_naturalTopology C ψProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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))Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
apply Set.Subset.antisymm
· intro x hxcl
change x ∈ zcCompletedDifferentialModulePreStageKernelIntersection C ψ
exact
(mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff C ψ x).2
(by
intro i
have hclosed_i :=
isClosed_zcCompletedDifferentialModulePreStageKernel_naturalTopology C ψ i
have hsubset_i :
((crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) ⊆
((zcCompletedDifferentialModulePreStageKernel C ψ i :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
intro y hy
exact
crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel
(C := C) (ψ := ψ) i hy
have hxker : x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i :=
closure_minimal hsubset_i hclosed_i hxcl
exact
(mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule
C ψ i x).1 hxker)
· intro x hxhat
have hxstage :
∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcCompletedDifferentialModulePreStageMap C ψ i x ∈
crossedDifferentialRelationSubmodule
(zcCompletedDifferentialModuleStageScalar C ψ i) :=
(mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff C ψ x).1
(by
simpa [zcCompletedDifferentialRelationFiniteClosedSubmodule] using hxhat)
exact
zcDiffModuleFiniteRelationReductions_mem_closure_relSubmodule
C ψ hdir x hxstageProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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 : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(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 = 0A continuous pre-quotient lift to a \(T_1\) target kills the finite-stage closed relation denominator. This is the general descent criterion for maps out of the separated completed universal module.
Show proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
have hxcl :
x ∈ closure
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ) :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) := by
have hEq :=
closure_crossedDifferentialRelationSubmodule_eq_finiteClosedSubmodule
C ψ hdir
rw [hEq]
exact hx
have hker_closed :
IsClosed
((fun y : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta y) ⁻¹'
({0} : Set A)) :=
isClosed_singleton.preimage hcont
have hrel_subset_ker :
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ) :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :
Set (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) ⊆
((fun y : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta y) ⁻¹'
({0} : Set A)) := by
intro y hy
exact
(crossedDifferentialRelationSubmodule_le_ker
(A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdelta) hy
exact closure_minimal hrel_subset_ker hker_closed hxclProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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 : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hcont :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
A
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta)) :
ZCSeparatedCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A :=
(zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).liftQ
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta)
(by
intro x hx
rw [LinearMap.mem_ker]
exact
crossedDifferentialModuleLiftLinear_kills_finiteClosedSubmodule_of_continuous
C ψ hdir delta hdelta hcont hx)The separated universal lift induced by a crossed differential whose pre-quotient lift is continuous for the finite-stage topology.
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 : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hcont :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
A
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta))
(g : G) :
zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
C ψ hdir delta hdelta hcont
(zcSeparatedUniversalDifferential C ψ g) =
delta gThe separated lift of a continuous crossed-differential prelift sends the separated universal differential of \(g\) to \(\delta(g)\).
Show proof
by
rw [zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift,
zcSeparatedUniversalDifferential, Submodule.mkQ_apply, Submodule.liftQ_apply]
simp only [crossedDifferentialModuleLiftLinear_single, one_smul]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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 = hLinear maps out of the separated completed differential module are equal when they agree on all separated universal differentials.
Show proof
by
apply Submodule.linearMap_qext _
apply Finsupp.lhom_ext
intro g r
have hsingle :
((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
(Finsupp.single g r) :
ZCSeparatedCompletedDifferentialModule C ψ) =
r • zcSeparatedUniversalDifferential C ψ g := by
rw [← Finsupp.smul_single_one]
rfl
change f ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
(Finsupp.single g r)) =
h ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ
(Finsupp.single g r))
simpa [hsingle, map_smul] using congrArg (fun z => r • z) (hfh g)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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 : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(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 hdelta hcontThe separated lift of a continuous crossed differential is unique among linear maps with the prescribed values on separated universal differentials.
Show proof
by
apply zcSeparatedCompletedDifferentialModuleHom_ext C ψ
intro g
rw [hf g, zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_universal]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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 : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(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 hdelta hcont
cont := ?_ }
rw [continuous_coinduced_dom]
change
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
A
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(fun x =>
zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
C ψ hdir delta hdelta hcont
((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x))
have hcomp :
(fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
C ψ hdir delta hdelta 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 hcontThe separated universal lift is bundled as a continuous linear map for the separated quotient topology.
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 : G → A)
(hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
(hcont :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
A
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta))
(m : ZCSeparatedCompletedDifferentialModule C ψ) :
zcSeparatedCompletedDifferentialModuleLiftContinuousLinearMapOfContinuousPrelift
C ψ hdir delta hdelta hcont m =
zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
C ψ hdir delta hdelta hcont mThe separated completed differential-module lift is evaluated after projection to the relevant finite-stage separated quotient.
Show proof
rflProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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 : G → A),
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta →
Continuous delta →
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
A
(zcCompletedDifferentialPreModuleNaturalTopology C ψ)
inferInstance
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta)) :
{delta : G → A //
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta ∧
Continuous delta} ≃
(letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) where
toFun delta :=
zcSeparatedCompletedDifferentialModuleLiftContinuousLinearMapOfContinuousPrelift
C ψ hdir delta.1 delta.2.1 (hprelift delta.1 delta.2.1 delta.2.2)
invFun f := by
letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
exact ⟨fun g => f (zcSeparatedUniversalDifferential C ψ g), by
constructor
· intro g h
change f (zcSeparatedUniversalDifferential C ψ (g * h)) =
f (zcSeparatedUniversalDifferential C ψ g) +
zcCompletedGroupAlgebraScalar C ψ g •
f (zcSeparatedUniversalDifferential C ψ h)
rw [zcSeparatedUniversalDifferential_mul]
simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul]
· exact f.cont.comp (continuous_zcSeparatedUniversalDifferential_naturalTopology C ψ)⟩
left_inv delta := by
apply Subtype.ext
funext g
exact
zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_universal
C ψ hdir delta.1 delta.2.1
(hprelift delta.1 delta.2.1 delta.2.2) g
right_inv f := by
letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
apply ContinuousLinearMap.ext
intro m
have hdelta :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ)
(fun g => f (zcSeparatedUniversalDifferential C ψ g)) := by
intro g h
change f (zcSeparatedUniversalDifferential C ψ (g * h)) =
f (zcSeparatedUniversalDifferential C ψ g) +
zcCompletedGroupAlgebraScalar C ψ g •
f (zcSeparatedUniversalDifferential C ψ h)
rw [zcSeparatedUniversalDifferential_mul]
simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul]
have hcontinuous_delta :
Continuous (fun g => f (zcSeparatedUniversalDifferential C ψ g)) :=
f.cont.comp (continuous_zcSeparatedUniversalDifferential_naturalTopology C ψ)
have hlin :
f.toLinearMap =
zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
C ψ hdir
(fun g => f (zcSeparatedUniversalDifferential C ψ g))
hdelta
(hprelift
(fun g => f (zcSeparatedUniversalDifferential C ψ g))
hdelta hcontinuous_delta) := by
apply zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_unique
C ψ hdir
intro g
rfl
exact congrFun (congrArg DFunLike.coe hlin.symm) mThis is the continuous representation theorem for the separated completed module, parameterized by the topological input that turns a continuous crossed differential into a continuous pre-quotient linear lift.
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 : G → A),
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta →
Continuous delta →
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
A
(zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom)
inferInstance
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta)) :
{delta : G → A //
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta ∧
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)
hpreliftdef 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 : G → A),
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta →
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 : G → A //
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta ∧
Continuous delta} ≃
(letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
ZCSeparatedCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) := by
refine
zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap
C ψ hdir ?_
intro delta hdelta hcont
rcases hfactor delta hdelta hcont with ⟨i, L, hL⟩
exact
continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor
C ψ delta i L hLThis is the continuous representation theorem for the separated completed module when every continuous crossed differential under consideration has a pre-quotient lift that factors through a finite pre-stage. This packages the finite-stage factorization criterion into the universal property, so the public theorem no longer takes the raw hprelift continuity hypothesis.
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 : G → A),
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta →
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 : G → A //
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta ∧
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)
hfactortheorem zcCompletedGroupAlgebra_smul_factor_through_finite_stage
{A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
[TopologicalSpace A] [Fintype 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 • aShow proof
by
classical
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly C) :=
⟨ProCGroups.FiniteGroupClass.finiteOnly C⟩
letI : ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C :=
hForm.containsTrivialQuotients
letI : Nonempty (ProCIntegerIndex C) :=
⟨ProCIntegerIndex.terminal (C := C) inferInstance⟩
letI : Nonempty (CompletedGroupAlgebraIndexInClass H C) :=
⟨_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndexInClass (G := H) C⟩
letI : Nonempty (ZCCompletedGroupAlgebraIndex C H) := inferInstance
letI : Finite (A → A) := Finite.of_fintype (A → A)
let S := zcCompletedGroupAlgebraSystem C H
letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, TopologicalSpace (S.X i) := fun _ => by
dsimp [S, zcCompletedGroupAlgebraSystem]
infer_instance
letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, CompactSpace (S.X i) := fun i => by
dsimp [S, zcCompletedGroupAlgebraSystem]
infer_instance
letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, T2Space (S.X i) := fun i => by
dsimp [S, zcCompletedGroupAlgebraSystem]
infer_instance
letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, TotallyDisconnectedSpace (S.X i) := fun i => by
dsimp [S, zcCompletedGroupAlgebraSystem]
infer_instance
let ρ : ZCCompletedGroupAlgebra C H → A → A := fun r a => r • a
have hρ : Continuous ρ := by
change Continuous (fun r : ZCCompletedGroupAlgebra C H => fun a : A => r • a)
exact continuous_pi fun a => continuous_id.smul continuous_const
rcases S.factors_through_projection_finite
(directed_zcCompletedGroupAlgebraIndex_of_formation C (H := H) hForm)
ρ hρ with
⟨j, act, _hact_continuous, hact⟩
refine ⟨j, act, ?_⟩
intro r a
have h := congrFun (congrFun hact r) a
simpa [ρ, S, zcCompletedGroupAlgebraSystem] using h.symmProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem crossedDifferentialModuleLiftLinear_factors_finite_discrete
{A : Type u} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
[TopologicalSpace A] [Fintype 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.IsProCGroup C G)
(delta : G → A)
(hdelta : IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta)
(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)Show proof
by
classical
rcases zcCompletedGroupAlgebra_smul_factor_through_finite_stage
(C := C) (H := H) (A := A) hForm with
⟨target, act, hact⟩
have hdelta_one : delta 1 = 0 := by
have h := hdelta 1 1
rw [map_one, one_smul] at h
have h' := congrArg (fun z : A => z - delta 1) h
have hzero : 0 = delta 1 := by
simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
simpa using hzero.symm
let W : Set G := {g | delta g = 0}
have hWopen : IsOpen W := by
change IsOpen (delta ⁻¹' ({0} : Set A))
exact (isOpen_discrete _).preimage hcont
have h1W : (1 : G) ∈ W := by
simpa [W] using hdelta_one
rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hWopen h1W with
⟨V0, hV0W⟩
let comapSource : OpenNormalSubgroupInClass C G :=
OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass
(G := G) (H := H) C hC ψc target.2)
let source : OpenNormalSubgroupInClass C G :=
⟨V0.1 ⊓ comapSource.1,
ProCGroups.FiniteGroupClass.Formation.quotient_inf_mem
(C := C) (G := G) hForm V0.1 comapSource.1 V0.2 comapSource.2⟩
let i : ZCCompletedDifferentialModuleIndex C ψc.toMonoidHom :=
{ source := source
target := target
compatible := by
intro g hg
have hgcomap : g ∈ (comapSource.1 : Subgroup G) := hg.2
change ψc.toMonoidHom g ∈
((((OrderDual.ofDual target.2).1 : OpenNormalSubgroup H) : Subgroup H))
simpa [comapSource, completedGroupAlgebraComapIndexInClass] using hgcomap }
have hsource_delta_zero :
∀ g : G, g ∈ (source.1 : Subgroup G) → delta g = 0 := by
intro g hg
exact hV0W hg.1
let deltaBar : zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i → A :=
Quotient.lift delta (by
intro a b hab
have hab_source : a⁻¹ * b ∈ (source.1 : Subgroup G) :=
(QuotientGroup.leftRel_apply).1 hab
have hab_zero : delta (a⁻¹ * b) = 0 :=
hsource_delta_zero (a⁻¹ * b) hab_source
have hprod := hdelta a (a⁻¹ * b)
have hrewrite : a * (a⁻¹ * b) = b := by simp only [mul_inv_cancel_left]
have hb : delta b =
delta a + zcCompletedGroupAlgebraScalar C ψc.toMonoidHom a •
delta (a⁻¹ * b) := by
simpa [hrewrite] using hprod
rw [hab_zero, smul_zero, add_zero] at hb
exact hb.symm)
let coeffMap :
zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i →
zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i →+ A :=
fun q =>
{ toFun := fun a => act a (deltaBar q)
map_zero' := by
have h := hact (0 : ZCCompletedGroupAlgebra C H) (deltaBar q)
simpa using h
map_add' := by
intro a b
rcases zcCompletedGroupAlgebraProjection_surjective C H target a with ⟨ra, hra⟩
rcases zcCompletedGroupAlgebraProjection_surjective C H target b with ⟨rb, hrb⟩
calc
act (a + b) (deltaBar q)
= act (zcCompletedGroupAlgebraProjection C H target (ra + rb)) (deltaBar q) := by
simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedGroupAlgebraProjection_add, hra, hrb]
_ = (ra + rb) • deltaBar q := hact (ra + rb) (deltaBar q)
_ = ra • deltaBar q + rb • deltaBar q := add_smul ra rb (deltaBar q)
_ = act a (deltaBar q) + act b (deltaBar q) := by
rw [← hact ra (deltaBar q), ← hact rb (deltaBar q), hra, hrb] }
let Llin :
CrossedDifferentialPreModule
(zcCompletedDifferentialModuleStageRing C ψc.toMonoidHom i)
(zcCompletedDifferentialModuleStageSource C ψc.toMonoidHom i) →ₗ[ℕ] A :=
Finsupp.lsum ℕ fun q => (coeffMap q).toNatLinearMap
refine ⟨i, (fun y => Llin y), ?_⟩
intro x
refine Finsupp.induction_linear x ?zero ?add ?single
· simp only [crossedDifferentialModuleLiftLinear, map_zero, ContinuousMonoidHom.coe_toMonoidHom,
zcCompletedDifferentialModulePreStageMap]
· intro x y hx hy
simp only [map_add, hx, ContinuousMonoidHom.coe_toMonoidHom, hy]
· intro g a
rw [crossedDifferentialModuleLiftLinear_single]
rw [zcCompletedDifferentialModulePreStageMap_single]
change a • delta g =
Llin
(Finsupp.single (zcCompletedDifferentialModuleStageSourceProj C ψc.toMonoidHom i g)
(zcCompletedGroupAlgebraProjection C H i.target a))
rw [Finsupp.lsum_single]
change a • delta g =
act (zcCompletedGroupAlgebraProjection C H target a)
(deltaBar (zcCompletedDifferentialModuleStageSourceProj C ψc.toMonoidHom i g))
simpa [deltaBar, zcCompletedDifferentialModuleStageSourceProj] using
(hact a (delta g)).symmProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_crossedDifferentialModuleLiftLinear_of_profiniteTarget
{M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
[TopologicalSpace M]
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(ψc : ContinuousMonoidHom G H)
(hG : ProCGroups.ProC.IsProCGroup C G)
(hM : _root_.CompletedGroupAlgebra.IsProfiniteModule
(ZCCompletedGroupAlgebra C H) M)
(delta : G → M)
(hdelta : IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta)
(hcont : Continuous delta) :
@Continuous
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
M
(zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom)
inferInstance
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta)For a profinite target module, continuity of the crossed differential forces continuity of its pre-quotient linear lift for the finite-stage topology.
Show proof
by
classical
letI : IsTopologicalAddGroup M := hM.2.1
letI : ContinuousAdd M := inferInstance
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψc.toMonoidHom
apply _root_.CompletedGroupAlgebra.continuous_of_forall_openSubmodule_quotient_continuous
(R := ZCCompletedGroupAlgebra C H) M hM
intro W hWopen
let hdisc : _root_.CompletedGroupAlgebra.IsDiscreteModule
(ZCCompletedGroupAlgebra C H) (M ⧸ W) :=
_root_.CompletedGroupAlgebra.quotient_openSubmodule_isDiscreteModule
(ZCCompletedGroupAlgebra C H) M hM W hWopen
letI : DiscreteTopology (M ⧸ W) := hdisc.2
letI : ContinuousSMul (ZCCompletedGroupAlgebra C H) (M ⧸ W) := hdisc.1.2.2
letI : Fintype (M ⧸ W) :=
Classical.choice
(_root_.CompletedGroupAlgebra.finite_quotient_of_openSubmodule
(ZCCompletedGroupAlgebra C H) M hM W hWopen)
let deltaQ : G → M ⧸ W := fun g => Submodule.mkQ W (delta g)
have hdeltaQ : IsCrossedDifferential
(zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) deltaQ :=
IsCrossedDifferential.map_linear hdelta (Submodule.mkQ W)
have hqcont : Continuous (Submodule.mkQ W : M → M ⧸ W) := by
change Continuous (Submodule.Quotient.mk (p := W))
exact continuous_quotient_mk'
have hcontQ : Continuous deltaQ := hqcont.comp hcont
rcases crossedDifferentialModuleLiftLinear_factors_finite_discrete
(C := C) (H := H) (A := M ⧸ W) hC hForm ψc hG deltaQ hdeltaQ hcontQ with
⟨i, L, hL⟩
have hEq :
(fun x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G =>
Submodule.mkQ W
(crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) delta x)) =
crossedDifferentialModuleLiftLinear
(R := ZCCompletedGroupAlgebra C H) deltaQ := by
funext x
refine Finsupp.induction_linear x ?zero ?add ?single
· simp only [crossedDifferentialModuleLiftLinear, map_zero, Submodule.mkQ_apply, deltaQ]
· intro x y hx hy
simp only [map_add, hx, hy]
· intro g a
simp only [crossedDifferentialModuleLiftLinear_single, map_smul, Submodule.mkQ_apply, deltaQ]
rw [hEq]
exact
continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor
C ψc.toMonoidHom deltaQ i L hLProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□def zcApsiContinuousCrossedDifferentialEquivContinuousLinearMapOfProfiniteTarget
{M : Type u} [AddCommGroup M] [Module (ZCCompletedGroupAlgebra C H) M]
[TopologicalSpace M]
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(ψc : ContinuousMonoidHom G H)
(hG : ProCGroups.ProC.IsProCGroup C G)
(hM : _root_.CompletedGroupAlgebra.IsProfiniteModule
(ZCCompletedGroupAlgebra C H) M) :
{delta : G → M //
IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψc.toMonoidHom) delta ∧
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 := _root_.CompletedGroupAlgebra.IsProfiniteModule.t1Space hM
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 hdelta hcont =>
continuous_crossedDifferentialModuleLiftLinear_of_profiniteTarget
C hC hForm ψc hG hM delta hdelta hcont)Mathematical profinite-target universal property for \(A_{\psi}(C)\): continuous crossed differentials into a profinite \(\mathbb{Z}_C\llbracket H\rrbracket\)-module are represented by continuous linear maps out of the separated completed Fox module.
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 ψShow proof
by
intro x hx
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
have hxcl :
x ∈ closure
((crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ) :
Submodule (ZCCompletedGroupAlgebra C H)
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) : Set
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)) :=
zcDiffModuleFiniteRelationReductions_mem_closure_relSubmodule
C ψ hdir x hx
simpa [hclosed.closure_eq] using hxclProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcDiffModuleFiniteRelationReductionsReflectRelations_of_relSubmoduleClosed
[Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
(hdir : Directed (· ≤ ·)
(id : ZCCompletedDifferentialModuleIndex C ψ →
ZCCompletedDifferentialModuleIndex C ψ))
(hclosed : zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ) :
zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψA named version of relation-reflection from closedness of the completed relation submodule.
Show proof
zcDiffModuleFiniteRelationReductionsReflectRelations_of_isClosed_relSubmodule
C ψ hdir hclosedProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations :
zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ ↔
zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψThe pre-quotient separation statement is exactly finite relation-reflection.
Show proof
by
constructor
· intro hpre x hx
apply hpre
intro i
exact
(mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule
C ψ i x).2 (hx i)
· intro hreflect x hx
apply hreflect
intro i
exact
(mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule
C ψ i x).1 (hx i)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcDiffModulePreStageProjsSeparate_iff_relSubmodule_eq_iInf_kernel :
zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ ↔
crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =
zcCompletedDifferentialModulePreStageKernelIntersection C ψPre-stage separation is equivalently the claim that the crossed-differential relation submodule is exactly the intersection of all finite-stage pre-kernels.
Show proof
by
constructor
· intro hpre
apply le_antisymm
· intro x hx
rw [zcCompletedDifferentialModulePreStageKernelIntersection, Submodule.mem_iInf]
intro i
exact
crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel
(C := C) (ψ := ψ) i hx
· intro x hx
apply hpre
intro i
have hxi : x ∈ zcCompletedDifferentialModulePreStageKernel C ψ i := by
exact
(Submodule.mem_iInf
(p := fun i : ZCCompletedDifferentialModuleIndex C ψ =>
zcCompletedDifferentialModulePreStageKernel C ψ i)).1
(by
simpa [zcCompletedDifferentialModulePreStageKernelIntersection] using hx) i
simpa using hxi
· intro hEq x hx
have hxint : x ∈ zcCompletedDifferentialModulePreStageKernelIntersection C ψ := by
rw [zcCompletedDifferentialModulePreStageKernelIntersection, Submodule.mem_iInf]
intro i
simpa using hx i
simpa [hEq] using hxintProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate
(hpre : zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ) :
zcCompletedDifferentialModuleStageProjectionsSeparate C ψPre-quotient finite-stage separation implies separation on the algebraic quotient.
Show proof
by
intro a b hab
have hcoord : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcCompletedDifferentialModuleStageProjection C ψ i a =
zcCompletedDifferentialModuleStageProjection C ψ i b := by
intro i
simpa [zcCompletedDifferentialModuleStageProjectionProduct,
zcCompletedDifferentialModuleStageProjectionAdd] using congrFun hab i
have hzero :
∀ z : ZCCompletedDifferentialModule C ψ,
(∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcCompletedDifferentialModuleStageProjection C ψ i z = 0) → z = 0 := by
intro z
refine Submodule.Quotient.induction_on
(p := crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ))
(C := fun z =>
(∀ i : ZCCompletedDifferentialModuleIndex C ψ,
zcCompletedDifferentialModuleStageProjection C ψ i z = 0) → z = 0)
z ?_
intro x hz
apply (Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ))
(x := x)).2
apply hpre
intro i
have hi := hz i
simpa [zcCompletedDifferentialModuleStageProjection_mkQ] using hi
apply sub_eq_zero.mp
apply hzero
intro i
rw [map_sub, hcoord i, sub_self]Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcDiffModuleStageProjsSeparate_of_relSubmodule_eq_iInf_kernel
(hker :
crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =
zcCompletedDifferentialModulePreStageKernelIntersection C ψ) :
zcCompletedDifferentialModuleStageProjectionsSeparate C ψKernel-intersection form of finite-stage separation on the algebraic quotient.
Show proof
zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate C ψ
((zcDiffModulePreStageProjsSeparate_iff_relSubmodule_eq_iInf_kernel
C ψ).2 hker)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□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 = bShow proof
by
apply hsep
funext i
exact h iProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating
(hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :
@T2Space (ZCCompletedDifferentialModule C ψ)
(zcCompletedDifferentialModuleNaturalTopology C ψ)Show proof
by
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleNaturalTopology C ψ
exact T2Space.of_injective_continuous hsep
(continuous_zcCompletedDifferentialModuleStageProjectionProduct_naturalTopology C ψ)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem t2Space_zcDiffModuleNaturalTopology_of_relSubmodule_eq_iInf_kernel
(hker :
crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =
zcCompletedDifferentialModulePreStageKernelIntersection C ψ) :
@T2Space (ZCCompletedDifferentialModule C ψ)
(zcCompletedDifferentialModuleNaturalTopology C ψ)Show proof
t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating C ψ
(zcDiffModuleStageProjsSeparate_of_relSubmodule_eq_iInf_kernel
C ψ hker)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_of_stageProjsSeparate
(hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :
zcCompletedDifferentialModuleRelationSubmoduleClosed C ψShow proof
by
letI : TopologicalSpace
(CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
zcCompletedDifferentialPreModuleNaturalTopology C ψ
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleNaturalTopology C ψ
letI : T2Space (ZCCompletedDifferentialModule C ψ) :=
t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating C ψ hsep
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 =>
(crossedDifferentialRelationSubmodule
(zcCompletedGroupAlgebraScalar C ψ)).mkQ x) ⁻¹'
({0} : Set (ZCCompletedDifferentialModule C ψ)) := by
ext x
simp only [SetLike.mem_coe, Submodule.mkQ_apply, Set.mem_preimage, Set.mem_singleton_iff,
Submodule.Quotient.mk_eq_zero]
rw [hpreimage]
exact isClosed_singleton.preimage
(continuous_zcCompletedDifferentialModule_mkQ_naturalTopology C ψ)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcDiffModuleRelSubmoduleClosed_of_finiteRelationReductionsReflectRelations
(hreflect :
zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ) :
zcCompletedDifferentialModuleRelationSubmoduleClosed C ψFinite relation reflection implies closedness of the algebraic crossed-differential relation submodule for the finite-stage pre-module topology.
Show proof
zcCompletedDifferentialModuleRelationSubmoduleClosed_of_stageProjsSeparate C ψ
(zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate C ψ
((zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations
C ψ).2 hreflect))Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcDiffModuleFiniteRelationReductionsReflectRelations_iff_relSubmodule_eq_iInf_kernel :
zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations C ψ ↔
crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =
zcCompletedDifferentialModulePreStageKernelIntersection C ψKernel-intersection formulation of finite relation reflection.
Show proof
(zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations
C ψ).symm.trans
(zcDiffModulePreStageProjsSeparate_iff_relSubmodule_eq_iInf_kernel
C ψ)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
[Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
(hdir : Directed (· ≤ ·)
(id : ZCCompletedDifferentialModuleIndex C ψ →
ZCCompletedDifferentialModuleIndex C ψ)) :
zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ ↔
zcCompletedDifferentialModuleStageProjectionsSeparate C ψShow proof
by
constructor
· intro hclosed
exact
zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate C ψ
((zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations
C ψ).2
(zcDiffModuleFiniteRelationReductionsReflectRelations_of_relSubmoduleClosed
C ψ hdir hclosed))
· intro hsep
exact zcCompletedDifferentialModuleRelationSubmoduleClosed_of_stageProjsSeparate C ψ hsepProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_iff_t2_naturalTopology
[Nonempty (ZCCompletedDifferentialModuleIndex C ψ)]
(hdir : Directed (· ≤ ·)
(id : ZCCompletedDifferentialModuleIndex C ψ →
ZCCompletedDifferentialModuleIndex C ψ)) :
zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ ↔
@T2Space (ZCCompletedDifferentialModule C ψ)
(zcCompletedDifferentialModuleNaturalTopology C ψ)In the directed finite-stage situation, closedness of the defining relation submodule is equivalent to Hausdorffness of the finite-stage natural topology on the algebraic quotient. This is the mathematical version of the paper-level principle that the source completion/closure has been reflected correctly into the closed quotient exactly when the finite-stage topology on the algebraic universal module is separated.
Show proof
by
constructor
· intro hclosed
exact
t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating C ψ
((zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
C ψ hdir).1 hclosed)
· intro hT2
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleNaturalTopology C ψ
letI : T2Space (ZCCompletedDifferentialModule C ψ) := hT2
exact
zcCompletedDifferentialModuleRelationSubmoduleClosed_of_t1_naturalTopology
C ψ (by infer_instance)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_add_zcCompletedDifferentialModuleNaturalTopology :
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ)Addition is continuous for the finite-stage completed topology.
Show proof
zcCompletedDifferentialModuleNaturalTopology C ψ
Continuous (fun p : ZCCompletedDifferentialModule C ψ ×
ZCCompletedDifferentialModule C ψ => p.1 + p.2) := by
letI : 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))Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_neg_zcCompletedDifferentialModuleNaturalTopology :
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ)Negation is continuous for the finite-stage completed topology.
Show proof
zcCompletedDifferentialModuleNaturalTopology C ψ
Continuous (fun a : ZCCompletedDifferentialModule C ψ => -a) := by
letI : 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)Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem isTopologicalAddGroup_zcCompletedDifferentialModuleNaturalTopology :
@IsTopologicalAddGroup (ZCCompletedDifferentialModule C ψ)
(zcCompletedDifferentialModuleNaturalTopology C ψ) _The finite-stage completed topology is an additive group topology.
Show proof
by
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleNaturalTopology C ψ
exact
{ continuous_add := by
simpa using continuous_add_zcCompletedDifferentialModuleNaturalTopology C ψ
continuous_neg := by
simpa using continuous_neg_zcCompletedDifferentialModuleNaturalTopology C ψ }Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcCompletedDifferentialModuleStageDifferential
(i : ZCCompletedDifferentialModuleIndex C ψ) :
Continuous (zcCompletedDifferentialModuleStageDifferential C ψ i)The finite-stage differential is continuous as a map out of the source group.
Show proof
by
letI : ContinuousMul G := (inferInstanceAs (IsTopologicalGroup G)).toContinuousMul
letI : DiscreteTopology (zcCompletedDifferentialModuleStageSource C ψ i) :=
ProCGroups.ProC.OpenNormalSubgroup.quotientDiscrete (G := G) i.source.1
have hdiff :
Continuous (fun q : zcCompletedDifferentialModuleStageSource C ψ i =>
universalCrossedDifferential (zcCompletedDifferentialModuleStageScalar C ψ i) q) :=
continuous_of_discreteTopology
simpa [zcCompletedDifferentialModuleStageDifferential,
zcCompletedDifferentialModuleStageSourceProj] using
hdiff.comp
(continuous_quotient_mk' : Continuous (fun g : G =>
QuotientGroup.mk' (i.source.1 : Subgroup G) g))Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcUniversalDifferential_naturalTopology :
@Continuous G (ZCCompletedDifferentialModule C ψ) inferInstance
(zcCompletedDifferentialModuleNaturalTopology C ψ)
(zcUniversalDifferential C ψ)The universal differential is continuous for the finite-stage completed topology on the algebraic quotient.
Show proof
by
rw [continuous_induced_rng]
change Continuous
(fun g : G =>
fun i : ZCCompletedDifferentialModuleIndex C ψ =>
zcCompletedDifferentialModuleStageProjectionAdd C ψ i
(zcUniversalDifferential C ψ g))
refine continuous_pi fun i => ?_
simpa using continuous_zcCompletedDifferentialModuleStageDifferential C ψ iProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem zcCompletedDifferentialModuleUniversalTopology_le_naturalTopology :
zcCompletedDifferentialModuleUniversalTopology C ψ ≤
zcCompletedDifferentialModuleNaturalTopology C ψThe universal final topology on the algebraic quotient is below the finite-stage completed topology.
Show proof
(continuous_zcUniversalDifferential_naturalTopology C ψ).coinduced_leProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap
[Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
(i : ZCCompletedDifferentialModuleIndex C ψ) :
Continuous (zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψ i)Show proof
continuous_of_discreteTopologyProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuous_zcToCompletedGroupAlgebra_naturalTopology
[Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
(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)The algebraic completed boundary is continuous for the finite-stage completed topology.
Show proof
by
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψc.toMonoidHom) :=
zcCompletedDifferentialModuleNaturalTopology C ψc.toMonoidHom
have hval : Continuous (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>
((zcToCompletedGroupAlgebra C ψc.toMonoidHom a : ZCCompletedGroupAlgebra C H) :
(j : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H j)) := by
refine continuous_pi fun j => ?_
let i := zcCompletedDifferentialModuleComapIndex C hC ψc j
have hstage : Continuous (fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>
zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
(zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i a)) :=
(continuous_zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap
C ψc.toMonoidHom i).comp
(continuous_zcCompletedDifferentialModuleStageProjection_naturalTopology
C ψc.toMonoidHom i)
have hcoord :
(fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>
zcCompletedGroupAlgebraProjection C H j
(zcToCompletedGroupAlgebra C ψc.toMonoidHom a)) =
(fun a : ZCCompletedDifferentialModule C ψc.toMonoidHom =>
zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψc.toMonoidHom i
(zcCompletedDifferentialModuleStageProjection C ψc.toMonoidHom i a)) := by
funext a
have h :=
congrArg (fun f =>
f a)
(zcDiffModuleStageBoundaryCompletedLinearMap_comp_stageProj
C ψc.toMonoidHom i)
simpa [LinearMap.comp_apply, i] using h.symm
rw [hcoord]
exact hstage
simpa only [Subtype.eta] using
(Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C H) hval
(fun a => (zcToCompletedGroupAlgebra C ψc.toMonoidHom a).property))Proof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□theorem continuousSMul_zcCompletedDifferentialModuleNaturalTopology
[Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] :
@ContinuousSMul (ZCCompletedGroupAlgebra C H)
(ZCCompletedDifferentialModule C ψ)
inferInstance inferInstance (zcCompletedDifferentialModuleNaturalTopology C ψ)Scalar multiplication by \(\mathbb{Z}_C\llbracket H\rrbracket\) is continuous for the finite-stage completed topology.
Show proof
by
letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
zcCompletedDifferentialModuleNaturalTopology C ψ
refine ⟨?_⟩
rw [continuous_induced_rng]
change Continuous
(fun p : ZCCompletedGroupAlgebra C H × ZCCompletedDifferentialModule C ψ =>
fun i : ZCCompletedDifferentialModuleIndex C ψ =>
zcCompletedDifferentialModuleStageProjectionAdd C ψ i (p.1 • p.2))
refine continuous_pi fun i => ?_
letI : TopologicalSpace (zcCompletedDifferentialModuleStageRing C ψ i) := inferInstance
letI : DiscreteTopology (zcCompletedDifferentialModuleStageRing C ψ i) := inferInstance
have hstageAction :
Continuous (fun p : zcCompletedDifferentialModuleStageRing C ψ i ×
ZCCompletedDifferentialModuleStage C ψ i => p.1 • p.2) :=
continuous_of_discreteTopology
have hcoeff :
Continuous (fun a : ZCCompletedGroupAlgebra C H =>
zcCompletedGroupAlgebraProjectionRingHom C H i.target a) :=
continuous_zcCompletedGroupAlgebraProjectionRingHom (C := C) (G := H) i.target
have hmodule :
Continuous (fun a : ZCCompletedDifferentialModule C ψ =>
zcCompletedDifferentialModuleStageProjectionAdd C ψ i a) :=
continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology C ψ i
have hcoord :
Continuous (fun p : ZCCompletedGroupAlgebra C H ×
ZCCompletedDifferentialModule C ψ =>
zcCompletedGroupAlgebraProjectionRingHom C H i.target p.1 •
zcCompletedDifferentialModuleStageProjectionAdd C ψ i p.2) :=
hstageAction.comp (hcoeff.comp continuous_fst |>.prodMk (hmodule.comp continuous_snd))
simpa [zcCompletedDifferentialModuleStageProjectionAdd_apply,
zcCompletedDifferentialModuleStage_completed_smul] using hcoordProof. Work with the finite-stage topology on the completed pre-module and its separated quotient. The topology is defined by the family of finite-stage projections, so continuity, Hausdorffness, closure, and quotient statements are tested after composing with those projections. The crossed-differential relation submodule is handled by its finite-stage closed denominator, and maps descend precisely when they kill that denominator.
□