mathlib documentation

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 M which is closed with respect to scalar multiplication.

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

Tags #

submodule, mul_action

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

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

source
@[instance]
def sub_mul_action.set.has_coe_t {R : Type u} {M : Type v} [has_scalar R M] :
has_coe_t (sub_mul_action R M) (set M)
Equations
source
@[instance]
def sub_mul_action.has_mem {R : Type u} {M : Type v} [has_scalar R M] :
has_mem M (sub_mul_action R M)
Equations
source
@[instance]
def sub_mul_action.has_coe_to_sort {R : Type u} {M : Type v} [has_scalar R M] :
has_coe_to_sort (sub_mul_action R M)
Equations
source
@[instance]
def sub_mul_action.has_top {R : Type u} {M : Type v} [has_scalar R M] :
has_top (sub_mul_action R M)
Equations
source
@[instance]
def sub_mul_action.has_bot {R : Type u} {M : Type v} [has_scalar R M] :
has_bot (sub_mul_action R M)
Equations
source
@[instance]
def sub_mul_action.inhabited {R : Type u} {M : Type v} [has_scalar R M] :
inhabited (sub_mul_action R M)
Equations
source
@[simp]
theorem sub_mul_action.coe_sort_coe {R : Type u} {M : Type v} [has_scalar R M] (p : sub_mul_action R M) :
↥↑p = ↥p
source
theorem sub_mul_action.exists {R : Type u} {M : Type v} [has_scalar R M] {p : sub_mul_action R M} {q : ↥p → Prop} :
(∃ (x : ↥p), q x) ↔ ∃ (x : M) (H : x ∈ p), q ⟨x, H⟩
source
theorem sub_mul_action.forall {R : Type u} {M : Type v} [has_scalar R M] {p : sub_mul_action R M} {q : ↥p → Prop} :
(∀ (x : ↥p), q x) ↔ ∀ (x : M) (H : x ∈ p), q ⟨x, H⟩
source
theorem sub_mul_action.coe_injective {R : Type u} {M : Type v} [has_scalar R M] :
function.injective coe
source
@[simp]
theorem sub_mul_action.coe_set_eq {R : Type u} {M : Type v} [has_scalar R M] {p q : sub_mul_action R M} :
↑p = ↑q ↔ p = q
source
theorem sub_mul_action.ext'_iff {R : Type u} {M : Type v} [has_scalar R M] {p q : sub_mul_action R M} :
p = q ↔ ↑p = ↑q
source
@[ext]
theorem sub_mul_action.ext {R : Type u} {M : Type v} [has_scalar R M] {p q : sub_mul_action R M} (h : ∀ (x : M), x ∈ p ↔ x ∈ q) :
p = q
source
@[simp]
theorem sub_mul_action.mem_coe {R : Type u} {M : Type v} [has_scalar R M] (p : sub_mul_action R M) {x : M} :
x ∈ ↑p ↔ x ∈ p
source
theorem sub_mul_action.smul_mem {R : Type u} {M : Type v} [has_scalar R M] (p : sub_mul_action R M) {x : M} (r : R) (h : x ∈ p) :
r • x ∈ p
source
@[instance]
def sub_mul_action.has_scalar {R : Type u} {M : Type v} [has_scalar R M] (p : sub_mul_action R M) :
has_scalar R ↥p
Equations
source
@[simp]
theorem sub_mul_action.coe_eq_coe {R : Type u} {M : Type v} [has_scalar R M] {p : sub_mul_action R M} {x y : ↥p} :
↑x = ↑y ↔ x = y
source
@[simp]
theorem sub_mul_action.coe_smul {R : Type u} {M : Type v} [has_scalar R M] {p : sub_mul_action R M} (r : R) (x : ↥p) :
↑(r • x) = r • ↑x
source
@[simp]
theorem sub_mul_action.coe_mk {R : Type u} {M : Type v} [has_scalar R M] {p : sub_mul_action R M} (x : M) (hx : x ∈ p) :
↑⟨x, hx⟩ = x
source
@[simp]
theorem sub_mul_action.coe_mem {R : Type u} {M : Type v} [has_scalar R M] {p : sub_mul_action R M} (x : ↥p) :
↑x ∈ p
source
@[simp]
theorem sub_mul_action.eta {R : Type u} {M : Type v} [has_scalar R M] {p : sub_mul_action R M} (x : ↥p) (hx : ↑x ∈ p) :
⟨↑x, hx⟩ = x
source
def sub_mul_action.subtype {R : Type u} {M : Type v} [has_scalar 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_scalar 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_scalar R M] (p : sub_mul_action R M) :
⇑(p.subtype) = subtype.val
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) {x : M} (u : units R) :
↑u • x ∈ p ↔ x ∈ p
source
@[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

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

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

If the scalar product forms a semimodule, 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] [semimodule 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] [semimodule R M] (p : sub_mul_action R M) {x : M} :
-x ∈ p ↔ x ∈ p
source
@[instance]
def sub_mul_action.has_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : sub_mul_action R M) :
has_neg ↥p
Equations
source
@[simp]
theorem sub_mul_action.coe_neg {R : Type u} {M : Type v} [ring R] [add_comm_group M] [semimodule R M] (p : sub_mul_action R M) (x : ↥p) :
↑-x = -↑x
source
theorem sub_mul_action.smul_mem_iff {R : Type u} {M : Type v} [division_ring R] [add_comm_group M] [module R M] (p : sub_mul_action R M) {r : R} {x : M} (r0 : r ≠ 0) :
r • x ∈ p ↔ x ∈ p