# 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] :

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.

• 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.

Instances
theorem SMulMemClass.smul_mem {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} [SMul R M] [SetLike S M] [self : SMulMemClass S R M] {s : S} (r : R) {m : M} :
m sr m s

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

class VAddMemClass (S : Type u_1) (R : outParam (Type u_2)) (M : Type u_3) [VAdd R M] [SetLike S M] :

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.

• 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.

Instances
theorem VAddMemClass.vadd_mem {S : Type u_1} {R : outParam (Type u_2)} {M : Type u_3} [VAdd R M] [SetLike S M] [self : VAddMemClass S R M] {s : S} (r : R) {m : M} :
m sr +ᵥ m s

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

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 900]
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 s

A subset closed under the additive action inherits that action.

Equations
• = { vadd := fun (r : R) (x : s) => r +ᵥ x, }
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 : s) :
r +ᵥ x s
@[instance 900]
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 s

A subset closed under the scalar action inherits that action.

Equations
• = { smul := fun (r : R) (x : s) => r x, }
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 s s
Equations
• =
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 s s
Equations
• =
@[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 : 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 : 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 +ᵥ x, hx = r +ᵥ x,
@[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 x, hx = r x,
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 : s) :
r +ᵥ x = r +ᵥ x,
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 : s) :
r x = r x,
@[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] :

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

• carrier : Set M

The underlying set of a SubMulAction.

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

The carrier set is closed under scalar multiplication.

Instances For
theorem SubMulAction.smul_mem' {R : Type u} {M : Type v} [SMul R M] (self : ) (c : R) {x : M} :
x self.carrierc x self.carrier

The carrier set is closed under scalar multiplication.

instance SubMulAction.instSetLike {R : Type u} {M : Type v} [SMul R M] :
SetLike () M
Equations
• SubMulAction.instSetLike = { coe := SubMulAction.carrier, coe_injective' := }
instance SubMulAction.instSMulMemClass {R : Type u} {M : Type v} [SMul R M] :
Equations
• =
@[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.

Equations
• p.copy s hs = { carrier := s, smul_mem' := }
Instances For
@[simp]
theorem SubMulAction.coe_copy {R : Type u} {M : Type v} [SMul R M] (p : ) (s : Set M) (hs : s = p) :
(p.copy s hs) = s
theorem SubMulAction.copy_eq {R : Type u} {M : Type v} [SMul R M] (p : ) (s : Set M) (hs : s = p) :
p.copy s hs = p
instance SubMulAction.instBot {R : Type u} {M : Type v} [SMul R M] :
Bot ()
Equations
• SubMulAction.instBot = { bot := { carrier := , smul_mem' := } }
instance SubMulAction.instInhabited {R : Type u} {M : Type v} [SMul R M] :
Equations
• SubMulAction.instInhabited = { default := }
theorem SubMulAction.smul_mem {R : Type u} {M : Type v} [SMul R M] (p : ) {x : M} (r : R) (h : x p) :
r x p
instance SubMulAction.instSMulSubtypeMem {R : Type u} {M : Type v} [SMul R M] (p : ) :
SMul R p
Equations
• p.instSMulSubtypeMem = { smul := fun (c : R) (x : p) => c x, }
@[simp]
theorem SubMulAction.val_smul {R : Type u} {M : Type v} [SMul R M] {p : } (r : R) (x : p) :
(r x) = r x
def SubMulAction.subtype {R : Type u} {M : Type v} [SMul R M] (p : ) :
p →ₑ[id] M

Embedding of a submodule p to the ambient space M.

Equations
• p.subtype = { toFun := Subtype.val, map_smul' := }
Instances For
@[simp]
theorem SubMulAction.subtype_apply {R : Type u} {M : Type v} [SMul R M] (p : ) (x : p) :
p.subtype x = x
theorem SubMulAction.subtype_eq_val {R : Type u} {M : Type v} [SMul R M] (p : ) :
p.subtype = Subtype.val
@[instance 75]
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 S'

A SubMulAction of a MulAction is a MulAction.

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

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

Equations
• = { toFun := Subtype.val, map_smul' := }
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 p
Equations
• p.smul' = { smul := fun (c : S) (x : p) => c x, }
instance SubMulAction.isScalarTower {S : Type u'} {R : Type u} {M : Type v} [] [] [SMul S R] [SMul S M] [] (p : ) :
IsScalarTower S R p
Equations
• =
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 p
Equations
• =
@[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 : 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] [] [] :
Equations
• =
instance SubMulAction.mulAction' {S : Type u'} {R : Type u} {M : Type v} [] [] [] [SMul S R] [] [] (p : ) :
MulAction S p

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

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

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

theorem SubMulAction.val_preimage_orbit {R : Type u} {M : Type v} [] [] {p : } (m : p) :
Subtype.val ⁻¹' =
theorem SubMulAction.mem_orbit_subMul_iff {R : Type u} {M : Type v} [] [] {p : } {x : p} {m : p} :
x x
theorem SubMulAction.stabilizer_of_subMul.submonoid {R : Type u} {M : Type v} [] [] {p : } (m : p) :

Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space

theorem SubMulAction.orbitRel_of_subMul {R : Type u} {M : Type v} [] [] (p : ) :
= Setoid.comap Subtype.val ()
theorem SubMulAction.stabilizer_of_subMul {R : Type u} {M : Type v} [] [] {p : } (m : 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 : (p).Nonempty) :
0 p
instance SubMulAction.instZeroSubtypeMemOfNonempty {R : Type u} {M : Type v} [] [] [Module R M] (p : ) [n_empty : Nonempty p] :
Zero p

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

Equations
• p.instZeroSubtypeMemOfNonempty = { zero := 0, }
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
instance SubMulAction.instNegSubtypeMem {R : Type u} {M : Type v} [Ring R] [] [Module R M] (p : ) :
Neg p
Equations
• p.instNegSubtypeMem = { neg := fun (x : p) => -x, }
@[simp]
theorem SubMulAction.val_neg {R : Type u} {M : Type v} [Ring R] [] [Module R M] (p : ) (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