English
For a StarSubalgebra S and a set s, adjoin R s ≤ S if and only if s ⊆ S. This is the precise restatement of the Galois connection.
Русский
Для звёздной подалгебры S и множества s верна эквивалентность adjoin R s ≤ S ⇔ s ⊆ S.
LaTeX
$$$\text{adjoin}(R,s) \le S \iff s \subseteq S$$$
Lean4
/-- Galois insertion between `adjoin` and `coe`. -/
protected def gi : GaloisInsertion (adjoin R : Set A → StarSubalgebra R A) (↑)
where
choice s hs := (adjoin R s).copy s <| le_antisymm (StarAlgebra.gc.le_u_l s) hs
gc := StarAlgebra.gc
le_l_u S := (StarAlgebra.gc (S : Set A) (adjoin R S)).1 <| le_rfl
choice_eq _ _ := StarSubalgebra.copy_eq _ _ _
