algebraicIndependent_ringHom_iff_of_comp_eq

English

For injective g and a compatibility h, AlgebraicIndependent S (g ∘ x) is equivalent to AlgebraicIndependent R x.

Русский

При инъективности g и совместимости h алгебраическая независимость S (g ∘ x) эквивалентна независимости R x.

LaTeX

$$$\\text{Injective}(g) \\Rightarrow (AlgebraicIndependent_S(g \\circ x) \\iff AlgebraicIndependent_R x)$$$

Lean4

theorem algebraicIndependent_ringHom_iff_of_comp_eq (hg : Function.Injective g)
    (h : RingHom.comp (algebraMap S B) f = RingHom.comp g (algebraMap R A)) :
    AlgebraicIndependent S (g ∘ x) ↔ AlgebraicIndependent R x :=
  ⟨fun H ↦ H.of_ringHom_of_comp_eq f g (EquivLike.injective f) h, fun H ↦
    H.ringHom_of_comp_eq f g (EquivLike.surjective f) hg h⟩

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