Documentation

Mathlib.GroupTheory.GroupAction.SubMulAction

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 #

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} :
∀ {inst : SMul R M} {inst_1 : 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} :
    ∀ {inst : VAdd R M} {inst_1 : 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.

    Not registered as an instance because R is an outParam in SMulMemClass S R M.

    Not registered as an instance because R is an outParam in SMulMemClass S R M.

    @[instance 50]
    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
    @[instance 50]
    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
    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 α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M 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] [MulMemClass S M] [IsScalarTower R M 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] [MulMemClass S M] [SMulCommClass R M 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} [Monoid R] [MulAction R M] [SetLike S M] [SMulMemClass S R M] {N : S} {x : M} :
    (∀ (a : R), a x N) x N
    @[instance 50]
    instance SetLike.vadd' {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] (s : S) :
    VAdd M s

    A subset closed under the additive action inherits that action.

    Equations
    @[instance 50]
    instance SetLike.smul' {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) :
    SMul M s

    A subset closed under the scalar action inherits that action.

    Equations
    @[simp]
    theorem SetLike.val_vadd_of_tower {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] (s : S) (r : M) (x : s) :
    (r +ᵥ x) = r +ᵥ x
    @[simp]
    theorem SetLike.val_smul_of_tower {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) (r : M) (x : s) :
    (r x) = r x
    @[simp]
    theorem SetLike.mk_vadd_of_tower_mk {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] (s : S) (r : M) (x : α) (hx : x s) :
    r +ᵥ x, hx = r +ᵥ x,
    @[simp]
    theorem SetLike.mk_smul_of_tower_mk {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) (r : M) (x : α) (hx : x s) :
    r x, hx = r x,
    theorem SetLike.vadd_of_tower_def {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] (s : S) (r : M) (x : s) :
    r +ᵥ x = r +ᵥ x,
    theorem SetLike.smul_of_tower_def {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) (r : M) (x : s) :
    r x = r x,
    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 : SubMulAction R M) (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] :
    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 : SubMulAction R M} {x : M} :
    x p.carrier x p
    theorem SubMulAction.ext_iff {R : Type u} {M : Type v} [SMul R M] {p : SubMulAction R M} {q : SubMulAction R M} :
    p = q ∀ (x : M), x p x q
    theorem SubMulAction.ext {R : Type u} {M : Type v} [SMul R M] {p : SubMulAction R M} {q : SubMulAction R M} (h : ∀ (x : M), x p x q) :
    p = q
    def SubMulAction.copy {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R 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
    • p.copy s hs = { carrier := s, smul_mem' := }
    @[simp]
    theorem SubMulAction.coe_copy {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) (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 : SubMulAction R M) (s : Set M) (hs : s = p) :
    p.copy s hs = p
    instance SubMulAction.instBot {R : Type u} {M : Type v} [SMul R M] :
    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 : SubMulAction R M) {x : M} (r : R) (h : x p) :
    r x p
    instance SubMulAction.instSMulSubtypeMem {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) :
    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 : SubMulAction R M} (r : R) (x : p) :
    (r x) = r x
    def SubMulAction.subtype {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) :
    p →ₑ[id] M

    Embedding of a submodule p to the ambient space M.

    Equations
    • p.subtype = { toFun := Subtype.val, map_smul' := }
    @[simp]
    theorem SubMulAction.subtype_apply {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) (x : p) :
    p.subtype x = x
    theorem SubMulAction.subtype_eq_val {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) :
    p.subtype = Subtype.val
    @[instance 75]
    instance SubMulAction.SMulMemClass.toMulAction {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {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} [Monoid R] [MulAction R M] {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
    @[simp]
    theorem SubMulAction.SMulMemClass.coeSubtype {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {A : Type u_1} [SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
    theorem SubMulAction.smul_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M} (h : x p) :
    s x p
    instance SubMulAction.smul' {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) :
    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} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) :
    IsScalarTower S R p
    Equations
    • =
    instance SubMulAction.isScalarTower' {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) {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} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) (s : S) (x : p) :
    (s x) = s x
    @[simp]
    theorem SubMulAction.smul_mem_iff' {R : Type u} {M : Type v} [Monoid R] [MulAction R M] (p : SubMulAction R M) {G : Type u_1} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] (g : G) {x : M} :
    g x p x p
    instance SubMulAction.isCentralScalar {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] :
    Equations
    • =
    instance SubMulAction.mulAction' {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] (p : SubMulAction R M) :
    MulAction S p

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

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

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

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

    Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space

    theorem SubMulAction.stabilizer_of_subMul {R : Type u} {M : Type v} [Group R] [MulAction R M] {p : SubMulAction R M} (m : p) :

    Stabilizers in group SubMulAction coincide with stabilizers in the ambient space

    theorem SubMulAction.zero_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : SubMulAction R M) (h : (↑p).Nonempty) :
    0 p
    instance SubMulAction.instZeroSubtypeMemOfNonempty {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : SubMulAction R M) [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] [AddCommGroup M] [Module R M] (p : SubMulAction R M) {x : M} (hx : x p) :
    -x p
    @[simp]
    theorem SubMulAction.neg_mem_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) {x : M} :
    -x p x p
    instance SubMulAction.instNegSubtypeMem {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) :
    Neg p
    Equations
    • p.instNegSubtypeMem = { neg := fun (x : p) => -x, }
    @[simp]
    theorem SubMulAction.val_neg {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) (x : p) :
    (-x) = -x
    theorem SubMulAction.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [GroupWithZero S] [Monoid R] [MulAction R M] [SMul S R] [MulAction S M] [IsScalarTower S R M] (p : SubMulAction R M) {s : S} {x : M} (s0 : s 0) :
    s x p x p
    def SubMulAction.inclusion {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) :
    s →ₑ[id] α

    The inclusion of a SubMulAction into the ambient set, as an equivariant map

    Equations
    • s.inclusion = { toFun := Subtype.val, map_smul' := }
    theorem SubMulAction.inclusion.toFun_eq_coe {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) :
    s.inclusion.toFun = Subtype.val
    theorem SubMulAction.inclusion.coe_eq {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) :
    s.inclusion = Subtype.val
    theorem SubMulAction.image_inclusion {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) :
    Set.range s.inclusion = s.carrier
    theorem SubMulAction.inclusion_injective {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) :
    Function.Injective s.inclusion