Documentation

Mathlib.Order.Sublocale

Sublocale #

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.

TODO #

Create separate definitions for sInf_mem and HImpClosed (also useful for CompleteSublattice)

References #

[J. Picada A. Pultr, Frames and Locales][picado2012]
https://ncatlab.org/nlab/show/sublocale
https://ncatlab.org/nlab/show/nucleus

structure Sublocale (X : Type u_2) [Order.Frame X] :

Type u_2

A sublocale of a locale X is a set S which is closed under all meets and such that x ⇨ s ∈ S for all x : X and s ∈ S.

Note that locales are the same thing as frames, but with reverse morphisms, which is why we assume Frame X. We only need to define locales categorically. See Locale.

carrier : Set X
The set corresponding to the sublocale.
sInf_mem' (s : Set X) : s ⊆ self.carrier → sInf s ∈ self.carrier
A sublocale is closed under all meets.
Do NOT use directly. Use Sublocale.sInf_mem instead.
himp_mem' (a b : X) : b ∈ self.carrier → a ⇨ b ∈ self.carrier
A sublocale is closed under heyting implication.
Do NOT use directly. Use Sublocale.himp_mem instead.

Instances For

instance Sublocale.instSetLike {X : Type u_1} [Order.Frame X] :

SetLike (Sublocale X) X

Equations

instance Sublocale.instPartialOrder {X : Type u_1} [Order.Frame X] :

PartialOrder (Sublocale X)

Equations

@[simp]

theorem Sublocale.mem_carrier {X : Type u_1} [Order.Frame X] {S : Sublocale X} {a : X} :

a ∈ S.carrier ↔ a ∈ S

@[simp]

theorem Sublocale.mem_mk {X : Type u_1} [Order.Frame X] {a : X} (carrier : Set X) (sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier) (himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier) :

a ∈ { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' } ↔ a ∈ carrier

@[simp]

theorem Sublocale.mk_le_mk {X : Type u_1} [Order.Frame X] (carrier₁ carrier₂ : Set X) (sInf_mem'₁ : ∀ s ⊆ carrier₁, sInf s ∈ carrier₁) (sInf_mem'₂ : ∀ s ⊆ carrier₂, sInf s ∈ carrier₂) (himp_mem'₁ : ∀ (a b : X), b ∈ carrier₁ → a ⇨ b ∈ carrier₁) (himp_mem'₂ : ∀ (a b : X), b ∈ carrier₂ → a ⇨ b ∈ carrier₂) :

{ carrier := carrier₁, sInf_mem' := sInf_mem'₁, himp_mem' := himp_mem'₁ } ≤ { carrier := carrier₂, sInf_mem' := sInf_mem'₂, himp_mem' := himp_mem'₂ } ↔ carrier₁ ⊆ carrier₂

theorem Sublocale.ext {X : Type u_1} [Order.Frame X] {S T : Sublocale X} (h : ∀ (x : X), x ∈ S ↔ x ∈ T) :

S = T

theorem Sublocale.ext_iff {X : Type u_1} [Order.Frame X] {S T : Sublocale X} :

S = T ↔ ∀ (x : X), x ∈ S ↔ x ∈ T

theorem Sublocale.sInf_mem {X : Type u_1} [Order.Frame X] {S : Sublocale X} {s : Set X} (hs : s ⊆ ↑S) :

theorem Sublocale.iInf_mem {X : Type u_1} [Order.Frame X] {ι : Sort u_2} {S : Sublocale X} {f : ι → X} (hf : ∀ (i : ι), f i ∈ S) :

⨅ (i : ι), f i ∈ S

theorem Sublocale.infClosed {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

theorem Sublocale.inf_mem {X : Type u_1} [Order.Frame X] {S : Sublocale X} {a b : X} (ha : a ∈ S) (hb : b ∈ S) :

a ⊓ b ∈ S

theorem Sublocale.top_mem {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

theorem Sublocale.himp_mem {X : Type u_1} [Order.Frame X] {S : Sublocale X} {a b : X} (hb : b ∈ S) :

a ⇨ b ∈ S

instance Sublocale.carrier.instSemilatticeInf {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

SemilatticeInf ↥S

Equations

instance Sublocale.carrier.instOrderTop {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

Equations

instance Sublocale.carrier.instHImp {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

HImp ↥S

Equations

instance Sublocale.carrier.instInfSet {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

Equations

@[simp]

theorem Sublocale.coe_inf {X : Type u_1} [Order.Frame X] {S : Sublocale X} (a b : ↥S) :

↑(a ⊓ b) = ↑a ⊓ ↑b

@[simp]

theorem Sublocale.coe_sInf {X : Type u_1} [Order.Frame X] {S : Sublocale X} (s : Set ↥S) :

↑(sInf s) = sInf (Subtype.val '' s)

@[simp]

theorem Sublocale.coe_iInf {X : Type u_1} [Order.Frame X] {ι : Sort u_2} {S : Sublocale X} (f : ι → ↥S) :

↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

instance Sublocale.carrier.instCompleteLattice {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

CompleteLattice ↥S

Equations

@[simp]

theorem Sublocale.coe_himp {X : Type u_1} [Order.Frame X] {S : Sublocale X} (a b : ↥S) :

↑(a ⇨ b) = ↑a ⇨ ↑b

instance Sublocale.carrier.instHeytingAlgebra {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

HeytingAlgebra ↥S

Equations

instance Sublocale.carrier.instFrame {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

Order.Frame ↥S

Equations

def Sublocale.restrict {X : Type u_1} [Order.Frame X] (S : Sublocale X) :

FrameHom X ↥S

The restriction from a locale X into the sublocale S.

Equations

Instances For

def Sublocale.giRestrict {X : Type u_1} [Order.Frame X] (S : Sublocale X) :

GaloisInsertion (⇑S.restrict) Subtype.val

The restriction corresponding to a sublocale forms a Galois insertion with the forgetful map from the sublocale to the original locale.

Equations

Instances For

@[simp]

theorem Sublocale.restrict_of_mem {X : Type u_1} [Order.Frame X] {S : Sublocale X} {a : X} (ha : a ∈ S) :

S.restrict a = ⟨a, ha⟩

def Sublocale.toNucleus {X : Type u_1} [Order.Frame X] (S : Sublocale X) :

The restriction from the locale X into a sublocale is a nucleus.

Equations

Instances For

@[simp]

theorem Sublocale.toNucleus_apply {X : Type u_1} [Order.Frame X] (S : Sublocale X) (x : X) :

S.toNucleus x = ↑(S.restrict x)

@[simp]

theorem Sublocale.range_toNucleus {X : Type u_1} [Order.Frame X] {S : Sublocale X} :

Set.range ⇑S.toNucleus = ↑S

@[simp]

theorem Sublocale.toNucleus_le_toNucleus {X : Type u_1} [Order.Frame X] {S T : Sublocale X} :

S.toNucleus ≤ T.toNucleus ↔ T ≤ S

def Nucleus.toSublocale {X : Type u_1} [Order.Frame X] (n : Nucleus X) :

The range of a nucleus is a sublocale.

Equations

Instances For

@[simp]

theorem Nucleus.coe_toSublocale {X : Type u_1} [Order.Frame X] (n : Nucleus X) :

↑n.toSublocale = Set.range ⇑n

@[simp]

theorem Nucleus.mem_toSublocale {X : Type u_1} [Order.Frame X] {n : Nucleus X} {x : X} :

x ∈ n.toSublocale ↔ ∃ (y : X), n y = x

@[simp]

theorem Nucleus.toSublocale_le_toSublocale {X : Type u_1} [Order.Frame X] {m n : Nucleus X} :

m.toSublocale ≤ n.toSublocale ↔ n ≤ m

@[simp]

theorem Nucleus.restrict_toSublocale {X : Type u_1} [Order.Frame X] (n : Nucleus X) (x : X) :

n.toSublocale.restrict x = ⟨n x, ⋯⟩

def nucleusIsoSublocale {X : Type u_1} [Order.Frame X] :

(Nucleus X)ᵒᵈ ≃o Sublocale X

The nuclei on a frame corresponds exactly to the sublocales on this frame. The sublocales are ordered dually to the nuclei.

Equations

Instances For

theorem nucleusIsoSublocale.eq_toSublocale {X : Type u_1} [Order.Frame X] :

Nucleus.toSublocale = ⇑nucleusIsoSublocale

theorem nucleusIsoSublocale.symm_eq_toNucleus {X : Type u_1} [Order.Frame X] :

Sublocale.toNucleus = ⇑nucleusIsoSublocale.symm

instance Sublocale.instCompleteLattice {X : Type u_1} [Order.Frame X] :

CompleteLattice (Sublocale X)

Equations

instance Sublocale.instCoframeMinimalAxioms {X : Type u_1} [Order.Frame X] :

Order.Coframe.MinimalAxioms (Sublocale X)

Equations

instance Sublocale.instCoframe {X : Type u_1} [Order.Frame X] :

Order.Coframe (Sublocale X)

Equations