Theorems · Definition · commutative algebra

IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv

{R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : IsDedekindDomain A] →
          {I : Ideal R} →
            {J : Ideal A} →
              [inst_3 : IsDedekindDomain R] →
                R ⧸ I ≃+* A ⧸ J →
                  I ≠ ⊥ →
                    J ≠ ⊥ →
                      ↑{L | L ∈ UniqueFactorizationMonoid.normalizedFactors I} ≃
                        ↑{M | M ∈ UniqueFactorizationMonoid.normalizedFactors J}

The bijection between the sets of normalized factors of I and J induced by a ring isomorphism f : R/I ≅ A/J.

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingCommRingIsDedekindDomainIsDedekindDomain