Lean4
/-- If a family of maps `g` is contained in another family `g'` (up to isomorphisms),
if `f : X₁ ⟶ X₂` is a morphism, and `X₂` is obtained from `X₁` by attaching cells
of the form `g`, then it is also obtained by attaching cells of the form `g'`. -/
def reindexCellTypes : AttachCells g' f where
ι := c.ι
π := a ∘ c.π
cofan₁ := Cofan.mk c.cofan₁.pt (fun i ↦ Arrow.leftFunc.map (ha (c.π i)).inv ≫ c.cofan₁.inj i)
cofan₂ := Cofan.mk c.cofan₂.pt (fun i ↦ Arrow.rightFunc.map (ha (c.π i)).inv ≫ c.cofan₂.inj i)
isColimit₁ :=
by
let e : Discrete.functor (fun i ↦ A (c.π i)) ≅ Discrete.functor (fun i ↦ A' (a (c.π i))) :=
Discrete.natIso (fun ⟨i⟩ ↦ Arrow.leftFunc.mapIso (ha (c.π i)))
refine
(IsColimit.precomposeHomEquiv e _).1 (IsColimit.ofIsoColimit c.isColimit₁ (Cofan.ext (Iso.refl _) (fun i ↦ ?_)))
simp [Cocones.precompose, e, Cofan.inj]
isColimit₂ :=
by
let e : Discrete.functor (fun i ↦ B (c.π i)) ≅ Discrete.functor (fun i ↦ B' (a (c.π i))) :=
Discrete.natIso (fun ⟨i⟩ ↦ Arrow.rightFunc.mapIso (ha (c.π i)))
refine
(IsColimit.precomposeHomEquiv e _).1 (IsColimit.ofIsoColimit c.isColimit₂ (Cofan.ext (Iso.refl _) (fun i ↦ ?_)))
simp [Cocones.precompose, e, Cofan.inj]
m := c.m
g₁ := c.g₁
g₂ := c.g₂
isPushout := c.isPushout
