hom_ext — Mathlib

English

In a pushout diagram given by AttachCells, equality of morphisms φ1, φ2 after composing with f and with every cell i implies φ1 = φ2.

Русский

В пушаут-диаграмме AttachCells равенство φ1 и φ2 по композициям с f и с каждым элементом клетки i требует, чтобы φ1 = φ2.

LaTeX

$$$\forall Z, \forall φ_1, φ_2:\ X_2 \to Z,\; (f \circ φ_1 = f \circ φ_2) \Rightarrow (\forall i, σ_i \circ φ_1 = σ_i \circ φ_2) \Rightarrow φ_1 = φ_2$$$

Lean4

theorem hom_ext {Z : C} {φ φ' : X₂ ⟶ Z} (h₀ : f ≫ φ = f ≫ φ') (h : ∀ i, c.cell i ≫ φ = c.cell i ≫ φ') : φ = φ' :=
  by
  apply c.isPushout.hom_ext h₀
  apply Cofan.IsColimit.hom_ext c.isColimit₂
  simpa [cell_def] using h

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