English
The same natural order isomorphism as above provides a bridge between two representations of invariants, reinforcing the equivalence of two constructions of invariant submodules.
Русский
Та же естественная порядковая изоморфизм обеспечивает мост между двумя способами представления инвариантов, подчеркивая эквивалентность двух конструкций инвариантных подпмодулей.
LaTeX
$$\\rho.invtSubmodule \\cong_o Submodule(MonoidAlgebra k G, \\rho.asModule)$$
Lean4
/-- The natural order isomorphism between the two ways to represent invariant submodules. -/
noncomputable def mapSubmodule : ρ.invtSubmodule ≃o Submodule (MonoidAlgebra k G) ρ.asModule
where
toFun
p :=
{ toAddSubmonoid := (p : Submodule k V).toAddSubmonoid.map ρ.asModuleEquiv.symm
smul_mem' :=
by
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, AddSubmonoid.mem_map,
Submodule.mem_toAddSubmonoid, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
refine fun x v hv ↦ ⟨ρ.asModuleEquiv (x • ρ.asModuleEquiv.symm v), ?_, rfl⟩
simpa using ρ.asAlgebraHom_mem_of_forall_mem p (ρ.mem_invtSubmodule.mp p.property) v hv x }
invFun
q :=
⟨(Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (q.restrictScalars k),
by
rw [invtSubmodule, Sublattice.mem_iInf]
intro g v hv
simp only [Submodule.orderIsoMapComap_symm_apply, Submodule.mem_comap] at hv ⊢
convert q.smul_mem (MonoidAlgebra.of k G g) hv using 1
rw [← asModuleEquiv_symm_map_rho]⟩
left_inv p := by ext; simp
right_inv q := by ext; aesop
map_rel_iff'
{p
q} :=
⟨fun h x hx ↦
by
suffices ρ.asModuleEquiv.symm x ∈ (q : Submodule k V).toAddSubmonoid.map ρ.asModuleEquiv.symm by simpa using this
exact h <| by simpa using hx, fun h x hx ↦ by aesop⟩
