toTopCat — Mathlib

English

There is a canonical functor from the lattice of open sets of X to TopCat that sends each open set to the corresponding subspace, with maps given by restriction.

Русский

Существует канонический функтор из множества открытых подмножеств X в TopCat, отображающий каждое открытое множество в соответствующее подпространство, а отображения — через ограничение.

LaTeX

$$toTopCat(X) : Opens(X) ⥤ TopCat$$

Lean4

/-- The functor from open sets in `X` to `TopCat`,
realising each open set as a topological space itself.
-/
def toTopCat (X : TopCat.{u}) : Opens X ⥤ TopCat
    where
  obj U := TopCat.of U
  map i := TopCat.ofHom ⟨fun x ↦ ⟨x.1, i.le x.2⟩, IsEmbedding.subtypeVal.continuous_iff.2 continuous_induced_dom⟩

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