lowerSetSupIrred — Mathlib

English

Birkhoff Representation for finite distributive lattices: any nonempty finite distributive lattice is isomorphic to the lattice of lower sets of its sup-irreducible elements.

Русский

Представление Биркхоффа для конечных распределительных решёток: любая ненулевая конечная распределительная решётка изоморфна решётке нижних множеств её суп-irreducible элементов.

LaTeX

$$$\\text{lowerSetSupIrred} : α \\cong_o \\mathrm{LowerSet}\\,\\{ a : α \\mid \\mathrm{SupIrred}\, a \\}$$$

Lean4

/-- **Birkhoff Representation for finite distributive lattices**. Any nonempty finite distributive
lattice is isomorphic to the lattice of lower sets of its sup-irreducible elements. -/
noncomputable def lowerSetSupIrred [OrderBot α] : α ≃o LowerSet { a : α // SupIrred a } :=
  Equiv.toOrderIso
    { toFun := fun a ↦ ⟨{b | ↑b ≤ a}, fun _ _ hcb hba ↦ hba.trans' hcb⟩
      invFun := fun s ↦ (s : Set { a : α // SupIrred a }).toFinset.sup (↑)
      left_inv := fun a ↦ by
        refine le_antisymm (Finset.sup_le fun b ↦ Set.mem_toFinset.1) ?_
        obtain ⟨s, rfl, hs⟩ := exists_supIrred_decomposition a
        exact Finset.sup_le fun i hi ↦ le_sup_of_le (b := ⟨i, hs hi⟩) (Set.mem_toFinset.2 <| le_sup (f := id) hi) le_rfl
      right_inv := fun s ↦ by
        ext a
        dsimp
        refine ⟨fun ha ↦ ?_, fun ha ↦ ?_⟩
        · obtain ⟨i, hi, ha⟩ := a.2.supPrime.le_finset_sup.1 ha
          exact s.lower ha (Set.mem_toFinset.1 hi)
        · dsimp
          exact le_sup (Set.mem_toFinset.2 ha) }
    (fun _ _ hbc _ ↦ le_trans' hbc) fun _ _ hst ↦ Finset.sup_mono <| Set.toFinset_mono hst

Похожие утверждения