Documentation

Mathlib.Order.Birkhoff

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 α:

If α is moreover a distributive lattice:

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 #

Tags #

birkhoff, representation, stone duality, lattice embedding

@[simp]
theorem UpperSet.infIrred_Ici {α : Type u_1} [PartialOrder α] (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 : α) :
@[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' := }
Instances For
    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' := }
    Instances For
      @[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
      Instances For
        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
        Instances For
          @[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 α] [OrderBot α] [Fintype α] [DecidablePred SupIrred] :
          α ≃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.
          Instances For
            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.
            Instances For
              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
              Instances For
                @[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.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 α] [OrderBot α] [Fintype α] [DecidablePred SupIrred] (a : α) :
                OrderEmbedding.birkhoffSet a = (OrderIso.lowerSetSupIrred a)
                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' := }
                Instances For
                  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' := }
                  Instances For
                    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