ProCGroups.FoxDifferential.Completed.Continuous.Universal.System

5 Theorems | 3 Definitions | 1 Abbreviation | 2 Instances

The principal declarations in this module are:

zcCompletedDifferentialModuleStageSystem The inverse system of finite source, target, and coefficient stages of \(A_{\psi}(C)\). - zcCompletedDifferentialPreModuleStageSystem The inverse system of finite pre-modules before quotienting by crossed-differential relations. - zcCompletedDifferentialModuleStageSystem_map_apply The system map on completed differential modules is evaluated coordinatewise at each finite coefficient stage. - zcCompletedDifferentialModuleStageSystem_projection_compatible Inverse-limit projections of the finite \(A_{\psi}(C)\) stage system are compatible with transition maps.

imports

Imported by

Definition FoxDifferential.zcCompletedDifferentialModuleStageSystem

def zcCompletedDifferentialModuleStageSystem :
    InverseSystem (I := ZCCompletedDifferentialModuleIndex C ψ) where
  X := fun i => ZCCompletedDifferentialModuleStage C ψ i
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij => zcCompletedDifferentialModuleStageTransition C ψ hij
  continuous_map := by
    intro i j hij
    letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := ⊥
    letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ j) := ⊥
    letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ j) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (zcCompletedDifferentialModuleStageTransition_id C ψ i)) x
  map_comp := by
    intro i j k hij hjk
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (zcCompletedDifferentialModuleStageTransition_comp C ψ hij hjk)) x

The inverse system of finite source, target, and coefficient stages of \(A_{\psi}(C)\).

Instance FoxDifferential.instAddCommGroupZCCompletedDifferentialModuleStageSystemStage

instance instAddCommGroupZCCompletedDifferentialModuleStageSystemStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    AddCommGroup ((zcCompletedDifferentialModuleStageSystem C ψ).X i) := by
  dsimp [zcCompletedDifferentialModuleStageSystem]
  infer_instance

Addition in the finite-stage completed differential-module system is defined coordinatewise.

Instance FoxDifferential.instIsAddGroupSystemZCCompletedDifferentialModuleStageSystem

instance instIsAddGroupSystemZCCompletedDifferentialModuleStageSystem :
    IsAddGroupSystem (zcCompletedDifferentialModuleStageSystem C ψ) where
  map_zero := by
    intro i j hij
    exact (zcCompletedDifferentialModuleStageTransition C ψ hij).map_zero
  map_add := by
    intro i j hij x y
    exact (zcCompletedDifferentialModuleStageTransition C ψ hij).map_add x y
  map_neg := by
    intro i j hij x
    exact map_neg (zcCompletedDifferentialModuleStageTransition C ψ hij) x

The inverse system of finite-stage group algebras has addition defined coordinatewise on compatible families.

Theorem FoxDifferential.zcCompletedDifferentialModuleStageSystem_map_apply

omit [IsTopologicalGroup G] in
@[simp]
theorem zcCompletedDifferentialModuleStageSystem_map_apply
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
    (x : ZCCompletedDifferentialModuleStage C ψ j) :
    (zcCompletedDifferentialModuleStageSystem C ψ).map hij x =
      zcCompletedDifferentialModuleStageTransition C ψ hij x

The system map on completed differential modules is evaluated coordinatewise at each finite coefficient stage.

Show Lean proof

Theorem FoxDifferential.zcCompletedDifferentialModuleStageSystem_projection_compatible

omit [IsTopologicalGroup G] in
@[simp]
theorem zcCompletedDifferentialModuleStageSystem_projection_compatible
    (x : (zcCompletedDifferentialModuleStageSystem C ψ).inverseLimit)
    (i j : ZCCompletedDifferentialModuleIndex C ψ) (hij : i ≤ j) :
    zcCompletedDifferentialModuleStageTransition C ψ hij
        ((zcCompletedDifferentialModuleStageSystem C ψ).projection j x) =
      (zcCompletedDifferentialModuleStageSystem C ψ).projection i x

Inverse-limit projections of the finite \(A_{\psi}(C)\) stage system are compatible with transition maps.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialPreModuleStageSystem

def zcCompletedDifferentialPreModuleStageSystem :
    InverseSystem (I := ZCCompletedDifferentialModuleIndex C ψ) where
  X := fun i =>
    CrossedDifferentialPreModule
      (zcCompletedDifferentialModuleStageRing C ψ i)
      (zcCompletedDifferentialModuleStageSource C ψ i)
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij => zcCompletedDifferentialModulePreStageTransition C ψ hij
  continuous_map := by
    intro i j hij
    letI : TopologicalSpace
        (CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψ i)
          (zcCompletedDifferentialModuleStageSource C ψ i)) := ⊥
    letI : TopologicalSpace
        (CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψ j)
          (zcCompletedDifferentialModuleStageSource C ψ j)) := ⊥
    letI : DiscreteTopology
        (CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψ j)
          (zcCompletedDifferentialModuleStageSource C ψ j)) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (zcCompletedDifferentialModulePreStageTransition_id C ψ i)) x
  map_comp := by
    intro i j k hij hjk
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (zcCompletedDifferentialModulePreStageTransition_comp C ψ hij hjk)) x

The inverse system of finite pre-modules before quotienting by crossed-differential relations.

Abbreviation FoxDifferential.ZCCompletedDifferentialPreModuleStageFamily

abbrev ZCCompletedDifferentialPreModuleStageFamily : Type u :=
  (zcCompletedDifferentialPreModuleStageSystem C ψ).inverseLimit

Compatible inverse-limit families of finite pre-stage elements.

Theorem FoxDifferential.zcCompletedDifferentialPreModuleStageSystem_map_apply

omit [IsTopologicalGroup G] in
@[simp]
theorem zcCompletedDifferentialPreModuleStageSystem_map_apply
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
    (x : CrossedDifferentialPreModule
      (zcCompletedDifferentialModuleStageRing C ψ j)
      (zcCompletedDifferentialModuleStageSource C ψ j)) :
    (zcCompletedDifferentialPreModuleStageSystem C ψ).map hij x =
      zcCompletedDifferentialModulePreStageTransition C ψ hij x

The finite pre-module inverse-system map evaluates as the explicit pre-stage transition.

Show Lean proof

Theorem FoxDifferential.zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap

omit [IsTopologicalGroup G] in
theorem zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap :
    (zcCompletedDifferentialPreModuleStageSystem C ψ).CompatibleMaps
      (fun i : ZCCompletedDifferentialModuleIndex C ψ =>
        zcCompletedDifferentialModulePreStageMap C ψ i)

The explicit finite pre-stage reductions of a completed pre-module element are compatible with finite transitions.

Show Lean proof

Definition FoxDifferential.zcCompletedDifferentialPreModuleStageFamilyMap

def zcCompletedDifferentialPreModuleStageFamilyMap :
    CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G →
      ZCCompletedDifferentialPreModuleStageFamily C ψ :=
  (zcCompletedDifferentialPreModuleStageSystem C ψ).inverseLimitLift
    (fun i : ZCCompletedDifferentialModuleIndex C ψ =>
      zcCompletedDifferentialModulePreStageMap C ψ i)
    (zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap C ψ)

The finite-stage family map sends a completed pre-module element to its compatible family of finite source, target, and coefficient stages.

Theorem FoxDifferential.zcCompletedDifferentialPreModuleStageFamilyMap_projection

omit [IsTopologicalGroup G] in
@[simp]
theorem zcCompletedDifferentialPreModuleStageFamilyMap_projection
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
    (zcCompletedDifferentialPreModuleStageSystem C ψ).projection i
        (zcCompletedDifferentialPreModuleStageFamilyMap C ψ x) =
      zcCompletedDifferentialModulePreStageMap C ψ i x

Projecting the finite-stage pre-module family map at a stage recovers the explicit pre-stage map at that stage.

Show Lean proof

ProCGroups.FoxDifferential.Completed.Continuous.Universal.System

Declarations