semiring from bounded distributive lattice

Stream: Is there code for X?

[Junyan Xu]

I'm not sure if this is worth adding to mathlib; all I have are some counterexamples that use this construction. Would like to hear about other use cases.

import Mathlib.Algebra.Order.Kleene

/-- A type synonym for converting a bounded lattice to an commutative semiring. -/
def SemiringOfLattice (α : Type*) : Type _ := α

namespace SemiringOfLattice

def equiv {α} : SemiringOfLattice α ≃ α := Equiv.refl α

instance {α} [Max α] : Max (SemiringOfLattice α) where
  max a b := equiv.symm (a.equiv ⊔ b.equiv)

instance {α} [DistribLattice α] [OrderBot α] [OrderTop α] :
    IdemCommSemiring (SemiringOfLattice α) where
  __ := equiv.injective.semilatticeSup _ fun _ _ ↦ rfl
  add a b := equiv.symm (a.equiv ⊔ b.equiv)
  add_assoc a := sup_assoc a.equiv
  zero := equiv.symm ⊥
  zero_add a := bot_sup_eq a.equiv
  add_zero a := sup_bot_eq a.equiv
  nsmul n a := if n = 0 then equiv.symm ⊥ else a
  nsmul_succ n a := show a.equiv = (if n = 0 then ⊥ else a.equiv) ⊔ a.equiv by
    rw [eq_comm, sup_eq_right]; split_ifs; exacts [bot_le, le_rfl]
  add_comm a := sup_comm a.equiv
  natCast n := if n = 0 then equiv.symm ⊥ else equiv.symm ⊤
  natCast_succ n := show (⊤ : α) = _ ⊔ ⊤ by simp only [le_top, sup_of_le_right]
  mul a b := equiv.symm (a.equiv ⊓ b.equiv)
  mul_assoc a := inf_assoc a.equiv
  npow n a := if n = 0 then equiv.symm ⊤ else a
  npow_succ n a := show a.equiv = (if n = 0 then ⊤ else a.equiv) ⊓ a.equiv by
    rw [eq_comm, inf_eq_right]; split_ifs; exacts [le_top, le_rfl]
  left_distrib a := inf_sup_left a.equiv
  right_distrib a := inf_sup_right a.equiv
  zero_mul a := bot_inf_eq a.equiv
  mul_zero a := inf_bot_eq a.equiv
  one := equiv.symm ⊤
  one_mul a := top_inf_eq a.equiv
  mul_one a := inf_top_eq a.equiv
  mul_comm a := inf_comm a.equiv
  bot_le a := bot_le (a := a.equiv)

end SemiringOfLattice

[Junyan Xu]

By the way I recently found the interesting paper Lattices, Spectral Spaces, and Closure Operations on Idempotent Semirings because I got curious whether all prime spectra of commutative semirings are spectral. Looks like it's not always the case. (Edit: it's always the case, see #23697)

[Eric Wieser]

I would guess we would use that to build the semiring instance on submodules?

[Junyan Xu]

Unfortunately, I think the multiplication doesn't agree ... Multiplication of submodules need not be commutative or idempotent. And submodules only form a modular lattice, not a distributive one.