Mathlib.Algebra.Module.Submodule.Pointwise

Submodule.pointwiseNeg definition

: Neg (Submodule R M)

Full source

/-- 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. -/
protected def pointwiseNeg : Neg (Submodule R M) where
  neg p :=
    { -p.toAddSubmonoid with
      smul_mem' := fun r m hm => Set.mem_neg.2 <| smul_neg r m ▸ p.smul_mem r <| Set.mem_neg.1 hm }

Negation of a submodule

Informal description

The negation operation on submodules of an $R$-module $M$ is defined such that for any submodule $p$, the negated submodule $-p$ consists of all elements $-x$ where $x \in p$. This operation preserves the submodule structure, meaning that if $p$ is closed under scalar multiplication, then $-p$ is also closed under scalar multiplication. Specifically, for any scalar $r \in R$ and element $m \in M$, if $-m \in p$, then $r \bullet (-m) = -(r \bullet m) \in -p$.

Submodule.coe_set_neg theorem

(S : Submodule R M) : ↑(-S) = -(S : Set M)

Full source

@[simp]
theorem coe_set_neg (S : Submodule R M) : ↑(-S) = -(S : Set M) :=
  rfl

Negation of Submodule Equals Negation of Underlying Set

Informal description

For any submodule $S$ of an $R$-module $M$, the underlying set of the negated submodule $-S$ is equal to the negation of the underlying set of $S$, i.e., $-S = \{-x \mid x \in S\}$.

Submodule.neg_toAddSubmonoid theorem

(S : Submodule R M) : (-S).toAddSubmonoid = -S.toAddSubmonoid

Full source

@[simp]
theorem neg_toAddSubmonoid (S : Submodule R M) : (-S).toAddSubmonoid = -S.toAddSubmonoid :=
  rfl

Negation Commutes with Additive Submonoid Construction in Submodules

Informal description

For any submodule $S$ of an $R$-module $M$, the additive submonoid associated with the negated submodule $-S$ is equal to the negation of the additive submonoid associated with $S$.

Submodule.mem_neg theorem

{g : M} {S : Submodule R M} : g ∈ -S ↔ -g ∈ S

Full source

@[simp]
theorem mem_neg {g : M} {S : Submodule R M} : g ∈ -Sg ∈ -S ↔ -g ∈ S :=
  Iff.rfl

Characterization of Membership in Negated Submodule

Informal description

For any element $g$ in an $R$-module $M$ and any submodule $S$ of $M$, the element $g$ belongs to the negated submodule $-S$ if and only if its negation $-g$ belongs to $S$.

Submodule.involutivePointwiseNeg definition

: InvolutiveNeg (Submodule R M)

Full source

/-- `Submodule.pointwiseNeg` is involutive.

This is available as an instance in the `Pointwise` locale. -/
protected def involutivePointwiseNeg : InvolutiveNeg (Submodule R M) where
  neg := Neg.neg
  neg_neg _S := SetLike.coe_injective <| neg_neg _

Involutivity of submodule negation

Informal description

For a module $M$ over a semiring $R$, the negation operation on submodules of $M$ is involutive. That is, for any submodule $S$ of $M$, we have $-(-S) = S$, where $-S$ denotes the submodule consisting of all elements $-x$ for $x \in S$.

Submodule.neg_le_neg theorem

(S T : Submodule R M) : -S ≤ -T ↔ S ≤ T

Full source

@[simp]
theorem neg_le_neg (S T : Submodule R M) : -S ≤ -T ↔ S ≤ T :=
  SetLike.coe_subset_coe.symm.trans Set.neg_subset_neg

Negation Preserves Submodule Inclusion: $-S \leq -T \leftrightarrow S \leq T$

Informal description

For any two submodules $S$ and $T$ of an $R$-module $M$, the negated submodule $-S$ is contained in $-T$ if and only if $S$ is contained in $T$.

Submodule.neg_le theorem

(S T : Submodule R M) : -S ≤ T ↔ S ≤ -T

Full source

theorem neg_le (S T : Submodule R M) : -S ≤ T ↔ S ≤ -T :=
  SetLike.coe_subset_coe.symm.trans Set.neg_subset

Submodule Negation Inclusion: $-S \leq T \leftrightarrow S \leq -T$

Informal description

For any two submodules $S$ and $T$ of an $R$-module $M$, the negated submodule $-S$ is contained in $T$ if and only if $S$ is contained in the negated submodule $-T$.

Submodule.negOrderIso definition

: Submodule R M ≃o Submodule R M

Full source

/-- `Submodule.pointwiseNeg` as an order isomorphism. -/
def negOrderIso : SubmoduleSubmodule R M ≃o Submodule R M where
  toEquiv := Equiv.neg _
  map_rel_iff' := @neg_le_neg _ _ _ _ _

Order isomorphism of submodule negation

Informal description

The order isomorphism `Submodule.negOrderIso` maps a submodule $S$ of an $R$-module $M$ to its negation $-S$, where $-S$ consists of all elements $-x$ for $x \in S$. This map is bijective and preserves the order relation, meaning $S \leq T$ if and only if $-S \leq -T$ for any submodules $S$ and $T$ of $M$.

Submodule.span_neg_eq_neg theorem

(s : Set M) : span R (-s) = -span R s

Full source

theorem span_neg_eq_neg (s : Set M) : span R (-s) = -span R s := by
  apply le_antisymm
  · rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]
    exact subset_span
  · rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]
    exact subset_span

Span of Negated Set Equals Negation of Span

Informal description

For any subset $s$ of an $R$-module $M$, the span of the negated set $-s$ is equal to the negation of the span of $s$, i.e., $$\operatorname{span}_R (-s) = -\operatorname{span}_R s.$$

Submodule.neg_inf theorem

(S T : Submodule R M) : -(S ⊓ T) = -S ⊓ -T

Full source

@[simp]
theorem neg_inf (S T : Submodule R M) : -(S ⊓ T) = -S ⊓ -T := rfl

Negation Preserves Submodule Intersection: $-(S \cap T) = (-S) \cap (-T)$

Informal description

For any two submodules $S$ and $T$ of an $R$-module $M$, the negation of their infimum equals the infimum of their negations, i.e., $-(S \cap T) = (-S) \cap (-T)$.

Submodule.neg_sup theorem

(S T : Submodule R M) : -(S ⊔ T) = -S ⊔ -T

Full source

@[simp]
theorem neg_sup (S T : Submodule R M) : -(S ⊔ T) = -S ⊔ -T :=
  (negOrderIso : SubmoduleSubmodule R M ≃o Submodule R M).map_sup S T

Negation Preserves Submodule Supremum: $-(S \sqcup T) = (-S) \sqcup (-T)$

Informal description

For any two submodules $S$ and $T$ of an $R$-module $M$, the negation of their supremum equals the supremum of their negations, i.e., $-(S \sqcup T) = (-S) \sqcup (-T)$.

Submodule.neg_bot theorem

: -(⊥ : Submodule R M) = ⊥

Full source

@[simp]
theorem neg_bot : -(⊥ : Submodule R M) = ⊥ :=
  SetLike.coe_injective <| (Set.neg_singleton 0).trans <| congr_arg _ neg_zero

Negation of Zero Submodule Equals Itself

Informal description

For any $R$-module $M$, the negation of the bottom submodule $\bot$ (the zero submodule) is equal to $\bot$ itself, i.e., $-0 = 0$.

Submodule.neg_top theorem

: -(⊤ : Submodule R M) = ⊤

Full source

@[simp]
theorem neg_top : -(⊤ : Submodule R M) = ⊤ :=
  SetLike.coe_injective <| Set.neg_univ

Negation of the Top Submodule Equals Itself

Informal description

For any $R$-module $M$, the negation of the top submodule $\top$ (the entire module $M$) is equal to $\top$ itself, i.e., $-M = M$.

Submodule.neg_iInf theorem

{ι : Sort*} (S : ι → Submodule R M) : (-⨅ i, S i) = ⨅ i, -S i

Full source

@[simp]
theorem neg_iInf {ι : Sort*} (S : ι → Submodule R M) : (-⨅ i, S i) = ⨅ i, -S i :=
  (negOrderIso : SubmoduleSubmodule R M ≃o Submodule R M).map_iInf _

Negation Commutes with Infimum of Submodules: $-\bigcap_i S_i = \bigcap_i (-S_i)$

Informal description

Let $R$ be a ring and $M$ an $R$-module. For any family of submodules $(S_i)_{i \in \iota}$ of $M$, the negation of their infimum equals the infimum of their negations, i.e., \[ -\left(\bigcap_{i} S_i\right) = \bigcap_{i} (-S_i). \]

Submodule.neg_iSup theorem

{ι : Sort*} (S : ι → Submodule R M) : (-⨆ i, S i) = ⨆ i, -S i

Full source

@[simp]
theorem neg_iSup {ι : Sort*} (S : ι → Submodule R M) : (-⨆ i, S i) = ⨆ i, -S i :=
  (negOrderIso : SubmoduleSubmodule R M ≃o Submodule R M).map_iSup _

Negation Commutes with Supremum of Submodules: $-\bigsqcup_i S_i = \bigsqcup_i (-S_i)$

Informal description

Let $M$ be a module over a ring $R$ and let $(S_i)_{i \in \iota}$ be a family of submodules of $M$. The negation of the supremum of the family $(S_i)$ equals the supremum of the negations of the submodules, i.e., \[ -\left(\bigsqcup_{i \in \iota} S_i\right) = \bigsqcup_{i \in \iota} (-S_i). \]

Submodule.neg_eq_self theorem

[Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : -p = p

Full source

@[simp]
theorem neg_eq_self [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : -p = p :=
  ext fun _ => p.neg_mem_iff

Negation of Submodule Equals Itself

Informal description

For any submodule $p$ of an $R$-module $M$ over a ring $R$, where $M$ is an additive commutative group, the negation of $p$ is equal to $p$ itself, i.e., $-p = p$.

Submodule.pointwiseZero instance

: Zero (Submodule R M)

Full source

instance pointwiseZero : Zero (Submodule R M) where
  zero := ⊥

Zero Submodule as Zero Element

Informal description

The zero submodule of an $R$-module $M$ is equipped with a zero element.

Submodule.pointwiseAdd instance

: Add (Submodule R M)

Full source

instance pointwiseAdd : Add (Submodule R M) where
  add := (· ⊔ ·)

Addition Operation on Submodules

Informal description

For any ring $R$ and $R$-module $M$, the submodules of $M$ can be equipped with an addition operation where the sum of two submodules $p$ and $q$ is defined as the smallest submodule containing both $p$ and $q$.

Submodule.pointwiseAddCommMonoid instance

: AddCommMonoid (Submodule R M)

Full source

instance pointwiseAddCommMonoid : AddCommMonoid (Submodule R M) where
  add_assoc := sup_assoc
  zero_add := bot_sup_eq
  add_zero := sup_bot_eq
  add_comm := sup_comm
  nsmul := nsmulRec

Additive Commutative Monoid Structure on Submodules

Informal description

For any ring $R$ and $R$-module $M$, the submodules of $M$ form an additive commutative monoid under the addition operation defined by $p + q = \sup(p, q)$ (the smallest submodule containing both $p$ and $q$), with the zero submodule as the additive identity.

Submodule.add_eq_sup theorem

(p q : Submodule R M) : p + q = p ⊔ q

Full source

@[simp]
theorem add_eq_sup (p q : Submodule R M) : p + q = p ⊔ q :=
  rfl

Sum of Submodules Equals Their Supremum

Informal description

For any two submodules $p$ and $q$ of an $R$-module $M$, the sum $p + q$ is equal to their supremum $p \sqcup q$ in the lattice of submodules.

Submodule.zero_eq_bot theorem

: (0 : Submodule R M) = ⊥

Full source

@[simp]
theorem zero_eq_bot : (0 : Submodule R M) = ⊥ :=
  rfl

Zero Submodule Equals Bottom Submodule

Informal description

The zero submodule of an $R$-module $M$ is equal to the bottom submodule (the trivial submodule containing only the zero element), i.e., $0 = \bot$.

Submodule.instIsOrderedAddMonoid instance

: IsOrderedAddMonoid (Submodule R M)

Full source

instance : IsOrderedAddMonoid (Submodule R M) :=
  { add_le_add_left := fun _a _b => sup_le_sup_left }

Submodules Form an Ordered Additive Monoid

Informal description

For any semiring $R$ and $R$-module $M$, the submodules of $M$ form an ordered additive monoid under the addition operation defined by $p + q = \sup(p, q)$ (the smallest submodule containing both $p$ and $q$), with the zero submodule as the additive identity. The order relation is given by inclusion of submodules, and addition is monotone with respect to this order.

Submodule.instCanonicallyOrderedAdd instance

: CanonicallyOrderedAdd (Submodule R M)

Full source

instance : CanonicallyOrderedAdd (Submodule R M) where
  exists_add_of_le := @fun _a b h => ⟨b, (sup_eq_right.2 h).symm⟩
  le_self_add := fun _a _b => le_sup_left

Submodules Form a Canonically Ordered Additive Monoid

Informal description

For any semiring $R$ and $R$-module $M$, the submodules of $M$ form a canonically ordered additive monoid. That is, the order relation $\leq$ on submodules coincides with the subtractibility relation, meaning that for any submodules $N_1, N_2 \subseteq M$, we have $N_1 \leq N_2$ if and only if there exists a submodule $N_3$ such that $N_2 = N_1 + N_3$.

Submodule.pointwiseDistribMulAction definition

: DistribMulAction α (Submodule R M)

Full source

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

This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseDistribMulAction : DistribMulAction α (Submodule R M) where
  smul a S := S.map (DistribMulAction.toLinearMap R M a : M →ₗ[R] M)
  one_smul S :=
    (congr_arg (fun f : Module.End R M => S.map f) (LinearMap.ext <| one_smul α)).trans S.map_id
  mul_smul _a₁ _a₂ S :=
    (congr_arg (fun f : Module.End R M => S.map f) (LinearMap.ext <| mul_smul _ _)).trans
      (S.map_comp _ _)
  smul_zero _a := map_bot _
  smul_add _a _S₁ _S₂ := map_sup _ _ _

Distributive multiplicative action on submodules

Informal description

Given a semiring $R$, an $R$-module $M$, and a monoid $\alpha$ acting distributively on $M$, the structure `Submodule.pointwiseDistribMulAction` defines a distributive multiplicative action of $\alpha$ on the submodules of $M$. For any $a \in \alpha$ and submodule $S \subseteq M$, the action $a \bullet S$ is defined as the image of $S$ under the linear map induced by the scalar multiplication by $a$. This action satisfies: 1. $1 \bullet S = S$ for the identity element $1 \in \alpha$, 2. $(a_1 \cdot a_2) \bullet S = a_1 \bullet (a_2 \bullet S)$ for any $a_1, a_2 \in \alpha$, 3. $a \bullet 0 = 0$ for the zero submodule, 4. $a \bullet (S_1 + S_2) = a \bullet S_1 + a \bullet S_2$ for any submodules $S_1, S_2 \subseteq M$.

Submodule.coe_pointwise_smul theorem

(a : α) (S : Submodule R M) : ↑(a • S) = a • (S : Set M)

Full source

@[simp]
theorem coe_pointwise_smul (a : α) (S : Submodule R M) : ↑(a • S) = a • (S : Set M) :=
  rfl

Equality of Set Images under Scalar Multiplication of Submodules

Informal description

For any scalar $a \in \alpha$ and any submodule $S$ of an $R$-module $M$, the underlying set of the scaled submodule $a \bullet S$ is equal to the pointwise scalar multiplication of $a$ on the set $S$, i.e., $\overline{a \bullet S} = a \bullet \overline{S}$ where $\overline{S}$ denotes the underlying set of $S$.

Submodule.pointwise_smul_toAddSubmonoid theorem

(a : α) (S : Submodule R M) : (a • S).toAddSubmonoid = a • S.toAddSubmonoid

Full source

@[simp]
theorem pointwise_smul_toAddSubmonoid (a : α) (S : Submodule R M) :
    (a • S).toAddSubmonoid = a • S.toAddSubmonoid :=
  rfl

Compatibility of Scalar Multiplication with Additive Submonoid Structure

Informal description

For any element $a$ of a monoid $\alpha$ acting distributively on an $R$-module $M$, and any submodule $S$ of $M$, the additive submonoid associated with the scalar multiple $a \bullet S$ is equal to the scalar multiple $a \bullet (S_{\text{add}})$, where $S_{\text{add}}$ is the additive submonoid associated with $S$.

Submodule.pointwise_smul_toAddSubgroup theorem

 {R M : Type*} [Ring R] [AddCommGroup M] [DistribMulAction α M] [Module R M] [SMulCommClass α R M] (a : α)
  (S : Submodule R M) : (a • S).toAddSubgroup = a • S.toAddSubgroup

Full source

@[simp]
theorem pointwise_smul_toAddSubgroup {R M : Type*} [Ring R] [AddCommGroup M] [DistribMulAction α M]
    [Module R M] [SMulCommClass α R M] (a : α) (S : Submodule R M) :
    (a • S).toAddSubgroup = a • S.toAddSubgroup :=
  rfl

Compatibility of Pointwise Scalar Multiplication with Additive Subgroup Structure

Informal description

Let $R$ be a ring and $M$ an $R$-module with an additive commutative group structure. Given a monoid $\alpha$ acting distributively on $M$ such that the actions of $\alpha$ and $R$ on $M$ commute, then for any $a \in \alpha$ and any submodule $S \subseteq M$, the additive subgroup associated with the pointwise scalar multiplication $a \bullet S$ is equal to the pointwise scalar multiplication of $a$ on the additive subgroup associated with $S$. That is, $(a \bullet S)_{\text{add}} = a \bullet S_{\text{add}}$.

Submodule.mem_smul_pointwise_iff_exists theorem

(m : M) (a : α) (S : Submodule R M) : m ∈ a • S ↔ ∃ b ∈ S, a • b = m

Full source

theorem mem_smul_pointwise_iff_exists (m : M) (a : α) (S : Submodule R M) :
    m ∈ a • Sm ∈ a • S ↔ ∃ b ∈ S, a • b = m :=
  Set.mem_smul_set

Characterization of Membership in Pointwise Scalar Multiplication of Submodules: $m \in a \bullet S$

Informal description

For any element $m$ in an $R$-module $M$, any element $a$ of a monoid $\alpha$ acting distributively on $M$, and any submodule $S$ of $M$, the element $m$ belongs to the pointwise scalar multiplication $a \bullet S$ if and only if there exists an element $b \in S$ such that $a \bullet b = m$.

Submodule.smul_mem_pointwise_smul theorem

(m : M) (a : α) (S : Submodule R M) : m ∈ S → a • m ∈ a • S

Full source

theorem smul_mem_pointwise_smul (m : M) (a : α) (S : Submodule R M) : m ∈ S → a • m ∈ a • S :=
  (Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set M))

Membership Preservation under Pointwise Scalar Multiplication

Informal description

Let $M$ be an $R$-module and $\alpha$ a monoid acting distributively on $M$. For any element $m \in M$, scalar $a \in \alpha$, and submodule $S \subseteq M$, if $m$ belongs to $S$, then the scalar multiple $a \cdot m$ belongs to the pointwise scalar multiplication $a \cdot S$.

Submodule.instCovariantClassHSMulLe instance

: CovariantClass α (Submodule R M) HSMul.hSMul LE.le

Full source

instance : CovariantClass α (Submodule R M) HSMul.hSMul LE.le :=
  ⟨fun _ _ => map_mono⟩

Monotonicity of Scalar Multiplication on Submodules

Informal description

For a semiring $R$, an $R$-module $M$, and a monoid $\alpha$ acting distributively on $M$, the scalar multiplication operation $\bullet$ on submodules of $M$ preserves the inclusion relation. That is, for any $a \in \alpha$ and submodules $S, T \subseteq M$, if $S \subseteq T$, then $a \bullet S \subseteq a \bullet T$.

Submodule.smul_bot' theorem

(a : α) : a • (⊥ : Submodule R M) = ⊥

Full source

/-- See also `Submodule.smul_bot`. -/
@[simp]
theorem smul_bot' (a : α) : a • (⊥ : Submodule R M) = ⊥ :=
  map_bot _

Scalar multiplication preserves the zero submodule

Informal description

For any element $a$ of a monoid $\alpha$ acting distributively on an $R$-module $M$, the scalar multiplication of $a$ with the zero submodule $\bot$ of $M$ is equal to the zero submodule, i.e., $a \bullet \bot = \bot$.

Submodule.smul_sup' theorem

(a : α) (S T : Submodule R M) : a • (S ⊔ T) = a • S ⊔ a • T

Full source

/-- See also `Submodule.smul_sup`. -/
theorem smul_sup' (a : α) (S T : Submodule R M) : a • (S ⊔ T) = a • S ⊔ a • T :=
  map_sup _ _ _

Distributivity of Scalar Multiplication over Submodule Supremum

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a monoid acting distributively on $M$. For any $a \in \alpha$ and submodules $S, T$ of $M$, the scalar multiplication of $a$ on the supremum of $S$ and $T$ equals the supremum of the scalar multiplications of $a$ on $S$ and $T$: \[ a \bullet (S \sqcup T) = (a \bullet S) \sqcup (a \bullet T). \]

Submodule.smul_span theorem

(a : α) (s : Set M) : a • span R s = span R (a • s)

Full source

theorem smul_span (a : α) (s : Set M) : a • span R s = span R (a • s) :=
  map_span _ _

Scalar Multiplication Commutes with Span: $a \bullet \operatorname{span}_R s = \operatorname{span}_R (a \bullet s)$

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a monoid acting distributively on $M$. For any element $a \in \alpha$ and subset $s \subseteq M$, the scalar multiplication of $a$ with the $R$-linear span of $s$ equals the $R$-linear span of the scalar multiplication of $a$ with $s$: \[ a \bullet \operatorname{span}_R s = \operatorname{span}_R (a \bullet s). \]

Submodule.smul_def theorem

(a : α) (S : Submodule R M) : a • S = span R (a • S : Set M)

Full source

lemma smul_def (a : α) (S : Submodule R M) : a • S = span R (a • S : Set M) := by simp [← smul_span]

Definition of Scalar Multiplication on Submodules via Span

Informal description

For a semiring $R$, an $R$-module $M$, a monoid $\alpha$ acting distributively on $M$, and a submodule $S$ of $M$, the scalar multiplication of $a \in \alpha$ on $S$ is equal to the $R$-linear span of the set $\{a \bullet x \mid x \in S\}$. That is, \[ a \bullet S = \operatorname{span}_R \{a \bullet x \mid x \in S\}. \]

Submodule.span_smul theorem

(a : α) (s : Set M) : span R (a • s) = a • span R s

Full source

theorem span_smul (a : α) (s : Set M) : span R (a • s) = a • span R s :=
  Eq.symm (span_image _).symm

Span-Scalar Commutation: $\operatorname{span}_R (a \bullet s) = a \bullet \operatorname{span}_R s$

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a monoid acting distributively on $M$. For any element $a \in \alpha$ and subset $s \subseteq M$, the $R$-linear span of the set $\{a \bullet x \mid x \in s\}$ is equal to the scalar multiplication of $a$ with the $R$-linear span of $s$: \[ \operatorname{span}_R (a \bullet s) = a \bullet \operatorname{span}_R s. \]

Submodule.pointwiseCentralScalar instance

 [DistribMulAction αᵐᵒᵖ M] [SMulCommClass αᵐᵒᵖ R M] [IsCentralScalar α M] : IsCentralScalar α (Submodule R M)

Full source

instance pointwiseCentralScalar [DistribMulAction αᵐᵒᵖ M] [SMulCommClass αᵐᵒᵖ R M]
    [IsCentralScalar α M] : IsCentralScalar α (Submodule R M) :=
  ⟨fun _a S => (congr_arg fun f : Module.End R M => S.map f) <| LinearMap.ext <| op_smul_eq_smul _⟩

Central Scalar Action on Submodules via Pointwise Multiplication

Informal description

For a semiring $R$, an $R$-module $M$, and a monoid $\alpha$ acting distributively on $M$ such that the actions of $\alpha$ and its multiplicative opposite $\alpha^\text{op}$ commute with the $R$-action, if the scalar multiplication by $\alpha$ on $M$ is central (i.e., the left and right actions coincide), then the induced pointwise scalar multiplication by $\alpha$ on the submodules of $M$ is also central.

Submodule.smul_le_self_of_tower theorem

 {α : Type*} [Monoid α] [SMul α R] [DistribMulAction α M] [SMulCommClass α R M] [IsScalarTower α R M] (a : α)
  (S : Submodule R M) : a • S ≤ S

Full source

@[simp]
theorem smul_le_self_of_tower {α : Type*} [Monoid α] [SMul α R] [DistribMulAction α M]
    [SMulCommClass α R M] [IsScalarTower α R M] (a : α) (S : Submodule R M) : a • S ≤ S := by
  rintro y ⟨x, hx, rfl⟩
  exact smul_of_tower_mem _ a hx

Submodule stability under compatible monoid actions: $a \bullet S \subseteq S$

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $\alpha$ a monoid acting on $R$ and $M$ such that: 1. The action of $\alpha$ on $M$ is distributive 2. The scalar multiplications by $\alpha$ and $R$ on $M$ commute 3. $\alpha$ acts on $M$ through $R$ (i.e., the action forms a scalar tower) Then for any $a \in \alpha$ and any submodule $S \subseteq M$, we have $a \bullet S \subseteq S$.

Submodule.pointwiseMulActionWithZero definition

: MulActionWithZero α (Submodule R M)

Full source

/-- 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`. -/
protected def pointwiseMulActionWithZero : MulActionWithZero α (Submodule R M) :=
  { Submodule.pointwiseDistribMulAction with
    zero_smul := fun S =>
      (congr_arg (fun f : M →ₗ[R] M => S.map f) (LinearMap.ext <| zero_smul α)).trans S.map_zero }

Multiplicative action with zero on submodules

Informal description

Given a semiring $R$, an $R$-module $M$, and a monoid $\alpha$ with zero acting distributively on $M$, the structure `Submodule.pointwiseMulActionWithZero` defines a multiplicative action with zero of $\alpha$ on the submodules of $M$. This action satisfies: 1. $0 \bullet S = 0$ for any submodule $S \subseteq M$, 2. $(a_1 \cdot a_2) \bullet S = a_1 \bullet (a_2 \bullet S)$ for any $a_1, a_2 \in \alpha$, 3. $1 \bullet S = S$ for the identity element $1 \in \alpha$.

Submodule.pointwiseSetSMul definition

: SMul (Set S) (Submodule R M)

Full source

/--
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`.
-/
protected def pointwiseSetSMul : SMul (Set S) (Submodule R M) where
  smul s N := sInf { p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p }

Action of a subset of a monoid on a submodule

Informal description

Given a semiring $ R $, an $ R $-module $ M $, and a monoid $ S $ acting distributively on $ M $, for any subset $ s \subseteq S $ and any submodule $ N \leq M $, the action $ s \bullet N $ is defined as the smallest submodule of $ M $ containing all elements of the form $ r \bullet n $ where $ r \in s $ and $ n \in N $.

Submodule.mem_set_smul_def theorem

 (x : M) : x ∈ s • N ↔ x ∈ sInf {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p}

Full source

lemma mem_set_smul_def (x : M) :
    x ∈ s • Nx ∈ s • N ↔
  x ∈ sInf { p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p } := Iff.rfl

Characterization of Membership in Pointwise Submodule Action

Informal description

For an element $x$ in an $R$-module $M$, $x$ belongs to the submodule $s \bullet N$ (where $s$ is a subset of a monoid $S$ acting on $M$ and $N$ is a submodule of $M$) if and only if $x$ belongs to the infimum of all submodules $p$ of $M$ that contain all elements of the form $r \bullet n$ for $r \in s$ and $n \in N$.

Submodule.mem_set_smul_of_mem_mem theorem

{r : S} {m : M} (mem1 : r ∈ s) (mem2 : m ∈ N) : r • m ∈ s • N

Full source

@[aesop safe]
lemma mem_set_smul_of_mem_mem {r : S} {m : M} (mem1 : r ∈ s) (mem2 : m ∈ N) :
    r • m ∈ s • N := by
  rw [mem_set_smul_def, mem_sInf]
  exact fun _ h => h mem1 mem2

Scalar multiple of elements from $s$ and $N$ lies in $s \bullet N$

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$. For any subset $s \subseteq S$ and any submodule $N \subseteq M$, if $r \in s$ and $m \in N$, then the scalar multiple $r \bullet m$ belongs to the submodule $s \bullet N$.

Submodule.set_smul_le theorem

 (p : Submodule R M) (closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) : s • N ≤ p

Full source

lemma set_smul_le (p : Submodule R M)
    (closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) :
    s • N ≤ p :=
  sInf_le closed_under_smul

Containment of Pointwise Submodule Action under Closure Condition

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$. For any subset $s \subseteq S$ and any submodule $N \leq M$, if a submodule $p \leq M$ satisfies that for all $r \in s$ and $n \in N$ we have $r \bullet n \in p$, then the submodule $s \bullet N$ is contained in $p$.

Submodule.set_smul_le_iff theorem

(p : Submodule R M) : s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p

Full source

lemma set_smul_le_iff (p : Submodule R M) :
    s • N ≤ p ↔
    ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p := by
  fconstructor
  · intro h r n hr hn
    exact h <| mem_set_smul_of_mem_mem hr hn
  · apply set_smul_le

Characterization of Submodule Containment under Pointwise Action

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$. For any subset $s \subseteq S$, any submodule $N \subseteq M$, and any submodule $p \subseteq M$, the following are equivalent: 1. The submodule $s \bullet N$ is contained in $p$. 2. For all $r \in s$ and $n \in N$, the scalar multiple $r \bullet n$ belongs to $p$.

Submodule.set_smul_eq_of_le theorem

 (p : Submodule R M) (closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p) (le : p ≤ s • N) : s • N = p

Full source

lemma set_smul_eq_of_le (p : Submodule R M)
    (closed_under_smul : ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p)
    (le : p ≤ s • N) :
    s • N = p :=
  le_antisymm (set_smul_le s N p closed_under_smul) le

Characterization of Pointwise Submodule Action via Closure and Containment

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$. For any subset $s \subseteq S$ and any submodule $N \leq M$, if a submodule $p \leq M$ satisfies: 1. For all $r \in s$ and $n \in N$, we have $r \bullet n \in p$; 2. $p$ is contained in $s \bullet N$; then $s \bullet N = p$.

Submodule.instCovariantClassSetHSMulLe instance

: CovariantClass (Set S) (Submodule R M) HSMul.hSMul LE.le

Full source

instance : CovariantClass (Set S) (Submodule R M) HSMul.hSMul LE.le :=
  ⟨fun _ _ _ le => set_smul_le _ _ _ fun _ _ hr hm => mem_set_smul_of_mem_mem (mem1 := hr)
    (mem2 := le hm)⟩

Monotonicity of Submodule Action under Subset Inclusion

Informal description

For a semiring $R$, an $R$-module $M$, and a monoid $S$ acting distributively on $M$, the action of subsets of $S$ on submodules of $M$ is order-preserving. That is, for any subsets $s, t \subseteq S$ and submodules $N, P \subseteq M$, if $s \subseteq t$ and $N \subseteq P$, then $s \bullet N \subseteq t \bullet P$.

Submodule.set_smul_mono_left theorem

{s t : Set S} (le : s ≤ t) : s • N ≤ t • N

Full source

lemma set_smul_mono_left {s t : Set S} (le : s ≤ t) :
    s • N ≤ t • N :=
  set_smul_le _ _ _ fun _ _ hr hm => mem_set_smul_of_mem_mem (mem1 := le hr)
    (mem2 := hm)

Monotonicity of Submodule Action with Respect to Subset Inclusion

Informal description

For any subsets $s$ and $t$ of a monoid $S$ acting distributively on an $R$-module $M$, if $s \subseteq t$, then the submodule $s \bullet N$ is contained in the submodule $t \bullet N$ for any submodule $N$ of $M$.

Submodule.set_smul_le_of_le_le theorem

{s t : Set S} {p q : Submodule R M} (le_set : s ≤ t) (le_submodule : p ≤ q) : s • p ≤ t • q

Full source

lemma set_smul_le_of_le_le {s t : Set S} {p q : Submodule R M}
    (le_set : s ≤ t) (le_submodule : p ≤ q) : s • p ≤ t • q :=
  le_trans (set_smul_mono_left _ le_set) <| smul_mono_right _ le_submodule

Monotonicity of Submodule Action with Respect to Subset and Submodule Inclusion

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$. For any subsets $s, t \subseteq S$ and submodules $p, q \subseteq M$, if $s \subseteq t$ and $p \subseteq q$, then the submodule $s \bullet p$ is contained in the submodule $t \bullet q$.

Submodule.set_smul_eq_iSup theorem

[SMulCommClass S R M] (s : Set S) (N : Submodule R M) : s • N = ⨆ (a ∈ s), a • N

Full source

lemma set_smul_eq_iSup [SMulCommClass S R M] (s : Set S) (N : Submodule R M) :
    s • N = ⨆ (a ∈ s), a • N := by
  refine Eq.trans (congrArg sInf ?_) csInf_Ici
  simp_rw [← Set.Ici_def, iSup_le_iff, @forall_comm M]
  exact Set.ext fun _ => forall₂_congr (fun _ _ => Iff.symm map_le_iff_le_comap)

Decomposition of Submodule Action as Supremum of Elementwise Actions

Informal description

Let $S$ be a monoid acting distributively on an $R$-module $M$, with the actions of $S$ and $R$ on $M$ commuting (i.e., $[SMulCommClass S R M]$). For any subset $s \subseteq S$ and any submodule $N \subseteq M$, the action of $s$ on $N$ is equal to the supremum of the actions of individual elements of $s$ on $N$: $$ s \bullet N = \bigsqcup_{a \in s} (a \bullet N). $$

Submodule.set_smul_span theorem

[SMulCommClass S R M] (s : Set S) (t : Set M) : s • span R t = span R (s • t)

Full source

theorem set_smul_span [SMulCommClass S R M] (s : Set S) (t : Set M) :
    s • span R t = span R (s • t) := by
  simp_rw [set_smul_eq_iSup, smul_span, iSup_span, Set.iUnion_smul_set]

Action of a Set on a Span Equals Span of the Action: $s \bullet \operatorname{span}_R t = \operatorname{span}_R (s \bullet t)$

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$ such that the actions of $S$ and $R$ on $M$ commute (i.e., $[SMulCommClass S R M]$). For any subset $s \subseteq S$ and any subset $t \subseteq M$, the action of $s$ on the $R$-linear span of $t$ equals the $R$-linear span of the action of $s$ on $t$: $$ s \bullet \operatorname{span}_R t = \operatorname{span}_R (s \bullet t). $$

Submodule.span_set_smul theorem

[SMulCommClass S R M] (s : Set S) (t : Set M) : span R (s • t) = s • span R t

Full source

theorem span_set_smul [SMulCommClass S R M] (s : Set S) (t : Set M) :
    span R (s • t) = s • span R t := (set_smul_span s t).symm

Span of Set Action Equals Action of Span: $\operatorname{span}_R (s \bullet t) = s \bullet \operatorname{span}_R t$

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$ such that the actions of $S$ and $R$ on $M$ commute (i.e., $[SMulCommClass\, S\, R\, M]$). For any subset $s \subseteq S$ and any subset $t \subseteq M$, the $R$-linear span of the action of $s$ on $t$ equals the action of $s$ on the $R$-linear span of $t$: $$ \operatorname{span}_R (s \bullet t) = s \bullet \operatorname{span}_R t. $$

Submodule.set_smul_inductionOn theorem

 {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) (mem_set_smul_of_mem_mem mem₁ mem₂))
  (smul₁ : ∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N), motive m mem → motive (r • m) (Submodule.smul_mem _ r mem))
    --
  (add :
    ∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N),
      motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) (Submodule.add_mem _ mem₁ mem₂))
  (zero : motive 0 (Submodule.zero_mem _)) : motive x hx

Full source

/--
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`
-/
@[elab_as_elim]
lemma set_smul_inductionOn {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) (mem_set_smul_of_mem_mem mem₁ mem₂))
    (smul₁ : ∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N) ,
      motive m mem → motive (r • m) (Submodule.smul_mem _ r mem)) --
    (add : ∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N),
      motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) (Submodule.add_mem _ mem₁ mem₂))
    (zero : motive 0 (Submodule.zero_mem _)) :
    motive x hx :=
  let ⟨_, h⟩ := set_smul_le s N
    { carrier := { m | ∃ (mem : m ∈ s • N), motive m mem },
      zero_mem' := ⟨Submodule.zero_mem _, zero⟩
      add_mem' := fun ⟨mem, h⟩ ⟨mem', h'⟩ ↦ ⟨_, add mem mem' h h'⟩
      smul_mem' := fun r _ ⟨mem, h⟩ ↦ ⟨_, smul₁ r mem h⟩ }
    (fun _ _ mem mem' ↦ ⟨mem_set_smul_of_mem_mem mem mem', smul₀ mem mem'⟩) hx
  h

Induction Principle for Submodule Action by a Set

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$. For a subset $s \subseteq S$ and a submodule $N \subseteq M$, to prove a property $P(x)$ holds for all $x \in s \bullet N$, it suffices to show: 1. For all $r \in s$ and $n \in N$, $P(r \bullet n)$ holds; 2. For all $r \in R$ and $m \in s \bullet N$, if $P(m)$ holds then $P(r \bullet m)$ holds; 3. For all $m_1, m_2 \in s \bullet N$, if $P(m_1)$ and $P(m_2)$ hold then $P(m_1 + m_2)$ holds; 4. $P(0)$ holds.

Submodule.set_smul_eq_map theorem

 [SMulCommClass R R N] :
  sR • N =
    Submodule.map (N.subtype.comp (Finsupp.lsum R <| DistribMulAction.toLinearMap _ _)) (Finsupp.supported N R sR)

Full source

lemma set_smul_eq_map [SMulCommClass R R N] :
    sR • N =
    Submodule.map
      (N.subtype.comp (Finsupp.lsum R <| DistribMulAction.toLinearMap _ _))
      (Finsupp.supported N R sR) := by
  classical
  apply set_smul_eq_of_le
  · intro r n hr hn
    exact ⟨Finsupp.single r ⟨n, hn⟩, Finsupp.single_mem_supported _ _ hr, by simp⟩
  · intro x hx
    obtain ⟨c, hc, rfl⟩ := hx
    simp only [LinearMap.coe_comp, coe_subtype, Finsupp.coe_lsum, Finsupp.sum, Function.comp_apply]
    rw [AddSubmonoid.coe_finset_sum]
    refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩
    · rintro r hr
      rw [mem_set_smul_def, Submodule.mem_sInf]
      rintro p hp
      exact hp (hc hr) (c r).2
    · ext x : 1
      simp only [Set.mem_iInter, SetLike.mem_coe]
      fconstructor
      · refine fun h ↦ h fun r n hr hn ↦ ?_
        rw [mem_set_smul_def, mem_sInf]
        exact fun p hp ↦ hp hr hn
      · aesop

Characterization of Submodule Action via Finitely Supported Functions

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $N$ a submodule of $M$. Suppose that the scalar multiplications by $R$ on $N$ commute (i.e., $[SMulCommClass R R N]$ holds). Then for any subset $s_R \subseteq R$, the submodule $s_R \bullet N$ is equal to the image of the finitely supported functions $R \to_{\text{f}} N$ with support contained in $s_R$ under the composition of the inclusion map $N \hookrightarrow M$ with the linear sum map induced by the scalar multiplication action.

Submodule.mem_set_smul theorem

 (x : M) [SMulCommClass R R N] : x ∈ sR • N ↔ ∃ (c : R →₀ N), (c.support : Set R) ⊆ sR ∧ x = c.sum fun r m ↦ r • m

Full source

lemma mem_set_smul (x : M) [SMulCommClass R R N] :
    x ∈ sR • Nx ∈ sR • N ↔ ∃ (c : R →₀ N), (c.support : Set R) ⊆ sR ∧ x = c.sum fun r m ↦ r • m := by
  fconstructor
  · intros h
    rw [set_smul_eq_map] at h
    obtain ⟨c, hc, rfl⟩ := h
    exact ⟨c, hc, rfl⟩
  · rw [mem_set_smul_def, Submodule.mem_sInf]
    rintro ⟨c, hc1, rfl⟩ p hp
    rw [Finsupp.sum, AddSubmonoid.coe_finset_sum]
    exact Submodule.sum_mem _ fun r hr ↦ hp (hc1 hr) (c _).2

Characterization of Elements in Submodule Action via Finitely Supported Functions

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $N$ a submodule of $M$ such that the scalar multiplications by $R$ on $N$ commute. For any subset $s_R \subseteq R$ and any element $x \in M$, $x$ belongs to the submodule $s_R \bullet N$ if and only if there exists a finitely supported function $c \colon R \to_{\text{f}} N$ with support contained in $s_R$ such that $x = \sum_{r \in \operatorname{supp}(c)} r \bullet c(r)$.

Submodule.empty_set_smul theorem

: (∅ : Set S) • N = ⊥

Full source

@[simp] lemma empty_set_smul : (∅ : Set S) • N = ⊥ := by
  ext
  fconstructor
  · intro hx
    rw [mem_set_smul_def, Submodule.mem_sInf] at hx
    exact hx ⊥ (fun r _ hr ↦ hr.elim)
  · rintro rfl; exact Submodule.zero_mem _

Action of Empty Set on Submodule Yields Zero Submodule

Informal description

For any submodule $N$ of an $R$-module $M$, the action of the empty set $\emptyset$ on $N$ yields the trivial submodule $\{0\}$, i.e., $\emptyset \bullet N = 0$.

Submodule.set_smul_bot theorem

: s • (⊥ : Submodule R M) = ⊥

Full source

@[simp] lemma set_smul_bot : s • (⊥ : Submodule R M) = ⊥ :=
  eq_bot_iff.mpr fun x hx ↦ by induction x, hx using set_smul_inductionOn <;> aesop

Action of a Set on the Zero Submodule Yields Zero Submodule

Informal description

For any subset $s$ of a monoid $S$ acting distributively on an $R$-module $M$, the action of $s$ on the trivial submodule $\{0\}$ of $M$ yields the trivial submodule $\{0\}$, i.e., $s \bullet \{0\} = \{0\}$.

Submodule.singleton_set_smul theorem

[SMulCommClass S R M] (r : S) : ({ r } : Set S) • N = r • N

Full source

lemma singleton_set_smul [SMulCommClass S R M] (r : S) : ({r} : Set S) • N = r • N := by
  apply set_smul_eq_of_le
  · rintro _ m rfl hm; exact ⟨m, hm, rfl⟩
  · rintro _ ⟨m, hm, rfl⟩
    rw [mem_set_smul_def, Submodule.mem_sInf]
    intro _ hp; exact hp rfl hm

Singleton Set Action Equals Element Action on Submodules

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$ such that the scalar multiplications by $R$ and $S$ commute. For any element $r \in S$ and submodule $N \leq M$, the action of the singleton set $\{r\}$ on $N$ equals the action of $r$ on $N$, i.e., $\{r\} \bullet N = r \bullet N$.

Submodule.mem_singleton_set_smul theorem

[SMulCommClass R S M] (r : S) (x : M) : x ∈ ({ r } : Set S) • N ↔ ∃ (m : M), m ∈ N ∧ x = r • m

Full source

lemma mem_singleton_set_smul [SMulCommClass R S M] (r : S) (x : M) :
    x ∈ ({r} : Set S) • Nx ∈ ({r} : Set S) • N ↔ ∃ (m : M), m ∈ N ∧ x = r • m := by
  fconstructor
  · intro hx
    induction x, hx using Submodule.set_smul_inductionOn with
    | smul₀ => aesop
    | @smul₁ t n mem h =>
      rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop,  smul_comm _ _ _⟩
    | add mem₁ mem₂ h₁ h₂ =>
      rcases h₁ with ⟨m₁, h₁, rfl⟩
      rcases h₂ with ⟨m₂, h₂, rfl⟩
      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
    | zero => exact ⟨0, Submodule.zero_mem _, by simp⟩
  · aesop

Characterization of Elements in Singleton Set Action on Submodule

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$ such that the scalar multiplications by $R$ and $S$ commute. For any element $r \in S$, any element $x \in M$, and any submodule $N \subseteq M$, we have that $x$ belongs to the submodule $\{r\} \bullet N$ if and only if there exists an element $m \in N$ such that $x = r \bullet m$.

Submodule.smul_inductionOn_pointwise theorem

 [SMulCommClass S R M] {a : S} {p : (x : M) → x ∈ a • N → Prop}
  (smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) (Submodule.smul_mem_pointwise_smul _ _ _ hs))
  (smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) (Submodule.smul_mem _ _ mem))
  (add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N), p x hx → p y hy → p (x + y) (Submodule.add_mem _ hx hy))
  (zero : p 0 (Submodule.zero_mem _)) {x : M} (hx : x ∈ a • N) : p x hx

Full source

lemma smul_inductionOn_pointwise [SMulCommClass S R M] {a : S} {p : (x : M) → x ∈ a • N → Prop}
    (smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) (Submodule.smul_mem_pointwise_smul _ _ _ hs))
    (smul₁ : ∀ (r : R) (m : M) (mem : m ∈ a • N), p m mem → p (r • m) (Submodule.smul_mem _ _ mem))
    (add : ∀ (x y : M) (hx : x ∈ a • N) (hy : y ∈ a • N),
      p x hx → p y hy → p (x + y) (Submodule.add_mem _ hx hy))
    (zero : p 0 (Submodule.zero_mem _)) {x : M} (hx : x ∈ a • N) :
    p x hx := by
  simp_all only [← Submodule.singleton_set_smul]
  let p' (x : M) (hx : x ∈ ({a} : Set S) • N) : Prop :=
    p x (by rwa [← Submodule.singleton_set_smul])
  refine Submodule.set_smul_inductionOn (motive := p') _ (N.singleton_set_smul a ▸ hx)
      (fun r n hr hn ↦ ?_) smul₁ add zero
  · simp only [Set.mem_singleton_iff] at hr
    subst hr
    exact smul₀ n hn

Induction Principle for Pointwise Scalar Multiplication of Submodules

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$ such that the scalar multiplications by $R$ and $S$ commute. For any element $a \in S$, submodule $N \subseteq M$, and property $p$, to prove $p(x)$ holds for all $x \in a \bullet N$, it suffices to show: 1. For all $s \in N$, $p(a \bullet s)$ holds; 2. For all $r \in R$ and $m \in a \bullet N$, if $p(m)$ holds then $p(r \bullet m)$ holds; 3. For all $x, y \in a \bullet N$, if $p(x)$ and $p(y)$ hold then $p(x + y)$ holds; 4. $p(0)$ holds.

Submodule.pointwiseSetMulAction definition

[SMulCommClass R R M] : MulAction (Set R) (Submodule R M)

Full source

/-- A subset of a ring `R` has a multiplicative action on submodules of a module over `R`. -/
protected def pointwiseSetMulAction [SMulCommClass R R M] :
    MulAction (Set R) (Submodule R M) where
  one_smul x := show {(1 : R)} • x = x from SetLike.ext fun m =>
    (mem_singleton_set_smul _ _ _).trans ⟨by rintro ⟨_, h, rfl⟩; rwa [one_smul],
      fun h => ⟨m, h, (one_smul _ _).symm⟩⟩
  mul_smul s t x := le_antisymm
    (set_smul_le _ _ _ <| by rintro _ _ ⟨_, _, _, _, rfl⟩ _; rw [mul_smul]; aesop)
    (set_smul_le _ _ _ fun r m hr hm ↦ by
      have : SMulCommClass R R x := ⟨fun r s m => Subtype.ext <| smul_comm _ _ _⟩
      obtain ⟨c, hc1, rfl⟩ := mem_set_smul _ _ _ |>.mp hm
      rw [Finsupp.sum, AddSubmonoid.coe_finset_sum]
      simp only [SetLike.val_smul, Finset.smul_sum, smul_smul]
      exact Submodule.sum_mem _ fun r' hr' ↦
        mem_set_smul_of_mem_mem (Set.mul_mem_mul hr (hc1 hr')) (c _).2)

Multiplicative action of subsets on submodules

Informal description

Given a semiring $ R $ and an $ R $-module $ M $, the type `Set R` of subsets of $ R $ acts on the type `Submodule R M` of submodules of $ M $ via scalar multiplication. This action satisfies the axioms of a multiplicative action: 1. The multiplicative identity acts as identity: $ \{1\} \bullet N = N $ for any submodule $ N $. 2. The action is compatible with multiplication of subsets: $ (s \cdot t) \bullet N = s \bullet (t \bullet N) $ for any subsets $ s, t \subseteq R $ and submodule $ N $. Here, $ s \bullet N $ is defined as the smallest submodule containing all elements $ r \bullet n $ where $ r \in s $ and $ n \in N $.

Submodule.pointwiseSetDistribMulAction definition

[SMulCommClass R R M] : DistribMulAction (Set R) (Submodule R M)

Full source

/-- In a ring, sets acts on submodules. -/
protected def pointwiseSetDistribMulAction [SMulCommClass R R M] :
    DistribMulAction (Set R) (Submodule R M) where
  smul_zero s := set_smul_bot s
  smul_add s x y := le_antisymm
    (set_smul_le _ _ _ <| by
      rintro r m hr hm
      rw [add_eq_sup, Submodule.mem_sup] at hm
      obtain ⟨a, ha, b, hb, rfl⟩ := hm
      rw [smul_add, add_eq_sup, Submodule.mem_sup]
      exact ⟨r • a, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := ha),
        r • b, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := hb), rfl⟩)
    (sup_le_iff.mpr ⟨smul_mono_right _ le_sup_left, smul_mono_right _ le_sup_right⟩)

Distributive action of subsets on submodules

Informal description

Given a semiring $ R $ and an $ R $-module $ M $, the type `Set R` of subsets of $ R $ acts distributively on the type `Submodule R M` of submodules of $ M $. This action satisfies the following properties: 1. Scalar multiplication by a subset preserves the zero submodule: $ s \bullet 0 = 0 $ for any subset $ s \subseteq R $. 2. Scalar multiplication by a subset distributes over the sum of submodules: $ s \bullet (N_1 + N_2) = s \bullet N_1 + s \bullet N_2 $ for any subset $ s \subseteq R $ and submodules $ N_1, N_2 $. Here, $ s \bullet N $ is defined as the smallest submodule containing all elements $ r \bullet n $ where $ r \in s $ and $ n \in N $.

Submodule.sup_set_smul theorem

(s t : Set S) : (s ⊔ t) • N = s • N ⊔ t • N

Full source

lemma sup_set_smul (s t : Set S) :
    (s ⊔ t) • N = s • N ⊔ t • N :=
  set_smul_eq_of_le _ _ _
    (by rintro _ _ (hr|hr) hn
        · exact Submodule.mem_sup_left (mem_set_smul_of_mem_mem hr hn)
        · exact Submodule.mem_sup_right (mem_set_smul_of_mem_mem hr hn))
    (sup_le (set_smul_mono_left _ le_sup_left) (set_smul_mono_left _ le_sup_right))

Union Action on Submodule Equals Supremum of Individual Actions

Informal description

Let $R$ be a semiring, $M$ an $R$-module, and $S$ a monoid acting distributively on $M$. For any subsets $s, t \subseteq S$ and any submodule $N \subseteq M$, the action of the union $s \cup t$ on $N$ equals the supremum of the actions of $s$ and $t$ on $N$, i.e., $$(s \cup t) \bullet N = (s \bullet N) \sqcup (t \bullet N).$$

Mathlib.Algebra.Module.Submodule.Pointwise

Implementation notes

Results

Notes