Mathlib.Algebra.Module.Submodule.Basic

Submodule.toAddSubmonoid_strictMono theorem

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

Full source

@[mono]
theorem toAddSubmonoid_strictMono : StrictMono (toAddSubmonoid : Submodule R M → AddSubmonoid M) :=
  fun _ _ => id

Strict Monotonicity of Submodule to Additive Submonoid Map

Informal description

The function that maps a submodule $p$ of an $R$-module $M$ to its underlying additive submonoid is strictly monotone with respect to the partial orders on submodules and additive submonoids. That is, for any submodules $p$ and $q$ of $M$, if $p < q$ then $p.toAddSubmonoid < q.toAddSubmonoid$.

Submodule.toAddSubmonoid_le theorem

: p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q

Full source

theorem toAddSubmonoid_le : p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q :=
  Iff.rfl

Submodule containment via additive submonoid containment

Informal description

For any two submodules $p$ and $q$ of a module $M$ over a semiring $R$, the additive submonoid associated with $p$ is contained in the additive submonoid associated with $q$ if and only if $p$ is contained in $q$ as submodules.

Submodule.toAddSubmonoid_mono theorem

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

Full source

@[mono]
theorem toAddSubmonoid_mono : Monotone (toAddSubmonoid : Submodule R M → AddSubmonoid M) :=
  toAddSubmonoid_strictMono.monotone

Monotonicity of Submodule-to-Additive-Submonoid Mapping

Informal description

The function that maps a submodule $p$ of an $R$-module $M$ to its underlying additive submonoid is monotone with respect to the partial orders on submodules and additive submonoids. That is, for any submodules $p$ and $q$ of $M$, if $p \leq q$ then $p.toAddSubmonoid \leq q.toAddSubmonoid$.

Submodule.toSubMulAction_strictMono theorem

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

Full source

@[mono]
theorem toSubMulAction_strictMono :
    StrictMono (toSubMulAction : Submodule R M → SubMulAction R M) := fun _ _ => id

Strict Monotonicity of Submodule-to-SubMulAction Mapping

Informal description

The function that maps a submodule $p$ of an $R$-module $M$ to its underlying subset (viewed as a `SubMulAction`) is strictly monotone with respect to the partial orders on submodules and subsets closed under scalar multiplication. That is, for any two submodules $p$ and $q$ of $M$, if $p < q$ then the corresponding subsets satisfy $p < q$ as well.

Submodule.toSubMulAction_mono theorem

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

Full source

@[mono]
theorem toSubMulAction_mono : Monotone (toSubMulAction : Submodule R M → SubMulAction R M) :=
  toSubMulAction_strictMono.monotone

Monotonicity of Submodule-to-SubMulAction Mapping

Informal description

The function that maps a submodule $p$ of an $R$-module $M$ to its underlying subset (viewed as a `SubMulAction`) is monotone with respect to the partial orders on submodules and subsets closed under scalar multiplication. That is, for any two submodules $p$ and $q$ of $M$, if $p \leq q$ then the corresponding subsets satisfy $p \leq q$ as well.

Submodule.sum_mem theorem

{t : Finset ι} {f : ι → M} : (∀ c ∈ t, f c ∈ p) → (∑ i ∈ t, f i) ∈ p

Full source

protected theorem sum_mem {t : Finset ι} {f : ι → M} : (∀ c ∈ t, f c ∈ p) → (∑ i ∈ t, f i) ∈ p :=
  sum_mem

Sum of Elements in a Submodule is in the Submodule

Informal description

Let $M$ be a module over a semiring $R$, and let $p$ be a submodule of $M$. For any finite set $t$ (indexed by $\iota$) and any function $f : \iota \to M$, if $f(c) \in p$ for every $c \in t$, then the sum $\sum_{i \in t} f(i)$ belongs to $p$.

Submodule.sum_smul_mem theorem

{t : Finset ι} {f : ι → M} (r : ι → R) (hyp : ∀ c ∈ t, f c ∈ p) : (∑ i ∈ t, r i • f i) ∈ p

Full source

theorem sum_smul_mem {t : Finset ι} {f : ι → M} (r : ι → R) (hyp : ∀ c ∈ t, f c ∈ p) :
    (∑ i ∈ t, r i • f i) ∈ p :=
  sum_mem fun i hi => smul_mem _ _ (hyp i hi)

Submodule closure under linear combinations of elements

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. For any finite set $t$ (indexed by type $\iota$), any function $f \colon \iota \to M$, and any function $r \colon \iota \to R$, if for every $c \in t$ we have $f(c) \in p$ (where $p$ is a submodule of $M$), then the sum $\sum_{i \in t} r(i) \cdot f(i)$ belongs to $p$.

Submodule.isCentralScalar instance

 [SMul S R] [SMul S M] [IsScalarTower S R M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M]
  [IsCentralScalar S M] : IsCentralScalar S p

Full source

instance isCentralScalar [SMul S R] [SMul S M] [IsScalarTower S R M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M]
    [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S p :=
  p.toSubMulAction.isCentralScalar

Submodules Inherit Central Scalar Actions

Informal description

For any submodule $p$ of an $R$-module $M$ with a scalar action by $S$, if $M$ has a central scalar action by $S$ (meaning the left and right scalar actions coincide), then $p$ inherits this central scalar action property.

Submodule.noZeroSMulDivisors instance

[NoZeroSMulDivisors R M] : NoZeroSMulDivisors R p

Full source

instance noZeroSMulDivisors [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R p :=
  ⟨fun {c} {x : p} h =>
    have : c = 0 ∨ (x : M) = 0 := eq_zero_or_eq_zero_of_smul_eq_zero (congr_arg Subtype.val h)
    this.imp_right (@Subtype.ext_iff _ _ x 0).mpr⟩

Submodules Inherit No Zero Scalar Divisors Property

Informal description

For any submodule $p$ of an $R$-module $M$, if $M$ has no zero scalar divisors (i.e., $r \cdot x = 0$ implies $r = 0$ or $x = 0$ for any $r \in R$ and $x \in M$), then the submodule $p$ also has no zero scalar divisors.

Submodule.instVAddSubtypeMem instance

[VAdd M α] : VAdd p α

Full source

instance [VAdd M α] : VAdd p α :=
  p.toAddSubmonoid.vadd

Additive Action Inherited by Submodules

Informal description

For any submodule $p$ of an $R$-module $M$ with an additive action on a type $\alpha$, the submodule $p$ inherits an additive action on $\alpha$ defined by $(s : p) +ᵥ a = (s : M) +ᵥ a$ for $s \in p$ and $a \in \alpha$.

Submodule.vaddCommClass instance

[VAdd M β] [VAdd α β] [VAddCommClass M α β] : VAddCommClass p α β

Full source

instance vaddCommClass [VAdd M β] [VAdd α β] [VAddCommClass M α β] : VAddCommClass p α β :=
  ⟨fun a => vadd_comm (a : M)⟩

Commutativity of Additive Actions for Submodules

Informal description

For any submodule $p$ of an $R$-module $M$, if there are additive actions of $M$ and $\alpha$ on $\beta$ that commute (i.e., satisfy $m +ᵥ (a +ᵥ b) = a +ᵥ (m +ᵥ b)$ for all $m \in M$, $a \in \alpha$, and $b \in \beta$), then the additive actions of $p$ and $\alpha$ on $\beta$ also commute.

Submodule.instFaithfulVAddSubtypeMem instance

[VAdd M α] [FaithfulVAdd M α] : FaithfulVAdd p α

Full source

instance [VAdd M α] [FaithfulVAdd M α] : FaithfulVAdd p α :=
  ⟨fun h => Subtype.ext <| eq_of_vadd_eq_vadd h⟩

Faithfulness of Additive Action Inherited by Submodules

Informal description

For any submodule $p$ of an $R$-module $M$ with a faithful additive action on a type $\alpha$, the induced additive action on $\alpha$ by $p$ is also faithful. That is, if $(s : p) +ᵥ a = (t : p) +ᵥ a$ for all $a \in \alpha$, then $s = t$.

Submodule.vadd_def theorem

[VAdd M α] (g : p) (m : α) : g +ᵥ m = (g : M) +ᵥ m

Full source

theorem vadd_def [VAdd M α] (g : p) (m : α) : g +ᵥ m = (g : M) +ᵥ m :=
  rfl

Definition of Additive Action for Submodule Elements

Informal description

For any submodule $p$ of an $R$-module $M$ with an additive action on a type $\alpha$, the additive action of an element $g \in p$ on $m \in \alpha$ is given by $g +ᵥ m = (g : M) +ᵥ m$, where $(g : M)$ denotes the inclusion of $g$ in $M$.

Submodule.toAddSubgroup_strictMono theorem

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

Full source

@[mono]
theorem toAddSubgroup_strictMono : StrictMono (toAddSubgroup : Submodule R M → AddSubgroup M) :=
  fun _ _ => id

Strict Monotonicity of Submodule to Additive Subgroup Map

Informal description

The map from a submodule $p$ of an $R$-module $M$ to its underlying additive subgroup is strictly monotone. That is, for any two submodules $p$ and $p'$ of $M$, if $p < p'$, then the additive subgroup corresponding to $p$ is strictly contained in the additive subgroup corresponding to $p'$.

Submodule.toAddSubgroup_le theorem

: p.toAddSubgroup ≤ p'.toAddSubgroup ↔ p ≤ p'

Full source

theorem toAddSubgroup_le : p.toAddSubgroup ≤ p'.toAddSubgroup ↔ p ≤ p' :=
  Iff.rfl

Submodule containment via additive subgroup containment

Informal description

For two submodules $p$ and $p'$ of an $R$-module $M$, the additive subgroup associated to $p$ is contained in the additive subgroup associated to $p'$ if and only if $p$ is contained in $p'$. In other words, $p.\text{toAddSubgroup} \leq p'.\text{toAddSubgroup} \leftrightarrow p \leq p'$.

Submodule.toAddSubgroup_mono theorem

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

Full source

@[mono]
theorem toAddSubgroup_mono : Monotone (toAddSubgroup : Submodule R M → AddSubgroup M) :=
  toAddSubgroup_strictMono.monotone

Monotonicity of Submodule-to-Additive-Subgroup Mapping

Informal description

The mapping from a submodule $p$ of an $R$-module $M$ to its underlying additive subgroup is monotone. That is, for any two submodules $p$ and $p'$ of $M$, if $p \leq p'$, then the additive subgroup corresponding to $p$ is contained in the additive subgroup corresponding to $p'$.

Submodule.neg_coe theorem

: -(p : Set M) = p

Full source

theorem neg_coe : -(p : Set M) = p :=
  Set.ext fun _ => p.neg_mem_iff

Negation of Submodule Set Equals Itself: $-p = p$

Informal description

For any submodule $p$ of a module $M$ over a ring $R$, the negation of the underlying set of $p$ is equal to $p$ itself, i.e., $-p = p$.

Submodule.not_mem_of_ortho theorem

{x : M} {N : Submodule R M} (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = (0 : M) → c = 0) : x ∉ N

Full source

theorem not_mem_of_ortho {x : M} {N : Submodule R M}
    (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = (0 : M) → c = 0) : x ∉ N := by
  intro hx
  simpa using ortho (-1) x hx

Non-membership Criterion via Orthogonality in Submodules

Informal description

Let $M$ be a module over a ring $R$, and let $N$ be a submodule of $M$. For an element $x \in M$, if for every scalar $c \in R$ and every element $y \in N$, the equation $c \cdot x + y = 0$ implies $c = 0$, then $x$ does not belong to $N$.

Submodule.ne_zero_of_ortho theorem

{x : M} {N : Submodule R M} (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = (0 : M) → c = 0) : x ≠ 0

Full source

theorem ne_zero_of_ortho {x : M} {N : Submodule R M}
    (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = (0 : M) → c = 0) : x ≠ 0 :=
  mt (fun h => show x ∈ N from h.symm ▸ N.zero_mem) (not_mem_of_ortho ortho)

Nonzero Element Criterion via Orthogonality in Submodules

Informal description

Let $M$ be a module over a ring $R$, and let $N$ be a submodule of $M$. For an element $x \in M$, if for every scalar $c \in R$ and every element $y \in N$, the equation $c \cdot x + y = 0$ implies $c = 0$, then $x$ is not equal to the zero element of $M$.

Submodule.smul_mem_iff theorem

(s0 : s ≠ 0) : s • x ∈ p ↔ x ∈ p

Full source

theorem smul_mem_iff (s0 : s ≠ 0) : s • x ∈ ps • x ∈ p ↔ x ∈ p :=
  p.toSubMulAction.smul_mem_iff s0

Submodule Membership Criterion under Scalar Multiplication: $s \cdot x \in p \leftrightarrow x \in p$ for $s \neq 0$

Informal description

For a nonzero scalar $s$ and an element $x$ in a module $M$ over a semiring $R$, the element $s \cdot x$ belongs to a submodule $p$ of $M$ if and only if $x$ belongs to $p$.

Subspace abbrev

(R : Type u) (M : Type v) [DivisionRing R] [AddCommGroup M] [Module R M]

Full source

/-- Subspace of a vector space. Defined to equal `Submodule`. -/
abbrev Subspace (R : Type u) (M : Type v) [DivisionRing R] [AddCommGroup M] [Module R M] :=
  Submodule R M

Subspace of a Vector Space

Informal description

Given a division ring $R$ and an $R$-module $M$ (which is equivalently an additive commutative group with a scalar multiplication by $R$), a *subspace* of $M$ is a subset of $M$ that is closed under addition and scalar multiplication, and thus inherits the structure of an $R$-module itself.

Tags