hom_ext_iff — Mathlib

English

Two morphisms are equal iff their underlying parts are equal and the component maps agree up to equality of their indices.

Русский

Два морфизма равны тогда и только тогда, когда их структуры совпадают и компоненты согласованы по индексу.

LaTeX

$$$f=g \\iff \\exists h_1: f.f=h_1=g.f \\land \\forall i, f.φ_i ≫ eqToHom(h_1) = g.φ_i$$$

Lean4

theorem hom_ext_iff {X Y : FormalCoproduct.{w} C} (f g : X ⟶ Y) :
    f = g ↔ ∃ h₁ : f.f = g.f, ∀ (i : X.I), f.φ i ≫ eqToHom (by rw [h₁]) = g.φ i :=
  ⟨(· ▸ by simp), fun ⟨h₁, h₂⟩ ↦ hom_ext h₁ h₂⟩

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