English
For any index j, the map from the bottom object to j along the generating family is a transfinite composition of pushouts of monomorphisms in the generating family of G.
Русский
Для любого индекса j отображение от нулевого объекта к j по порождающей семье является трансфинитной композицией pushouts мономорфизмов из порождающей семьи G.
LaTeX
$$$\\forall j,\\; (\\text{bot} \\to j)\\text{ is a TransfiniteCompositionOfShape of pushouts of monomorphisms in }\\langle G \\rangle$$$
Lean4
/-- For any `j`, the map `(functor hG A₀ J).map (homOfLE bot_le : ⊥ ⟶ j)`
is a transfinite composition of pushouts of monomorphisms in the
family `generatingMonomorphisms G`. -/
noncomputable def transfiniteCompositionOfShapeMapFromBot (j : J) :
(generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (Set.Iic j)
((functor hG A₀ J).map (homOfLE bot_le : ⊥ ⟶ j))
where
F := (Set.initialSegIic j).monotone.functor ⋙ functor hG A₀ J
isoBot := Iso.refl _
incl :=
{ app k := (functor hG A₀ J).map (homOfLE k.2)
naturality k k' h := by simp [MonoOver.forget] }
isColimit := colimitOfDiagramTerminal isTerminalTop _
map_mem k
hk := by
dsimp [MonoOver.forget]
convert pushouts_ofLE_le_largerSubobject hG (transfiniteIterate (largerSubobject hG) k.1 A₀) using 2
all_goals rw [Set.Iic.succ_eq_of_not_isMax hk, transfiniteIterate_succ _ _ _ (Set.not_isMax_coe _ hk)]
