English
Let l: α → β and u: β → α form a Galois coinsertion between a preorder α and a preorder β, where β has a bottom element. Then α can be equipped with a bottom element defined by ⊥_α := choice(⊥_β), yielding an OrderBot α. In particular, the bottom of α is obtained by applying the right adjoint to the bottom of β, and this bottom satisfies ⊥_α ≤ a for all a ∈ α.
Русский
Пусть l: α → β и u: β → α образуют коинсерцию Гало между частично упорядоченными множествами α и β, причём β имеет нижнюю границу ⊥. Тогда на α течёт нижняя граница ⊥_α, заданная как ⊥_α := choice(⊥_β), образуя структуру OrderBot на α. Конкретно, нижняя граница α задаётся через правая смежность к нижней границе β и выполняет ⊥_α ≤ a для всех a ∈ α.
LaTeX
$$$\mathrm{Bottom\,Lifting}\;:\; \mathrm{OrderBot}(\alpha)\;\text{defined by}\; \bot_{\alpha} := gi(\bot_{\beta}) \, \wedge \, (\forall a\in\alpha)\; \bot_{\alpha} \le a.$$$
Lean4
/-- Lift the bot along a Galois coinsertion -/
abbrev liftOrderBot [Preorder β] [OrderBot β] (gi : GaloisCoinsertion l u) : OrderBot α :=
{ @OrderDual.instOrderBot _ _ gi.dual.liftOrderTop with bot := gi.choice ⊥ <| bot_le }
-- See note [reducible non-instances]
