Theorems · Definition · category theory
Locale.pt
CategoryTheory.Functor Locale TopCat
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.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement · cited by 16,252
- Opposite.unopproof · cited by 2,231
- TopCatstatement · cited by 1,889
- Quiver.Hom.unopproof · cited by 903
- TopCat.ofHomproof · cited by 44
- Frm.carrierproof · cited by 23
- FrameHom.compproof · cited by 10
- Frm.Hom.homproof · cited by 7
- Localestatement and proof · cited by 2
- Locale.PTproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- Locale.adjunctionTopToLocalePTstatement · cited by 0