homMk_eq — Mathlib

English

For any LeftFraction f, homMk f equals the image of f under the localization map, i.e., homMk f = f.map (Q W).

Русский

Для левой дроби f равенство обозначает, что homMk f совпадает с образом f через локализационный отображатель.

LaTeX

$$$\forall {C} [\text{Category } C] {W}, {X Y : C} (f : W.LeftFraction X Y), homMk f = f.map (Q W) (Localization.inverts _ W)$$$

Lean4

theorem homMk_eq {X Y : C} (f : LeftFraction W X Y) : homMk f = f.map (Q W) (Localization.inverts _ W) :=
  by
  have := Localization.inverts (Q W) W f.s f.hs
  rw [← Q_map_comp_Qinv f.f f.s f.hs, ← cancel_mono ((Q W).map f.s), assoc, Qiso_inv_hom_id, comp_id, map_comp_map_s]

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