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 ∈ 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.isAtom {α : Type u_1} [CompleteLattice α] {S : Set α} (self : IsCompactlyGenerated.BooleanGenerators S) (I : α) : I ∈ S → IsAtom I

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

theorem IsCompactlyGenerated.BooleanGenerators.finitelyAtomistic {α : Type u_1} [CompleteLattice α] {S : Set α} (self : IsCompactlyGenerated.BooleanGenerators S) (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 : IsCompactlyGenerated.BooleanGenerators S) {T : Set α} (hTS : T ⊆ S) : IsCompactlyGenerated.BooleanGenerators T

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

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

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

theorem IsCompactlyGenerated.BooleanGenerators.sSup_inter {α : Type u_1} [CompleteLattice α] [IsCompactlyGenerated α] {S : Set α} (hS : IsCompactlyGenerated.BooleanGenerators S) {T₁ : Set α} {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 α] [IsCompactlyGenerated α] {S : Set α} (hS : IsCompactlyGenerated.BooleanGenerators S) (h : sSup S = ⊤) : DistribLattice α

A lattice generated by boolean generators is a distributive lattice.

Equations

• hS.distribLattice_of_sSup_eq_top h = DistribLattice.mk ⋯

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

noncomputable def IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top {α : Type u_1} [CompleteLattice α] [IsCompactlyGenerated α] {S : Set α} (hS : IsCompactlyGenerated.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 = let _i := hS.distribLattice_of_sSup_eq_top h; let_fun this := ⋯; DistribLattice.booleanAlgebraOfComplemented α

theorem IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms {α : Type u_1} [CompleteLattice α] [IsCompactlyGenerated α] {S : Set α} (hS : IsCompactlyGenerated.BooleanGenerators S) (X : Set α) (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 α] [IsCompactlyGenerated α] {S : Set α} (hS : IsCompactlyGenerated.BooleanGenerators S) (h : sSup S = ⊤) : S = {a : α | IsAtom a}