English
Given z1, z2, z3 with h3 compatibility, z1.comp z2 equals Localization.Hom.mk (z1.comp₀ z2 z3).
Русский
При данных z1, z2, z3 с совместимостью h3, z1.comp z2 равно Localization.Hom.mk (z1.comp₀ z2 z3).
LaTeX
$$z_1.comp z_2 = Localization.Hom.mk\left(z_1.comp_0 z_2 z_3\right)$$
Lean4
theorem trans {X Y : C} {z₁ z₂ z₃ : W.LeftFraction X Y} [HasLeftCalculusOfFractions W] (h₁₂ : LeftFractionRel z₁ z₂)
(h₂₃ : LeftFractionRel z₂ z₃) : LeftFractionRel z₁ z₃ :=
by
obtain ⟨Z₄, t₁, t₂, hst, hft, ht⟩ := h₁₂
obtain ⟨Z₅, u₂, u₃, hsu, hfu, hu⟩ := h₂₃
obtain ⟨⟨v₄, v₅, hv₅⟩, fac⟩ :=
HasLeftCalculusOfFractions.exists_leftFraction (RightFraction.mk (z₁.s ≫ t₁) ht (z₃.s ≫ u₃))
simp only [Category.assoc] at fac
have eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄ := by simpa only [← reassoc_of% hsu, reassoc_of% hst] using fac
obtain ⟨Z₇, w, hw, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₂.hs eq
simp only [Category.assoc] at fac'
refine ⟨Z₇, t₁ ≫ v₄ ≫ w, u₃ ≫ v₅ ≫ w, ?_, ?_, ?_⟩
· rw [reassoc_of% fac]
· rw [reassoc_of% hft, ← fac', reassoc_of% hfu]
· rw [← reassoc_of% fac, ← reassoc_of% hsu, ← Category.assoc]
exact W.comp_mem _ _ hu (W.comp_mem _ _ hv₅ hw)
