Zulip Chat Archive
Stream: new members
Topic: stabilizer of a submodule
Paul Nelson (Jan 07 2024 at 15:25):
I wasn't able to find anything like the following in mathlib, but thought I'd ask:
def Subalgebra.stabilizer
(R : Type) [CommRing R]
{V : Type} [AddCommGroup V] [Module R V]
(U : Submodule R V)
: Subalgebra R (Module.End R V)
:= by sorry
def Subalgebra.mem_stabilizer_iff
(R : Type) [CommRing R]
{V : Type} [AddCommGroup V] [Module R V]
(U : Submodule R V)
(x : Module.End R V)
: x ∈ Subalgebra.stabilizer R U ↔ ∀ v ∈ U, x v ∈ U
:= by sorry
Eric Wieser (Jan 07 2024 at 17:46):
If we had this, I would hope it would be in the generality of an arbitrary action, not just an endomorphism (of course there isn't really any difference, but it would then match the other content on stabilizers)
Last updated: May 02 2025 at 03:31 UTC