Commit 2023-10-21 09:35 21c7184c

View on Github →

feat: Adjunction between topological spaces and locales (#4593) We define the contravariant functors between the categories of Frames and Topological Spaces and prove that they form an adjunction. Work started at the BIRS workshop "Formalization of Cohomology Theories", Banff, May 2023.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.setOf_bot

added theorem Set.setOf_top

Created Mathlib/Topology/Order/Category/FrameAdjunction.lean

added theorem Locale.PT.isOpen_iff

added def Locale.PT

added def Locale.adjunctionTopToLocalePT

added def Locale.counitAppCont

added def Locale.localePointOfSpacePoint

added def Locale.openOfElementHom

added def Locale.pt

Modified Mathlib/Topology/Sets/Opens.lean

added theorem TopologicalSpace.Opens.mk_empty

added theorem TopologicalSpace.Opens.mk_univ

Modified docs/references.bib