mono_map_natDegree_eq — Mathlib

English

Let φ be an additive map from polynomial ring R[X] to S[X], k a bound, and fu a monotone function. If φ kills all monomials of degree less than k, and φ maps each monomial m to a polynomial of degree fu(deg m), with fu strictly increasing beyond k, then φ sends any polynomial p to a polynomial of degree fu(deg p).

Русский

Пусть φ — аддитивное отображение от кольца многочленов R[X] в S[X], k — граница, и fu — монотонная функция. Пусть φ обнуляет все мономы степени < k, и каждый мономом m сопоставляется полином φ(m) степени fu(deg m); если fu возрастает строго при возрастании степени, то φ переводит любой полином p в полином степени fu(deg p).

LaTeX

$$$\\forall P\\,\\forall φ:\\, (R[X] \\to S[X]),\\ N:\\mathbb{N},\\ fu:\\mathbb{N}\\to\\mathbb{N},\\ fu_0:\\forall n\\, n\\le N\\Rightarrow fu(n)=0\\ ;\\ fc:\\forall n

Lean4

/-- Let `φ : R[x] → S[x]` be an additive map, `k : ℕ` a bound, and `fu : ℕ → ℕ` a
"sufficiently monotone" map.  Assume also that
* `φ` maps to `0` all monomials of degree less than `k`,
* `φ` maps each monomial `m` in `R[x]` to a polynomial `φ m` of degree `fu (deg m)`.
Then, `φ` maps each polynomial `p` in `R[x]` to a polynomial of degree `fu (deg p)`. -/
theorem mono_map_natDegree_eq {S F : Type*} [Semiring S] [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]] {φ : F}
    {p : R[X]} (k : ℕ) (fu : ℕ → ℕ) (fu0 : ∀ {n}, n ≤ k → fu n = 0) (fc : ∀ {n m}, k ≤ n → n < m → fu n < fu m)
    (φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0) (φ_mon_nat : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = fu n) :
    (φ p).natDegree = fu p.natDegree :=
  by
  refine
    induction_with_natDegree_le (fun p => (φ p).natDegree = fu p.natDegree) p.natDegree (by simp [fu0]) ?_ ?_ _ rfl.le
  · intro n r r0 _
    rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]
  · intro f g fg _ fk gk
    rw [natDegree_add_eq_right_of_natDegree_lt fg, map_add]
    by_cases FG : k ≤ f.natDegree
    · rw [natDegree_add_eq_right_of_natDegree_lt, gk]
      rw [fk, gk]
      exact fc FG fg
    · cases k
      · exact (FG (Nat.zero_le _)).elim
      · rwa [φ_k (not_le.mp FG), zero_add]

Похожие утверждения