restrict_equiv_mapSubmodule — Mathlib

English

There is a natural R[X]-linear equivalence between a restricted AEval and a polynomial-submodule representation.

Русский

Существует естественное R[X]-линейное эквивалентность между ограниченным AEval и изображением подмодуля над полиномами.

LaTeX

$$$(AEval\ R\ p\ (Algebra.lsmul\ R\ R\ M\ a)\ restrict\ hp) \simeq_{R[X]} mapSubmodule R M a ⟨p, hp⟩$$$

Lean4

/-- The natural `R[X]`-linear equivalence between the two ways to represent an invariant submodule.
-/
noncomputable def restrict_equiv_mapSubmodule :
    (AEval R p <| (Algebra.lsmul R R M a).restrict hp) ≃ₗ[R[X]] mapSubmodule R M a ⟨p, hp⟩ :=
  LinearEquiv.ofAEval ((Algebra.lsmul R R M a).restrict hp) (equiv_mapSubmodule a p hp)
    (fun x ↦ by simp [equiv_mapSubmodule, X_smul_of])

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