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.

Tags

submodule, mul_action

ink

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

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

  smul_mem : ∀ {s : S} (r : R) {m : M}, m ∈ s → r • 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.

ink

class VAddMemClass (S : Type u_1) (R : outParam (Type u_2)) (M : Type u_3) [inst : VAdd R M] [inst : SetLike S M] : Type

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

  vadd_mem : ∀ {s : S} (r : R) {m : M}, m ∈ s → r +ᵥ 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.

ink

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

• SetLike.vadd s = { vadd := fun r x => { val := r +ᵥ ↑x, property := (_ : r +ᵥ ↑x ∈ s) } }

ink

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

• (_ : r +ᵥ ↑x ∈ s) = (_ : r +ᵥ ↑x ∈ s)

ink

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

• SetLike.smul s = { smul := fun r x => { val := r • ↑x, property := (_ : r • ↑x ∈ s) } }

ink

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

ink

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

ink

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

ink

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

ink

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) }

ink

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) }

ink

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

ink

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

• The underlying set of a SubMulAction.

  carrier : Set M

• The carrier set is closed under scalar multiplication.

  smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier

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

ink

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

Equations

• SubMulAction.instSetLikeSubMulAction = { coe := SubMulAction.carrier, coe_injective' := (_ : ∀ (p q : SubMulAction R M), p.carrier = q.carrier → p = q) }

ink

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

Equations

• SubMulAction.instSMulMemClassSubMulActionInstSetLikeSubMulAction = { smul_mem := (_ : ∀ {s : SubMulAction R M} (c : R) {x : M}, x ∈ s.carrier → c • x ∈ s.carrier) }

ink

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

ink

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

ink

def SubMulAction.copy {R : Type u} {M : Type v} [inst : 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

• SubMulAction.copy p s hs = { carrier := s, smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ s → c • x ∈ s) }

ink

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

ink

theorem SubMulAction.copy_eq {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 = p

ink

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

Equations

• SubMulAction.instBotSubMulAction = { bot := { carrier := ∅, smul_mem' := (_ : R → ∀ (h : M), ¬h ∈ ∅) } }

ink

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

Equations

• SubMulAction.instInhabitedSubMulAction = { default := ⊥ }

ink

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

ink

instance SubMulAction.instSMulSubtypeMemSubMulActionInstMembershipInstSetLikeSubMulAction {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) : SMul R { x // x ∈ p }

Equations

• SubMulAction.instSMulSubtypeMemSubMulActionInstMembershipInstSetLikeSubMulAction p = { smul := fun c x => { val := c • ↑x, property := (_ : c • ↑x ∈ p) } }

ink

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

ink

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

• SubMulAction.subtype p = { toFun := Subtype.val, map_smul' := (_ : ∀ (a : R) (a_1 : { x // x ∈ p }), a • ↑a_1 = a • ↑a_1) }

ink

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

ink

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

ink

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

• SubMulAction.SMulMemClass.toMulAction S' = Function.Injective.mulAction Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ∀ (r : R) (x : { x // x ∈ S' }), ↑(r • x) = r • ↑x)

ink

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

• SubMulAction.SMulMemClass.subtype S' = { toFun := Subtype.val, map_smul' := (_ : ∀ (x : R) (x_1 : { x // x ∈ S' }), ↑(x • x_1) = ↑(x • x_1)) }

ink

@[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) : ↑(SubMulAction.SMulMemClass.subtype S') = Subtype.val

ink

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

ink

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

• SubMulAction.smul' p = { smul := fun c x => { val := c • ↑x, property := (_ : c • ↑x ∈ p) } }

ink

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

• @SubMulAction.isScalarTower = @SubMulAction.isScalarTower.proof_1

ink

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

• @SubMulAction.isScalarTower' = @SubMulAction.isScalarTower'.proof_1

ink

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

ink

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

ink

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

• @SubMulAction.isCentralScalar = @SubMulAction.isCentralScalar.proof_1

ink

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

• SubMulAction.mulAction' p = MulAction.mk (_ : ∀ (x : { x // x ∈ p }), 1 • x = x) (_ : ∀ (c₁ c₂ : S) (x : { x // x ∈ p }), (c₁ * c₂) • x = c₁ • c₂ • x)

ink

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

• SubMulAction.mulAction p = SubMulAction.mulAction' p

ink

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.

ink

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 }) : MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R ↑m

Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space

ink

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 }) : MulAction.stabilizer R m = MulAction.stabilizer R ↑m

Stabilizers in group SubMulAction coincide with stabilizers in the ambient space

ink

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

ink

instance SubMulAction.instZeroSubtypeMemSubMulActionToSMulToZeroToAddMonoidToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroInstMembershipInstSetLikeSubMulAction {R : Type u} {M : Type v} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : SubMulAction R M) [n_empty : Nonempty { x // x ∈ p }] : Zero { x // x ∈ 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.

ink

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

ink

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

ink

instance SubMulAction.instNegSubtypeMemSubMulActionToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassToZeroToMonoidWithZeroToSemiringToSMulWithZeroToMulActionWithZeroToAddCommMonoidInstMembershipInstSetLikeSubMulAction {R : Type u} {M : Type v} [inst : Ring R] [inst : AddCommGroup M] [inst : Module R M] (p : SubMulAction R M) : Neg { x // x ∈ p }

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

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