Order adjoints and Galois connections

Stream: maths

[Yaël Dillies]

I am currently wondering whether docs#IsOrderRightAdjoint is just docs#GaloisConnection with extra steps. Here is my attempt at proving so:

import Mathlib.Order.SemiconjSup

variable {α β : Type*} [Preorder α] [Preorder β] {f : α → β} {g : β → α}

example : IsOrderRightAdjoint f g ↔ GaloisConnection f g where
  mp hfg a b := by
    unfold IsOrderRightAdjoint at hfg
    refine ⟨fun hab ↦ (hfg b).1 hab, fun hab ↦ ?_⟩
    sorry
  mpr hfg b := by simpa [hfg.le_iff_le] using isLUB_Iic

[Yaël Dillies]

I believe they are not actually equivalent unless f preserves suprema and, α is a semilattice and β is a complete lattice, in which case I have a proof:

import Mathlib.Order.SemiconjSup

namespace LeftOrdContinuous
variable {α β : Type*} [SemilatticeSup α] [SemilatticeSup β] {f : α → β}

lemma monotone (hf : LeftOrdContinuous f) : Monotone f := .of_map_sup hf.map_sup

end LeftOrdContinuous

variable {α β : Type*} [SemilatticeSup α] [CompleteLattice β] {f : α → β} {g : β → α}

example (hf : LeftOrdContinuous f) : IsOrderRightAdjoint f g ↔ GaloisConnection f g where
  mp hfg a b := by
    refine ⟨fun hab ↦ (hfg b).1 hab, fun hab ↦ (hf.monotone hab).trans ?_⟩
    simp [← (hf (hfg b)).sSup_eq]
  mpr hfg b := by simpa [hfg.le_iff_le] using isLUB_Iic

[Yaël Dillies]

@Yury G. Kudryashov, did you have any use case for IsOrderRightAdjoint that is not covered GaloisConnection?

[Yury G. Kudryashov]

I think that I added this definition before I understood Galois connections well enough.

[Yury G. Kudryashov]

I'll try to look at this tomorrow.

[Yury G. Kudryashov]

I forgot to add it to my TODO list. Doing it now.

[Yury G. Kudryashov]

I added this definition for 1 application about rotation numbers. I'll try to port it to GaloisConnection later tonight (I hope, there is a GaloisConnection there).