English
The successor structure's morphism property is subordinate to the arrow-property structure in Arrow C; formally, (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow C).
Русский
Свойство морфизма структуры-последовательности подчинено свойству стрелки в Arrow C; именно (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow C).
LaTeX
$$$\\bigl((\\text{succStruct}\\;I\\;\\kappa).\\text{prop}\\bigr) \\le \\bigl(\\text{propArrow}\\;I\\bigr).\\text{functorCategory}(\\mathrm{Arrow}(C))$$$
Lean4
theorem succStruct_prop_le_propArrow : (succStruct I κ).prop ≤ (propArrow.{w} I).functorCategory (Arrow C) :=
by
haveI := locallySmall I κ
haveI := isSmall I κ
haveI := hasColimitsOfShape_discrete I κ
haveI := hasPushouts I κ
intro _ _ _ ⟨F⟩ f
constructor
· nth_rw 1 [← I.ofHoms_homFamily]
apply pushouts_mk _ (functorObj_isPushout I.homFamily (F.obj f).hom)
exact coproducts_of_small _ _ (colimitsOfShape_colimMap _ (by rintro ⟨j⟩; constructor))
· rw [MorphismProperty.isomorphisms.iff]
dsimp [succStruct]
infer_instance
