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.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 = 0x = 0) (hr : r I) {p : Polynomial R} :
p 0Polynomial.eval₂ f r p = 0∃ (i : ), p.coeff i 0 p.coeff i Ideal.comap f I

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 Px = 0) :
pP, 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))) :

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
@[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) :
@[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) :
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] :
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) :
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 0Polynomial.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) :
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) :
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) :
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) :
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) :
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) :
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 ) :
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} :
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) :
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 ) :
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) :
QI, 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) :
QI, 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) :
QI, 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) :
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) :
@[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
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) :
    theorem Ideal.under_top (A : Type u_2) [CommSemiring A] (B : Type u_3) [Semiring B] [Algebra A B] :
    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.

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

      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] :
      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] :
      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 ) :
      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] :
      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
      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 = Ideal.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 = 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
        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 = Ideal.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.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] :

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