English
If W is a MorphismProperty on C with a right calculus of fractions for a localization L : C ⥤ D, then the opposite situation W.unop on Cᵒᵖ has a left calculus of fractions.
Русский
Если W является свойством морфизмов на C и существует правый калькулюс дробей для локализации L : C ⥤ D, тогда противоположное свойство W.unop на Cᵒᵖ обладает левым калькулюсом дробей.
LaTeX
$$$\operatorname{HasLeftCalculusOfFractions}(W^{op})$$$
Lean4
instance (W : MorphismProperty Cᵒᵖ) [h : W.HasRightCalculusOfFractions] : W.unop.HasLeftCalculusOfFractions
where
exists_leftFraction X Y
φ := by
obtain ⟨ψ, eq⟩ := h.exists_rightFraction φ.op
exact ⟨ψ.unop, Quiver.Hom.op_inj eq⟩
ext X' X Y f₁ f₂ s hs
eq := by
obtain ⟨Y', t, ht, fac⟩ := h.ext f₁.op f₂.op s.op hs (Quiver.Hom.unop_inj eq)
exact ⟨Opposite.unop Y', t.unop, ht, Quiver.Hom.op_inj fac⟩
