English
There exists a lifting instance that assigns to a set s of R the structure of a NonUnitalStarSubsemiring R, provided s contains 0 and is closed under addition, multiplication, and star.
Русский
Существует инстанс подъёма множества, который на множество s над R накладывает структуру NonUnitalStarSubsemiring R, при условии что 0∈s и s замкнуется по сложению, умножению и звезде.
LaTeX
$$CanLift(Set R, NonUnitalStarSubsemiring R, ↑ , …)$$
Lean4
/-- If all elements of `s : Set A` commute pairwise and with elements of `star s`, then `adjoin R s`
is a non-unital commutative semiring.
See note [reducible non-instances]. -/
abbrev adjoinNonUnitalCommSemiringOfComm {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a)
(hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) : NonUnitalCommSemiring (adjoin R s) :=
{ (adjoin R s).toNonUnitalSemiring 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₂ }
