TruncationSplitNaturality.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.TwoDegreeFormality.upper_to_lower_eq_zero line 15
Source documentation
Ext^3 kills the only possible off-diagonal ambiguity in a truncation splitting.
```
theorem upper_to_lower_eq_zero (f : upper X ⟶ lower Y) : f = 0 := by
…
```
lemma OAI.LittleFinitistic.TwoDegreeFormality.truncation_split_square line 23
theorem OAI.LittleFinitistic.TwoDegreeFormality.truncationSplit_naturality line 50
Source documentation
The chosen actual splitting commutes with every morphism of two-degree objects.
```
theorem truncationSplit_naturality (f : X ⟶ Y) :
    f ≫ (truncationSplit P Y hY).iso.hom = (truncationSplit P X hX).iso.hom ≫ biprod.map
      ((DerivedTruncation.t.truncLT 0).map f) ((DerivedTruncation.t.truncGE 0).map f) :=
…
```
Mentions: OAI.LittleFinitistic.TwoDegreeFormality.truncationSplit