transfiniteCompositionOfShape — Mathlib

English

Reiterates that a relative cell complex can be expressed as a transfinite composition of pushouts of coproducts over a shape J.

Русский

Повторяет, что относительный клеточный комплекс может быть выражен как трансфинитная композиция пушаутов копроподс по форме J.

LaTeX

$$$\text{transfiniteCompositionOfShape}$$$

Lean4

/-- If `f` is a relative cell complex with respect to a constant
family of morphisms `g`, then `f` is a transfinite composition
of pushouts of coproducts of morphisms in the family `g`. -/
@[simps toTransfiniteCompositionOfShape]
def transfiniteCompositionOfShape {α : Type*} {A B : α → C} (g : (i : α) → (A i ⟶ B i))
    (c : RelativeCellComplex.{w} (fun (_ : J) ↦ g) f) :
    (coproducts.{w} (ofHoms g)).pushouts.TransfiniteCompositionOfShape J f
    where
  toTransfiniteCompositionOfShape := c.toTransfiniteCompositionOfShape
  map_mem j hj := (c.attachCells j hj).pushouts_coproducts

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