Birkhoff's representation theorem

This file proves the Birkhoff representation theorem: Any finite distributive lattice can be represented as a sublattice of some powerset algebra.

Precisely, any nonempty finite distributive lattice is isomorphic to the lattice of lower sets of its irreducible elements. And conversely it is isomorphic to the order of its irreducible lower sets.

Main declarations

For a nonempty finite distributive lattice α:

• OrderIso.lowerSetSupIrred: α is isomorphic to the lattice of lower sets of its irreducible elements.
• OrderIso.supIrredLowerSet: α is isomorphic to the order of its irreducible lower sets.
• OrderEmbedding.birkhoffSet, OrderEmbedding.birkhoffFinset: Order embedding of α into the powerset lattice of its irreducible elements.
• LatticeHom.birkhoffSet, LatticeHom.birkhoffFinet: Same as the previous two, but bundled as an injective lattice homomorphism.
• exists_birkhoff_representation: α embeds into some powerset algebra. You should prefer using this over the explicit Birkhoff embedding because the Birkhoff embedding is littered with decidability footguns that this existential-packaged version can afford to avoid.

See also

This correspondence between finite distributive lattices and finite boolean algebras is made functorial in... TODO: Actually do it.

Tags

birkhoff, representation, stone duality, lattice embedding

@[simp]

theorem UpperSet.infIrred_Ici {α : Type u_1} [SemilatticeInf α] (a : α) : InfIrred (UpperSet.Ici a)

@[simp]

theorem UpperSet.infIrred_iff_of_finite {α : Type u_1} [SemilatticeInf α] {s : UpperSet α} [Finite α] : InfIrred s ↔ ∃ (a : α), UpperSet.Ici a = s

@[simp]

theorem LowerSet.supIrred_Iic {α : Type u_1} [SemilatticeSup α] (a : α) : SupIrred (LowerSet.Iic a)

@[simp]

theorem LowerSet.supIrred_iff_of_finite {α : Type u_1} [SemilatticeSup α] {s : LowerSet α} [Finite α] : SupIrred s ↔ ∃ (a : α), LowerSet.Iic a = s

noncomputable def OrderIso.lowerSetSupIrred {α : Type u_1} [DistribLattice α] [Fintype α] [OrderBot α] : α ≃o LowerSet { a : α // SupIrred a }

Birkhoff's Representation Theorem. Any nonempty finite distributive lattice is isomorphic to the lattice of lower sets of its sup-irreducible elements.

Equations

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

noncomputable def OrderIso.supIrredLowerSet {α : Type u_1} [DistribLattice α] [Fintype α] [OrderBot α] : α ≃o { s : LowerSet α // SupIrred s }

Any nonempty finite distributive lattice is isomorphic to its lattice of sup-irreducible lower sets. This is the other unitor of Birkhoff's representation theorem.

Equations

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

noncomputable def OrderEmbedding.birkhoffSet (α : Type u_1) [DistribLattice α] [Fintype α] : α ↪o Set { a : α // SupIrred a }

Birkhoff's Representation Theorem. Any finite distributive lattice can be embedded in a powerset lattice.

Equations

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

noncomputable def OrderEmbedding.birkhoffFinset (α : Type u_1) [DistribLattice α] [Fintype α] [DecidablePred SupIrred] : α ↪o Finset { a : α // SupIrred a }

Birkhoff's Representation Theorem. Any finite distributive lattice can be embedded in a powerset lattice.

Equations

• OrderEmbedding.birkhoffFinset α = RelEmbedding.trans (OrderEmbedding.birkhoffSet α) (OrderIso.toOrderEmbedding (OrderIso.symm Fintype.finsetOrderIsoSet))

@[simp]

theorem OrderEmbedding.coe_birkhoffFinset {α : Type u_1} [DistribLattice α] [Fintype α] [DecidablePred SupIrred] (a : α) : ↑((OrderEmbedding.birkhoffFinset α) a) = (OrderEmbedding.birkhoffSet α) a

@[simp]

theorem OrderEmbedding.birkhoffSet_sup {α : Type u_1} [DistribLattice α] [Fintype α] (a : α) (b : α) : (OrderEmbedding.birkhoffSet α) (a ⊔ b) = (OrderEmbedding.birkhoffSet α) a ∪ (OrderEmbedding.birkhoffSet α) b

@[simp]

theorem OrderEmbedding.birkhoffSet_inf {α : Type u_1} [DistribLattice α] [Fintype α] (a : α) (b : α) : (OrderEmbedding.birkhoffSet α) (a ⊓ b) = (OrderEmbedding.birkhoffSet α) a ∩ (OrderEmbedding.birkhoffSet α) b

@[simp]

theorem OrderEmbedding.birkhoffFinset_sup {α : Type u_1} [DistribLattice α] [Fintype α] [DecidablePred SupIrred] [DecidableEq α] (a : α) (b : α) : (OrderEmbedding.birkhoffFinset α) (a ⊔ b) = (OrderEmbedding.birkhoffFinset α) a ∪ (OrderEmbedding.birkhoffFinset α) b

@[simp]

theorem OrderEmbedding.birkhoffFinset_inf {α : Type u_1} [DistribLattice α] [Fintype α] [DecidablePred SupIrred] [DecidableEq α] (a : α) (b : α) : (OrderEmbedding.birkhoffFinset α) (a ⊓ b) = (OrderEmbedding.birkhoffFinset α) a ∩ (OrderEmbedding.birkhoffFinset α) b

@[simp]

theorem OrderEmbedding.birkhoffSet_apply {α : Type u_1} [DistribLattice α] [Fintype α] [OrderBot α] (a : α) : (OrderEmbedding.birkhoffSet α) a = ↑(OrderIso.lowerSetSupIrred a)

noncomputable def LatticeHom.birkhoffSet (α : Type u_1) [DistribLattice α] [Fintype α] : LatticeHom α (Set { a : α // SupIrred a })

Birkhoff's Representation Theorem. Any finite distributive lattice can be embedded in a powerset lattice.

Equations

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

noncomputable def LatticeHom.birkhoffFinset (α : Type u_1) [DistribLattice α] [Fintype α] [DecidableEq α] [DecidablePred SupIrred] : LatticeHom α (Finset { a : α // SupIrred a })

Birkhoff's Representation Theorem. Any finite distributive lattice can be embedded in a powerset lattice.

Equations

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

theorem LatticeHom.birkhoffFinset_injective (α : Type u_1) [DistribLattice α] [Fintype α] [DecidableEq α] [DecidablePred SupIrred] : Function.Injective ⇑(LatticeHom.birkhoffFinset α)

theorem exists_birkhoff_representation (α : Type u) [Finite α] [DistribLattice α] : ∃ (β : Type u) (x : DecidableEq β) (x_1 : Fintype β) (f : LatticeHom α (Finset β)), Function.Injective ⇑f