A Galois connection restricts to an order isomorphism between the closed elements

For a Galois connection l ⊣ u, the elements of α fixed by u ∘ l and those of β fixed by l ∘ u correspond order-isomorphically, with l and u exchanging them. Mathlib has only the one-sided ClosureOperator.gi. Stated for a bare GaloisConnection on two PartialOrders.

Every "the operation is an involution on a characterised class" theorem of convex analysis is an instance: conjugacy on the closed convex functions on the two sides of a pairing (Rockafellar's Corollary 12.2.1), polarity on the closed convex cones (Theorem 14.1), the gauge and support-function correspondences. Those connections are antitone — presented, as Mathlib presents them, with one side an OrderDual — so the correspondences are order anti-isomorphisms.

Main results

• GaloisConnection.closedsOrderIso — the isomorphism.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §12, §14.

def GaloisConnection.closedsOrderIso {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : { a : α // u (l a) = a } ≃o { b : β // l (u b) = b }

{a // u (l a) = a} and {b // l (u b) = b} are the two classes on which the connection's round trips are the identity, and l/u exchange them order-isomorphically.

Equations

• gc.closedsOrderIso = { toFun := fun (a : { a : α // u (l a) = a }) => ⟨l ↑a, ⋯⟩, invFun := fun (b : { b : β // l (u b) = b }) => ⟨u ↑b, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem GaloisConnection.closedsOrderIso_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a : { a : α // u (l a) = a }) : ↑(gc.closedsOrderIso a) = l ↑a

@[simp]

theorem GaloisConnection.closedsOrderIso_symm_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (b : { b : β // l (u b) = b }) : ↑(gc.closedsOrderIso.symm b) = u ↑b