Theorems · Definition · commutative algebra

Polynomial.UniversalCoprimeFactorizationRing.homEquiv

{R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {n : ℕ} →
            (m k : ℕ) →
              (hn : n = m + k) →
                (p : Polynomial.MonicDegreeEq R n) →
                  (Polynomial.UniversalCoprimeFactorizationRing m k hn p →ₐ[R] S) ≃
                    { q // ↑q.1 * ↑q.2 = Polynomial.map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }

The universal factorization ring represents S ↦ "factorizations of p into coprime (monic deg m) * (monic deg k) in S".

Defined in

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra