English
There exists a nonempty AttachCells structure for g and f iff the pushouts of coproducts of g along f exist.
Русский
Существует ненулевой AttachCells-построение для g и f тогда и только тогда существуют пушауты копроductов g вдоль f.
LaTeX
$$$\mathrm{Nonempty}(\mathrm{AttachCells}\, g\, f) \iff (\mathrm{coproducts}(\mathrm{ofHoms}\, g)).\mathrm{pushouts}\ f$$$
Lean4
theorem nonempty_attachCells_iff : Nonempty (AttachCells.{w} g f) ↔ (coproducts.{w} (ofHoms g)).pushouts f :=
by
constructor
· rintro ⟨c⟩
exact c.pushouts_coproducts
· rintro ⟨Y₁, Y₂, m, g₁, g₂, h, sq⟩
rw [coproducts_iff] at h
obtain ⟨ι, ⟨F₁, F₂, c₁, c₂, h₁, h₂, φ, hφ⟩⟩ := h
let π (i : ι) : α := ((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose
let e (i : ι) : Arrow.mk (φ.app ⟨i⟩) ≅ Arrow.mk (g (π i)) := eqToIso (((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose_spec)
let e₁ (i : ι) : F₁.obj ⟨i⟩ ≅ A (π i) := Arrow.leftFunc.mapIso (e i)
let e₂ (i : ι) : F₂.obj ⟨i⟩ ≅ B (π i) := Arrow.rightFunc.mapIso (e i)
exact
⟨{ ι := ι
π := π
cofan₁ := Cofan.mk c₁.pt (fun i ↦ (e₁ i).inv ≫ c₁.ι.app ⟨i⟩)
cofan₂ := Cofan.mk c₂.pt (fun i ↦ (e₂ i).inv ≫ c₂.ι.app ⟨i⟩)
isColimit₁ :=
(IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₁ i)) _).1
(IsColimit.ofIsoColimit h₁ (Cocones.ext (Iso.refl _) (by simp)))
isColimit₂ :=
(IsColimit.precomposeHomEquiv (Discrete.natIso (fun ⟨i⟩ ↦ e₂ i)) _).1
(IsColimit.ofIsoColimit h₂ (Cocones.ext (Iso.refl _) (by simp)))
hm i := by simp [e₁, e₂]
isPushout := sq, .. }⟩
