System.lean

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
    let : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := ⊥
    let : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ j) := ⊥
    let : 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

instance instAddCommGroupZCCompletedDifferentialModuleStageSystemStage
    (i : ZCCompletedDifferentialModuleIndex C ψ) :
    AddCommGroup ((zcCompletedDifferentialModuleStageSystem C ψ).X i)

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

theorem zcCompletedDifferentialModuleStageSystem_map_apply
    {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
    (x : ZCCompletedDifferentialModuleStage C ψ j) :
    (zcCompletedDifferentialModuleStageSystem C ψ).map hij x =
      zcCompletedDifferentialModuleStageTransition C ψ hij x

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

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
    let : TopologicalSpace
        (CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψ i)
          (zcCompletedDifferentialModuleStageSource C ψ i)) := ⊥
    let : TopologicalSpace
        (CrossedDifferentialPreModule
          (zcCompletedDifferentialModuleStageRing C ψ j)
          (zcCompletedDifferentialModuleStageSource C ψ j)) := ⊥
    let : 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

abbrev ZCCompletedDifferentialPreModuleStageFamily : Type u

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

theorem zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap :
    (zcCompletedDifferentialPreModuleStageSystem C ψ).CompatibleMaps
      (fun i : ZCCompletedDifferentialModuleIndex C ψ =>
        zcCompletedDifferentialModulePreStageMap C ψ i) := by
  intro i j hij
  funext x
  exact zcCompletedDifferentialModulePreStageTransition_preStageMap C ψ hij x

def zcCompletedDifferentialPreModuleStageFamilyMap :
    CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G →
      ZCCompletedDifferentialPreModuleStageFamily C ψ

theorem zcCompletedDifferentialPreModuleStageFamilyMap_projection
    (i : ZCCompletedDifferentialModuleIndex C ψ)
    (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
    (zcCompletedDifferentialPreModuleStageSystem C ψ).projection i
        (zcCompletedDifferentialPreModuleStageFamilyMap C ψ x) =
      zcCompletedDifferentialModulePreStageMap C ψ i x