functorObj — Mathlib

English

Given an inducing map f, the functor object construction on opens yields the largest open subset preimage containing U.

Русский

Дано индукцирующее отображение f, конструкция объектов функторов на открытых множествах дает наибольший открытый подмножество прообраза, содержащий U.

LaTeX

$$$ \text{functorObj: Opens(X)\to Opens(Y) with } U \mapsto \text{sup}\{s\in Opens(Y) : (Opens.map f).s = U\}. $$$

Lean4

/-- Given an inducing map `X ⟶ Y` and some `U : Opens X`, this is the union of all open sets
whose preimage is `U`. This is right adjoint to `Opens.map`. -/
@[nolint unusedArguments]
def functorObj {X Y : TopCat} {f : X ⟶ Y} (_ : IsInducing f) (U : Opens X) : Opens Y :=
  sSup {s : Opens Y | (Opens.map f).obj s = U}

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