OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorResolutionComplex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.termObject line 11
  2. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.complex line 13
  3. instance OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.projectiveTerm line 17
  4. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.term_vanishes line 19
  5. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.differential_left line 30

    Source documentation

    Every differential preserves the regular left B-action.

    theorem differential_left (n : ℕ) (b : B) (x : term k B l n) :
    differential k B l n (b • x) = b • differential k B l n x := by
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.term, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.differential

  6. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.complex_exactAt line 40
  7. abbrev OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentationHom line 71
  8. instance OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation_epi line 74
  9. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentationMap line 78

    Source documentation

    The actual B-extended resolution augmentation as a chain map.

    def augmentationMap : complex k B l ⟶
    (HomologicalComplex.single _ (.up ℕ) l).obj (ModuleCat.of (B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ (TerminalTensor B)) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.complex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor

  10. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.differential_last_zero line 89
  11. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentationMap_quasiIsoAt_last line 94
  12. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentationMap_quasiIso line 150

    Source documentation

    Actual augmentation quasi-isomorphism for the finite right-BC-projective resolution.

    theorem augmentationMap_quasiIso : QuasiIso (augmentationMap k B l) := by
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentationMap