Lifting lattice structures

Stream: Is there code for X?

[Eric Wieser]

Do we have these?

def semilattice_sup.lift {α β : Type*} [semilattice_sup α] [has_sup β]
  (f : β → α) (hf : function.injective f)
  (hsup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) : semilattice_sup β :=
{ sup := (⊔),
  le_sup_left := λ a b, le_sup_left.trans_eq (hsup a b).symm,
  le_sup_right := λ a b, le_sup_right.trans_eq (hsup a b).symm,
  sup_le := λ a b c hab hbc, (hsup a b).trans_le (sup_le hab hbc),
  ..partial_order.lift f hf }

def semilattice_inf.lift {α β : Type*} [semilattice_inf α] [has_inf β]
  (f : β → α) (hf : function.injective f)
  (hinf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) : semilattice_inf β :=
{ inf := (⊓),
  inf_le_left := λ a b, (hinf a b).trans_le inf_le_left,
  inf_le_right := λ a b, (hinf a b).trans_le inf_le_right,
  le_inf := λ a b c hab hbc, (le_inf hab hbc).trans_eq (hinf b c).symm,
  ..partial_order.lift f hf }

def lattice.lift {α β : Type*} [lattice α] [has_sup β] [has_inf β]
  (f : β → α) (hf : function.injective f)
  (hsup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
  (hinf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) : lattice β :=
{ ..semilattice_sup.lift f hf hsup,
  ..semilattice_inf.lift f hf hinf,
  ..partial_order.lift f hf }

[Eric Wieser]

Maybe they're hiding somewhere in monotone? Here f is monotone by definition of the partial_order we set up.