# 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.

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} [] (a : α) :
@[simp]
theorem UpperSet.infIrred_iff_of_finite {α : Type u_1} [] {s : } [] :
∃ (a : α),
@[simp]
theorem LowerSet.supIrred_Iic {α : Type u_1} [] (a : α) :
@[simp]
theorem LowerSet.supIrred_iff_of_finite {α : Type u_1} [] {s : } [] :
∃ (a : α),
def OrderEmbedding.supIrredLowerSet {α : Type u_1} [] :
α ↪o { 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 : α) => ⟨, , inj' := , map_rel_iff' := }
Instances For
def OrderEmbedding.infIrredUpperSet {α : Type u_1} [] :
α ↪o { 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 : α) => ⟨, , inj' := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderEmbedding.supIrredLowerSet_apply {α : Type u_1} [] (a : α) :
OrderEmbedding.supIrredLowerSet a = ,
@[simp]
theorem OrderEmbedding.infIrredUpperSet_apply {α : Type u_1} [] (a : α) :
OrderEmbedding.infIrredUpperSet a = ,
theorem OrderEmbedding.supIrredLowerSet_surjective {α : Type u_1} [] [] :
Function.Surjective OrderEmbedding.supIrredLowerSet
theorem OrderEmbedding.infIrredUpperSet_surjective {α : Type u_1} [] [] :
Function.Surjective OrderEmbedding.infIrredUpperSet
noncomputable def OrderIso.supIrredLowerSet {α : Type u_1} [] [] :
α ≃o { 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
Instances For
noncomputable def OrderIso.infIrredUpperSet {α : Type u_1} [] [] :
α ≃o { 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
Instances For
@[simp]
theorem OrderIso.supIrredLowerSet_apply {α : Type u_1} [] [] (a : α) :
OrderIso.supIrredLowerSet a = ,
@[simp]
theorem OrderIso.infIrredUpperSet_apply {α : Type u_1} [] [] (a : α) :
OrderIso.infIrredUpperSet a = ,
@[simp]
theorem OrderIso.supIrredLowerSet_symm_apply {α : Type u_1} [] [] [] (s : { s : // }) [Fintype s] :
OrderIso.supIrredLowerSet.symm s = (s).toFinset.sup id
@[simp]
theorem OrderIso.infIrredUpperSet_symm_apply {α : Type u_1} [] [] [] (s : { s : // }) [Fintype s] :
OrderIso.infIrredUpperSet.symm s = (s).toFinset.inf id
noncomputable def OrderIso.lowerSetSupIrred {α : Type u_1} [] [] [] [DecidablePred SupIrred] :
α ≃o LowerSet { 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.
Instances For
noncomputable def OrderEmbedding.birkhoffSet {α : Type u_1} [] [] [DecidablePred SupIrred] :
α ↪o Set { 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.
Instances For
noncomputable def OrderEmbedding.birkhoffFinset {α : Type u_1} [] [] [DecidablePred SupIrred] :
α ↪o Finset { 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
Instances For
@[simp]
theorem OrderEmbedding.coe_birkhoffFinset {α : Type u_1} [] [] [DecidablePred SupIrred] (a : α) :
(OrderEmbedding.birkhoffFinset a) = OrderEmbedding.birkhoffSet a
@[simp]
theorem OrderEmbedding.birkhoffSet_sup {α : Type u_1} [] [] [DecidablePred SupIrred] (a : α) (b : α) :
OrderEmbedding.birkhoffSet (a b) = OrderEmbedding.birkhoffSet a OrderEmbedding.birkhoffSet b
@[simp]
theorem OrderEmbedding.birkhoffSet_inf {α : Type u_1} [] [] [DecidablePred SupIrred] (a : α) (b : α) :
OrderEmbedding.birkhoffSet (a b) = OrderEmbedding.birkhoffSet a OrderEmbedding.birkhoffSet b
@[simp]
theorem OrderEmbedding.birkhoffFinset_sup {α : Type u_1} [] [] [DecidablePred SupIrred] [] (a : α) (b : α) :
OrderEmbedding.birkhoffFinset (a b) = OrderEmbedding.birkhoffFinset a OrderEmbedding.birkhoffFinset b
@[simp]
theorem OrderEmbedding.birkhoffFinset_inf {α : Type u_1} [] [] [DecidablePred SupIrred] [] (a : α) (b : α) :
OrderEmbedding.birkhoffFinset (a b) = OrderEmbedding.birkhoffFinset a OrderEmbedding.birkhoffFinset b
@[simp]
theorem OrderEmbedding.birkhoffSet_apply {α : Type u_1} [] [] [] [DecidablePred SupIrred] (a : α) :
OrderEmbedding.birkhoffSet a = (OrderIso.lowerSetSupIrred a)
noncomputable def LatticeHom.birkhoffSet {α : Type u_1} [] [] [DecidablePred SupIrred] :
LatticeHom α (Set { 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' := }
Instances For
noncomputable def LatticeHom.birkhoffFinset {α : Type u_1} [] [] [DecidablePred SupIrred] :
LatticeHom α (Finset { 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' := }
Instances For
theorem LatticeHom.birkhoffFinset_injective {α : Type u_1} [] [] [DecidablePred SupIrred] :
Function.Injective LatticeHom.birkhoffFinset
theorem exists_birkhoff_representation (α : Type u) [] [] :
∃ (β : Type u) (x : ) (x_1 : ) (f : LatticeHom α ()),