# mathlibdocumentation

group_theory.group_action.sub_mul_action

# Sets invariant to a mul_action#

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

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

## Main definitions #

• sub_mul_action.mul_action - the mul_action R M transferred to the subtype.
• sub_mul_action.mul_action' - the mul_action S M transferred to the subtype when is_scalar_tower S R M.
• sub_mul_action.is_scalar_tower - the is_scalar_tower S R M transferred to the subtype.

## Tags #

submodule, mul_action

structure sub_mul_action (R : Type u) (M : Type v) [ M] :
Type v

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

Instances for sub_mul_action
@[protected, instance]
def sub_mul_action.set_like {R : Type u} {M : Type v} [ M] :
Equations
@[simp]
theorem sub_mul_action.mem_carrier {R : Type u} {M : Type v} [ M] {p : M} {x : M} :
@[ext]
theorem sub_mul_action.ext {R : Type u} {M : Type v} [ M] {p q : M} (h : ∀ (x : M), x p x q) :
p = q
@[protected]
def sub_mul_action.copy {R : Type u} {M : Type v} [ M] (p : M) (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
@[simp]
theorem sub_mul_action.coe_copy {R : Type u} {M : Type v} [ M] (p : M) (s : set M) (hs : s = p) :
(p.copy s hs) = s
theorem sub_mul_action.copy_eq {R : Type u} {M : Type v} [ M] (p : M) (s : set M) (hs : s = p) :
p.copy s hs = p
@[protected, instance]
def sub_mul_action.has_bot {R : Type u} {M : Type v} [ M] :
Equations
@[protected, instance]
def sub_mul_action.inhabited {R : Type u} {M : Type v} [ M] :
Equations
theorem sub_mul_action.smul_mem {R : Type u} {M : Type v} [ M] (p : M) {x : M} (r : R) (h : x p) :
r x p
@[protected, instance]
def sub_mul_action.has_smul {R : Type u} {M : Type v} [ M] (p : M) :
p
Equations
@[simp, norm_cast]
theorem sub_mul_action.coe_smul {R : Type u} {M : Type v} [ M] {p : M} (r : R) (x : p) :
(r x) = r x
@[simp, norm_cast]
theorem sub_mul_action.coe_mk {R : Type u} {M : Type v} [ M] {p : M} (x : M) (hx : x p) :
x, hx⟩ = x
@[protected]
def sub_mul_action.subtype {R : Type u} {M : Type v} [ M] (p : M) :

Embedding of a submodule p to the ambient space M.

Equations
@[simp]
theorem sub_mul_action.subtype_apply {R : Type u} {M : Type v} [ M] (p : M) (x : p) :
theorem sub_mul_action.subtype_eq_val {R : Type u} {M : Type v} [ M] (p : M) :
theorem sub_mul_action.smul_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [monoid R] [ M] [ R] [ M] [ M] (p : M) (s : S) {x : M} (h : x p) :
s x p
@[protected, instance]
def sub_mul_action.has_smul' {S : Type u'} {R : Type u} {M : Type v} [monoid R] [ M] [ R] [ M] [ M] (p : M) :
p
Equations
@[protected, instance]
def sub_mul_action.is_scalar_tower {S : Type u'} {R : Type u} {M : Type v} [monoid R] [ M] [ R] [ M] [ M] (p : M) :
p
@[simp, norm_cast]
theorem sub_mul_action.coe_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [monoid R] [ M] [ R] [ M] [ M] (p : M) (s : S) (x : p) :
(s x) = s x
@[simp]
theorem sub_mul_action.smul_mem_iff' {R : Type u} {M : Type v} [monoid R] [ M] (p : M) {G : Type u_1} [group G] [ R] [ M] [ M] (g : G) {x : M} :
g x p x p
@[protected, instance]
def sub_mul_action.is_central_scalar {S : Type u'} {R : Type u} {M : Type v} [monoid R] [ M] [ R] [ M] [ M] (p : M) [ R] [ M] [ M] [ M] :
@[protected, instance]
def sub_mul_action.mul_action' {S : Type u'} {R : Type u} {M : Type v} [monoid R] [ M] [monoid S] [ R] [ M] [ M] (p : M) :
p

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

Equations
@[protected, instance]
def sub_mul_action.mul_action {R : Type u} {M : Type v} [monoid R] [ M] (p : M) :
p
Equations
theorem sub_mul_action.coe_image_orbit {R : Type u} {M : Type v} [monoid R] [ M] {p : M} (m : p) :
=

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

theorem sub_mul_action.stabilizer_of_sub_mul.submonoid {R : Type u} {M : Type v} [monoid R] [ M] {p : M} (m : p) :

Stabilizers in monoid sub_mul_action coincide with stabilizers in the ambient space

theorem sub_mul_action.stabilizer_of_sub_mul {R : Type u} {M : Type v} [group R] [ M] {p : M} (m : p) :

Stabilizers in group sub_mul_action coincide with stabilizers in the ambient space

theorem sub_mul_action.zero_mem {R : Type u} {M : Type v} [semiring R] [ M] (p : M) (h : p.nonempty) :
0 p
@[protected, instance]
def sub_mul_action.has_zero {R : Type u} {M : Type v} [semiring R] [ M] (p : M) [n_empty : nonempty p] :

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

Equations
theorem sub_mul_action.neg_mem {R : Type u} {M : Type v} [ring R] [ M] (p : M) {x : M} (hx : x p) :
-x p
@[simp]
theorem sub_mul_action.neg_mem_iff {R : Type u} {M : Type v} [ring R] [ M] (p : M) {x : M} :
-x p x p
@[protected, instance]
def sub_mul_action.has_neg {R : Type u} {M : Type v} [ring R] [ M] (p : M) :
Equations
@[simp, norm_cast]
theorem sub_mul_action.coe_neg {R : Type u} {M : Type v} [ring R] [ M] (p : M) (x : p) :
theorem sub_mul_action.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [monoid R] [ M] [ R] [ M] [ M] (p : M) {s : S} {x : M} (s0 : s 0) :
s x p x p