OAI/Algebra/Finitistic/Ordinary/OrdinaryResolutionComplex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.extendedVertex line 14

   Source documentation

   Extending the source idempotents by zero keeps all right ideals in the same C.

   def extendedVertex (n : ℕ) : ChainAlgebra k l :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

2. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.extendedArrow line 17
3. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.extendedVertex_idempotent line 20
4. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.extendedArrow_target line 27
5. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.extendedArrow_square line 35
6. abbrev OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionIdeal line 41
7. abbrev OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionTerm line 42
8. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionDifferential line 46

   Source documentation

   Actual left-arrow differentials, with no transport of module types.

   def resolutionDifferential (n : ℕ) : resolutionTerm k l n ⟶ resolutionTerm k l (n+1) :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionTerm

9. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionDifferential_square line 52
10. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalProjectiveComplex line 59

    Source documentation

    The source's projective complex, extended by zero after degree l.

    def terminalProjectiveComplex : CochainComplex (ModuleCat.{u} (ChainAlgebra k l)ᵐᵒᵖ) ℕ :=
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

11. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionTerm_projective line 62
12. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionTerm_vanishes line 72