hom_ext' — Mathlib

English

The homomorphism component of the isoCoprod is the biprod description.

Русский

Гомоморфизм изоморфизма biprod.isoCoprod равен biprod.desc coprod.inl coprod.inr.

LaTeX

$$$ (\biprod.isoCoprod X Y).hom = \biprod.desc \; \text{coprod.inl} \; \text{coprod.inr} $$$

Lean4

@[ext]
theorem hom_ext' {X Y Z : C} [HasBinaryBiproduct X Y] (f g : X ⊞ Y ⟶ Z) (h₀ : biprod.inl ≫ f = biprod.inl ≫ g)
    (h₁ : biprod.inr ≫ f = biprod.inr ≫ g) : f = g :=
  BinaryCofan.IsColimit.hom_ext (BinaryBiproduct.isColimit X Y) h₀ h₁

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