Mathlib.Algebra.Module.Submodule.Lattice

Submodule.instBot instance

: Bot (Submodule R M)

Full source

/-- The set `{0}` is the bottom element of the lattice of submodules. -/
instance : Bot (Submodule R M) :=
  ⟨{ (⊥ : AddSubmonoid M) with
      carrier := {0}
      smul_mem' := by simp }⟩

The Zero Submodule as Bottom Element

Informal description

For any module $M$ over a semiring $R$, the submodule $\{0\}$ is the bottom element in the lattice of submodules of $M$.

Submodule.inhabited' instance

: Inhabited (Submodule R M)

Full source

instance inhabited' : Inhabited (Submodule R M) :=
  ⟨⊥⟩

Nonempty Collection of Submodules

Informal description

For any module $M$ over a semiring $R$, the collection of submodules of $M$ is nonempty.

Submodule.bot_coe theorem

: ((⊥ : Submodule R M) : Set M) = {0}

Full source

@[simp]
theorem bot_coe : ((⊥ : Submodule R M) : Set M) = {0} :=
  rfl

Zero Submodule as Singleton Set

Informal description

The underlying set of the bottom submodule (the zero submodule) in a module $M$ over a semiring $R$ is equal to the singleton set $\{0\}$.

Submodule.bot_toAddSubmonoid theorem

: (⊥ : Submodule R M).toAddSubmonoid = ⊥

Full source

@[simp]
theorem bot_toAddSubmonoid : (⊥ : Submodule R M).toAddSubmonoid = ⊥ :=
  rfl

Zero Submodule's Additive Submonoid is Bottom Element

Informal description

For any module $M$ over a semiring $R$, the additive submonoid associated with the zero submodule $\{0\}$ is equal to the bottom element of the lattice of additive submonoids of $M$.

Submodule.bot_toAddSubgroup theorem

{R M} [Ring R] [AddCommGroup M] [Module R M] : (⊥ : Submodule R M).toAddSubgroup = ⊥

Full source

@[simp]
lemma bot_toAddSubgroup {R M} [Ring R] [AddCommGroup M] [Module R M] :
    (⊥ : Submodule R M).toAddSubgroup = ⊥ := rfl

Zero Submodule Corresponds to Trivial Additive Subgroup

Informal description

For a module $M$ over a ring $R$ where $M$ is an additive commutative group, the additive subgroup corresponding to the bottom submodule (i.e., the zero submodule $\{0\}$) is equal to the bottom element in the lattice of additive subgroups of $M$.

Submodule.mem_bot theorem

{x : M} : x ∈ (⊥ : Submodule R M) ↔ x = 0

Full source

@[simp]
theorem mem_bot {x : M} : x ∈ (⊥ : Submodule R M)x ∈ (⊥ : Submodule R M) ↔ x = 0 :=
  Set.mem_singleton_iff

Membership in Zero Submodule is Equivalent to Being Zero

Informal description

For any element $x$ in a module $M$ over a semiring $R$, $x$ belongs to the zero submodule $\{0\}$ if and only if $x = 0$.

Submodule.uniqueBot instance

: Unique (⊥ : Submodule R M)

Full source

instance uniqueBot : Unique (⊥ : Submodule R M) :=
  ⟨inferInstance, fun x ↦ Subtype.ext <| (mem_bot R).1 x.mem⟩

Uniqueness of the Zero Submodule

Informal description

The zero submodule $\{0\}$ of a module $M$ over a semiring $R$ has a unique structure, meaning there is exactly one element (the zero element) in this submodule.

Submodule.instOrderBot instance

: OrderBot (Submodule R M)

Full source

instance : OrderBot (Submodule R M) where
  bot := ⊥
  bot_le p x := by simp +contextual [zero_mem]

The Zero Submodule is the Bottom Element in the Lattice of Submodules

Informal description

For any module $M$ over a semiring $R$, the lattice of submodules of $M$ has a bottom element, which is the zero submodule $\{0\}$. This means that for any submodule $N$ of $M$, we have $\{0\} \subseteq N$.

Submodule.bot_ext theorem

(x y : (⊥ : Submodule R M)) : x = y

Full source

@[ext high]
protected theorem bot_ext (x y : (⊥ : Submodule R M)) : x = y := by
  rcases x with ⟨x, xm⟩; rcases y with ⟨y, ym⟩; congr
  rw [(Submodule.eq_bot_iff _).mp rfl x xm]
  rw [(Submodule.eq_bot_iff _).mp rfl y ym]

Uniqueness of Elements in Zero Submodule

Informal description

For any two elements $x$ and $y$ in the zero submodule $\{0\}$ of a module $M$ over a semiring $R$, we have $x = y$.

Submodule.ne_bot_iff theorem

(p : Submodule R M) : p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ (0 : M)

Full source

protected theorem ne_bot_iff (p : Submodule R M) : p ≠ ⊥p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ (0 : M) := by
  simp only [ne_eq, p.eq_bot_iff, not_forall, exists_prop]

Non-triviality Criterion for Submodules: $p \neq \{0\} \leftrightarrow \exists x \in p, x \neq 0$

Informal description

A submodule $p$ of a module $M$ over a semiring $R$ is not equal to the zero submodule $\{0\}$ if and only if there exists a nonzero element $x \in p$ (i.e., $x \in p$ and $x \neq 0$).

Submodule.nonzero_mem_of_bot_lt theorem

{p : Submodule R M} (bot_lt : ⊥ < p) : ∃ a : p, a ≠ 0

Full source

theorem nonzero_mem_of_bot_lt {p : Submodule R M} (bot_lt : ⊥ < p) : ∃ a : p, a ≠ 0 :=
  let ⟨b, hb₁, hb₂⟩ := p.ne_bot_iff.mp bot_lt.ne'
  ⟨⟨b, hb₁⟩, hb₂ ∘ congr_arg Subtype.val⟩

Existence of Nonzero Element in Non-Trivial Submodule

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, if the zero submodule $\{0\}$ is strictly contained in $p$ (i.e., $\{0\} < p$), then there exists a nonzero element $a \in p$.

Submodule.exists_mem_ne_zero_of_ne_bot theorem

{p : Submodule R M} (h : p ≠ ⊥) : ∃ b : M, b ∈ p ∧ b ≠ 0

Full source

theorem exists_mem_ne_zero_of_ne_bot {p : Submodule R M} (h : p ≠ ⊥) : ∃ b : M, b ∈ p ∧ b ≠ 0 :=
  let ⟨b, hb₁, hb₂⟩ := p.ne_bot_iff.mp h
  ⟨b, hb₁, hb₂⟩

Existence of Non-zero Element in Non-trivial Submodule

Informal description

For any non-trivial submodule $p$ of a module $M$ over a semiring $R$ (i.e., $p \neq \{0\}$), there exists a non-zero element $b \in M$ such that $b \in p$.

Submodule.botEquivPUnit definition

: (⊥ : Submodule R M) ≃ₗ[R] PUnit.{v + 1}

Full source

/-- The bottom submodule is linearly equivalent to punit as an `R`-module. -/
@[simps]
def botEquivPUnit : (⊥ : Submodule R M) ≃ₗ[R] PUnit.{v+1} where
  toFun _ := PUnit.unit
  invFun _ := 0
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := rfl

Linear equivalence between the zero submodule and the one-element type

Informal description

The bottom submodule $\{0\}$ of a module $M$ over a semiring $R$ is linearly equivalent to the one-element type $\mathrm{PUnit}$ as an $R$-module. The equivalence maps every element of the zero submodule to the unique element of $\mathrm{PUnit}$, and maps the unique element back to $0 \in M$.

Submodule.subsingleton_iff_eq_bot theorem

: Subsingleton p ↔ p = ⊥

Full source

theorem subsingleton_iff_eq_bot : SubsingletonSubsingleton p ↔ p = ⊥ := by
  rw [subsingleton_iff, Submodule.eq_bot_iff]
  refine ⟨fun h x hx ↦ by simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩,
    fun h ⟨x, hx⟩ ⟨y, hy⟩ ↦ by simp [h x hx, h y hy]⟩

Subsingleton Characterization of the Zero Submodule: $\text{Subsingleton}\,p \leftrightarrow p = \bot$

Informal description

A submodule $p$ of a module $M$ over a semiring $R$ is a subsingleton (i.e., has at most one element) if and only if $p$ is the zero submodule $\{0\}$.

Submodule.nontrivial_iff_ne_bot theorem

: Nontrivial p ↔ p ≠ ⊥

Full source

theorem nontrivial_iff_ne_bot : NontrivialNontrivial p ↔ p ≠ ⊥ := by
  rw [iff_not_comm, not_nontrivial_iff_subsingleton, subsingleton_iff_eq_bot]

Nontrivial Submodule Characterization: $p$ nontrivial $\leftrightarrow p \neq \bot$

Informal description

A submodule $p$ of a module $M$ over a semiring $R$ is nontrivial (i.e., contains at least two distinct elements) if and only if $p$ is not equal to the zero submodule $\{0\}$.

Submodule.instTop instance

: Top (Submodule R M)

Full source

/-- The universal set is the top element of the lattice of submodules. -/
instance : Top (Submodule R M) :=
  ⟨{ (⊤ : AddSubmonoid M) with
      carrier := Set.univ
      smul_mem' := fun _ _ _ ↦ trivial }⟩

The Universal Submodule is the Top Element

Informal description

For any semiring $R$ and any $R$-module $M$, the lattice of submodules of $M$ has a top element, which is the submodule consisting of all elements of $M$.

Submodule.top_coe theorem

: ((⊤ : Submodule R M) : Set M) = Set.univ

Full source

@[simp]
theorem top_coe : ((⊤ : Submodule R M) : Set M) = Set.univ :=
  rfl

Top Submodule as Universal Set

Informal description

The underlying set of the top submodule of an $R$-module $M$ is equal to the universal set of $M$, i.e., $(\top : \text{Submodule } R M) = \text{univ}$.

Submodule.top_toAddSubmonoid theorem

: (⊤ : Submodule R M).toAddSubmonoid = ⊤

Full source

@[simp]
theorem top_toAddSubmonoid : (⊤ : Submodule R M).toAddSubmonoid = ⊤ :=
  rfl

Top Submodule's Additive Submonoid is Universal

Informal description

For any semiring $R$ and any $R$-module $M$, the underlying additive submonoid of the top submodule (i.e., the entire module $M$) is equal to the top additive submonoid of $M$.

Submodule.top_toAddSubgroup theorem

{R M} [Ring R] [AddCommGroup M] [Module R M] : (⊤ : Submodule R M).toAddSubgroup = ⊤

Full source

@[simp]
lemma top_toAddSubgroup {R M} [Ring R] [AddCommGroup M] [Module R M] :
    (⊤ : Submodule R M).toAddSubgroup = ⊤ := rfl

Top Submodule's Additive Subgroup is Universal

Informal description

Let $R$ be a ring and $M$ be an additive commutative group equipped with an $R$-module structure. The additive subgroup associated with the top submodule of $M$ (i.e., the submodule containing all elements of $M$) is equal to the top additive subgroup of $M$.

Submodule.mem_top theorem

{x : M} : x ∈ (⊤ : Submodule R M)

Full source

@[simp]
theorem mem_top {x : M} : x ∈ (⊤ : Submodule R M) :=
  trivial

Every Element Belongs to the Universal Submodule

Informal description

For any element $x$ in an $R$-module $M$, $x$ belongs to the top submodule of $M$, i.e., $x \in \top$.

Submodule.instOrderTop instance

: OrderTop (Submodule R M)

Full source

instance : OrderTop (Submodule R M) where
  top := ⊤
  le_top _ _ _ := trivial

The Universal Submodule as the Greatest Element in the Lattice of Submodules

Informal description

For any semiring $R$ and any $R$-module $M$, the lattice of submodules of $M$ has a top element, which is the submodule consisting of all elements of $M$. Moreover, this top element is the greatest element in the partial order of submodules, meaning that every submodule is contained in the top submodule.

Submodule.topEquiv definition

: (⊤ : Submodule R M) ≃ₗ[R] M

Full source

/-- The top submodule is linearly equivalent to the module.

This is the module version of `AddSubmonoid.topEquiv`. -/
@[simps]
def topEquiv : (⊤ : Submodule R M) ≃ₗ[R] M where
  toFun x := x
  invFun x := ⟨x, mem_top⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv _ := rfl
  right_inv _ := rfl

Linear equivalence between the universal submodule and the module

Informal description

The top submodule of an $R$-module $M$, which consists of all elements of $M$, is linearly equivalent to $M$ itself. The equivalence is given by the identity map in both directions, preserving addition and scalar multiplication.

Submodule.instInfSet instance

: InfSet (Submodule R M)

Full source

instance : InfSet (Submodule R M) :=
  ⟨fun S ↦
    { carrier := ⋂ s ∈ S, (s : Set M)
      zero_mem' := by simp [zero_mem]
      add_mem' := by simp +contextual [add_mem]
      smul_mem' := by simp +contextual [smul_mem] }⟩

Infimum Structure on Submodules

Informal description

For any semiring $R$ and module $M$ over $R$, the lattice of submodules of $M$ has an infimum structure where the infimum of a collection of submodules is their intersection.

Submodule.instMin instance

: Min (Submodule R M)

Full source

instance : Min (Submodule R M) :=
  ⟨fun p q ↦
    { carrier := p ∩ q
      zero_mem' := by simp [zero_mem]
      add_mem' := by simp +contextual [add_mem]
      smul_mem' := by simp +contextual [smul_mem] }⟩

Minimum Operation on Submodules as Intersection

Informal description

For a module $M$ over a semiring $R$, the submodules of $M$ form a lattice with a minimum operation, where the minimum of two submodules $p$ and $q$ is their intersection $p \cap q$.

Submodule.completeLattice instance

: CompleteLattice (Submodule R M)

Full source

instance completeLattice : CompleteLattice (Submodule R M) :=
  { (inferInstance : OrderTop (Submodule R M)),
    (inferInstance : OrderBot (Submodule R M)) with
    sup := fun a b ↦ sInf { x | a ≤ x ∧ b ≤ x }
    le_sup_left := fun _ _ ↦ le_sInf' fun _ ⟨h, _⟩ ↦ h
    le_sup_right := fun _ _ ↦ le_sInf' fun _ ⟨_, h⟩ ↦ h
    sup_le := fun _ _ _ h₁ h₂ ↦ sInf_le' ⟨h₁, h₂⟩
    inf := (· ⊓ ·)
    le_inf := fun _ _ _ ↦ Set.subset_inter
    inf_le_left := fun _ _ ↦ Set.inter_subset_left
    inf_le_right := fun _ _ ↦ Set.inter_subset_right
    sSup S := sInf {sm | ∀ s ∈ S, s ≤ sm}
    le_sSup := fun _ _ hs ↦ le_sInf' fun _ hq ↦ by exact hq _ hs
    sSup_le := fun _ _ hs ↦ sInf_le' hs
    le_sInf := fun _ _ ↦ le_sInf'
    sInf_le := fun _ _ ↦ sInf_le' }

Complete Lattice Structure on Submodules

Informal description

For any semiring $R$ and $R$-module $M$, the lattice of submodules of $M$ forms a complete lattice where: - The partial order is given by inclusion of submodules ($p \leq q$ means $p \subseteq q$) - The infimum of two submodules is their intersection - The bottom element $\bot$ is the zero submodule $\{0\}$ - The top element $\top$ is the entire module $M$ - Arbitrary infima and suprema exist (given by intersections and spans respectively)

Submodule.inf_coe theorem

: ↑(p ⊓ q) = (p ∩ q : Set M)

Full source

@[simp]
theorem inf_coe : ↑(p ⊓ q) = (p ∩ q : Set M) :=
  rfl

Infimum of Submodules as Set Intersection

Informal description

For any two submodules $p$ and $q$ of a module $M$ over a semiring $R$, the underlying set of their infimum $p \sqcap q$ is equal to the intersection of their underlying sets, i.e., \[ \text{carrier}(p \sqcap q) = \text{carrier}(p) \cap \text{carrier}(q). \]

Submodule.mem_inf theorem

{p q : Submodule R M} {x : M} : x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q

Full source

@[simp]
theorem mem_inf {p q : Submodule R M} {x : M} : x ∈ p ⊓ qx ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q :=
  Iff.rfl

Characterization of Membership in Submodule Infimum: $x \in p \sqcap q \leftrightarrow x \in p \land x \in q$

Informal description

For any submodules $p$ and $q$ of a module $M$ over a semiring $R$, and any element $x \in M$, we have $x \in p \sqcap q$ if and only if $x \in p$ and $x \in q$. Here, $p \sqcap q$ denotes the infimum (greatest lower bound) of $p$ and $q$ in the lattice of submodules, which coincides with their intersection as sets.

Submodule.sInf_coe theorem

(P : Set (Submodule R M)) : (↑(sInf P) : Set M) = ⋂ p ∈ P, ↑p

Full source

@[simp]
theorem sInf_coe (P : Set (Submodule R M)) : (↑(sInf P) : Set M) = ⋂ p ∈ P, ↑p :=
  rfl

Infimum of Submodules as Intersection of Carriers

Informal description

For any set $P$ of submodules of a module $M$ over a semiring $R$, the underlying set of the infimum of $P$ is equal to the intersection of the underlying sets of all submodules in $P$. That is, \[ \text{carrier}(\inf P) = \bigcap_{p \in P} \text{carrier}(p). \]

Submodule.finset_inf_coe theorem

{ι} (s : Finset ι) (p : ι → Submodule R M) : (↑(s.inf p) : Set M) = ⋂ i ∈ s, ↑(p i)

Full source

@[simp]
theorem finset_inf_coe {ι} (s : Finset ι) (p : ι → Submodule R M) :
    (↑(s.inf p) : Set M) = ⋂ i ∈ s, ↑(p i) := by
  letI := Classical.decEq ι
  refine s.induction_on ?_ fun i s _ ih ↦ ?_
  · simp
  · rw [Finset.inf_insert, inf_coe, ih]
    simp

Finite Infimum of Submodules as Intersection of Carriers

Informal description

For any finite set $s$ of indices and any family of submodules $(p_i)_{i \in \iota}$ of a module $M$ over a semiring $R$, the underlying set of the infimum $\inf_{i \in s} p_i$ is equal to the intersection $\bigcap_{i \in s} p_i$ of the underlying sets of the submodules. That is, \[ \text{carrier}\left(\inf_{i \in s} p_i\right) = \bigcap_{i \in s} \text{carrier}(p_i). \]

Submodule.iInf_coe theorem

{ι} (p : ι → Submodule R M) : (↑(⨅ i, p i) : Set M) = ⋂ i, ↑(p i)

Full source

@[simp]
theorem iInf_coe {ι} (p : ι → Submodule R M) : (↑(⨅ i, p i) : Set M) = ⋂ i, ↑(p i) := by
  rw [iInf, sInf_coe]; simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']

Infimum of Submodules as Intersection of Carriers for Indexed Family

Informal description

For any indexed family of submodules $(p_i)_{i \in \iota}$ of a module $M$ over a semiring $R$, the underlying set of the infimum $\bigsqcap_i p_i$ is equal to the intersection $\bigcap_i p_i$ of the underlying sets of the submodules. That is, \[ \text{carrier}\left(\bigsqcap_i p_i\right) = \bigcap_i \text{carrier}(p_i). \]

Submodule.mem_sInf theorem

{S : Set (Submodule R M)} {x : M} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Full source

@[simp]
theorem mem_sInf {S : Set (Submodule R M)} {x : M} : x ∈ sInf Sx ∈ sInf S ↔ ∀ p ∈ S, x ∈ p :=
  Set.mem_iInter₂

Characterization of Membership in Infimum of Submodules

Informal description

For any set $S$ of submodules of a module $M$ over a semiring $R$, and any element $x \in M$, the element $x$ belongs to the infimum of $S$ if and only if $x$ belongs to every submodule $p \in S$. In symbols: $$x \in \bigwedge S \leftrightarrow \forall p \in S, x \in p$$

Submodule.mem_iInf theorem

{ι} (p : ι → Submodule R M) {x} : (x ∈ ⨅ i, p i) ↔ ∀ i, x ∈ p i

Full source

@[simp]
theorem mem_iInf {ι} (p : ι → Submodule R M) {x} : (x ∈ ⨅ i, p i) ↔ ∀ i, x ∈ p i := by
  rw [← SetLike.mem_coe, iInf_coe, Set.mem_iInter]; rfl

Characterization of Membership in Infimum of Submodules for Indexed Family

Informal description

For any indexed family of submodules $(p_i)_{i \in \iota}$ of a module $M$ over a semiring $R$, and any element $x \in M$, the element $x$ belongs to the infimum $\bigsqcap_i p_i$ if and only if $x$ belongs to every submodule $p_i$ in the family. In symbols: $$x \in \bigsqcap_i p_i \leftrightarrow \forall i, x \in p_i$$

Submodule.mem_finset_inf theorem

{ι} {s : Finset ι} {p : ι → Submodule R M} {x : M} : x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i

Full source

@[simp]
theorem mem_finset_inf {ι} {s : Finset ι} {p : ι → Submodule R M} {x : M} :
    x ∈ s.inf px ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i := by
  simp only [← SetLike.mem_coe, finset_inf_coe, Set.mem_iInter]

Characterization of Membership in Finite Infimum of Submodules

Informal description

For any finite set $s$ of indices, any family of submodules $(p_i)_{i \in \iota}$ of an $R$-module $M$, and any element $x \in M$, the element $x$ belongs to the infimum $\inf_{i \in s} p_i$ if and only if $x$ belongs to $p_i$ for every $i \in s$. In symbols: $$x \in \bigsqcap_{i \in s} p_i \leftrightarrow \forall i \in s, x \in p_i$$

Submodule.inf_iInf theorem

{ι : Type*} [Nonempty ι] {p : ι → Submodule R M} (q : Submodule R M) : q ⊓ ⨅ i, p i = ⨅ i, q ⊓ p i

Full source

lemma inf_iInf {ι : Type*} [Nonempty ι] {p : ι → Submodule R M} (q : Submodule R M) :
    q ⊓ ⨅ i, p i = ⨅ i, q ⊓ p i :=
  SetLike.coe_injective <| by simpa only [inf_coe, iInf_coe] using Set.inter_iInter _ _

Intersection Distributes over Infimum of Submodules

Informal description

Let $M$ be a module over a semiring $R$, and let $\{p_i\}_{i \in \iota}$ be a nonempty family of submodules of $M$ indexed by $\iota$. For any submodule $q$ of $M$, the intersection of $q$ with the infimum of the family $\{p_i\}$ is equal to the infimum of the family $\{q \cap p_i\}$. In symbols: \[ q \cap \bigsqcap_i p_i = \bigsqcap_i (q \cap p_i). \]

Submodule.mem_sup_left theorem

{S T : Submodule R M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Full source

theorem mem_sup_left {S T : Submodule R M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T := by
  have : S ≤ S ⊔ T := le_sup_left
  rw [LE.le] at this
  exact this

Inclusion of Left Submodule in Supremum

Informal description

For any submodules $S$ and $T$ of an $R$-module $M$, if an element $x \in M$ belongs to $S$, then it also belongs to the supremum $S \sqcup T$ of the submodules.

Submodule.mem_sup_right theorem

{S T : Submodule R M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Full source

theorem mem_sup_right {S T : Submodule R M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T := by
  have : T ≤ S ⊔ T := le_sup_right
  rw [LE.le] at this
  exact this

Right Submodule Inclusion in Supremum

Informal description

For any submodules $S$ and $T$ of an $R$-module $M$, if an element $x \in M$ belongs to $T$, then $x$ also belongs to the supremum $S \sqcup T$ of the submodules.

Submodule.add_mem_sup theorem

{S T : Submodule R M} {s t : M} (hs : s ∈ S) (ht : t ∈ T) : s + t ∈ S ⊔ T

Full source

theorem add_mem_sup {S T : Submodule R M} {s t : M} (hs : s ∈ S) (ht : t ∈ T) : s + t ∈ S ⊔ T :=
  add_mem (mem_sup_left hs) (mem_sup_right ht)

Sum of Elements from Submodules Belongs to Their Supremum

Informal description

Let $M$ be a module over a semiring $R$, and let $S$ and $T$ be submodules of $M$. For any elements $s \in S$ and $t \in T$, their sum $s + t$ belongs to the supremum $S \sqcup T$ of the submodules.

Submodule.sub_mem_sup theorem

 {R' M' : Type*} [Ring R'] [AddCommGroup M'] [Module R' M'] {S T : Submodule R' M'} {s t : M'} (hs : s ∈ S)
  (ht : t ∈ T) : s - t ∈ S ⊔ T

Full source

theorem sub_mem_sup {R' M' : Type*} [Ring R'] [AddCommGroup M'] [Module R' M']
    {S T : Submodule R' M'} {s t : M'} (hs : s ∈ S) (ht : t ∈ T) : s - t ∈ S ⊔ T := by
  rw [sub_eq_add_neg]
  exact add_mem_sup hs (neg_mem ht)

Difference of Submodule Elements Belongs to Their Supremum

Informal description

Let $R'$ be a ring, $M'$ an additive commutative group with a module structure over $R'$, and $S$, $T$ submodules of $M'$. For any elements $s \in S$ and $t \in T$, their difference $s - t$ belongs to the supremum $S \sqcup T$ of the submodules.

Submodule.mem_iSup_of_mem theorem

{ι : Sort*} {b : M} {p : ι → Submodule R M} (i : ι) (h : b ∈ p i) : b ∈ ⨆ i, p i

Full source

theorem mem_iSup_of_mem {ι : Sort*} {b : M} {p : ι → Submodule R M} (i : ι) (h : b ∈ p i) :
    b ∈ ⨆ i, p i :=
  (le_iSup p i) h

Element in Submodule Implies Element in Supremum of Submodules

Informal description

Let $M$ be a module over a semiring $R$, and let $\{p_i\}_{i \in \iota}$ be a family of submodules of $M$ indexed by a type $\iota$. For any element $b \in M$ and any index $i \in \iota$, if $b$ belongs to the submodule $p_i$, then $b$ also belongs to the supremum $\bigsqcup_{i \in \iota} p_i$ of the family of submodules.

Submodule.sum_mem_iSup theorem

 {ι : Type*} [Fintype ι] {f : ι → M} {p : ι → Submodule R M} (h : ∀ i, f i ∈ p i) : (∑ i, f i) ∈ ⨆ i, p i

Full source

theorem sum_mem_iSup {ι : Type*} [Fintype ι] {f : ι → M} {p : ι → Submodule R M}
    (h : ∀ i, f i ∈ p i) : (∑ i, f i) ∈ ⨆ i, p i :=
  sum_mem fun i _ ↦ mem_iSup_of_mem i (h i)

Sum of Elements in Submodules Belongs to Their Supremum

Informal description

Let $M$ be a module over a semiring $R$, and let $\{p_i\}_{i \in \iota}$ be a finite family of submodules of $M$ indexed by a finite type $\iota$. For any family of elements $\{f_i\}_{i \in \iota}$ in $M$ such that each $f_i$ belongs to $p_i$, the sum $\sum_{i \in \iota} f_i$ belongs to the supremum $\bigsqcup_{i \in \iota} p_i$ of the family of submodules.

Submodule.sum_mem_biSup theorem

 {ι : Type*} {s : Finset ι} {f : ι → M} {p : ι → Submodule R M} (h : ∀ i ∈ s, f i ∈ p i) : (∑ i ∈ s, f i) ∈ ⨆ i ∈ s, p i

Full source

theorem sum_mem_biSup {ι : Type*} {s : Finset ι} {f : ι → M} {p : ι → Submodule R M}
    (h : ∀ i ∈ s, f i ∈ p i) : (∑ i ∈ s, f i) ∈ ⨆ i ∈ s, p i :=
  sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_iSup_of_mem hi (h i hi)

Sum of Elements in Submodules Belongs to Their Bounded Supremum

Informal description

Let $M$ be a module over a semiring $R$, $\iota$ a type, $s$ a finite subset of $\iota$, and $f : \iota \to M$ a family of elements in $M$. For each $i \in s$, let $p_i$ be a submodule of $M$ such that $f(i) \in p_i$. Then the sum $\sum_{i \in s} f(i)$ belongs to the supremum $\bigsqcup_{i \in s} p_i$ of the submodules $p_i$ indexed by $i \in s$.

Submodule.mem_sSup_of_mem theorem

{S : Set (Submodule R M)} {s : Submodule R M} (hs : s ∈ S) : ∀ {x : M}, x ∈ s → x ∈ sSup S

Full source

theorem mem_sSup_of_mem {S : Set (Submodule R M)} {s : Submodule R M} (hs : s ∈ S) :
    ∀ {x : M}, x ∈ s → x ∈ sSup S := by
  have := le_sSup hs
  rw [LE.le] at this
  exact this

Element in Submodule Implies Element in Supremum of Submodule Set

Informal description

For any set $S$ of submodules of an $R$-module $M$ and any submodule $s \in S$, if an element $x \in M$ belongs to $s$, then $x$ also belongs to the supremum of $S$ (i.e., the smallest submodule containing all submodules in $S$).

Submodule.toAddSubmonoid_sSup theorem

(s : Set (Submodule R M)) : (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)

Full source

@[simp]
theorem toAddSubmonoid_sSup (s : Set (Submodule R M)) :
    (sSup s).toAddSubmonoid = sSup (toAddSubmonoidtoAddSubmonoid '' s) := by
  let p : Submodule R M :=
    { toAddSubmonoid := sSup (toAddSubmonoidtoAddSubmonoid '' s)
      smul_mem' := fun t {m} h ↦ by
        simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢
        induction h using AddSubmonoid.iSup_induction' with
        | mem p x hx =>
          obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
          apply le_sSup
          rw [Subtype.range_coe_subtype]
          exact ⟨p, hp, rfl⟩
        | one => simpa only [smul_zero] using zero_mem _
        | mul _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_mem }
  refine le_antisymm (?_ : sSup s ≤ p) ?_
  · exact sSup_le fun q hq ↦ le_sSup <| Set.mem_image_of_mem toAddSubmonoid hq
  · exact sSup_le fun _ ⟨q, hq, hq'⟩ ↦ hq'.symm ▸ le_sSup hq

Supremum of Submodules Preserves Additive Submonoid Structure

Informal description

For any set $S$ of submodules of an $R$-module $M$, the additive submonoid associated with the supremum of $S$ is equal to the supremum of the images of the additive submonoids associated with each submodule in $S$. In other words, \[ (\bigsqcup_{p \in S} p).\text{toAddSubmonoid} = \bigsqcup_{p \in S} (p.\text{toAddSubmonoid}). \]

Submodule.subsingleton_iff theorem

: Subsingleton (Submodule R M) ↔ Subsingleton M

Full source

@[simp]
theorem subsingleton_iff : SubsingletonSubsingleton (Submodule R M) ↔ Subsingleton M :=
  have h : SubsingletonSubsingleton (Submodule R M) ↔ Subsingleton (AddSubmonoid M) := by
    rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj,
      bot_toAddSubmonoid, top_toAddSubmonoid]
  h.trans AddSubmonoid.subsingleton_iff

Submodule Lattice is Subsingleton iff Module is Subsingleton

Informal description

The lattice of submodules of an $R$-module $M$ is a subsingleton (has at most one element) if and only if $M$ itself is a subsingleton.

Submodule.nontrivial_iff theorem

: Nontrivial (Submodule R M) ↔ Nontrivial M

Full source

@[simp]
theorem nontrivial_iff : NontrivialNontrivial (Submodule R M) ↔ Nontrivial M :=
  not_iff_not.mp
    ((not_nontrivial_iff_subsingleton.trans <| subsingleton_iff R).trans
      not_nontrivial_iff_subsingleton.symm)

Nontriviality Equivalence for Submodule Lattice and Module

Informal description

The lattice of submodules of an $R$-module $M$ is nontrivial (contains at least two distinct elements) if and only if $M$ itself is nontrivial (contains at least two distinct elements).

Submodule.instUniqueOfSubsingleton instance

[Subsingleton M] : Unique (Submodule R M)

Full source

instance [Subsingleton M] : Unique (Submodule R M) :=
  ⟨⟨⊥⟩, fun a => @Subsingleton.elim _ ((subsingleton_iff R).mpr ‹_›) a _⟩

Uniqueness of Submodules for Subsingleton Modules

Informal description

For any module $M$ over a semiring $R$, if $M$ is a subsingleton (i.e., has at most one element), then the lattice of submodules of $M$ has exactly one element, namely the zero submodule $\{0\}$.

Submodule.unique' instance

[Subsingleton R] : Unique (Submodule R M)

Full source

instance unique' [Subsingleton R] : Unique (Submodule R M) := by
  haveI := Module.subsingleton R M; infer_instance

Uniqueness of Submodules for Subsingleton Semirings

Informal description

For any module $M$ over a semiring $R$, if $R$ is a subsingleton (i.e., has at most one element), then the lattice of submodules of $M$ has exactly one element, namely the zero submodule $\{0\}$.

Submodule.instNontrivial instance

[Nontrivial M] : Nontrivial (Submodule R M)

Full source

instance [Nontrivial M] : Nontrivial (Submodule R M) :=
  (nontrivial_iff R).mpr ‹_›

Nontriviality of Submodule Lattice for Nontrivial Modules

Informal description

For any module $M$ over a semiring $R$, if $M$ is nontrivial (contains at least two distinct elements), then the lattice of submodules of $M$ is also nontrivial (contains at least two distinct submodules).

Submodule.disjoint_def theorem

{p p' : Submodule R M} : Disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = (0 : M)

Full source

theorem disjoint_def {p p' : Submodule R M} : DisjointDisjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = (0 : M) :=
  disjoint_iff_inf_le.trans <| show (∀ x, x ∈ p ∧ x ∈ p' → x ∈ ({0} : Set M)) ↔ _ by simp

Disjointness Criterion for Submodules: $p \cap p' = \{0\}$

Informal description

For any two submodules $p$ and $p'$ of an $R$-module $M$, the submodules are disjoint if and only if every element $x$ that belongs to both $p$ and $p'$ must be the zero element of $M$.

Submodule.disjoint_def' theorem

{p p' : Submodule R M} : Disjoint p p' ↔ ∀ x ∈ p, ∀ y ∈ p', x = y → x = (0 : M)

Full source

theorem disjoint_def' {p p' : Submodule R M} :
    DisjointDisjoint p p' ↔ ∀ x ∈ p, ∀ y ∈ p', x = y → x = (0 : M) :=
  disjoint_def.trans
    ⟨fun h x hx _ hy hxy ↦ h x hx <| hxy.symm ▸ hy, fun h x hx hx' ↦ h _ hx x hx' rfl⟩

Disjoint Submodules Criterion: $x = y \implies x = 0$

Informal description

For any two submodules $p$ and $p'$ of an $R$-module $M$, the submodules are disjoint if and only if for all $x \in p$ and $y \in p'$, if $x = y$ then $x = 0$.

Submodule.mem_right_iff_eq_zero_of_disjoint theorem

{p p' : Submodule R M} (h : Disjoint p p') {x : p} : (x : M) ∈ p' ↔ x = 0

Full source

theorem mem_right_iff_eq_zero_of_disjoint {p p' : Submodule R M} (h : Disjoint p p') {x : p} :
    (x : M) ∈ p'(x : M) ∈ p' ↔ x = 0 :=
  ⟨fun hx => coe_eq_zero.1 <| disjoint_def.1 h x x.2 hx, fun h => h.symm ▸ p'.zero_mem⟩

Characterization of Zero Elements in Disjoint Submodules

Informal description

For any two submodules $p$ and $p'$ of an $R$-module $M$, if $p$ and $p'$ are disjoint (i.e., $p \cap p' = \{0\}$), then for any element $x \in p$, we have $x \in p'$ if and only if $x = 0$.

Submodule.mem_left_iff_eq_zero_of_disjoint theorem

{p p' : Submodule R M} (h : Disjoint p p') {x : p'} : (x : M) ∈ p ↔ x = 0

Full source

theorem mem_left_iff_eq_zero_of_disjoint {p p' : Submodule R M} (h : Disjoint p p') {x : p'} :
    (x : M) ∈ p(x : M) ∈ p ↔ x = 0 :=
  ⟨fun hx => coe_eq_zero.1 <| disjoint_def.1 h x hx x.2, fun h => h.symm ▸ p.zero_mem⟩

Characterization of Zero Element in Disjoint Submodules: $x \in p \cap p' \iff x = 0$ for $x \in p'$

Informal description

Let $M$ be a module over a semiring $R$, and let $p$ and $p'$ be two submodules of $M$ such that $p$ and $p'$ are disjoint (i.e., $p \cap p' = \{0\}$). Then for any element $x \in p'$, we have $x \in p$ if and only if $x = 0$.

AddSubmonoid.toNatSubmodule definition

: AddSubmonoid M ≃o Submodule ℕ M

Full source

/-- An additive submonoid is equivalent to a ℕ-submodule. -/
def AddSubmonoid.toNatSubmodule : AddSubmonoidAddSubmonoid M ≃o Submodule ℕ M where
  toFun S := { S with smul_mem' := fun r s hs ↦ show r • s ∈ S from nsmul_mem hs _ }
  invFun := Submodule.toAddSubmonoid
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' := Iff.rfl

Equivalence between additive submonoids and ℕ-submodules

Informal description

The equivalence between additive submonoids of an additive commutative monoid $M$ and $\mathbb{N}$-submodules of $M$, where the order structure is preserved. Specifically: - The forward map converts an additive submonoid $S$ to a $\mathbb{N}$-submodule by extending it with the natural scalar multiplication property (repeated addition) - The inverse map converts a $\mathbb{N}$-submodule back to its underlying additive submonoid - The equivalence preserves the order structure (inclusion relations)

AddSubmonoid.toNatSubmodule_symm theorem

: ⇑(AddSubmonoid.toNatSubmodule.symm : _ ≃o AddSubmonoid M) = Submodule.toAddSubmonoid

Full source

@[simp]
theorem AddSubmonoid.toNatSubmodule_symm :
    ⇑(AddSubmonoid.toNatSubmodule.symm : _ ≃o AddSubmonoid M) = Submodule.toAddSubmonoid :=
  rfl

Inverse of the Equivalence between Additive Submonoids and $\mathbb{N}$-Submodules

Informal description

The inverse of the order isomorphism `AddSubmonoid.toNatSubmodule` is equal to the function `Submodule.toAddSubmonoid`, which maps a $\mathbb{N}$-submodule back to its underlying additive submonoid. That is, for any $\mathbb{N}$-submodule $S$ of $M$, we have $S.\text{toNatSubmodule}^{-1} = S.\text{toAddSubmonoid}$.

AddSubmonoid.coe_toNatSubmodule theorem

(S : AddSubmonoid M) : (S.toNatSubmodule : Set M) = S

Full source

@[simp]
theorem AddSubmonoid.coe_toNatSubmodule (S : AddSubmonoid M) :
    (S.toNatSubmodule : Set M) = S :=
  rfl

Equality of Underlying Sets in Additive Submonoid to ℕ-Submodule Conversion

Informal description

For any additive submonoid $S$ of an additive commutative monoid $M$, the underlying set of the corresponding $\mathbb{N}$-submodule obtained via the equivalence `AddSubmonoid.toNatSubmodule` is equal to $S$ itself. In other words, $(S.\text{toNatSubmodule} : \text{Set } M) = S$.

AddSubmonoid.toNatSubmodule_toAddSubmonoid theorem

(S : AddSubmonoid M) : S.toNatSubmodule.toAddSubmonoid = S

Full source

@[simp]
theorem AddSubmonoid.toNatSubmodule_toAddSubmonoid (S : AddSubmonoid M) :
    S.toNatSubmodule.toAddSubmonoid = S :=
  AddSubmonoid.toNatSubmodule.symm_apply_apply S

Recovery of Additive Submonoid from $\mathbb{N}$-Submodule Correspondence

Informal description

For any additive submonoid $S$ of an additive commutative monoid $M$, the underlying additive submonoid of the $\mathbb{N}$-submodule corresponding to $S$ via the order isomorphism is equal to $S$ itself. That is, the composition of the forward and inverse maps recovers the original submonoid.

Submodule.toAddSubmonoid_toNatSubmodule theorem

(S : Submodule ℕ M) : S.toAddSubmonoid.toNatSubmodule = S

Full source

@[simp]
theorem Submodule.toAddSubmonoid_toNatSubmodule (S : Submodule ℕ M) :
    S.toAddSubmonoid.toNatSubmodule = S :=
  AddSubmonoid.toNatSubmodule.apply_symm_apply S

$\mathbb{N}$-submodule to additive submonoid roundtrip identity: $S_{\text{toAddSubmonoid} \to \text{toNatSubmodule}} = S$

Informal description

For any $\mathbb{N}$-submodule $S$ of an additive commutative monoid $M$, the $\mathbb{N}$-submodule obtained by first converting $S$ to an additive submonoid and then back to an $\mathbb{N}$-submodule is equal to $S$ itself.

AddSubgroup.toIntSubmodule definition

: AddSubgroup M ≃o Submodule ℤ M

Full source

/-- An additive subgroup is equivalent to a ℤ-submodule. -/
def AddSubgroup.toIntSubmodule : AddSubgroupAddSubgroup M ≃o Submodule ℤ M where
  toFun S := { S with smul_mem' := fun _ _ hs ↦ S.zsmul_mem hs _ }
  invFun := Submodule.toAddSubgroup
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' := Iff.rfl

Order isomorphism between additive subgroups and ℤ-submodules

Informal description

There is an order-preserving isomorphism between the lattice of additive subgroups of an additive commutative group $M$ and the lattice of $\mathbb{Z}$-submodules of $M$. Specifically: - The forward direction maps an additive subgroup $S$ to the $\mathbb{Z}$-submodule with the same underlying set, where scalar multiplication is given by the group's integer multiple operation. - The inverse direction maps a $\mathbb{Z}$-submodule back to its underlying additive subgroup. - This bijection preserves the order structure (inclusion relations) between subgroups and submodules.

AddSubgroup.toIntSubmodule_symm theorem

: ⇑(AddSubgroup.toIntSubmodule.symm : _ ≃o AddSubgroup M) = Submodule.toAddSubgroup

Full source

@[simp]
theorem AddSubgroup.toIntSubmodule_symm :
    ⇑(AddSubgroup.toIntSubmodule.symm : _ ≃o AddSubgroup M) = Submodule.toAddSubgroup :=
  rfl

Inverse of the Additive Subgroup to ℤ-Submodule Isomorphism

Informal description

The inverse of the order isomorphism between additive subgroups of $M$ and $\mathbb{Z}$-submodules of $M$ is given by the canonical map from $\mathbb{Z}$-submodules back to additive subgroups. Specifically, for any $\mathbb{Z}$-submodule $S$, the inverse map sends $S$ to its underlying additive subgroup via the function `Submodule.toAddSubgroup`.

AddSubgroup.coe_toIntSubmodule theorem

(S : AddSubgroup M) : (S.toIntSubmodule : Set M) = S

Full source

@[simp]
theorem AddSubgroup.coe_toIntSubmodule (S : AddSubgroup M) :
    (S.toIntSubmodule : Set M) = S :=
  rfl

Equality of Underlying Sets in Additive Subgroup to ℤ-Submodule Conversion

Informal description

For any additive subgroup $S$ of an additive commutative group $M$, the underlying set of the corresponding $\mathbb{Z}$-submodule obtained via the order isomorphism `AddSubgroup.toIntSubmodule` is equal to $S$ itself. In other words, $(S.\text{toIntSubmodule} : \text{Set } M) = S$.

AddSubgroup.toIntSubmodule_toAddSubgroup theorem

(S : AddSubgroup M) : S.toIntSubmodule.toAddSubgroup = S

Full source

@[simp]
theorem AddSubgroup.toIntSubmodule_toAddSubgroup (S : AddSubgroup M) :
    S.toIntSubmodule.toAddSubgroup = S :=
  AddSubgroup.toIntSubmodule.symm_apply_apply S

Round-trip property of additive subgroup to ℤ-submodule conversion: $S \mapsto \mathbb{Z}\text{-submodule} \mapsto S$

Informal description

For any additive subgroup $S$ of an additive commutative group $M$, the $\mathbb{Z}$-submodule obtained by applying the order isomorphism `AddSubgroup.toIntSubmodule` to $S$, when converted back to an additive subgroup via `Submodule.toAddSubgroup`, recovers the original subgroup $S$. In other words, the composition of these operations is the identity on additive subgroups.

Submodule.toAddSubgroup_toIntSubmodule theorem

(S : Submodule ℤ M) : S.toAddSubgroup.toIntSubmodule = S

Full source

@[simp]
theorem Submodule.toAddSubgroup_toIntSubmodule (S : Submodule ℤ M) :
    S.toAddSubgroup.toIntSubmodule = S :=
  AddSubgroup.toIntSubmodule.apply_symm_apply S

Submodule-Invariant Under Subgroup Conversion: $S_{\mathbb{Z}} \to S_{\text{add}} \to S_{\mathbb{Z}} = S_{\mathbb{Z}}$

Informal description

For any $\mathbb{Z}$-submodule $S$ of an additive commutative group $M$, the $\mathbb{Z}$-submodule obtained by first converting $S$ to an additive subgroup and then back to a $\mathbb{Z}$-submodule is equal to $S$ itself. In other words, the composition of the operations: 1. `toAddSubgroup`: converting a $\mathbb{Z}$-submodule to its underlying additive subgroup 2. `toIntSubmodule`: converting an additive subgroup back to a $\mathbb{Z}$-submodule results in the original submodule.

Implementation notes