OAI/Algebra/Finitistic/Localization/TwoDegreeSplitting.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.TwoDegreeFormality.C line 12
  2. abbrev OAI.LittleFinitistic.TwoDegreeFormality.D line 13
  3. abbrev OAI.LittleFinitistic.TwoDegreeFormality.H line 14
  4. abbrev OAI.LittleFinitistic.TwoDegreeFormality.stalk line 15
  5. def OAI.LittleFinitistic.TwoDegreeFormality.upperIso line 18
  6. def OAI.LittleFinitistic.TwoDegreeFormality.lowerIso line 23
  7. def OAI.LittleFinitistic.TwoDegreeFormality.lowerShiftIso line 30
  8. theorem OAI.LittleFinitistic.TwoDegreeFormality.connecting_eq_zero line 36

    Source documentation

    The connecting map of the actual truncation triangle vanishes by Ext^4=0.

    theorem connecting_eq_zero : (triangle X).mor₃ = 0 := by
…
  9. structure OAI.LittleFinitistic.TwoDegreeFormality.TruncationSplit line 45

    Source documentation

    A splitting of the actual truncation triangle, retaining its inclusion and projection.

    structure TruncationSplit where
…
  10. def OAI.LittleFinitistic.TwoDegreeFormality.truncationSplit line 50
  11. def OAI.LittleFinitistic.TwoDegreeFormality.splitIso line 56

    Source documentation

    Actual B-linear two-degree formality, with the manuscript's shift by three.

    def splitIso : X ≅ stalk P (H P 0 X) ⊞ (stalk P (H P (-3) X))⟦(3 : ℤ)⟧ :=
…

    Mentions: OAI.LittleFinitistic.TwoDegreeFormality.stalk, OAI.LittleFinitistic.TwoDegreeFormality.H