Documentation

CompPoly.Multivariate.FinSuccEquiv

`finSuccEquiv` for `CMvPolynomial` #

This file defines the computable multivariate polynomial equivalence for splitting off one variable, mirroring MvPolynomial.finSuccEquiv from Mathlib.

In Mathlib, MvPolynomial accepts a general type σ for the index set of the variables. Then, optionEquivLeft provides the algebra isomorphism MvPolynomial (Option σ) R ≃ₐ[R] Polynomial (MvPolynomial σ R). Finally, finSuccEquiv is defined as the composition of the rename step (Fin (n+1) ≃ Option (Fin n)) with optionEquivLeft. There is no such distinction in CMvPolynomial because the variables are of type Fin n by definition. Therefore, only CMvPolynomial.finSuccEquiv applies.

Main definitions #

CMvPolynomial.finSuccEquiv — noncomputable ring equivalence CMvPolynomial (n+1) R ≃+* Polynomial (CMvPolynomial n R), viewing a polynomial in n+1 variables as a univariate polynomial over n variables.
CMvPolynomial.finSuccEquivNth p — computable ring equivalence CMvPolynomial (n+1) R ≃+* CompPoly.CPolynomial (CMvPolynomial n R) for an arbitrary pivot p, splitting off variable p. Both directions are eval₂ folds, so they compute; the ring-equivalence laws are proved by extensionality on the C/X generators.
CMvPolynomial.finSuccEquivNthHom p / finSuccEquivNthInvHom p — its two directions as RingHoms.

Implementation notes #

finSuccEquiv is noncomputable because it goes through the polyRingEquiv bridge between CMvPolynomial and MvPolynomial; its forward/inverse correctness is obtained structurally from the underlying Mathlib AlgEquiv via RingEquiv.trans.

finSuccEquivNth avoids that bridge in its definition (staying inside the computable CMvPolynomial / CPolynomial world), and only crosses to Mathlib in the proof of map_polyRingEquiv_toPoly_finSuccEquivNth, which identifies it with MvPolynomial.finSuccEquivNth after transport.

Polynomial-level ring equivalence #

noncomputable def CPoly.polynomialCMvPolyEquiv {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :

Polynomial (CMvPolynomial n R) ≃+* Polynomial (MvPolynomial (Fin n) R)

Polynomial.mapEquiv through the CMvPolynomial ↔ MvPolynomial bridge.

Instances For

`finSuccEquiv` #

noncomputable def CMvPolynomial.finSuccEquiv {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :

CPoly.CMvPolynomial (n + 1) R ≃+* Polynomial (CPoly.CMvPolynomial n R)

Ring equivalence splitting off the first variable: CMvPolynomial (n+1) R ≃+* Polynomial (CMvPolynomial n R).

This mirrors MvPolynomial.finSuccEquiv R n. The 0-th variable becomes the univariate indeterminate Polynomial.X, and variables 1, …, n become the multivariate variables of the coefficient ring CMvPolynomial n R.

Instances For

@[simp]

theorem CMvPolynomial.finSuccEquiv_symm_apply_apply {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p : CPoly.CMvPolynomial (n + 1) R) :

finSuccEquiv.symm (finSuccEquiv p) = p

The equivalence is a left inverse: applying the inverse then forward is the identity.

@[simp]

theorem CMvPolynomial.finSuccEquiv_apply_symm_apply {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (q : Polynomial (CPoly.CMvPolynomial n R)) :

finSuccEquiv (finSuccEquiv.symm q) = q

The equivalence is a right inverse: applying forward then the inverse is the identity.

theorem CMvPolynomial.finSuccEquiv_add {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : CPoly.CMvPolynomial (n + 1) R) :

finSuccEquiv (p + q) = finSuccEquiv p + finSuccEquiv q

finSuccEquiv preserves addition.

theorem CMvPolynomial.finSuccEquiv_mul {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : CPoly.CMvPolynomial (n + 1) R) :

finSuccEquiv (p * q) = finSuccEquiv p * finSuccEquiv q

finSuccEquiv preserves multiplication.

@[simp]

theorem CMvPolynomial.finSuccEquiv_zero {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :

finSuccEquiv 0 = 0

finSuccEquiv maps zero to zero.

@[simp]

theorem CMvPolynomial.finSuccEquiv_one {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :

finSuccEquiv 1 = 1

finSuccEquiv maps one to one.

The computable `finSuccEquivNth` (arbitrary pivot) #

Unlike finSuccEquiv above, this stays inside the computable CMvPolynomial / CPolynomial world and works for an arbitrary pivot p.

def CPoly.CMvPolynomial.fseVars {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

Fin (n + 1) → CompPoly.CPolynomial (CMvPolynomial n R)

Assignment used by the forward direction: variable p goes to the univariate X, every other variable p.succAbove j goes to the constant C (X j).

Instances For

@[simp]

theorem CPoly.CMvPolynomial.fseVars_same {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

fseVars p p = CompPoly.CPolynomial.X

@[simp]

theorem CPoly.CMvPolynomial.fseVars_succAbove {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) (j : Fin n) :

fseVars p (p.succAbove j) = CompPoly.CPolynomial.C (X j)

def CPoly.CMvPolynomial.finSuccEquivNthHom {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

CMvPolynomial (n + 1) R →+* CompPoly.CPolynomial (CMvPolynomial n R)

Forward direction of finSuccEquivNth, as a RingHom. Splits variable p off as the univariate indeterminate over the other n variables. Computable.

Instances For

def CPoly.CMvPolynomial.insertVarHom {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p : Fin (n + 1)) :

CMvPolynomial n R →+* CMvPolynomial (n + 1) R

"Insert a dummy variable at position p": the embedding CMvPolynomial n R →+* CMvPolynomial (n+1) R sending X j to X (p.succAbove j). Computable.

Instances For

def CPoly.CMvPolynomial.finSuccEquivNthInvHom {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

CompPoly.CPolynomial (CMvPolynomial n R) →+* CMvPolynomial (n + 1) R

Inverse direction of finSuccEquivNth, as a RingHom. Computable.

Instances For

@[simp]

theorem CPoly.CMvPolynomial.finSuccEquivNthHom_C {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) (c : R) :

(finSuccEquivNthHom p) (C c) = CompPoly.CPolynomial.C (C c)

@[simp]

theorem CPoly.CMvPolynomial.finSuccEquivNthHom_X_same {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

(finSuccEquivNthHom p) (X p) = CompPoly.CPolynomial.X

@[simp]

theorem CPoly.CMvPolynomial.finSuccEquivNthHom_X_succAbove {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) (j : Fin n) :

(finSuccEquivNthHom p) (X (p.succAbove j)) = CompPoly.CPolynomial.C (X j)

@[simp]

theorem CPoly.CMvPolynomial.insertVarHom_C {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p : Fin (n + 1)) (c : R) :

(insertVarHom p) (C c) = C c

@[simp]

theorem CPoly.CMvPolynomial.insertVarHom_X {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p : Fin (n + 1)) (j : Fin n) :

(insertVarHom p) (X j) = X (p.succAbove j)

@[simp]

theorem CPoly.CMvPolynomial.finSuccEquivNthInvHom_C {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) (q : CMvPolynomial n R) :

(finSuccEquivNthInvHom p) (CompPoly.CPolynomial.C q) = (insertVarHom p) q

@[simp]

theorem CPoly.CMvPolynomial.finSuccEquivNthInvHom_X {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

(finSuccEquivNthInvHom p) CompPoly.CPolynomial.X = X p

theorem CPoly.CMvPolynomial.finSuccEquivNthHom_comp_insertVarHom {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

(finSuccEquivNthHom p).comp (insertVarHom p) = CompPoly.CPolynomial.CHom

finSuccEquivNthHom composed with insertVarHom is the constant embedding CMvPolynomial n R →+* CPolynomial (CMvPolynomial n R).

theorem CPoly.CMvPolynomial.finSuccEquivNthHom_comp_inv {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

(finSuccEquivNthHom p).comp (finSuccEquivNthInvHom p) = RingHom.id (CompPoly.CPolynomial (CMvPolynomial n R))

theorem CPoly.CMvPolynomial.finSuccEquivNthInvHom_comp_fwd {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

(finSuccEquivNthInvHom p).comp (finSuccEquivNthHom p) = RingHom.id (CMvPolynomial (n + 1) R)

def CPoly.CMvPolynomial.finSuccEquivNth {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) :

CMvPolynomial (n + 1) R ≃+* CompPoly.CPolynomial (CMvPolynomial n R)

The computable finSuccEquivNth: a ring equivalence CMvPolynomial (n+1) R ≃+* CompPoly.CPolynomial (CMvPolynomial n R) for an arbitrary pivot p. Both directions compute.

Instances For

@[simp]

theorem CPoly.CMvPolynomial.finSuccEquivNth_apply {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) (P : CMvPolynomial (n + 1) R) :

(finSuccEquivNth p) P = (finSuccEquivNthHom p) P

@[simp]

theorem CPoly.CMvPolynomial.finSuccEquivNth_symm_apply {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) (Q : CompPoly.CPolynomial (CMvPolynomial n R)) :

(finSuccEquivNth p).symm Q = (finSuccEquivNthInvHom p) Q

Compatibility with Mathlib's `MvPolynomial.finSuccEquivNth` #

theorem CPoly.CMvPolynomial.map_polyRingEquiv_toPoly_finSuccEquivNth {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) (P : CMvPolynomial (n + 1) R) :

Polynomial.map polyRingEquiv.toRingHom ((finSuccEquivNthHom p) P).toPoly = (MvPolynomial.finSuccEquivNth R p) (fromCMvPolynomial P)

The computable finSuccEquivNth, transported to Mathlib's MvPolynomial/Polynomial world along polyRingEquiv and CPolynomial.toPoly, is Mathlib's MvPolynomial.finSuccEquivNth.

theorem CPoly.CMvPolynomial.natDegree_finSuccEquivNthHom {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Fin (n + 1)) (P : CMvPolynomial (n + 1) R) :

((finSuccEquivNthHom p) P).natDegree = degreeOf p P

The univariate degree of finSuccEquivNth p P is the degree of variable p in P.

theorem CPoly.CMvPolynomial.natDegree_finSuccEquivNthHom_le {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {d : ℕ} (p : Fin (n + 1)) (P : CMvPolynomial (n + 1) R) (hP : ∀ (k : Fin (n + 1)), degreeOf k P ≤ d) :

((finSuccEquivNthHom p) P).natDegree ≤ d

finSuccEquivNth p P has univariate degree at most d whenever P has per-variable degree at most d.