OAI/Algebra/Finitistic/Ordinary/OrdinaryTerminalResolution.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OrdinarySimulation.TerminalSimple line 10

   Source documentation

   W is the genuine terminal right simple, via the terminal character.

   def TerminalSimple := k
   …

2. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalSimple.(instance at line 12) line 12
3. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalSimple.(instance at line 13) line 13
4. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalSimple.(instance at line 14) line 14
5. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.augmentation line 20

   Source documentation

   The augmentation of the terminal right projective.

   def augmentation : rightTerm (k := k) (Fin.last l) →ₗ[(ChainAlgebra k l)ᵐᵒᵖ] TerminalSimple k where
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TerminalSimple

6. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.augmentation_zero_iff line 25
7. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.augmentation_surjective line 28
8. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.augmentation_exact line 41

   Source documentation

   Exactness at the augmentation for every positive chain length.

   theorem augmentation_exact (x : rightTerm (k := k) (Fin.last (l+1))) :
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm

9. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.augmentation_zero_injective line 47
10. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.zeroLengthResolution line 58

    Source documentation

    For l=0, the source resolution is the actual isomorphism e₀C ≅ W.

    def zeroLengthResolution : rightTerm (k := k) (Fin.last 0) ≃ₗ[(ChainAlgebra k 0)ᵐᵒᵖ] TerminalSimple k :=
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TerminalSimple