Generators for Boolean algebras

In this file, we provide an alternative constructor for Boolean algebras.

A set of Boolean generators in a compactly generated complete lattice is a subset S such that

• the elements of S are all atoms, and
• the set S satisfies an atomicity condition: any compact element below the supremum of a subset s of generators is equal to the supremum of a subset of s.

Main declarations

• IsCompactlyGenerated.BooleanGenerators: the predicate described above.
• IsCompactlyGenerated.BooleanGenerators.complementedLattice_of_sSup_eq_top: if S generates the entire lattice, then it is complemented.
• IsCompactlyGenerated.BooleanGenerators.distribLattice_of_sSup_eq_top: if S generates the entire lattice, then it is distributive.
• IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top: if S generates the entire lattice, then it is a Boolean algebra.

structure IsCompactlyGenerated.BooleanGenerators {α : Type u_1} [CompleteLattice α] (S : Set α) : Prop

An alternative constructor for Boolean algebras.

A set of Boolean generators in a compactly generated complete lattice is a subset S such that

• the elements of S are all atoms, and
• the set S satisfies an atomicity condition: any compact element below the supremum of a finite subset s of generators is equal to the supremum of a subset of s.

If the supremum of S is the whole lattice, then the lattice is a Boolean algebra (see IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top).

• isAtom (I : α) : I ∈ S → IsAtom I

  The elements in a collection of Boolean generators are all atoms.

• finitelyAtomistic (s : Finset α) (a : α) : ↑s ⊆ S → CompleteLattice.IsCompactElement a → a ≤ s.sup id → ∃ t ⊆ s, a = t.sup id

  The elements in a collection of Boolean generators satisfy an atomicity condition: any compact element below the supremum of a finite subset s of generators is equal to the supremum of a subset of s.

theorem IsCompactlyGenerated.BooleanGenerators.mono {α : Type u_1} [CompleteLattice α] {S : Set α} (hS : BooleanGenerators S) {T : Set α} (hTS : T ⊆ S) : BooleanGenerators T

theorem IsCompactlyGenerated.BooleanGenerators.atomistic {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : BooleanGenerators S) (a : α) (ha : a ≤ sSup S) : ∃ T ⊆ S, a = sSup T

theorem IsCompactlyGenerated.BooleanGenerators.isAtomistic_of_sSup_eq_top {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : BooleanGenerators S) (h : sSup S = ⊤) : IsAtomistic α

theorem IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atoms {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : BooleanGenerators S) (a : α) (ha : IsAtom a) (haS : a ≤ sSup S) : a ∈ S

theorem IsCompactlyGenerated.BooleanGenerators.sSup_inter {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : BooleanGenerators S) {T₁ T₂ : Set α} (hT₁ : T₁ ⊆ S) (hT₂ : T₂ ⊆ S) : sSup (T₁ ∩ T₂) = sSup T₁ ⊓ sSup T₂

def IsCompactlyGenerated.BooleanGenerators.distribLattice_of_sSup_eq_top {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : BooleanGenerators S) (h : sSup S = ⊤) : DistribLattice α

A lattice generated by Boolean generators is a distributive lattice.

Equations

• hS.distribLattice_of_sSup_eq_top h = { toLattice := CompleteLattice.toConditionallyCompleteLattice.toLattice, le_sup_inf := ⋯ }

theorem IsCompactlyGenerated.BooleanGenerators.complementedLattice_of_sSup_eq_top {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : BooleanGenerators S) (h : sSup S = ⊤) : ComplementedLattice α

noncomputable def IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : BooleanGenerators S) (h : sSup S = ⊤) : BooleanAlgebra α

A compactly generated complete lattice generated by Boolean generators is a Boolean algebra.

Equations

• hS.booleanAlgebra_of_sSup_eq_top h = DistribLattice.booleanAlgebraOfComplemented α

theorem IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : BooleanGenerators S) (X Y : Set α) (hX : X ⊆ S) (hY : Y ⊆ S) : sSup X ≤ sSup Y ↔ X ⊆ Y

theorem IsCompactlyGenerated.BooleanGenerators.eq_atoms_of_sSup_eq_top {α : Type u_1} [CompleteLattice α] {S : Set α} [IsCompactlyGenerated α] (hS : BooleanGenerators S) (h : sSup S = ⊤) : S = {a : α | IsAtom a}