principals — Mathlib

English

There exists a contravariant functor princip als: X → Opens(X) to the opposite category, with princip als(x) = principalOpen(x).

Русский

Существует контравариантный функтор princip als: X → Opens(X)ᵒᵖ, заданный princip als(х) = principalOpen(х).

LaTeX

$$$\mathrm{principals}: X \to \mathrm{Opens}(X)^{\mathrm{op}}\quad \text{defined by } \mathrm{principals}(x) = \operatorname{principalOpen}(x)\;\text{and the action on morphisms is inclusion.}$$$

Lean4

/-- The functor sending `x : X` to the principal open associated with `x`. -/
@[simps]
def principals : X ⥤ (Opens X)ᵒᵖ where
  obj x := .op <| principalOpen x
  map {x y} f := .op <| principalOpen_le f.le |>.hom

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