Theorems · Theorem · commutative algebra

exists_finite_inj_algHom_of_fg

∀ (k : Type u_2) (R : Type u_3) [inst : Field k] [inst_1 : CommRing R] [Nontrivial R] [a : Algebra k R]
  [fin : Algebra.FiniteType k R], ∃ s g, Function.Injective ⇑g ∧ g.Finite

For a finitely generated algebra A over a field k, there exists a natural number s and an injective homomorphism from k[X_0, X_1, ..., X_(s-1)] to A such that A is finite over k[X_0, X_1, ..., X_(s-1)].

Defined in

Mathlib.RingTheory.NoetherNormalization

Cited by

0 results in Mathlib

Foundations

Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldCommRingNontrivialAlgebraAlgebra.FiniteType