OrderEmbedding that is an OrderIso on its image

Stream: Is there code for X?

[Snir Broshi]

I have an docs#OrderEmbedding that can be docs#OrderIso on its image, e.g.

def mulTwo : ℕ ↪o ℕ :=
  OrderEmbedding.ofMapLEIff (2 * ·) <| by lia

or

def replicateZero : ℕ ↪o Multiset ℕ :=
  OrderEmbedding.ofMapLEIff (Multiset.replicate · 0) <| @Multiset.replicate_le_replicate _ 0

The problem is that OrderEmbedding only provides inequalities over sups/infs (docs#OrderEmbedding.le_map_sup / docs#OrderEmbedding.map_inf_le) rather than equalities (docs#OrderIso.map_sup / docs#OrderIso.map_inf).

Is there a type for that? (hopefully where I don't have to provide an inverse function, but it's not a deal breaker)
And is there a nice condition under which an OrderEmbedding satisfies equalities for sups/infs/top/bot?
(e.g. Real.arctan is an order embedding but it doesn't preserve top/bot)

[Yaël Dillies]

Sorry, I don't understand what your question is. Any order embedding is an order isomorphism on its image.

[Snir Broshi]

Yaël Dillies said:

Sorry, I don't understand what your question is. Any order embedding is an order isomorphism on its image.

Yes there's docs#OrderEmbedding.orderIso, but that converts the image to a Subtype, so it loses most of its lattice structure (sup/inf/top/bot).

What I meant was: What hypotheses do I have to add on f to the following code to make the theorems hold, and is there already such an existing type that extends OrderEmbedding?

import Mathlib
variable {α β : Type*} [CompleteDistribLattice α] [CompleteDistribLattice β] (f : α ↪o β)

theorem map_bot : f ⊥ = ⊥ := sorry
theorem map_top : f ⊥ = ⊥ := sorry

theorem map_inf (x y : α) : f (x ⊓ y) = f x ⊓ f y := sorry
theorem map_sup (x y : α) : f (x ⊔ y) = f x ⊔ f y := sorry

theorem isMax_apply (x : α) : IsMax (f x) ↔ IsMax x := sorry
theorem isMin_apply (x : α) : IsMin (f x) ↔ IsMin x := sorry

These theorems are true for the two embeddings I gave as examples above (at least the applicable theorems after adjusting the typeclasses)

[Snir Broshi]

OrderEmbedding provides similar theorems but with inequalities, similar to a Galois connection, whereas I'm looking for something more like a group/ring homomorphism - preserve the structure

[Yaël Dillies]

We have docs#LatticeHom. If you separately assume injectivity, then you get what you asked for

[Snir Broshi]

Ooh there's even a docs#BoundedLatticeHom and a docs#CompleteLatticeHom, this looks exactly like what I was looking for, thanks!
Though now the problem becomes finding a "simple" way to construct such a hom, like docs#OrderEmbedding.ofMapLEIff for embeddings. Is there a single condition I can prove that'll provide all the fields for a lattice hom, or is there no way to avoid proving the sup/inf/top/bot theorems?

[Yaël Dillies]

A simple way is to have a Galois connection

[Snir Broshi]

I didn't find any relation between GaloisConnection/GaloisInsertion/GaloisCoinsertion and LatticeHom/BoundedLatticeHom/CompleteLatticeHom, how can it help?
(also creating an inverse function is daunting)

[Yaël Dillies]

See docs#GaloisConnection.l_sup and alike