isStableUnderTransfiniteCompositionOfShape_llp

English

A second set of lift-related lemmas ensures that the lift construction is compatible with the functorial mapping along the index, yielding a coherent WellOrderInductionData structure.

Русский

Вторая серия лемм о лифтинге гарантирует совместимость конструкции лифта с отображениями функторного отображения по индексу, образуя когерентную структуру WellOrderInductionData.

LaTeX

$$$$ \text{lift}_{j} : (sqFunctor\ c\ p\ f\ g).obj( j ) \to X $$$$

Lean4

instance isStableUnderTransfiniteCompositionOfShape_llp : W.llp.IsStableUnderTransfiniteCompositionOfShape J :=
  by
  rw [isStableUnderTransfiniteCompositionOfShape_iff]
  rintro X Y f ⟨h⟩
  have : W.llp (h.incl.app ⊥) := fun _ _ p hp ↦
    HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot (hc := h.isColimit)
      (fun j hj ↦ h.map_mem j hj _ hp)
  exact (MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk h.isoBot.symm (Iso.refl _))).2 this

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