le_equalizer — Mathlib

English

If φ,ψ: C(s,R) →_R A are algebra homomorphisms and they agree on the image of X, then polynomialFunctions s is contained in the equalizer of φ and ψ: polynomialFunctions s ≤ AlgHom.equalizer φ ψ.

Русский

Если φ, ψ: C(s,R) →_R A — алгебра-гомоморфизмы и они согласны на образ X, то polynomialFunctions s ⊆ equalizer φ ψ.

LaTeX

$$$polynomialFunctions\\,s \\le AlgHom.equalizer\\,φ\\,ψ$$$

Lean4

theorem le_equalizer {A : Type*} [Semiring A] [Algebra R A] (s : Set R) (φ ψ : C(s, R) →ₐ[R] A)
    (h : φ (toContinuousMapOnAlgHom s X) = ψ (toContinuousMapOnAlgHom s X)) :
    polynomialFunctions s ≤ AlgHom.equalizer φ ψ :=
  by
  rw [polynomialFunctions.eq_adjoin_X s]
  exact φ.adjoin_le_equalizer ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h

Похожие утверждения