Theorems · Definition · commutative algebra

FractionalIdeal.quotientEquiv

{R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [IsFractionRing R K] →
            [IsDedekindDomain R] →
              (I J I' J' : FractionalIdeal (nonZeroDivisors R) K) →
                I * J' = I' * J →
                  J ≤ I →
                    J' ≤ I' →
                      J' ≠ 0 →
                        I ≠ 0 → (↥↑I ⧸ Submodule.comap (↑I).subtype ↑J) ≃ₗ[R] ↥↑I' ⧸ Submodule.comap (↑I').subtype ↑J'

Let I J I' J' be nonzero fractional ideals in a Dedekind domain with J ≤ I and J' ≤ I'. If I/J = I'/J' in the group of fractional ideals (i.e. I * J' = I' * J), then I/J ≃ I'/J' as quotient R-modules.

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsFractionRingIsDedekindDomain