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)))
:
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.
@[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)
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
Instances For
theorem
Ideal.under_def
(A : Type u_2)
[CommSemiring A]
{B : Type u_3}
[Semiring B]
[Algebra A B]
(P : Ideal B)
:
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)
:
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 by the algebraMap.
Instances
instance
Ideal.over_under
{A : Type u_2}
[CommSemiring A]
{B : Type u_3}
[Semiring B]
[Algebra A B]
(P : Ideal B)
:
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)
:
instance
Ideal.top_liesOver_top
(A : Type u_2)
[CommSemiring A]
(B : Type u_3)
[Semiring B]
[Algebra A B]
:
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]
:
@[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)
:
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]
:
@[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]
:
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]
:
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)
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)
:
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)
:
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)
:
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
@[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)
:
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]
:
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)
:
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, ⋯⟩
Instances For
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)
: