English
The opposite of the algebra generated by a set matches the algebra generated by the opposite elements: (Algebra.adjoin_R s)^{op} = Algebra.adjoin_R (unop⁻¹' s).
Русский
Противоположность порождает алгебру, генерируемую множеством, совпадает с алгеброй, порождённой противоположными элементами: (Algebra.adjoin_R s)^{op} = Algebra.adjoin_R (unop⁻¹' s).
LaTeX
$$$$(\\mathrm{Algebra.adjoin}_R s)^{op} = \\mathrm{Algebra.adjoin}_R (\\mathrm{unop}^{-1}\\, s)$$$$
Lean4
theorem op_adjoin (s : Set A) : (Algebra.adjoin R s).op = Algebra.adjoin R (MulOpposite.unop ⁻¹' s) :=
by
apply toSubsemiring_injective
simp_rw [Algebra.adjoin, op_toSubsemiring, Subsemiring.op_closure, Set.preimage_union]
congr with x
simp_rw [Set.mem_preimage, Set.mem_range, MulOpposite.algebraMap_apply]
congr!
rw [← MulOpposite.op_injective.eq_iff (b := x.unop), MulOpposite.op_unop]
