fac — Mathlib

English

For a morphism f with effective epi property and any e: Y → W, if two arrows into Y agree after composing with f, then composing with the universal desc map gives equality with e.

Русский

Для морфизма f с эффективной эпиклассностью и любого e: Y → W, если два гомоморфизма в Y согласуются после композиции с f, то композиция через универсальный desc даёт равенство с e.

LaTeX

$$$f \\circ EffectiveEpi.desc(f,e,h) = e$$$

Lean4

@[reassoc (attr := simp)]
theorem fac {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) : f ≫ EffectiveEpi.desc f e h = e :=
  (EffectiveEpi.getStruct f).fac e h

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