OAI/Algebra/Finitistic/Ordinary/OrdinaryXAugmentation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.OrdinarySimulation.XResolution.ordinaryXObject line 16

    Source documentation

    The actual ordinary X, represented as a genuine D-bimodule.

    abbrev ordinaryXObject : ModuleCat.{u} ((AlgebraD k l B) ⊗[k] (AlgebraD k l B)ᵐᵒᵖ) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.AlgebraD

  2. def OAI.LittleFinitistic.OrdinarySimulation.XResolution.recoveredObjectIso line 19
  3. def OAI.LittleFinitistic.OrdinarySimulation.XResolution.targetIso line 31

    Source documentation

    The previous component target is exactly X in degree zero, with both D-actions.

    def targetIso : target P a l ≅ (HomologicalComplex.single _ (.up ℤ) 0).obj (ordinaryXObject P a l) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.target, OAI.LittleFinitistic.OrdinarySimulation.XResolution.ordinaryXObject

  4. def OAI.LittleFinitistic.OrdinarySimulation.XResolution.augmentationToX line 36
  5. theorem OAI.LittleFinitistic.OrdinarySimulation.XResolution.augmentationToX_quasiIso line 41

    Source documentation

    The actual bounded right-projective complex augments quasi-isomorphically to X.

    theorem augmentationToX_quasiIso : QuasiIso (augmentationToX P a l) := by
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.augmentationToX