OAI/Algebra/Finitistic/Ordinary/OrdinaryChainResolution.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.arrow_mul line 12
2. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.smul_diagonal line 21
3. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.smul_radical line 23
4. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex_diagonal line 25
5. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.arrow_diagonal line 27
6. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.arrow_radical line 29
7. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex_succ_mul line 33

   Source documentation

   The two displayed coordinates of each noninitial right projective.

   theorem vertex_succ_mul (i : Fin l) (x : ChainAlgebra k l) :
       vertex k l i.succ * x = x.1 i.succ • vertex k l i.succ + x.2 i • arrow k l i := by
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.arrow

8. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex_zero_mul line 48

   Source documentation

   The initial projective has no radical coordinate.

   theorem vertex_zero_mul (x : ChainAlgebra k l) :
       vertex k l 0 * x = x.1 0 • vertex k l 0 := by
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex

9. abbrev OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm line 59

   Source documentation

   Actual right projectives in the source resolution.

   abbrev rightTerm (i : Fin (l+1)) := IdempotentTensor.rightIdeal (vertex k l i)

   Mentions: OAI.LittleFinitistic.IdempotentTensor.rightIdeal, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex

10. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.leftMultiply line 61
11. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.retract line 66
12. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightRegularEquiv line 71
13. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm_projective line 79
14. def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionMap line 87

    Source documentation

    The differential is actual left multiplication by the source arrow.

    def resolutionMap (i : Fin l) : rightTerm (k := k) i.castSucc →ₗ[(ChainAlgebra k l)ᵐᵒᵖ] rightTerm (k := k) i.succ :=
    …

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

15. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionMap_value line 92
16. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm_succ_expansion line 96

    Source documentation

    This is the explicit two-coordinate expansion, not a dimension argument.

    theorem rightTerm_succ_expansion (i : Fin l) (x : rightTerm (k := k) i.succ) :
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm

17. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionMap_square line 102

    Source documentation

    The source's resolution differentials square to zero.

    theorem resolutionMap_square (i : ℕ) (hi : i+1 < l) :
        (resolutionMap (k := k) (⟨i+1,hi⟩ : Fin l)).comp
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionMap

18. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionMap_zero_iff line 109
19. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionMap_range line 122

    Source documentation

    Exact description of the image: the one-dimensional radical in the next term.

    theorem resolutionMap_range (i : Fin l) (x : rightTerm (k := k) i.succ) :
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm

20. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolution_exact line 144

    Source documentation

    Exactness at every interior projective, with no assumed resolution predicate.

    theorem resolution_exact (i : ℕ) (hi : i+1 < l)
        (x : rightTerm (k := k) (⟨i+1,by omega⟩ : Fin (l+1))) :
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.rightTerm

21. theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolution_first_injective line 152

    Source documentation

    Injectivity of the first nonzero differential in the resolution.

    theorem resolution_first_injective (hl : 0 < l) :
        Function.Injective (resolutionMap (k := k) (⟨0,hl⟩ : Fin l)) := by
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.resolutionMap