uniq — Mathlib

English

The effective epi structure provides a unique desc map: if m: X → W satisfies f ≫ m = e, then m = EffectiveEpi.desc f e h.

Русский

Структура эффективной эпиморфии задаёт единственный desc: если m: X → W удовлетворяет f ≫ m = e, то m = EffectiveEpi.desc f e h.

LaTeX

$$m = EffectiveEpi.desc f e h$$

Lean4

theorem uniq {X Y W : C} (f : Y ⟶ X) [EffectiveEpi f] (e : Y ⟶ W)
    (h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), g₁ ≫ f = g₂ ≫ f → g₁ ≫ e = g₂ ≫ e) (m : X ⟶ W) (hm : f ≫ m = e) :
    m = EffectiveEpi.desc f e h :=
  (EffectiveEpi.getStruct f).uniq e h _ hm

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