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. See nucleusIsoSublocale.

• toFun : X → X
• map_inf' (a b : X) : self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
• idempotent' (x : X) : self.toFun (self.toFun x) ≤ self.toFun x

  A nucleus is idempotent.

  Do not use this directly. Instead use NucleusClass.idempotent.

• le_apply' (x : X) : x ≤ self.toFun x

  A nucleus is increasing.

  Do not use this directly. Instead use NucleusClass.le_apply.

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

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

• map_inf (f : F) (a b : X) : f (a ⊓ b) = f a ⊓ f 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.

instance Nucleus.instFunLike {X : Type u_1} [SemilatticeInf X] : FunLike (Nucleus X) X X

def Nucleus.Simps.apply {X : Type u_1} [SemilatticeInf X] (n : Nucleus X) : X → X

See Note [custom simps projection]

@[simp]

theorem Nucleus.toFun_eq_coe {X : Type u_1} [SemilatticeInf X] (n : Nucleus X) : n.toFun = ⇑n

@[simp]

theorem Nucleus.coe_toInfHom {X : Type u_1} [SemilatticeInf X] (n : Nucleus X) : ⇑n.toInfHom = ⇑n

@[simp]

theorem Nucleus.coe_mk {X : Type u_1} [SemilatticeInf 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

instance Nucleus.instNucleusClass {X : Type u_1} [SemilatticeInf X] : NucleusClass (Nucleus X) X

def Nucleus.toClosureOperator {X : Type u_1} [SemilatticeInf X] (n : Nucleus X) : ClosureOperator X

Every nucleus is a ClosureOperator.

@[simp]

theorem Nucleus.idempotent {X : Type u_1} [SemilatticeInf X] {n : Nucleus X} (x : X) : n (n x) = n x

theorem Nucleus.le_apply {X : Type u_1} [SemilatticeInf X] {n : Nucleus X} {x : X} : x ≤ n x

theorem Nucleus.monotone {X : Type u_1} [SemilatticeInf X] {n : Nucleus X} : Monotone ⇑n

theorem Nucleus.map_inf {X : Type u_1} [SemilatticeInf X] {n : Nucleus X} {x y : X} : n (x ⊓ y) = n x ⊓ n y

theorem Nucleus.ext {X : Type u_1} [SemilatticeInf X] {m n : Nucleus X} (h : ∀ (a : X), m a = n a) : m = n

theorem Nucleus.ext_iff {X : Type u_1} [SemilatticeInf X] {m n : Nucleus X} : m = n ↔ ∀ (a : X), m a = n a

instance Nucleus.instPartialOrder {X : Type u_1} [SemilatticeInf X] : PartialOrder (Nucleus X)

@[simp]

theorem Nucleus.coe_le_coe {X : Type u_1} [SemilatticeInf X] {n m : Nucleus X} : ⇑m ≤ ⇑n ↔ m ≤ n

@[simp]

theorem Nucleus.coe_lt_coe {X : Type u_1} [SemilatticeInf X] {n m : Nucleus X} : ⇑m < ⇑n ↔ m < n

@[simp]

theorem Nucleus.mk_le_mk {X : Type u_1} [SemilatticeInf X] (toInfHom₁ toInfHom₂ : InfHom X X) (le_apply₁ : ∀ (x : X), toInfHom₁.toFun (toInfHom₁.toFun x) ≤ toInfHom₁.toFun x) (le_apply₂ : ∀ (x : X), toInfHom₂.toFun (toInfHom₂.toFun x) ≤ toInfHom₂.toFun x) (idempotent₁ : ∀ (x : X), x ≤ toInfHom₁.toFun x) (idempotent₂ : ∀ (x : X), x ≤ toInfHom₂.toFun x) : { toInfHom := toInfHom₁, idempotent' := le_apply₁, le_apply' := idempotent₁ } ≤ { toInfHom := toInfHom₂, idempotent' := le_apply₂, le_apply' := idempotent₂ } ↔ toInfHom₁ ≤ toInfHom₂

theorem GCongr.Nucleus.mk_le_mk {X : Type u_1} [SemilatticeInf X] (toInfHom₁ toInfHom₂ : InfHom X X) (le_apply₁ : ∀ (x : X), toInfHom₁.toFun (toInfHom₁.toFun x) ≤ toInfHom₁.toFun x) (le_apply₂ : ∀ (x : X), toInfHom₂.toFun (toInfHom₂.toFun x) ≤ toInfHom₂.toFun x) (idempotent₁ : ∀ (x : X), x ≤ toInfHom₁.toFun x) (idempotent₂ : ∀ (x : X), x ≤ toInfHom₂.toFun x) : toInfHom₁ ≤ toInfHom₂ → { toInfHom := toInfHom₁, idempotent' := le_apply₁, le_apply' := idempotent₁ } ≤ { toInfHom := toInfHom₂, idempotent' := le_apply₂, le_apply' := idempotent₂ }

Alias of the reverse direction of Nucleus.mk_le_mk.

instance Nucleus.instMin {X : Type u_1} [SemilatticeInf X] : Min (Nucleus X)

@[simp]

theorem Nucleus.coe_inf {X : Type u_1} [SemilatticeInf X] (m n : Nucleus X) : ⇑(m ⊓ n) = ⇑m ⊓ ⇑n

@[simp]

theorem Nucleus.inf_apply {X : Type u_1} [SemilatticeInf X] (m n : Nucleus X) (x : X) : (m ⊓ n) x = m x ⊓ n x

instance Nucleus.instSemilatticeInf {X : Type u_1} [SemilatticeInf X] : SemilatticeInf (Nucleus X)

instance Nucleus.instBot {X : Type u_1} [SemilatticeInf X] : OrderBot (Nucleus X)

The smallest nucleus is the identity.

@[simp]

theorem Nucleus.coe_bot {X : Type u_1} [SemilatticeInf X] : ⇑⊥ = id

@[simp]

theorem Nucleus.bot_apply {X : Type u_1} [SemilatticeInf X] (x : X) : ⊥ x = x

instance Nucleus.instTopHomClass {X : Type u_1} [SemilatticeInf X] [OrderTop X] : TopHomClass (Nucleus X) X X

A nucleus preserves ⊤.

instance Nucleus.instTop {X : Type u_1} [SemilatticeInf X] [OrderTop X] : Top (Nucleus X)

The largest nucleus sends everything to ⊤.

@[simp]

theorem Nucleus.coe_top {X : Type u_1} [SemilatticeInf X] [OrderTop X] : ⇑⊤ = ⊤

@[simp]

theorem Nucleus.top_apply {X : Type u_1} [SemilatticeInf X] [OrderTop X] (x : X) : ⊤ x = ⊤

instance Nucleus.instBoundedOrder {X : Type u_1} [SemilatticeInf X] [OrderTop X] : BoundedOrder (Nucleus X)

instance Nucleus.instInfSet {X : Type u_1} [CompleteLattice X] : InfSet (Nucleus X)

@[simp]

theorem Nucleus.sInf_apply {X : Type u_1} [CompleteLattice X] (s : Set (Nucleus X)) (x : X) : (sInf s) x = ⨅ j ∈ s, 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

instance Nucleus.instCompleteSemilatticeInf {X : Type u_1} [CompleteLattice X] : CompleteSemilatticeInf (Nucleus X)

instance Nucleus.instCompleteLattice {X : Type u_1} [CompleteLattice X] : CompleteLattice (Nucleus 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] : HImp (Nucleus X)

@[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

instance Nucleus.instHeytingAlgebra {X : Type u_1} [Order.Frame X] : HeytingAlgebra (Nucleus X)

instance Nucleus.instFrame {X : Type u_1} [Order.Frame X] : Order.Frame (Nucleus X)

theorem Nucleus.mem_range {X : Type u_1} [Order.Frame X] {n : Nucleus X} {x : X} : x ∈ Set.range ⇑n ↔ n x = x

instance Nucleus.instCompleteLatticeElemRangeCoe {X : Type u_1} [Order.Frame X] {n : Nucleus X} : CompleteLattice ↑(Set.range ⇑n)

instance Nucleus.range.instFrameMinimalAxioms {X : Type u_1} [Order.Frame X] {n : Nucleus X} : Order.Frame.MinimalAxioms ↑(Set.range ⇑n)

instance Nucleus.instFrameElemRangeCoe {X : Type u_1} [Order.Frame X] {n : Nucleus X} : Order.Frame ↑(Set.range ⇑n)

def Nucleus.restrict {X : Type u_1} [Order.Frame X] (n : Nucleus X) : FrameHom X ↑(Set.range ⇑n)

Restrict a nucleus to its range.

@[simp]

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

def Nucleus.giRestrict {X : Type u_1} [Order.Frame X] (n : Nucleus X) : GaloisInsertion (⇑n.restrict) Subtype.val

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

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