Constant coefficient reduction of maps between free polynomial modules

Setting every variable to zero reduces a linear map between free modules over MvPolynomial σ R to an R-linear map. This file constructs that reduction over a commutative semiring and records its compatibility with composition and linear operations.

For inputs in the k-th power of the ideal of variables, the coefficients of total degree k are computed by the reduced map (LinearMap.coeff_apply_of_mem_pow_idealOfVars). For a weighted homogeneous map, reduction respects the induced degrees on generators and commutes with filtering by a set of degrees (LinearMap.filter_constantCoeffReduction_apply). These facts provide the polynomial input to graded exactness arguments.

theorem LinearMap.comp_apply_mapRange_constantCoeff {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] {μ : Type u_5} (g : (κ →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] μ →₀ MvPolynomial σ R) (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) {f₀ : (ι →₀ R) →ₗ[R] κ →₀ R} {g₀ : (κ →₀ R) →ₗ[R] μ →₀ R} (hf₀ : ∀ (x : ι →₀ MvPolynomial σ R), f₀ (Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ x) = Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ (f x)) (hg₀ : ∀ (x : κ →₀ MvPolynomial σ R), g₀ (Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ x) = Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ (g x)) (x : ι →₀ MvPolynomial σ R) : (g₀ ∘ₗ f₀) (Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ x) = Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ ((g ∘ₗ f) x)

If f₀ and g₀ are the reductions of f and g modulo the variables, then g₀ ∘ f₀ is the reduction of g ∘ f.

theorem LinearMap.eq_of_mapRange_constantCoeff {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] (f₀ f₀' : (ι →₀ R) →ₗ[R] κ →₀ R) {f f' : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R} (hf₀ : ∀ (x : ι →₀ MvPolynomial σ R), f₀ (Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ x) = Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ (f x)) (hf₀' : ∀ (x : ι →₀ MvPolynomial σ R), f₀' (Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ x) = Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ (f' x)) (h : f = f') : f₀ = f₀'

A reduction modulo the variables is determined by the map it reduces: reductions f₀ of f and f₀' of f' agree when f = f'.

noncomputable def LinearMap.constantCoeffReduction {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) : (ι →₀ R) →ₗ[R] κ →₀ R

The reduction of an S-linear map f : (ι →₀ S) → (κ →₀ S) modulo the variables, for S = R[V_v : v ∈ σ]: the R-linear map (ι →₀ R) → (κ →₀ R) whose matrix coefficients are the constant coefficients of those of f. It commutes with taking constant coefficients (LinearMap.constantCoeffReduction_mapRange_constantCoeff).

Equations

• f.constantCoeffReduction = Finsupp.linearCombination R fun (i : ι) => Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ (f (Finsupp.single i 1))

@[simp]

theorem LinearMap.constantCoeffReduction_single_apply {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) (i : ι) (c : R) (j : κ) : (f.constantCoeffReduction (Finsupp.single i c)) j = c * MvPolynomial.constantCoeff ((f (Finsupp.single i 1)) j)

The matrix coefficients of the reduction of f modulo the variables are the constant coefficients of those of f.

@[simp]

theorem LinearMap.constantCoeffReduction_mapRange_constantCoeff {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) (x : ι →₀ MvPolynomial σ R) : f.constantCoeffReduction (Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ x) = Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ (f x)

The reduction commutes with setting the variables to zero. Applying constantCoeffReduction f to the constant coefficients of x gives the constant coefficients of f x.

@[simp]

theorem LinearMap.constantCoeffReduction_comp {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] {μ : Type u_5} (g : (κ →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] μ →₀ MvPolynomial σ R) (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) : (g ∘ₗ f).constantCoeffReduction = g.constantCoeffReduction ∘ₗ f.constantCoeffReduction

The reduction of a composite is the composite of the reductions.

@[simp]

theorem LinearMap.constantCoeffReduction_id {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] : id.constantCoeffReduction = id

The identity map reduces to the identity map.

@[simp]

theorem LinearMap.constantCoeffReduction_add {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] (f g : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) : (f + g).constantCoeffReduction = f.constantCoeffReduction + g.constantCoeffReduction

Reduction commutes with addition of linear maps.

@[simp]

theorem LinearMap.constantCoeffReduction_smul {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] (p : MvPolynomial σ R) (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) : (p • f).constantCoeffReduction = MvPolynomial.constantCoeff p • f.constantCoeffReduction

Reduction commutes with scalar multiplication of linear maps.

@[simp]

theorem LinearMap.constantCoeffReduction_zero {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] : constantCoeffReduction 0 = 0

The reduction of the zero map is zero.

@[simp]

theorem LinearMap.constantCoeffReduction_neg {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommRing R] (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) : (-f).constantCoeffReduction = -f.constantCoeffReduction

Reduction commutes with negation of linear maps.

@[simp]

theorem LinearMap.constantCoeffReduction_sub {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommRing R] (f g : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) : (f - g).constantCoeffReduction = f.constantCoeffReduction - g.constantCoeffReduction

Reduction commutes with subtraction of linear maps.

theorem LinearMap.coeff_apply_of_mem_pow_idealOfVars {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) {k : ℕ} {z : ι →₀ MvPolynomial σ R} (hz : ∀ (i : ι), z i ∈ MvPolynomial.idealOfVars σ R ^ k) {e : σ →₀ ℕ} (he : Finsupp.degree e = k) (j : κ) : ((f z) j).coeff e = (f.constantCoeffReduction (Finsupp.mapRange ⇑(MvPolynomial.lcoeff R e) ⋯ z)) j

On J ^ k • (ι →₀ S), the coefficients of f in total degree k are computed by the canonical reduction of f modulo the variables.

theorem LinearMap.degree_eq_of_constantCoeffReduction_single_apply_ne_zero {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] {w : σ → ℤ} {g : ι → ℤ} {g' : κ → ℤ} {r : ℤ} (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) (hhom : ∀ (i : ι) (j : κ), MvPolynomial.IsWeightedHomogeneous w ((f (Finsupp.single i 1)) j) (g i + r - g' j)) {i : ι} {j : κ} {c : R} (h : (f.constantCoeffReduction (Finsupp.single i c)) j ≠ 0) : g' j = g i + r

The reduction of f moves the source generator degree g to the target degree g' by r.

theorem LinearMap.filter_constantCoeffReduction_apply {R : Type u_1} {σ : Type u_2} {ι : Type u_3} {κ : Type u_4} [CommSemiring R] {w : σ → ℤ} {g : ι → ℤ} {g' : κ → ℤ} {r : ℤ} (f : (ι →₀ MvPolynomial σ R) →ₗ[MvPolynomial σ R] κ →₀ MvPolynomial σ R) (hhom : ∀ (i : ι) (j : κ), MvPolynomial.IsWeightedHomogeneous w ((f (Finsupp.single i 1)) j) (g i + r - g' j)) (P : ℤ → Prop) [DecidablePred P] (u : ι →₀ R) : Finsupp.filter (fun (j : κ) => P (g' j)) (f.constantCoeffReduction u) = f.constantCoeffReduction (Finsupp.filter (fun (i : ι) => P (g i + r)) u)

The reduction of f commutes with restricting to generators in a set of degrees, up to the shift by r.