iic — Mathlib

English

If G is a ComposableArrows C n, then the composite arrow G.hom is a transfinite composition of shape Fin(n+1).

Русский

Если G является ComposableArrows C n, то композиция стрел G.hom является трансфинитной композицией формы Fin(n+1).

LaTeX

$$$\text{TransfiniteCompositionOfShape}(\text{Fin} (n+1), G.hom)$$$

Lean4

/-- A transfinite composition of shape `J` induces a transfinite composition
of shape `Set.Iic j` for any `j : J`. -/
@[simps]
noncomputable def iic (j : J) : TransfiniteCompositionOfShape (Set.Iic j) (c.F.map (homOfLE bot_le : ⊥ ⟶ j))
    where
  F := (Set.initialSegIic j).monotone.functor ⋙ c.F
  isoBot := Iso.refl _
  incl :=
    { app i := c.F.map (homOfLE i.2)
      naturality i i'
        φ := by
        dsimp
        rw [← Functor.map_comp, Category.comp_id]
        rfl }
  isColimit := colimitOfDiagramTerminal isTerminalTop _

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