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) : p.coeff 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) : p.coeff 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 : ℕ), p.coeff i ≠ 0 ∧ p.coeff 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))) ⋯)

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)) : ((Ideal.Quotient.mk (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)).comp Polynomial.C).comp (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) = (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))) ⋯).comp ((Ideal.Quotient.mk P).comp 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 Mathlib.RingTheory.Jacobson.Polynomial.

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.

instance Ideal.Quotient.algebraQuotientMapQuotient {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {p : Ideal R} [Algebra R S] : Algebra (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)

R / p has a canonical map to S / pS.

Equations

• Ideal.Quotient.algebraQuotientMapQuotient = Ideal.Quotient.algebraQuotientOfLEComap ⋯

@[simp]

theorem Ideal.Quotient.algebraMap_quotient_map_quotient {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {p : Ideal R} [Algebra R S] (x : R) : (algebraMap (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((algebraMap R S) x)

@[simp]

theorem Ideal.Quotient.mk_smul_mk_quotient_map_quotient {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {p : Ideal R} [Algebra R S] (x : R) (y : S) : (Ideal.Quotient.mk p) x • (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) y = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((algebraMap R S) 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)

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)

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 : ℕ), p.coeff i ≠ 0 ∧ p.coeff 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 J : Ideal S} [I.IsPrime] (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 : ℕ), p.coeff 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 J : Ideal S} [I.IsPrime] (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.mem_of_one_mem {S : Type u_2} [CommRing S] {I : Ideal S} (h : 1 ∈ I) (x : S) : x ∈ I

theorem Ideal.comap_lt_comap_of_integral_mem_sdiff {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {I J : Ideal S} [Algebra R S] [hI : I.IsPrime] (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] [Algebra.IsIntegral R S] (I : Ideal S) [I.IsPrime] (hI : (Ideal.comap (algebraMap R S) I).IsMaximal) : I.IsMaximal

theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap' {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (I : Ideal S) [I.IsPrime] (hI : (Ideal.comap f I).IsMaximal) : I.IsMaximal

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] [Algebra.IsIntegral R S] (hI : Ideal.comap (algebraMap R S) I = ⊥) : I = ⊥

theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (I : Ideal S) [hI : I.IsMaximal] : (Ideal.comap (algebraMap R S) I).IsMaximal

theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal' {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.IsIntegral) (I : Ideal S) [I.IsMaximal] : (Ideal.comap f I).IsMaximal

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 J : Ideal A} [I.IsPrime] (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) [I.IsPrime] (hI : (Ideal.comap (algebraMap R A) I).IsMaximal) : I.IsMaximal

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 J : Ideal ↥(integralClosure R S)} [I.IsPrime] (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)) [I.IsPrime] (hI : (Ideal.comap (algebraMap R ↥(integralClosure R S)) I).IsMaximal) : I.IsMaximal

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] [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (hP : RingHom.ker (algebraMap R S) ≤ P) : ∃ (Q : Ideal S), Q.IsPrime ∧ 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] [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (I : Ideal S) [I.IsPrime] (hIP : Ideal.comap (algebraMap R S) I ≤ P) : ∃ Q ≥ I, Q.IsPrime ∧ 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) [P.IsPrime] (I : Ideal S) (hI : Ideal.comap (algebraMap R S) I ≤ P) : ∃ Q ≥ I, Q.IsPrime ∧ 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] [Algebra.IsIntegral R S] (P : Ideal R) [P.IsPrime] (I : Ideal S) (hIP : Ideal.comap (algebraMap R S) I ≤ P) : ∃ Q ≥ I, Q.IsPrime ∧ 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] [Algebra.IsIntegral R S] (P : Ideal R) [P_max : P.IsMaximal] (hP : RingHom.ker (algebraMap R S) ≤ P) : ∃ (Q : Ideal S), Q.IsMaximal ∧ 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

theorem Ideal.map_eq_top_iff_of_ker_le {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal R} (hf₁ : RingHom.ker f ≤ I) (hf₂ : f.IsIntegral) : Ideal.map f I = ⊤ ↔ I = ⊤

theorem Ideal.map_eq_top_iff {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal R} (hf₁ : Function.Injective ⇑f) (hf₂ : f.IsIntegral) : Ideal.map f I = ⊤ ↔ I = ⊤

@[reducible, inline]

abbrev Ideal.under (A : Type u_2) [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) : Ideal A

The ideal obtained by pulling back the ideal P from B to A.

Equations

• Ideal.under A P = Ideal.comap (algebraMap A B) P

theorem Ideal.under_def (A : Type u_2) [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) : Ideal.under A P = Ideal.comap (algebraMap A B) P

instance Ideal.IsPrime.under (A : Type u_2) [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) [hP : P.IsPrime] : (Ideal.under A P).IsPrime

@[simp]

theorem Ideal.under_smul (A : Type u_2) [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) {G : Type u_5} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (g : G) : Ideal.under A (g • P) = Ideal.under A P

theorem Ideal.under_top (A : Type u_2) [CommSemiring A] (B : Type u_3) [Semiring B] [Algebra A B] : Ideal.under A ⊤ = ⊤

class Ideal.LiesOver {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) (p : Ideal A) : Prop

P lies over p if p is the preimage of P of the algebraMap.

• over : p = Ideal.under A P

instance Ideal.over_under {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) : P.LiesOver (Ideal.under A P)

theorem Ideal.over_def {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] : p = Ideal.under A P

theorem Ideal.mem_of_liesOver {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] (x : A) : x ∈ p ↔ (algebraMap A B) x ∈ P

instance Ideal.top_liesOver_top (A : Type u_2) [CommSemiring A] (B : Type u_3) [Semiring B] [Algebra A B] : ⊤.LiesOver ⊤

theorem Ideal.eq_top_iff_of_liesOver {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] : P = ⊤ ↔ p = ⊤

theorem Ideal.LiesOver.of_eq_comap {A : Type u_2} [CommSemiring A] {B : Type u_3} {C : Type u_4} [Semiring B] [Semiring C] [Algebra A B] [Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [Q.LiesOver p] {F : Type u_5} [FunLike F B C] [AlgHomClass F A B C] (f : F) (h : P = Ideal.comap f Q) : P.LiesOver p

theorem Ideal.LiesOver.of_eq_map_equiv {A : Type u_2} [CommSemiring A] {B : Type u_3} {C : Type u_4} [Semiring B] [Semiring C] [Algebra A B] [Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [P.LiesOver p] {E : Type u_5} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : Q = Ideal.map σ P) : Q.LiesOver p

instance Ideal.comap_liesOver {A : Type u_2} [CommSemiring A] {B : Type u_3} {C : Type u_4} [Semiring B] [Semiring C] [Algebra A B] [Algebra A C] (Q : Ideal C) (p : Ideal A) [Q.LiesOver p] {F : Type u_5} [FunLike F B C] [AlgHomClass F A B C] (f : F) : (Ideal.comap f Q).LiesOver p

instance Ideal.map_equiv_liesOver {A : Type u_2} [CommSemiring A] {B : Type u_3} {C : Type u_4} [Semiring B] [Semiring C] [Algebra A B] [Algebra A C] (P : Ideal B) (p : Ideal A) [P.LiesOver p] {E : Type u_5} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) : (Ideal.map σ P).LiesOver p

@[simp]

theorem Ideal.under_under {A : Type u_2} [CommSemiring A] {B : Type u_3} [CommSemiring B] {C : Type u_4} [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) : Ideal.under A (Ideal.under B 𝔓) = Ideal.under A 𝔓

theorem Ideal.LiesOver.trans {A : Type u_2} [CommSemiring A] {B : Type u_3} [CommSemiring B] {C : Type u_4} [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (P : Ideal B) (p : Ideal A) [𝔓.LiesOver P] [P.LiesOver p] : 𝔓.LiesOver p

theorem Ideal.LiesOver.tower_bot {A : Type u_2} [CommSemiring A] {B : Type u_3} [CommSemiring B] {C : Type u_4} [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (P : Ideal B) (p : Ideal A) [hp : 𝔓.LiesOver p] [hP : 𝔓.LiesOver P] : P.LiesOver p

instance Ideal.under_liesOver_of_liesOver {A : Type u_2} [CommSemiring A] (B : Type u_3) [CommSemiring B] {C : Type u_4} [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (p : Ideal A) [𝔓.LiesOver p] : (Ideal.under B 𝔓).LiesOver p

@[simp]

theorem Ideal.under_bot (A : Type u_2) [CommRing A] (B : Type u_3) [Ring B] [Nontrivial B] [Algebra A B] [NoZeroSMulDivisors A B] : Ideal.under A ⊥ = ⊥

instance Ideal.bot_liesOver_bot (A : Type u_2) [CommRing A] (B : Type u_3) [Ring B] [Nontrivial B] [Algebra A B] [NoZeroSMulDivisors A B] : ⊥.LiesOver ⊥

theorem Ideal.ne_bot_of_liesOver_of_ne_bot {A : Type u_2} [CommRing A] {B : Type u_3} [Ring B] [Nontrivial B] [Algebra A B] [NoZeroSMulDivisors A B] {p : Ideal A} (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] : P ≠ ⊥

instance Ideal.Quotient.algebraOfLiesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] : Algebra (A ⧸ p) (B ⧸ P)

If P lies over p, then canonically B ⧸ P is a A ⧸ p-algebra.

Equations

• Ideal.Quotient.algebraOfLiesOver P p = Ideal.Quotient.algebraQuotientOfLEComap ⋯

instance Ideal.Quotient.isScalarTower_of_liesOver (R : Type u_2) [CommSemiring R] {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] [Algebra R A] [Algebra R B] [IsScalarTower R A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] : IsScalarTower R (A ⧸ p) (B ⧸ P)

instance Ideal.Quotient.module_finite_of_liesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [Module.Finite A B] : Module.Finite (A ⧸ p) (B ⧸ P)

B ⧸ P is a finite A ⧸ p-module if B is a finite A-module.

instance Ideal.Quotient.algebra_finiteType_of_liesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [Algebra.FiniteType A B] : Algebra.FiniteType (A ⧸ p) (B ⧸ P)

B ⧸ P is a finitely generated A ⧸ p-algebra if B is a finitely generated A-algebra.

instance Ideal.Quotient.isNoetherian_of_liesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [IsNoetherian A B] : IsNoetherian (A ⧸ p) (B ⧸ P)

B ⧸ P is a Noetherian A ⧸ p-module if B is a Noetherian A-module.

theorem Ideal.Quotient.algebraMap_injective_of_liesOver {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] : Function.Injective ⇑(algebraMap (A ⧸ p) (B ⧸ P))

instance Ideal.Quotient.instNoZeroSMulDivisorsQuotientOfIsPrime {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [P.IsPrime] : NoZeroSMulDivisors (A ⧸ p) (B ⧸ P)

theorem Ideal.Quotient.nontrivial_of_liesOver_of_ne_top {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) {p : Ideal A} [P.LiesOver p] (hp : p ≠ ⊤) : Nontrivial (B ⧸ P)

theorem Ideal.Quotient.nontrivial_of_liesOver_of_isPrime {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [hp : p.IsPrime] : Nontrivial (B ⧸ P)

def Ideal.Quotient.algEquivOfEqMap {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [Q.LiesOver p] [P.LiesOver p] {E : Type u_7} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : Q = Ideal.map σ P) : (B ⧸ P) ≃ₐ[A ⧸ p] C ⧸ Q

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' := ⋯ }

@[simp]

theorem Ideal.Quotient.algEquivOfEqMap_apply {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [Q.LiesOver p] [P.LiesOver p] {E : Type u_7} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : Q = Ideal.map σ P) (x : B) : (Ideal.Quotient.algEquivOfEqMap p σ h) ((Ideal.Quotient.mk P) x) = (Ideal.Quotient.mk Q) (σ x)

def Ideal.Quotient.algEquivOfEqComap {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [Q.LiesOver p] [P.LiesOver p] {E : Type u_7} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : P = Ideal.comap σ Q) : (B ⧸ P) ≃ₐ[A ⧸ p] C ⧸ Q

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

• Ideal.Quotient.algEquivOfEqComap p σ h = Ideal.Quotient.algEquivOfEqMap p σ ⋯

@[simp]

theorem Ideal.Quotient.algEquivOfEqComap_apply {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [Q.LiesOver p] [P.LiesOver p] {E : Type u_7} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : P = Ideal.comap σ Q) (x : B) : (Ideal.Quotient.algEquivOfEqComap p σ h) ((Ideal.Quotient.mk P) x) = (Ideal.Quotient.mk Q) (σ x)

def Ideal.Quotient.stabilizerHom {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] (G : Type u_6) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] : ↥(MulAction.stabilizer G P) →* (B ⧸ P) ≃ₐ[A ⧸ p] B ⧸ P

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.

@[simp]

theorem Ideal.Quotient.stabilizerHom_apply {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] (G : Type u_6) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (g : ↥(MulAction.stabilizer G P)) (b : B) : ((Ideal.Quotient.stabilizerHom P p G) g) ((Ideal.Quotient.mk P) b) = (Ideal.Quotient.mk P) (g • b)

instance Ideal.IsMaximal.under (A : Type u_2) [CommRing A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (P : Ideal B) [P.IsMaximal] : (Ideal.under A P).IsMaximal

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.

theorem Ideal.IsMaximal.of_liesOver_isMaximal {A : Type u_2} [CommRing A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [hpm : p.IsMaximal] [P.IsPrime] : P.IsMaximal

theorem Ideal.IsMaximal.of_isMaximal_liesOver {A : Type u_2} [CommRing A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [P.IsMaximal] : p.IsMaximal

instance Ideal.Quotient.algebra_isIntegral_of_liesOver {A : Type u_2} [CommRing A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] : Algebra.IsIntegral (A ⧸ p) (B ⧸ P)

B ⧸ P is an integral A ⧸ p-algebra if B is a integral A-algebra.

theorem Ideal.exists_ideal_liesOver_maximal_of_isIntegral {A : Type u_2} [CommRing A] (p : Ideal A) [p.IsMaximal] (B : Type u_4) [CommRing B] [Nontrivial B] [Algebra A B] [NoZeroSMulDivisors A B] [Algebra.IsIntegral A B] : ∃ (P : Ideal B), P.IsMaximal ∧ P.LiesOver p

def primesOver {A : Type u_2} [CommSemiring A] (p : Ideal A) (B : Type u_3) [Semiring B] [Algebra A B] : Set (Ideal B)

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}

instance primesOver.isPrime {A : Type u_2} [CommSemiring A] (p : Ideal A) {B : Type u_3} [Semiring B] [Algebra A B] (Q : ↑(primesOver p B)) : (↑Q).IsPrime

instance primesOver.liesOver {A : Type u_2} [CommSemiring A] (p : Ideal A) {B : Type u_3} [Semiring B] [Algebra A B] (Q : ↑(primesOver p B)) : (↑Q).LiesOver p

@[reducible, inline]

abbrev primesOver.mk {A : Type u_2} [CommSemiring A] (p : Ideal A) {B : Type u_3} [Semiring B] [Algebra A B] (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] : ↑(primesOver p B)

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, ⋯⟩

instance primesOver.isMaximal {A : Type u_2} [CommRing A] {p : Ideal A} [p.IsMaximal] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] (Q : ↑(primesOver p B)) : (↑Q).IsMaximal

theorem primesOver_bot (A : Type u_2) [CommRing A] (B : Type u_3) [CommRing B] [Algebra A B] [NoZeroSMulDivisors A B] [Algebra.IsIntegral A B] [Nontrivial A] [IsDomain B] : primesOver ⊥ B = {⊥}