English
If l: α → β and u: β → α form a GaloisInsertion between α and β, then the dualized pair forms a GaloisCoinsertion between αᵒᵈ and βᵒᵈ, with the dualized left and right adjoints given by l' = toDual ∘ l ∘ ofDual and u' = toDual ∘ u ∘ ofDual.
Русский
Если пары l: α → β и u: β → α образуют вставку Галуа между α и β, то дуальная пара образует коинсерцию Галуа между αᵒᵈ и βᵒᵈ, а дуальные лево- и правосторонние сопряженные отображения заданы как l' = toDual ∘ l ∘ ofDual и u' = toDual ∘ u ∘ ofDual.
LaTeX
$$$(l,u) \\text{ is a GaloisInsertion between } \\alpha,\\beta \\Rightarrow \\left( toDual \\circ l \\circ ofDual,\\; toDual \\circ u \\circ ofDual \\right) \\text{ is a GaloisCoinsertion between } \\alpha^{op},\\beta^{op}.$$$
Lean4
/-- Make a `GaloisCoinsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisInsertion` between `α` and
`β`. -/
def dual [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
GaloisInsertion l u → GaloisCoinsertion (toDual ∘ u ∘ ofDual) (toDual ∘ l ∘ ofDual) := fun x =>
⟨x.1, x.2.dual, x.3, x.4⟩
