# Documentation

Mathlib.GroupTheory.GroupAction.SubMulAction

# Sets invariant to a MulAction#

In this file we define SubMulAction R M; a subset of a MulAction R M which is closed with respect to scalar multiplication.

For most uses, typically Submodule R M is more powerful.

## Main definitions #

• SubMulAction.mulAction - the MulAction R M transferred to the subtype.
• SubMulAction.mulAction' - the MulAction S M transferred to the subtype when IsScalarTower S R M.
• SubMulAction.isScalarTower - the IsScalarTower S R M transferred to the subtype.

## Tags #

submodule, mul_action

class SMulMemClass (S : Type u_1) (R : outParam (Type u_2)) (M : Type u_3) [SMul R M] [SetLike S M] :
• smul_mem : ∀ {s : S} (r : R) {m : M}, m sr m s

Multiplication by a scalar on an element of the set remains in the set.

SMulMemClass S R M says S is a type of subsets s ≤ M that are closed under the scalar action of R on M.

Note that only R is marked as an outParam here, since M is supplied by the SetLike class instead.

Instances
class VAddMemClass (S : Type u_1) (R : outParam (Type u_2)) (M : Type u_3) [VAdd R M] [SetLike S M] :
• vadd_mem : ∀ {s : S} (r : R) {m : M}, m sr +ᵥ m s

Addition by a scalar with an element of the set remains in the set.

VAddMemClass S R M says S is a type of subsets s ≤ M that are closed under the additive action of R on M.

Note that only R is marked as an outParam here, since M is supplied by the SetLike class instead.

Instances
theorem AddSubmonoidClass.nsmulMemClass {S : Type u_1} {M : Type u_2} [] [SetLike S M] [] :

Not registered as an instance because R is an outParam in SMulMemClass S R M.

theorem AddSubgroupClass.zsmulMemClass {S : Type u_1} {M : Type u_2} [] [SetLike S M] [] :

Not registered as an instance because R is an outParam in SMulMemClass S R M.

instance SetLike.vadd {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) :
VAdd R { x // x s }

A subset closed under the additive action inherits that action.

theorem SetLike.vadd.proof_1 {S : Type u_2} {R : Type u_3} {M : Type u_1} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
r +ᵥ x s
instance SetLike.smul {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) :
SMul R { x // x s }

A subset closed under the scalar action inherits that action.

theorem SMulMemClass.ofIsScalarTower (S : Type u_1) (M : Type u_2) (N : Type u_3) (α : Type u_4) [SetLike S α] [SMul M N] [SMul M α] [] [] [SMulMemClass S N α] [] :

This can't be an instance because Lean wouldn't know how to find N, but we can still use this to manually derive SMulMemClass on specific types.

instance SetLike.instIsScalarTower {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] [Mul M] [] [] (s : S) :
IsScalarTower R { x // x s } { x // x s }
instance SetLike.instSMulCommClass {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] [Mul M] [] [] (s : S) :
SMulCommClass R { x // x s } { x // x s }
@[simp]
theorem SetLike.val_vadd {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
↑(r +ᵥ x) = r +ᵥ x
@[simp]
theorem SetLike.val_smul {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
↑(r x) = r x
@[simp]
theorem SetLike.mk_vadd_mk {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : M) (hx : x s) :
r +ᵥ { val := x, property := hx } = { val := r +ᵥ x, property := (_ : r +ᵥ x s) }
@[simp]
theorem SetLike.mk_smul_mk {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) (r : R) (x : M) (hx : x s) :
r { val := x, property := hx } = { val := r x, property := (_ : r x s) }
theorem SetLike.vadd_def {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
r +ᵥ x = { val := ↑(r +ᵥ x), property := (_ : r +ᵥ x s) }
theorem SetLike.smul_def {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
r x = { val := ↑(r x), property := (_ : r x s) }
@[simp]
theorem SetLike.forall_smul_mem_iff {R : Type u_1} {M : Type u_2} {S : Type u_3} [] [] [SetLike S M] [SMulMemClass S R M] {N : S} {x : M} :
(∀ (a : R), a x N) x N
structure SubMulAction (R : Type u) (M : Type v) [SMul R M] :
• carrier : Set M

The underlying set of a SubMulAction.

• smul_mem' : ∀ (c : R) {x : M}, x s.carrierc x s.carrier

The carrier set is closed under scalar multiplication.

A SubMulAction is a set which is closed under scalar multiplication.

Instances For
instance SubMulAction.instSetLikeSubMulAction {R : Type u} {M : Type v} [SMul R M] :
SetLike () M
@[simp]
theorem SubMulAction.mem_carrier {R : Type u} {M : Type v} [SMul R M] {p : } {x : M} :
x p.carrier x p
theorem SubMulAction.ext {R : Type u} {M : Type v} [SMul R M] {p : } {q : } (h : ∀ (x : M), x p x q) :
p = q
def SubMulAction.copy {R : Type u} {M : Type v} [SMul R M] (p : ) (s : Set M) (hs : s = p) :

Copy of a sub_mul_action with a new carrier equal to the old one. Useful to fix definitional equalities.

Instances For
@[simp]
theorem SubMulAction.coe_copy {R : Type u} {M : Type v} [SMul R M] (p : ) (s : Set M) (hs : s = p) :
↑() = s
theorem SubMulAction.copy_eq {R : Type u} {M : Type v} [SMul R M] (p : ) (s : Set M) (hs : s = p) :
= p
instance SubMulAction.instBotSubMulAction {R : Type u} {M : Type v} [SMul R M] :
Bot ()
theorem SubMulAction.smul_mem {R : Type u} {M : Type v} [SMul R M] (p : ) {x : M} (r : R) (h : x p) :
r x p
@[simp]
theorem SubMulAction.val_smul {R : Type u} {M : Type v} [SMul R M] {p : } (r : R) (x : { x // x p }) :
↑(r x) = r x
def SubMulAction.subtype {R : Type u} {M : Type v} [SMul R M] (p : ) :
{ x // x p } →[R] M

Embedding of a submodule p to the ambient space M.

Instances For
@[simp]
theorem SubMulAction.subtype_apply {R : Type u} {M : Type v} [SMul R M] (p : ) (x : { x // x p }) :
↑() x = x
theorem SubMulAction.subtype_eq_val {R : Type u} {M : Type v} [SMul R M] (p : ) :
↑() = Subtype.val
instance SubMulAction.SMulMemClass.toMulAction {R : Type u} {M : Type v} [] [] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
MulAction R { x // x S' }

A SubMulAction of a MulAction is a MulAction.

def SubMulAction.SMulMemClass.subtype {R : Type u} {M : Type v} [] [] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
{ x // x S' } →[R] M

The natural MulActionHom over R from a SubMulAction of M to M.

Instances For
@[simp]
theorem SubMulAction.SMulMemClass.coeSubtype {R : Type u} {M : Type v} [] [] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
= Subtype.val
theorem SubMulAction.smul_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [] [] [SMul S R] [SMul S M] [] (p : ) (s : S) {x : M} (h : x p) :
s x p
instance SubMulAction.smul' {S : Type u'} {R : Type u} {M : Type v} [] [] [SMul S R] [SMul S M] [] (p : ) :
SMul S { x // x p }
instance SubMulAction.isScalarTower {S : Type u'} {R : Type u} {M : Type v} [] [] [SMul S R] [SMul S M] [] (p : ) :
IsScalarTower S R { x // x p }
instance SubMulAction.isScalarTower' {S : Type u'} {R : Type u} {M : Type v} [] [] [SMul S R] [SMul S M] [] (p : ) {S' : Type u_1} [SMul S' R] [SMul S' S] [SMul S' M] [IsScalarTower S' R M] [IsScalarTower S' S M] :
IsScalarTower S' S { x // x p }
@[simp]
theorem SubMulAction.val_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [] [] [SMul S R] [SMul S M] [] (p : ) (s : S) (x : { x // x p }) :
↑(s x) = s x
@[simp]
theorem SubMulAction.smul_mem_iff' {R : Type u} {M : Type v} [] [] (p : ) {G : Type u_1} [] [SMul G R] [] [] (g : G) {x : M} :
g x p x p
instance SubMulAction.isCentralScalar {S : Type u'} {R : Type u} {M : Type v} [] [] [SMul S R] [SMul S M] [] (p : ) [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [] [] :
IsCentralScalar S { x // x p }
instance SubMulAction.mulAction' {S : Type u'} {R : Type u} {M : Type v} [] [] [] [SMul S R] [] [] (p : ) :
MulAction S { x // x p }

If the scalar product forms a MulAction, then the subset inherits this action

instance SubMulAction.mulAction {R : Type u} {M : Type v} [] [] (p : ) :
MulAction R { x // x p }
theorem SubMulAction.val_image_orbit {R : Type u} {M : Type v} [] [] {p : } (m : { x // x p }) :
Subtype.val '' =

Orbits in a SubMulAction coincide with orbits in the ambient space.

theorem SubMulAction.stabilizer_of_subMul.submonoid {R : Type u} {M : Type v} [] [] {p : } (m : { x // x p }) :

Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space

theorem SubMulAction.stabilizer_of_subMul {R : Type u} {M : Type v} [] [] {p : } (m : { x // x p }) :

Stabilizers in group SubMulAction coincide with stabilizers in the ambient space

theorem SubMulAction.zero_mem {R : Type u} {M : Type v} [] [] [Module R M] (p : ) (h : ) :
0 p

If the scalar product forms a Module, and the SubMulAction is not ⊥, then the subset inherits the zero.

theorem SubMulAction.neg_mem {R : Type u} {M : Type v} [Ring R] [] [Module R M] (p : ) {x : M} (hx : x p) :
-x p
@[simp]
theorem SubMulAction.neg_mem_iff {R : Type u} {M : Type v} [Ring R] [] [Module R M] (p : ) {x : M} :
-x p x p
@[simp]
theorem SubMulAction.val_neg {R : Type u} {M : Type v} [Ring R] [] [Module R M] (p : ) (x : { x // x p }) :
↑(-x) = -x
theorem SubMulAction.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [] [] [] [SMul S R] [] [] (p : ) {s : S} {x : M} (s0 : s 0) :
s x p x p