algebraicIndependent_iff — Mathlib

English

Let f: A → A' be an algebra homomorphism. If f is injective, then AlgebraicIndependent R (f ∘ x) is equivalent to AlgebraicIndependent R x.

Русский

Пусть f: A → A' — алгебраический гомоморфизм и инъективен. Тогда AlgebraicIndependent R (f ∘ x) эквивалентно AlgebraicIndependent R x.

LaTeX

$$$\\\\mathrm{AlgHom}\\\\(R,A,A') \\\\(f) \\\\Rightarrow \\\\text{Injective}(f) \\\\Rightarrow \\\\mathrm{AlgebraicIndependent}(R,(f\\\\circ x)) \\\\iff \\\\mathrm{AlgebraicIndependent}(R,x)$$$

Lean4

theorem algebraicIndependent_iff (f : A →ₐ[R] A') (hf : Injective f) :
    AlgebraicIndependent R (f ∘ x) ↔ AlgebraicIndependent R x :=
  ⟨fun h => h.of_comp f, fun h => h.map hf.injOn⟩

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