OAI/Algebra/Finitistic/Localization/OddDouble.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OddDouble.sourceProjector line 14
2. def OAI.LittleFinitistic.OddDouble.targetProjector line 17
3. theorem OAI.LittleFinitistic.OddDouble.sourceProjector_idem line 24
4. theorem OAI.LittleFinitistic.OddDouble.targetProjector_idem line 29
5. theorem OAI.LittleFinitistic.OddDouble.sourceProjector_comp line 34
6. theorem OAI.LittleFinitistic.OddDouble.comp_targetProjector line 37
7. theorem OAI.LittleFinitistic.OddDouble.targetProjector_comp_second line 49
8. theorem OAI.LittleFinitistic.OddDouble.third_comp_sourceProjector line 54
9. theorem OAI.LittleFinitistic.OddDouble.cone_splitting line 62

   Source documentation

   Splitting data for the cone of a morphism admitting a generalized inverse. These are the five biproduct equations in the idempotent completion.

   theorem cone_splitting :
       ∃ (s : T.obj₁⟦(1 : ℤ)⟧ ⟶ T.obj₃) (t : T.obj₃ ⟶ T.obj₂),
         (sourceProjector T u)⟦(1 : ℤ)⟧' ≫ s = s ∧
         s ≫ T.mor₃ = (sourceProjector T u)⟦(1 : ℤ)⟧' ∧
         t ≫ targetProjector T u = t ∧
         T.mor₂ ≫ t = targetProjector T u ∧
         s ≫ t = 0 ∧
         t ≫ T.mor₂ + T.mor₃ ≫ s = 𝟙 T.obj₃ := by
   …

   Mentions: OAI.LittleFinitistic.OddDouble.sourceProjector, OAI.LittleFinitistic.OddDouble.targetProjector

10. def OAI.LittleFinitistic.OddDouble.formalKernel line 110
11. def OAI.LittleFinitistic.OddDouble.formalCokernel line 115
12. theorem OAI.LittleFinitistic.OddDouble.regular_cone_iso line 122

    Source documentation

    The cone of a regular morphism is the direct sum of its formal cokernel and the shifted formal kernel in the idempotent completion.

    theorem regular_cone_iso :
        Nonempty ((toKaroubi C).obj T.obj₃ ≅ formalCokernel T u hu ⊞ formalKernel T u hu) := by
    …

    Mentions: OAI.LittleFinitistic.OddDouble.formalCokernel, OAI.LittleFinitistic.OddDouble.formalKernel

13. def OAI.LittleFinitistic.OddDouble.formalShift line 157
14. theorem OAI.LittleFinitistic.OddDouble.odd_double_one line 163

    Source documentation

    The first odd double is the cone of the complementary idempotent.

    theorem odd_double_one (U : Karoubi C) :
        ∃ S : C, Nonempty ((toKaroubi C).obj S ≅ U ⊞ formalShift U 1) := by
    …

    Mentions: OAI.LittleFinitistic.OddDouble.formalShift

15. def OAI.LittleFinitistic.OddDouble.formalShiftFunctor line 191
16. instance OAI.LittleFinitistic.OddDouble.(instance at line 199) line 199
17. def OAI.LittleFinitistic.OddDouble.retractProjector line 202
18. def OAI.LittleFinitistic.OddDouble.retractProjectorIso line 213
19. theorem OAI.LittleFinitistic.OddDouble.odd_double_three_nested line 227

    Source documentation

    The second cone realizes the third odd double, with three successive shifts.

    theorem odd_double_three_nested (U : Karoubi C) :
        ∃ Z : C, Nonempty ((toKaroubi C).obj Z ≅
          U ⊞ formalShift (formalShift (formalShift U 1) 1) 1) := by
    …

    Mentions: OAI.LittleFinitistic.OddDouble.formalShift

20. def OAI.LittleFinitistic.OddDouble.formalIso line 303
21. def OAI.LittleFinitistic.OddDouble.formalShiftAdd line 322
22. theorem OAI.LittleFinitistic.OddDouble.odd_double_three line 328

    Source documentation

    Both odd doubles in the manuscript are represented by actual objects.

    theorem odd_double_three (U : Karoubi C) :
        ∃ Z : C, Nonempty ((toKaroubi C).obj Z ≅ U ⊞ formalShift U 3) := by
    …

    Mentions: OAI.LittleFinitistic.OddDouble.formalShift