English
The universal polynomial, under the appropriate symmetry, has homogeneous components of degree card n; i.e., the left-inverse image is homogeneous of degree Fintype.card n.
Русский
У универсального полинома существует однородная структура по степеням, где суммарная степень равна card n.
LaTeX
$$((\\mathrm{optionEquivLeft}\\ R (n \\times n)).symm (\\mathrm{univ}\\ R n)).\\mathrm{IsHomogeneous}(\\mathrm{Fintype.card} n)$$
Lean4
theorem optionEquivLeft_symm_univ_isHomogeneous :
((optionEquivLeft R (n × n)).symm (univ R n)).IsHomogeneous (Fintype.card n) :=
by
have aux : Fintype.card n = 0 + ∑ i : n, 1 := by
simp only [zero_add, Finset.sum_const, smul_eq_mul, mul_one, Fintype.card]
simp only [aux, univ, charpoly, charmatrix, scalar_apply, RingHom.mapMatrix_apply, det_apply', sub_apply, map_apply,
of_apply, map_sum, map_mul, map_intCast, map_prod, map_sub, optionEquivLeft_symm_apply, Polynomial.aevalTower_C,
rename_X, diagonal, mvPolynomialX]
apply IsHomogeneous.sum
rintro i -
apply IsHomogeneous.mul
· apply isHomogeneous_C
· apply IsHomogeneous.prod
rintro j -
by_cases h : i j = j
· simp only [h, ↓reduceIte, Polynomial.aevalTower_X, IsHomogeneous.sub, isHomogeneous_X]
· simp only [h, ↓reduceIte, map_zero, zero_sub, (isHomogeneous_X _ _).neg]
