English
If W has a right calculus of fractions, then W.op has a left calculus of fractions with explicit left-fraction existence transported via op.
Русский
Если у W есть правая теория дробей, то W.op имеет левую теорию дробей, существование левых дробей переносится через операцию Opposite.
LaTeX
$$$\forall {C D} [\text{Category } C] [\text{Category } D] (L : C \to D) (W : MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions],
W.op.HasLeftCalculusOfFractions$$$
Lean4
instance [h : W.HasLeftCalculusOfFractions] : W.op.HasRightCalculusOfFractions
where
exists_rightFraction X Y
φ := by
obtain ⟨ψ, eq⟩ := h.exists_leftFraction φ.unop
exact ⟨ψ.op, Quiver.Hom.unop_inj eq⟩
ext X Y Y' f₁ f₂ s hs
eq := by
obtain ⟨X', t, ht, fac⟩ := h.ext f₁.unop f₂.unop s.unop hs (Quiver.Hom.op_inj eq)
exact ⟨Opposite.op X', t.op, ht, Quiver.Hom.unop_inj fac⟩
