pushouts_coproducts — Mathlib

English

For AttachCells data, the pushouts along the coproducts of g exist; i.e., the construction (coproducts (ofHoms g)).pushouts f yields a pushout object.

Русский

Для данных AttachCells существуют взятия противопоставлений по копродуктам; то есть конструкция (coproducts (ofHoms g)).pushouts f образует pushout.

LaTeX

$$$ (\\text{coproducts}(\\text{ofHoms } g)).\\text{pushouts } f$$$

Lean4

theorem pushouts_coproducts : (coproducts.{w} (ofHoms g)).pushouts f :=
  by
  refine ⟨_, _, _, _, _, ?_, c.isPushout⟩
  have : c.m = c.isColimit₁.desc (Cocone.mk _ (Discrete.natTrans (fun ⟨i⟩ ↦ by exact g (c.π i)) ≫ c.cofan₂.ι)) :=
    c.isColimit₁.hom_ext (fun ⟨i⟩ ↦ by rw [IsColimit.fac]; exact c.hm i)
  rw [this, coproducts_iff]
  exact ⟨c.ι, ⟨_, _, _, _, c.isColimit₁, c.isColimit₂, _, fun i ↦ ⟨_⟩⟩⟩

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