The poset adjoint functor theorem

[UPSTREAM] candidate: a map between complete lattices is a left adjoint iff it preserves arbitrary suprema (exists_galoisConnection_iff_forall_sSup); mathlib has GaloisConnection.l_sSup but not the converse. On a finite lattice the criterion reduces to binary sup-preservation plus ⊥-preservation (exists_galoisConnection_iff_forall_sup).

theorem galoisConnection_of_forall_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {f : α → β} (hf : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) : GaloisConnection f fun (b : β) => sSup {a : α | f a ≤ b}

Poset adjoint functor theorem, construction half: a sSup-preserving map between complete lattices is a left adjoint, with right adjoint λ b => sSup {a | f a ≤ b}.

theorem exists_galoisConnection_iff_forall_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α → β) : (∃ (u : β → α), GaloisConnection f u) ↔ ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a

Poset adjoint functor theorem: a map between complete lattices is a left adjoint iff it preserves arbitrary suprema.

theorem exists_galoisConnection_iff_forall_sup {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Finite α] [SemilatticeSup β] [OrderBot β] (f : α → β) : (∃ (u : β → α), GaloisConnection f u) ↔ (∀ (p q : α), f (p ⊔ q) = f p ⊔ f q) ∧ f ⊥ = ⊥

On a finite lattice, left-adjointness is exactly binary sup-preservation plus ⊥-preservation.