English
If all elements of s commute pairwise and also commute with star b for all b in s, then the adjoin R s is a commutative semiring.
Русский
Если все элементы s коммутируют попарно и также коммутируют со звездой элемента b для всех b в s, то адъюнкт R s образует коммутативную полуспирину.
LaTeX
$$$\operatorname{adjoin}_R s \text{ is a }\mathrm{CommSemiring}$, provided $\forall a,b\in s,\ ab=ba$ and $a\star b=\star b\, a$.$$
Lean4
/-- If all elements of `s : Set A` commute pairwise and also commute pairwise with elements of
`star s`, then `StarSubalgebra.adjoin R s` is commutative. See note [reducible non-instances]. -/
abbrev adjoinCommSemiringOfComm {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a)
(hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) : CommSemiring (adjoin R s) :=
{ (adjoin R s).toSemiring with
mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
by
have hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a := fun a ha b hb ↦
Set.union_star_self_comm (fun _ ha _ hb ↦ hcomm _ hb _ ha) (fun _ ha _ hb ↦ hcomm_star _ hb _ ha) b hb a ha
have := adjoin_le_centralizer_centralizer R s
apply this at h₁
apply this at h₂
rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂
exact Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ h₁ _ h₂ }
