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 Mathlib/GroupTheory/Submonoid/Pointwise.lean.

Other than section set_acting_on_submodules, most of the lemmas in this file are direct copies of lemmas from Mathlib/GroupTheory/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.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

    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 : 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.pointwiseNeg as an order isomorphism.

      Equations
      Instances For
        theorem Submodule.closure_neg {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (s : Set M) :
        @[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.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 (x x_1 : Submodule R M) => x x_1 }
        Equations
        @[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 =
        Equations
        • Submodule.instCanonicallyOrderedAddCommMonoidSubmodule = let __src := Submodule.pointwiseAddCommMonoid; let __src_1 := Submodule.completeLattice; CanonicallyOrderedAddCommMonoid.mk
        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) :
          (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) :
          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 : 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) :
          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) :
          Equations
          • =
          @[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] :

          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 = let __src := Submodule.pointwiseDistribMulAction; MulActionWithZero.mk
          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 principal, 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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (s : Set S) (N : Submodule R M) (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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (s : Set S) (N : Submodule R M) (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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (s : Set S) (N : Submodule R M) (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_right {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (s : Set S) {p : Submodule R M} {q : Submodule R M} (le : p q) :
              s p s q
              theorem Submodule.set_smul_mono_left {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (N : Submodule R M) {s : Set 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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] {s : Set S} {t : Set S} {p : Submodule R M} {q : Submodule R M} (le_set : s t) (le_submodule : p q) :
              s p t q
              theorem Submodule.set_smul_inductionOn {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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 principal 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 principal, 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 = (Finsupp.sum c fun (r : R) (m : N) => r m)
              @[simp]
              theorem Submodule.empty_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (N : Submodule R M) :
              @[simp]
              theorem Submodule.set_smul_bot {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [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] (N : Submodule R M) [SMulCommClass R R M] (r : R) :
              {r} N = r N
              theorem Submodule.mem_singleton_set_smul {R : Type u_2} {M : Type u_3} [Semiring R] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (N : Submodule R M) [SMulCommClass R S M] (r : S) (x : M) :
              x {r} N ∃ m ∈ N, x = r m

              A subset of a ring R has a multiplicative action on submodules of a module over R.

              Equations
              Instances For
                theorem Submodule.set_smul_eq_iSup {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 M] :
                sR N = ⨆ r ∈ sR, r N

                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] {S : Type u_4} [Monoid S] [AddCommMonoid M] [Module R M] [DistribMulAction S M] (N : Submodule R M) (s : Set S) (t : Set S) :
                  (s t) N = s N t N
                  theorem Submodule.coe_span_smul {R' : Type u_5} {M' : Type u_6} [CommSemiring R'] [AddCommMonoid M'] [Module R' M'] (s : Set R') (N : Submodule R' M') :
                  (Ideal.span s) N = s N