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

• SubMulAction.mulAction - the MulAction R M transferred to the subtype.
• SubMulAction.mulAction' - the MulAction S M transferred to the subtype when IsScalarTower S R M.
• SubMulAction.isScalarTower - the IsScalarTower S R M transferred to the subtype.
• SubMulAction.inclusion — the inclusion of a SubMulAction, as an equivariant map

Tags

submodule, multiplicative action

class SMulMemClass (S : Type u_1) (R : outParam (Type u_2)) (M : Type u_3) [SMul R M] [SetLike S M] : Prop

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 ∈ s → r • 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] : Prop

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 ∈ s → r +ᵥ m ∈ s

  Addition by a scalar with an element of the set remains in the set.

theorem AddSubmonoidClass.nsmulMemClass {S : Type u_1} {M : Type u_2} [AddMonoid M] [SetLike S M] [AddSubmonoidClass S M] : SMulMemClass S ℕ M

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

theorem AddSubgroupClass.zsmulMemClass {S : Type u_1} {M : Type u_2} [SubNegMonoid M] [SetLike S M] [AddSubgroupClass S M] : SMulMemClass S ℤ M

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

@[implicit_reducible, 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

• SetLike.smul s = { smul := fun (r : R) (x : ↥s) => ⟨r • ↑x, ⋯⟩ }

@[implicit_reducible, 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

• SetLike.vadd s = { vadd := fun (r : R) (x : ↥s) => ⟨r +ᵥ ↑x, ⋯⟩ }

@[instance 50]

instance SetLike.instSMulCommClassSubtypeMem {S : Type u'} {T : Type u''} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) [SMul T M] [SMulMemClass S T M] [SMulCommClass T R M] : SMulCommClass T R ↥s

@[instance 50]

instance SetLike.instVAddCommClassSubtypeMem {S : Type u'} {T : Type u''} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) [VAdd T M] [VAddMemClass S T M] [VAddCommClass T R M] : VAddCommClass T R ↥s

@[instance 50]

instance SetLike.instIsLeftCancelSMulSubtypeMem {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) [IsLeftCancelSMul R M] : IsLeftCancelSMul R ↥s

@[instance 50]

instance SetLike.instIsLeftCancelVAddSubtypeMem {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) [IsLeftCancelVAdd R M] : IsLeftCancelVAdd R ↥s

@[instance 50]

instance SetLike.instIsCancelSMulSubtypeMem {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S) [IsCancelSMul R M] : IsCancelSMul R ↥s

@[instance 50]

instance SetLike.instIsCancelVAddSubtypeMem {S : Type u'} {R : Type u} {M : Type v} [VAdd R M] [SetLike S M] [hS : VAddMemClass S R M] (s : S) [IsCancelVAdd R M] : IsCancelVAdd R ↥s

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 α] : SMulMemClass S M α

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.

theorem VAddMemClass.ofVAddAssocClass (S : Type u_1) (M : Type u_2) (N : Type u_3) (α : Type u_4) [SetLike S α] [VAdd M N] [VAdd M α] [AddMonoid N] [AddAction N α] [VAddMemClass S N α] [VAddAssocClass M N α] : VAddMemClass S M α

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

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

@[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.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.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, ⋯⟩

@[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, ⋯⟩

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, ⋯⟩

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, ⋯⟩

@[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

@[implicit_reducible, 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

• SetLike.smul' s = { smul := fun (r : M) (x : ↥s) => ⟨r • ↑x, ⋯⟩ }

@[implicit_reducible, 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

• SetLike.vadd' s = { vadd := fun (r : M) (x : ↥s) => ⟨r +ᵥ ↑x, ⋯⟩ }

@[instance 50]

instance SetLike.instIsScalarTowerSubtypeMem {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) : IsScalarTower M N ↥s

@[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.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.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, ⋯⟩

@[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, ⋯⟩

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, ⋯⟩

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, ⋯⟩

@[instance 50]

instance SetLike.instSMulCommClassSubtypeMem_1 {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) [SMulCommClass M N α] : SMulCommClass M N ↥s

@[instance 50]

instance SetLike.instVAddCommClassSubtypeMem_1 {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) [VAddCommClass M N α] : VAddCommClass M N ↥s

@[instance 50]

instance SetLike.instSMulCommClassSubtypeMem_2 {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) [SMulCommClass N M α] : SMulCommClass N M ↥s

@[instance 50]

instance SetLike.instVAddCommClassSubtypeMem_2 {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) [VAddCommClass N M α] : VAddCommClass N M ↥s

structure SubAddAction (R : Type u) (M : Type v) [VAdd R M] : Type v

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

• carrier : Set M

  The underlying set of a SubAddAction.

• vadd_mem' (c : R) {x : M} : x ∈ self.carrier → c +ᵥ x ∈ self.carrier

  The carrier set is closed under scalar multiplication.

structure SubMulAction (R : Type u) (M : Type v) [SMul R M] : Type v

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.carrier → c • x ∈ self.carrier

  The carrier set is closed under scalar multiplication.

@[implicit_reducible]

instance SubMulAction.instSetLike {R : Type u} {M : Type v} [SMul R M] : SetLike (SubMulAction R M) M

Equations

• SubMulAction.instSetLike = { coe := SubMulAction.carrier, coe_injective' := ⋯ }

@[implicit_reducible]

instance SubAddAction.instSetLike {R : Type u} {M : Type v} [VAdd R M] : SetLike (SubAddAction R M) M

Equations

• SubAddAction.instSetLike = { coe := SubAddAction.carrier, coe_injective' := ⋯ }

@[implicit_reducible]

instance SubMulAction.instPartialOrder {R : Type u} {M : Type v} [SMul R M] : PartialOrder (SubMulAction R M)

Equations

• SubMulAction.instPartialOrder = PartialOrder.ofSetLike (SubMulAction R M) M

@[implicit_reducible]

instance SubAddAction.instPartialOrder {R : Type u} {M : Type v} [VAdd R M] : PartialOrder (SubAddAction R M)

Equations

• SubAddAction.instPartialOrder = PartialOrder.ofSetLike (SubAddAction R M) M

instance SubMulAction.instSMulMemClass {R : Type u} {M : Type v} [SMul R M] : SMulMemClass (SubMulAction R M) R M

instance SubAddAction.instVAddMemClass {R : Type u} {M : Type v} [VAdd R M] : VAddMemClass (SubAddAction R M) R M

@[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

@[simp]

theorem SubAddAction.mem_carrier {R : Type u} {M : Type v} [VAdd R M] {p : SubAddAction R M} {x : M} : x ∈ p.carrier ↔ x ∈ ↑p

theorem SubMulAction.ext {R : Type u} {M : Type v} [SMul R M] {p q : SubMulAction R M} (h : ∀ (x : M), x ∈ p ↔ x ∈ q) : p = q

theorem SubAddAction.ext {R : Type u} {M : Type v} [VAdd R M] {p q : SubAddAction R M} (h : ∀ (x : M), x ∈ p ↔ x ∈ q) : p = q

theorem SubMulAction.ext_iff {R : Type u} {M : Type v} [SMul R M] {p q : SubMulAction R M} : p = q ↔ ∀ (x : M), x ∈ p ↔ x ∈ q

theorem SubAddAction.ext_iff {R : Type u} {M : Type v} [VAdd R M] {p q : SubAddAction R M} : p = q ↔ ∀ (x : M), x ∈ p ↔ x ∈ q

def SubMulAction.copy {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = ↑p) : SubMulAction R M

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' := ⋯ }

def SubAddAction.copy {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) (s : Set M) (hs : s = ↑p) : SubAddAction R M

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, vadd_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

@[simp]

theorem SubAddAction.coe_copy {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction 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

theorem SubAddAction.copy_eq {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) (s : Set M) (hs : s = ↑p) : p.copy s hs = p

@[implicit_reducible]

instance SubMulAction.instBot {R : Type u} {M : Type v} [SMul R M] : Bot (SubMulAction R M)

Equations

• SubMulAction.instBot = { bot := { carrier := ∅, smul_mem' := ⋯ } }

@[implicit_reducible]

instance SubAddAction.instBot {R : Type u} {M : Type v} [VAdd R M] : Bot (SubAddAction R M)

Equations

• SubAddAction.instBot = { bot := { carrier := ∅, vadd_mem' := ⋯ } }

@[implicit_reducible]

instance SubMulAction.instInhabited {R : Type u} {M : Type v} [SMul R M] : Inhabited (SubMulAction R M)

Equations

• SubMulAction.instInhabited = { default := ⊥ }

@[implicit_reducible]

instance SubAddAction.instInhabited {R : Type u} {M : Type v} [VAdd R M] : Inhabited (SubAddAction R M)

Equations

• SubAddAction.instInhabited = { default := ⊥ }

@[implicit_reducible]

instance SubMulAction.instTop {R : Type u} {M : Type v} [SMul R M] : Top (SubMulAction R M)

Equations

• SubMulAction.instTop = { top := { carrier := Set.univ, smul_mem' := ⋯ } }

@[implicit_reducible]

instance SubAddAction.instTop {R : Type u} {M : Type v} [VAdd R M] : Top (SubAddAction R M)

Equations

• SubAddAction.instTop = { top := { carrier := Set.univ, vadd_mem' := ⋯ } }

@[implicit_reducible]

instance SubMulAction.instMax {R : Type u} {M : Type v} [SMul R M] : Max (SubMulAction R M)

Equations

• SubMulAction.instMax = { max := fun (s t : SubMulAction R M) => { carrier := ↑s ∪ ↑t, smul_mem' := ⋯ } }

@[implicit_reducible]

instance SubAddAction.instMax {R : Type u} {M : Type v} [VAdd R M] : Max (SubAddAction R M)

Equations

• SubAddAction.instMax = { max := fun (s t : SubAddAction R M) => { carrier := ↑s ∪ ↑t, vadd_mem' := ⋯ } }

@[implicit_reducible]

instance SubMulAction.instMin {R : Type u} {M : Type v} [SMul R M] : Min (SubMulAction R M)

Equations

• SubMulAction.instMin = { min := fun (s t : SubMulAction R M) => { carrier := ↑s ∩ ↑t, smul_mem' := ⋯ } }

@[implicit_reducible]

instance SubAddAction.instMin {R : Type u} {M : Type v} [VAdd R M] : Min (SubAddAction R M)

Equations

• SubAddAction.instMin = { min := fun (s t : SubAddAction R M) => { carrier := ↑s ∩ ↑t, vadd_mem' := ⋯ } }

@[implicit_reducible]

instance SubMulAction.instSupSet {R : Type u} {M : Type v} [SMul R M] : SupSet (SubMulAction R M)

Equations

• SubMulAction.instSupSet = { sSup := fun (S : Set (SubMulAction R M)) => { carrier := ⋃ s ∈ S, ↑s, smul_mem' := ⋯ } }

@[implicit_reducible]

instance SubAddAction.instSupSet {R : Type u} {M : Type v} [VAdd R M] : SupSet (SubAddAction R M)

Equations

• SubAddAction.instSupSet = { sSup := fun (S : Set (SubAddAction R M)) => { carrier := ⋃ s ∈ S, ↑s, vadd_mem' := ⋯ } }

@[implicit_reducible]

instance SubMulAction.instInfSet {R : Type u} {M : Type v} [SMul R M] : InfSet (SubMulAction R M)

Equations

• SubMulAction.instInfSet = { sInf := fun (S : Set (SubMulAction R M)) => { carrier := ⋂ s ∈ S, ↑s, smul_mem' := ⋯ } }

@[implicit_reducible]

instance SubAddAction.instInfSet {R : Type u} {M : Type v} [VAdd R M] : InfSet (SubAddAction R M)

Equations

• SubAddAction.instInfSet = { sInf := fun (S : Set (SubAddAction R M)) => { carrier := ⋂ s ∈ S, ↑s, vadd_mem' := ⋯ } }

@[implicit_reducible]

instance SubMulAction.instCompleteLattice {R : Type u} {M : Type v} [SMul R M] : CompleteLattice (SubMulAction R M)

Equations

• SubMulAction.instCompleteLattice = Function.Injective.completeLattice SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[implicit_reducible]

instance SubAddAction.instCompleteLattice {R : Type u} {M : Type v} [VAdd R M] : CompleteLattice (SubAddAction R M)

Equations

• SubAddAction.instCompleteLattice = Function.Injective.completeLattice SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem SubMulAction.mem_iSup {R : Type u} {M : Type v} [SMul R M] {ι : Sort u_1} {p : ι → SubMulAction R M} {x : M} : x ∈ ⨆ (i : ι), p i ↔ ∃ (i : ι), x ∈ p i

@[simp]

theorem SubAddAction.mem_iSup {R : Type u} {M : Type v} [VAdd R M] {ι : Sort u_1} {p : ι → SubAddAction R M} {x : M} : x ∈ ⨆ (i : ι), p i ↔ ∃ (i : ι), x ∈ p i

@[simp]

theorem SubMulAction.mem_iInf {R : Type u} {M : Type v} [SMul R M] {ι : Sort u_1} {p : ι → SubMulAction R M} {x : M} : x ∈ ⨅ (i : ι), p i ↔ ∀ (i : ι), x ∈ p i

@[simp]

theorem SubAddAction.mem_iInf {R : Type u} {M : Type v} [VAdd R M] {ι : Sort u_1} {p : ι → SubAddAction R M} {x : M} : x ∈ ⨅ (i : ι), p i ↔ ∀ (i : ι), x ∈ p i

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

theorem SubAddAction.vadd_mem {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) {x : M} (r : R) (h : x ∈ p) : r +ᵥ x ∈ p

@[implicit_reducible]

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, ⋯⟩ }

@[implicit_reducible]

instance SubAddAction.instVAddSubtypeMem {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) : VAdd R ↥p

Equations

• p.instVAddSubtypeMem = { vadd := 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

@[simp]

theorem SubAddAction.val_vadd {R : Type u} {M : Type v} [VAdd R M] {p : SubAddAction 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' := ⋯ }

def SubAddAction.subtype {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) : ↥p →ₑ[id] M

Embedding of a submodule p to the ambient space M.

Equations

• p.subtype = { toFun := Subtype.val, map_vadd' := ⋯ }

@[simp]

theorem SubMulAction.subtype_apply {R : Type u} {M : Type v} [SMul R M] {p : SubMulAction R M} (x : ↥p) : p.subtype x = ↑x

@[simp]

theorem SubAddAction.subtype_apply {R : Type u} {M : Type v} [VAdd R M] {p : SubAddAction R M} (x : ↥p) : p.subtype x = ↑x

theorem SubMulAction.subtype_injective {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) : Function.Injective ⇑p.subtype

theorem SubMulAction.subtype_eq_val {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) : ⇑p.subtype = Subtype.val

theorem SubAddAction.subtype_eq_val {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) : ⇑p.subtype = Subtype.val

@[implicit_reducible, 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

• SubMulAction.SMulMemClass.toMulAction S' = Function.Injective.mulAction Subtype.val ⋯ ⋯

@[implicit_reducible, instance 75]

instance SubAddAction.SMulMemClass.toAddAction {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {A : Type u_1} [SetLike A M] [hA : VAddMemClass A R M] (S' : A) : AddAction R ↥S'

A SubAddAction of an AddAction is an AddAction.

Equations

• SubAddAction.SMulMemClass.toAddAction S' = Function.Injective.addAction Subtype.val ⋯ ⋯

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

• SubMulAction.SMulMemClass.subtype S' = { toFun := Subtype.val, map_smul' := ⋯ }

def SubAddAction.SMulMemClass.subtype {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {A : Type u_1} [SetLike A M] [hA : VAddMemClass A R M] (S' : A) : ↥S' →ₑ[id] M

The natural AddActionHom over R from a SubAddAction of M to M.

Equations

• SubAddAction.SMulMemClass.subtype S' = { toFun := Subtype.val, map_vadd' := ⋯ }

@[simp]

theorem SubMulAction.SMulMemClass.subtype_apply {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 : ↥S') : (SMulMemClass.subtype S') x = ↑x

theorem SubMulAction.SMulMemClass.subtype_injective {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) : Function.Injective ⇑(SMulMemClass.subtype S')

@[simp]

theorem SubMulAction.SMulMemClass.coe_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) : ⇑(SMulMemClass.subtype S') = Subtype.val

@[simp]

theorem SubAddAction.SMulMemClass.coe_subtype {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {A : Type u_1} [SetLike A M] [hA : VAddMemClass A R M] (S' : A) : ⇑(SMulMemClass.subtype S') = Subtype.val

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

theorem SubAddAction.vadd_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) (s : S) {x : M} (h : x ∈ p) : s +ᵥ x ∈ p

@[implicit_reducible]

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, ⋯⟩ }

@[implicit_reducible]

instance SubAddAction.vadd' {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) : VAdd S ↥p

Equations

• p.vadd' = { vadd := 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

instance SubAddAction.vaddAssocClass {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) : VAddAssocClass S R ↥p

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

instance SubAddAction.vaddAssocClass' {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) {S' : Type u_1} [VAdd S' R] [VAdd S' S] [VAdd S' M] [VAddAssocClass S' R M] [VAddAssocClass S' S M] : VAddAssocClass S' S ↥p

@[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 SubAddAction.val_vadd_of_tower {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction 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

@[simp]

theorem SubAddAction.vadd_mem_iff' {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] (p : SubAddAction R M) {G : Type u_1} [AddGroup G] [VAdd G R] [AddAction G M] [VAddAssocClass 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 ↥p

instance SubAddAction.isCentralVAdd {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [VAdd S R] [VAdd S M] [VAddAssocClass S R M] (p : SubAddAction R M) [VAdd Sᵃᵒᵖ R] [VAdd Sᵃᵒᵖ M] [VAddAssocClass Sᵃᵒᵖ R M] [IsCentralVAdd S M] : IsCentralVAdd S ↥p

@[implicit_reducible]

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

• p.mulAction' = { toSMul := p.smul', mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

instance SubAddAction.addAction' {S : Type u'} {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S R] [AddAction S M] [VAddAssocClass S R M] (p : SubAddAction R M) : AddAction S ↥p

Equations

• p.addAction' = { toVAdd := p.vadd', add_vadd := ⋯, zero_vadd := ⋯ }

@[implicit_reducible]

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'

@[implicit_reducible]

instance SubAddAction.addAction {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] (p : SubAddAction R M) : AddAction R ↥p

Equations

• p.addAction = p.addAction'

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 SubAddAction.val_image_orbit {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {p : SubAddAction R M} (m : ↥p) : Subtype.val '' AddAction.orbit R m = AddAction.orbit R ↑m

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 SubAddAction.val_preimage_orbit {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {p : SubAddAction R M} (m : ↥p) : Subtype.val ⁻¹' AddAction.orbit R ↑m = AddAction.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 m : ↥p} : x ∈ MulAction.orbit R m ↔ ↑x ∈ MulAction.orbit R ↑m

theorem SubAddAction.mem_orbit_subAdd_iff {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {p : SubAddAction R M} {x m : ↥p} : x ∈ AddAction.orbit R m ↔ ↑x ∈ AddAction.orbit R ↑m

theorem SubMulAction.stabilizer_of_subMul.submonoid {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {p : SubMulAction R M} (m : ↥p) : MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R ↑m

Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space

theorem SubAddAction.stabilizer_of_subMul.addSubmonoid {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {p : SubAddAction R M} (m : ↥p) : AddAction.stabilizerAddSubmonoid R m = AddAction.stabilizerAddSubmonoid R ↑m

theorem SubMulAction.orbitRel_of_subMul {R : Type u} {M : Type v} [Group R] [MulAction R M] (p : SubMulAction R M) : MulAction.orbitRel R ↥p = Setoid.comap Subtype.val (MulAction.orbitRel R M)

theorem SubAddAction.orbitRel_of_subAdd {R : Type u} {M : Type v} [AddGroup R] [AddAction R M] (p : SubAddAction R M) : AddAction.orbitRel R ↥p = Setoid.comap Subtype.val (AddAction.orbitRel R M)

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

Stabilizers in group SubMulAction coincide with stabilizers in the ambient space

theorem SubAddAction.stabilizer_of_subAdd {R : Type u} {M : Type v} [AddGroup R] [AddAction R M] {p : SubAddAction R M} (m : ↥p) : AddAction.stabilizer R m = AddAction.stabilizer R ↑m

@[implicit_reducible]

instance SubMulAction.instCompl {R : Type u} {M : Type v} [Group R] [MulAction R M] : Compl (SubMulAction R M)

SubMulAction on the complement of an invariant subset

Equations

• SubMulAction.instCompl = { compl := fun (s : SubMulAction R M) => { carrier := (↑s)ᶜ, smul_mem' := ⋯ } }

@[implicit_reducible]

instance SubAddAction.instCompl {R : Type u} {M : Type v} [AddGroup R] [AddAction R M] : Compl (SubAddAction R M)

SubAddAction on the complement of an invariant subset

Equations

• SubAddAction.instCompl = { compl := fun (s : SubAddAction R M) => { carrier := (↑s)ᶜ, vadd_mem' := ⋯ } }

theorem SubMulAction.compl_def {R : Type u} {M : Type v} [Group R] [MulAction R M] (s : SubMulAction R M) : sᶜ.carrier = (↑s)ᶜ

theorem SubAddAction.compl_def {R : Type u} {M : Type v} [AddGroup R] [AddAction R M] (s : SubAddAction R M) : sᶜ.carrier = (↑s)ᶜ

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

@[implicit_reducible]

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

@[implicit_reducible]

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' := ⋯ }

def SubAddAction.inclusion {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction M α) : ↥s →ₑ[id] α

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

Equations

• s.inclusion = { toFun := Subtype.val, map_vadd' := ⋯ }

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 SubAddAction.inclusion.toFun_eq_coe {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction 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 SubAddAction.inclusion.coe_eq {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction 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 SubAddAction.image_inclusion {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction 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

theorem SubAddAction.inclusion_injective {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction M α) : Function.Injective ⇑s.inclusion

def Units.nonZeroSubMul (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] : SubMulAction Rˣ M

The non-zero elements of M are invariant under the action by the units of R.

Equations

• Units.nonZeroSubMul R M = { carrier := {x : M | x ≠ 0}, smul_mem' := ⋯ }

@[implicit_reducible]

instance Units.instMulActionSubtypeNeOfNat (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] : MulAction Rˣ { x : M // x ≠ 0 }

Equations

• Units.instMulActionSubtypeNeOfNat R M = (Units.nonZeroSubMul R M).mulAction'

@[simp]

theorem Units.smul_coe (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (a : Rˣ) (x : { x : M // x ≠ 0 }) : ↑(a • x) = a • ↑x

theorem Units.orbitRel_nonZero_iff (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (x y : { v : M // v ≠ 0 }) : (MulAction.orbitRel Rˣ { v : M // v ≠ 0 }) x y ↔ (MulAction.orbitRel Rˣ M) ↑x ↑y

theorem smul_mem_fixedPoints_of_normal {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {H : Subgroup G} [hH : H.Normal] (g : G) {a : α} (ha : a ∈ MulAction.fixedPoints (↥H) α) : g • a ∈ MulAction.fixedPoints (↥H) α

theorem vadd_mem_fixedPoints_of_normal {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {H : AddSubgroup G} [hH : H.Normal] (g : G) {a : α} (ha : a ∈ AddAction.fixedPoints (↥H) α) : g +ᵥ a ∈ AddAction.fixedPoints (↥H) α

def fixedPointsSubMulOfNormal {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {H : Subgroup G} [hH : H.Normal] : SubMulAction G α

The set of fixed points of a normal subgroup is stable under the group action.

Equations

• fixedPointsSubMulOfNormal = { carrier := MulAction.fixedPoints (↥H) α, smul_mem' := ⋯ }

def fixedPointsSubAddOfNormal {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {H : AddSubgroup G} [hH : H.Normal] : SubAddAction G α

The set of fixed points of a normal subgroup is stable under the group action.

Equations

• fixedPointsSubAddOfNormal = { carrier := AddAction.fixedPoints (↥H) α, vadd_mem' := ⋯ }

@[implicit_reducible]

instance instMulActionElemFixedPointsSubtypeMemSubgroupOfNormal {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {H : Subgroup G} [hH : H.Normal] : MulAction G ↑(MulAction.fixedPoints (↥H) α)

Equations

• instMulActionElemFixedPointsSubtypeMemSubgroupOfNormal = fixedPointsSubMulOfNormal.mulAction'

@[simp]

theorem coe_smul_fixedPoints_of_normal {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {H : Subgroup G} [hH : H.Normal] (g : G) (a : ↑(MulAction.fixedPoints (↥H) α)) : ↑(g • a) = g • ↑a