opensFunctor — Mathlib

English

Given an open immersion f: X → Y, there is a functor Opens X ⥤ Opens Y sending an open set U ⊆ X to its image under f.

Русский

При открытом погружении f: X → Y существует функтор Opens X ⥤ Opens Y, отправляющий открытое множество U ⊆ X в образ f(U).

LaTeX

$$$ Opens X \to Opens Y \text{ induced by } f$$$

Lean4

/-- The functor `Opens X ⥤ Opens Y` associated with an open immersion `f : X ⟶ Y`. -/
abbrev opensFunctor {X Y : LocallyRingedSpace} (f : X ⟶ Y) [H : LocallyRingedSpace.IsOpenImmersion f] :
    Opens X ⥤ Opens Y :=
  H.base_open.isOpenMap.functor

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