Frames, completely distributive lattices and Boolean algebras

In this file we define and provide API for frames, completely distributive lattices and completely distributive Boolean algebras.

Typeclasses

• Order.Frame: Frame: A complete lattice whose ⊓⊓ distributes over ⨆⨆.
• Order.Coframe: Coframe: A complete lattice whose ⊔⊔ distributes over ⨅⨅.
• CompleteDistribLattice: Completely distributive lattices: A complete lattice whose ⊓⊓ and ⊔⊔ distribute over ⨆⨆ and ⨅⨅ respectively.
• CompleteBooleanAlgebra: Completely distributive Boolean algebra: A Boolean algebra whose ⊓⊓ and ⊔⊔ distribute over ⨆⨆ and ⨅⨅ respectively.

A set of opens gives rise to a topological space precisely if it forms a frame. Such a frame is also completely distributive, but not all frames are. Filter is a coframe but not a completely distributive lattice.

TODO

Add instances for Prod

References

• Wikipedia, Complete Heyting algebra
• [Francis Borceux, Handbook of Categorical Algebra III][borceux-vol3]

ink

class Order.Frame (α : Type u_1) extends CompleteLattice : Type u_1

• In a frame, ⊓⊓ distributes over ⨆⨆.

  inf_supₛ_le_supᵢ_inf : ∀ (a : α) (s : Set α), a ⊓ supₛ s ≤ ⨆ b, ⨆ h, a ⊓ b

A frame, aka complete Heyting algebra, is a complete lattice whose ⊓⊓ distributes over ⨆⨆.

ink

class Order.Coframe (α : Type u_1) extends CompleteLattice : Type u_1

• In a coframe, ⊔⊔ distributes over ⨅⨅.

  infᵢ_sup_le_sup_infₛ : ∀ (a : α) (s : Set α), (⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s

A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice whose ⊔⊔ distributes over ⨅⨅.

ink

class CompleteDistribLattice (α : Type u_1) extends Order.Frame : Type u_1

• In a completely distributive lattice, ⊔⊔ distributes over ⨅⨅.

  infᵢ_sup_le_sup_infₛ : ∀ (a : α) (s : Set α), (⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s

A completely distributive lattice is a complete lattice whose ⊔⊔ and ⊓⊓ respectively distribute over ⨅⨅ and ⨆⨆.

ink

instance CompleteDistribLattice.toCoframe {α : Type u} [inst : CompleteDistribLattice α] : Order.Coframe α

Equations

• CompleteDistribLattice.toCoframe = let src := inst; Order.Coframe.mk (_ : ∀ (a : α) (s : Set α), (⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s)

ink

instance OrderDual.coframe {α : Type u} [inst : Order.Frame α] : Order.Coframe αᵒᵈ

Equations

• OrderDual.coframe = let src := OrderDual.completeLattice α; Order.Coframe.mk (_ : ∀ (a : α) (s : Set α), a ⊓ supₛ s ≤ ⨆ b, ⨆ h, a ⊓ b)

ink

theorem inf_supₛ_eq {α : Type u} [inst : Order.Frame α] {s : Set α} {a : α} : a ⊓ supₛ s = ⨆ b, ⨆ h, a ⊓ b

ink

theorem supₛ_inf_eq {α : Type u} [inst : Order.Frame α] {s : Set α} {b : α} : supₛ s ⊓ b = ⨆ a, ⨆ h, a ⊓ b

ink

theorem supᵢ_inf_eq {α : Type u} {ι : Sort w} [inst : Order.Frame α] (f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

ink

theorem inf_supᵢ_eq {α : Type u} {ι : Sort w} [inst : Order.Frame α] (a : α) (f : ι → α) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i

ink

theorem supᵢ₂_inf_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [inst : Order.Frame α] {f : (i : ι) → κ i → α} (a : α) : (⨆ i, ⨆ j, f i j) ⊓ a = ⨆ i, ⨆ j, f i j ⊓ a

ink

theorem inf_supᵢ₂_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [inst : Order.Frame α] {f : (i : ι) → κ i → α} (a : α) : (a ⊓ ⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, a ⊓ f i j

ink

theorem supᵢ_inf_supᵢ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} : ((⨆ i, f i) ⊓ ⨆ j, g j) = ⨆ i, f i.fst ⊓ g i.snd

ink

theorem bsupᵢ_inf_bsupᵢ {α : Type u} [inst : Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} : ((⨆ i, ⨆ h, f i) ⊓ ⨆ j, ⨆ h, g j) = ⨆ p, ⨆ h, f p.fst ⊓ g p.snd

ink

theorem supₛ_inf_supₛ {α : Type u} [inst : Order.Frame α] {s : Set α} {t : Set α} : supₛ s ⊓ supₛ t = ⨆ p, ⨆ h, p.fst ⊓ p.snd

ink

theorem supᵢ_disjoint_iff {α : Type u} {ι : Sort w} [inst : Order.Frame α] {a : α} {f : ι → α} : Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a

ink

theorem disjoint_supᵢ_iff {α : Type u} {ι : Sort w} [inst : Order.Frame α] {a : α} {f : ι → α} : Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)

ink

theorem supᵢ₂_disjoint_iff {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [inst : Order.Frame α] {a : α} {f : (i : ι) → κ i → α} : Disjoint (⨆ i, ⨆ j, f i j) a ↔ ∀ (i : ι) (j : κ i), Disjoint (f i j) a

ink

theorem disjoint_supᵢ₂_iff {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [inst : Order.Frame α] {a : α} {f : (i : ι) → κ i → α} : Disjoint a (⨆ i, ⨆ j, f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)

ink

theorem supₛ_disjoint_iff {α : Type u} [inst : Order.Frame α] {a : α} {s : Set α} : Disjoint (supₛ s) a ↔ ∀ (b : α), b ∈ s → Disjoint b a

ink

theorem disjoint_supₛ_iff {α : Type u} [inst : Order.Frame α] {a : α} {s : Set α} : Disjoint a (supₛ s) ↔ ∀ (b : α), b ∈ s → Disjoint a b

ink

theorem supᵢ_inf_of_monotone {α : Type u} [inst : Order.Frame α] {ι : Type u_1} [inst : Preorder ι] [inst : IsDirected ι fun x x_1 => x ≤ x_1] {f : ι → α} {g : ι → α} (hf : Monotone f) (hg : Monotone g) : (⨆ i, f i ⊓ g i) = (⨆ i, f i) ⊓ ⨆ i, g i

ink

theorem supᵢ_inf_of_antitone {α : Type u} [inst : Order.Frame α] {ι : Type u_1} [inst : Preorder ι] [inst : IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)] {f : ι → α} {g : ι → α} (hf : Antitone f) (hg : Antitone g) : (⨆ i, f i ⊓ g i) = (⨆ i, f i) ⊓ ⨆ i, g i

ink

instance Pi.frame {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → Order.Frame (π i)] : Order.Frame ((i : ι) → π i)

Equations

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

ink

instance Frame.toDistribLattice {α : Type u} [inst : Order.Frame α] : DistribLattice α

Equations

• Frame.toDistribLattice = DistribLattice.ofInfSupLe (_ : ∀ (a b c : α), a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c)

ink

instance OrderDual.frame {α : Type u} [inst : Order.Coframe α] : Order.Frame αᵒᵈ

Equations

• OrderDual.frame = let src := OrderDual.completeLattice α; Order.Frame.mk (_ : ∀ (a : α) (s : Set α), (⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s)

ink

theorem sup_infₛ_eq {α : Type u} [inst : Order.Coframe α] {s : Set α} {a : α} : a ⊔ infₛ s = ⨅ b, ⨅ h, a ⊔ b

ink

theorem infₛ_sup_eq {α : Type u} [inst : Order.Coframe α] {s : Set α} {b : α} : infₛ s ⊔ b = ⨅ a, ⨅ h, a ⊔ b

ink

theorem infᵢ_sup_eq {α : Type u} {ι : Sort w} [inst : Order.Coframe α] (f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a

ink

theorem sup_infᵢ_eq {α : Type u} {ι : Sort w} [inst : Order.Coframe α] (a : α) (f : ι → α) : (a ⊔ ⨅ i, f i) = ⨅ i, a ⊔ f i

ink

theorem infᵢ₂_sup_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [inst : Order.Coframe α] {f : (i : ι) → κ i → α} (a : α) : (⨅ i, ⨅ j, f i j) ⊔ a = ⨅ i, ⨅ j, f i j ⊔ a

ink

theorem sup_infᵢ₂_eq {α : Type u} {ι : Sort w} {κ : ι → Sort u_1} [inst : Order.Coframe α] {f : (i : ι) → κ i → α} (a : α) : (a ⊔ ⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, a ⊔ f i j

ink

theorem infᵢ_sup_infᵢ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} : ((⨅ i, f i) ⊔ ⨅ i, g i) = ⨅ i, f i.fst ⊔ g i.snd

ink

theorem binfᵢ_sup_binfᵢ {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} : ((⨅ i, ⨅ h, f i) ⊔ ⨅ j, ⨅ h, g j) = ⨅ p, ⨅ h, f p.fst ⊔ g p.snd

ink

theorem infₛ_sup_infₛ {α : Type u} [inst : Order.Coframe α] {s : Set α} {t : Set α} : infₛ s ⊔ infₛ t = ⨅ p, ⨅ h, p.fst ⊔ p.snd

ink

theorem infᵢ_sup_of_monotone {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} [inst : Preorder ι] [inst : IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)] {f : ι → α} {g : ι → α} (hf : Monotone f) (hg : Monotone g) : (⨅ i, f i ⊔ g i) = (⨅ i, f i) ⊔ ⨅ i, g i

ink

theorem infᵢ_sup_of_antitone {α : Type u} [inst : Order.Coframe α] {ι : Type u_1} [inst : Preorder ι] [inst : IsDirected ι fun x x_1 => x ≤ x_1] {f : ι → α} {g : ι → α} (hf : Antitone f) (hg : Antitone g) : (⨅ i, f i ⊔ g i) = (⨅ i, f i) ⊔ ⨅ i, g i

ink

instance Pi.coframe {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → Order.Coframe (π i)] : Order.Coframe ((i : ι) → π i)

Equations

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

ink

instance Coframe.toDistribLattice {α : Type u} [inst : Order.Coframe α] : DistribLattice α

Equations

• Coframe.toDistribLattice = let src := inst; DistribLattice.mk (_ : ∀ (a b c : α), (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c)

ink

instance instCompleteDistribLatticeOrderDual {α : Type u} [inst : CompleteDistribLattice α] : CompleteDistribLattice αᵒᵈ

Equations

• instCompleteDistribLatticeOrderDual = let src := OrderDual.frame; let src_1 := OrderDual.coframe; CompleteDistribLattice.mk (_ : ∀ (a : αᵒᵈ) (s : Set αᵒᵈ), (⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s)

ink

instance Pi.completeDistribLattice {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → CompleteDistribLattice (π i)] : CompleteDistribLattice ((i : ι) → π i)

Equations

• Pi.completeDistribLattice = let src := Pi.frame; let src_1 := Pi.coframe; CompleteDistribLattice.mk (_ : ∀ (a : (i : ι) → π i) (s : Set ((i : ι) → π i)), (⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s)

ink

class CompleteBooleanAlgebra (α : Type u_1) extends BooleanAlgebra , SupSet , InfSet : Type u_1

• Any upper bound is more than the set supremum.

  supₛ_le : ∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → supₛ s ≤ a
• toInfSet : InfSet α

• Any element of a set is more than the set infimum.

  infₛ_le : ∀ (s : Set α) (a : α), a ∈ s → infₛ s ≤ a

• Any lower bound is less than the set infimum.

  le_infₛ : ∀ (s : Set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ infₛ s

• In a frame, ⊓⊓ distributes over ⨆⨆.

  inf_supₛ_le_supᵢ_inf : ∀ (a : α) (s : Set α), a ⊓ supₛ s ≤ ⨆ b, ⨆ h, a ⊓ b

• In a completely distributive lattice, ⊔⊔ distributes over ⨅⨅.

  infᵢ_sup_le_sup_infₛ : ∀ (a : α) (s : Set α), (⨅ b, ⨅ h, a ⊔ b) ≤ a ⊔ infₛ s

A complete Boolean algebra is a completely distributive Boolean algebra.

ink

instance Pi.completeBooleanAlgebra {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → CompleteBooleanAlgebra (π i)] : CompleteBooleanAlgebra ((i : ι) → π i)

Equations

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

ink

instance Prop.completeBooleanAlgebra : CompleteBooleanAlgebra Prop

Equations

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

ink

theorem compl_infᵢ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ι → α} : infᵢ fᶜ = ⨆ i, f iᶜ

ink

theorem compl_supᵢ {α : Type u} {ι : Sort w} [inst : CompleteBooleanAlgebra α] {f : ι → α} : supᵢ fᶜ = ⨅ i, f iᶜ

ink

theorem compl_infₛ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α} : infₛ sᶜ = ⨆ i, ⨆ h, iᶜ

ink

theorem compl_supₛ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α} : supₛ sᶜ = ⨅ i, ⨅ h, iᶜ

ink

theorem compl_infₛ' {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α} : infₛ sᶜ = supₛ (compl '' s)

ink

theorem compl_supₛ' {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α} : supₛ sᶜ = infₛ (compl '' s)

ink

def Function.Injective.frame {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : Order.Frame β] (f : α → β) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_supₛ : ∀ (s : Set α), f (supₛ s) = ⨆ a, ⨆ h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = ⨅ a, ⨅ h, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : Order.Frame α

Pullback an Order.Frame along an injection.

Equations

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

ink

def Function.Injective.coframe {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : Order.Coframe β] (f : α → β) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_supₛ : ∀ (s : Set α), f (supₛ s) = ⨆ a, ⨆ h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = ⨅ a, ⨅ h, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : Order.Coframe α

Pullback an Order.Coframe along an injection.

Equations

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

ink

def Function.Injective.completeDistribLattice {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : CompleteDistribLattice β] (f : α → β) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_supₛ : ∀ (s : Set α), f (supₛ s) = ⨆ a, ⨆ h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = ⨅ a, ⨅ h, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : CompleteDistribLattice α

Pullback a CompleteDistribLattice along an injection.

Equations

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

ink

def Function.Injective.completeBooleanAlgebra {α : Type u} {β : Type v} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : HasCompl α] [inst : SDiff α] [inst : CompleteBooleanAlgebra β] (f : α → β) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_supₛ : ∀ (s : Set α), f (supₛ s) = ⨆ a, ⨆ h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = ⨅ a, ⨅ h, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f (aᶜ) = f aᶜ) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : CompleteBooleanAlgebra α

Pullback a CompleteBooleanAlgebra along an injection.

Equations

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

ink

instance PUnit.completeBooleanAlgebra : CompleteBooleanAlgebra PUnit

Equations

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

ink

@[simp]

theorem PUnit.supₛ_eq (s : Set PUnit) : supₛ s = PUnit.unit

ink

@[simp]

theorem PUnit.infₛ_eq (s : Set PUnit) : infₛ s = PUnit.unit