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.

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

@[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 GCongr.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₂ → { carrier := carrier₁, sInf_mem' := sInf_mem'₁, himp_mem' := himp_mem'₁ } ≤ { carrier := carrier₂, sInf_mem' := sInf_mem'₂, himp_mem' := himp_mem'₂ }

Alias of the reverse direction of Sublocale.mk_le_mk.

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) : sInf 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} : InfClosed ↑S

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} : ⊤ ∈ S

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

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

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

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

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

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

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

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.

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.

@[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) : Nucleus X

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

@[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) : Sublocale X

The range of a nucleus is a sublocale.

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

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

Alias of the reverse direction of Nucleus.toSublocale_le_toSublocale.

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

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)

instance Sublocale.instCoframeMinimalAxioms {X : Type u_1} [Order.Frame X] : Order.Coframe.MinimalAxioms (Sublocale X)

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