OAI/Algebra/Finitistic/Localization/SourceVerdier.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.SourceVerdier.Proj line 13
  2. abbrev OAI.LittleFinitistic.SourceVerdier.K line 14
  3. abbrev OAI.LittleFinitistic.SourceVerdier.vertex line 17

    Source documentation

    The manuscript's specified vertex idempotent.

    abbrev vertex (i : Fin 3) : B P := ThreeVertexAlgebra.vertex (QuadraticEncoding.composition P) i

    Mentions: OAI.LittleFinitistic.ThreeVertexAlgebra.vertex, OAI.LittleFinitistic.QuadraticEncoding.composition

  4. theorem OAI.LittleFinitistic.SourceVerdier.vertex_idem line 19
  5. def OAI.LittleFinitistic.SourceVerdier.E line 23

    Source documentation

    E_i = e_i B as an actual finite projective right module.

    def E (i : Fin 3) : Proj P := VertexProjectives.object (vertex P i) (vertex_idem P i)

    Mentions: OAI.LittleFinitistic.SourceVerdier.Proj, OAI.LittleFinitistic.VertexProjectives.object, OAI.LittleFinitistic.SourceVerdier.vertex, OAI.LittleFinitistic.SourceVerdier.vertex_idem

  6. theorem OAI.LittleFinitistic.SourceVerdier.target01 line 25
  7. theorem OAI.LittleFinitistic.SourceVerdier.target12 line 30
  8. def OAI.LittleFinitistic.SourceVerdier.arrow01 line 36

    Source documentation

    The actual right-module arrow maps, given by left multiplication.

    def arrow01 (i : Fin (d+1)) : E P 0 ⟶ E P 1 :=
…

    Mentions: OAI.LittleFinitistic.SourceVerdier.E

  9. def OAI.LittleFinitistic.SourceVerdier.arrow12 line 39
  10. def OAI.LittleFinitistic.SourceVerdier.stalk line 44

    Source documentation

    Regard a projective as a bounded complex concentrated in degree zero.

    def stalk : Proj P ⥤ K P :=
…

    Mentions: OAI.LittleFinitistic.SourceVerdier.Proj, OAI.LittleFinitistic.SourceVerdier.K

  11. def OAI.LittleFinitistic.SourceVerdier.s line 50
  12. def OAI.LittleFinitistic.SourceVerdier.s' line 51
  13. def OAI.LittleFinitistic.SourceVerdier.cones line 54

    Source documentation

    The cone choices are made once, in K, before any evaluation module is chosen.

    def cones : TwoConeVerdier.ConePair (K P) := by
…

    Mentions: OAI.LittleFinitistic.TwoConeVerdier.ConePair, OAI.LittleFinitistic.SourceVerdier.K

  14. theorem OAI.LittleFinitistic.SourceVerdier.cones_first line 61
  15. theorem OAI.LittleFinitistic.SourceVerdier.cones_second line 62
  16. abbrev OAI.LittleFinitistic.SourceVerdier.S line 65

    Source documentation

    Exactly the thick closure of Cone(s), Cone(s').

    abbrev S : ObjectProperty (K P) := (cones P).S

    Mentions: OAI.LittleFinitistic.SourceVerdier.K, OAI.LittleFinitistic.SourceVerdier.cones

  17. abbrev OAI.LittleFinitistic.SourceVerdier.Sigma line 66
  18. abbrev OAI.LittleFinitistic.SourceVerdier.Q line 68

    Source documentation

    Section 3's actual Verdier quotient K/S.

    abbrev Q := (cones P).Q

    Mentions: OAI.LittleFinitistic.SourceVerdier.cones

  19. abbrev OAI.LittleFinitistic.SourceVerdier.q line 69
  20. theorem OAI.LittleFinitistic.SourceVerdier.fraction_calculus line 72

    Source documentation

    The actual, proved fraction and localization hypotheses needed by DiagramLifting.

    theorem fraction_calculus : (Sigma P).HasRightCalculusOfFractions := inferInstance

    Mentions: OAI.LittleFinitistic.SourceVerdier.Sigma

  21. theorem OAI.LittleFinitistic.SourceVerdier.localization line 73
  22. theorem OAI.LittleFinitistic.SourceVerdier.triangulated line 74
  23. instance OAI.LittleFinitistic.SourceVerdier.s_inverted line 76
  24. instance OAI.LittleFinitistic.SourceVerdier.s'_inverted line 78
  25. theorem OAI.LittleFinitistic.SourceVerdier.zero_fraction line 81