esymmAlgHom_fin_surjective — Mathlib

English

For every n, esymmAlgHom (Fin n) R n is surjective.

Русский

Для каждого n отображение esymmAlgHom (Fin n) R n сюрьективно.

LaTeX

$$$\operatorname{Surjective}(\operatorname{esymmAlgHom}(\operatorname{Fin} n)\, R\, n)$$$

Lean4

theorem esymmAlgHom_fin_surjective (h : m ≤ n) : Function.Surjective (esymmAlgHom (Fin m) R n) :=
  by
  intro p
  obtain ⟨q, rfl⟩ := (esymmAlgHom_fin_bijective R m).2 p
  rw [← AlgHom.mem_range]
  induction q using MvPolynomial.induction_on with
  | C r => rw [← algebraMap_eq, AlgHom.commutes]; apply Subalgebra.algebraMap_mem
  | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
  | mul_X p i hp =>
    rw [map_mul]
    apply Subalgebra.mul_mem _ hp
    rw [AlgHom.mem_range]
    refine ⟨X ⟨i, i.2.trans_le h⟩, ?_⟩
    simp_rw [esymmAlgHom, aeval_X]

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