relativeCellComplexιObj — Mathlib

English

The transfinite composition of shape ιObj along κ exists for the small object factorization; i.e., the tower built via ιObj admits a well-defined transfinite composition.

Русский

Существует трансфинитная композиция формы ιObj вдоль κ для факторизации малого объекта; башня, построенная через ιObj, имеет корректную трансфинитную композицию.

LaTeX

$$$\\text{transfiniteCompositionsOfShape}_{\\mathrm{ιObj}}(I,\\kappa) : \\mathrm{HasTransfiniteComposition}$$$

Lean4

/-- The morphism `ιObj I κ f` is a relative `I`-cell complex. -/
noncomputable def relativeCellComplexιObj :
    RelativeCellComplex.{w} (fun (_ : κ.ord.toType) ↦ I.homFamily) (ιObj I κ f) :=
  by
  have := hasIterationOfShape I κ
  let h := transfiniteCompositionOfShapeSuccStructPropιIteration I κ
  exact
    { toTransfiniteCompositionOfShape := h.toTransfiniteCompositionOfShape.map ((evaluation _ _).obj f ⋙ Arrow.leftFunc)
      attachCells j hj := attachCellsOfSuccStructProp I κ (h.map_mem j hj) f }

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