OAI/Algebra/Finitistic/Selected/SelectedRectification.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.SelectedRectification.D0 line 11
  2. abbrev OAI.LittleFinitistic.SelectedRectification.D1 line 12
  3. abbrev OAI.LittleFinitistic.SelectedRectification.D2 line 13
  4. abbrev OAI.LittleFinitistic.SelectedRectification.F line 14
  5. def OAI.LittleFinitistic.SelectedRectification.f line 15
  6. def OAI.LittleFinitistic.SelectedRectification.g line 16
  7. def OAI.LittleFinitistic.SelectedRectification.relations line 17
  8. def OAI.LittleFinitistic.SelectedRectification.bimodule line 25

    Source documentation

    One explicit bimodule complex chosen before any evaluation module.

    def bimodule : BiComplex ℂ (QuadraticEncoding.B P) :=
…

    Mentions: OAI.LittleFinitistic.QuadraticEncoding.B

  9. theorem OAI.LittleFinitistic.SelectedRectification.verified line 30

    Source documentation

    The single fixed selecting complex satisfies the full rectification lemma, including all original vertex and arrow maps, independently of Y.

    theorem verified : ∃ lo hi : ℤ, RectificationLemma.Verified P D0 D1 D2 f g relations lo hi := by
…

    Mentions: OAI.LittleFinitistic.RectificationLemma.Verified, OAI.LittleFinitistic.SelectedRectification.D0, OAI.LittleFinitistic.SelectedRectification.D1, OAI.LittleFinitistic.SelectedRectification.D2, OAI.LittleFinitistic.SelectedRectification.f, OAI.LittleFinitistic.SelectedRectification.g, OAI.LittleFinitistic.SelectedRectification.relations