English
Given an equivalence e between index sets, one can replace the index type in an AttachCells structure by transporting along e, obtaining an equivalent AttachCells structure with the reindexed indices.
Русский
Существует замещение индексов в структуре AttachCells по эквиваленции e, получая эквивалентную структуру с переиндексированными индексами.
LaTeX
$$$\forall ι',\ e:\ ι' \simeq c.ι \Rightarrow\mathrm{AttachCells}_{g,f} \to \mathrm{AttachCells}_{g,f}$$$
Lean4
/-- This definition allows the replacement of the `ι` field of
a `AttachCells g f` structure by an equivalent type. -/
@[simps]
def reindex {ι' : Type w'} (e : ι' ≃ c.ι) : AttachCells.{w'} g f
where
ι := ι'
π i' := c.π (e i')
cofan₁ := Cofan.mk c.cofan₁.pt (fun i' ↦ c.cofan₁.inj (e i'))
cofan₂ := Cofan.mk c.cofan₂.pt (fun i' ↦ c.cofan₂.inj (e i'))
isColimit₁ := IsColimit.whiskerEquivalence (c.isColimit₁) (Discrete.equivalence e)
isColimit₂ := IsColimit.whiskerEquivalence (c.isColimit₂) (Discrete.equivalence e)
m := c.m
g₁ := c.g₁
g₂ := c.g₂
hm i' := c.hm (e i')
isPushout := c.isPushout
