Documentation

Mathlib.RingTheory.Ideal.Over

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.comap_map_eq_self_iff_of_isPrime {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] {f : R →+* S} (p : Ideal R) [p.IsPrime] :

comap f (map f p) = p ↔ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p

For a prime ideal p of R, p extended to S and restricted back to R is p if and only if p is the restriction of a prime in S.

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 ∈ 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 ∈ 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 ∈ comap f I

theorem Ideal.injective_quotient_le_comap_map {R : Type u_1} [CommRing R] (P : Ideal (Polynomial R)) :

Function.Injective ⇑(quotientMap (map (Polynomial.mapRingHom (Quotient.mk (comap Polynomial.C P))) P) (Polynomial.mapRingHom (Quotient.mk (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)) :

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

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 ⧸ 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 ⧸ map (algebraMap R S) p)) ((mk p) x) = (mk (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) :

(mk p) x • (mk (map (algebraMap R S) p)) y = (mk (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 ⧸ 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 ⧸ 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 ∈ 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 (Quotient.mk (comap f I)) p ≠ 0) (hpI : Polynomial.eval₂ f r p ∈ I) :

∃ (i : ℕ), p.coeff i ∈ ↑(comap f J) \ ↑(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 (Quotient.mk (comap f I)) p ≠ 0) (hp : Polynomial.eval₂ f r p ∈ I) :

comap f I < 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) :

comap (algebraMap R S) I < 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) :

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 : (comap (algebraMap R S) 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 : (comap f 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) :

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) :

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

(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] :

(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) :

comap (algebraMap R A) I < 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 : (comap (algebraMap R A) 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 ≠ ⊥) :

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} :

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) :

comap (algebraMap R ↥(integralClosure R S)) I < 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 : (comap (algebraMap R ↥(integralClosure R S)) 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 ≠ ⊥) :

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)} :

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 ∧ 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 : comap (algebraMap R S) I ≤ P) :

∃ Q ≥ I, Q.IsPrime ∧ 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 : comap (algebraMap R S) I ≤ P) :

∃ Q ≥ I, Q.IsPrime ∧ 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 : comap (algebraMap R S) I ≤ P) :

∃ Q ≥ I, Q.IsPrime ∧ 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 ∧ 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) :

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) :

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) :

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

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

under A P = 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) :

under A (g • P) = under A P

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

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) :

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

over : p = under A P

Instances

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

P.LiesOver (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 = 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 = comap f Q) :

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 = map σ 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) :

(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) :

(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) :

under A (under B 𝔓) = 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] :

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] :

(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] :

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] :

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.

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

FaithfulSMul (A ⧸ p) (B ⧸ P)

@[deprecated Ideal.Quotient.instFaithfulSMul (since := "2025-01-31")]

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] :

FaithfulSMul (A ⧸ p) (B ⧸ P)

Alias of Ideal.Quotient.instFaithfulSMul.

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

Instances For

@[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 = map σ P) (x : B) :

(algEquivOfEqMap p σ h) ((mk P) x) = (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 = 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 σ ⋯

Instances For

@[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 = comap σ Q) (x : B) :

(algEquivOfEqComap p σ h) ((mk P) x) = (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.

Instances For

@[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) :

((stabilizerHom P p G) g) ((mk P) b) = (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] :

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] :

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] :

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

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

Instances For

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 = {⊥}