Theorems · Definition · commutative algebra

IsDedekindDomain.HeightOneSpectrum.quotientEquivPiOfProdEq

{R : Type u_1} →
  [inst : CommRing R] →
    {ι : Type u_4} →
      [IsDedekindDomain R] →
        [inst_2 : Fintype ι] →
          (I : Ideal R) →
            (P : ι → IsDedekindDomain.HeightOneSpectrum R) →
              (e : ι → ℕ) →
                (Pairwise fun i j => P i ≠ P j) →
                  ∏ i, (P i).asIdeal ^ e i = I → R ⧸ I ≃+* ((i : ι) → R ⧸ (P i).asIdeal ^ e i)

Chinese remainder theorem for a Dedekind domain: if the ideal I factors as ∏ i, P i ^ e i, then R ⧸ I factors as Π i, R ⧸ (P i ^ e i). See IsDedekindDomain.quotientEquivPiOfProdEq for the version in terms of Ideal R.

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Cited by

0 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDedekindDomainFintype