English
A GaloisInsertion between αᵒᵈ and βᵒᵈ yields a GaloisCoinsertion between α and β by reversing the dualization: l' = toDual ∘ u ∘ ofDual and u' = toDual ∘ l ∘ ofDual.
Русский
Вставка Галуа между αᵒᵈ и βᵒᵈ порождает коинсерцию Галуа между α и β через обратное двойственное отображение: l' = toDual ∘ u ∘ ofDual, u' = toDual ∘ l ∘ ofDual.
LaTeX
$$$\\text{If } (l,u) \\text{ is a GaloisInsertion between } α^{op},β^{op}, \\text{ then } (toDual \\circ u \\circ ofDual,\\; toDual \\circ l \\circ ofDual) \\text{ is a GaloisCoinsertion between } α,β.$$$
Lean4
/-- Make a `GaloisCoinsertion` between `α` and `β` from a `GaloisInsertion` between `αᵒᵈ` and
`βᵒᵈ`. -/
def ofDual [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :
GaloisInsertion l u → GaloisCoinsertion (ofDual ∘ u ∘ toDual) (ofDual ∘ l ∘ toDual) := fun x =>
⟨x.1, x.2.dual, x.3, x.4⟩
