hom_ext — Mathlib

English

If two ring homomorphisms f,g: R →+* Ring.Perfection S p have identical zero-coefficients after applying coeff, then f=g.

Русский

Если два гомоморфизма f,g: R →+* Ring.Perfection S p имеют одинаковые нулевые коэффициенты после применения coeff, то f=g.

LaTeX

$$$(\\text{lift } p,R,S, P, m)^{-1} \\circ \\text{RingHom.ext} \\Rightarrow f=g$$$

Lean4

theorem hom_ext {R : Type u₁} [CommSemiring R] [CharP R p] [PerfectRing R p] {S : Type u₂} [CommSemiring S] [CharP S p]
    {f g : R →+* Ring.Perfection S p} (hfg : ∀ x, coeff S p 0 (f x) = coeff S p 0 (g x)) : f = g :=
  (lift p R S).symm.injective <| RingHom.ext hfg

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