hom_ext — Mathlib

English

If two ring homomorphisms f,g: R →+* Ring.Perfection S p agree after projection through coeff at 0 against a π, then f=g.

Русский

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

LaTeX

$$∀ x, π(f x) = π(g x) ⇒ f = g$$

Lean4

theorem hom_ext [PerfectRing R p] {S : Type u₂} [CommSemiring S] [CharP S p] {P : Type u₃} [CommSemiring P] [CharP P p]
    [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) {f g : R →+* P} (hfg : ∀ x, π (f x) = π (g x)) : f = g :=
  (lift p R S P π m).symm.injective <| RingHom.ext hfg

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