uniq — Mathlib

English

The EffectiveEpiFamily structure admits a unique desc morphism: if m satisfies π a ≫ m = e a for all a, then m equals the desc map.

Русский

Структура EffectiveEpiFamily допускает уникальный morphism-desc: если для всех a выполняется π a ≫ m = e a, то m равно соответствующей desc.

LaTeX

$$m = EffectiveEpiFamily.desc X π e h$$

Lean4

theorem uniq {B W : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [EffectiveEpiFamily X π]
    (e : (a : α) → (X a ⟶ W))
    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π _ = g₂ ≫ π _ → g₁ ≫ e _ = g₂ ≫ e _) (m : B ⟶ W)
    (hm : ∀ a, π a ≫ m = e a) : m = EffectiveEpiFamily.desc X π e h :=
  (EffectiveEpiFamily.getStruct X π).uniq e h m hm

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