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