of_has_biproduct₂ — Mathlib

English

With zero objects and zero morphisms, the square X ⊕ Y with zero maps yields a bi-cartesian square: IsPushout (0 : X ⟶ 0) (0 : Y ⟶ 0) biprod.inl biprod.inr.

Русский

При наличии нулевых объектов и нулевых морфизмов квадрат X ⊕ Y с нулевыми отображениями образует бикартезианский квадрат: IsPushout (0 : X ⟶ 0) (0 : Y ⟶ 0) biprod.inl biprod.inr.

LaTeX

$$$ \\operatorname{IsPushout}(0_{X}, 0_{Y}, \\mathrm{inl}, \\mathrm{inr}) $$$

Lean4

/-- ```
   0 -----0---> X
   |            |
   0           inl
   |            |
   v            v
   Y --inr--> X ⊞ Y
```
is a bi-Cartesian square.
-/
@[simp]
theorem of_has_biproduct₂ [HasBinaryBiproduct X Y] : BicartesianSq (0 : 0 ⟶ X) (0 : 0 ⟶ Y) biprod.inl biprod.inr := by
  convert of_is_biproduct₂ (BinaryBiproduct.isBilimit X Y)

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