English
Extensional equality for composed components: ext_from_iff ensures coequalization via components implies equality of maps.
Русский
Расширение через компоненты и их композиции: ext_from_iff обеспечивает равенство отображений при равенстве их компонент.
LaTeX
$$$f,g: X ⊞ Y \to Z$;\ f=g \iff (f \circ \mathrm{biprod.inl} = g \circ \mathrm{biprod.inl}) \land (f \circ \mathrm{biprod.inr} = g \circ \mathrm{biprod.inr})$$$
Lean4
@[simp]
theorem ofComponents_comp {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂)
(g₁₁ : Y₁ ⟶ Z₁) (g₁₂ : Y₁ ⟶ Z₂) (g₂₁ : Y₂ ⟶ Z₁) (g₂₂ : Y₂ ⟶ Z₂) :
Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ Biprod.ofComponents g₁₁ g₁₂ g₂₁ g₂₂ =
Biprod.ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁)
(f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) :=
by
dsimp [Biprod.ofComponents]
ext <;>
simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst, biprod.inl_snd, biprod.inr_fst, biprod.inr_snd,
biprod.inl_fst_assoc, biprod.inl_snd_assoc, biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp,
Category.assoc]
