Pointwise instances on Submodules

This file provides:

• Submodule.pointwiseNeg

and the actions

• Submodule.pointwiseDistribMulAction
• Submodule.pointwiseMulActionWithZero

which matches the action of Set.mulActionSet.

These actions are available in the Pointwise locale.

Implementation notes

Most of the lemmas in this file are direct copies of lemmas from GroupTheory/Submonoid/Pointwise.lean.

def Submodule.pointwiseNeg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] : Neg (Submodule R M)

The submodule with every element negated. Note if R is a ring and not just a semiring, this is a no-op, as shown by Submodule.neg_eq_self.

Recall that When R is the semiring corresponding to the nonnegative elements of R', Submodule R' M is the type of cones of M. This instance reflects such cones about 0.

This is available as an instance in the Pointwise locale.

@[simp]

theorem Submodule.coe_set_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S : Submodule R M) : ↑(-S) = -↑S

@[simp]

theorem Submodule.neg_toAddSubmonoid {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S : Submodule R M) : (-S).toAddSubmonoid = -S.toAddSubmonoid

@[simp]

theorem Submodule.mem_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] {g : M} {S : Submodule R M} : g ∈ -S ↔ -g ∈ S

def Submodule.involutivePointwiseNeg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] : InvolutiveNeg (Submodule R M)

Submodule.pointwiseNeg is involutive.

This is available as an instance in the Pointwise locale.

@[simp]

theorem Submodule.neg_le_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) : -S ≤ -T ↔ S ≤ T

theorem Submodule.neg_le {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) : -S ≤ T ↔ S ≤ -T

def Submodule.negOrderIso {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] : Submodule R M ≃o Submodule R M

Submodule.pointwiseNeg as an order isomorphism.

theorem Submodule.closure_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (s : Set M) : Submodule.span R (-s) = -Submodule.span R s

@[simp]

theorem Submodule.neg_inf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) : -(S ⊓ T) = -S ⊓ -T

@[simp]

theorem Submodule.neg_sup {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) : -(S ⊔ T) = -S ⊔ -T

@[simp]

theorem Submodule.neg_bot {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] : -⊥ = ⊥

@[simp]

theorem Submodule.neg_top {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] : -⊤ = ⊤

@[simp]

theorem Submodule.neg_iInf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] {ι : Sort u_4} (S : ι → Submodule R M) : -⨅ (i : ι), S i = ⨅ (i : ι), -S i

@[simp]

theorem Submodule.neg_iSup {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] {ι : Sort u_4} (S : ι → Submodule R M) : -⨆ (i : ι), S i = ⨆ (i : ι), -S i

@[simp]

theorem Submodule.neg_eq_self {R : Type u_2} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : -p = p

instance Submodule.pointwiseAddCommMonoid {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : AddCommMonoid (Submodule R M)

@[simp]

theorem Submodule.add_eq_sup {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R M) : p + q = p ⊔ q

@[simp]

theorem Submodule.zero_eq_bot {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : 0 = ⊥

instance Submodule.instCanonicallyOrderedAddMonoidSubmodule {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : CanonicallyOrderedAddMonoid (Submodule R M)

def Submodule.pointwiseDistribMulAction {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] : DistribMulAction α (Submodule R M)

The action on a submodule corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

@[simp]

theorem Submodule.coe_pointwise_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (S : Submodule R M) : ↑(a • S) = a • ↑S

@[simp]

theorem Submodule.pointwise_smul_toAddSubmonoid {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (S : Submodule R M) : (a • S).toAddSubmonoid = a • S.toAddSubmonoid

@[simp]

theorem Submodule.pointwise_smul_toAddSubgroup {α : Type u_1} [Monoid α] {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [DistribMulAction α M] [Module R M] [SMulCommClass α R M] (a : α) (S : Submodule R M) : Submodule.toAddSubgroup (a • S) = a • Submodule.toAddSubgroup S

theorem Submodule.smul_mem_pointwise_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (m : M) (a : α) (S : Submodule R M) : m ∈ S → a • m ∈ a • S

@[simp]

theorem Submodule.smul_bot' {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) : a • ⊥ = ⊥

See also Submodule.smul_bot.

theorem Submodule.smul_sup' {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (S : Submodule R M) (T : Submodule R M) : a • (S ⊔ T) = a • S ⊔ a • T

See also Submodule.smul_sup.

theorem Submodule.smul_span {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (s : Set M) : a • Submodule.span R s = Submodule.span R (a • s)

theorem Submodule.span_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] (a : α) (s : Set M) : Submodule.span R (a • s) = a • Submodule.span R s

instance Submodule.pointwiseCentralScalar {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] [DistribMulAction αᵐᵒᵖ M] [SMulCommClass αᵐᵒᵖ R M] [IsCentralScalar α M] : IsCentralScalar α (Submodule R M)

@[simp]

theorem Submodule.smul_le_self_of_tower {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Semiring α] [Module α R] [Module α M] [SMulCommClass α R M] [IsScalarTower α R M] (a : α) (S : Submodule R M) : a • S ≤ S

def Submodule.pointwiseMulActionWithZero {α : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring α] [Module α M] [SMulCommClass α R M] : MulActionWithZero α (Submodule R M)

The action on a submodule corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

This is a stronger version of Submodule.pointwiseDistribMulAction. Note that add_smul does not hold so this cannot be stated as a Module.