English
In a category with binary coproducts A ⊔ X and B ⊔ X, the square with coprod.inl and coprod.map f (ids) is a pushout: IsPushout coprod.inl f (coprod.map f (id_X)) coprod.inl.
Русский
В категории с бинным копродуктом A ⊔ X и B ⊔ X диаграмма с coprod.inl и coprod.map f(идентично) является пуш-аутом.
LaTeX
$$$ \\operatorname{IsPushout}(\\operatorname{coprod.inl}, f, \\operatorname{coprod.map}(f, \\mathrm{id}_X), \\operatorname{coprod.inl}) $$$
Lean4
/-- In a category, given a morphism `f : A ⟶ B` and an object `X`,
this is the obvious pushout diagram:
```
A ⟶ A ⨿ X
| |
v v
B ⟶ B ⨿ X
```
-/
theorem of_coprod_inl_with_id {A B : C} (f : A ⟶ B) (X : C) [HasBinaryCoproduct A X] [HasBinaryCoproduct B X] :
IsPushout coprod.inl f (coprod.map f (𝟙 X)) coprod.inl
where
w := by simp
isColimit' :=
⟨PushoutCocone.isColimitAux' _
(fun s ↦ by
refine ⟨coprod.desc s.inr (coprod.inr ≫ s.inl), ?_, ?_, ?_⟩
· ext
· simp [PushoutCocone.condition]
· simp
· simp
· intro m h₁ h₂
dsimp at m h₁ h₂ ⊢
ext
· simpa using h₂
· simp [← h₁])⟩
