Nucleus #
Locales are the dual concept to frames. Locale theory is a branch of point-free topology, where intuitively locales are like topological spaces which may or may not have enough points. Sublocales of a locale generalize the concept of subspaces in topology to the point-free setting.
A nucleus is an endomorphism of a frame which corresponds to a sublocale.
References #
https://ncatlab.org/nlab/show/sublocale https://ncatlab.org/nlab/show/nucleus
A nucleus is an inflationary idempotent inf
-preserving endomorphism of a semilattice.
In a frame, nuclei correspond to sublocales.
- toFun : X → X
A
Nucleus
is idempotent.Do not use this directly. Instead use
NucleusClass.idempotent
.A
Nucleus
is increasing.Do not use this directly. Instead use
NucleusClass.le_apply
.
Instances For
NucleusClass F X
states that F is a type of nuclei.
A nucleus is idempotent.
A nucleus is inflationary.
Instances
Every Nucleus
is a ClosureOperator
.
Equations
- n.toClosureOperator = ClosureOperator.mk' ⇑n ⋯ ⋯ ⋯
Instances For
A Nucleus
preserves ⊤.
Equations
The smallest Nucleus
is the identity.
The biggest Nucleus
sends everything to ⊤
.
Equations
- Nucleus.instBoundedOrder = { toTop := Nucleus.instTop, le_top := ⋯, toBot := Nucleus.instBot, bot_le := ⋯ }
Equations
- Nucleus.instCompleteSemilatticeInf = { toPartialOrder := Nucleus.instPartialOrder, toInfSet := Nucleus.instInfSet, sInf_le := ⋯, le_sInf := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Nucleus.range.instFrameMinimalAxioms = { toCompleteLattice := Nucleus.instCompleteLatticeElemRangeCoe, inf_sSup_le_iSup_inf := ⋯ }
Restrict a nucleus to its range.
Equations
- n.restrict = { toFun := Set.rangeFactorization ⇑n, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }
Instances For
The restriction of a nucleus to its range forms a Galois insertion with the forgetful map from the range to the original frame.