English
If t is triangulated and P.IsTriangulated, then P.trW.HasRightCalculusOfFractions.
Русский
Если t треугольная и P IsTriangulated, то P.trW имеет правые вычислительные дроби.
LaTeX
$$$[IsTriangulated C] [P.IsTriangulated] : P.trW.HasRightCalculusOfFractions$$$
Lean4
instance [IsTriangulated C] [P.IsTriangulated] : P.trW.HasRightCalculusOfFractions
where
exists_rightFraction X Y
φ := by
obtain ⟨Z, f, g, H, mem⟩ := φ.hs
obtain ⟨X', f', h', mem'⟩ := distinguished_cocone_triangle₁ (φ.f ≫ f)
obtain ⟨a, ⟨ha₁, _⟩⟩ := complete_distinguished_triangle_morphism₁ _ _ mem' H φ.f (𝟙 Z) (by simp)
exact ⟨MorphismProperty.RightFraction.mk f' ⟨_, _, _, mem', mem⟩ a, ha₁⟩
ext Y Z Z' f₁ f₂ s hs
hf₁ := by
rw [P.trW_iff'] at hs
obtain ⟨Z, g, h, H, mem⟩ := hs
have hf₂ : (f₁ - f₂) ≫ s = 0 := by rw [sub_comp, hf₁, sub_self]
obtain ⟨q, hq⟩ := Triangle.coyoneda_exact₂ _ H _ hf₂
obtain ⟨Y', r, t, mem'⟩ := distinguished_cocone_triangle₁ q
refine ⟨Y', r, ?_, ?_⟩
· exact ⟨_, _, _, mem', mem⟩
· have eq := comp_distTriang_mor_zero₁₂ _ mem'
dsimp at eq
rw [← sub_eq_zero, ← comp_sub, hq, reassoc_of% eq, zero_comp]
