English
The comp₀_rel relation is preserved under the LeftFractionRel equivalence: if z1, z2, z3 satisfy h3 and h3', then z1.comp₀ z2 z3 is related to z1.comp₀ z2 z3'.
Русский
Связь comp₀_rel сохраняется под эквивалентностью LeftFractionRel: если z1, z2, z3 удовлетворяют совместимости h3 и h3', то z1.comp₀ z2 z3 эквивалентно z1.comp₀ z2 z3'.
LaTeX
$$LeftFractionRel( z1.comp0 z2 z3, z1.comp0 z2 z3' )$$
Lean4
/-- The equivalence class of `z₁.comp₀ z₂ z₃` does not depend on the choice of `z₃` provided
they satisfy the compatibility `z₂.f ≫ z₃.s = z₁.s ≫ z₃.f`. -/
theorem comp₀_rel [W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
(z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y') (h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f) (h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f) :
LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃') :=
by
obtain ⟨z₄, fac⟩ := exists_leftFraction (RightFraction.mk z₃.s z₃.hs z₃'.s)
dsimp at fac
have eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s := by rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
obtain ⟨Y, t, ht, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₁.hs eq
simp only [assoc] at fac'
refine ⟨Y, z₄.f ≫ t, z₄.s ≫ t, ?_, ?_, ?_⟩
· simp only [comp₀, assoc, reassoc_of% fac]
· simp only [comp₀, assoc, fac']
· simp only [comp₀, assoc, ← reassoc_of% fac]
exact W.comp_mem _ _ z₂.hs (W.comp_mem _ _ z₃'.hs (W.comp_mem _ _ z₄.hs ht))
