ringHom_ext — Mathlib

English

If f1 and f2 are two rational maps from K to L that agree on the image of A in K, then f1 = f2.

Русский

Если два гомоморфизма кольца f1 и f2: K →+* L совпадают на образе A в K, то f1 = f2.

LaTeX

$$$(\forall x : A, f_1(\operatorname{algebraMap} A K x) = f_2(\operatorname{algebraMap} A K x)) \Rightarrow f_1 = f_2$$$

Lean4

/-- Another version of unique to give two lift maps should be equal -/
theorem ringHom_ext {f1 f2 : K →+* L} (hf : ∀ x : A, f1 (algebraMap A K x) = f2 (algebraMap A K x)) : f1 = f2 :=
  by
  ext z
  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := A) z
  rw [map_div₀, map_div₀, hf, hf]

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