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