algHom_ext — Mathlib

English

If two algebra homomorphisms f,g: A/I → S agree after precomposition with the quotient map mkₐ, then f = g.

Русский

Если два алгеброгомоморфизма f,g: A/I → S согласованы после предобразования через mkₐ, то f = g.

LaTeX

$$$ \forall f,g: A/I \to_{R_1} S, \ (f \circ mkₐ = g \circ mkₐ) \Rightarrow f = g $$$

Lean4

theorem algHom_ext {I : Ideal A} [I.IsTwoSided] {S} [Semiring S] [Algebra R₁ S] ⦃f g : A ⧸ I →ₐ[R₁] S⦄
    (h : f.comp (Quotient.mkₐ R₁ I) = g.comp (Quotient.mkₐ R₁ I)) : f = g :=
  AlgHom.ext fun x => Quotient.inductionOn' x <| AlgHom.congr_fun h

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