inverts — Mathlib

English

For any W with left calculus of fractions and any E, the functor Q W is inverted by W in a universal way, ensuring that W-inverted arrows become isomorphisms and localization is universal.

Русский

Для любого W с левой теорией дробей и любого E, прообраз Q W умножает на инвертируемые стрелки, приводя к уникальному локализационному свойству, т.е. локализация универсальна по отношению к W.

LaTeX

$$$\forall {C} [\text{Category } C] {W} [W.HasLeftCalculusOfFractions] {E} [\text{Category } E], W.IsInvertedBy (Q W)$$$

Lean4

theorem inverts : W.IsInvertedBy (Q W) := fun _ _ s hs => (inferInstance : IsIso (Qiso s hs).hom)

Похожие утверждения