mathlib3 documentation

group_theory.group_action.sub_mul_action

Sets invariant to a mul_action #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Tags #

submodule, mul_action

source
@[class]
structure smul_mem_class (S : Type u_1) (R : out_param (Type u_2)) (M : Type u_3) [has_smul R M] [set_like S M] :
Type

smul_mem_class 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 out_param here, since M is supplied by the set_like class instead.

Instances of this typeclass
Instances of other typeclasses for smul_mem_class
  • smul_mem_class.has_sizeof_inst
source
@[class]
structure vadd_mem_class (S : Type u_1) (R : out_param (Type u_2)) (M : Type u_3) [has_vadd R M] [set_like S M] :
Type

vadd_mem_class 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 out_param here, since M is supplied by the set_like class instead.

Instances for vadd_mem_class
  • vadd_mem_class.has_sizeof_inst
source
@[protected, instance]
def set_like.has_vadd {S : Type u'} {R : Type u} {M : Type v} [has_vadd R M] [set_like S M] [hS : vadd_mem_class S R M] (s : S) :
has_vadd R ↥s

A subset closed under the additive action inherits that action.

Equations
source
@[protected, instance]
def set_like.has_smul {S : Type u'} {R : Type u} {M : Type v} [has_smul R M] [set_like S M] [hS : smul_mem_class S R M] (s : S) :
has_smul R ↥s

A subset closed under the scalar action inherits that action.

Equations
source
@[protected, simp, norm_cast]
theorem set_like.coe_vadd {S : Type u'} {R : Type u} {M : Type v} [has_vadd R M] [set_like S M] [hS : vadd_mem_class S R M] (s : S) (r : R) (x : ↥s) :
↑(r +ᵥ x) = r +ᵥ ↑x
source
@[protected, simp, norm_cast]
theorem set_like.coe_smul {S : Type u'} {R : Type u} {M : Type v} [has_smul R M] [set_like S M] [hS : smul_mem_class S R M] (s : S) (r : R) (x : ↥s) :
↑(r • x) = r • ↑x
source
@[simp]
theorem set_like.mk_smul_mk {S : Type u'} {R : Type u} {M : Type v} [has_smul R M] [set_like S M] [hS : smul_mem_class S R M] (s : S) (r : R) (x : M) (hx : x ∈ s) :
r • ⟨x, hx⟩ = ⟨r • x, _⟩
source
@[simp]
theorem set_like.mk_vadd_mk {S : Type u'} {R : Type u} {M : Type v} [has_vadd R M] [set_like S M] [hS : vadd_mem_class S R M] (s : S) (r : R) (x : M) (hx : x ∈ s) :
r +ᵥ ⟨x, hx⟩ = ⟨r +ᵥ x, _⟩
source
theorem set_like.vadd_def {S : Type u'} {R : Type u} {M : Type v} [has_vadd R M] [set_like S M] [hS : vadd_mem_class S R M] (s : S) (r : R) (x : ↥s) :
r +ᵥ x = ⟨r +ᵥ ↑x, _⟩
source
theorem set_like.smul_def {S : Type u'} {R : Type u} {M : Type v} [has_smul R M] [set_like S M] [hS : smul_mem_class S R M] (s : S) (r : R) (x : ↥s) :
r • x = ⟨r • ↑x, _⟩
source
@[simp]
theorem set_like.forall_smul_mem_iff {R : Type u_1} {M : Type u_2} {S : Type u_3} [monoid R] [mul_action R M] [set_like S M] [smul_mem_class S R M] {N : S} {x : M} :
(∀ (a : R), a • x ∈ N) ↔ x ∈ N
source
structure sub_mul_action (R : Type u) (M : Type v) [has_smul R M] :
Type v

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

Instances for sub_mul_action
source
@[protected, instance]
def sub_mul_action.set_like {R : Type u} {M : Type v} [has_smul R M] :
set_like (sub_mul_action R M) M
Equations
source
@[protected, instance]
def sub_mul_action.smul_mem_class {R : Type u} {M : Type v} [has_smul R M] :
smul_mem_class (sub_mul_action R M) R M
Equations
source
@[simp]
theorem sub_mul_action.mem_carrier {R : Type u} {M : Type v} [has_smul R M] {p : sub_mul_action R M} {x : M} :
x ∈ p.carrier ↔ x ∈ ↑p
source
@[ext]
theorem sub_mul_action.ext {R : Type u} {M : Type v} [has_smul R M] {p q : sub_mul_action R M} (h : ∀ (x : M), x ∈ p ↔ x ∈ q) :
p = q
source
@[protected]
def sub_mul_action.copy {R : Type u} {M : Type v} [has_smul R M] (p : sub_mul_action R M) (s : set M) (hs : s = ↑p) :
sub_mul_action R M

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

Equations
source
@[simp]
theorem sub_mul_action.coe_copy {R : Type u} {M : Type v} [has_smul R M] (p : sub_mul_action R M) (s : set M) (hs : s = ↑p) :
↑(p.copy s hs) = s
source
theorem sub_mul_action.copy_eq {R : Type u} {M : Type v} [has_smul R M] (p : sub_mul_action R M) (s : set M) (hs : s = ↑p) :
p.copy s hs = p
source
@[protected, instance]
def sub_mul_action.has_bot {R : Type u} {M : Type v} [has_smul R M] :
has_bot (sub_mul_action R M)
Equations
source
@[protected, instance]
def sub_mul_action.inhabited {R : Type u} {M : Type v} [has_smul R M] :
inhabited (sub_mul_action R M)
Equations
source
theorem sub_mul_action.smul_mem {R : Type u} {M : Type v} [has_smul R M] (p : sub_mul_action R M) {x : M} (r : R) (h : x ∈ p) :
r • x ∈ p
source
@[protected, instance]
def sub_mul_action.has_smul {R : Type u} {M : Type v} [has_smul R M] (p : sub_mul_action R M) :
has_smul R ↥p
Equations
source
@[simp, norm_cast]
theorem sub_mul_action.coe_smul {R : Type u} {M : Type v} [has_smul R M] {p : sub_mul_action R M} (r : R) (x : ↥p) :
↑(r • x) = r • ↑x
source
@[simp, norm_cast]
theorem sub_mul_action.coe_mk {R : Type u} {M : Type v} [has_smul R M] {p : sub_mul_action R M} (x : M) (hx : x ∈ p) :
↑⟨x, hx⟩ = x
source
@[protected]
def sub_mul_action.subtype {R : Type u} {M : Type v} [has_smul R M] (p : sub_mul_action R M) :
↥p →[R] M

Embedding of a submodule p to the ambient space M.

Equations
source
@[simp]
theorem sub_mul_action.subtype_apply {R : Type u} {M : Type v} [has_smul R M] (p : sub_mul_action R M) (x : ↥p) :
⇑(p.subtype) x = ↑x
source
theorem sub_mul_action.subtype_eq_val {R : Type u} {M : Type v} [has_smul R M] (p : sub_mul_action R M) :
⇑(p.subtype) = subtype.val
source
@[protected, instance]
def sub_mul_action.smul_mem_class.to_mul_action {R : Type u} {M : Type v} [monoid R] [mul_action R M] {A : Type u_1} [set_like A M] [hA : smul_mem_class A R M] (S' : A) :
mul_action R ↥S'

A sub_mul_action of a mul_action is a mul_action.

Equations
source
@[protected]
def sub_mul_action.smul_mem_class.subtype {R : Type u} {M : Type v} [monoid R] [mul_action R M] {A : Type u_1} [set_like A M] [hA : smul_mem_class A R M] (S' : A) :
↥S' →[R] M

The natural mul_action_hom over R from a sub_mul_action of M to M.

Equations
source
@[protected, simp]
theorem sub_mul_action.smul_mem_class.coe_subtype {R : Type u} {M : Type v} [monoid R] [mul_action R M] {A : Type u_1} [set_like A M] [hA : smul_mem_class A R M] (S' : A) :
⇑(sub_mul_action.smul_mem_class.subtype S') = coe
source
theorem sub_mul_action.smul_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [monoid R] [mul_action R M] [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (p : sub_mul_action R M) (s : S) {x : M} (h : x ∈ p) :
s • x ∈ p
source
@[protected, instance]
def sub_mul_action.has_smul' {S : Type u'} {R : Type u} {M : Type v} [monoid R] [mul_action R M] [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (p : sub_mul_action R M) :
has_smul S ↥p
Equations
source
@[protected, instance]
def sub_mul_action.is_scalar_tower {S : Type u'} {R : Type u} {M : Type v} [monoid R] [mul_action R M] [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (p : sub_mul_action R M) :
is_scalar_tower S R ↥p
source
@[protected, instance]
def sub_mul_action.is_scalar_tower' {S : Type u'} {R : Type u} {M : Type v} [monoid R] [mul_action R M] [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (p : sub_mul_action R M) {S' : Type u_1} [has_smul S' R] [has_smul S' S] [has_smul S' M] [is_scalar_tower S' R M] [is_scalar_tower S' S M] :
is_scalar_tower S' S ↥p
source
@[simp, norm_cast]
theorem sub_mul_action.coe_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [monoid R] [mul_action R M] [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (p : sub_mul_action R M) (s : S) (x : ↥p) :
↑(s • x) = s • ↑x
source
@[simp]
theorem sub_mul_action.smul_mem_iff' {R : Type u} {M : Type v} [monoid R] [mul_action R M] (p : sub_mul_action R M) {G : Type u_1} [group G] [has_smul G R] [mul_action G M] [is_scalar_tower G R M] (g : G) {x : M} :
g • x ∈ p ↔ x ∈ p
source
@[protected, instance]
def sub_mul_action.is_central_scalar {S : Type u'} {R : Type u} {M : Type v} [monoid R] [mul_action R M] [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (p : sub_mul_action R M) [has_smul Sᵐᵒᵖ R] [has_smul Sᵐᵒᵖ M] [is_scalar_tower Sᵐᵒᵖ R M] [is_central_scalar S M] :
is_central_scalar S ↥p
source
@[protected, instance]
def sub_mul_action.mul_action' {S : Type u'} {R : Type u} {M : Type v} [monoid R] [mul_action R M] [monoid S] [has_smul S R] [mul_action S M] [is_scalar_tower S R M] (p : sub_mul_action R M) :
mul_action S ↥p

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

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

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

source
theorem sub_mul_action.stabilizer_of_sub_mul.submonoid {R : Type u} {M : Type v} [monoid R] [mul_action R M] {p : sub_mul_action R M} (m : ↥p) :
mul_action.stabilizer.submonoid R m = mul_action.stabilizer.submonoid R ↑m

Stabilizers in monoid sub_mul_action coincide with stabilizers in the ambient space

source
theorem sub_mul_action.stabilizer_of_sub_mul {R : Type u} {M : Type v} [group R] [mul_action R M] {p : sub_mul_action R M} (m : ↥p) :
mul_action.stabilizer R m = mul_action.stabilizer R ↑m

Stabilizers in group sub_mul_action coincide with stabilizers in the ambient space

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

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

Equations
source
theorem sub_mul_action.neg_mem {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (p : sub_mul_action R M) {x : M} (hx : x ∈ p) :
-x ∈ p
source
@[simp]
theorem sub_mul_action.neg_mem_iff {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (p : sub_mul_action R M) {x : M} :
-x ∈ p ↔ x ∈ p
source
@[protected, instance]
def sub_mul_action.has_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (p : sub_mul_action R M) :
has_neg ↥p
Equations
source
@[simp, norm_cast]
theorem sub_mul_action.coe_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (p : sub_mul_action R M) (x : ↥p) :
↑-x = -↑x
source
theorem sub_mul_action.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [group_with_zero S] [monoid R] [mul_action R M] [has_smul S R] [mul_action S M] [is_scalar_tower S R M] (p : sub_mul_action R M) {s : S} {x : M} (s0 : s ≠ 0) :
s • x ∈ p ↔ x ∈ p