hom_ext' — Mathlib

English

If two maps f, g: X.obj Δ ⟶ Z agree after precomposing with every cofan injection from the distinguished summands, then f = g.

Русский

Если две стрелки f и g совпадают после префиксирования через каждую inj кокона на выделенные подчасти, то f = g.

LaTeX

$$$\forall A, (s.cofan(\Delta).inj A) \;\circ\; f = (s.cofan(\Delta).inj A) \;\circ\; g \Rightarrow f = g$$$

Lean4

theorem hom_ext' {Z : C} {Δ : SimplexCategoryᵒᵖ} (f g : X.obj Δ ⟶ Z)
    (h : ∀ A : IndexSet Δ, (s.cofan Δ).inj A ≫ f = (s.cofan Δ).inj A ≫ g) : f = g :=
  Cofan.IsColimit.hom_ext (s.isColimit Δ) _ _ h

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