English
For every n, the algebra homomorphism esymmAlgHom (Fin n) R n is bijective.
Русский
Для любого n отображение esymmAlgHom (Fin n) R n является биективным.
LaTeX
$$$\text{Bijective}(\operatorname{esymmAlgHom}(\operatorname{Fin} n)\, R\, n)$$$
Lean4
theorem esymmAlgHom_fin_bijective (n : ℕ) : Function.Bijective (esymmAlgHom (Fin n) R n) :=
by
use esymmAlgHom_fin_injective R le_rfl
rintro ⟨p, hp⟩
rw [← AlgHom.mem_range]
obtain rfl | h0 := eq_or_ne p 0
· exact Subalgebra.zero_mem _
induction he : p.supDegree toLex using WellFoundedLT.induction generalizing p with
| _ t ih
subst he
let t := Finsupp.equivFunOnFinite.symm (invAccumulate n n <| ↑(ofLex <| p.supDegree toLex))
have hd : (esymmAlgHomMonomial _ t <| p.leadingCoeff toLex).supDegree toLex = p.supDegree toLex :=
by
rw [← ofLex_inj, DFunLike.ext'_iff, supDegree_esymmAlgHomMonomial _ _ le_rfl]
· exact accumulate_invAccumulate le_rfl hp.antitone_supDegree
· rwa [Ne, leadingCoeff_eq_zero toLex.injective]
obtain he | hne := eq_or_ne p (esymmAlgHomMonomial _ t <| p.leadingCoeff toLex)
· convert AlgHom.mem_range_self _ (monomial t <| p.leadingCoeff toLex)
have := (supDegree_sub_lt_of_leadingCoeff_eq toLex.injective hd.symm ?_).resolve_right hne
· specialize ih _ this _ (Subalgebra.sub_mem _ hp <| isSymmetric_esymmAlgHomMonomial _ _) _ rfl
· rwa [sub_ne_zero]
convert ← Subalgebra.add_mem _ ih ⟨monomial t (p.leadingCoeff toLex), rfl⟩
apply sub_add_cancel p
· rw [leadingCoeff_esymmAlgHomMonomial t le_rfl]
