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