Mathlib.Algebra.Module.Submodule.Defs

Submodule structure

(R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v
    extends AddSubmonoid M, SubMulAction R M

Full source

/-- A submodule of a module is one which is closed under vector operations.
  This is a sufficient condition for the subset of vectors in the submodule
  to themselves form a module. -/
structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v
    extends AddSubmonoid M, SubMulAction R M

Submodule of a module

Informal description

A submodule of a module $M$ over a semiring $R$ is a subset of $M$ that contains the zero vector and is closed under addition and scalar multiplication. Specifically, for a submodule $S \subseteq M$: 1. $0 \in S$ 2. For any $x, y \in S$, $x + y \in S$ 3. For any $r \in R$ and $x \in S$, $r \bullet x \in S$ This structure ensures that $S$ itself forms a module over $R$ with the inherited operations.

Submodule.setLike instance

: SetLike (Submodule R M) M

Full source

instance setLike : SetLike (Submodule R M) M where
  coe s := s.carrier
  coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h

Submodules as Set-like Structures

Informal description

For any semiring $R$ and module $M$ over $R$, the type of submodules of $M$ has a `SetLike` structure, meaning that submodules can be treated as sets of elements of $M$ with an injective coercion.

Submodule.carrier_eq_coe theorem

(s : Submodule R M) : s.carrier = s

Full source

@[simp] lemma carrier_eq_coe (s : Submodule R M) : s.carrier = s := rfl

Submodule Carrier Equals Submodule as Set

Informal description

For any submodule $s$ of a module $M$ over a semiring $R$, the carrier set of $s$ is equal to $s$ itself when viewed as a subset of $M$.

Submodule.ofClass definition

 {S R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M]
  (s : S) : Submodule R M

Full source

/-- The actual `Submodule` obtained from an element of a `SMulMemClass` and `AddSubmonoidClass`. -/
@[simps]
def ofClass {S R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M]
    [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) : Submodule R M where
  carrier := s
  add_mem' := add_mem
  zero_mem' := zero_mem _
  smul_mem' := SMulMemClass.smul_mem

Submodule construction from additive and multiplicative closure properties

Informal description

Given a subset $s$ of a module $M$ over a semiring $R$ that is closed under addition, contains zero, and is closed under scalar multiplication, the function `Submodule.ofClass` constructs a submodule of $M$ with carrier set $s$. More precisely, if: 1. $S$ is a type of subsets of $M$ (with `SetLike S M`), 2. $S$ forms an additive submonoid class (with `AddSubmonoidClass S M`), and 3. $S$ is closed under scalar multiplication (with `SMulMemClass S R M`), then for any $s \in S$, `Submodule.ofClass s` is the submodule of $M$ whose underlying set is $s$.

Submodule.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallHSMul instance

 :
  CanLift (Set M) (Submodule R M) (↑)
    (fun s ↦ 0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ (r : R) {x}, x ∈ s → r • x ∈ s)

Full source

instance (priority := 100) : CanLift (Set M) (Submodule R M) (↑)
    (fun s ↦ 0 ∈ s0 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ (r : R) {x}, x ∈ s → r • x ∈ s) where
  prf s h :=
    ⟨ { carrier := s
        zero_mem' := h.1
        add_mem' := h.2.1
        smul_mem' := h.2.2 },
      rfl ⟩

Lifting Condition for Submodules from Subsets

Informal description

A subset $s$ of a module $M$ over a semiring $R$ can be lifted to a submodule of $M$ if and only if $s$ contains the zero vector and is closed under addition and scalar multiplication. That is, $0 \in s$, and for all $x, y \in s$ and $r \in R$, we have $x + y \in s$ and $r \bullet x \in s$.

Submodule.addSubmonoidClass instance

: AddSubmonoidClass (Submodule R M) M

Full source

instance addSubmonoidClass : AddSubmonoidClass (Submodule R M) M where
  zero_mem _ := AddSubmonoid.zero_mem' _
  add_mem := AddSubsemigroup.add_mem' _

Submodules as Additive Submonoids

Informal description

For any semiring $R$ and module $M$ over $R$, the type of submodules of $M$ forms an additive submonoid class. This means that every submodule $S \subseteq M$ contains the zero vector and is closed under addition.

Submodule.smulMemClass instance

: SMulMemClass (Submodule R M) R M

Full source

instance smulMemClass : SMulMemClass (Submodule R M) R M where
  smul_mem {s} c _ h := SubMulAction.smul_mem' s.toSubMulAction c h

Submodules are Closed Under Scalar Multiplication

Informal description

For any semiring $R$ and module $M$ over $R$, the type of submodules of $M$ forms a class of subsets closed under scalar multiplication. That is, for any submodule $S \subseteq M$ and any scalar $r \in R$, if $x \in S$ then $r \bullet x \in S$.

Submodule.mem_toAddSubmonoid theorem

(p : Submodule R M) (x : M) : x ∈ p.toAddSubmonoid ↔ x ∈ p

Full source

@[simp]
theorem mem_toAddSubmonoid (p : Submodule R M) (x : M) : x ∈ p.toAddSubmonoidx ∈ p.toAddSubmonoid ↔ x ∈ p :=
  Iff.rfl

Membership in Submodule and its Additive Submonoid Coincide

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$ and any element $x \in M$, the element $x$ belongs to the underlying additive submonoid of $p$ if and only if $x$ belongs to $p$ itself.

Submodule.mem_mk theorem

{S : AddSubmonoid M} {x : M} (h) : x ∈ (⟨S, h⟩ : Submodule R M) ↔ x ∈ S

Full source

@[simp]
theorem mem_mk {S : AddSubmonoid M} {x : M} (h) : x ∈ (⟨S, h⟩ : Submodule R M)x ∈ (⟨S, h⟩ : Submodule R M) ↔ x ∈ S :=
  Iff.rfl

Membership in Submodule Construction via Additive Submonoid

Informal description

For any additive submonoid $S$ of a module $M$ over a semiring $R$, and any element $x \in M$, the element $x$ belongs to the submodule $\langle S, h \rangle$ (where $h$ is a proof that $S$ is closed under scalar multiplication) if and only if $x \in S$.

Submodule.coe_set_mk theorem

(S : AddSubmonoid M) (h) : ((⟨S, h⟩ : Submodule R M) : Set M) = S

Full source

@[simp]
theorem coe_set_mk (S : AddSubmonoid M) (h) : ((⟨S, h⟩ : Submodule R M) : Set M) = S :=
  rfl

Submodule Construction Preserves Underlying Set

Informal description

For any additive submonoid $S$ of a module $M$ over a semiring $R$, and any proof $h$ that $S$ is closed under scalar multiplication, the underlying set of the submodule constructed from $S$ and $h$ is equal to $S$ itself. In other words, if we construct a submodule $\langle S, h \rangle$ from $S$ and $h$, then the coercion of this submodule to a set of $M$ satisfies $(\langle S, h \rangle : \text{Set } M) = S$.

Submodule.eta theorem

(h) : ({ p with smul_mem' := h } : Submodule R M) = p

Full source

@[simp] theorem eta (h) : ({p with smul_mem' := h} : Submodule R M) = p :=
  rfl

Submodule Construction via Scalar Multiplication Closure Property

Informal description

Given a submodule $p$ of a module $M$ over a semiring $R$, and a proof $h$ that $p$ is closed under scalar multiplication, the submodule constructed by replacing the scalar multiplication closure property of $p$ with $h$ is equal to $p$ itself.

Submodule.mk_le_mk theorem

{S S' : AddSubmonoid M} (h h') : (⟨S, h⟩ : Submodule R M) ≤ (⟨S', h'⟩ : Submodule R M) ↔ S ≤ S'

Full source

@[simp]
theorem mk_le_mk {S S' : AddSubmonoid M} (h h') :
    (⟨S, h⟩ : Submodule R M) ≤ (⟨S', h'⟩ : Submodule R M) ↔ S ≤ S' :=
  Iff.rfl

Submodule Ordering via Additive Submonoid Ordering

Informal description

For any two additive submonoids $S$ and $S'$ of a module $M$ over a semiring $R$, and given proofs $h$ and $h'$ that $S$ and $S'$ are closed under scalar multiplication, the submodule $\langle S, h \rangle$ is less than or equal to the submodule $\langle S', h' \rangle$ if and only if $S$ is less than or equal to $S'$ as additive submonoids.

Submodule.ext theorem

(h : ∀ x, x ∈ p ↔ x ∈ q) : p = q

Full source

@[ext]
theorem ext (h : ∀ x, x ∈ px ∈ p ↔ x ∈ q) : p = q :=
  SetLike.ext h

Submodule Extensionality: $p = q \iff \forall x, x \in p \leftrightarrow x \in q$

Informal description

For any two submodules $p$ and $q$ of a module $M$ over a semiring $R$, if for every element $x \in M$ we have $x \in p$ if and only if $x \in q$, then $p = q$.

Submodule.carrier_inj theorem

: p.carrier = q.carrier ↔ p = q

Full source

@[deprecated SetLike.coe_set_eq (since := "2025-04-20")]
theorem carrier_inj : p.carrier = q.carrier ↔ p = q :=
  (SetLike.coe_injective (A := Submodule R M)).eq_iff

Equality of Submodules via Carrier Sets

Informal description

For any two submodules $p$ and $q$ of a module $M$ over a semiring $R$, the underlying sets of $p$ and $q$ are equal if and only if $p = q$ as submodules.

Submodule.copy definition

(p : Submodule R M) (s : Set M) (hs : s = ↑p) : Submodule R M

Full source

/-- Copy of a submodule with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[simps]
protected def copy (p : Submodule R M) (s : Set M) (hs : s = ↑p) : Submodule R M where
  carrier := s
  zero_mem' := by simpa [hs] using p.zero_mem'
  add_mem' := hs.symm ▸ p.add_mem'
  smul_mem' := by simpa [hs] using p.smul_mem'

Copy of a submodule with a specified carrier set

Informal description

Given a submodule $p$ of a module $M$ over a semiring $R$ and a set $s$ equal to the carrier set of $p$, the function returns a new submodule with carrier set $s$ that is definitionally equal to $p$.

Submodule.copy_eq theorem

(S : Submodule R M) (s : Set M) (hs : s = ↑S) : S.copy s hs = S

Full source

theorem copy_eq (S : Submodule R M) (s : Set M) (hs : s = ↑S) : S.copy s hs = S :=
  SetLike.coe_injective hs

Equality of Submodule Copy with Original

Informal description

For any submodule $S$ of a module $M$ over a semiring $R$, and any subset $s$ of $M$ such that $s$ equals the underlying set of $S$, the copy of $S$ with carrier set $s$ is equal to $S$ itself.

Submodule.toAddSubmonoid_injective theorem

: Injective (toAddSubmonoid : Submodule R M → AddSubmonoid M)

Full source

theorem toAddSubmonoid_injective : Injective (toAddSubmonoid : Submodule R M → AddSubmonoid M) :=
  fun p q h => SetLike.ext'_iff.2 (show (p.toAddSubmonoid : Set M) = q from SetLike.ext'_iff.1 h)

Injectivity of Submodule to Additive Submonoid Map

Informal description

The function that maps a submodule $p$ of a module $M$ over a semiring $R$ to its underlying additive submonoid is injective. That is, if two submodules $p$ and $q$ have the same additive submonoid structure, then $p = q$.

Submodule.toAddSubmonoid_inj theorem

: p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q

Full source

@[simp]
theorem toAddSubmonoid_inj : p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q :=
  toAddSubmonoid_injective.eq_iff

Equality of Submodules via Underlying Additive Submonoids

Informal description

For any two submodules $p$ and $q$ of a module $M$ over a semiring $R$, the underlying additive submonoids of $p$ and $q$ are equal if and only if $p = q$.

Submodule.coe_toAddSubmonoid theorem

(p : Submodule R M) : (p.toAddSubmonoid : Set M) = p

Full source

@[simp]
theorem coe_toAddSubmonoid (p : Submodule R M) : (p.toAddSubmonoid : Set M) = p :=
  rfl

Submodule to Additive Submonoid Set Equality

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the underlying set of the additive submonoid associated with $p$ is equal to $p$ itself.

Submodule.toSubMulAction_injective theorem

: Injective (toSubMulAction : Submodule R M → SubMulAction R M)

Full source

theorem toSubMulAction_injective : Injective (toSubMulAction : Submodule R M → SubMulAction R M) :=
  fun p q h => SetLike.ext'_iff.2 (show (p.toSubMulAction : Set M) = q from SetLike.ext'_iff.1 h)

Injectivity of Submodule to SubMulAction Map

Informal description

The function that maps a submodule $p$ of a module $M$ over a semiring $R$ to its underlying subset closed under scalar multiplication (as a `SubMulAction`) is injective. That is, for any two submodules $p$ and $q$, if their associated `SubMulAction` structures are equal, then $p = q$.

Submodule.toSubMulAction_inj theorem

: p.toSubMulAction = q.toSubMulAction ↔ p = q

Full source

theorem toSubMulAction_inj : p.toSubMulAction = q.toSubMulAction ↔ p = q :=
  toSubMulAction_injective.eq_iff

Equality of Submodules via Scalar Multiplication Closure

Informal description

For any two submodules $p$ and $q$ of a module $M$ over a semiring $R$, the subset closed under scalar multiplication associated with $p$ is equal to that of $q$ if and only if $p = q$.

Submodule.coe_toSubMulAction theorem

(p : Submodule R M) : (p.toSubMulAction : Set M) = p

Full source

@[simp]
theorem coe_toSubMulAction (p : Submodule R M) : (p.toSubMulAction : Set M) = p :=
  rfl

Submodule as Subset Equals Itself Under Scalar Multiplication Closure

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the underlying set of the submodule $p$ (viewed as a subset closed under scalar multiplication) is equal to $p$ itself.

SMulMemClass.toModule instance

: Module R S'

Full source

/-- A submodule of a `Module` is a `Module`. -/
instance (priority := 75) toModule : Module R S' := fast_instance%
  Subtype.coe_injective.module R (AddSubmonoidClass.subtype S') (SetLike.val_smul S')

Module Structure on Scalar-Multiplication-Closed Subsets

Informal description

For any subset $S'$ of a module $M$ over a semiring $R$ that is closed under scalar multiplication, $S'$ inherits a module structure from $M$.

SMulMemClass.toModule' definition

 (S R' R A : Type*) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Semiring R'] [SMul R' R] [Module R' A]
  [IsScalarTower R' R A] [SetLike S A] [AddSubmonoidClass S A] [SMulMemClass S R A] (s : S) : Module R' s

Full source

/-- This can't be an instance because Lean wouldn't know how to find `R`, but we can still use
this to manually derive `Module` on specific types. -/
def toModule' (S R' R A : Type*) [Semiring R] [NonUnitalNonAssocSemiring A]
    [Module R A] [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A]
    [SetLike S A] [AddSubmonoidClass S A] [SMulMemClass S R A] (s : S) :
    Module R' s :=
  haveI : SMulMemClass S R' A := SMulMemClass.ofIsScalarTower S R' R A
  SMulMemClass.toModule s

Module structure on scalar-multiplication-closed subsets under compatible scalar actions

Informal description

Given a semiring $R'$, a semiring $R$, and a non-unital non-associative semiring $A$ equipped with a module structure over $R$ and $R'$, where $R'$ acts on $R$ and $A$ in a compatible way (i.e., the scalar multiplication tower property holds), then for any subset $s$ of $A$ that is closed under addition and scalar multiplication (i.e., an additive submonoid and closed under scalar multiplication by $R$), $s$ inherits a module structure over $R'$.

Submodule.mem_carrier theorem

: x ∈ p.carrier ↔ x ∈ (p : Set M)

Full source

theorem mem_carrier : x ∈ p.carrierx ∈ p.carrier ↔ x ∈ (p : Set M) :=
  Iff.rfl

Membership in Submodule Carrier Set Equivalence

Informal description

For any element $x$ in a module $M$ over a semiring $R$ and any submodule $p$ of $M$, the element $x$ belongs to the carrier set of $p$ if and only if $x$ belongs to $p$ when viewed as a subset of $M$.

Submodule.zero_mem theorem

: (0 : M) ∈ p

Full source

@[simp]
protected theorem zero_mem : (0 : M) ∈ p :=
  zero_mem _

Zero Vector Belongs to Every Submodule

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the zero vector $0 \in M$ is contained in $p$.

Submodule.add_mem theorem

(h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p

Full source

protected theorem add_mem (h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p :=
  add_mem h₁ h₂

Closure of Submodule under Addition

Informal description

For any elements $x$ and $y$ in a submodule $p$ of an $R$-module $M$, their sum $x + y$ is also in $p$.

Submodule.smul_mem theorem

(r : R) (h : x ∈ p) : r • x ∈ p

Full source

theorem smul_mem (r : R) (h : x ∈ p) : r • x ∈ p :=
  p.smul_mem' r h

Closure of Submodule under Scalar Multiplication

Informal description

For any scalar $r$ in the semiring $R$ and any element $x$ in the submodule $p$ of the $R$-module $M$, the scalar multiple $r \bullet x$ is also in $p$.

Submodule.smul_of_tower_mem theorem

[SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (h : x ∈ p) : r • x ∈ p

Full source

theorem smul_of_tower_mem [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (h : x ∈ p) :
    r • x ∈ p :=
  p.toSubMulAction.smul_of_tower_mem r h

Closure of Submodule under Scalar Multiplication in Scalar Tower Context

Informal description

Let $M$ be a module over a semiring $R$, and let $S$ be another type equipped with scalar multiplication actions on both $R$ and $M$ such that the scalar multiplication tower property holds (i.e., $(s \cdot r) \bullet x = s \bullet (r \bullet x)$ for $s \in S$, $r \in R$, $x \in M$). For any submodule $p$ of $M$, if $x \in p$ and $r \in S$, then the scalar multiple $r \bullet x$ is also in $p$.

Submodule.smul_mem_iff' theorem

[Group G] [MulAction G M] [SMul G R] [IsScalarTower G R M] (g : G) : g • x ∈ p ↔ x ∈ p

Full source

@[simp]
theorem smul_mem_iff' [Group G] [MulAction G M] [SMul G R] [IsScalarTower G R M] (g : G) :
    g • x ∈ pg • x ∈ p ↔ x ∈ p :=
  p.toSubMulAction.smul_mem_iff' g

Submodule Invariance under Group Action: $g \bullet x \in p \leftrightarrow x \in p$

Informal description

Let $G$ be a group acting on an $R$-module $M$ via scalar multiplication, where the action of $G$ on $M$ is compatible with the scalar multiplication by $R$ (i.e., $(g \cdot r) \bullet x = g \bullet (r \bullet x)$ for all $g \in G$, $r \in R$, $x \in M$). For any submodule $p$ of $M$ and any $g \in G$, we have $g \bullet x \in p$ if and only if $x \in p$.

Submodule.smul_mem_iff'' theorem

[Invertible r] : r • x ∈ p ↔ x ∈ p

Full source

@[simp]
lemma smul_mem_iff'' [Invertible r] :
    r • x ∈ pr • x ∈ p ↔ x ∈ p := by
  refine ⟨fun h ↦ ?_, p.smul_mem r⟩
  rw [← invOf_smul_smul r x]
  exact p.smul_mem _ h

Submodule Membership Criterion for Invertible Scalars: $r \bullet x \in p \leftrightarrow x \in p$

Informal description

For any invertible scalar $r$ in a semiring $R$ and any element $x$ in an $R$-module $M$, the scalar multiple $r \bullet x$ belongs to a submodule $p$ of $M$ if and only if $x$ itself belongs to $p$.

Submodule.add instance

: Add p

Full source

instance add : Add p :=
  ⟨fun x y => ⟨x.1 + y.1, add_mem x.2 y.2⟩⟩

Additive Structure on Submodules

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the submodule $p$ inherits an additive structure from $M$, making it an additive set.

Submodule.zero instance

: Zero p

Full source

instance zero : Zero p :=
  ⟨⟨0, zero_mem _⟩⟩

Zero Vector in Submodules

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, $p$ contains the zero vector of $M$.

Submodule.inhabited instance

: Inhabited p

Full source

instance inhabited : Inhabited p :=
  ⟨0⟩

Nonemptiness of Submodules

Informal description

Every submodule $p$ of a module $M$ over a semiring $R$ is nonempty, as it contains the zero vector.

Submodule.smul instance

[SMul S R] [SMul S M] [IsScalarTower S R M] : SMul S p

Full source

instance smul [SMul S R] [SMul S M] [IsScalarTower S R M] : SMul S p :=
  ⟨fun c x => ⟨c • x.1, smul_of_tower_mem _ c x.2⟩⟩

Scalar Multiplication on Submodules in a Scalar Tower

Informal description

For any semiring $R$, module $M$ over $R$, and submodule $p$ of $M$, if there is a scalar multiplication operation of a type $S$ on both $R$ and $M$ such that the scalar multiplications form a tower (i.e., $(s \cdot r) \bullet m = s \bullet (r \bullet m)$ for $s \in S$, $r \in R$, $m \in M$), then $p$ inherits a scalar multiplication operation from $S$.

Submodule.isScalarTower instance

[SMul S R] [SMul S M] [IsScalarTower S R M] : IsScalarTower S R p

Full source

instance isScalarTower [SMul S R] [SMul S M] [IsScalarTower S R M] : IsScalarTower S R p :=
  p.toSubMulAction.isScalarTower

Scalar Tower Property for Submodules

Informal description

For any semiring $R$, module $M$ over $R$, and submodule $p$ of $M$, if there is a scalar multiplication operation of a type $S$ on both $R$ and $M$ such that the scalar multiplications form a tower (i.e., $(s \cdot r) \bullet m = s \bullet (r \bullet m)$ for $s \in S$, $r \in R$, $m \in M$), then the induced scalar multiplication actions on $p$ also form a scalar tower.

Submodule.isScalarTower' instance

 {S' : Type*} [SMul S R] [SMul S M] [SMul S' R] [SMul S' M] [SMul S S'] [IsScalarTower S' R M] [IsScalarTower S S' M]
  [IsScalarTower S R M] : IsScalarTower S S' p

Full source

instance isScalarTower' {S' : Type*} [SMul S R] [SMul S M] [SMul S' R] [SMul S' M] [SMul S S']
    [IsScalarTower S' R M] [IsScalarTower S S' M] [IsScalarTower S R M] : IsScalarTower S S' p :=
  p.toSubMulAction.isScalarTower'

Scalar Tower Property for Submodules with Multiple Scalar Actions

Informal description

For any semiring $R$, module $M$ over $R$, and submodule $p$ of $M$, if there are scalar multiplication operations of types $S$ and $S'$ on $R$ and $M$ such that: 1. $S'$ forms a scalar tower with $R$ and $M$ (i.e., $(s' \cdot r) \cdot m = s' \cdot (r \cdot m)$ for all $s' \in S'$, $r \in R$, $m \in M$), 2. $S$ forms a scalar tower with $S'$ and $M$ (i.e., $(s \cdot s') \cdot m = s \cdot (s' \cdot m)$ for all $s \in S$, $s' \in S'$, $m \in M$), and 3. $S$ forms a scalar tower with $R$ and $M$ (i.e., $(s \cdot r) \cdot m = s \cdot (r \cdot m)$ for all $s \in S$, $r \in R$, $m \in M$), then $S$ forms a scalar tower with $S'$ and $p$ (i.e., $(s \cdot s') \cdot x = s \cdot (s' \cdot x)$ for all $s \in S$, $s' \in S'$, $x \in p$).

Submodule.nonempty theorem

: (p : Set M).Nonempty

Full source

protected theorem nonempty : (p : Set M).Nonempty :=
  ⟨0, p.zero_mem⟩

Nonemptiness of Submodules

Informal description

Every submodule $p$ of a module $M$ over a semiring $R$ is nonempty.

Submodule.mk_eq_zero theorem

{x} (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0

Full source

@[simp]
theorem mk_eq_zero {x} (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 :=
  Subtype.ext_iff_val

Submodule Element Equals Zero if and only if Underlying Element Equals Zero

Informal description

For any element $x$ in a submodule $p$ of a module $M$ over a semiring $R$, the element $\langle x, h \rangle$ (where $h$ is a proof that $x \in p$) is equal to zero in the submodule $p$ if and only if $x$ is equal to zero in $M$.

Submodule.coe_eq_zero theorem

{x : p} : (x : M) = 0 ↔ x = 0

Full source

@[norm_cast]
theorem coe_eq_zero {x : p} : (x : M) = 0 ↔ x = 0 :=
  (SetLike.coe_eq_coe : (x : M) = (0 : p) ↔ x = 0)

Zero Criterion in Submodules via Coercion

Informal description

For any element $x$ of a submodule $p$ of a module $M$ over a semiring $R$, the coercion of $x$ to $M$ equals the zero vector in $M$ if and only if $x$ is the zero element in $p$. That is, $(x : M) = 0 \leftrightarrow x = 0$.

Submodule.coe_add theorem

(x y : p) : (↑(x + y) : M) = ↑x + ↑y

Full source

@[simp, norm_cast]
theorem coe_add (x y : p) : (↑(x + y) : M) = ↑x + ↑y :=
  rfl

Coercion Preserves Addition in Submodules

Informal description

For any elements $x$ and $y$ in a submodule $p$ of a module $M$ over a semiring $R$, the coercion of their sum in $p$ to $M$ equals the sum of their coercions to $M$, i.e., $(x + y) = x + y$ where the left-hand side is interpreted in $M$ and the right-hand side is the sum in $M$ of the coerced elements.

Submodule.coe_zero theorem

: ((0 : p) : M) = 0

Full source

@[simp, norm_cast]
theorem coe_zero : ((0 : p) : M) = 0 :=
  rfl

Zero Vector Coercion in Submodules: $(0 : p) = 0 \in M$

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the zero vector of $p$ (when viewed as an element of $M$) is equal to the zero vector of $M$, i.e., $(0 : p) = 0 \in M$.

Submodule.coe_smul theorem

(r : R) (x : p) : ((r • x : p) : M) = r • (x : M)

Full source

@[norm_cast]
theorem coe_smul (r : R) (x : p) : ((r • x : p) : M) = r • (x : M) :=
  rfl

Submodule Scalar Multiplication Coercion: $(r \bullet x)_M = r \bullet x_M$

Informal description

For any scalar $r$ in a semiring $R$ and any element $x$ in a submodule $p$ of a module $M$ over $R$, the coercion of the scalar multiple $r \bullet x$ in $p$ back to $M$ equals the scalar multiple $r \bullet x$ in $M$.

Submodule.coe_smul_of_tower theorem

[SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : p) : ((r • x : p) : M) = r • (x : M)

Full source

@[simp, norm_cast]
theorem coe_smul_of_tower [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : p) :
    ((r • x : p) : M) = r • (x : M) :=
  rfl

Scalar Multiplication in Submodule Matches Parent Module in Scalar Tower Context

Informal description

Let $R$ be a semiring, $M$ a module over $R$, and $p$ a submodule of $M$. Suppose $S$ is a type with scalar multiplication operations on both $R$ and $M$ such that the scalar multiplications form a tower (i.e., $(s \cdot r) \bullet m = s \bullet (r \bullet m)$ for $s \in S$, $r \in R$, $m \in M$). Then for any $r \in S$ and $x \in p$, the scalar multiplication $r \bullet x$ in $p$ corresponds to $r \bullet x$ in $M$ under the coercion map.

Submodule.coe_mk theorem

(x : M) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : M) = x

Full source

@[norm_cast]
theorem coe_mk (x : M) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : M) = x :=
  rfl

Submodule Coercion Identity: $\langle x, hx \rangle_M = x$

Informal description

For any element $x$ in a module $M$ over a semiring $R$, and any proof $hx$ that $x$ belongs to a submodule $p$ of $M$, the coercion of the submodule element $\langle x, hx \rangle$ back to $M$ equals $x$.

Submodule.coe_mem theorem

(x : p) : (x : M) ∈ p

Full source

theorem coe_mem (x : p) : (x : M) ∈ p :=
  x.2

Submodule Element Membership

Informal description

For any element $x$ in a submodule $p$ of a module $M$ over a semiring $R$, the underlying element $x$ (when viewed as an element of $M$) belongs to the submodule $p$.

Submodule.addCommMonoid instance

: AddCommMonoid p

Full source

instance addCommMonoid : AddCommMonoid p := fast_instance%
  { p.toAddSubmonoid.toAddCommMonoid with }

Submodules as Additive Commutative Monoids

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the submodule $p$ inherits an additive commutative monoid structure from $M$.

Submodule.module' instance

[Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : Module S p

Full source

instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
    Module S p := fast_instance%
  { (show MulAction S p from p.toSubMulAction.mulAction') with
    smul_zero := fun a => by ext; simp
    zero_smul := fun a => by ext; simp
    add_smul := fun a b x => by ext; simp [add_smul]
    smul_add := fun a x y => by ext; simp [smul_add] }

Submodule as Module over Scalar Semiring

Informal description

For any semiring $S$ with a scalar multiplication action on a semiring $R$, and a module $M$ over $R$ that is also a module over $S$ with compatible scalar multiplications (i.e., $(s \cdot r) \cdot m = s \cdot (r \cdot m)$ for all $s \in S$, $r \in R$, $m \in M$), any submodule $p$ of $M$ inherits a module structure over $S$.

Submodule.module instance

: Module R p

Full source

instance module : Module R p :=
  p.module'

Submodules as Modules

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the submodule $p$ inherits a module structure over $R$ with the same operations as $M$.

Submodule.addSubgroupClass instance

[Module R M] : AddSubgroupClass (Submodule R M) M

Full source

instance addSubgroupClass [Module R M] : AddSubgroupClass (Submodule R M) M :=
  { Submodule.addSubmonoidClass with neg_mem := fun p {_} => p.toSubMulAction.neg_mem }

Submodules as Additive Subgroups

Informal description

For any semiring $R$ and module $M$ over $R$, the type of submodules of $M$ forms an additive subgroup class. This means that every submodule $S \subseteq M$ is closed under addition, contains the zero vector, and is closed under negation.

Submodule.neg_mem theorem

(hx : x ∈ p) : -x ∈ p

Full source

protected theorem neg_mem (hx : x ∈ p) : -x ∈ p :=
  neg_mem hx

Closure of Submodule under Additive Inversion

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, if an element $x$ belongs to $p$, then its additive inverse $-x$ also belongs to $p$.

Submodule.toAddSubgroup definition

: AddSubgroup M

Full source

/-- Reinterpret a submodule as an additive subgroup. -/
def toAddSubgroup : AddSubgroup M :=
  { p.toAddSubmonoid with neg_mem' := fun {_} => p.neg_mem }

Submodule as additive subgroup

Informal description

The function converts a submodule $p$ of a module $M$ over a semiring $R$ into an additive subgroup of $M$, where the underlying set remains the same and the additive inverse property is preserved.

Submodule.coe_toAddSubgroup theorem

: (p.toAddSubgroup : Set M) = p

Full source

@[simp]
theorem coe_toAddSubgroup : (p.toAddSubgroup : Set M) = p :=
  rfl

Submodule to Additive Subgroup Coercion Equality

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the underlying set of the additive subgroup obtained from $p$ via the `toAddSubgroup` function is equal to $p$ itself. In other words, the coercion of $p.toAddSubgroup$ to a set of elements of $M$ is identical to $p$.

Submodule.mem_toAddSubgroup theorem

: x ∈ p.toAddSubgroup ↔ x ∈ p

Full source

@[simp]
theorem mem_toAddSubgroup : x ∈ p.toAddSubgroupx ∈ p.toAddSubgroup ↔ x ∈ p :=
  Iff.rfl

Membership Equivalence Between Submodule and Its Additive Subgroup

Informal description

For any element $x$ in a module $M$ over a semiring $R$, and any submodule $p$ of $M$, the element $x$ belongs to the additive subgroup associated with $p$ if and only if $x$ belongs to $p$ itself. In other words, $x \in p.\text{toAddSubgroup} \leftrightarrow x \in p$.

Submodule.toAddSubgroup_injective theorem

: Injective (toAddSubgroup : Submodule R M → AddSubgroup M)

Full source

theorem toAddSubgroup_injective : Injective (toAddSubgroup : Submodule R M → AddSubgroup M)
  | _, _, h => SetLike.ext (SetLike.ext_iff.1 h :)

Injectivity of Submodule to Additive Subgroup Conversion

Informal description

The function that maps a submodule $p$ of a module $M$ over a semiring $R$ to its underlying additive subgroup is injective. In other words, if two submodules $p$ and $p'$ have the same underlying additive subgroup, then $p = p'$.

Submodule.toAddSubgroup_inj theorem

: p.toAddSubgroup = p'.toAddSubgroup ↔ p = p'

Full source

@[simp]
theorem toAddSubgroup_inj : p.toAddSubgroup = p'.toAddSubgroup ↔ p = p' :=
  toAddSubgroup_injective.eq_iff

Submodule Equality via Additive Subgroup Equality

Informal description

For any two submodules $p$ and $p'$ of a module $M$ over a semiring $R$, the equality of their associated additive subgroups $p.\text{toAddSubgroup} = p'.\text{toAddSubgroup}$ holds if and only if $p = p'$.

Submodule.sub_mem theorem

: x ∈ p → y ∈ p → x - y ∈ p

Full source

protected theorem sub_mem : x ∈ p → y ∈ p → x - y ∈ p :=
  sub_mem

Submodule Closed Under Subtraction

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, if $x$ and $y$ are elements of $p$, then their difference $x - y$ is also an element of $p$.

Submodule.neg_mem_iff theorem

: -x ∈ p ↔ x ∈ p

Full source

protected theorem neg_mem_iff : -x ∈ p-x ∈ p ↔ x ∈ p :=
  neg_mem_iff

Negation Membership Criterion for Submodules

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, and for any element $x \in M$, the negation $-x$ is in $p$ if and only if $x$ is in $p$.

Submodule.add_mem_iff_left theorem

: y ∈ p → (x + y ∈ p ↔ x ∈ p)

Full source

protected theorem add_mem_iff_left : y ∈ p → (x + y ∈ px + y ∈ p ↔ x ∈ p) :=
  add_mem_cancel_right

Submodule Membership Criterion via Left Addition: $x + y \in p \leftrightarrow x \in p$ when $y \in p$

Informal description

Let $M$ be a module over a semiring $R$, and let $p$ be a submodule of $M$. For any elements $x, y \in M$, if $y \in p$, then $x + y \in p$ if and only if $x \in p$.

Submodule.add_mem_iff_right theorem

: x ∈ p → (x + y ∈ p ↔ y ∈ p)

Full source

protected theorem add_mem_iff_right : x ∈ p → (x + y ∈ px + y ∈ p ↔ y ∈ p) :=
  add_mem_cancel_left

Membership Criterion for Sum in Submodule: Right Addend Case

Informal description

Let $M$ be a module over a semiring $R$, and let $p$ be a submodule of $M$. For any elements $x, y \in M$, if $x \in p$, then $x + y \in p$ if and only if $y \in p$.

Submodule.coe_neg theorem

(x : p) : ((-x : p) : M) = -x

Full source

protected theorem coe_neg (x : p) : ((-x : p) : M) = -x :=
  NegMemClass.coe_neg _

Negation commutes with submodule coercion

Informal description

For any element $x$ in a submodule $p$ of a module $M$ over a semiring $R$, the coercion of the negation of $x$ in $p$ to $M$ equals the negation of the coercion of $x$ to $M$, i.e., $(-x : p) = -x$ where $x$ is considered as an element of $M$.

Submodule.coe_sub theorem

(x y : p) : (↑(x - y) : M) = ↑x - ↑y

Full source

protected theorem coe_sub (x y : p) : (↑(x - y) : M) = ↑x - ↑y :=
  AddSubgroupClass.coe_sub _ _

Coercion Preserves Subtraction in Submodules

Informal description

For any elements $x$ and $y$ in a submodule $p$ of a module $M$ over a semiring $R$, the coercion of their difference $x - y$ in $p$ equals the difference of their coercions in $M$, i.e., $(x - y) = x - y$ (where the left-hand side is interpreted in $p$ and the right-hand side in $M$).

Submodule.sub_mem_iff_left theorem

(hy : y ∈ p) : x - y ∈ p ↔ x ∈ p

Full source

theorem sub_mem_iff_left (hy : y ∈ p) : x - y ∈ px - y ∈ p ↔ x ∈ p := by
  rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]

Submodule Membership Criterion via Left Subtraction: $x - y \in p \leftrightarrow x \in p$ when $y \in p$

Informal description

Let $M$ be a module over a semiring $R$, and let $p$ be a submodule of $M$. For any elements $x, y \in M$, if $y \in p$, then $x - y \in p$ if and only if $x \in p$.

Submodule.sub_mem_iff_right theorem

(hx : x ∈ p) : x - y ∈ p ↔ y ∈ p

Full source

theorem sub_mem_iff_right (hx : x ∈ p) : x - y ∈ px - y ∈ p ↔ y ∈ p := by
  rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]

Membership Criterion for Difference in Submodule: Right Subtrahend Case

Informal description

Let $M$ be a module over a semiring $R$, and let $p$ be a submodule of $M$. For any elements $x, y \in M$, if $x \in p$, then $x - y \in p$ if and only if $y \in p$.

Submodule.addCommGroup instance

: AddCommGroup p

Full source

instance addCommGroup : AddCommGroup p := fast_instance%
  { p.toAddSubgroup.toAddCommGroup with }

Submodules as Commutative Additive Groups

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the additive group structure on $p$ is commutative.

SubmoduleClass.module' instance

 {T : Type*} [Semiring R] [AddCommMonoid M] [Semiring S] [Module R M] [SMul S R] [Module S M] [IsScalarTower S R M]
  [SetLike T M] [AddSubmonoidClass T M] [SMulMemClass T R M] (t : T) : Module S t

Full source

instance (priority := 75) module' {T : Type*} [Semiring R] [AddCommMonoid M] [Semiring S]
    [Module R M] [SMul S R] [Module S M] [IsScalarTower S R M] [SetLike T M] [AddSubmonoidClass T M]
    [SMulMemClass T R M] (t : T) : Module S t where
  one_smul _ := by ext; simp
  mul_smul _ _ _ := by ext; simp [mul_smul]
  smul_zero _ := by ext; simp
  zero_smul _ := by ext; simp
  add_smul _ _ _ := by ext; simp [add_smul]
  smul_add _ _ _ := by ext; simp [smul_add]

Module Structure on Scalar-Multiplication-Closed Subsets

Informal description

For any semiring $R$, additive commutative monoid $M$ with a module structure over $R$, semiring $S$ with a scalar multiplication action on $R$, and a module structure of $S$ on $M$ satisfying the scalar tower condition, if $T$ is a type of subsets of $M$ that forms an additive submonoid and is closed under scalar multiplication by $R$, then any subset $t \in T$ inherits a module structure over $S$.

SubmoduleClass.module instance

 [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :
  Module R s

Full source

instance (priority := 75) module [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M]
    [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) : Module R s :=
  module' s

Module Structure on Submodules

Informal description

For any semiring $R$, additive commutative monoid $M$ with a module structure over $R$, and a subset $s$ of $M$ that forms an additive submonoid and is closed under scalar multiplication by $R$, the subset $s$ inherits a module structure over $R$.

Tags