English
There is a natural order isomorphism between invariant submodules and polynomial submodules of AEval R M a.
Русский
Существует естественная взаимнооднозначная монотонная преборка между инвариантными подмодулями и подмодулями над AEval R M a.
LaTeX
$$$\mathrm{mapSubmodule}: (\ Algebra.lsmul\ R\ R\ M\ a).invtSubmodule \cong_o Submodule(\ Polynomial\ R) (AEval\ R\ M\ a)$$$
Lean4
/-- The natural order isomorphism between the two ways to represent invariant submodules. -/
def mapSubmodule : (Algebra.lsmul R R M a).invtSubmodule ≃o Submodule R[X] (AEval R M a)
where
toFun
p :=
{ toAddSubmonoid := (p : Submodule R M).toAddSubmonoid.map (of R M a)
smul_mem' := by
rintro f - ⟨m : M, h : m ∈ (p : Submodule R M), rfl⟩
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, AddSubmonoid.mem_map,
Submodule.mem_toAddSubmonoid]
exact ⟨aeval a f • m, aeval_apply_smul_mem_of_le_comap' h f a p.2, of_aeval_smul a f m⟩ }
invFun
q :=
⟨(Submodule.orderIsoMapComap (of R M a)).symm (q.restrictScalars R), fun m hm ↦ by
simpa [← X_smul_of] using q.smul_mem (X : R[X]) hm⟩
left_inv p := by ext; simp
right_inv q := by ext; aesop
map_rel_iff' {p p'} := ⟨fun h x hx ↦ by aesop (rule_sets := [SetLike!]), fun h x hx ↦ by aesop⟩
