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.

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)

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

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

• over : p = under A P

theorem Ideal.liesOver_iff {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

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_6} [FunLike F B C] [AlgHomClass F A B C] (f : F) (h : P = 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_6} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) (h : Q = map σ P) : Q.LiesOver p

instance Ideal.LiesOver.smul {A : Type u_2} [CommSemiring A] {B : Type u_3} [Semiring B] [Algebra A B] {P : Ideal B} {p : Ideal A} {G : Type u_5} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (g : G) [h : P.LiesOver p] : (g • P).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_6} [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_6} [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] : P.LiesOver p

theorem Ideal.map_under_le_under_map {A : Type u_2} [CommSemiring A] {B : Type u_3} [CommSemiring B] [Algebra A B] (P : Ideal B) {C : Type u_5} {D : Type u_6} [CommSemiring C] [Semiring D] [Algebra A C] [Algebra C D] [Algebra A D] [Algebra B D] [IsScalarTower A C D] [IsScalarTower A B D] : map (algebraMap A C) (under A P) ≤ under C (map (algebraMap B D) P)

Consider the following commutative diagram of ring maps

A → B
↓   ↓
C → D

and let P be an ideal of B. The image in C of the ideal of A under P is included in the ideal of C under the image of P in D.

theorem Ideal.under_map_eq_map_under {A : Type u_2} [CommSemiring A] {B : Type u_3} [CommSemiring B] [Algebra A B] (P : Ideal B) {C : Type u_5} {D : Type u_6} [CommSemiring C] [Semiring D] [Algebra A C] [Algebra C D] [Algebra A D] [Algebra B D] [IsScalarTower A C D] [IsScalarTower A B D] (h₁ : (map (algebraMap A C) (under A P)).IsMaximal) (h₂ : map (algebraMap B D) P ≠ ⊤) : under C (map (algebraMap B D) P) = map (algebraMap A C) (under A P)

Consider the following commutative diagram of ring maps

A → B
↓   ↓
C → D

and let P be an ideal of B. Assume that the image in C of the ideal of A under P is maximal and that the image of P in D is not equal to D, then the image in C of the ideal of A under P is equal to the ideal of C under the image of P in D.

theorem Ideal.disjoint_primeCompl_of_liesOver {A : Type u_2} [CommSemiring A] {C : Type u_4} [Semiring C] [Algebra A C] (𝔓 : Ideal C) (p : Ideal A) [p.IsPrime] [hPp : 𝔓.LiesOver p] : Disjoint ↑(Algebra.algebraMapSubmonoid C p.primeCompl) ↑𝔓

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

@[simp]

theorem Ideal.Quotient.algebraMap_mk_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] (x : A) : (algebraMap (A ⧸ p) (B ⧸ P)) ((mk p) x) = (mk P) ((algebraMap A B) x)

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

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

@[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 σ ⋯

@[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.

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

theorem Ideal.Quotient.ker_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] : (stabilizerHom P p G).ker = ((Submodule.toAddSubgroup P).inertia G).subgroupOf (MulAction.stabilizer G P)

theorem Ideal.Quotient.map_ker_stabilizer_subtype {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] : Subgroup.map (MulAction.stabilizer G P).subtype (stabilizerHom P p G).ker = (Submodule.toAddSubgroup P).inertia G

def Ideal.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

• p.primesOver B = {P : Ideal B | P.IsPrime ∧ P.LiesOver p}

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

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

@[reducible, inline]

abbrev Ideal.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] : ↑(p.primesOver B)

If an ideal P of B is prime and lying over p, then it is in primesOver p B.

Equations

• Ideal.primesOver.mk p P = ⟨P, ⋯⟩

theorem Ideal.ne_bot_of_mem_primesOver {R : Type u_1} [CommRing R] {S : Type u_4} [Ring S] [Algebra R S] [Nontrivial S] [NoZeroSMulDivisors R S] {p : Ideal R} (hp : p ≠ ⊥) {P : Ideal S} (hP : P ∈ p.primesOver S) : P ≠ ⊥