opensFunctor — Mathlib

English

The opensFunctor is a functor that sends an open subset of X to the corresponding open subset of Y under an open immersion f: X → Y.

Русский

opensFunctor — это функтор, отправляющий открытое подмножество X в соответствующее подмножество Y по открытым вложениям f: X → Y.

LaTeX

$$$\\text{opensFunctor} : X.{\\text{Opens}} ⥤ Y.{\\text{Opens}}$$$

Lean4

/-- The functor `opens X ⥤ opens Y` associated with an open immersion `f : X ⟶ Y`. -/
abbrev opensFunctor : X.Opens ⥤ Y.Opens :=
  LocallyRingedSpace.IsOpenImmersion.opensFunctor f.toLRSHom

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