Qiso_hom_inv_id — Mathlib

English

For any morphism s in W, the map (Q W).map s has a quasi-inverse given by Qinv s hs, making a genuine isomorphism in the localization.

Русский

Для любого морфизма s из W отображение (Q W).map s имеет квазиобратную стрелку Qinv s hs, образуя изоморфизм в локализации.

LaTeX

$$$\forall {C} [\text{Category } C] {W} [W.HasLeftCalculusOfFractions] {X Y} (s: X \to Y) (hs: W s), (Q W).map s ≫ Qinv s hs = 1$$$

Lean4

@[reassoc (attr := simp)]
theorem Qiso_hom_inv_id {X Y : C} (s : X ⟶ Y) (hs : W s) : (Q W).map s ≫ Qinv s hs = 𝟙 _ :=
  (Qiso s hs).hom_inv_id

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