English
There is a Galois connection between the star-closure operator adjoin R and the forgetful coe map to Subalgebra: adjoin R s ≤ S iff s ⊆ S.
Русский
Существует связь Гало между замыканием по звездочке и отображением забвения: adjoin R s ≤ S ⇔ s ⊆ S.
LaTeX
$$$\text{GaloisConnection}(\mathrm{adjoin}(R,\cdot),\uparrow)\;:\; \forall s,S,\; \mathrm{adjoin}(R,s) \le S \Leftrightarrow s \subseteq S.$$$
Lean4
protected theorem gc : GaloisConnection (adjoin R : Set A → StarSubalgebra R A) (↑) :=
by
intro s S
rw [← toSubalgebra_le_iff, adjoin_toSubalgebra, Algebra.adjoin_le_iff, coe_toSubalgebra]
exact
⟨fun h => Set.subset_union_left.trans h, fun h =>
Set.union_subset h fun x hx => star_star x ▸ star_mem (show star x ∈ S from h hx)⟩
