mapping compact elements of complete lattices

Stream: general

[Alex J. Best]

What are the weakest assumptions on a morphism e for which we can prove for elements of complete lattices
lemma is_compact_element_iff (a : α) : is_compact_element (e a) ↔ is_compact_element a :=
I have it for order_iso's e, but really I would like it for some sort of order embedding (or maybe an injective complete lattice hom or something like that).
My actual use case is the inclusion of a sublattice into a bigger one, where the sublattice is obtained by truncating to all elements below some give element, so as long as that works I'm happy.
Maybe this would also take the form of assumptions on partial inverses f and e, as long as it works I don't mind that either!

import order.compactly_generated
import order.hom.complete_lattice

open complete_lattice

section

protected lemma order_iso.image_symm_eq_preimage {M₁ M₂ : Type*} [has_le M₁] [has_le M₂] (e : M₁ ≃o M₂)
  (s : set M₂) : e.symm '' s = e ⁻¹' s :=
by rw [e.symm.image_eq_preimage, e.symm_symm]

variables {α β : Type*} [complete_lattice α] [complete_lattice β] (e : α ≃o β)

lemma order_iso.map_is_compact_element (a : α) : is_compact_element a → is_compact_element (e a) :=
begin
  simp only [is_compact_element],
  intros h S hS,
  classical,
  obtain ⟨T, hT, hTle⟩ := h (e ⁻¹' S) _,
  { refine ⟨T.image e, by simpa, _⟩,
    apply_fun e at hTle,
    convert hTle,
    simp [finset.sup_image, finset.sup_eq_Sup_image, finset.sup_id_eq_Sup,
      order_iso.map_Sup, Sup_image], },
  { apply_fun e.symm at hS,
    rw [order_iso.symm_apply_apply, order_iso.map_Sup] at hS,
    rwa [← order_iso.image_symm_eq_preimage, Sup_image], },
end

lemma order_iso.is_compact_element_iff (a : α) : is_compact_element (e a) ↔ is_compact_element a :=
⟨λ h, e.symm_apply_apply a ▸ (e.symm.map_is_compact_element (e a)) h, e.map_is_compact_element a⟩

end

@Yaël Dillies :grinning:

[Jireh Loreaux]

What about Galois insertions? (I have not looked at any of the statements, this is just what jumped out at me from your description.)