Skip to content

Chinese remainder theorem for polynomial quotients

2 fully proved

Ideal

DefinitionChinese remainder theorem as an algebra isomorphism#✓fully proved

Let \(K\) be a commutative semiring, let \(R\) be a commutative ring that is a \(K\)-algebra, and let \((I_i)_{i \in \iota}\) be a family of ideals of \(R\) indexed by a finite type \(\iota\) that are pairwise coprime, that is, \(I_i + I_j = R\) for \(i \ne j\). Then the map sending the class of \(r \in R\) to \((r \bmod I_i)_{i \in \iota}\) is an isomorphism of \(K\)-algebras from \(R / \bigcap_i I_i\) to \(\prod_i R / I_i\).

noncomputable def quotientInfAlgEquivPiQuotient :
    (R ⧸ ⨅ i, I i) ≃ₐ[K] (∀ i, R ⧸ I i) :=
  AlgEquiv.ofRingEquiv (f := Ideal.quotientInfRingEquivPiQuotient I h) (fun c => by
    ext i
    rfl)
Used by 1
Used byBase change of \(K(X)/(f)\) along a factorization of \(f\) over \(K'\)

Adjoin Root

DefinitionBase change of \(K(X)/(f)\) along a factorization of \(f\) over \(K'\)#✓fully proved

Let \(K\) and \(K'\) be fields with \(K'\) a \(K\)-algebra, let \(f \in K[X]\), and let \((g_i)_{i \in \iota}\) be a family of irreducible polynomials in \(K'[X]\), indexed by a finite type \(\iota\), that are pairwise non-associated and whose product \(\prod_i g_i\) is associated (equal up to a unit) to the image of \(f\) in \(K'[X]\). Then there is an isomorphism of \(K'\)-algebras

\[(K[X]/(f)) \otimes_K K' \cong \prod_{i \in \iota} K'[X]/(g_i),\]

where the tensor product is a \(K'\)-algebra through its right factor. For \(p \in K[X]\) with class \([p]\) in \(K[X]/(f)\) and for \(c \in K'\), it sends \([p] \otimes c\) to the family of the classes of \(c\,p\) modulo the \(g_i\), with \(p\) read in \(K'[X]\).

AdjoinRoot.tensorProductAlgEquivPi · 21 lines 
noncomputable def tensorProductAlgEquivPi {K K' : Type*} [Field K] [Field K']
    [Algebra K K'] {ι : Type*} [Fintype ι] (f : Polynomial K)
    (g : ι → Polynomial K') (hirr : ∀ i, Irreducible (g i))
    (hne : Pairwise fun i j => ¬Associated (g i) (g j))
    (hprod : Associated (Polynomial.map (algebraMap K K') f) (∏ i, g i)) :
    letI := Algebra.TensorProduct.rightAlgebra (R := K) (A := AdjoinRoot f)
      (B := K');
    (AdjoinRoot f ⊗[K] K') ≃ₐ[K'] (∀ i, AdjoinRoot (g i)) := by
  letI := Algebra.TensorProduct.rightAlgebra (R := K) (A := AdjoinRoot f)
    (B := K')
  have hprime : ∀ i, Prime (g i) := fun i =>
    UniqueFactorizationMonoid.irreducible_iff_prime.mp (hirr i)
  have hcop : Pairwise fun i j => IsCoprime (g i) (g j) := fun i j hij =>
    (hprime i).coprime_iff_not_dvd.mpr fun hdvd =>
      hne hij ((hprime i).associated_of_dvd (hprime j) hdvd)
  have hspan :
    Ideal.span ({Polynomial.map (algebraMap K K') f} : Set (Polynomial K')) =
      Ideal.span ({∏ i, g i} : Set (Polynomial K')) :=
    Ideal.span_singleton_eq_span_singleton.mpr hprod
  exact ((tensorProductAlgEquiv f).trans
    (Ideal.quotientEquivAlgOfEq K' hspan)).trans (prodAlgEquiv g hcop)
Sources
  • This is the algebraic decomposition in ATLAS N86, Corollary 4.39 of MIT 18.785 Number Theory I. The corresponding upstream declaration is TensorSplitting.adjoinRoot_tensor_algEquiv_prod. There, L is presented as K[X] / (f), the extension K' / K is arbitrary, and the distinct irreducible factors of f over K' are represented here by g, hirr, hne, and hprod. The source assumes that f is irreducible and separable in order to say that L / K is a finite separable field extension. Those assumptions are not needed for this CRT decomposition of the explicitly presented algebra AdjoinRoot f; accordingly, this theorem makes no stronger field or finite-etale claim about its factors.
Uses 1
Statement usesChinese remainder theorem as an algebra isomorphism

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.