English
There is a Galois insertion between adjoin and the coercion to Set; i.e., the pair (adjoin R, ↑) forms a Galois insertion with Subalgebra viewed as a subset of A.
Русский
Существует Галуа-инсерция между операциями порождения adjoin и включением в множество; пара (adjoin R, ↑) образует Галуа-инсерцию между подалгебрами и их множествами внутри A.
LaTeX
$$$\text{GaloisInsertion}(\mathrm{adjoin}_R,\uparrow)$$$
Lean4
protected theorem gc : GaloisConnection (adjoin R : Set A → Subalgebra R A) (↑) := fun s S =>
⟨fun H => le_trans (le_trans Set.subset_union_right Subsemiring.subset_closure) H, fun H =>
show Subsemiring.closure (Set.range (algebraMap R A) ∪ s) ≤ S.toSubsemiring from
Subsemiring.closure_le.2 <| Set.union_subset S.range_subset H⟩
