ringHom_of_comp_eq — Mathlib

English

If A is algebraic over R and the ring homomorphisms f, g satisfy a certain composition equality, then B is algebraic over S.

Русский

Если A алгебраичен над R и выполняется равенство композиции гомоморфизмов f и g, то B алгебраичен над S.

LaTeX

$$$[\text{Algebra.IsAlgebraic}(R, A)] \to (f, g, h) \Rightarrow IsAlgebraic(S, B).$$$

Lean4

theorem ringHom_of_comp_eq [Algebra.IsAlgebraic R A] (hf : Function.Injective f) (hg : Function.Surjective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) : Algebra.IsAlgebraic S B :=
  by
  refine ⟨fun b ↦ ?_⟩
  obtain ⟨a, rfl⟩ := hg b
  exact (Algebra.IsAlgebraic.isAlgebraic a).ringHom_of_comp_eq f g hf h

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