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.
Let P
be an ideal in R[x]
. The map
R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R))
is injective.
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 Mathlib.RingTheory.Jacobson.Polynomial
.
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)
.
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
.
R / p
has a canonical map to S / pS
.
Equations
- Ideal.Quotient.algebraQuotientMapQuotient = Ideal.Quotient.algebraQuotientOfLEComap ⋯
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
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
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
The ideal obtained by pulling back the ideal P
from B
to A
.
Equations
- Ideal.under A P = Ideal.comap (algebraMap A B) P
Instances For
P
lies over p
if p
is the preimage of P
of the algebraMap
.
- over : p = Ideal.under A P
Instances
B ⧸ P
is a finite A ⧸ p
-module if B
is a finite A
-module.
B ⧸ P
is a finitely generated A ⧸ p
-algebra if B
is a finitely generated A
-algebra.
B ⧸ P
is a Noetherian A ⧸ p
-module if B
is a Noetherian A
-module.
An A ⧸ p
-algebra isomorphism between B ⧸ P
and C ⧸ Q
induced by an A
-algebra
isomorphism between B
and C
, where Q = σ P
.
Equations
- Ideal.Quotient.algEquivOfEqMap p σ h = { toEquiv := (P.quotientEquiv Q (↑σ) h).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
An A ⧸ p
-algebra isomorphism between B ⧸ P
and C ⧸ Q
induced by an A
-algebra
isomorphism between B
and C
, where P = σ⁻¹ Q
.
Equations
Instances For
If P
lies over p
, then the stabilizer of P
acts on the extension (B ⧸ P) / (A ⧸ p)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If B
is an integral A
-algebra, P
is a maximal ideal of B
, then the pull back of
P
is also a maximal ideal of A
.
B ⧸ P
is an integral A ⧸ p
-algebra if B
is a integral A
-algebra.
The set of all prime ideals in B
that lie over an ideal p
of A
.
Equations
- primesOver p B = {P : Ideal B | P.IsPrime ∧ P.LiesOver p}
Instances For
If an ideal P
of B
is prime and lying over p
, then it is in primesOver p B
.
Equations
- primesOver.mk p P = ⟨P, ⋯⟩