functor — Mathlib

English

An inducing map f defines a functor from Opens X to Opens Y.

Русский

Индукциирующее отображение f задаёт функтор между открытыми множествами: Opens X → Opens Y.

LaTeX

$$$ \text{functor}_{hf}:\ Opens(X) \to Opens(Y).$$$

Lean4

/-- An inducing map `f : X ⟶ Y` induces a functor `Opens X ⥤ Opens Y`. -/
@[simps]
def functor {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) : Opens X ⥤ Opens Y
    where
  obj := hf.functorObj
  map {U V} h := homOfLE (hf.le_functorObj_iff.mpr ((hf.map_functorObj U).trans_le h.le))

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