OAI/Algebra/Finitistic/Ordinary/OrdinaryResolutionQuasiIso.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionInitial_injective line 11
2. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalProjectiveComplex_exactAt line 19

   Source documentation

   Exactness in every degree except the terminal homology degree.

   theorem terminalProjectiveComplex_exactAt (n : ℕ) (hn : n ≠ l) :
       (terminalProjectiveComplex k l).ExactAt n := by
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalProjectiveComplex

3. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionAugmentation_surjective line 42
4. instance OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionAugmentation_epi line 45
5. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionAugmentation_comp line 48
6. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionAugmentation_exact line 54
7. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionAugmentation_zero_injective line 66
8. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionDifferential_last_zero line 70
9. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.exact_post_iso line 76

   Source documentation

   Postcomposing a short complex's second map by an isomorphism preserves exactness.

   theorem exact_post_iso {R : Type u} [Ring R] {X Y Z Z' : ModuleCat.{u} R}
       (f : X ⟶ Y) (g : Y ⟶ Z) (hfg : f ≫ g = 0) (e : Z ≅ Z')
       (h : (ShortComplex.mk f g hfg).Exact) :
       (ShortComplex.mk f (g ≫ e.hom) (by rw [← Category.assoc, hfg, zero_comp])).Exact := by
   …

10. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalAugmentationMap_quasiIsoAt_last line 87

    Source documentation

    The augmentation is a quasi-isomorphism at the terminal degree.

    theorem terminalAugmentationMap_quasiIsoAt_last :
        QuasiIsoAt (terminalAugmentationMap k l) l := by
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalAugmentationMap

11. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalAugmentationMap_quasiIso line 144

    Source documentation

    The source's finite projective resolution now has its actual augmentation quasi-isomorphism.

    theorem terminalAugmentationMap_quasiIso : QuasiIso (terminalAugmentationMap k l) := by
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalAugmentationMap