transfiniteCompositionOfShapeιIteration

English

The inclusion ιIteration J is a transfinite composition of shape J of morphisms in Φ.prop.

Русский

Включение ιIteration J является трансфинитной композицией формы J из морфизмов в Φ.prop.

LaTeX

$$$Φ.prop.TransfiniteCompositionOfShape J (Φ.ιIteration J)$$$

Lean4

/-- The inclusion `Φ.ιIteration J` is a transfinite composition of
shape `J` of morphisms in `Φ.prop`. -/
@[simps]
noncomputable def transfiniteCompositionOfShapeιIteration : Φ.prop.TransfiniteCompositionOfShape J (Φ.ιIteration J)
    where
  isoBot := Φ.iterationFunctorObjBotIso J
  map_mem j
    hj := by
    have := (Φ.iter (Order.succ j)).prop_map_succ j (Order.lt_succ_of_not_isMax hj)
    rw [prop_iff] at this ⊢
    simp only [Φ.iterationFunctor_obj j (Φ.iter (Order.succ j)) (Order.le_succ j),
      Φ.arrowMk_iterationFunctor_map _ _ (Order.le_succ j) (Φ.iter (Order.succ j)) (by simp), this]
  F := Φ.iterationFunctor J
  incl := (Φ.iterationCocone J).ι
  isColimit := Φ.isColimitIterationCocone J

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