pt

Mathlib.Topology.Order.Category.FrameAdjunction

URI: https://scilib.ai/kg/mathlib#Locale.pt

Lean4

/-- The covariant functor `pt` from the category of locales to the category of
topological spaces, which sends a locale `L` to the topological space `PT L` of homomorphisms
from `L` to `Prop` and a locale homomorphism `f` to a continuous function between the spaces
of points. -/
def pt : Locale ⥤ TopCat where
  obj L := .of (PT L.unop)
  map f := TopCat.ofHom ⟨fun p ↦ p.comp f.unop.hom, continuous_def.2 <| by rintro s ⟨u, rfl⟩; use f.unop u; rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru