English
Let α and β be preordered sets and suppose l: α → β, u: β → α form a Galois coinsertion. Then the dualized pair, given by l' = toDual ∘ u ∘ ofDual and u' = toDual ∘ l ∘ ofDual, constitutes a Galois insertion between αᵒᵈ and βᵒᵈ.
Русский
Пусть α и β — множество с упорядочиванием, а пары l: α → β и u: β → α образуют коинсерцию Галуа. Тогда их дуальные отображения l' = toDual ∘ u ∘ ofDual и u' = toDual ∘ l ∘ ofDual образуют вставку Галуа между αᵒᵈ и βᵒᵈ.
LaTeX
$$$\\text{If } (l,u) \\text{ is a Galois coinsertion between } \\alpha \\text{ and } \\beta, \\ \\text{then } (toDual \\circ u \\circ ofDual,\\; toDual \\circ l \\circ ofDual) \\text{ is a Galois insertion between } \\alpha^{op},\\beta^{op}.$$$
Lean4
/-- Make a `GaloisInsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisCoinsertion` between `α` and
`β`. -/
def dual [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
GaloisCoinsertion l u → GaloisInsertion (toDual ∘ u ∘ ofDual) (toDual ∘ l ∘ ofDual) := fun x =>
⟨x.1, x.2.dual, x.3, x.4⟩
