13 Commutative algebra

TheoremGoing-up and going-down theorems#

Mathlib records this with 4 declarations.

Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain: 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

Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain.{u_1, u_2} {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, Q.IsPrime ∧ Ideal.under R Q = P

Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime: More general going-up theorem than exists_ideal_over_prime_of_isIntegral_of_isDomain. Generalized to arbitrary length chains in Ideal.exists_ltSeries_of_hasGoingUp.

Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime.{u_1, u_2} {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.under R I ≤ P) : ∃ Q ≥ I, Q.IsPrime ∧ Ideal.under R Q = P

Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap: An R-algebra S has the going down property if and only if generalizations lift along Spec S → Spec R.

Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.{u_3, u_4} {R : Type u_3} {S : Type u_4}
  [CommRing R] [CommRing S] [Algebra R S] :
  Algebra.HasGoingDown R S ↔ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))

Algebra.HasGoingDown.of_comap_localRingHom_surjective: If for every prime of S, the map Spec Sₚ → Spec Rₚ is surjective, the algebra satisfies going down.

Algebra.HasGoingDown.of_comap_localRingHom_surjective.{u_3, u_4} {R : Type u_3} {S : Type u_4}
  [CommRing R] [CommRing S] [Algebra R S]
  (H :
    ∀ (P : Ideal S) [inst : P.IsPrime],
      Function.Surjective
        (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))) :
  Algebra.HasGoingDown R S
Sources
MathlibIdeal.exists_ideal_over_prime_of_isIntegral_of_isDomain · Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime · Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap · Algebra.HasGoingDown.of_comap_localRingHom_surjective
Uses 9
Statement usesAssociative algebra over a commutative ring · Filter · Localization · Polynomial in one indeterminate · Zariski topology
Proof usesGenerating sets · Local ring · Quotient space (Fundamentals) · Sum of subspaces

TheoremJacobson density theorem#

Mathlib states this as jacobson_density.

jacobson_density.{u_2, u_4} {R : Type u_2} [Ring R] {M : Type u_4} [AddCommGroup M]
  [_root_.Module R M] [IsSemisimpleModule R M] (f : Module.End (Module.End R M) M) (s : Finset M) :
  ∃ r, ∀ m ∈ s, f m = r • m
Sources
Mathlibjacobson_density
Uses 10
Statement usesFinite set · Integer · Linear map · Sum of subspaces
Proof usesFinitely supported function · Generating sets · Kernel of a linear map · Product of vector spaces · Quotient space (Fundamentals) · Range of a linear map

TheoremKrull's principal ideal theorem#

Krull's principal ideal theorem (also known as Krullscher Hauptidealsatz) : In a commutative Noetherian ring R, any prime ideal that is minimal over a principal ideal has height at most 1.

Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes.{u_1} {R : Type u_1} [CommRing R]
  [IsNoetherianRing R] (I : Ideal R) [Submodule.IsPrincipal I] (p : Ideal R)
  (hp : p ∈ I.minimalPrimes) : p.height ≤ 1
Sources
MathlibIdeal.height_le_one_of_isPrincipal_of_mem_minimalPrimes
Uses 11
Statement usesNoetherian ring · Prime spectrum · Principal ideal domain
Proof usesAssociative algebra over a commutative ring · Characteristic zero · Local ring · Localization · Noetherian module · Polynomial in one indeterminate · Quotient space (Fundamentals) · Sum of subspaces

TheoremLasker–Noether theorem#

Mathlib states this as Submodule.isPrimary_decomposition_pairwise_ne_radical.

Submodule.isPrimary_decomposition_pairwise_ne_radical.{u_1, u_2} {R : Type u_1} {M : Type u_2}
  [CommSemiring R] [AddCommMonoid M] [_root_.Module R M] {N : Submodule R M}
  {s : Finset (Submodule R M)} (hs : s.inf id = N)
  (hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary) :
  ∃ t,
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t).Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) fun J => (J.colon Set.univ).radical)
Sources
MathlibSubmodule.isPrimary_decomposition_pairwise_ne_radical
Uses 4
Statement usesFinite set · Ideal of a commutative ring · Linear map · Sum of subspaces

TheoremVieta's formulas#

A sum version of Vieta's formula for Multiset: the product of the linear terms X + λ where λ runs through a multiset s is equal to a linear combination of the symmetric functions esymm s of the λ's .

Multiset.prod_X_add_C_eq_sum_esymm.{u_1} {R : Type u_1} [CommSemiring R] (s : Multiset R) :
  (Multiset.map (fun r => Polynomial.X + Polynomial.C r) s).prod =
    ∑ j ∈ Finset.range (s.card + 1), Polynomial.C (s.esymm j) * Polynomial.X ^ (s.card - j)
Sources
MathlibMultiset.prod_X_add_C_eq_sum_esymm
Uses 2 · Used by 1
Statement usesLinear map · Polynomial in one indeterminate
Used byRelationship between the coefficients and the roots of a split polynomial

InstanceWedderburn's little theorem#

A finite division ring is a field. See Finite.isDomain_to_isField and Fintype.divisionRingOfIsDomain for more general statements, but these create data, and therefore may cause diamonds if used improperly.

littleWedderburn.{u_1} (D : Type u_1) [DivisionRing D] [Finite D] : Field D
Sources
MathliblittleWedderburn
Uses 2
Statement usesField · Rational number

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.