Documentation

Mathlib.Order.Nucleus

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

structure Nucleus (X : Type u_2) [SemilatticeInf X] extends InfHom X X :
Type u_2

A nucleus is an inflationary idempotent inf-preserving endomorphism of a semilattice. In a frame, nuclei correspond to sublocales.

class NucleusClass (F : Type u_2) (X : Type u_3) [SemilatticeInf X] [FunLike F X X] extends InfHomClass F X X :

NucleusClass F X states that F is a type of nuclei.

  • map_inf (f : F) (a b : X) : f (ab) = f af b
  • idempotent (x : X) (f : F) : f (f x) f x

    A nucleus is idempotent.

  • le_apply (x : X) (f : F) : x f x

    A nucleus is inflationary.

Instances
    instance Nucleus.instFunLike {X : Type u_1} [CompleteLattice X] :
    Equations
    theorem Nucleus.toFun_eq_coe {X : Type u_1} [CompleteLattice X] (n : Nucleus X) :
    n.toFun = n
    @[simp]
    theorem Nucleus.coe_toInfHom {X : Type u_1} [CompleteLattice X] (n : Nucleus X) :
    n.toInfHom = n
    @[simp]
    theorem Nucleus.coe_mk {X : Type u_1} [CompleteLattice X] (f : InfHom X X) (h1 : ∀ (x : X), f.toFun (f.toFun x) f.toFun x) (h2 : ∀ (x : X), x f.toFun x) :
    { toInfHom := f, idempotent' := h1, le_apply' := h2 } = f
    theorem Nucleus.idempotent {X : Type u_1} [CompleteLattice X] {n : Nucleus X} {x : X} :
    n (n x) = n x
    theorem Nucleus.le_apply {X : Type u_1} [CompleteLattice X] {n : Nucleus X} {x : X} :
    x n x
    theorem Nucleus.monotone {X : Type u_1} [CompleteLattice X] {n : Nucleus X} :
    theorem Nucleus.map_inf {X : Type u_1} [CompleteLattice X] {n : Nucleus X} {x y : X} :
    n (xy) = n xn y
    theorem Nucleus.ext {X : Type u_1} [CompleteLattice X] {m n : Nucleus X} (h : ∀ (a : X), m a = n a) :
    m = n
    theorem Nucleus.ext_iff {X : Type u_1} [CompleteLattice X] {m n : Nucleus X} :
    m = n ∀ (a : X), m a = n a

    A Nucleus preserves ⊤.

    @[simp]
    theorem Nucleus.coe_le_coe {X : Type u_1} [CompleteLattice X] {n m : Nucleus X} :
    m n m n
    @[simp]
    theorem Nucleus.coe_lt_coe {X : Type u_1} [CompleteLattice X] {n m : Nucleus X} :
    m < n m < n
    instance Nucleus.instBot {X : Type u_1} [CompleteLattice X] :

    The smallest Nucleus is the identity.

    Equations
    • Nucleus.instBot = { bot := { toFun := fun (x : X) => x, map_inf' := , idempotent' := , le_apply' := } }
    instance Nucleus.instTop {X : Type u_1} [CompleteLattice X] :

    The biggest Nucleus sends everything to .

    Equations
    @[simp]
    theorem Nucleus.coe_bot {X : Type u_1} [CompleteLattice X] :
    = id
    @[simp]
    theorem Nucleus.coe_top {X : Type u_1} [CompleteLattice X] :
    =
    @[simp]
    theorem Nucleus.bot_apply {X : Type u_1} [CompleteLattice X] (x : X) :
    x = x
    @[simp]
    theorem Nucleus.top_apply {X : Type u_1} [CompleteLattice X] (x : X) :
    Equations
    Equations
    @[simp]
    theorem Nucleus.sInf_apply {X : Type u_1} [CompleteLattice X] (s : Set (Nucleus X)) (x : X) :
    (sInf s) x = js, j x
    @[simp]
    theorem Nucleus.iInf_apply {X : Type u_1} [CompleteLattice X] {ι : Type u_2} (f : ιNucleus X) (x : X) :
    (iInf f) x = ⨅ (j : ι), (f j) x
    @[simp]
    theorem Nucleus.inf_apply {X : Type u_1} [CompleteLattice X] (m n : Nucleus X) (x : X) :
    (mn) x = m xn x
    theorem Nucleus.map_himp_le {X : Type u_1} [Order.Frame X] {n : Nucleus X} {x y : X} :
    n (x y) x n y
    theorem Nucleus.map_himp_apply {X : Type u_1} [Order.Frame X] (n : Nucleus X) (x y : X) :
    n (x n y) = x n y
    instance Nucleus.instHImp {X : Type u_1} [Order.Frame X] :
    Equations
    • Nucleus.instHImp = { himp := fun (m n : Nucleus X) => { toFun := fun (x : X) => ⨅ (y : X), ⨅ (_ : y x), m y n y, map_inf' := , idempotent' := , le_apply' := } }
    @[simp]
    theorem Nucleus.himp_apply {X : Type u_1} [Order.Frame X] (m n : Nucleus X) (x : X) :
    (m n) x = ⨅ (y : X), ⨅ (_ : y x), m y n y
    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.
    theorem Nucleus.mem_range {X : Type u_1} [Order.Frame X] {n : Nucleus X} {x : X} :
    x Set.range n n x = x
    def Nucleus.restrict {X : Type u_1} [Order.Frame X] (n : Nucleus X) :
    FrameHom X (Set.range n)

    Restrict a nucleus to its range.

    Equations
    @[simp]
    theorem Nucleus.restrict_toFun {X : Type u_1} [Order.Frame X] (n : Nucleus X) (a✝ : X) :
    n.restrict a✝ = Set.rangeFactorization (⇑n) a✝

    The restriction of a nucleus to its range forms a Galois insertion with the forgetful map from the range to the original frame.

    Equations
    theorem Nucleus.comp_eq_right_iff_le {X : Type u_1} [Order.Frame X] {n m : Nucleus X} :
    n m = m n m
    @[simp]
    theorem Nucleus.range_subset_range {X : Type u_1} [Order.Frame X] {n m : Nucleus X} :
    Set.range m Set.range n n m