English
There is a Galois insertion between adjoin and inclusion, exhibiting an optimal construction of adjoin as a closure operator.
Русский
Существует Галуа-вставка между adjoin и включением, иллюстрирующая адьон как операцию замыкания.
LaTeX
$$$\text{gi} : \text{GaloisInsertion}(\operatorname{adjoin}_R, \uparrow)$$$
Lean4
/-- Galois insertion between `adjoin` and `SetLike.coe`. -/
protected def gi : GaloisInsertion (adjoin R : Set A → NonUnitalSubalgebra R A) (↑)
where
choice s hs := (adjoin R s).copy s <| le_antisymm (NonUnitalAlgebra.gc.le_u_l s) hs
gc := NonUnitalAlgebra.gc
le_l_u S := (NonUnitalAlgebra.gc (S : Set A) (adjoin R S)).1 <| le_rfl
choice_eq _ _ := NonUnitalSubalgebra.copy_eq _ _ _
