ProCGroups.FoxDifferential.Completed.Continuous.Universal.NaturalTopology

76 Theorems | 23 Definitions | 3 Abbreviations

The principal declarations in this module are:

zcCompletedDifferentialModuleStageProjectionAdd The additive finite-stage projection from the algebraic completed differential module. - zcCompletedDifferentialModuleStageProjectionProduct The product of all finite source/target/coefficient projections of the algebraic quotient. - zcCompletedDifferentialModuleStageProjectionAdd_apply The additive stage projection has the same underlying function as the unbundled completed differential-module stage projection. - zcCompletedDifferentialModuleStageProjectionAdd_universal The additive finite-stage projection sends the universal differential to the corresponding finite-stage differential.

import

ProCGroups.FoxDifferential.Completed.Continuous.Universal.System

Imported by

Definition FoxDifferential.zcCompletedDifferentialModuleStageProjectionAdd

def zcCompletedDifferentialModuleStageProjectionAdd
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    ZCCompletedDifferentialModule C ψ →+
      ZCCompletedDifferentialModuleStage C ψ i :=
  (zcCompletedDifferentialModuleStageProjection C ψ i).toAddMonoidHom

The additive finite-stage projection from the algebraic completed differential module.

Theorem FoxDifferential.zcCompletedDifferentialModuleStageProjectionAdd_apply

omit [IsTopologicalGroup G] in
@[simp]
theorem zcCompletedDifferentialModuleStageProjectionAdd_apply
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (a : ZCCompletedDifferentialModule C ψ) :
    zcCompletedDifferentialModuleStageProjectionAdd C ψ i a =
      zcCompletedDifferentialModuleStageProjection C ψ i a

The additive stage projection has the same underlying function as the unbundled completed differential-module stage projection.

Show Lean proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageProjectionAdd_universal

omit [IsTopologicalGroup G] in
@[simp]
theorem zcCompletedDifferentialModuleStageProjectionAdd_universal
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcCompletedDifferentialModuleStageProjectionAdd C ψ i
        (zcUniversalDifferential C ψ g) =
      zcCompletedDifferentialModuleStageDifferential C ψ i g

The additive finite-stage projection sends the universal differential to the corresponding finite-stage differential.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleStageProjectionProduct

def zcCompletedDifferentialModuleStageProjectionProduct :
    ZCCompletedDifferentialModule C ψ →
      ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        ZCCompletedDifferentialModuleStage C ψ i :=
  fun a i => zcCompletedDifferentialModuleStageProjectionAdd C ψ i a

The product of all finite source/target/coefficient projections of the algebraic quotient.

Theorem FoxDifferential.zcCompletedDifferentialModuleStageProjectionProduct_apply

omit [IsTopologicalGroup G] in
@[simp]
theorem zcCompletedDifferentialModuleStageProjectionProduct_apply
    (a : ZCCompletedDifferentialModule C ψ)
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcCompletedDifferentialModuleStageProjectionProduct C ψ a i =
      zcCompletedDifferentialModuleStageProjectionAdd C ψ i a

The product of additive stage projections evaluates at i as the additive projection at i.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleNaturalTopology

@[implicit_reducible]
def zcCompletedDifferentialModuleNaturalTopology :
    TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
  TopologicalSpace.induced
    (zcCompletedDifferentialModuleStageProjectionProduct C ψ) inferInstance

The finite-stage completed topology on the algebraic completed differential module. This topology is named deliberately: it is not installed as a global instance.

Theorem FoxDifferential.continuous_zcCompletedDifferentialModuleStageProjectionProduct_naturalTopology

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology

omit [IsTopologicalGroup G] in
theorem continuous_zcCompletedDifferentialModuleStageProjectionAdd_naturalTopology
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    @Continuous (ZCCompletedDifferentialModule C ψ)
      (ZCCompletedDifferentialModuleStage C ψ i)
      (zcCompletedDifferentialModuleNaturalTopology C ψ) inferInstance
      (zcCompletedDifferentialModuleStageProjectionAdd C ψ i)

Each finite-stage projection is continuous for the finite-stage completed topology.

Show Lean proof

Theorem FoxDifferential.continuous_zcCompletedDifferentialModuleStageProjection_naturalTopology

omit [IsTopologicalGroup G] in
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 Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleStageProjectionsSeparate

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.

Definition FoxDifferential.zcCompletedDifferentialModulePreStageProjectionsSeparate

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 ψ)

Pre-quotient finite-stage separation says that elements killed by every finite-stage crossed-differential projection are exactly the defining crossed-differential relations.

Definition FoxDifferential.zcCompletedDifferentialModulePreStageKernel

def zcCompletedDifferentialModulePreStageKernel
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    Submodule (ZCCompletedGroupAlgebra C H)
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
  LinearMap.ker
    (crossedDifferentialModuleLiftLinear
      (R := ZCCompletedGroupAlgebra C H)
      (zcCompletedDifferentialModuleStageDifferential C ψ i))

The kernel on the pre-module cut out by one finite source/target/coefficient stage.

Theorem FoxDifferential.mem_zcCompletedDifferentialModulePreStageKernel_iff

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

Membership in a completed differential-module pre-stage kernel is equivalent to vanishing of the corresponding finite-stage coordinate.

Show Lean proof

Theorem FoxDifferential.mem_zcDiffModulePreStageKernel_iff_preStageMap_mem_relSubmodule

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

Membership in a finite pre-stage kernel is equivalently membership of the explicit source-and-coefficient reduction in the finite crossed-differential relation submodule.

Show Lean proof

Theorem FoxDifferential.crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel

omit [IsTopologicalGroup G] in
theorem crossedDiffRelSubmodule_le_zcDiffModulePreStageKernel
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) ≤
      zcCompletedDifferentialModulePreStageKernel C ψ i

Every defining crossed-differential relation is killed by every finite stage.

Show Lean proof

Theorem FoxDifferential.zcCompletedDifferentialModulePreStageMap_mem_relationSubmodule_of_mem

omit [IsTopologicalGroup G] in
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)

The explicit finite pre-stage map sends completed crossed-differential relations to finite crossed-differential relations.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModulePreStageKernelIntersection

def zcCompletedDifferentialModulePreStageKernelIntersection :
    Submodule (ZCCompletedGroupAlgebra C H)
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
  ⨅ i : ZCCompletedDifferentialModuleIndex C ψ,
    zcCompletedDifferentialModulePreStageKernel C ψ i

The common finite-stage kernel on the pre-module.

Theorem FoxDifferential.mem_zcCompletedDifferentialModulePreStageKernelIntersection_iff

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

Membership in the intersection of completed differential-module pre-stage kernels is equivalent to vanishing of the corresponding finite-stage coordinate.

Show Lean proof

Abbreviation FoxDifferential.zcCompletedDifferentialRelationFiniteClosedSubmodule

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.

Abbreviation FoxDifferential.ZCSeparatedCompletedDifferentialModule

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.

Abbreviation FoxDifferential.ZCApsi

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 FoxDifferential.crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule

omit [IsTopologicalGroup G] in
theorem crossedDifferentialRelationSubmodule_le_finiteClosedSubmodule :
    crossedDifferentialRelationSubmodule
      (zcCompletedGroupAlgebraScalar C ψ) ≤
    zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ

Algebraic crossed-differential relations vanish in the finite-stage separated quotient.

Show Lean proof

Definition FoxDifferential.zcSeparatedUniversalDifferential

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

The universal crossed differential into the separated completed quotient.

Theorem FoxDifferential.zcSeparatedUniversalDifferential_commutator_right_kernel

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

Commutator formula for the separated universal differential when the right factor lies in the kernel of the target homomorphism.

Show Lean proof

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModule_mk_eq_zero_iff

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

A representative is zero in the separated quotient exactly when all finite reductions are finite crossed-differential relations.

Show Lean proof

Definition FoxDifferential.zcSeparatedCompletedDifferentialModuleStageProjectionAdd

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 := C) (ψ := ψ) (x :=
            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 FoxDifferential.zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ

omit [IsTopologicalGroup G] in
@[simp]
theorem zcSeparatedCompletedDifferentialModuleStageProjectionAdd_mkQ
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
    zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i
        ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x) =
      crossedDifferentialModuleLiftLinear
        (R := ZCCompletedGroupAlgebra C H)
        (zcCompletedDifferentialModuleStageDifferential C ψ i) x

The separated finite-stage projection of a quotient representative is the finite-stage crossed-differential lift of that representative.

Show Lean proof

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModuleStageProjectionAdd_universal

omit [IsTopologicalGroup G] in
@[simp]
theorem zcSeparatedCompletedDifferentialModuleStageProjectionAdd_universal
    (i : ZCCompletedDifferentialModuleIndex C ψ) (g : G) :
    zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i
        (zcSeparatedUniversalDifferential C ψ g) =
      zcCompletedDifferentialModuleStageDifferential C ψ i g

The separated finite-stage projection sends the separated universal differential to the corresponding finite-stage differential.

Show Lean proof

Definition FoxDifferential.zcSeparatedCompletedDifferentialModuleStageProjectionProduct

def zcSeparatedCompletedDifferentialModuleStageProjectionProduct :
    ZCSeparatedCompletedDifferentialModule C ψ →
      ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        ZCCompletedDifferentialModuleStage C ψ i :=
  fun a i => zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a

The product of all finite-stage projections from the separated completed quotient.

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModuleStageProjectionProduct_apply

omit [IsTopologicalGroup G] in
@[simp]
theorem zcSeparatedCompletedDifferentialModuleStageProjectionProduct_apply
    (a : ZCSeparatedCompletedDifferentialModule C ψ)
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ a i =
      zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a

The product projection from the separated completed differential module evaluates at i as its additive stage projection.

Show Lean proof

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModuleStageProjectionsSeparate

omit [IsTopologicalGroup G] in
theorem zcSeparatedCompletedDifferentialModuleStageProjectionsSeparate :
    ∀ x : ZCSeparatedCompletedDifferentialModule C ψ,
      (∀ i : ZCCompletedDifferentialModuleIndex C ψ,
        zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i x = 0) →
      x = 0

The finite-stage projections separate points of the separated completed quotient.

Show Lean proof

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModuleStageProjectionProduct_injective

omit [IsTopologicalGroup G] in
theorem zcSeparatedCompletedDifferentialModuleStageProjectionProduct_injective :
    Function.Injective
      (zcSeparatedCompletedDifferentialModuleStageProjectionProduct C ψ)

The finite-stage projection product is injective on the separated completed quotient.

Show Lean proof

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModuleStageProjection_ext

omit [IsTopologicalGroup G] in
theorem zcSeparatedCompletedDifferentialModuleStageProjection_ext
    {a b : ZCSeparatedCompletedDifferentialModule C ψ}
    (h : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
      zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i a =
        zcSeparatedCompletedDifferentialModuleStageProjectionAdd C ψ i b) :
    a = b

Extensionality for the separated completed quotient by finite-stage projections.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleToSeparated

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 FoxDifferential.zcCompletedDifferentialModuleToSeparated_universal

omit [IsTopologicalGroup G] in
@[simp]
theorem zcCompletedDifferentialModuleToSeparated_universal (g : G) :
    zcCompletedDifferentialModuleToSeparated C ψ
      (zcUniversalDifferential C ψ g) =
    zcSeparatedUniversalDifferential C ψ g

The quotient map to the separated completed module sends the universal differential to the separated universal differential.

Show Lean proof

Theorem FoxDifferential.crossedDifferentialBoundaryLiftLinear_kills_finiteClosedSubmodule

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

The 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 Lean proof

Definition FoxDifferential.zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra

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 FoxDifferential.zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_universal

omit [IsTopologicalGroup G] in
@[simp]
theorem zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_universal
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (ψc : ContinuousMonoidHom G H)
    (g : G) :
    zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra C hC ψc
        (zcSeparatedUniversalDifferential C ψc.toMonoidHom g) =
      zcCompletedGroupAlgebraBoundary C ψc.toMonoidHom g

The universal completed Fox map from the separated completed differential module to the completed group algebra is characterized by finite-stage Fox coordinate formulas.

Show Lean proof

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModuleToCompletedGroupAlgebra_comp_toSeparated

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

The completed Fox map to the completed group algebra agrees with the separated quotient map on finite-stage coordinates.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations

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.

Definition FoxDifferential.zcCompletedDifferentialPreModuleNaturalTopology

@[implicit_reducible]
def zcCompletedDifferentialPreModuleNaturalTopology :
    TopologicalSpace (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
  TopologicalSpace.induced
    (zcCompletedDifferentialPreModuleStageFamilyMap C ψ) inferInstance

The finite-stage topology on the completed pre-module, before quotienting by the crossed-differential relations.

Theorem FoxDifferential.continuous_zcCompletedDifferentialModulePreStageMap_naturalTopology

omit [IsTopologicalGroup G] in
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)

Each finite pre-stage reduction is continuous for the finite-stage topology on the completed pre-module.

Show Lean proof

Definition FoxDifferential.zcSeparatedCompletedDifferentialModuleNaturalTopology

@[implicit_reducible]
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 FoxDifferential.continuous_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology

omit [IsTopologicalGroup G] in
theorem continuous_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology :
    @Continuous
      (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
      (ZCSeparatedCompletedDifferentialModule C ψ)
      (zcCompletedDifferentialPreModuleNaturalTopology C ψ)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
      (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

The quotient map to the separated completed module is continuous for the finite-stage pre-module topology and the separated quotient topology.

Show Lean proof

Theorem FoxDifferential.isQuotientMap_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology

omit [IsTopologicalGroup G] in
theorem isQuotientMap_zcSeparatedCompletedDifferentialModule_mkQ_naturalTopology :
    letI : TopologicalSpace
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
      zcCompletedDifferentialPreModuleNaturalTopology C ψ
    letI : TopologicalSpace (ZCSeparatedCompletedDifferentialModule C ψ) :=
      zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ
    Topology.IsQuotientMap (zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ

The quotient map defining the separated completed module is a quotient map for the finite-stage pre-module topology.

Show Lean proof

Theorem FoxDifferential.continuous_zcSeparatedCompletedDifferentialModule_iff_comp_mkQ

omit [IsTopologicalGroup G] in
theorem continuous_zcSeparatedCompletedDifferentialModule_iff_comp_mkQ
    {C : ProCGroups.FiniteGroupClass.{u}} {ψ : G →* H}
    {A : Type u} [TopologicalSpace A]
    {f : ZCSeparatedCompletedDifferentialModule C ψ → A} :
    @Continuous
        (ZCSeparatedCompletedDifferentialModule C ψ) A
        (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ) inferInstance f ↔
      @Continuous
        (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) A
        (zcCompletedDifferentialPreModuleNaturalTopology C ψ) inferInstance
        (fun x => f ((zcCompletedDifferentialRelationFiniteClosedSubmodule C ψ).mkQ x))

Continuity out of the separated completed module can be tested after precomposing with the defining quotient map.

Show Lean proof

Theorem FoxDifferential.continuous_zcSepDiffModuleStageProjAdd_naturalTopology

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.continuous_zcSepDiffModuleStageProjProduct_naturalTopology

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.t2Space_zcSeparatedCompletedDifferentialModuleNaturalTopology

omit [IsTopologicalGroup G] in
theorem t2Space_zcSeparatedCompletedDifferentialModuleNaturalTopology :
    @T2Space
      (ZCSeparatedCompletedDifferentialModule C ψ)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)

The separated completed quotient is Hausdorff for the separated finite-stage quotient topology.

Show Lean proof

Theorem FoxDifferential.zcSepDiffModuleNaturalTopology_eq_induced_stageProjProduct

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

In the directed finite-stage situation, the separated quotient topology is exactly the topology induced by all finite-stage separated projections.

Show Lean proof

Theorem FoxDifferential.continuous_zcCompletedDifferentialPreModule_single_one_naturalTopology

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))

The pre-module generator map g \(\mapsto\) dg is continuous for the finite-stage pre-module topology.

Show Lean proof

Theorem FoxDifferential.continuous_zcSeparatedUniversalDifferential_naturalTopology

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 Lean proof

Theorem FoxDifferential.continuous_crossedDifferentialModuleLiftLinear_of_preStageMap_factor

omit [IsTopologicalGroup G] in
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)

A pre-quotient linear lift is continuous for the finite-stage pre-module topology when it factors through one finite pre-stage reduction. This is the standard way to discharge the hprelift input in applications where the target data is already finite-stage.

Show Lean proof

Theorem FoxDifferential.continuous_crossedDifferentialModuleLiftLinear_stageDifferential

omit [IsTopologicalGroup G] in
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))

The canonical lift to a finite differential-module stage is continuous for the finite-stage pre-module topology.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialModuleRelationSubmoduleClosed

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 FoxDifferential.zcDiffModuleRelSubmoduleClosed_of_inj_continuous_comp_mkQ

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.continuous_zcCompletedDifferentialModule_mkQ_naturalTopology

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

The quotient map from the completed pre-module to the algebraic quotient is continuous for the finite-stage topologies.

Show Lean proof

Theorem FoxDifferential.zcCompletedDifferentialModuleRelationSubmoduleClosed_of_t1_naturalTopology

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.zcDiffModuleRelSubmoduleClosed_of_inj_continuous_naturalTopology

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.zcDiffModuleFiniteRelationReductions_mem_closure_relSubmodule

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.isClosed_zcCompletedDifferentialModulePreStageKernel_naturalTopology

omit [IsTopologicalGroup G] in
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))

Each finite-stage pre-kernel is closed for the finite-stage topology on the completed pre-module.

Show Lean proof

Theorem FoxDifferential.isClosed_zcCompletedDifferentialRelationFiniteClosedSubmodule_naturalTopology

omit [IsTopologicalGroup G] in
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))

The finite-stage closed relation denominator is closed for the finite-stage pre-module topology.

Show Lean proof

Theorem FoxDifferential.isClosed_zero_zcSeparatedCompletedDifferentialModuleNaturalTopology

omit [IsTopologicalGroup G] in
theorem isClosed_zero_zcSeparatedCompletedDifferentialModuleNaturalTopology :
    @IsClosed (ZCSeparatedCompletedDifferentialModule C ψ)
      (zcSeparatedCompletedDifferentialModuleNaturalTopology C ψ)
      ({0} : Set (ZCSeparatedCompletedDifferentialModule C ψ))

The zero class is closed in the separated completed differential module for the finite-stage quotient topology.

Show Lean proof

Theorem FoxDifferential.closure_crossedDifferentialRelationSubmodule_eq_finiteClosedSubmodule

omit [IsTopologicalGroup G] in
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))

The finite-stage closed relation denominator is exactly the closure of the algebraic crossed-differential relation submodule for the finite-stage pre-module topology.

Show Lean proof

Theorem FoxDifferential.crossedDifferentialModuleLiftLinear_kills_finiteClosedSubmodule_of_continuous

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

A 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 Lean proof

Definition FoxDifferential.zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift

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

The separated universal lift induced by a crossed differential whose pre-quotient lift is continuous for the finite-stage topology.

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_universal

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

The separated lift of a continuous crossed-differential prelift sends the separated universal differential of \(g\) to \(\delta(g)\).

Show Lean proof

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModuleHom_ext

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

Linear maps out of the separated completed differential module are equal when they agree on all separated universal differentials.

Show Lean proof

Theorem FoxDifferential.zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_unique

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

The separated lift of a continuous crossed differential is unique among linear maps with the prescribed values on separated universal differentials.

Show Lean proof

Definition FoxDifferential.zcSeparatedCompletedDifferentialModuleLiftContinuousLinearMapOfContinuousPrelift

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

The separated universal lift is bundled as a continuous linear map for the separated quotient topology.

Theorem FoxDifferential.zcSepDiffModuleLiftContinuousLinearMapOfContinuousPrelift_apply

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

The separated completed differential-module lift is evaluated after projection to the relevant finite-stage separated quotient.

Show Lean proof

Definition FoxDifferential.zcSeparatedCompletedContinuousCrossedDifferentialEquivContinuousLinearMap

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

This 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.

Definition FoxDifferential.zcSepContCrossedDiffEquivCLM

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

Continuous representation theorem with the finite-stage index nonemptiness and directedness supplied from a continuous homomorphism and the finite quotient-class hypotheses. The only remaining topological input is the pre-quotient lift continuity.

Definition FoxDifferential.zcSepCompletedContCrossedDiffEquivContinuousLinearMapOfFiniteStageFactorization

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

This 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.

Definition FoxDifferential.zcSepContCrossedDiffEquivCLMOfFiniteStage

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

Continuous representation theorem with finite-stage index data supplied from a continuous homomorphism and raw pre-lift continuity discharged by finite-stage factorization.

Theorem FoxDifferential.zcCompletedGroupAlgebra_smul_factor_through_finite_stage

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

The \(\mathbb{Z}_C\llbracket H\rrbracket\)-action on a finite discrete target factors through one finite coefficient-and-H stage.

Show Lean proof

Theorem FoxDifferential.crossedDifferentialModuleLiftLinear_factors_finite_discrete

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

A finite discrete target crossed differential has a pre-quotient lift factoring through one finite source/target/coefficient stage.

Show Lean proof

Theorem FoxDifferential.continuous_crossedDifferentialModuleLiftLinear_of_profiniteTarget

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

For a profinite target module, continuity of the crossed differential forces continuity of its pre-quotient linear lift for the finite-stage topology.

Show Lean proof

Definition FoxDifferential.zcApsiContinuousCrossedDifferentialEquivContinuousLinearMapOfProfiniteTarget

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

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 FoxDifferential.zcDiffModuleFiniteRelationReductionsReflectRelations_of_isClosed_relSubmodule

omit [IsTopologicalGroup G] in
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 ψ

If the completed crossed-differential relation submodule is closed for the finite-stage pre-module topology, then finite relation reductions reflect actual completed relations.

Show Lean proof

Theorem FoxDifferential.zcDiffModuleFiniteRelationReductionsReflectRelations_of_relSubmoduleClosed

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations

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

The pre-quotient separation statement is exactly finite relation-reflection.

Show Lean proof

Theorem FoxDifferential.zcDiffModulePreStageProjsSeparate_iff_relSubmodule_eq_iInf_kernel

omit [IsTopologicalGroup G] in
theorem zcDiffModulePreStageProjsSeparate_iff_relSubmodule_eq_iInf_kernel
    (C : ProCGroups.FiniteGroupClass.{u}) (ψ : G →* H) :
    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 Lean proof

Theorem FoxDifferential.zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate

omit [IsTopologicalGroup G] in
theorem zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate
    (hpre : zcCompletedDifferentialModulePreStageProjectionsSeparate C ψ) :
    zcCompletedDifferentialModuleStageProjectionsSeparate C ψ

Pre-quotient finite-stage separation implies separation on the algebraic quotient.

Show Lean proof

Theorem FoxDifferential.zcDiffModuleStageProjsSeparate_of_relSubmodule_eq_iInf_kernel

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageProjection_ext_of_separating

omit [IsTopologicalGroup G] in
theorem zcCompletedDifferentialModuleStageProjection_ext_of_separating
    (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ)
    {a b : ZCCompletedDifferentialModule C ψ}
    (h : ∀ i : ZCCompletedDifferentialModuleIndex C ψ,
      zcCompletedDifferentialModuleStageProjectionAdd C ψ i a =
        zcCompletedDifferentialModuleStageProjectionAdd C ψ i b) :
    a = b

If the finite-stage projection product is injective, then equality of every finite coordinate implies equality in the genuine universal module.

Show Lean proof

Theorem FoxDifferential.t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating

omit [IsTopologicalGroup G] in
theorem t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating
    (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :
    @T2Space (ZCCompletedDifferentialModule C ψ)
      (zcCompletedDifferentialModuleNaturalTopology C ψ)

The finite-stage completed topology is Hausdorff once the finite-stage projections separate points.

Show Lean proof

Theorem FoxDifferential.t2Space_zcDiffModuleNaturalTopology_of_relSubmodule_eq_iInf_kernel

omit [IsTopologicalGroup G] in
theorem t2Space_zcDiffModuleNaturalTopology_of_relSubmodule_eq_iInf_kernel
    (hker :
      crossedDifferentialRelationSubmodule (zcCompletedGroupAlgebraScalar C ψ) =
        zcCompletedDifferentialModulePreStageKernelIntersection C ψ) :
    @T2Space (ZCCompletedDifferentialModule C ψ)
      (zcCompletedDifferentialModuleNaturalTopology C ψ)

Kernel-intersection form of the Hausdorff property for the finite-stage completed topology.

Show Lean proof

Theorem FoxDifferential.zcCompletedDifferentialModuleRelationSubmoduleClosed_of_stageProjsSeparate

omit [IsTopologicalGroup G] in
theorem zcCompletedDifferentialModuleRelationSubmoduleClosed_of_stageProjsSeparate
    (hsep : zcCompletedDifferentialModuleStageProjectionsSeparate C ψ) :
    zcCompletedDifferentialModuleRelationSubmoduleClosed C ψ

If finite-stage projections separate the algebraic quotient, then the defining relation submodule is closed for the finite-stage topology on the completed pre-module.

Show Lean proof

Theorem FoxDifferential.zcDiffModuleRelSubmoduleClosed_of_finiteRelationReductionsReflectRelations

omit [IsTopologicalGroup G] in
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 Lean proof

Theorem FoxDifferential.zcDiffModuleFiniteRelationReductionsReflectRelations_iff_relSubmodule_eq_iInf_kernel

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

Kernel-intersection formulation of finite relation reflection.

Show Lean proof

Theorem FoxDifferential.zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate

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

In the directed finite-stage situation, closedness of the completed relation submodule is equivalent to finite-stage separation of the algebraic quotient.

Show Lean proof

Theorem FoxDifferential.zcCompletedDifferentialModuleRelationSubmoduleClosed_iff_t2_naturalTopology

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

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 Lean proof

Theorem FoxDifferential.continuous_add_zcCompletedDifferentialModuleNaturalTopology

omit [IsTopologicalGroup G] in
theorem continuous_add_zcCompletedDifferentialModuleNaturalTopology :
    letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
      zcCompletedDifferentialModuleNaturalTopology C ψ
    Continuous (fun p : ZCCompletedDifferentialModule C ψ ×
        ZCCompletedDifferentialModule C ψ => p.1 + p.2)

Addition is continuous for the finite-stage completed topology.

Show Lean proof

Theorem FoxDifferential.continuous_neg_zcCompletedDifferentialModuleNaturalTopology

omit [IsTopologicalGroup G] in
theorem continuous_neg_zcCompletedDifferentialModuleNaturalTopology :
    letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
      zcCompletedDifferentialModuleNaturalTopology C ψ
    Continuous (fun a : ZCCompletedDifferentialModule C ψ => -a)

Negation is continuous for the finite-stage completed topology.

Show Lean proof

Theorem FoxDifferential.isTopologicalAddGroup_zcCompletedDifferentialModuleNaturalTopology

omit [IsTopologicalGroup G] in
theorem isTopologicalAddGroup_zcCompletedDifferentialModuleNaturalTopology :
    @IsTopologicalAddGroup (ZCCompletedDifferentialModule C ψ)
      (zcCompletedDifferentialModuleNaturalTopology C ψ) _

The finite-stage completed topology is an additive group topology.

Show Lean proof

Theorem FoxDifferential.continuous_zcCompletedDifferentialModuleStageDifferential

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 Lean proof

Theorem FoxDifferential.continuous_zcUniversalDifferential_naturalTopology

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 Lean proof

Theorem FoxDifferential.zcUniversalDifferentialFinalTopology_le_naturalTopology

theorem zcUniversalDifferentialFinalTopology_le_naturalTopology :
    zcUniversalDifferentialFinalTopology C ψ ≤
      zcCompletedDifferentialModuleNaturalTopology C ψ

The universal final topology on the algebraic quotient is below the finite-stage completed topology.

Show Lean proof

Theorem FoxDifferential.continuous_zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap

omit [IsTopologicalGroup G] in
theorem continuous_zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    Continuous (zcCompletedDifferentialModuleStageBoundaryCompletedLinearMap C ψ i)

The finite-stage boundary map is continuous for the completed differential-module topology defined by the finite-stage projections.

Show Lean proof

Theorem FoxDifferential.continuous_zcToCompletedGroupAlgebra_naturalTopology

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

The algebraic completed boundary is continuous for the finite-stage completed topology.

Show Lean proof

Theorem FoxDifferential.continuousSMul_zcCompletedDifferentialModuleNaturalTopology

omit [IsTopologicalGroup G] in
theorem continuousSMul_zcCompletedDifferentialModuleNaturalTopology :
    @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 Lean proof

ProCGroups.FoxDifferential.Completed.Continuous.Universal.NaturalTopology

Declarations