English
If r ≠ 0, for t ∈ Fin n →₀ ℕ with n ≤ m, the ofLex of the supremum of toLex applied to esymmAlgMonomial (Fin m) t r equals accumulate n m t.
Русский
Если r ≠ 0, то для t ∈ Fin n →₀ ℕ с n ≤ m, выполняется равенство ofLex(supDegree toLex (esymmAlgMonomial (Fin m) t r)) = accumulate n m t.
LaTeX
$$$\text{ofLex}(\supDegree \text{toLex} <| \operatorname{esymmAlgMonomial} (\operatorname{Fin} m) t r) = \operatorname{accumulate} n m t$$$
Lean4
theorem supDegree_esymmAlgHomMonomial (hr : r ≠ 0) (t : Fin n →₀ ℕ) (hnm : n ≤ m) :
ofLex (supDegree toLex <| esymmAlgHomMonomial (Fin m) t r) = accumulate n m t :=
by
nontriviality R
induction t using Finsupp.induction₂ with
| zero => simp_rw [esymmAlgHom_zero, supDegree_toLex_C, ofLex_zero, Finsupp.coe_zero, map_zero]
| add_single i _ _ _ _ ih =>
have := i.2.trans_le hnm
rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
Monic.supDegree_mul_of_ne_zero_left toLex.injective toLex_add, ofLex_add, Finsupp.coe_add, ih, Finsupp.coe_add,
map_add, Monic.supDegree_pow rfl toLex_add toLex.injective, ofLex_smul, Finsupp.coe_smul, supDegree_esymm this, ←
map_nsmul, ← Finsupp.coe_smul, Finsupp.smul_single, nsmul_one, Nat.cast_id]
· exact monic_esymm this
· exact (monic_esymm this).pow toLex_add toLex.injective
· rwa [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_esymmAlgHomMonomial _ hnm]
