of_ringHom_of_comp_eq — Mathlib

English

If g(a) is transcendental over S and the composition of rings via f matches that via g, then a is transcendental over R.

Русский

Если g(a) транспендентно над S и композиции гомоморфизмов совпадают, то a транспендентен над R.

LaTeX

$$$Transcendental(S, g(a)) \Rightarrow Transcendental(R, a)$ при условии равенства композиции и подходящих условий на f, g.$$

Lean4

theorem of_ringHom_of_comp_eq [H : Algebra.Transcendental S B] (hf : Function.Injective f) (hg : Function.Surjective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Algebra.Transcendental R A :=
  by
  rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢
  exact fun halg ↦ H (halg.ringHom_of_comp_eq f g hf hg h)

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