Quasi-finite primes in polynomial algebras #
theorem
Polynomial.not_weaklyQuasiFiniteAt
{R : Type u_1}
[CommRing R]
(P : Ideal (Polynomial R))
[P.IsPrime]
:
theorem
Polynomial.not_quasiFiniteAt
{R : Type u_1}
[CommRing R]
(P : Ideal (Polynomial R))
[P.IsPrime]
:
R[X] is not quasi-finite over R at any prime.
theorem
Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(f : Polynomial R →ₐ[R] S)
(P : Ideal S)
[P.IsPrime]
[Algebra.WeaklyQuasiFiniteAt R P]
:
theorem
Polynomial.map_under_lt_comap_of_quasiFiniteAt
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(f : Polynomial R →ₐ[R] S)
(P : Ideal S)
[P.IsPrime]
[Algebra.QuasiFiniteAt R P]
:
theorem
Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(f : Polynomial R →ₐ[R] S)
(hf : Function.Surjective ⇑f)
(P : Ideal S)
[P.IsPrime]
[Algebra.WeaklyQuasiFiniteAt R P]
:
¬RingHom.ker f ≤ Ideal.map C (Ideal.under R P)
theorem
Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(f : Polynomial R →ₐ[R] S)
(hf : Function.Surjective ⇑f)
(P : Ideal S)
[P.IsPrime]
[Algebra.QuasiFiniteAt R P]
:
¬RingHom.ker f ≤ Ideal.map C (Ideal.under R P)
If P is a prime of R[X]/I that is quasi finite over R,
then I is not contained in (P ∩ R)[X].
For usability, we replace I by the kernel of a surjective map R[X] →ₐ[R] S.