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 #

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

Sublocale.instSetLike = { coe := fun (x : Sublocale X) => x.carrier, coe_injective' := ⋯ }

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

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

Sublocale.carrier.instSemilatticeInf = Subtype.semilatticeInf ⋯

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

Equations

Sublocale.carrier.instOrderTop = Subtype.orderTop ⋯

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

HImp ↥S

Equations

Sublocale.carrier.instHImp = { himp := fun (a b : ↥S) => ⟨↑a ⇨ ↑b, ⋯⟩ }

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

Equations

Sublocale.carrier.instInfSet = { sInf := fun (x : Set ↥S) => ⟨sInf (Subtype.val '' x), ⋯⟩ }

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

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

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

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

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

Order.Frame ↥S

Equations

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

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

S.restrict = { toFun := fun (x : X) => sInf {s : ↥S | x ≤ ↑s}, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }

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

S.giRestrict = Sublocale.giAux✝ S

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

S.toNucleus = { toFun := fun (x : X) => ↑(S.restrict x), map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ }

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

n.toSublocale = { carrier := Set.range ⇑n, sInf_mem' := ⋯, himp_mem' := ⋯ }

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

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.

Equations

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

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

Sublocale.instCompleteLattice = nucleusIsoSublocale.toGaloisInsertion.liftCompleteLattice

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

Order.Coframe.MinimalAxioms (Sublocale X)

Equations

Sublocale.instCoframeMinimalAxioms = { toCompleteLattice := Sublocale.instCompleteLattice, iInf_sup_le_sup_sInf := ⋯ }

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

Order.Coframe (Sublocale X)

Equations

Sublocale.instCoframe = Order.Coframe.ofMinimalAxioms Sublocale.instCoframeMinimalAxioms