Hull-Kernel Topology

Let α be a CompleteLattice and let T be a subset of α. The pair of maps S → sInf (Subtype.val '' S) and a → T ↓∩ Ici a are often referred to as the kernel and the hull respectively. They form an antitone Galois connection between the subsets of T and α. When α can be generated from T by taking infs, this becomes a Galois insertion and the relative topology (Topology.lower) on T takes on a particularly simple form: the relative-open sets are exactly the sets of the form (hull T a)ᶜ for some a in α. The topological closure coincides with the closure arising from the Galois insertion. For this reason the relative lower topology on T is often referred to as the "hull-kernel topology". The names "Jacobson topology" and "structure topology" also occur in the literature.

Main statements

• PrimitiveSpectrum.isTopologicalBasis_relativeLower - the sets (hull a)ᶜ form a basis for the relative lower topology on T.
• PrimitiveSpectrum.isOpen_iff - for a complete lattice, the sets (hull a)ᶜ are the relative topology.
• PrimitiveSpectrum.gc - the kernel and the hull form a Galois connection
• PrimitiveSpectrum.gi - when T generates α, the Galois connection becomes an insertion.

Implementation notes

The antitone Galois connection from Set T to α is implemented as a monotone Galois connection between Set T to αᵒᵈ.

Motivation

The motivating example for the study of a set T of prime elements which generate α is the primitive spectrum of the lattice of M-ideals of a Banach space.

References

• Gierz et al, A Compendium of Continuous Lattices
• Henriksen et al, Joincompact spaces, continuous lattices and C-algebras*

Tags

lower topology, hull-kernel topology, Jacobson topology, structure topology, primitive spectrum

@[reducible, inline]

abbrev PrimitiveSpectrum.hull {α : Type u_1} [SemilatticeInf α] (T : Set α) (a : α) : Set ↑T

For a of type α the set of element of T which dominate a is the hull of a in T.

Equations

• PrimitiveSpectrum.hull T a = Subtype.val ⁻¹' Set.Ici a

theorem PrimitiveSpectrum.hull_inf {α : Type u_1} [SemilatticeInf α] {T : Set α} (hT : ∀ p ∈ T, InfPrime p) (a b : α) : hull T (a ⊓ b) = hull T a ∪ hull T b

theorem PrimitiveSpectrum.hull_finsetInf {α : Type u_1} [SemilatticeInf α] {T : Set α} [DecidableEq α] [OrderTop α] (hT : ∀ p ∈ T, InfPrime p) (F : Finset α) : hull T (F.inf id) = Subtype.val ⁻¹' ↑(upperClosure ↑F)

theorem PrimitiveSpectrum.preimage_upperClosure_compl_finset {α : Type u_1} [SemilatticeInf α] {T : Set α} [DecidableEq α] [OrderTop α] (hT : ∀ p ∈ T, InfPrime p) (F : Finset α) : Subtype.val ⁻¹' (↑(upperClosure ↑F))ᶜ = (hull T (F.inf id))ᶜ

theorem PrimitiveSpectrum.isTopologicalBasis_relativeLower {α : Type u_1} [SemilatticeInf α] {T : Set α} [DecidableEq α] [OrderTop α] [TopologicalSpace α] [Topology.IsLower α] (hT : ∀ p ∈ T, InfPrime p) : TopologicalSpace.IsTopologicalBasis {S : Set ↑T | ∃ (a : α), (hull T a)ᶜ = S}

theorem PrimitiveSpectrum.hull_iSup {α : Type u_1} [CompleteLattice α] {T : Set α} {ι : Sort v} (s : ι → α) : hull T (iSup s) = ⋂ (i : ι), hull T (s i)

theorem PrimitiveSpectrum.hull_sSup {α : Type u_1} [CompleteLattice α] {T : Set α} (S : Set α) : hull T (sSup S) = ⋂₀ {x : Set ↑T | ∃ a ∈ S, hull T a = x}

theorem PrimitiveSpectrum.isOpen_iff {α : Type u_1} [CompleteLattice α] {T : Set α} [TopologicalSpace α] [Topology.IsLower α] [DecidableEq α] (hT : ∀ p ∈ T, InfPrime p) (S : Set ↑T) : IsOpen S ↔ ∃ (a : α), S = (hull T a)ᶜ

theorem PrimitiveSpectrum.isClosed_iff {α : Type u_1} [CompleteLattice α] {T : Set α} [TopologicalSpace α] [Topology.IsLower α] [DecidableEq α] (hT : ∀ p ∈ T, InfPrime p) {S : Set ↑T} : IsClosed S ↔ ∃ (a : α), S = hull T a

@[reducible, inline]

abbrev PrimitiveSpectrum.kernel {α : Type u_1} [CompleteLattice α] {T : Set α} (S : Set ↑T) : α

For a subset S of T, kernel S is the infimum of S (considered as a set of α)

Equations

• PrimitiveSpectrum.kernel S = sInf (Subtype.val '' S)

theorem PrimitiveSpectrum.gc {α : Type u_1} [CompleteLattice α] {T : Set α} : GaloisConnection (fun (S : Set ↑T) => OrderDual.toDual (kernel S)) fun (a : αᵒᵈ) => hull T (OrderDual.ofDual a)

theorem PrimitiveSpectrum.gc_closureOperator {α : Type u_1} [CompleteLattice α] {T : Set α} (S : Set ↑T) : ⋯.closureOperator S = hull T (kernel S)

def PrimitiveSpectrum.OrderGenerates {α : Type u_1} [CompleteLattice α] (T : Set α) : Prop

T order generates α if, for every a in α, there exists a subset of T such that a is the kernel of S.

Equations

• PrimitiveSpectrum.OrderGenerates T = ∀ (a : α), ∃ (S : Set ↑T), a = PrimitiveSpectrum.kernel S

def PrimitiveSpectrum.gi {α : Type u_1} [CompleteLattice α] {T : Set α} (hG : OrderGenerates T) : GaloisInsertion (⇑OrderDual.toDual ∘ kernel) (hull T ∘ ⇑OrderDual.ofDual)

When T is order generating, the kernel and the hull form a Galois insertion

Equations

• PrimitiveSpectrum.gi hG = ⋯.toGaloisInsertion ⋯

theorem PrimitiveSpectrum.kernel_hull {α : Type u_1} [CompleteLattice α] {T : Set α} (hG : OrderGenerates T) (a : α) : kernel (hull T a) = a

theorem PrimitiveSpectrum.hull_kernel_of_isClosed {α : Type u_1} [CompleteLattice α] {T : Set α} [TopologicalSpace α] [Topology.IsLower α] [DecidableEq α] (hT : ∀ p ∈ T, InfPrime p) (hG : OrderGenerates T) {C : Set ↑T} (h : IsClosed C) : hull T (kernel C) = C

theorem PrimitiveSpectrum.closedsGC_closureOperator {α : Type u_1} [CompleteLattice α] {T : Set α} [TopologicalSpace α] [Topology.IsLower α] [DecidableEq α] (hT : ∀ p ∈ T, InfPrime p) (hG : OrderGenerates T) (S : Set ↑T) : ⋯.closureOperator S = hull T (kernel S)