esymmAlgEquiv — Mathlib

English

If the cardinality of σ equals n, esymmAlgEquiv σ R hn provides an algebra isomorphism between MvPolynomial(Fin n) R and the symmetric subalgebra σ R.

Русский

Если кардинал σ равен n, esymmAlgEquiv σ R hn задаёт алгебраическое изоморфизм между MvPolynomial(Fin n) R и симметрической подалгеброй σ R.

LaTeX

$$$\text{esymmAlgEquiv}(\sigma\, R\, hn) : MvPolynomial(\mathrm{Fin}\, n) R \cong_{R} \text{symmetricSubalgebra } \sigma R$$$

Lean4

/-- If the cardinality of `σ` is `n`, then `esymmAlgHom σ R n` is an isomorphism. -/
@[simps! apply]
noncomputable def esymmAlgEquiv (hn : Fintype.card σ = n) : MvPolynomial (Fin n) R ≃ₐ[R] symmetricSubalgebra σ R :=
  AlgEquiv.ofBijective (esymmAlgHom σ R n) ⟨esymmAlgHom_injective R hn.ge, esymmAlgHom_surjective R hn.le⟩

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