Pointwise instances on Submodules #
This file provides:
and the actions
which matches the action of Set.mulActionSet.
This file also provides:
Submodule.pointwiseSetSMulSubmodule: forR-moduleM, as : Set Rcan act onN : Submodule R Mby definings • Nto be the smallest submodule containing alla • nwherea ∈ sandn ∈ N.
These actions are available in the Pointwise locale.
Implementation notes #
For an R-module M, the action of a subset of R acting on a submodule of M introduced in
section set_acting_on_submodules does not have a counterpart in the files
Mathlib/Algebra/Group/Submonoid/Pointwise.lean and
Mathlib/Algebra/GroupWithZero/Submonoid/Pointwise.lean.
Other than section set_acting_on_submodules, most of the lemmas in this file are direct copies of
lemmas from the file Mathlib/Algebra/Group/Submonoid/Pointwise.lean.
def
Submodule.pointwiseNeg
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommGroup M]
[Module 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.
Equations
- Submodule.pointwiseNeg = { neg := fun (p : Submodule R M) => let __src := -p.toAddSubmonoid; { toAddSubmonoid := __src, smul_mem' := ⋯ } }
Instances For
@[simp]
theorem
Submodule.neg_toAddSubmonoid
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommGroup M]
[Module R M]
(S : Submodule R M)
:
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.
Equations
- Submodule.involutivePointwiseNeg = { toNeg := Submodule.pointwiseNeg, neg_neg := ⋯ }
Instances For
def
Submodule.negOrderIso
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommGroup M]
[Module R M]
:
Submodule.pointwiseNeg as an order isomorphism.
Instances For
@[deprecated Submodule.span_neg_eq_neg (since := "2025-04-08")]
theorem
Submodule.closure_neg
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommGroup M]
[Module R M]
(s : Set M)
:
Alias of Submodule.span_neg_eq_neg.
@[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)
:
instance
Submodule.pointwiseZero
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- Submodule.pointwiseZero = { zero := ⊥ }
instance
Submodule.pointwiseAdd
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- Submodule.pointwiseAdd = { add := fun (x1 x2 : Submodule R M) => x1 ⊔ x2 }
instance
Submodule.pointwiseAddCommMonoid
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
AddCommMonoid (Submodule R M)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Submodule.add_eq_sup
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p q : Submodule R M)
:
@[simp]
theorem
Submodule.zero_eq_bot
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
instance
Submodule.instIsOrderedAddMonoid
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
IsOrderedAddMonoid (Submodule R M)
instance
Submodule.instCanonicallyOrderedAdd
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
@[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)
:
@[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)
:
theorem
Submodule.mem_smul_pointwise_iff_exists
{α : 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)
:
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)
:
instance
Submodule.instCovariantClassHSMulLe
{α : Type u_1}
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Monoid α]
[DistribMulAction α M]
[SMulCommClass α R M]
:
CovariantClass α (Submodule R M) HSMul.hSMul LE.le
@[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 : α)
:
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 T : Submodule R M)
:
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)
:
theorem
Submodule.smul_def
{α : 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)
:
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)
:
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}
[Monoid α]
[SMul α R]
[DistribMulAction α M]
[SMulCommClass α R M]
[IsScalarTower α R M]
(a : α)
(S : Submodule R M)
:
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.
Equations
- Submodule.pointwiseMulActionWithZero = { toMulAction := DistribMulAction.toMulAction, smul_zero := ⋯, zero_smul := ⋯ }
Instances For
Sets acting on Submodules #
Let R be a (semi)ring and M an R-module. Let S be a monoid which acts on M distributively,
then subsets of S can act on submodules of M.
For subset s ⊆ S and submodule N ≤ M, we define s • N to be the smallest submodule containing
all r • n where r ∈ s and n ∈ N.
Results #
For arbitrary monoids S acting distributively on M, there is an induction principle for s • N:
To prove P holds for all s • N, it is enough
to prove:
- for all
r ∈ sandn ∈ N,P (r • n); - for all
randm ∈ s • N,P (r • n); - for all
m₁, m₂,P m₁andP m₂impliesP (m₁ + m₂); P 0.
To invoke this induction principle, use induction x, hx using Submodule.set_smul_inductionOn where
x : M and hx : x ∈ s • N
When we consider subset of R acting on M
Submodule.pointwiseSetDistribMulAction: the action described above is distributive.Submodule.mem_set_smul:x ∈ s • Niffxcan be written asr₀ n₀ + ... + rₖ nₖwhererᵢ ∈ sandnᵢ ∈ N.Submodule.coe_span_smul:s • Nis the same as⟨s⟩ • Nwhere⟨s⟩is the ideal spanned bys.
Notes #
- If we assume the addition on subsets of
Ris the⊔and subtraction⊓i.e. useSetSemiring, then this action actually gives a module structure on submodules ofMover subsets ofR. - If we generalize so that
r • Nmakes sense for allr : S, thenSubmodule.singleton_set_smulandSubmodule.singleton_set_smulcan be generalized as well.
def
Submodule.pointwiseSetSMul
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
:
Let s ⊆ R be a set and N ≤ M be a submodule, then s • N is the smallest submodule containing
all r • n where r ∈ s and n ∈ N.
Equations
Instances For
instance
Submodule.instCovariantClassSetHSMulLe
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
:
CovariantClass (Set S) (Submodule R M) HSMul.hSMul LE.le
theorem
Submodule.set_smul_eq_iSup
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
[SMulCommClass S R M]
(s : Set S)
(N : Submodule R M)
:
theorem
Submodule.set_smul_span
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
[SMulCommClass S R M]
(s : Set S)
(t : Set M)
:
theorem
Submodule.span_set_smul
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
[SMulCommClass S R M]
(s : Set S)
(t : Set M)
:
theorem
Submodule.set_smul_inductionOn
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
{s : Set S}
{N : Submodule R M}
{motive : (x : M) → x ∈ s • N → Prop}
(x : M)
(hx : x ∈ s • N)
(smul₀ : ∀ ⦃r : S⦄ ⦃n : M⦄ (mem₁ : r ∈ s) (mem₂ : n ∈ N), motive (r • n) ⋯)
(smul₁ : ∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N), motive m mem → motive (r • m) ⋯)
(add : ∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N), motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) ⋯)
(zero : motive 0 ⋯)
:
motive x hx
Induction principle for set acting on submodules. To prove P holds for all s • N, it is enough
to prove:
- for all
r ∈ sandn ∈ N,P (r • n); - for all
randm ∈ s • N,P (r • n); - for all
m₁, m₂,P m₁andP m₂impliesP (m₁ + m₂); P 0.
To invoke this induction principle, use induction x, hx using Submodule.set_smul_inductionOn where
x : M and hx : x ∈ s • N
theorem
Submodule.set_smul_eq_map
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(sR : Set R)
(N : Submodule R M)
[SMulCommClass R R ↥N]
:
sR • N = map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribMulAction.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
@[simp]
theorem
Submodule.empty_set_smul
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
(N : Submodule R M)
:
@[simp]
theorem
Submodule.set_smul_bot
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
(s : Set S)
:
theorem
Submodule.singleton_set_smul
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
(N : Submodule R M)
[SMulCommClass S R M]
(r : S)
:
theorem
Submodule.mem_singleton_set_smul
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
(N : Submodule R M)
[SMulCommClass R S M]
(r : S)
(x : M)
:
theorem
Submodule.smul_inductionOn_pointwise
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_4}
[Monoid S]
[DistribMulAction S M]
(N : Submodule R M)
[SMulCommClass S R M]
{a : S}
{p : (x : M) → x ∈ a • N → Prop}
(smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯)
(smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) ⋯)
(add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) ⋯)
(zero : p 0 ⋯)
{x : M}
(hx : x ∈ a • N)
:
p x hx
noncomputable def
Submodule.pointwiseSetMulAction
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[SMulCommClass R R M]
:
A subset of a ring R has a multiplicative action on submodules of a module over R.
Equations
- Submodule.pointwiseSetMulAction = { toSMul := Submodule.pointwiseSetSMul, one_smul := ⋯, mul_smul := ⋯ }
Instances For
noncomputable def
Submodule.pointwiseSetDistribMulAction
{R : Type u_2}
{M : Type u_3}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[SMulCommClass R R M]
:
DistribMulAction (Set R) (Submodule R M)
In a ring, sets acts on submodules.
Equations
- Submodule.pointwiseSetDistribMulAction = { toMulAction := Submodule.pointwiseSetMulAction, smul_zero := ⋯, smul_add := ⋯ }