Documentation

Mathlib.Algebra.Module.Submodule.Pointwise

Pointwise instances on Submodules #

This file provides:

and the actions

which matches the action of Set.mulActionSet.

This file also provides:

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
    Instances For
      @[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) :
      @[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

      Submodule.pointwiseNeg is involutive.

      This is available as an instance in the Pointwise locale.

      Equations
        Instances For
          @[simp]
          theorem Submodule.neg_le_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S 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 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.pointwiseNeg as an order isomorphism.

          Equations
            Instances For
              theorem Submodule.span_neg_eq_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (s : Set M) :
              span R (-s) = -span R s
              @[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) :
              span R (-s) = -span R s

              Alias of Submodule.span_neg_eq_neg.

              @[simp]
              theorem Submodule.neg_inf {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) :
              -(ST) = -S-T
              @[simp]
              theorem Submodule.neg_sup {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) :
              -(ST) = -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.pointwiseZero {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
              Equations
                instance Submodule.pointwiseAdd {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
                Equations
                  Equations
                    @[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) :
                    p + q = pq
                    @[simp]
                    theorem Submodule.zero_eq_bot {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
                    0 =
                    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] :

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

                    This is available as an instance in the Pointwise locale.

                    Equations
                      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) :
                        ↑(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) :
                        @[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) :
                        m a S bS, a b = 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) :
                        m Sa 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 : α) :

                        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) :
                        a (ST) = a Sa 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 span R s = span R (a s)
                        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) :
                        a S = 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) :
                        span R (a s) = a span R s
                        @[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) :
                        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] :

                        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
                          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:

                            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

                            Notes #

                            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] :
                            SMul (Set S) (Submodule R 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
                                theorem Submodule.mem_set_smul_def {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) (x : M) :
                                x s N x sInf {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r sn Nr n p}
                                theorem Submodule.mem_set_smul_of_mem_mem {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} {r : S} {m : M} (mem1 : r s) (mem2 : m N) :
                                r m s N
                                theorem Submodule.set_smul_le {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 p : Submodule R M) (closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r sn Nr n p) :
                                s N p
                                theorem Submodule.set_smul_le_iff {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 p : Submodule R M) :
                                s N p ∀ ⦃r : S⦄ ⦃n : M⦄, r sn Nr n p
                                theorem Submodule.set_smul_eq_of_le {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 p : Submodule R M) (closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r sn Nr n p) (le : p s N) :
                                s N = p
                                theorem Submodule.set_smul_mono_left {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) {s t : Set S} (le : s t) :
                                s N t N
                                theorem Submodule.set_smul_le_of_le_le {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 t : Set S} {p q : Submodule R M} (le_set : s t) (le_submodule : p q) :
                                s p t q
                                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) :
                                s N = as, a N
                                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) :
                                s span R t = span R (s t)
                                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) :
                                span R (s t) = s span R t
                                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 NProp} (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 memmotive (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 ∈ s and n ∈ N, P (r • n);
                                • for all r and m ∈ s • N, P (r • n);
                                • for all m₁, m₂, P m₁ and P m₂ implies P (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] :
                                theorem Submodule.mem_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (sR : Set R) (N : Submodule R M) (x : M) [SMulCommClass R R N] :
                                x sR N ∃ (c : R →₀ N), c.support sR x = (c.sum fun (r : R) (m : N) => r m)
                                @[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) :
                                {r} N = r N
                                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) :
                                x {r} N mN, x = r 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 NProp} (smul₀ : ∀ (s : M) (hs : s N), p (a s) ) (smul₁ : ∀ (r : R) (m : M) (mem : m a N), p m memp (r m) ) (add : ∀ (x y : M) (hx : x a N) (hy : y a N), p x hxp y hyp (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
                                  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] :

                                    In a ring, sets acts on submodules.

                                    Equations
                                      Instances For
                                        theorem Submodule.sup_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) (s t : Set S) :
                                        (st) N = s Nt N