inr_fst — Mathlib

English

Dual statement via opposite category: a pullback in C corresponds to a pushout in C^op.

Русский

Дуалитет через противоположную категорию: пуллбак в C эквивалентен пушауту в C^op.

LaTeX

$$$ IsPullback fst snd f g \\Rightarrow IsPushout g^{op} f^{op} snd^{op} fst^{op} $$$

Lean4

/-- The square
```
  Y --inr--> X ⊞ Y
  |            |
  0           fst
  |            |
  v            v
  0 ---0-----> X
```
is a pullback square.
-/
@[simp]
theorem inr_fst (X Y : C) [HasBinaryBiproduct X Y] : IsPullback biprod.inr (0 : Y ⟶ 0) biprod.fst (0 : 0 ⟶ X) :=
  inr_fst' (BinaryBiproduct.isBilimit X Y)

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