fac — Mathlib

English

For a family X: α → C with epimorphic components π a, and a family e a : X a → W, the component π a composed with the desc equals e a.

Русский

Для семейства X: α → C с эпиморфическими компонентами π a и семейства e a: X a → W, компонент π a через desc равен e a.

LaTeX

$$$\\pi a \\circ EffectiveEpiFamily.desc X \\pi e h = e a$$$

Lean4

@[reassoc (attr := simp)]
theorem fac {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 _) (a : α) :
    π a ≫ EffectiveEpiFamily.desc X π e h = e a :=
  (EffectiveEpiFamily.getStruct X π).fac e h a

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