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

Equations

• Nucleus.instFunLike = { coe := fun (x : Nucleus X) => x.toFun, coe_injective' := ⋯ }

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

See Note [custom simps projection]

Equations

• Nucleus.Simps.apply n = ⇑n

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

Equations

• n.toClosureOperator = ClosureOperator.mk' ⇑n ⋯ ⋯ ⋯

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

Equations

• Nucleus.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯

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

Equations

• Nucleus.instMin = { min := fun (m n : Nucleus X) => { toFun := ⇑m ⊓ ⇑n, map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ } }

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

Equations

• Nucleus.instSemilatticeInf = Function.Injective.semilatticeInf (fun (f : Nucleus X) => ⇑f) ⋯ ⋯

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

The smallest nucleus is the identity.

Equations

• Nucleus.instBot = { bot := { toFun := fun (x : X) => x, map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ }, bot_le := ⋯ }

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

Equations

• Nucleus.instTop = { top := { toFun := ⊤, map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ } }

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

Equations

• Nucleus.instBoundedOrder = { toTop := Nucleus.instTop, le_top := ⋯, toBot := Nucleus.instBot.toBot, bot_le := ⋯ }

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

Equations

• Nucleus.instInfSet = { sInf := fun (s : Set (Nucleus X)) => { toFun := fun (x : X) => ⨅ f ∈ s, f x, map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ } }

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

Equations

• Nucleus.instCompleteSemilatticeInf = { toPartialOrder := Nucleus.instPartialOrder, toInfSet := Nucleus.instInfSet, sInf_le := ⋯, le_sInf := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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)

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Equations

• Nucleus.instCompleteLatticeElemRangeCoe = (Nucleus.giAux✝ n).liftCompleteLattice

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

Equations

• Nucleus.range.instFrameMinimalAxioms = { toCompleteLattice := Nucleus.instCompleteLatticeElemRangeCoe, inf_sSup_le_iSup_inf := ⋯ }

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

Equations

• Nucleus.instFrameElemRangeCoe = Order.Frame.ofMinimalAxioms Nucleus.range.instFrameMinimalAxioms

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

• n.restrict = { toFun := Set.rangeFactorization ⇑n, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }

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

Equations

• n.giRestrict = Nucleus.giAux✝ n

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