English
Let R be a nonunital, nonassociative semiring and let closure: Set R → NonUnitalSubsemiring R be the closure operator, with the inclusion map to sets. Then closure is left adjoint to the inclusion, i.e. for every subset S ⊆ R and every NonUnitalSubsemiring X of R, closure(S) ≤ X if and only if S ⊆ X.
Русский
Пусть R — полусемиринг без единицы, а замыкание: Set R → NonUnitalSubsemiring R — это оператор замыкания. Тогда он образует левую сопряженность с включением: для любой подмножества S ⊆ R и любого неупорядоченного полуполусемиринга X в R выполняется closure(S) ≤ X тогда и только тогда, когда S ⊆ X.
LaTeX
$$$\\forall S \\subseteq R, \\forall X \\in \\mathrm{NonUnitalSubsemiring}(R),\\quad \\operatorname{closure}(S) \\le X \\iff S \\subseteq X$$$
Lean4
/-- `closure` forms a Galois insertion with the coercion to set. -/
protected def gi : GaloisInsertion (@closure R _) (↑)
where
choice s _ := closure s
gc _ _ := closure_le
le_l_u _ := subset_closure
choice_eq _ _ := rfl
