galois_connection

A Galois connection is a pair of functions l and u satisfying l a ≤ b ↔ a ≤ u b. They are closely connected to adjoint functors in category theory.

order_iso.to_galois_connection

Makes a Galois connection from an order-preserving bijection.

galois_insertion

A Galois insertion is a Galois connection where l ∘ u = id. It also contains a constructive choice function, to give better definitional equalities when lifting order structures.

order_iso.to_galois_insertion

Makes a Galois insertion from an order-preserving bijection.

galois_connection.lift_order_bot

Lift the bottom along a Galois connection

galois_insertion.lift_semilattice_sup

Lift the suprema along a Galois insertion

galois_insertion.lift_semilattice_inf

Lift the infima along a Galois insertion

galois_insertion.lift_lattice

Lift the suprema and infima along a Galois insertion

galois_insertion.lift_order_top

Lift the top along a Galois insertion

galois_insertion.lift_bounded_lattice

Lift the top, bottom, suprema, and infima along a Galois insertion

galois_insertion.lift_complete_lattice

Lift all suprema and infima along a Galois insertion