English
There is a Galois insertion between adjoin and the SetLike.coe map, providing a canonical way to recover S from adjoin R S.
Русский
Существует вставка Гало между adjoin и отображением SetLike.coe, задающая канонический способ восстановления S из adjoin_R S.
LaTeX
$$$$ \text{GaloisInsertion}(adjoin_R, \\uparrow) \text{ between sets and subalgebras} $$$$
Lean4
/-- Galois insertion between `adjoin` and `SetLike.coe`. -/
protected def gi : GaloisInsertion (adjoin R : Set A → NonUnitalStarSubalgebra R A) (↑)
where
choice s hs := (adjoin R s).copy s <| le_antisymm (NonUnitalStarAlgebra.gc.le_u_l s) hs
gc := NonUnitalStarAlgebra.gc
le_l_u S := (NonUnitalStarAlgebra.gc (S : Set A) (adjoin R S)).1 <| le_rfl
choice_eq _ _ := NonUnitalStarSubalgebra.copy_eq _ _ _
