English
If J is cof interconnected (IsCofilteredOrEmpty J), then for any f : j ⟶ i, the map F.map f sends F.eventualRange j into F.eventualRange i.
Русский
Если J—кофильтрованный (IsCofilteredOrEmpty J), то для любого f : j ⟶ i отображение F.map f отправляет F.eventualRange j в F.eventualRange i.
LaTeX
$$$(F.map f)\;:\; F.eventualRange j \to F.eventualRange i$ maps each element of the eventual range at j into the eventual range at i.$$
Lean4
/-- The subfunctor of `F` obtained by restricting to the eventual range at each index. -/
@[simps]
def toEventualRanges : J ⥤ Type v where
obj j := F.eventualRange j
map f := (F.eventualRange_mapsTo f).restrict _ _ _
map_id
i := by
simp +unfoldPartialApp only [MapsTo.restrict, Subtype.map, F.map_id]
ext
rfl
map_comp _
_ := by
simp +unfoldPartialApp only [MapsTo.restrict, Subtype.map, F.map_comp]
rfl
