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
A sub_mul_action is a set which is closed under scalar multiplication.
@[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
- sub_mul_action.set.has_coe_t = {coe := λ (s : sub_mul_action R M), s.carrier}
@[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
- sub_mul_action.has_mem = {mem := λ (x : M) (p : sub_mul_action R M), x ∈ ↑p}
@[instance]
Equations
- sub_mul_action.has_coe_to_sort = {S := Type v, coe := λ (p : sub_mul_action R M), {x // x ∈ p}}
@[instance]
def
sub_mul_action.has_top
{R : Type u}
{M : Type v}
[has_scalar R M] :
has_top (sub_mul_action R M)
@[instance]
def
sub_mul_action.has_bot
{R : Type u}
{M : Type v}
[has_scalar R M] :
has_bot (sub_mul_action R M)
@[instance]
def
sub_mul_action.inhabited
{R : Type u}
{M : Type v}
[has_scalar R M] :
inhabited (sub_mul_action R M)
Equations
@[simp]
theorem
sub_mul_action.coe_sort_coe
{R : Type u}
{M : Type v}
[has_scalar R M]
(p : sub_mul_action R M) :
theorem
sub_mul_action.exists
{R : Type u}
{M : Type v}
[has_scalar R M]
{p : sub_mul_action R M}
{q : ↥p → Prop} :
theorem
sub_mul_action.forall
{R : Type u}
{M : Type v}
[has_scalar R M]
{p : sub_mul_action R M}
{q : ↥p → Prop} :
@[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} :
theorem
sub_mul_action.ext'_iff
{R : Type u}
{M : Type v}
[has_scalar R M]
{p q : sub_mul_action R M} :
@[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
@[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} :
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) :
@[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
@[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} :
@[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) :
@[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) :
@[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) :
@[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) :
Embedding of a submodule p
to the ambient space M
.
@[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) :
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
@[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) :
@[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
- p.mul_action = {to_has_scalar := {smul := has_scalar.smul p.has_scalar}, one_smul := _, mul_smul := _}
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
@[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] :
If the scalar product forms a semimodule
, and the sub_mul_action
is not ⊥
, then the
subset inherits the zero.
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) :
@[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} :
@[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) :
@[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) :
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) :