English
For a fixed index i and a subset s ⊆ F.obj i, the subfunctor F.toPreimages s is defined by taking at each j the intersection over all arrows f : j ⟶ i of the preimages F.map f^{-1}(s), with maps given by restricting F.map g to these intersections.
Русский
Для фиксированного индекса i и подмножества s ⊆ F.obj i, подфунктор F.toPreimages s задаётся через пересечение по всем стрелкам f : j ⟶ i предобразов s; отображения задаются ограничением F.map g на эти пересечения.
LaTeX
$$$\text{toPreimages } s : J ⥤ Type\ v$, где\n\quad (\text{obj } j) = \bigcap_{f : j \to i} F.map f^{-1}(s)$,\nи отображение по g является ограничением соответствующих отображений.$$
Lean4
/-- The subfunctor of `F` obtained by restricting to the preimages of a set `s ∈ F.obj i`. -/
@[simps]
def toPreimages : J ⥤ Type v where
obj j := ⋂ f : j ⟶ i, F.map f ⁻¹' s
map
g :=
MapsTo.restrict (F.map g) _ _ fun x h => by
rw [mem_iInter] at h ⊢
intro f
rw [← mem_preimage, preimage_preimage, mem_preimage]
convert h (g ≫ f); rw [F.map_comp]; rfl
map_id
j := by
simp +unfoldPartialApp only [MapsTo.restrict, Subtype.map, F.map_id]
ext
rfl
map_comp f
g := by
simp +unfoldPartialApp only [MapsTo.restrict, Subtype.map, F.map_comp]
rfl
