English
In the starred setting, the star-closure of polynomialFunctions s is contained in the equalizer of StarAlgHom φ ψ when φ and ψ agree on the image of X; i.e., (polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ.
Русский
В звездной обстановке звездочное замыкание polynomialFunctions s содержится во множестве равновесия StarAlgHom φ ψ тогда, когда φ и ψ согласны на образ X.
LaTeX
$$$(polynomialFunctions\\,s).starClosure \\le StarAlgHom.equalizer\\,φ\\ ψ$$$
Lean4
theorem starClosure_le_equalizer {A : Type*} [StarRing R] [ContinuousStar R] [Semiring A] [StarRing A] [Algebra R A]
(s : Set R) (φ ψ : C(s, R) →⋆ₐ[R] A) (h : φ (toContinuousMapOnAlgHom s X) = ψ (toContinuousMapOnAlgHom s X)) :
(polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ :=
by
rw [polynomialFunctions.starClosure_eq_adjoin_X s]
exact StarAlgHom.adjoin_le_equalizer φ ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h
