homMk_eq_of_leftFractionRel — Mathlib

English

Let C be a category and W a morphism property with a left calculus of fractions. For any X,Y in C and left fractions z1,z2 : W.LeftFraction X Y with LeftFractionRel z1 z2, the corresponding arrows in the localization are equal.

Русский

Пусть C — категория, W — свойство морфизмов с левой теорией дробей; для любых объектов X,Y в C и левых дробях z1,z2 : W.LeftFraction X Y, удовлетворяющих LeftFractionRel z1 z2, соответствующие стрелки в локализации совпадают.

LaTeX

$$$\forall {C} {D} [\text{Category } C] [\text{Category } D] {W} {X Y : C},\quad z_1,z_2 : W.LeftFraction X Y\;\to\;LeftFractionRel(z_1,z_2)\;\Rightarrow\; homMk(z_1)=homMk(z_2)$$$

Lean4

theorem homMk_eq_of_leftFractionRel {X Y : C} (z₁ z₂ : W.LeftFraction X Y) (h : LeftFractionRel z₁ z₂) :
    homMk z₁ = homMk z₂ :=
  Quot.sound h

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