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