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) [inst : SMul R M] [inst : SetLike S M] :
  • Multiplication by a scalar on an element of the set remains in the set.

    smul_mem : ∀ {s : S} (r : R) {m : M}, m sr m s

SMulMemClass S R M says S is a type of subsets s ≤ M≤ 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.

Instances
    class VAddMemClass (S : Type u_1) (R : outParam (Type u_2)) (M : Type u_3) [inst : VAdd R M] [inst : SetLike S M] :
    • Addition by a scalar with an element of the set remains in the set.

      vadd_mem : ∀ {s : S} (r : R) {m : M}, m sr +ᵥ m s

    VAddMemClass S R M says S is a type of subsets s ≤ M≤ 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.

    Instances
      instance SetLike.vadd {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst : SetLike S M] [hS : VAddMemClass S R M] (s : S) :
      VAdd R { x // x s }

      A subset closed under the additive action inherits that action.

      Equations
      def SetLike.vadd.proof_1 {S : Type u_2} {R : Type u_3} {M : Type u_1} [inst : VAdd R M] [inst : SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
      r +ᵥ x s
      Equations
      instance SetLike.smul {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst : SetLike S M] [hS : SMulMemClass S R M] (s : S) :
      SMul R { x // x s }

      A subset closed under the scalar action inherits that action.

      Equations
      @[simp]
      theorem SetLike.val_vadd {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst : SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
      ↑(r +ᵥ x) = r +ᵥ x
      @[simp]
      theorem SetLike.val_smul {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst : SetLike S M] [hS : SMulMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
      ↑(r x) = r x
      @[simp]
      theorem SetLike.mk_vadd_mk {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst : SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : M) (hx : x s) :
      r +ᵥ { val := x, property := hx } = { val := r +ᵥ x, property := (_ : r +ᵥ x s) }
      @[simp]
      theorem SetLike.mk_smul_mk {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst : SetLike S M] [hS : SMulMemClass S R M] (s : S) (r : R) (x : M) (hx : x s) :
      r { val := x, property := hx } = { val := r x, property := (_ : r x s) }
      theorem SetLike.vadd_def {S : Type u'} {R : Type u} {M : Type v} [inst : VAdd R M] [inst : SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
      r +ᵥ x = { val := ↑(r +ᵥ x), property := (_ : r +ᵥ x s) }
      theorem SetLike.smul_def {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst : SetLike S M] [hS : SMulMemClass S R M] (s : S) (r : R) (x : { x // x s }) :
      r x = { val := ↑(r x), property := (_ : r x s) }
      @[simp]
      theorem SetLike.forall_smul_mem_iff {R : Type u_1} {M : Type u_2} {S : Type u_3} [inst : Monoid R] [inst : MulAction R M] [inst : SetLike S M] [inst : SMulMemClass S R M] {N : S} {x : M} :
      (∀ (a : R), a x N) x N
      structure SubMulAction (R : Type u) (M : Type v) [inst : SMul R M] :
      • The underlying set of a SubMulAction.

        carrier : Set M
      • The carrier set is closed under scalar multiplication.

        smul_mem' : ∀ (c : R) {x : M}, x carrierc x carrier

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

      Instances For
        instance SubMulAction.instSetLikeSubMulAction {R : Type u} {M : Type v} [inst : SMul R M] :
        Equations
        • SubMulAction.instSetLikeSubMulAction = { coe := SubMulAction.carrier, coe_injective' := (_ : ∀ (p q : SubMulAction R M), p.carrier = q.carrierp = q) }
        Equations
        • SubMulAction.instSMulMemClassSubMulActionInstSetLikeSubMulAction = { smul_mem := (_ : ∀ {s : SubMulAction R M} (c : R) {x : M}, x s.carrierc x s.carrier) }
        @[simp]
        theorem SubMulAction.mem_carrier {R : Type u} {M : Type v} [inst : SMul R M] {p : SubMulAction R M} {x : M} :
        x p.carrier x p
        theorem SubMulAction.ext {R : Type u} {M : Type v} [inst : 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} [inst : 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
        @[simp]
        theorem SubMulAction.coe_copy {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = p) :
        ↑(SubMulAction.copy p s hs) = s
        theorem SubMulAction.copy_eq {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = p) :
        instance SubMulAction.instBotSubMulAction {R : Type u} {M : Type v} [inst : SMul R M] :
        Equations
        • SubMulAction.instBotSubMulAction = { bot := { carrier := , smul_mem' := (_ : R∀ (h : M), ¬h ) } }
        instance SubMulAction.instInhabitedSubMulAction {R : Type u} {M : Type v} [inst : SMul R M] :
        Equations
        • SubMulAction.instInhabitedSubMulAction = { default := }
        theorem SubMulAction.smul_mem {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) {x : M} (r : R) (h : x p) :
        r x p
        Equations
        @[simp]
        theorem SubMulAction.val_smul {R : Type u} {M : Type v} [inst : SMul R M] {p : SubMulAction R M} (r : R) (x : { x // x p }) :
        ↑(r x) = r x
        def SubMulAction.subtype {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) :
        { x // x p } →[R] M

        Embedding of a submodule p to the ambient space M.

        Equations
        @[simp]
        theorem SubMulAction.subtype_apply {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (x : { x // x p }) :
        ↑(SubMulAction.subtype p) x = x
        theorem SubMulAction.subtype_eq_val {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) :
        ↑(SubMulAction.subtype p) = Subtype.val
        instance SubMulAction.SMulMemClass.toMulAction {R : Type u} {M : Type v} [inst : Monoid R] [inst : MulAction R M] {A : Type u_1} [inst : SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
        MulAction R { x // x S' }

        A SubMulAction of a MulAction is a MulAction.

        Equations
        def SubMulAction.SMulMemClass.subtype {R : Type u} {M : Type v} [inst : Monoid R] [inst : MulAction R M] {A : Type u_1} [inst : SetLike A M] [hA : SMulMemClass A R M] (S' : A) :
        { x // x S' } →[R] 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} [inst : Monoid R] [inst : MulAction R M] {A : Type u_1} [inst : 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} [inst : Monoid R] [inst : MulAction R M] [inst : SMul S R] [inst : SMul S M] [inst : 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} [inst : Monoid R] [inst : MulAction R M] [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] (p : SubMulAction R M) :
        SMul S { x // x p }
        Equations
        instance SubMulAction.isScalarTower {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst : MulAction R M] [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] (p : SubMulAction R M) :
        IsScalarTower S R { x // x p }
        Equations
        instance SubMulAction.isScalarTower' {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst : MulAction R M] [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] (p : SubMulAction R M) {S' : Type u_1} [inst : SMul S' R] [inst : SMul S' S] [inst : SMul S' M] [inst : IsScalarTower S' R M] [inst : IsScalarTower S' S M] :
        IsScalarTower S' S { x // x p }
        Equations
        @[simp]
        theorem SubMulAction.val_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst : MulAction R M] [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] (p : SubMulAction R M) (s : S) (x : { x // x p }) :
        ↑(s x) = s x
        @[simp]
        theorem SubMulAction.smul_mem_iff' {R : Type u} {M : Type v} [inst : Monoid R] [inst : MulAction R M] (p : SubMulAction R M) {G : Type u_1} [inst : Group G] [inst : SMul G R] [inst : MulAction G M] [inst : 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} [inst : Monoid R] [inst : MulAction R M] [inst : SMul S R] [inst : SMul S M] [inst : IsScalarTower S R M] (p : SubMulAction R M) [inst : SMul Sᵐᵒᵖ R] [inst : SMul Sᵐᵒᵖ M] [inst : IsScalarTower Sᵐᵒᵖ R M] [inst : IsCentralScalar S M] :
        IsCentralScalar S { x // x p }
        Equations
        instance SubMulAction.mulAction' {S : Type u'} {R : Type u} {M : Type v} [inst : Monoid R] [inst : MulAction R M] [inst : Monoid S] [inst : SMul S R] [inst : MulAction S M] [inst : IsScalarTower S R M] (p : SubMulAction R M) :
        MulAction S { x // x p }

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

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

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

        theorem SubMulAction.stabilizer_of_subMul.submonoid {R : Type u} {M : Type v} [inst : Monoid R] [inst : MulAction R M] {p : SubMulAction R M} (m : { x // x p }) :

        Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space

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

        Stabilizers in group SubMulAction coincide with stabilizers in the ambient space

        theorem SubMulAction.zero_mem {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : SubMulAction R M) (h : Set.Nonempty p) :
        0 p

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

        Equations
        • One or more equations did not get rendered due to their size.
        theorem SubMulAction.neg_mem {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] [inst : 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} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] (p : SubMulAction R M) {x : M} :
        -x p x p
        @[simp]
        theorem SubMulAction.val_neg {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] (p : SubMulAction R M) (x : { x // x p }) :
        ↑(-x) = -x
        theorem SubMulAction.smul_mem_iff {S : Type u'} {R : Type u} {M : Type v} [inst : GroupWithZero S] [inst : Monoid R] [inst : MulAction R M] [inst : SMul S R] [inst : MulAction S M] [inst : IsScalarTower S R M] (p : SubMulAction R M) {s : S} {x : M} (s0 : s 0) :
        s x p x p