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} [SMul R M] [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} [VAdd R M] [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.

      theorem SetLike.vadd.proof_1 {S : Type u_2} {R : Type u_3} {M : Type u_1} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) (r : R) (x : { x : M // x s }) :
      r +ᵥ x s
      @[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 { x : M // x 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 { x : M // x 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 { x : M // x s } { x : M // x 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 { x : M // x s } { x : M // x 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 : { x : M // 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 : { x : M // 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 : { x : M // 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 : { x : M // 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
      theorem SetLike.vadd'.proof_1 {S : Type u_2} {M : Type u_3} {N : Type u_4} {α : Type u_1} [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] (s : S) (r : M) (x : { x : α // x s }) :
      r +ᵥ x s
      @[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 { x : α // x 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 { x : α // x 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 : { x : α // 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 : { x : α // 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 : { x : α // 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 : { x : α // 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' := }
        Instances For
          @[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 { x : M // x p }
          Equations
          • p.instSMulSubtypeMem = { smul := fun (c : R) (x : { x : M // 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 : { x : M // x p }) :
          (r x) = r x
          def SubMulAction.subtype {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) :
          { x : M // x p } →ₑ[id] M

          Embedding of a submodule p to the ambient space M.

          Equations
          • p.subtype = { toFun := Subtype.val, map_smul' := }
          Instances For
            @[simp]
            theorem SubMulAction.subtype_apply {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) (x : { x : 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 { x : M // x 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) :
            { x : M // x S' } →ₑ[id] M

            The natural MulActionHom over R from a SubMulAction of M to M.

            Equations
            Instances For
              @[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 { x : M // x p }
              Equations
              • p.smul' = { smul := fun (c : S) (x : { x : M // 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 { x : M // x 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 { x : M // x 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 : { x : M // 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] :
              IsCentralScalar S { x : M // x p }
              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 { x : M // 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} [Monoid R] [MulAction R M] (p : SubMulAction R M) :
              MulAction R { x : M // x 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 : { x : M // 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.val_preimage_orbit {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {p : SubMulAction R M} (m : { x : M // x 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 : { x : M // x p }} {m : { x : M // x p }} :

              Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space

              theorem SubMulAction.orbitRel_of_subMul {R : Type u} {M : Type v} [Group R] [MulAction R M] (p : SubMulAction R M) :
              MulAction.orbitRel R { x : M // x p } = Setoid.comap Subtype.val (MulAction.orbitRel R M)
              theorem SubMulAction.stabilizer_of_subMul {R : Type u} {M : Type v} [Group R] [MulAction R M] {p : SubMulAction R M} (m : { x : M // x 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 { x : M // x p }] :
              Zero { x : M // x 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 { x : M // x p }
              Equations
              • p.instNegSubtypeMem = { neg := fun (x : { x : M // 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 : { x : 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 α) :
              { x : α // x s } →ₑ[id] α

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

              Equations
              • s.inclusion = { toFun := Subtype.val, map_smul' := }
              Instances For
                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