Universal factorization ring

Let R be a commutative ring and p : R[X] be monic of degree n and let n = m + k. We construct the universal ring of the following functors on R-Alg:

• S ↦ "monic polynomials over S of degree n": Represented by R[X₁,...,Xₙ]. See MvPolynomial.mapEquivMonic.
• S ↦ "factorizations of p into (monic deg m) * (monic deg k) in S": Represented by an R-algebra (Polynomial.UniversalFactorizationRing) that is finitely-presented as an R-module. See Polynomial.UniversalFactorizationRing.homEquiv.
• S ↦ "factorizations of p into coprime (monic deg m) * (monic deg k) in S": Represented by an etale R-algebra (TODO).

def Polynomial.freeMonic (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial (MvPolynomial (Fin n) R)

The free monic polynomial of degree n, as a polynomial in R[X₁,...,Xₙ][X].

Equations

• Polynomial.freeMonic R n = Polynomial.X ^ n + ∑ i : Fin n, Polynomial.C (MvPolynomial.X i) * Polynomial.X ^ ↑i

theorem Polynomial.coeff_freeMonic (R : Type u_1) [CommRing R] (n k : ℕ) : (freeMonic R n).coeff k = if h : k < n then MvPolynomial.X ⟨k, h⟩ else if k = n then 1 else 0

theorem Polynomial.degree_freeMonic (R : Type u_1) [CommRing R] (n : ℕ) [Nontrivial R] : (freeMonic R n).degree = ↑n

theorem Polynomial.natDegree_freeMonic (R : Type u_1) [CommRing R] (n : ℕ) [Nontrivial R] : (freeMonic R n).natDegree = n

theorem Polynomial.monic_freeMonic (R : Type u_1) [CommRing R] (n : ℕ) : (freeMonic R n).Monic

theorem Polynomial.map_map_freeMonic (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] (n : ℕ) (f : R →+* S) : map (MvPolynomial.map f) (freeMonic R n) = freeMonic S n

def Polynomial.MonicDegreeEq.freeMonic (R : Type u_1) [CommRing R] (n : ℕ) : MonicDegreeEq (MvPolynomial (Fin n) R) n

The free monic polynomial of degree n, as a MonicDegreeEq in R[X₁,...,Xₙ][X].

Equations

• Polynomial.MonicDegreeEq.freeMonic R n = ⟨Polynomial.freeMonic R n, ⋯⟩

@[simp]

theorem Polynomial.MonicDegreeEq.freeMonic_coe (R : Type u_1) [CommRing R] (n : ℕ) : ↑(freeMonic R n) = Polynomial.freeMonic R n

def MvPolynomial.mapEquivMonic (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (n : ℕ) : (MvPolynomial (Fin n) R →ₐ[R] S) ≃ Polynomial.MonicDegreeEq S n

MonicDegreeEq · n is representable by R[X₁,...,Xₙ], with the universal element being freeMonic.

Equations

• One or more equations did not get rendered due to their size.

theorem MvPolynomial.coe_mapEquivMonic_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S) (g : S →ₐ[R] T) : ↑((mapEquivMonic R T n) (g.comp f)) = Polynomial.map ↑g ↑((mapEquivMonic R S n) f)

theorem MvPolynomial.coe_mapEquivMonic_comp' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S) (g : S →ₐ[R] T) : (mapEquivMonic R T n) (g.comp f) = ((mapEquivMonic R S n) f).map ↑g

theorem MvPolynomial.mapEquivMonic_symm_map {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (n : ℕ) (p : Polynomial.MonicDegreeEq S n) (g : S →ₐ[R] T) : (mapEquivMonic R T n).symm (p.map ↑g) = g.comp ((mapEquivMonic R S n).symm p)

theorem MvPolynomial.mapEquivMonic_symm_map_algebraMap {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (n : ℕ) (p : Polynomial.MonicDegreeEq S n) [Algebra S T] [IsScalarTower R S T] : (mapEquivMonic R T n).symm (p.map (algebraMap S T)) = (IsScalarTower.toAlgHom R S T).comp ((mapEquivMonic R S n).symm p)

def MvPolynomial.universalFactorizationMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : MvPolynomial (Fin n) R →ₐ[R] TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)

In light of the fact that MonicDegreeEq · n is representable by R[X₁,...,Xₙ], this is the map R[X₁,...,Xₘ₊ₖ] → R[X₁,...,Xₘ] ⊗ R[X₁,...,Xₖ] corresponding to the multiplication MonicDegreeEq · m × MonicDegreeEq · k → MonicDegreeEq · (m + k).

Equations

• One or more equations did not get rendered due to their size.

theorem MvPolynomial.universalFactorizationMap_freeMonic (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : Polynomial.map (↑(universalFactorizationMap R n m k hn)) (Polynomial.freeMonic R n) = Polynomial.map (algebraMap (MvPolynomial (Fin m) R) (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R))) (Polynomial.freeMonic R m) * Polynomial.map (↑Algebra.TensorProduct.includeRight) (Polynomial.freeMonic R k)

theorem MvPolynomial.universalFactorizationMap_comp_map (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMap S n m k hn).comp (map (algebraMap R S)) = (Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S))) ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S))) ⋯).comp (universalFactorizationMap R n m k hn).toRingHom

def MvPolynomial.universalFactorizationMapLiftEquiv (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (n m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq S n) : { f : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R) →ₐ[R] S // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p } ≃ { q : Polynomial.MonicDegreeEq S m × Polynomial.MonicDegreeEq S k // ↑q.1 * ↑q.2 = ↑p }

Lifts along universalFactorizationMap corresponds to factorization of p into monic polynomials with fixed degrees.

Equations

• One or more equations did not get rendered due to their size.

theorem MvPolynomial.ker_eval₂Hom_universalFactorizationMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : RingHom.ker (eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun (x : Fin m) => X x ⊗ₜ[R] 1) fun (x : Fin k) => 1 ⊗ₜ[R] X x)) = Ideal.span (Set.range fun (i : Fin n) => C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

def MvPolynomial.universalFactorizationMapPresentation (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) (Fin m ⊕ Fin k) (Fin n)

The canonical presentation of universalFactorizationMap.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_σ' (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (f : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) : (universalFactorizationMapPresentation R n m k hn).σ' f = (map C) ((tensorEquivSum R (Fin m) (Fin k) R) f)

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : Algebra.algebraMap = (aeval (Sum.elim (fun (x : Fin m) => X x ⊗ₜ[R] 1) fun (x : Fin k) => 1 ⊗ₜ[R] X x)).toRingHom

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_algebra_smul (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (c : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)) (x : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)) : SMul.smul c x = (aeval (Sum.elim (fun (x : Fin m) => X x ⊗ₜ[R] 1) fun (x : Fin k) => 1 ⊗ₜ[R] X x)).toRingHom c * x

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_val (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (a✝ : Fin m ⊕ Fin k) : (universalFactorizationMapPresentation R n m k hn).val a✝ = Sum.elim (fun (x : Fin m) => X x ⊗ₜ[R] 1) (fun (x : Fin k) => 1 ⊗ₜ[R] X x) a✝

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_relation (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin n) : (universalFactorizationMapPresentation R n m k hn).relation i = C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i)))

@[simp]

theorem MvPolynomial.universalFactorizationMapPresentation_map (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (a✝ : Fin n) : (universalFactorizationMapPresentation R n m k hn).map a✝ = (⇑finSumFinEquiv.symm ∘ ⇑(finCongr hn)) a✝

theorem MvPolynomial.pderiv_inl_universalFactorizationMap_X (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin m) (j : Fin n) : (pderiv (Sum.inl i)) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X j))) = if ↑j < ↑i then 0 else if h : ↑j - ↑i < k then X (Sum.inr ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = k then 1 else 0

theorem MvPolynomial.pderiv_inr_universalFactorizationMap_X (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin k) (j : Fin n) : (pderiv (Sum.inr i)) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X j))) = if ↑j < ↑i then 0 else if h : ↑j - ↑i < m then X (Sum.inl ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = m then 1 else 0

theorem MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMapPresentation R n m k hn).jacobiMatrix = -((Matrix.reindex (finCongr ⋯) (finCongr ⋯)) ((Polynomial.map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inl)).toRingHom (Polynomial.freeMonic R m)).sylvester (Polynomial.map ((mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp (rename Sum.inr)).toRingHom (Polynomial.freeMonic R k)) m k)).transpose

theorem MvPolynomial.universalFactorizationMapPresentation_jacobian (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMapPresentation R n m k hn).jacobian = (-1) ^ n * (Polynomial.map Algebra.TensorProduct.includeLeftRingHom (Polynomial.freeMonic R m)).resultant (Polynomial.map Algebra.TensorProduct.includeRight.toRingHom (Polynomial.freeMonic R k))

theorem MvPolynomial.finitePresentation_universalFactorizationMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMap R n m k hn).FinitePresentation

theorem MvPolynomial.finite_universalFactorizationMap (R : Type u_1) [CommRing R] (n m k : ℕ) (hn : n = m + k) : (universalFactorizationMap R n m k hn).Finite

def Polynomial.UniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Type u_1

The universal factorization ring of a monic polynomial p of degree n. This is the representing object of the functor S ↦ "factorizations of p into (monic deg m) * (monic deg k) in S". See UniversalFactorizationRing.homEquiv.

Equations

• Polynomial.UniversalFactorizationRing m k hn p = TensorProduct (MvPolynomial (Fin n) R) R (TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R))

instance Polynomial.instCommRingUniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : CommRing (UniversalFactorizationRing m k hn p)

Equations

• Polynomial.instCommRingUniversalFactorizationRing m k hn p = Algebra.TensorProduct.instCommRing

instance Polynomial.instAlgebraUniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Algebra R (UniversalFactorizationRing m k hn p)

Equations

• Polynomial.instAlgebraUniversalFactorizationRing m k hn p = Algebra.TensorProduct.leftAlgebra

def Polynomial.UniversalFactorizationRing.fromTensor {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R) →ₐ[R] UniversalFactorizationRing m k hn p

The canonical map R[X₁,...,Xₘ] ⊗ R[X₁,...,Xₙ] → UniversalFactorizationRing.

Equations

• Polynomial.UniversalFactorizationRing.fromTensor m k hn p = AlgHom.restrictScalars R Algebra.TensorProduct.includeRight

def Polynomial.UniversalFactorizationRing.monicDegreeEq {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : MonicDegreeEq (UniversalFactorizationRing m k hn p) n

The image of p in the universal factorization ring of p.

Equations

• Polynomial.UniversalFactorizationRing.monicDegreeEq m k hn p = ⟨Polynomial.map (algebraMap R (Polynomial.UniversalFactorizationRing m k hn p)) ↑p, ⋯⟩

@[simp]

theorem Polynomial.UniversalFactorizationRing.monicDegreeEq_coe {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : ↑(monicDegreeEq m k hn p) = map (algebraMap R (UniversalFactorizationRing m k hn p)) ↑p

theorem Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) = (Algebra.ofId R (UniversalFactorizationRing m k hn p)).comp ((MvPolynomial.mapEquivMonic R R n).symm p)

theorem Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap' {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : (fromTensor m k hn p).comp (MvPolynomial.universalFactorizationMap R n m k hn) = (MvPolynomial.mapEquivMonic R (UniversalFactorizationRing m k hn p) n).symm (monicDegreeEq m k hn p)

def Polynomial.UniversalFactorizationRing.factor₁ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : MonicDegreeEq (UniversalFactorizationRing m k hn p) m

The first factor of p in the universal factorization ring of p.

Equations

• One or more equations did not get rendered due to their size.

def Polynomial.UniversalFactorizationRing.factor₂ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : MonicDegreeEq (UniversalFactorizationRing m k hn p) k

The second factor of p in the universal factorization ring of p.

Equations

• One or more equations did not get rendered due to their size.

theorem Polynomial.UniversalFactorizationRing.factor₁_mul_factor₂ {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : ↑(factor₁ m k hn p) * ↑(factor₂ m k hn p) = ↑(monicDegreeEq m k hn p)

def Polynomial.UniversalFactorizationRing.homEquiv {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : (UniversalFactorizationRing m k hn p →ₐ[R] S) ≃ { q : MonicDegreeEq S m × MonicDegreeEq S k // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p }

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

Equations

• One or more equations did not get rendered due to their size.

instance Polynomial.instFiniteUniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Module.Finite R (UniversalFactorizationRing m k hn p)

instance Polynomial.instFinitePresentationUniversalFactorizationRing {R : Type u_1} [CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n) : Algebra.FinitePresentation R (UniversalFactorizationRing m k hn p)