Ideals over/under ideals #
This file concerns ideals lying over other ideals.
Let f : R →+* S be a ring homomorphism (typically a ring extension), I an ideal of R and
J an ideal of S. We say J lies over I (and I under J) if I is the f-preimage of J.
This is expressed here by writing I = J.comap f.
Implementation notes #
The proofs of the comap_ne_bot and comap_lt_comap families use an approach
specific for their situation: we construct an element in I.comap f from the
coefficients of a minimal polynomial.
Once mathlib has more material on the localization at a prime ideal, the results
can be proven using more general going-up/going-down theory.
theorem
Ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{I : Ideal S}
{r : S}
(hr : r ∈ I)
{p : Polynomial R}
(hp : Polynomial.eval₂ f r p ∈ I)
:
Polynomial.coeff p 0 ∈ Ideal.comap f I
theorem
Ideal.coeff_zero_mem_comap_of_root_mem
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{I : Ideal S}
{r : S}
(hr : r ∈ I)
{p : Polynomial R}
(hp : Polynomial.eval₂ f r p = 0)
:
Polynomial.coeff p 0 ∈ Ideal.comap f I
theorem
Ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{I : Ideal S}
{r : S}
(r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0)
(hr : r ∈ I)
{p : Polynomial R}
:
p ≠ 0 → Polynomial.eval₂ f r p = 0 → ∃ (i : ℕ), Polynomial.coeff p i ≠ 0 ∧ Polynomial.coeff p i ∈ Ideal.comap f I
theorem
Ideal.injective_quotient_le_comap_map
{R : Type u_1}
[CommRing R]
(P : Ideal (Polynomial R))
:
Function.Injective
⇑(Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)
(Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)))
(_ :
P ≤ Ideal.comap (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)))
(Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)))
Let P be an ideal in R[x]. The map
R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R))
is injective.
theorem
Ideal.quotient_mk_maps_eq
{R : Type u_1}
[CommRing R]
(P : Ideal (Polynomial R))
:
RingHom.comp
(RingHom.comp
(Ideal.Quotient.mk (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P))
Polynomial.C)
(Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) = RingHom.comp
(Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)
(Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)))
(_ :
P ≤ Ideal.comap (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)))
(Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)))
(RingHom.comp (Ideal.Quotient.mk P) Polynomial.C)
The identity in this lemma asserts that the "obvious" square
R → (R / (P ∩ R))
↓ ↓
R[x] / P → (R / (P ∩ R))[x] / (P / (P ∩ R))
commutes. It is used, for instance, in the proof of quotient_mk_comp_C_is_integral_of_jacobson,
in the file RingTheory.Jacobson.
theorem
Ideal.exists_nonzero_mem_of_ne_bot
{R : Type u_1}
[CommRing R]
{P : Ideal (Polynomial R)}
(Pb : P ≠ ⊥)
(hP : ∀ (x : R), Polynomial.C x ∈ P → x = 0)
:
∃ p ∈ P, Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) p ≠ 0
This technical lemma asserts the existence of a polynomial p in an ideal P ⊂ R[x]
that is non-zero in the quotient R / (P ∩ R) [x]. The assumptions are equivalent to
P ≠ 0 and P ∩ R = (0).
theorem
Ideal.comap_eq_of_scalar_tower_quotient
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{p : Ideal R}
{P : Ideal S}
[Algebra R S]
[Algebra (R ⧸ p) (S ⧸ P)]
[IsScalarTower R (R ⧸ p) (S ⧸ P)]
(h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P)))
:
Ideal.comap (algebraMap R S) P = p
If there is an injective map R/p → S/P such that following diagram commutes:
R → S
↓ ↓
R/p → S/P
then P lies over p.
def
Ideal.Quotient.algebraQuotientOfLEComap
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{p : Ideal R}
{P : Ideal S}
(h : p ≤ Ideal.comap f P)
:
If P lies over p, then R / p has a canonical map to S / P.
Equations
Instances For
instance
Ideal.Quotient.algebraQuotientMapQuotient
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{p : Ideal R}
:
R / p has a canonical map to S / pS.
Equations
- Ideal.Quotient.algebraQuotientMapQuotient = Ideal.Quotient.algebraQuotientOfLEComap (_ : p ≤ Ideal.comap f (Ideal.map f p))
@[simp]
theorem
Ideal.Quotient.algebraMap_quotient_map_quotient
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{p : Ideal R}
(x : R)
:
(algebraMap (R ⧸ p) (S ⧸ Ideal.map f p)) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk (Ideal.map f p)) (f x)
@[simp]
theorem
Ideal.Quotient.mk_smul_mk_quotient_map_quotient
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{p : Ideal R}
(x : R)
(y : S)
:
(Ideal.Quotient.mk p) x • (Ideal.Quotient.mk (Ideal.map f p)) y = (Ideal.Quotient.mk (Ideal.map f p)) (f x * y)
instance
Ideal.Quotient.tower_quotient_map_quotient
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{p : Ideal R}
[Algebra R S]
:
IsScalarTower R (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Equations
- (_ : IsScalarTower R (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) = (_ : IsScalarTower R (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p))
instance
Ideal.QuotientMapQuotient.isNoetherian
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
[IsNoetherian R S]
(I : Ideal R)
:
IsNoetherian (R ⧸ I) (S ⧸ Ideal.map (algebraMap R S) I)
Equations
- (_ : IsNoetherian (R ⧸ I) (S ⧸ Ideal.map (algebraMap R S) I)) = (_ : IsNoetherian (R ⧸ I) (S ⧸ Ideal.map (algebraMap R S) I))
theorem
Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{I : Ideal S}
[IsDomain S]
{r : S}
(r_ne_zero : r ≠ 0)
(hr : r ∈ I)
{p : Polynomial R}
:
p ≠ 0 → Polynomial.eval₂ f r p = 0 → ∃ (i : ℕ), Polynomial.coeff p i ≠ 0 ∧ Polynomial.coeff p i ∈ Ideal.comap f I
theorem
Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{I : Ideal S}
{J : Ideal S}
[Ideal.IsPrime I]
(hIJ : I ≤ J)
{r : S}
(hr : r ∈ ↑J \ ↑I)
{p : Polynomial R}
(p_ne_zero : Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0)
(hpI : Polynomial.eval₂ f r p ∈ I)
:
∃ (i : ℕ), Polynomial.coeff p i ∈ ↑(Ideal.comap f J) \ ↑(Ideal.comap f I)
theorem
Ideal.comap_lt_comap_of_root_mem_sdiff
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{I : Ideal S}
{J : Ideal S}
[Ideal.IsPrime I]
(hIJ : I ≤ J)
{r : S}
(hr : r ∈ ↑J \ ↑I)
{p : Polynomial R}
(p_ne_zero : Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0)
(hp : Polynomial.eval₂ f r p ∈ I)
:
Ideal.comap f I < Ideal.comap f J
theorem
Ideal.comap_lt_comap_of_integral_mem_sdiff
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{I : Ideal S}
{J : Ideal S}
[Algebra R S]
[hI : Ideal.IsPrime I]
(hIJ : I ≤ J)
{x : S}
(mem : x ∈ ↑J \ ↑I)
(integral : IsIntegral R x)
:
Ideal.comap (algebraMap R S) I < Ideal.comap (algebraMap R S) J
theorem
Ideal.comap_ne_bot_of_root_mem
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{f : R →+* S}
{I : Ideal S}
[IsDomain S]
{r : S}
(r_ne_zero : r ≠ 0)
(hr : r ∈ I)
{p : Polynomial R}
(p_ne_zero : p ≠ 0)
(hp : Polynomial.eval₂ f r p = 0)
:
Ideal.comap f I ≠ ⊥
theorem
Ideal.isMaximal_of_isIntegral_of_isMaximal_comap
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
(hRS : Algebra.IsIntegral R S)
(I : Ideal S)
[Ideal.IsPrime I]
(hI : Ideal.IsMaximal (Ideal.comap (algebraMap R S) I))
:
theorem
Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
(f : R →+* S)
(hf : RingHom.IsIntegral f)
(I : Ideal S)
[hI' : Ideal.IsPrime I]
(hI : Ideal.IsMaximal (Ideal.comap f I))
:
theorem
Ideal.comap_ne_bot_of_algebraic_mem
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{I : Ideal S}
[Algebra R S]
[IsDomain S]
{x : S}
(x_ne_zero : x ≠ 0)
(x_mem : x ∈ I)
(hx : IsAlgebraic R x)
:
Ideal.comap (algebraMap R S) I ≠ ⊥
theorem
Ideal.comap_ne_bot_of_integral_mem
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{I : Ideal S}
[Algebra R S]
[Nontrivial R]
[IsDomain S]
{x : S}
(x_ne_zero : x ≠ 0)
(x_mem : x ∈ I)
(hx : IsIntegral R x)
:
Ideal.comap (algebraMap R S) I ≠ ⊥
theorem
Ideal.eq_bot_of_comap_eq_bot
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
{I : Ideal S}
[Algebra R S]
[Nontrivial R]
[IsDomain S]
(hRS : Algebra.IsIntegral R S)
(hI : Ideal.comap (algebraMap R S) I = ⊥)
:
theorem
Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
(hRS : Algebra.IsIntegral R S)
(I : Ideal S)
[hI : Ideal.IsMaximal I]
:
Ideal.IsMaximal (Ideal.comap (algebraMap R S) I)
theorem
Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'
{R : Type u_3}
{S : Type u_4}
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : RingHom.IsIntegral f)
(I : Ideal S)
(hI : Ideal.IsMaximal I)
:
Ideal.IsMaximal (Ideal.comap f I)
theorem
Ideal.IsIntegralClosure.comap_lt_comap
{R : Type u_1}
[CommRing R]
(S : Type u_2)
[CommRing S]
[Algebra R S]
{A : Type u_3}
[CommRing A]
[Algebra R A]
[Algebra A S]
[IsScalarTower R A S]
[IsIntegralClosure A R S]
{I : Ideal A}
{J : Ideal A}
[Ideal.IsPrime I]
(I_lt_J : I < J)
:
Ideal.comap (algebraMap R A) I < Ideal.comap (algebraMap R A) J
theorem
Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap
{R : Type u_1}
[CommRing R]
(S : Type u_2)
[CommRing S]
[Algebra R S]
{A : Type u_3}
[CommRing A]
[Algebra R A]
[Algebra A S]
[IsScalarTower R A S]
[IsIntegralClosure A R S]
(I : Ideal A)
[Ideal.IsPrime I]
(hI : Ideal.IsMaximal (Ideal.comap (algebraMap R A) I))
:
theorem
Ideal.IsIntegralClosure.comap_ne_bot
{R : Type u_1}
[CommRing R]
(S : Type u_2)
[CommRing S]
[Algebra R S]
{A : Type u_3}
[CommRing A]
[Algebra R A]
[Algebra A S]
[IsScalarTower R A S]
[IsIntegralClosure A R S]
[IsDomain A]
[Nontrivial R]
{I : Ideal A}
(I_ne_bot : I ≠ ⊥)
:
Ideal.comap (algebraMap R A) I ≠ ⊥
theorem
Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot
{R : Type u_1}
[CommRing R]
(S : Type u_2)
[CommRing S]
[Algebra R S]
{A : Type u_3}
[CommRing A]
[Algebra R A]
[Algebra A S]
[IsScalarTower R A S]
[IsIntegralClosure A R S]
[IsDomain A]
[Nontrivial R]
{I : Ideal A}
:
Ideal.comap (algebraMap R A) I = ⊥ → I = ⊥
theorem
Ideal.IntegralClosure.comap_lt_comap
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
{I : Ideal ↥(integralClosure R S)}
{J : Ideal ↥(integralClosure R S)}
[Ideal.IsPrime I]
(I_lt_J : I < J)
:
Ideal.comap (algebraMap R ↥(integralClosure R S)) I < Ideal.comap (algebraMap R ↥(integralClosure R S)) J
theorem
Ideal.IntegralClosure.isMaximal_of_isMaximal_comap
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
(I : Ideal ↥(integralClosure R S))
[Ideal.IsPrime I]
(hI : Ideal.IsMaximal (Ideal.comap (algebraMap R ↥(integralClosure R S)) I))
:
theorem
Ideal.IntegralClosure.comap_ne_bot
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
[IsDomain S]
[Nontrivial R]
{I : Ideal ↥(integralClosure R S)}
(I_ne_bot : I ≠ ⊥)
:
Ideal.comap (algebraMap R ↥(integralClosure R S)) I ≠ ⊥
theorem
Ideal.IntegralClosure.eq_bot_of_comap_eq_bot
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
[IsDomain S]
[Nontrivial R]
{I : Ideal ↥(integralClosure R S)}
:
Ideal.comap (algebraMap R ↥(integralClosure R S)) I = ⊥ → I = ⊥
theorem
Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
[IsDomain S]
(H : Algebra.IsIntegral R S)
(P : Ideal R)
[Ideal.IsPrime P]
(hP : RingHom.ker (algebraMap R S) ≤ P)
:
∃ (Q : Ideal S), Ideal.IsPrime Q ∧ Ideal.comap (algebraMap R S) Q = P
comap (algebraMap R S) is a surjection from the prime spec of R to prime spec of S.
hP : (algebraMap R S).ker ≤ P is a slight generalization of the extension being injective
theorem
Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
(H : Algebra.IsIntegral R S)
(P : Ideal R)
[Ideal.IsPrime P]
(I : Ideal S)
[Ideal.IsPrime I]
(hIP : Ideal.comap (algebraMap R S) I ≤ P)
:
∃ Q ≥ I, Ideal.IsPrime Q ∧ Ideal.comap (algebraMap R S) Q = P
More general going-up theorem than exists_ideal_over_prime_of_isIntegral_of_isDomain.
TODO: Version of going-up theorem with arbitrary length chains (by induction on this)?
Not sure how best to write an ascending chain in Lean
theorem
Ideal.exists_ideal_comap_le_prime
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
(P : Ideal R)
[Ideal.IsPrime P]
(I : Ideal S)
(hI : Ideal.comap (algebraMap R S) I ≤ P)
:
∃ Q ≥ I, Ideal.IsPrime Q ∧ Ideal.comap (algebraMap R S) Q ≤ P
theorem
Ideal.exists_ideal_over_prime_of_isIntegral
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
(H : Algebra.IsIntegral R S)
(P : Ideal R)
[Ideal.IsPrime P]
(I : Ideal S)
(hIP : Ideal.comap (algebraMap R S) I ≤ P)
:
∃ Q ≥ I, Ideal.IsPrime Q ∧ Ideal.comap (algebraMap R S) Q = P
theorem
Ideal.exists_ideal_over_maximal_of_isIntegral
{R : Type u_1}
[CommRing R]
{S : Type u_2}
[CommRing S]
[Algebra R S]
(H : Algebra.IsIntegral R S)
(P : Ideal R)
[P_max : Ideal.IsMaximal P]
(hP : RingHom.ker (algebraMap R S) ≤ P)
:
∃ (Q : Ideal S), Ideal.IsMaximal Q ∧ Ideal.comap (algebraMap R S) Q = P
comap (algebraMap R S) is a surjection from the max spec of S to max spec of R.
hP : (algebraMap R S).ker ≤ P is a slight generalization of the extension being injective