Birkhoff representation

This file proves two facts which together are commonly referred to as "Birkhoff representation":

1. Any nonempty finite partial order is isomorphic to the partial order of sup-irreducible elements in its lattice of lower sets.
2. Any nonempty finite distributive lattice is isomorphic to the lattice of lower sets of its partial order of sup-irreducible elements.

Main declarations

For a finite nonempty partial order α:

• OrderEmbedding.supIrredLowerSet: α is isomorphic to the order of its irreducible lower sets.

If α is moreover a distributive lattice:

• OrderIso.lowerSetSupIrred: α is isomorphic to the lattice of lower sets of its irreducible elements.
• 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

These results form the object part of finite Stone duality: the functorial contravariant equivalence between the category of finite distributive lattices and the category of finite partial orders. TODO: extend to morphisms.

References

• [G. Birkhoff, Rings of sets][birkhoff1937]

Tags

birkhoff, representation, stone duality, lattice embedding

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def OrderEmbedding.supIrredLowerSet {α : Type u_1} [PartialOrder α] : α ↪o { s : LowerSet α // SupIrred s }

The Birkhoff Embedding of a finite partial order as sup-irreducible elements in its lattice of lower sets.

Equations

• OrderEmbedding.supIrredLowerSet = { toFun := fun (a : α) => ⟨LowerSet.Iic a, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }

def OrderEmbedding.infIrredUpperSet {α : Type u_1} [PartialOrder α] : α ↪o { s : UpperSet α // InfIrred s }

The Birkhoff Embedding of a finite partial order as inf-irreducible elements in its lattice of lower sets.

Equations

• OrderEmbedding.infIrredUpperSet = { toFun := fun (a : α) => ⟨UpperSet.Ici a, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem OrderEmbedding.supIrredLowerSet_apply {α : Type u_1} [PartialOrder α] (a : α) : OrderEmbedding.supIrredLowerSet a = ⟨LowerSet.Iic a, ⋯⟩

@[simp]

theorem OrderEmbedding.infIrredUpperSet_apply {α : Type u_1} [PartialOrder α] (a : α) : OrderEmbedding.infIrredUpperSet a = ⟨UpperSet.Ici a, ⋯⟩

theorem OrderEmbedding.supIrredLowerSet_surjective {α : Type u_1} [PartialOrder α] [Finite α] : Function.Surjective ⇑OrderEmbedding.supIrredLowerSet

theorem OrderEmbedding.infIrredUpperSet_surjective {α : Type u_1} [PartialOrder α] [Finite α] : Function.Surjective ⇑OrderEmbedding.infIrredUpperSet

noncomputable def OrderIso.supIrredLowerSet {α : Type u_1} [PartialOrder α] [Finite α] : α ≃o { s : LowerSet α // SupIrred s }

Birkhoff Representation for partial orders. Any partial order is isomorphic to the partial order of sup-irreducible elements in its lattice of lower sets.

Equations

• OrderIso.supIrredLowerSet = RelIso.ofSurjective OrderEmbedding.supIrredLowerSet ⋯

noncomputable def OrderIso.infIrredUpperSet {α : Type u_1} [PartialOrder α] [Finite α] : α ≃o { s : UpperSet α // InfIrred s }

Birkhoff Representation for partial orders. Any partial order is isomorphic to the partial order of inf-irreducible elements in its lattice of upper sets.

Equations

• OrderIso.infIrredUpperSet = RelIso.ofSurjective OrderEmbedding.infIrredUpperSet ⋯

@[simp]

theorem OrderIso.supIrredLowerSet_apply {α : Type u_1} [PartialOrder α] [Finite α] (a : α) : OrderIso.supIrredLowerSet a = ⟨LowerSet.Iic a, ⋯⟩

@[simp]

theorem OrderIso.infIrredUpperSet_apply {α : Type u_1} [PartialOrder α] [Finite α] (a : α) : OrderIso.infIrredUpperSet a = ⟨UpperSet.Ici a, ⋯⟩

@[simp]

theorem OrderIso.supIrredLowerSet_symm_apply {α : Type u_1} [SemilatticeSup α] [OrderBot α] [Finite α] (s : { s : LowerSet α // SupIrred s }) [Fintype ↥↑s] : OrderIso.supIrredLowerSet.symm s = (↑↑s).toFinset.sup id

@[simp]

theorem OrderIso.infIrredUpperSet_symm_apply {α : Type u_1} [SemilatticeInf α] [OrderTop α] [Finite α] (s : { s : UpperSet α // InfIrred s }) [Fintype ↥↑s] : OrderIso.infIrredUpperSet.symm s = (↑↑s).toFinset.inf id

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

Birkhoff Representation for finite distributive lattices. 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 OrderEmbedding.birkhoffSet {α : Type u_1} [DistribLattice α] [Fintype α] [DecidablePred SupIrred] : α ↪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 Fintype.finsetOrderIsoSet.symm.toOrderEmbedding

@[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 α] [DecidablePred SupIrred] (a b : α) : OrderEmbedding.birkhoffSet (a ⊔ b) = OrderEmbedding.birkhoffSet a ∪ OrderEmbedding.birkhoffSet b

@[simp]

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

@[simp]

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

@[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

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

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

Equations

• LatticeHom.birkhoffSet = { toFun := ⇑OrderEmbedding.birkhoffSet, map_sup' := ⋯, map_inf' := ⋯ }

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

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

Equations

• LatticeHom.birkhoffFinset = { toFun := ⇑OrderEmbedding.birkhoffFinset, map_sup' := ⋯, map_inf' := ⋯ }

theorem LatticeHom.birkhoffFinset_injective {α : Type u_1} [DistribLattice α] [Fintype α] [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