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

structure 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} : Membership.mem s m → Membership.mem s (HSMul.hSMul r m)

  Multiplication by a scalar on an element of the set remains in the set.

structure 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} : Membership.mem s m → Membership.mem s (HVAdd.hVAdd r m)

  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 Nat 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 Int M

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

def 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 (Subtype fun (x : M) => Membership.mem s x)

A subset closed under the scalar action inherits that action.

Equations

• Eq (SetLike.smul s) { smul := fun (r : R) (x : Subtype fun (x : M) => Membership.mem s x) => ⟨HSMul.hSMul r x.val, ⋯⟩ }

def 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 (Subtype fun (x : M) => Membership.mem s x)

A subset closed under the additive action inherits that action.

Equations

• Eq (SetLike.vadd s) { vadd := fun (r : R) (x : Subtype fun (x : M) => Membership.mem s x) => ⟨HVAdd.hVAdd r x.val, ⋯⟩ }

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 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 (Subtype fun (x : M) => Membership.mem s x) (Subtype fun (x : M) => Membership.mem s x)

theorem 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 (Subtype fun (x : M) => Membership.mem s x) (Subtype fun (x : M) => Membership.mem s x)

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 : Subtype fun (x : M) => Membership.mem s x) : Eq (HSMul.hSMul r x).val (HSMul.hSMul r x.val)

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 : Subtype fun (x : M) => Membership.mem s x) : Eq (HVAdd.hVAdd r x).val (HVAdd.hVAdd r x.val)

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 : Membership.mem s x) : Eq (HSMul.hSMul r ⟨x, hx⟩) ⟨HSMul.hSMul r x, ⋯⟩

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 : Membership.mem s x) : Eq (HVAdd.hVAdd r ⟨x, hx⟩) ⟨HVAdd.hVAdd 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 : Subtype fun (x : M) => Membership.mem s x) : Eq (HSMul.hSMul r x) ⟨HSMul.hSMul r x.val, ⋯⟩

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 : Subtype fun (x : M) => Membership.mem s x) : Eq (HVAdd.hVAdd r x) ⟨HVAdd.hVAdd r x.val, ⋯⟩

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} : Iff (∀ (a : R), Membership.mem N (HSMul.hSMul a x)) (Membership.mem N x)

def 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 (Subtype fun (x : α) => Membership.mem s x)

A subset closed under the scalar action inherits that action.

Equations

• Eq (SetLike.smul' s) { smul := fun (r : M) (x : Subtype fun (x : α) => Membership.mem s x) => ⟨HSMul.hSMul r x.val, ⋯⟩ }

def 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 (Subtype fun (x : α) => Membership.mem s x)

A subset closed under the additive action inherits that action.

Equations

• Eq (SetLike.vadd' s) { vadd := fun (r : M) (x : Subtype fun (x : α) => Membership.mem s x) => ⟨HVAdd.hVAdd r x.val, ⋯⟩ }

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 : Subtype fun (x : α) => Membership.mem s x) : Eq (HSMul.hSMul r x).val (HSMul.hSMul r x.val)

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 : Subtype fun (x : α) => Membership.mem s x) : Eq (HVAdd.hVAdd r x).val (HVAdd.hVAdd r x.val)

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 : Membership.mem s x) : Eq (HSMul.hSMul r ⟨x, hx⟩) ⟨HSMul.hSMul r x, ⋯⟩

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 : Membership.mem s x) : Eq (HVAdd.hVAdd r ⟨x, hx⟩) ⟨HVAdd.hVAdd 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 : Subtype fun (x : α) => Membership.mem s x) : Eq (HSMul.hSMul r x) ⟨HSMul.hSMul r x.val, ⋯⟩

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 : Subtype fun (x : α) => Membership.mem s x) : Eq (HVAdd.hVAdd r x) ⟨HVAdd.hVAdd r x.val, ⋯⟩

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} : Membership.mem self.carrier x → Membership.mem self.carrier (HVAdd.hVAdd c x)

  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} : Membership.mem self.carrier x → Membership.mem self.carrier (HSMul.hSMul c x)

  The carrier set is closed under scalar multiplication.

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

Equations

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

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

Equations

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

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

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

theorem SubMulAction.mem_carrier {R : Type u} {M : Type v} [SMul R M] {p : SubMulAction R M} {x : M} : Iff (Membership.mem p.carrier x) (Membership.mem (SetLike.coe p) x)

theorem SubAddAction.mem_carrier {R : Type u} {M : Type v} [VAdd R M] {p : SubAddAction R M} {x : M} : Iff (Membership.mem p.carrier x) (Membership.mem (SetLike.coe p) x)

theorem SubMulAction.ext {R : Type u} {M : Type v} [SMul R M] {p q : SubMulAction R M} (h : ∀ (x : M), Iff (Membership.mem p x) (Membership.mem q x)) : Eq p q

theorem SubAddAction.ext {R : Type u} {M : Type v} [VAdd R M] {p q : SubAddAction R M} (h : ∀ (x : M), Iff (Membership.mem p x) (Membership.mem q x)) : Eq p q

theorem SubMulAction.ext_iff {R : Type u} {M : Type v} [SMul R M] {p q : SubMulAction R M} : Iff (Eq p q) (∀ (x : M), Iff (Membership.mem p x) (Membership.mem q x))

theorem SubAddAction.ext_iff {R : Type u} {M : Type v} [VAdd R M] {p q : SubAddAction R M} : Iff (Eq p q) (∀ (x : M), Iff (Membership.mem p x) (Membership.mem q x))

def SubMulAction.copy {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) (s : Set M) (hs : Eq s (SetLike.coe 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

• Eq (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 : Eq s (SetLike.coe 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

• Eq (p.copy s hs) { carrier := s, vadd_mem' := ⋯ }

theorem SubMulAction.coe_copy {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) (s : Set M) (hs : Eq s (SetLike.coe p)) : Eq (SetLike.coe (p.copy s hs)) s

theorem SubAddAction.coe_copy {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) (s : Set M) (hs : Eq s (SetLike.coe p)) : Eq (SetLike.coe (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 : Eq s (SetLike.coe p)) : Eq (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 : Eq s (SetLike.coe p)) : Eq (p.copy s hs) p

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

Equations

• Eq SubMulAction.instBot { bot := { carrier := EmptyCollection.emptyCollection, smul_mem' := ⋯ } }

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

Equations

• Eq SubAddAction.instBot { bot := { carrier := EmptyCollection.emptyCollection, vadd_mem' := ⋯ } }

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

Equations

• Eq SubMulAction.instInhabited { default := Bot.bot }

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

Equations

• Eq SubAddAction.instInhabited { default := Bot.bot }

theorem SubMulAction.smul_mem {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) {x : M} (r : R) (h : Membership.mem p x) : Membership.mem p (HSMul.hSMul r x)

theorem SubAddAction.vadd_mem {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) {x : M} (r : R) (h : Membership.mem p x) : Membership.mem p (HVAdd.hVAdd r x)

def SubMulAction.instSMulSubtypeMem {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) : SMul R (Subtype fun (x : M) => Membership.mem p x)

Equations

• Eq p.instSMulSubtypeMem { smul := fun (c : R) (x : Subtype fun (x : M) => Membership.mem p x) => ⟨HSMul.hSMul c x.val, ⋯⟩ }

def SubAddAction.instVAddSubtypeMem {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) : VAdd R (Subtype fun (x : M) => Membership.mem p x)

Equations

• Eq p.instVAddSubtypeMem { vadd := fun (c : R) (x : Subtype fun (x : M) => Membership.mem p x) => ⟨HVAdd.hVAdd c x.val, ⋯⟩ }

theorem SubMulAction.val_smul {R : Type u} {M : Type v} [SMul R M] {p : SubMulAction R M} (r : R) (x : Subtype fun (x : M) => Membership.mem p x) : Eq (HSMul.hSMul r x).val (HSMul.hSMul r x.val)

theorem SubAddAction.val_vadd {R : Type u} {M : Type v} [VAdd R M] {p : SubAddAction R M} (r : R) (x : Subtype fun (x : M) => Membership.mem p x) : Eq (HVAdd.hVAdd r x).val (HVAdd.hVAdd r x.val)

def SubMulAction.subtype {R : Type u} {M : Type v} [SMul R M] (p : SubMulAction R M) : MulActionHom id (Subtype fun (x : M) => Membership.mem p x) M

Embedding of a submodule p to the ambient space M.

Equations

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

def SubAddAction.subtype {R : Type u} {M : Type v} [VAdd R M] (p : SubAddAction R M) : AddActionHom id (Subtype fun (x : M) => Membership.mem p x) M

Embedding of a submodule p to the ambient space M.

Equations

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

theorem SubMulAction.subtype_apply {R : Type u} {M : Type v} [SMul R M] {p : SubMulAction R M} (x : Subtype fun (x : M) => Membership.mem p x) : Eq (DFunLike.coe p.subtype x) x.val

theorem SubAddAction.subtype_apply {R : Type u} {M : Type v} [VAdd R M] {p : SubAddAction R M} (x : Subtype fun (x : M) => Membership.mem p x) : Eq (DFunLike.coe p.subtype x) x.val

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

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

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

def 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 (Subtype fun (x : M) => Membership.mem S' x)

A SubMulAction of a MulAction is a MulAction.

Equations

• Eq (SubMulAction.SMulMemClass.toMulAction S') (Function.Injective.mulAction Subtype.val ⋯ ⋯)

def 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 (Subtype fun (x : M) => Membership.mem S' x)

A SubAddAction of an AddAction is an AddAction.

Equations

• Eq (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) : MulActionHom id (Subtype fun (x : M) => Membership.mem S' x) M

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

Equations

• Eq (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) : AddActionHom id (Subtype fun (x : M) => Membership.mem S' x) M

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

Equations

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

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 : Subtype fun (x : M) => Membership.mem S' x) : Eq (DFunLike.coe (SMulMemClass.subtype S') x) x.val

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 (DFunLike.coe (SMulMemClass.subtype S'))

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) : Eq (DFunLike.coe (SMulMemClass.subtype S')) Subtype.val

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) : Eq (DFunLike.coe (SMulMemClass.subtype S')) Subtype.val

@[deprecated SubMulAction.SMulMemClass.coe_subtype (since := "2025-02-18")]

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) : Eq (DFunLike.coe (SMulMemClass.subtype S')) Subtype.val

Alias of SubMulAction.SMulMemClass.coe_subtype.

@[deprecated SubAddAction.SMulMemClass.coe_subtype (since := "2025-02-18")]

theorem SubAddAction.SMulMemClass.coeSubtype {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) : Eq (DFunLike.coe (SMulMemClass.subtype S')) Subtype.val

Alias of SubAddAction.SMulMemClass.coe_subtype.

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 : Membership.mem p x) : Membership.mem p (HSMul.hSMul s x)

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 : Membership.mem p x) : Membership.mem p (HVAdd.hVAdd s x)

def 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 (Subtype fun (x : M) => Membership.mem p x)

Equations

• Eq p.smul' { smul := fun (c : S) (x : Subtype fun (x : M) => Membership.mem p x) => ⟨HSMul.hSMul c x.val, ⋯⟩ }

def 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 (Subtype fun (x : M) => Membership.mem p x)

Equations

• Eq p.vadd' { vadd := fun (c : S) (x : Subtype fun (x : M) => Membership.mem p x) => ⟨HVAdd.hVAdd c x.val, ⋯⟩ }

theorem 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 (Subtype fun (x : M) => Membership.mem p x)

theorem SubAddAction.isScalarTower {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 (Subtype fun (x : M) => Membership.mem p x)

theorem 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 (Subtype fun (x : M) => Membership.mem p x)

theorem SubAddAction.isScalarTower' {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 (Subtype fun (x : M) => Membership.mem p x)

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 : Subtype fun (x : M) => Membership.mem p x) : Eq (HSMul.hSMul s x).val (HSMul.hSMul s x.val)

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 : Subtype fun (x : M) => Membership.mem p x) : Eq (HVAdd.hVAdd s x).val (HVAdd.hVAdd s x.val)

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} : Iff (Membership.mem p (HSMul.hSMul g x)) (Membership.mem p x)

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} : Iff (Membership.mem p (HVAdd.hVAdd g x)) (Membership.mem p x)

theorem 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 (MulOpposite S) R] [SMul (MulOpposite S) M] [IsScalarTower (MulOpposite S) R M] [IsCentralScalar S M] : IsCentralScalar S (Subtype fun (x : M) => Membership.mem p x)

theorem 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 (AddOpposite S) R] [VAdd (AddOpposite S) M] [VAddAssocClass (AddOpposite S) R M] [IsCentralVAdd S M] : IsCentralVAdd S (Subtype fun (x : M) => Membership.mem p x)

def 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 (Subtype fun (x : M) => Membership.mem p x)

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

Equations

• Eq p.mulAction' { smul := fun (x1 : S) (x2 : Subtype fun (x : M) => Membership.mem p x) => HSMul.hSMul x1 x2, one_smul := ⋯, mul_smul := ⋯ }

def 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 (Subtype fun (x : M) => Membership.mem p x)

Equations

• Eq p.addAction' { vadd := fun (x1 : S) (x2 : Subtype fun (x : M) => Membership.mem p x) => HVAdd.hVAdd x1 x2, zero_vadd := ⋯, add_vadd := ⋯ }

def SubMulAction.mulAction {R : Type u} {M : Type v} [Monoid R] [MulAction R M] (p : SubMulAction R M) : MulAction R (Subtype fun (x : M) => Membership.mem p x)

Equations

• Eq p.mulAction p.mulAction'

def SubAddAction.addAction {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] (p : SubAddAction R M) : AddAction R (Subtype fun (x : M) => Membership.mem p x)

Equations

• Eq 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 : Subtype fun (x : M) => Membership.mem p x) : Eq (Set.image Subtype.val (MulAction.orbit R m)) (MulAction.orbit R m.val)

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 : Subtype fun (x : M) => Membership.mem p x) : Eq (Set.image Subtype.val (AddAction.orbit R m)) (AddAction.orbit R m.val)

theorem SubMulAction.val_preimage_orbit {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {p : SubMulAction R M} (m : Subtype fun (x : M) => Membership.mem p x) : Eq (Set.preimage Subtype.val (MulAction.orbit R m.val)) (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 : Subtype fun (x : M) => Membership.mem p x) : Eq (Set.preimage Subtype.val (AddAction.orbit R m.val)) (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 : Subtype fun (x : M) => Membership.mem p x} : Iff (Membership.mem (MulAction.orbit R m) x) (Membership.mem (MulAction.orbit R m.val) x.val)

theorem SubAddAction.mem_orbit_subAdd_iff {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {p : SubAddAction R M} {x m : Subtype fun (x : M) => Membership.mem p x} : Iff (Membership.mem (AddAction.orbit R m) x) (Membership.mem (AddAction.orbit R m.val) x.val)

theorem SubMulAction.stabilizer_of_subMul.submonoid {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {p : SubMulAction R M} (m : Subtype fun (x : M) => Membership.mem p x) : Eq (MulAction.stabilizerSubmonoid R m) (MulAction.stabilizerSubmonoid R m.val)

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 : Subtype fun (x : M) => Membership.mem p x) : Eq (AddAction.stabilizerAddSubmonoid R m) (AddAction.stabilizerAddSubmonoid R m.val)

theorem SubMulAction.orbitRel_of_subMul {R : Type u} {M : Type v} [Group R] [MulAction R M] (p : SubMulAction R M) : Eq (MulAction.orbitRel R (Subtype fun (x : M) => Membership.mem p x)) (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) : Eq (AddAction.orbitRel R (Subtype fun (x : M) => Membership.mem p x)) (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 : Subtype fun (x : M) => Membership.mem p x) : Eq (MulAction.stabilizer R m) (MulAction.stabilizer R m.val)

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 : Subtype fun (x : M) => Membership.mem p x) : Eq (AddAction.stabilizer R m) (AddAction.stabilizer R m.val)

theorem SubMulAction.zero_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : SubMulAction R M) (h : (SetLike.coe p).Nonempty) : Membership.mem p 0

def SubMulAction.instZeroSubtypeMemOfNonempty {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : SubMulAction R M) [n_empty : Nonempty (Subtype fun (x : M) => Membership.mem p x)] : Zero (Subtype fun (x : M) => Membership.mem p x)

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

Equations

• Eq 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 : Membership.mem p x) : Membership.mem p (Neg.neg x)

theorem SubMulAction.neg_mem_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) {x : M} : Iff (Membership.mem p (Neg.neg x)) (Membership.mem p x)

def SubMulAction.instNegSubtypeMem {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) : Neg (Subtype fun (x : M) => Membership.mem p x)

Equations

• Eq p.instNegSubtypeMem { neg := fun (x : Subtype fun (x : M) => Membership.mem p x) => ⟨Neg.neg x.val, ⋯⟩ }

theorem SubMulAction.val_neg {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] (p : SubMulAction R M) (x : Subtype fun (x : M) => Membership.mem p x) : Eq (Neg.neg x).val (Neg.neg x.val)

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 : Ne s 0) : Iff (Membership.mem p (HSMul.hSMul s x)) (Membership.mem p x)

def SubMulAction.inclusion {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) : MulActionHom id (Subtype fun (x : α) => Membership.mem s x) α

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

Equations

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

def SubAddAction.inclusion {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction M α) : AddActionHom id (Subtype fun (x : α) => Membership.mem s x) α

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

Equations

• Eq 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 α) : Eq 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 α) : Eq s.inclusion.toFun Subtype.val

theorem SubMulAction.inclusion.coe_eq {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) : Eq (DFunLike.coe s.inclusion) Subtype.val

theorem SubAddAction.inclusion.coe_eq {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction M α) : Eq (DFunLike.coe s.inclusion) Subtype.val

theorem SubMulAction.image_inclusion {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) : Eq (Set.range (DFunLike.coe s.inclusion)) s.carrier

theorem SubAddAction.image_inclusion {M : Type u_1} {α : Type u_2} [AddMonoid M] [AddAction M α] (s : SubAddAction M α) : Eq (Set.range (DFunLike.coe s.inclusion)) s.carrier

theorem SubMulAction.inclusion_injective {M : Type u_1} {α : Type u_2} [Monoid M] [MulAction M α] (s : SubMulAction M α) : Function.Injective (DFunLike.coe s.inclusion)

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

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

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

Equations

• Eq (Units.nonZeroSubMul R M) { carrier := setOf fun (x : M) => Ne x 0, smul_mem' := ⋯ }

def Units.instMulActionSubtypeNeOfNat (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] : MulAction (Units R) (Subtype fun (x : M) => Ne x 0)

Equations

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

theorem Units.smul_coe (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (a : Units R) (x : Subtype fun (x : M) => Ne x 0) : Eq (HSMul.hSMul a x).val (HSMul.hSMul a x.val)

theorem Units.orbitRel_nonZero_iff (R : Type u_1) (M : Type u_2) [Monoid R] [AddCommMonoid M] [DistribMulAction R M] (x y : Subtype fun (v : M) => Ne v 0) : Iff (Setoid.r x y) (Setoid.r x.val y.val)