exists_rightFraction — Mathlib

English

For any morphism f : L.obj X ⟶ L.obj Y, there exists φ ∈ W.RightFraction X Y such that f = φ.map L (Localization.inverts L W).

Русский

Для любого морфизма f: L.obj X → L.obj Y существует φ ∈ W.RightFraction X Y такой, что f = φ.map L (Localization.inverts L W).

LaTeX

$$$\exists \phi : W.RightFraction X Y, f = \phi.map L (Localization.inverts L W)$$$

Lean4

theorem exists_rightFraction {X Y : C} (f : L.obj X ⟶ L.obj Y) :
    ∃ (φ : W.RightFraction X Y), f = φ.map L (Localization.inverts L W) :=
  by
  obtain ⟨φ, eq⟩ := Localization.exists_leftFraction L.op W.op f.op
  refine ⟨φ.unop, Quiver.Hom.op_inj ?_⟩
  rw [eq, MorphismProperty.RightFraction.op_map]
  rfl

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