Mathlib.Algebra.Algebra.Operations

SubMulAction.algebraMap_mem theorem

(r : R) : algebraMap R A r ∈ (1 : SubMulAction R A)

Full source

theorem algebraMap_mem (r : R) : algebraMapalgebraMap R A r ∈ (1 : SubMulAction R A) :=
  ⟨r, (algebraMap_eq_smul_one r).symm⟩

Image of Algebra Map Lies in Unit Submodule

Informal description

For any element $r$ in a commutative (semi)ring $R$ and any $R$-algebra $A$, the image of $r$ under the algebra map $\text{algebraMap}\, R\, A$ is contained in the unit submodule $1$ of $A$ (where $1$ is defined as the smallest submodule containing all scalar multiples of the multiplicative identity of $A$).

SubMulAction.mem_one' theorem

{x : A} : x ∈ (1 : SubMulAction R A) ↔ ∃ y, algebraMap R A y = x

Full source

theorem mem_one' {x : A} : x ∈ (1 : SubMulAction R A)x ∈ (1 : SubMulAction R A) ↔ ∃ y, algebraMap R A y = x :=
  exists_congr fun r => by rw [algebraMap_eq_smul_one]

Characterization of Elements in the Unit Submodule via Algebra Map

Informal description

An element $x$ of an $R$-algebra $A$ belongs to the submodule $1$ (the submodule generated by the multiplicative identity of $A$) if and only if there exists an element $y \in R$ such that the algebra map $\text{algebraMap}\, R\, A$ evaluated at $y$ equals $x$.

Submodule.one instance

: One (Submodule R A)

Full source

/-- `1 : Submodule R A` is the submodule `R ∙ 1` of `A`.
-/
instance one : One (Submodule R A) :=
  ⟨LinearMap.range (LinearMap.toSpanSingleton R A 1)⟩

The Unit Submodule of an Algebra

Informal description

The submodule $1$ of an $R$-algebra $A$ is defined as the $R$-linear span of the multiplicative identity element $1_A$ in $A$, denoted by $R \cdot 1_A$. This submodule consists of all elements of the form $r \cdot 1_A$ for $r \in R$.

Submodule.one_eq_span theorem

: (1 : Submodule R A) = R ∙ 1

Full source

theorem one_eq_span : (1 : Submodule R A) = R ∙ 1 :=
  (LinearMap.span_singleton_eq_range _ _ _).symm

Unit Submodule as Span of Identity Element

Informal description

The unit submodule $1$ of an $R$-algebra $A$ is equal to the $R$-linear span of the multiplicative identity element $1_A$, i.e., $1 = R \cdot 1_A$.

Submodule.le_one_toAddSubmonoid theorem

: 1 ≤ (1 : Submodule R A).toAddSubmonoid

Full source

theorem le_one_toAddSubmonoid : 1 ≤ (1 : Submodule R A).toAddSubmonoid := by
  rintro x ⟨n, rfl⟩
  exact ⟨n, show (n : R) • (1 : A) = n by rw [Nat.cast_smul_eq_nsmul, nsmul_one]⟩

Inclusion of Additive Submonoid Generated by 1 in Unit Submodule's Additive Submonoid

Informal description

The additive submonoid generated by the multiplicative identity $1$ in an $R$-algebra $A$ is contained in the additive submonoid associated with the unit submodule $1$ of $A$.

Submodule.toSubMulAction_one theorem

: (1 : Submodule R A).toSubMulAction = 1

Full source

@[simp]
theorem toSubMulAction_one : (1 : Submodule R A).toSubMulAction = 1 :=
  SetLike.ext fun _ ↦ by rw [one_eq_span, SubMulAction.mem_one]; exact mem_span_singleton

Equality of Unit Submodule and its Scalar Action Closure: $(1 : \text{Submodule}\, R\, A).\text{toSubMulAction} = 1$

Informal description

For an $R$-algebra $A$, the submodule $1$ (defined as the $R$-linear span of the multiplicative identity $1_A$) is equal to the multiplicative identity submodule when viewed as a subset closed under scalar multiplication. That is, $(1 : \text{Submodule}\, R\, A).\text{toSubMulAction} = 1$.

Submodule.one_eq_span_one_set theorem

: (1 : Submodule R A) = span R 1

Full source

theorem one_eq_span_one_set : (1 : Submodule R A) = span R 1 :=
  one_eq_span

Unit Submodule as Span of Identity Element

Informal description

The unit submodule $1$ of an $R$-algebra $A$ is equal to the $R$-linear span of the singleton set $\{1_A\}$, where $1_A$ is the multiplicative identity in $A$. In other words, $1 = R \cdot 1_A$.

Submodule.one_le theorem

{P : Submodule R A} : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P

Full source

@[simp]
theorem one_le {P : Submodule R A} : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P := by
  simp [one_eq_span]

Unit Submodule Containment Criterion: $1 \leq P \iff 1_A \in P$

Informal description

For any submodule $P$ of an $R$-algebra $A$, the unit submodule $1$ (the $R$-linear span of the multiplicative identity $1_A$) is contained in $P$ if and only if the multiplicative identity $1_A$ belongs to $P$. In other words, $1 \leq P \iff 1_A \in P$.

Submodule.instSMul instance

: SMul (Submodule R A) (Submodule R M)

Full source

instance : SMul (Submodule R A) (Submodule R M) where
  smul A' M' :=
  { __ := A'.toAddSubmonoid • M'.toAddSubmonoid
    smul_mem' := fun r m hm ↦ AddSubmonoid.smul_induction_on hm
      (fun a ha m hm ↦ by rw [← smul_assoc]; exact AddSubmonoid.smul_mem_smul (A'.smul_mem r ha) hm)
      fun m₁ m₂ h₁ h₂ ↦ by rw [smul_add]; exact (A'.1 • M'.1).add_mem h₁ h₂ }

Scalar Multiplication of Submodules

Informal description

For a semiring $R$ and an $R$-module $M$, the submodules of $M$ form a structure with a scalar multiplication operation $\bullet : \text{Submodule } R A \to \text{Submodule } R M \to \text{Submodule } R M$, where for submodules $I \subseteq A$ and $N \subseteq M$, the product $I \bullet N$ is the smallest submodule of $M$ containing all elements of the form $r \bullet n$ for $r \in I$ and $n \in N$.

Submodule.smul_toAddSubmonoid theorem

: (I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid

Full source

theorem smul_toAddSubmonoid : (I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid := rfl

Additive Submonoid of Scalar Product of Submodules Equals Scalar Product of Additive Submonoids

Informal description

For submodules $I$ of an $R$-algebra $A$ and $N$ of an $R$-module $M$, the additive submonoid associated with the scalar product submodule $I \bullet N$ is equal to the scalar product of the additive submonoids associated with $I$ and $N$. That is, \[ (I \bullet N).\text{toAddSubmonoid} = I.\text{toAddSubmonoid} \bullet N.\text{toAddSubmonoid}. \]

Submodule.smul_mem_smul theorem

{r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N

Full source

theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N :=
  AddSubmonoid.smul_mem_smul hr hn

Scalar multiplication preserves membership in submodule products

Informal description

For any elements $r \in I$ and $n \in N$ of submodules $I$ and $N$ respectively, the scalar product $r \bullet n$ belongs to the submodule product $I \bullet N$.

Submodule.smul_le theorem

: I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P

Full source

theorem smul_le : I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P :=
  AddSubmonoid.smul_le

Submodule Product Containment Criterion via Elementwise Condition

Informal description

For submodules $I$ of an $R$-algebra $A$ and $N$, $P$ of an $R$-module $M$, the submodule product $I \bullet N$ is contained in $P$ if and only if for every $r \in I$ and $n \in N$, the scalar product $r \bullet n$ belongs to $P$.

Submodule.coe_set_smul theorem

: (I : Set A) • N = I • N

Full source

@[simp, norm_cast]
lemma coe_set_smul : (I : Set A) • N = I • N :=
  set_smul_eq_of_le _ _ _
    (fun _ _ hr hx ↦ smul_mem_smul hr hx)
    (smul_le.mpr fun _ hr _ hx ↦ mem_set_smul_of_mem_mem hr hx)

Equality of Pointwise and Submodule Scalar Multiplication

Informal description

For any subset $I$ of an $R$-algebra $A$ viewed as a set, and any submodule $N$ of an $R$-module $M$, the pointwise scalar multiplication $I \bullet N$ (defined as the smallest submodule containing all $r \bullet n$ for $r \in I$ and $n \in N$) is equal to the submodule scalar product $I \bullet N$.

Submodule.smul_induction_on theorem

 {p : M → Prop} {x} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)) (add : ∀ x y, p x → p y → p (x + y)) : p x

Full source

@[elab_as_elim]
theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n))
    (add : ∀ x y, p x → p y → p (x + y)) : p x :=
  AddSubmonoid.smul_induction_on H smul add

Induction Principle for Elements of Submodule Scalar Product

Informal description

Let $I$ be a submodule of an $R$-algebra $A$, $N$ a submodule of an $R$-module $M$, and $p : M \to \mathrm{Prop}$ a predicate on $M$. For any $x \in I \bullet N$, if: 1. For all $r \in I$ and $n \in N$, the predicate $p$ holds for the scalar product $r \bullet n$, and 2. For any $x, y \in M$, if $p(x)$ and $p(y)$ hold, then $p(x + y)$ holds, then $p(x)$ holds.

Submodule.smul_induction_on' theorem

 {x : M} (hx : x ∈ I • N) {p : ∀ x, x ∈ I • N → Prop}
  (smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (smul_mem_smul hr hn))
  (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›)) : p x hx

Full source

/-- Dependent version of `Submodule.smul_induction_on`. -/
@[elab_as_elim]
theorem smul_induction_on' {x : M} (hx : x ∈ I • N) {p : ∀ x, x ∈ I • N → Prop}
    (smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (smul_mem_smul hr hn))
    (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›)) : p x hx := by
  refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H
  exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩)
    fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩

Dependent Induction Principle for Submodule Scalar Products

Informal description

Let $R$ be a semiring, $A$ an $R$-algebra, and $M$ an $R$-module. Given submodules $I \subseteq A$ and $N \subseteq M$, for any element $x \in I \bullet N$ and predicate $p : M \to \mathrm{Prop}$ defined on elements of $I \bullet N$, if: 1. For all $r \in I$ and $n \in N$, the predicate $p$ holds for $r \bullet n$, and 2. For any $x, y \in M$ in $I \bullet N$, if $p(x)$ and $p(y)$ hold, then $p(x + y)$ holds, then $p(x)$ holds.

Submodule.smul_mono theorem

(hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P

Full source

theorem smul_mono (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P :=
  AddSubmonoid.smul_le_smul hij hnp

Monotonicity of Submodule Multiplication: $I \subseteq J$ and $N \subseteq P$ implies $I \bullet N \subseteq J \bullet P$

Informal description

Let $R$ be a semiring and let $A$ be an $R$-algebra. For any submodules $I, J$ of $A$ and $N, P$ of an $R$-module $M$, if $I \subseteq J$ and $N \subseteq P$, then the submodule product $I \bullet N$ is contained in $J \bullet P$.

Submodule.smul_mono_left theorem

(h : I ≤ J) : I • N ≤ J • N

Full source

theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N :=
  smul_mono h le_rfl

Left Monotonicity of Submodule Multiplication: $I \subseteq J$ implies $I \bullet N \subseteq J \bullet N$

Informal description

For submodules $I$ and $J$ of an $R$-algebra $A$ and a submodule $N$ of an $R$-module $M$, if $I \subseteq J$, then the submodule product $I \bullet N$ is contained in $J \bullet N$.

Submodule.instCovariantClassHSMulLe_1 instance

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

Full source

instance : CovariantClass (Submodule R A) (Submodule R M) HSMul.hSMul LE.le :=
  ⟨fun _ _ => smul_mono le_rfl⟩

Covariance of Submodule Scalar Multiplication with Respect to Inclusion

Informal description

For any semiring $R$, $R$-algebra $A$, and $R$-module $M$, the scalar multiplication operation $\bullet$ on submodules is covariant with respect to the inclusion order. That is, for any submodules $I, J \subseteq A$ and $N \subseteq M$, if $I \subseteq J$, then $I \bullet N \subseteq J \bullet N$.

Submodule.smul_bot theorem

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

Full source

@[simp]
theorem smul_bot : I • (⊥ : Submodule R M) = ⊥ :=
  toAddSubmonoid_injective <| AddSubmonoid.addSubmonoid_smul_bot _

$I \bullet \bot = \bot$ for submodule scalar multiplication

Informal description

For any submodule $I$ of an $R$-algebra $A$ and the zero submodule $\bot$ of an $R$-module $M$, the scalar multiplication $I \bullet \bot$ equals the zero submodule $\bot$.

Submodule.bot_smul theorem

: (⊥ : Submodule R A) • N = ⊥

Full source

@[simp]
theorem bot_smul : (⊥ : Submodule R A) • N = ⊥ :=
  le_bot_iff.mp <| smul_le.mpr <| by rintro _ rfl _ _; rw [zero_smul]; exact zero_mem _

Zero Submodule Scalar Multiplication Yields Zero Submodule: $\bot \bullet N = \bot$

Informal description

For any submodule $N$ of an $R$-module $M$, the scalar multiplication of the zero submodule $\bot$ of an $R$-algebra $A$ with $N$ equals the zero submodule $\bot$ of $M$, i.e., $\bot \bullet N = \bot$.

Submodule.smul_sup theorem

: I • (N ⊔ P) = I • N ⊔ I • P

Full source

theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P :=
  toAddSubmonoid_injective <| by
    simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup]

Distributivity of Submodule Scalar Multiplication over Supremum: $I \bullet (N \sqcup P) = I \bullet N \sqcup I \bullet P$

Informal description

For any submodule $I$ of an $R$-algebra $A$ and submodules $N, P$ of an $R$-module $M$, the scalar multiplication $I \bullet (N \sqcup P)$ equals the supremum of the scalar multiplications $I \bullet N$ and $I \bullet P$, i.e., $$ I \bullet (N \sqcup P) = (I \bullet N) \sqcup (I \bullet P). $$

Submodule.sup_smul theorem

: (I ⊔ J) • N = I • N ⊔ J • N

Full source

theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N :=
  le_antisymm (smul_le.mpr fun mn hmn p hp ↦ by
    obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
    rw [add_smul]; exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp)
    (sup_le (smul_mono_left le_sup_left) <| smul_mono_left le_sup_right)

Distributivity of Submodule Multiplication over Supremum: $(I \sqcup J) \bullet N = I \bullet N \sqcup J \bullet N$

Informal description

For submodules $I$ and $J$ of an $R$-algebra $A$ and a submodule $N$ of an $R$-module $M$, the product of the supremum $I \sqcup J$ with $N$ equals the supremum of the individual products $I \bullet N$ and $J \bullet N$, i.e., $$(I \sqcup J) \bullet N = (I \bullet N) \sqcup (J \bullet N).$$

Submodule.smul_assoc theorem

 {B} [Semiring B] [Module R B] [Module A B] [Module B M] [IsScalarTower R A B] [IsScalarTower R B M]
  [IsScalarTower A B M] (I : Submodule R A) (J : Submodule R B) (N : Submodule R M) : (I • J) • N = I • J • N

Full source

protected theorem smul_assoc {B} [Semiring B] [Module R B] [Module A B] [Module B M]
    [IsScalarTower R A B] [IsScalarTower R B M] [IsScalarTower A B M]
    (I : Submodule R A) (J : Submodule R B) (N : Submodule R M) :
    (I • J) • N = I • J • N :=
  le_antisymm
    (smul_le.2 fun _ hrsij t htn ↦ smul_induction_on hrsij
      (fun r hr s hs ↦ smul_assoc r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn))
      fun x y ↦ (add_smul x y t).symm ▸ add_mem)
    (smul_le.2 fun r hr _ hsn ↦ smul_induction_on hsn
      (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn)
      fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem)

Associativity of Submodule Multiplication in a Scalar Tower

Informal description

Let $R$ be a semiring, and let $A$, $B$, and $M$ be modules over $R$ with the following additional structures: - $B$ is a semiring and an $R$-module - $M$ is an $R$-module, a $B$-module, and an $A$-module - The scalar multiplications satisfy the tower properties: - $R$ acts on $A$ and $A$ acts on $B$ compatibly: $r \cdot (a \cdot b) = (r \cdot a) \cdot b$ for $r \in R$, $a \in A$, $b \in B$ - $R$ acts on $B$ and $B$ acts on $M$ compatibly: $r \cdot (b \cdot m) = (r \cdot b) \cdot m$ for $r \in R$, $b \in B$, $m \in M$ - $A$ acts on $B$ and $B$ acts on $M$ compatibly: $a \cdot (b \cdot m) = (a \cdot b) \cdot m$ for $a \in A$, $b \in B$, $m \in M$ Then for any submodules $I \subseteq A$, $J \subseteq B$, and $N \subseteq M$, the following associativity holds for submodule multiplication: $$(I \cdot J) \cdot N = I \cdot (J \cdot N)$$

Submodule.smul_iSup theorem

{ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} : I • (⨆ i, t i) = ⨆ i, I • t i

Full source

theorem smul_iSup {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} :
    I • (⨆ i, t i)= ⨆ i, I • t i :=
  toAddSubmonoid_injective <| by
    simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup]

Distributivity of Submodule Multiplication over Supremum: $I \cdot (\bigsqcup_i t_i) = \bigsqcup_i (I \cdot t_i)$

Informal description

Let $R$ be a semiring, $A$ an $R$-algebra, and $M$ an $R$-module. For any submodule $I$ of $A$ and any family of submodules $(t_i)_{i \in \iota}$ of $M$, the scalar multiplication of $I$ with the supremum of the family $(t_i)$ equals the supremum of the scalar multiplications of $I$ with each $t_i$: $$ I \cdot \left( \bigsqcup_{i \in \iota} t_i \right) = \bigsqcup_{i \in \iota} (I \cdot t_i). $$

Submodule.iSup_smul theorem

{ι : Sort*} {t : ι → Submodule R A} {N : Submodule R M} : (⨆ i, t i) • N = ⨆ i, t i • N

Full source

theorem iSup_smul {ι : Sort*} {t : ι → Submodule R A} {N : Submodule R M} :
    (⨆ i, t i) • N = ⨆ i, t i • N :=
  le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (motive := (· • s ∈ _)) ht
    (fun i t ht ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs)
    (by simp_rw [zero_smul]; apply zero_mem) fun x y ↦ by simp_rw [add_smul]; apply add_mem)
    (iSup_le fun i ↦ Submodule.smul_mono_left <| le_iSup _ i)

Distributivity of Supremum over Submodule Multiplication: $(\bigsqcup_i t_i) \bullet N = \bigsqcup_i (t_i \bullet N)$

Informal description

Let $R$ be a semiring, $A$ an $R$-algebra, and $M$ an $R$-module. For any family of submodules $(t_i)_{i \in \iota}$ of $A$ and any submodule $N$ of $M$, the scalar multiplication of the supremum of the family $(t_i)$ with $N$ equals the supremum of the scalar multiplications of each $t_i$ with $N$: \[ \left( \bigsqcup_{i \in \iota} t_i \right) \bullet N = \bigsqcup_{i \in \iota} (t_i \bullet N). \]

Submodule.one_smul theorem

: (1 : Submodule R A) • N = N

Full source

protected theorem one_smul : (1 : Submodule R A) • N = N := by
  refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_
  · obtain ⟨r, rfl⟩ := hr
    rw [LinearMap.toSpanSingleton_apply, smul_one_smul]; exact N.smul_mem r hm
  · rw [← one_smul A m]; exact smul_mem_smul (one_le.mp le_rfl) hm

Unit Submodule Acts as Identity in Scalar Multiplication: $1 \bullet N = N$

Informal description

For any submodule $N$ of an $R$-module $M$, the scalar multiplication of the unit submodule $1$ (the $R$-linear span of the multiplicative identity $1_A$) with $N$ equals $N$ itself, i.e., $1 \bullet N = N$.

Submodule.smul_subset_smul theorem

: (↑I : Set A) • (↑N : Set M) ⊆ (↑(I • N) : Set M)

Full source

theorem smul_subset_smul : (↑I : Set A) • (↑N : Set M) ⊆ (↑(I • N) : Set M) :=
  AddSubmonoid.smul_subset_smul

Inclusion of Pointwise Scalar Multiplication in Submodule Product

Informal description

For submodules $I$ of an $R$-algebra $A$ and $N$ of an $R$-module $M$, the pointwise scalar multiplication of their underlying sets is contained in the underlying set of their scalar product submodule. That is, \[ I \cdot N \subseteq I \bullet N \] where $I \cdot N$ denotes the pointwise product $\{a \cdot n \mid a \in I, n \in N\}$ and $I \bullet N$ denotes the submodule generated by these products.

Submodule.mul instance

: Mul (Submodule R A)

Full source

/-- Multiplication of sub-R-modules of an R-module A that is also a semiring. The submodule `M * N`
consists of finite sums of elements `m * n` for `m ∈ M` and `n ∈ N`. -/
instance mul : Mul (Submodule R A) where
  mul := (· • ·)

Multiplication of Submodules in an Algebra

Informal description

For a commutative ring (or semiring) $R$ and an $R$-algebra $A$, the collection of submodules $\text{Submodule } R A$ is equipped with a multiplication operation. Given two submodules $M$ and $N$, their product $M * N$ is defined as the smallest submodule containing all products $m * n$ for $m \in M$ and $n \in N$.

Submodule.mul_mem_mul theorem

(hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N

Full source

theorem mul_mem_mul (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N :=
  smul_mem_smul hm hn

Product of Submodule Elements Belongs to Submodule Product

Informal description

For any elements $m \in M$ and $n \in N$ of submodules $M$ and $N$ respectively in an $R$-algebra $A$, the product $m \cdot n$ belongs to the submodule product $M \cdot N$.

Submodule.mul_le theorem

: M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P

Full source

theorem mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P :=
  smul_le

Submodule Product Containment Criterion: $M \cdot N \leq P \iff \forall m \in M, \forall n \in N, m \cdot n \in P$

Informal description

For submodules $M$, $N$, and $P$ of an $R$-algebra $A$, the product submodule $M \cdot N$ is contained in $P$ if and only if for every $m \in M$ and $n \in N$, the product $m \cdot n$ belongs to $P$.

Submodule.mul_toAddSubmonoid theorem

(M N : Submodule R A) : (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid

Full source

theorem mul_toAddSubmonoid (M N : Submodule R A) :
    (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid := rfl

Product of Submodules as Additive Submonoids

Informal description

For any two submodules $M$ and $N$ of an $R$-algebra $A$, the underlying additive submonoid of their product $M * N$ is equal to the product of their underlying additive submonoids, i.e., $(M * N).\text{toAddSubmonoid} = M.\text{toAddSubmonoid} * N.\text{toAddSubmonoid}$.

Submodule.mul_induction_on theorem

 {C : A → Prop} {r : A} (hr : r ∈ M * N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r

Full source

@[elab_as_elim]
protected theorem mul_induction_on {C : A → Prop} {r : A} (hr : r ∈ M * N)
    (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r :=
  smul_induction_on hr hm ha

Induction Principle for Elements in the Product of Submodules

Informal description

Let $M$ and $N$ be submodules of an $R$-algebra $A$, and let $C : A \to \mathrm{Prop}$ be a predicate on $A$. For any $r \in M \cdot N$, if: 1. For all $m \in M$ and $n \in N$, the predicate $C$ holds for the product $m \cdot n$, and 2. For any $x, y \in A$, if $C(x)$ and $C(y)$ hold, then $C(x + y)$ holds, then $C(r)$ holds.

Submodule.mul_induction_on' theorem

 {C : ∀ r, r ∈ M * N → Prop} (mem_mul_mem : ∀ m (hm : m ∈ M) n (hn : n ∈ N), C (m * n) (mul_mem_mul hm hn))
  (add : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem hx hy)) {r : A} (hr : r ∈ M * N) : C r hr

Full source

/-- A dependent version of `mul_induction_on`. -/
@[elab_as_elim]
protected theorem mul_induction_on' {C : ∀ r, r ∈ M * N → Prop}
    (mem_mul_mem : ∀ m (hm : m ∈ M) n (hn : n ∈ N), C (m * n) (mul_mem_mul hm hn))
    (add : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem hx hy)) {r : A} (hr : r ∈ M * N) :
    C r hr :=
  smul_induction_on' hr mem_mul_mem add

Dependent Induction Principle for Products of Submodules

Informal description

Let $M$ and $N$ be submodules of an $R$-algebra $A$, and let $C$ be a predicate on elements of $M \cdot N$ (indexed by their membership proof). If: 1. For all $m \in M$ and $n \in N$, the predicate $C$ holds for $m \cdot n$ (with its membership proof), and 2. For any $x, y \in M \cdot N$, if $C$ holds for $x$ and $y$, then $C$ holds for $x + y$, then $C$ holds for every element $r \in M \cdot N$ (with its membership proof).

Submodule.mul_bot theorem

: M * ⊥ = ⊥

Full source

@[simp]
theorem mul_bot : M * ⊥ = ⊥ :=
  smul_bot _

Multiplication of a Submodule by the Zero Submodule Yields the Zero Submodule

Informal description

For any submodule $M$ of an $R$-algebra $A$, the product of $M$ with the zero submodule $\{0\}$ is the zero submodule, i.e., $M \cdot \{0\} = \{0\}$.

Submodule.bot_mul theorem

: ⊥ * M = ⊥

Full source

@[simp]
theorem bot_mul : ⊥ * M = ⊥ :=
  bot_smul _

Zero Submodule Multiplication: $\{0\} \cdot M = \{0\}$

Informal description

For any submodule $M$ of an $R$-algebra $A$, the product of the zero submodule $\{0\}$ with $M$ is the zero submodule, i.e., $\{0\} \cdot M = \{0\}$.

Submodule.one_mul theorem

: (1 : Submodule R A) * M = M

Full source

protected theorem one_mul : (1 : Submodule R A) * M = M :=
  Submodule.one_smul _

Left Identity Property of Unit Submodule: $1 \cdot M = M$

Informal description

For any submodule $M$ of an $R$-algebra $A$, the product of the unit submodule $1$ (the $R$-linear span of the multiplicative identity $1_A$) with $M$ equals $M$ itself, i.e., $1 \cdot M = M$.

Submodule.mul_le_mul theorem

(hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q

Full source

@[mono]
theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q :=
  smul_mono hmp hnq

Monotonicity of Submodule Multiplication: $M \subseteq P$ and $N \subseteq Q$ implies $M * N \subseteq P * Q$

Informal description

Let $R$ be a commutative ring (or semiring) and $A$ be an $R$-algebra. For any submodules $M, N, P, Q$ of $A$, if $M \subseteq P$ and $N \subseteq Q$, then the product submodule $M * N$ is contained in $P * Q$.

Submodule.mul_le_mul_left theorem

(h : M ≤ N) : M * P ≤ N * P

Full source

theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P :=
  smul_mono_left h

Left Monotonicity of Submodule Multiplication: $M \subseteq N$ implies $M * P \subseteq N * P$

Informal description

Let $R$ be a commutative ring (or semiring) and $A$ an $R$-algebra. For any submodules $M$, $N$, and $P$ of $A$, if $M \subseteq N$, then the product submodule $M * P$ is contained in $N * P$.

Submodule.mul_le_mul_right theorem

(h : N ≤ P) : M * N ≤ M * P

Full source

theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P :=
  smul_mono_right _ h

Right Monotonicity of Submodule Multiplication: $N \subseteq P$ implies $M * N \subseteq M * P$

Informal description

Let $R$ be a commutative ring (or semiring) and $A$ an $R$-algebra. For any submodules $M, N, P$ of $A$, if $N \subseteq P$, then the product submodule $M * N$ is contained in $M * P$.

Submodule.mul_comm_of_commute theorem

(h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M

Full source

theorem mul_comm_of_commute (h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M :=
  toAddSubmonoid_injective <| AddSubmonoid.mul_comm_of_commute h

Commutativity of Submodule Product Under Elementwise Commutation

Informal description

Let $R$ be a commutative ring (or semiring), $A$ an $R$-algebra, and $M$, $N$ submodules of $A$. If every element of $M$ commutes with every element of $N$ (i.e., for all $m \in M$ and $n \in N$, $m * n = n * m$), then the product submodules satisfy $M * N = N * M$.

Submodule.mul_sup theorem

: M * (N ⊔ P) = M * N ⊔ M * P

Full source

theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P :=
  smul_sup _ _ _

Distributivity of Submodule Multiplication over Supremum: $M * (N \sqcup P) = M * N \sqcup M * P$

Informal description

For any submodules $M$, $N$, and $P$ of an $R$-algebra $A$, the product of $M$ with the supremum of $N$ and $P$ equals the supremum of the products $M * N$ and $M * P$, i.e., $$ M * (N \sqcup P) = (M * N) \sqcup (M * P). $$

Submodule.sup_mul theorem

: (M ⊔ N) * P = M * P ⊔ N * P

Full source

theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P :=
  sup_smul _ _ _

Distributivity of Submodule Multiplication over Supremum: $(M \sqcup N) * P = M * P \sqcup N * P$

Informal description

For any submodules $M$, $N$, and $P$ of an $R$-algebra $A$, the product of the supremum of $M$ and $N$ with $P$ equals the supremum of the products $M * P$ and $N * P$, i.e., $$(M \sqcup N) * P = (M * P) \sqcup (N * P).$$

Submodule.mul_subset_mul theorem

: (↑M : Set A) * (↑N : Set A) ⊆ (↑(M * N) : Set A)

Full source

theorem mul_subset_mul : (↑M : Set A) * (↑N : Set A) ⊆ (↑(M * N) : Set A) :=
  smul_subset_smul _ _

Inclusion of Pointwise Product in Submodule Product

Informal description

For any two submodules $M$ and $N$ of an $R$-algebra $A$, the pointwise product of their underlying sets is contained in the underlying set of their submodule product. That is, \[ M \cdot N \subseteq M * N \] where $M \cdot N$ denotes the set $\{m \cdot n \mid m \in M, n \in N\}$ and $M * N$ denotes the smallest submodule containing all such products.

Submodule.restrictScalars_mul theorem

 {A B C} [Semiring A] [Semiring B] [Semiring C] [SMul A B] [Module A C] [Module B C] [IsScalarTower A C C]
  [IsScalarTower B C C] [IsScalarTower A B C] {I J : Submodule B C} :
  (I * J).restrictScalars A = I.restrictScalars A * J.restrictScalars A

Full source

lemma restrictScalars_mul {A B C} [Semiring A] [Semiring B] [Semiring C]
    [SMul A B] [Module A C] [Module B C] [IsScalarTower A C C] [IsScalarTower B C C]
    [IsScalarTower A B C] {I J : Submodule B C} :
    (I * J).restrictScalars A = I.restrictScalars A * J.restrictScalars A :=
  rfl

Compatibility of Submodule Multiplication with Restriction of Scalars

Informal description

Let $A$, $B$, and $C$ be semirings with $A$ acting on $B$ via scalar multiplication, and $C$ being a module over both $A$ and $B$. Assume the scalar multiplications satisfy the tower property: 1. $A$ acts on $C$ compatibly with $A$ acting on itself, 2. $B$ acts on $C$ compatibly with $B$ acting on itself, 3. $A$ acts on $C$ through $B$. For any two submodules $I$ and $J$ of $C$ as a $B$-module, the restriction of scalars of their product equals the product of their restrictions of scalars: $$(I \cdot J)\restriction_A = I\restriction_A \cdot J\restriction_A$$

Submodule.iSup_mul theorem

(s : ι → Submodule R A) (t : Submodule R A) : (⨆ i, s i) * t = ⨆ i, s i * t

Full source

theorem iSup_mul (s : ι → Submodule R A) (t : Submodule R A) : (⨆ i, s i) * t = ⨆ i, s i * t :=
  iSup_smul

Distributivity of Supremum over Submodule Multiplication: $(\bigsqcup_i s_i) \cdot t = \bigsqcup_i (s_i \cdot t)$

Informal description

Let $R$ be a commutative ring (or semiring), $A$ an $R$-algebra, and $\{s_i\}_{i \in \iota}$ a family of submodules of $A$. For any submodule $t$ of $A$, the product of the supremum of the family $\{s_i\}$ with $t$ equals the supremum of the products of each $s_i$ with $t$: \[ \left( \bigsqcup_{i \in \iota} s_i \right) \cdot t = \bigsqcup_{i \in \iota} (s_i \cdot t). \]

Submodule.mul_iSup theorem

(t : Submodule R A) (s : ι → Submodule R A) : (t * ⨆ i, s i) = ⨆ i, t * s i

Full source

theorem mul_iSup (t : Submodule R A) (s : ι → Submodule R A) : (t * ⨆ i, s i) = ⨆ i, t * s i :=
  smul_iSup

Distributivity of Submodule Multiplication over Supremum: $t \cdot (\bigsqcup_i s_i) = \bigsqcup_i (t \cdot s_i)$

Informal description

Let $R$ be a commutative ring (or semiring), $A$ an $R$-algebra, and $\{s_i\}_{i \in \iota}$ a family of submodules of $A$. For any submodule $t$ of $A$, the product of $t$ with the supremum of the family $\{s_i\}$ equals the supremum of the products of $t$ with each $s_i$: $$ t \cdot \left( \bigsqcup_{i \in \iota} s_i \right) = \bigsqcup_{i \in \iota} (t \cdot s_i). $$

Submodule.instNonUnitalSemiring instance

: NonUnitalSemiring (Submodule R A)

Full source

/-- Sub-`R`-modules of an `R`-module form an idempotent semiring. -/
instance : NonUnitalSemiring (Submodule R A) where
  __ := toAddSubmonoid_injective.semigroup _ mul_toAddSubmonoid
  zero_mul := bot_mul
  mul_zero := mul_bot
  left_distrib := mul_sup
  right_distrib := sup_mul

Non-Unital Semiring Structure on Submodules of an Algebra

Informal description

For any commutative ring (or semiring) $R$ and $R$-algebra $A$, the collection of submodules $\text{Submodule } R A$ forms a non-unital semiring under the operations of addition (supremum of submodules) and multiplication (product of submodules). Specifically: 1. The addition operation is associative and commutative, with the zero submodule as the additive identity. 2. The multiplication operation is associative and distributes over addition. 3. The zero submodule is absorbing for multiplication (i.e., $0 \cdot M = M \cdot 0 = 0$ for any submodule $M$).

Submodule.instPowNat instance

: Pow (Submodule R A) ℕ

Full source

instance : Pow (Submodule R A) ℕ where
  pow s n := npowRec n s

Natural Power Operation on Submodules

Informal description

For a commutative ring (or semiring) $R$ and an $R$-algebra $A$, the collection of submodules $\text{Submodule } R A$ is equipped with a natural power operation $M^n$ for any submodule $M$ and natural number $n$, where $M^n$ is defined recursively as the product of $M$ with itself $n$ times.

Submodule.pow_eq_npowRec theorem

{n : ℕ} : M ^ n = npowRec n M

Full source

theorem pow_eq_npowRec {n : ℕ} : M ^ n = npowRec n M := rfl

Submodule Power Equals Recursive Power Operation: $M^n = \text{npowRec}(n, M)$

Informal description

For any natural number $n$ and any submodule $M$ of an $R$-algebra $A$, the $n$-th power of $M$ is equal to the result of applying the recursive power operation `npowRec` to $n$ and $M$. That is, $M^n = \text{npowRec}(n, M)$.

Submodule.pow_zero theorem

: M ^ 0 = 1

Full source

protected theorem pow_zero : M ^ 0 = 1 := rfl

Zeroth Power of Submodule Equals Unit Submodule

Informal description

For any submodule $M$ of an $R$-algebra $A$, the zeroth power of $M$ equals the unit submodule, i.e., $M^0 = 1$.

Submodule.pow_succ theorem

{n : ℕ} : M ^ (n + 1) = M ^ n * M

Full source

protected theorem pow_succ {n : ℕ} : M ^ (n + 1) = M ^ n * M := rfl

Recursive Power Formula for Submodules: $M^{n+1} = M^n \cdot M$

Informal description

For any submodule $M$ of an $R$-algebra $A$ and any natural number $n$, the $(n+1)$-th power of $M$ is equal to the product of the $n$-th power of $M$ and $M$ itself, i.e., $M^{n+1} = M^n \cdot M$.

Submodule.pow_add theorem

{m n : ℕ} (h : n ≠ 0) : M ^ (m + n) = M ^ m * M ^ n

Full source

protected theorem pow_add {m n : ℕ} (h : n ≠ 0) : M ^ (m + n) = M ^ m * M ^ n :=
  npowRec_add m n h _ M.one_mul

Power Addition Formula for Submodules: $M^{m+n} = M^m \cdot M^n$ when $n \neq 0$

Informal description

For any submodule $M$ of an $R$-algebra $A$ and any natural numbers $m$ and $n$ with $n \neq 0$, the $(m+n)$-th power of $M$ equals the product of the $m$-th power and the $n$-th power of $M$, i.e., $M^{m+n} = M^m \cdot M^n$.

Submodule.pow_one theorem

: M ^ 1 = M

Full source

protected theorem pow_one : M ^ 1 = M := by
  rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul]

First Power Identity for Submodules: $M^1 = M$

Informal description

For any submodule $M$ of an $R$-algebra $A$, the first power of $M$ equals $M$ itself, i.e., $M^1 = M$.

Submodule.pow_succ' theorem

{n : ℕ} (h : n ≠ 0) : M ^ (n + 1) = M * M ^ n

Full source

/-- `Submodule.pow_succ` with the right hand side commuted. -/
protected theorem pow_succ' {n : ℕ} (h : n ≠ 0) : M ^ (n + 1) = M * M ^ n := by
  rw [add_comm, M.pow_add h, Submodule.pow_one]

Recursive power formula for submodules: $M^{n+1} = M \cdot M^n$ when $n \neq 0$

Informal description

For any submodule $M$ of an $R$-algebra $A$ and any nonzero natural number $n$, the $(n+1)$-th power of $M$ equals the product of $M$ with the $n$-th power of $M$, i.e., $M^{n+1} = M \cdot M^n$.

Submodule.pow_toAddSubmonoid theorem

{n : ℕ} (h : n ≠ 0) : (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n

Full source

theorem pow_toAddSubmonoid {n : ℕ} (h : n ≠ 0) : (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n := by
  induction n with
  | zero => exact (h rfl).elim
  | succ n ih =>
    rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]
    cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]

Power of Submodule's Additive Submonoid Equals Additive Submonoid of Power: $(M^n).\text{toAddSubmonoid} = (M.\text{toAddSubmonoid})^n$ for $n \neq 0$

Informal description

For any natural number $n \neq 0$ and any submodule $M$ of an $R$-algebra $A$, the underlying additive submonoid of the $n$-th power of $M$ is equal to the $n$-th power of the underlying additive submonoid of $M$, i.e., $(M^n).\text{toAddSubmonoid} = (M.\text{toAddSubmonoid})^n$.

Submodule.le_pow_toAddSubmonoid theorem

{n : ℕ} : M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

Full source

theorem le_pow_toAddSubmonoid {n : ℕ} : M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid := by
  obtain rfl | hn := Decidable.eq_or_ne n 0
  · rw [Submodule.pow_zero, pow_zero]
    exact le_one_toAddSubmonoid
  · exact (pow_toAddSubmonoid M hn).ge

Inclusion of Additive Submonoid Powers in Submodule Powers: $(M.\text{toAddSubmonoid})^n \leq (M^n).\text{toAddSubmonoid}$

Informal description

For any natural number $n$ and any submodule $M$ of an $R$-algebra $A$, the $n$-th power of the additive submonoid associated with $M$ is contained in the additive submonoid associated with the $n$-th power of $M$, i.e., $(M.\text{toAddSubmonoid})^n \leq (M^n).\text{toAddSubmonoid}$.

Submodule.pow_subset_pow theorem

{n : ℕ} : (↑M : Set A) ^ n ⊆ ↑(M ^ n : Submodule R A)

Full source

theorem pow_subset_pow {n : ℕ} : (↑M : Set A) ^ n ⊆ ↑(M ^ n : Submodule R A) :=
  trans AddSubmonoid.pow_subset_pow (le_pow_toAddSubmonoid M)

Set Power Contained in Submodule Power: $(M : \text{Set } A)^n \subseteq M^n$

Informal description

For any natural number $n$ and any submodule $M$ of an $R$-algebra $A$, the $n$-th power of the underlying set of $M$ is contained in the underlying set of the $n$-th power of $M$ as a submodule. In symbols: $$(M : \text{Set } A)^n \subseteq (M^n : \text{Set } A)$$ where $M^n$ denotes the $n$-fold product of the submodule $M$ with itself.

Submodule.pow_mem_pow theorem

{x : A} (hx : x ∈ M) (n : ℕ) : x ^ n ∈ M ^ n

Full source

theorem pow_mem_pow {x : A} (hx : x ∈ M) (n : ℕ) : x ^ n ∈ M ^ n :=
  pow_subset_pow _ <| Set.pow_mem_pow hx

Power of Element in Submodule Belongs to Power of Submodule: $x^n \in M^n$

Informal description

For any element $x$ in a submodule $M$ of an $R$-algebra $A$ and any natural number $n$, the $n$-th power $x^n$ belongs to the $n$-th power submodule $M^n$.

Submodule.restrictScalars_pow theorem

 {A B C : Type*} [Semiring A] [Semiring B] [Semiring C] [SMul A B] [Module A C] [Module B C] [IsScalarTower A C C]
  [IsScalarTower B C C] [IsScalarTower A B C] {I : Submodule B C} :
  ∀ {n : ℕ}, (hn : n ≠ 0) → (I ^ n).restrictScalars A = I.restrictScalars A ^ n

Full source

lemma restrictScalars_pow {A B C : Type*} [Semiring A] [Semiring B]
    [Semiring C] [SMul A B] [Module A C] [Module B C]
    [IsScalarTower A C C] [IsScalarTower B C C] [IsScalarTower A B C]
    {I : Submodule B C} :
    ∀ {n : ℕ}, (hn : n ≠ 0) → (I ^ n).restrictScalars A = I.restrictScalars A ^ n
  | 1, _ => by simp [Submodule.pow_one]
  | n + 2, _ => by
    simp [Submodule.pow_succ (n := n + 1), restrictScalars_mul, restrictScalars_pow n.succ_ne_zero]

Compatibility of Restriction of Scalars with Submodule Powers: $(I^n)\big|_{A} = (I\big|_{A})^n$ for $n \neq 0$

Informal description

Let $A$, $B$, and $C$ be semirings with $A$ acting on $B$ and $C$, and $B$ acting on $C$. Suppose the scalar multiplications satisfy the tower properties: 1. $A$ acts on $C$ through $A \to C$ and $C \to C$, 2. $B$ acts on $C$ through $B \to C$ and $C \to C$, 3. $A$ acts on $C$ through $A \to B \to C$. For any $B$-submodule $I$ of $C$ and any nonzero natural number $n$, the restriction of scalars of the $n$-th power of $I$ to $A$ equals the $n$-th power of the restriction of scalars of $I$ to $A$, i.e., $$(I^n)\big|_{A} = (I\big|_{A})^n.$$

Submodule.one_eq_range theorem

: (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A)

Full source

theorem one_eq_range : (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A) := by
  rw [one_eq_span, LinearMap.span_singleton_eq_range,
    LinearMap.toSpanSingleton_eq_algebra_linearMap]

Unit Submodule as Range of Algebra Linear Map

Informal description

The unit submodule $1$ of an $R$-algebra $A$ is equal to the range of the algebra linear map $\text{Algebra.linearMap}_R^A \colon R \to A$. In other words, $1 = \{ r \cdot 1_A \mid r \in R \}$.

Submodule.algebraMap_mem theorem

(r : R) : algebraMap R A r ∈ (1 : Submodule R A)

Full source

theorem algebraMap_mem (r : R) : algebraMapalgebraMap R A r ∈ (1 : Submodule R A) := by
  simp [one_eq_range]

Algebra Map Image in Unit Submodule

Informal description

For any element $r$ in a commutative semiring $R$ and any $R$-algebra $A$, the image of $r$ under the algebra map $\text{algebraMap}_R^A \colon R \to A$ belongs to the unit submodule $1 \subseteq A$, which is the $R$-linear span of the multiplicative identity $1_A$ in $A$.

Submodule.mem_one theorem

{x : A} : x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x

Full source

@[simp]
theorem mem_one {x : A} : x ∈ (1 : Submodule R A)x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x := by
  simp [one_eq_range]

Characterization of Elements in the Unit Submodule of an Algebra

Informal description

An element $x$ of an $R$-algebra $A$ belongs to the unit submodule $1 \subseteq A$ if and only if there exists an element $y \in R$ such that $x$ is the image of $y$ under the algebra map $\text{algebraMap}_R^A \colon R \to A$. In other words, $x \in 1$ if and only if $x = y \cdot 1_A$ for some $y \in R$.

Submodule.map_one theorem

{A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') : map f.toLinearMap (1 : Submodule R A) = 1

Full source

protected theorem map_one {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
    map f.toLinearMap (1 : Submodule R A) = 1 := by
  ext
  simp

Preservation of Unit Submodule under Algebra Homomorphisms

Informal description

Let $R$ be a commutative semiring, $A$ and $A'$ be $R$-algebras, and $f \colon A \to A'$ be an $R$-algebra homomorphism. Then the image of the unit submodule $1 \subseteq A$ under the linear map associated to $f$ is equal to the unit submodule $1 \subseteq A'$. In other words, $f_*(1_A) = 1_{A'}$ where $1_A = R \cdot 1_A$ and $1_{A'} = R \cdot 1_{A'}$ are the $R$-linear spans of the multiplicative identities in $A$ and $A'$ respectively.

Submodule.map_op_one theorem

: map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R A) = 1

Full source

@[simp]
theorem map_op_one :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R A) = 1 := by
  ext x
  induction x
  simp

Preservation of Unit Submodule under Multiplicative Opposite Linear Equivalence

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. The image of the unit submodule $1 \subseteq A$ under the canonical linear equivalence $\text{op} : A \simeq A^\text{op}$ is equal to the unit submodule $1 \subseteq A^\text{op}$. In other words, if $1_A = R \cdot 1_A$ is the $R$-linear span of the multiplicative identity in $A$, then $\text{op}(1_A) = 1_{A^\text{op}}$, where $1_{A^\text{op}}$ is the $R$-linear span of the multiplicative identity in $A^\text{op}$.

Submodule.comap_op_one theorem

: comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R Aᵐᵒᵖ) = 1

Full source

@[simp]
theorem comap_op_one :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R Aᵐᵒᵖ) = 1 := by
  ext
  simp

Pullback of Unit Submodule via Opposite Algebra Equivalence

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. The pullback of the unit submodule $1 \subseteq A^\text{op}$ along the canonical linear equivalence $\text{op} : A \to A^\text{op}$ is equal to the unit submodule $1 \subseteq A$. In other words, $\text{comap}(\text{op}, 1_{A^\text{op}}) = 1_A$, where: - $\text{op} : A \to A^\text{op}$ is the canonical linear equivalence to the multiplicative opposite algebra - $1_{A^\text{op}} = R \cdot 1_{A^\text{op}}$ is the unit submodule of $A^\text{op}$ - $1_A = R \cdot 1_A$ is the unit submodule of $A$

Submodule.map_unop_one theorem

: map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R Aᵐᵒᵖ) = 1

Full source

@[simp]
theorem map_unop_one :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) (1 : Submodule R Aᵐᵒᵖ) = 1 := by
  rw [← comap_equiv_eq_map_symm, comap_op_one]

Preservation of Unit Submodule under Inverse Opposite Linear Equivalence

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. The image of the unit submodule $1 \subseteq A^\text{op}$ under the inverse of the canonical linear equivalence $\text{op} : A \simeq A^\text{op}$ is equal to the unit submodule $1 \subseteq A$. In other words, $\text{unop}(1_{A^\text{op}}) = 1_A$, where: - $\text{unop} : A^\text{op} \to A$ is the inverse of the canonical linear equivalence - $1_{A^\text{op}} = R \cdot 1_{A^\text{op}}$ is the unit submodule of $A^\text{op}$ - $1_A = R \cdot 1_A$ is the unit submodule of $A$

Submodule.comap_unop_one theorem

: comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R A) = 1

Full source

@[simp]
theorem comap_unop_one :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) (1 : Submodule R A) = 1 := by
  rw [← map_equiv_eq_comap_symm, map_op_one]

Pullback of Unit Submodule via Opposite Algebra Equivalence: $\text{op}^{-1}(1_A) = 1_{A^\text{op}}$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. The pullback of the unit submodule $1 \subseteq A$ under the inverse of the canonical linear equivalence $\text{op} : A \simeq A^\text{op}$ is equal to the unit submodule $1 \subseteq A^\text{op}$. In other words, if $1_A = R \cdot 1_A$ is the $R$-linear span of the multiplicative identity in $A$, then $\text{op}^{-1}(1_A) = 1_{A^\text{op}}$, where $1_{A^\text{op}}$ is the $R$-linear span of the multiplicative identity in $A^\text{op}$.

Submodule.mul_eq_map₂ theorem

: M * N = map₂ (LinearMap.mul R A) M N

Full source

theorem mul_eq_map₂ : M * N = map₂ (LinearMap.mul R A) M N :=
  le_antisymm (mul_le.mpr fun _m hm _n ↦ apply_mem_map₂ _ hm)
    (map₂_le.mpr fun _m hm _n ↦ mul_mem_mul hm)

Submodule Product as Bilinear Map Image: $M \cdot N = \text{map}_2(\cdot, M, N)$

Informal description

For any submodules $M$ and $N$ of an $R$-algebra $A$, the product submodule $M \cdot N$ is equal to the image of $M$ and $N$ under the bilinear multiplication map $\text{map}_2(\cdot, M, N)$, where $\cdot$ denotes the multiplication operation in $A$.

Submodule.span_mul_span theorem

: span R S * span R T = span R (S * T)

Full source

theorem span_mul_span : span R S * span R T = span R (S * T) := by
  rw [mul_eq_map₂]; apply map₂_span_span

Span of Product Sets Equals Product of Spans in Submodules

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any subsets $S, T \subseteq A$, the product of the submodules $\operatorname{span}_R S$ and $\operatorname{span}_R T$ equals the span of their pointwise product set $S \cdot T = \{s \cdot t \mid s \in S, t \in T\}$. In other words: \[ (\operatorname{span}_R S) \cdot (\operatorname{span}_R T) = \operatorname{span}_R (S \cdot T). \]

Submodule.mul_def theorem

: M * N = span R (M * N : Set A)

Full source

lemma mul_def : M * N = span R (M * N : Set A) := by simp [← span_mul_span]

Submodule product equals span of pointwise product

Informal description

For any submodules $M$ and $N$ of an $R$-algebra $A$, the product submodule $M \cdot N$ is equal to the $R$-linear span of the pointwise product set $\{m \cdot n \mid m \in M, n \in N\}$.

Submodule.mul_one theorem

: M * 1 = M

Full source

protected theorem mul_one : M * 1 = M := by
  conv_lhs => rw [one_eq_span, ← span_eq M]
  rw [span_mul_span]
  simp

Right Identity Property for Submodule Multiplication: $M \cdot 1 = M$

Informal description

For any submodule $M$ of an $R$-algebra $A$, the product of $M$ with the unit submodule $1$ (which is the $R$-linear span of the multiplicative identity $1_A$) equals $M$ itself, i.e., $M \cdot 1 = M$.

Submodule.map_mul theorem

 {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
  map f.toLinearMap (M * N) = map f.toLinearMap M * map f.toLinearMap N

Full source

protected theorem map_mul {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
    map f.toLinearMap (M * N) = map f.toLinearMap M * map f.toLinearMap N :=
  calc
    map f.toLinearMap (M * N) = ⨆ i : M, (N.map (LinearMap.mul R A i)).map f.toLinearMap := by
      rw [mul_eq_map₂]; apply map_iSup
    _ = map f.toLinearMap M * map f.toLinearMap N := by
      rw [mul_eq_map₂]
      apply congr_arg sSup
      ext S
      constructor <;> rintro ⟨y, hy⟩
      · use ⟨f y, mem_map.mpr ⟨y.1, y.2, rfl⟩⟩
        refine Eq.trans ?_ hy
        ext
        simp
      · obtain ⟨y', hy', fy_eq⟩ := mem_map.mp y.2
        use ⟨y', hy'⟩
        refine Eq.trans ?_ hy
        rw [f.toLinearMap_apply] at fy_eq
        ext
        simp [fy_eq]

Image of Submodule Product under Algebra Homomorphism: $f(M \cdot N) = f(M) \cdot f(N)$

Informal description

Let $R$ be a commutative semiring, and let $A$ and $A'$ be $R$-algebras. For any $R$-algebra homomorphism $f \colon A \to A'$ and submodules $M, N \subseteq A$, the image of the product submodule $M \cdot N$ under the linear map associated to $f$ equals the product of the images of $M$ and $N$ under $f$. That is, \[ f(M \cdot N) = f(M) \cdot f(N). \]

Submodule.map_op_mul theorem

 :
  map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M

Full source

theorem map_op_mul :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) N *
        map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M := by
  apply le_antisymm
  · simp_rw [map_le_iff_le_comap]
    refine mul_le.2 fun m hm n hn => ?_
    rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]
    show opop n * op m ∈ _
    exact mul_mem_mul hn hm
  · refine mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)
    rw [Submodule.mem_map_equiv] at hm hn ⊢
    exact mul_mem_mul hn hm

Image of Submodule Product under Opposite Algebra Equivalence: $\text{op}(M \cdot N) = \text{op}(N) \cdot \text{op}(M)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any submodules $M, N \subseteq A$, the image of the product submodule $M \cdot N$ under the linear equivalence $\text{op} : A \to A^\text{op}$ (which reverses multiplication) equals the product of the images of $N$ and $M$ under $\text{op}$ in the opposite algebra $A^\text{op}$. That is, $$\text{op}(M \cdot N) = \text{op}(N) \cdot \text{op}(M)$$ where multiplication on the right side is performed in $A^\text{op}$.

Submodule.comap_unop_mul theorem

 :
  comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) N *
      comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M

Full source

theorem comap_unop_mul :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) (M * N) =
      comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) N *
        comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) M := by
  simp_rw [← map_equiv_eq_comap_symm, map_op_mul]

Preimage of Submodule Product under Opposite Algebra Equivalence: $\text{op}^{-1}(M \cdot N) = \text{op}^{-1}(N) \cdot \text{op}^{-1}(M)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any submodules $M, N \subseteq A$, the preimage of the product submodule $M \cdot N$ under the inverse of the linear equivalence $\text{op} : A \to A^\text{op}$ (which reverses multiplication) equals the product of the preimages of $N$ and $M$ under $\text{op}^{-1}$ in the opposite algebra $A^\text{op}$. That is, $$\text{op}^{-1}(M \cdot N) = \text{op}^{-1}(N) \cdot \text{op}^{-1}(M)$$ where multiplication on the right side is performed in $A^\text{op}$.

Submodule.map_unop_mul theorem

 (M N : Submodule R Aᵐᵒᵖ) :
  map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) N *
      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M

Full source

theorem map_unop_mul (M N : Submodule R Aᵐᵒᵖ) :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) (M * N) =
      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) N *
        map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) M :=
  have : Function.Injective (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) :=
    LinearEquiv.injective _
  map_injective_of_injective this <| by
    rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]

Image of Opposite Submodule Product under Unopposite Equivalence: $\text{unop}(M \cdot N) = \text{unop}(N) \cdot \text{unop}(M)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any submodules $M, N$ of the multiplicative opposite algebra $A^\text{op}$, the image of the product submodule $M \cdot N$ under the inverse of the opposite algebra linear equivalence $\text{unop} : A^\text{op} \to A$ equals the product of the images of $N$ and $M$ under $\text{unop}$ in the original algebra $A$. That is, $$\text{unop}(M \cdot N) = \text{unop}(N) \cdot \text{unop}(M)$$ where multiplication on the right side is performed in $A$.

Submodule.comap_op_mul theorem

 (M N : Submodule R Aᵐᵒᵖ) :
  comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) N *
      comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M

Full source

theorem comap_op_mul (M N : Submodule R Aᵐᵒᵖ) :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
      comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) N *
        comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M := by
  simp_rw [comap_equiv_eq_map_symm, map_unop_mul]

Preimage of Opposite Submodule Product under Opposite Equivalence: $\text{op}^{-1}(M \cdot N) = \text{op}^{-1}(N) \cdot \text{op}^{-1}(M)$

Informal description

Let $R$ be a commutative semiring and $A$ be an $R$-algebra. For any submodules $M, N$ of the multiplicative opposite algebra $A^\text{op}$, the preimage of the product submodule $M \cdot N$ under the linear equivalence $\text{op} : A \to A^\text{op}$ equals the product of the preimages of $N$ and $M$ under $\text{op}$ in the original algebra $A$. That is, $$\text{op}^{-1}(M \cdot N) = \text{op}^{-1}(N) \cdot \text{op}^{-1}(M)$$ where multiplication on the right side is performed in $A$.

Submodule.instIsScalarTower instance

[IsScalarTower α A A] : IsScalarTower α (Submodule R A) (Submodule R A)

Full source

instance [IsScalarTower α A A] : IsScalarTower α (Submodule R A) (Submodule R A) where
  smul_assoc a S T := by
    rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]

Tower Property for Scalar Multiplication on Submodules

Informal description

For any type $\alpha$ and $R$-algebra $A$ where $\alpha$ acts on $A$ through scalar multiplication, if the scalar multiplication satisfies the tower property (i.e., $a \cdot (b \cdot x) = (a \cdot b) \cdot x$ for all $a, b \in \alpha$ and $x \in A$), then the submodules of $A$ also satisfy the tower property with respect to the induced scalar multiplication. Specifically, for any submodules $M, N \subseteq A$, the scalar multiplication satisfies $a \cdot (M \cdot N) = (a \cdot M) \cdot N$.

Submodule.instSMulCommClass instance

[SMulCommClass α A A] : SMulCommClass α (Submodule R A) (Submodule R A)

Full source

instance [SMulCommClass α A A] : SMulCommClass α (Submodule R A) (Submodule R A) where
  smul_comm a S T := by
    rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, mul_smul_comm]

Commutativity of Scalar Multiplication and Submodule Multiplication

Informal description

For a commutative semiring $R$, an $R$-algebra $A$, and a type $\alpha$ with a scalar multiplication action on $A$ that commutes with the multiplication in $A$ (i.e., $[\text{SMulCommClass } \alpha A A]$), the scalar multiplication by $\alpha$ on the submodules of $A$ commutes with the multiplication of submodules. In other words, for any $a \in \alpha$ and submodules $M, N \subseteq A$, we have $a \bullet (M * N) = (a \bullet M) * N = M * (a \bullet N)$.

Submodule.instSMulCommClass_1 instance

[SMulCommClass A α A] : SMulCommClass (Submodule R A) α (Submodule R A)

Full source

instance [SMulCommClass A α A] : SMulCommClass (Submodule R A) α (Submodule R A) :=
  have := SMulCommClass.symm A α A; .symm ..

Commutativity of Submodule Multiplication with Scalar Action

Informal description

For a commutative semiring $R$, an $R$-algebra $A$, and a type $\alpha$ with a scalar multiplication action on $A$ that commutes with the multiplication in $A$ (i.e., $[\text{SMulCommClass } A \alpha A]$), the scalar multiplication by $\alpha$ on the submodules of $A$ commutes with the multiplication of submodules. In other words, for any submodule $M \subseteq A$ and $a \in \alpha$, we have $M \cdot (a \bullet N) = a \bullet (M \cdot N)$ for any submodule $N \subseteq A$.

Submodule.hasDistribPointwiseNeg definition

{A} [Ring A] [Algebra R A] : HasDistribNeg (Submodule R A)

Full source

/-- `Submodule.pointwiseNeg` distributes over multiplication.

This is available as an instance in the `Pointwise` locale. -/
protected def hasDistribPointwiseNeg {A} [Ring A] [Algebra R A] : HasDistribNeg (Submodule R A) :=
  toAddSubmonoid_injective.hasDistribNeg _ neg_toAddSubmonoid mul_toAddSubmonoid

Distributivity of negation over multiplication in submodules

Informal description

For a ring $A$ that is an algebra over a commutative ring $R$, the negation operation on submodules of $A$ distributes over their multiplication. That is, for any submodules $M$ and $N$ of $A$, we have: 1. $- (M * N) = (-M) * N$ 2. $- (M * N) = M * (-N)$ where $M * N$ denotes the submodule generated by all products $m * n$ for $m \in M$ and $n \in N$.

Submodule.mem_span_mul_finite_of_mem_span_mul theorem

 {R A} [Semiring R] [AddCommMonoid A] [Mul A] [Module R A] {S : Set A} {S' : Set A} {x : A} (hx : x ∈ span R (S * S')) :
  ∃ T T' : Finset A, ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (T * T' : Set A)

Full source

theorem mem_span_mul_finite_of_mem_span_mul {R A} [Semiring R] [AddCommMonoid A] [Mul A]
    [Module R A] {S : Set A} {S' : Set A} {x : A} (hx : x ∈ span R (S * S')) :
    ∃ T T' : Finset A, ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (T * T' : Set A) := by
  classical
  obtain ⟨U, h, hU⟩ := mem_span_finite_of_mem_span hx
  obtain ⟨T, T', hS, hS', h⟩ := Finset.subset_mul h
  use T, T', hS, hS'
  have h' : (U : Set A) ⊆ T * T' := by assumption_mod_cast
  have h'' := span_mono h' hU
  assumption

Finite generation property for elements in the span of a product of subsets in an algebra

Informal description

Let $R$ be a semiring and $A$ be an $R$-algebra with multiplication. For any subsets $S, S' \subseteq A$ and any element $x \in \operatorname{span}_R (S * S')$, where $S * S' = \{s \cdot s' \mid s \in S, s' \in S'\}$, there exist finite subsets $T \subseteq S$ and $T' \subseteq S'$ such that $x \in \operatorname{span}_R (T * T')$.

Submodule.mul_eq_span_mul_set theorem

(s t : Submodule R A) : s * t = span R ((s : Set A) * (t : Set A))

Full source

theorem mul_eq_span_mul_set (s t : Submodule R A) : s * t = span R ((s : Set A) * (t : Set A)) := by
  rw [mul_eq_map₂]; exact map₂_eq_span_image2 _ s t

Product of Submodules as Span of Pointwise Product Set

Informal description

For any two submodules $s$ and $t$ of an $R$-algebra $A$, the product submodule $s \cdot t$ is equal to the $R$-linear span of the pointwise product set $\{x \cdot y \mid x \in s, y \in t\}$.

Submodule.mem_span_mul_finite_of_mem_mul theorem

 {P Q : Submodule R A} {x : A} (hx : x ∈ P * Q) :
  ∃ T T' : Finset A, (T : Set A) ⊆ P ∧ (T' : Set A) ⊆ Q ∧ x ∈ span R (T * T' : Set A)

Full source

theorem mem_span_mul_finite_of_mem_mul {P Q : Submodule R A} {x : A} (hx : x ∈ P * Q) :
    ∃ T T' : Finset A, (T : Set A) ⊆ P ∧ (T' : Set A) ⊆ Q ∧ x ∈ span R (T * T' : Set A) :=
  Submodule.mem_span_mul_finite_of_mem_span_mul
    (by rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx)

Finite generation property for elements in the product of submodules

Informal description

Let $R$ be a semiring and $A$ an $R$-algebra. For any submodules $P, Q$ of $A$ and any element $x \in P \cdot Q$, there exist finite subsets $T \subseteq P$ and $T' \subseteq Q$ such that $x$ belongs to the $R$-linear span of the pointwise product set $T \cdot T' = \{t \cdot t' \mid t \in T, t' \in T'\}$.

Submodule.mem_span_singleton_mul theorem

{x y : A} : x ∈ span R { y } * P ↔ ∃ z ∈ P, y * z = x

Full source

theorem mem_span_singleton_mul {x y : A} : x ∈ span R {y} * Px ∈ span R {y} * P ↔ ∃ z ∈ P, y * z = x := by
  simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map, mem_map, LinearMap.mul_apply_apply]

Characterization of Elements in the Product of a Span and a Submodule: $x \in \langle y \rangle \cdot P \leftrightarrow \exists z \in P, y \cdot z = x$

Informal description

For any elements $x, y$ in an $R$-algebra $A$ and a submodule $P$ of $A$, the element $x$ belongs to the product of the span of $\{y\}$ and $P$ if and only if there exists an element $z \in P$ such that $y \cdot z = x$.

Submodule.mem_mul_span_singleton theorem

{x y : A} : x ∈ P * span R { y } ↔ ∃ z ∈ P, z * y = x

Full source

theorem mem_mul_span_singleton {x y : A} : x ∈ P * span R {y}x ∈ P * span R {y} ↔ ∃ z ∈ P, z * y = x := by
  simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map_flip, mem_map, LinearMap.flip_apply,
    LinearMap.mul_apply_apply]

Characterization of elements in $P \cdot \langle y \rangle$ via factorization

Informal description

For any elements $x, y$ in an $R$-algebra $A$ and a submodule $P$ of $A$, the element $x$ belongs to the product submodule $P \cdot \operatorname{span}_R \{y\}$ if and only if there exists an element $z \in P$ such that $z \cdot y = x$.

Submodule.span_singleton_mul theorem

{x : A} {p : Submodule R A} : Submodule.span R { x } * p = x • p

Full source

lemma span_singleton_mul {x : A} {p : Submodule R A} :
    Submodule.span R {x} * p = x • p := ext fun _ ↦ mem_span_singleton_mul

Span-Submodule Product Equals Scalar Multiplication: $\langle x \rangle \cdot p = x \bullet p$

Informal description

For any element $x$ in an $R$-algebra $A$ and any submodule $p$ of $A$, the product of the span of $\{x\}$ with $p$ is equal to the scalar multiplication of $x$ with $p$, i.e., $\langle x \rangle \cdot p = x \bullet p$.

Submodule.mem_smul_iff_inv_mul_mem theorem

 {S} [DivisionSemiring S] [Algebra R S] {x : S} {p : Submodule R S} {y : S} (hx : x ≠ 0) : y ∈ x • p ↔ x⁻¹ * y ∈ p

Full source

lemma mem_smul_iff_inv_mul_mem {S} [DivisionSemiring S] [Algebra R S] {x : S} {p : Submodule R S}
    {y : S} (hx : x ≠ 0) : y ∈ x • py ∈ x • p ↔ x⁻¹ * y ∈ p := by
  constructor
  · rintro ⟨a, ha : a ∈ p, rfl⟩; simpa [inv_mul_cancel_left₀ hx]
  · exact fun h ↦ ⟨_, h, by simp [mul_inv_cancel_left₀ hx]⟩

Characterization of Scalar Multiplication by Invertible Elements in Submodules over Division Semirings

Informal description

Let $S$ be a division semiring with an $R$-algebra structure, and let $p$ be a submodule of $S$ over $R$. For any nonzero element $x \in S$ and any element $y \in S$, we have $y \in x \bullet p$ if and only if $x^{-1} \cdot y \in p$.

Submodule.mul_mem_smul_iff theorem

 {S} [CommRing S] [Algebra R S] {x : S} {p : Submodule R S} {y : S} (hx : x ∈ nonZeroDivisors S) : x * y ∈ x • p ↔ y ∈ p

Full source

lemma mul_mem_smul_iff {S} [CommRing S] [Algebra R S] {x : S} {p : Submodule R S} {y : S}
    (hx : x ∈ nonZeroDivisors S) :
    x * y ∈ x • px * y ∈ x • p ↔ y ∈ p := by
  simp [mem_smul_pointwise_iff_exists, mul_cancel_left_mem_nonZeroDivisors hx]

Characterization of Scalar Multiplication by Non-zero-divisors in Submodules over Commutative Rings

Informal description

Let $S$ be a commutative ring with an $R$-algebra structure, and let $p$ be a submodule of $S$ over $R$. For any element $x \in S$ that is a non-zero-divisor and any element $y \in S$, we have $x \cdot y \in x \bullet p$ if and only if $y \in p$.

Submodule.mul_smul_mul_eq_smul_mul_smul theorem

(x y : R) : (x * y) • (M * N) = (x • M) * (y • N)

Full source

theorem mul_smul_mul_eq_smul_mul_smul (x y : R) : (x * y) • (M * N) = (x • M) * (y • N) := by
  ext
  refine ⟨?_, fun hx ↦ Submodule.mul_induction_on hx ?_ fun _ _ hx hy ↦ Submodule.add_mem _ hx hy⟩
  · rintro ⟨_, hx, rfl⟩
    rw [DistribMulAction.toLinearMap_apply]
    refine Submodule.mul_induction_on hx (fun m hm n hn ↦ ?_) (fun _ _ hn hm ↦ ?_)
    · rw [mul_smul_mul_comm]
      exact mul_mem_mul (smul_mem_pointwise_smul m x M hm) (smul_mem_pointwise_smul n y N hn)
    · rw [smul_add]
      exact Submodule.add_mem _ hn hm
  · rintro _ ⟨m, hm, rfl⟩ _ ⟨n, hn, rfl⟩
    simp_rw [DistribMulAction.toLinearMap_apply, smul_mul_smul_comm]
    exact smul_mem_pointwise_smul _ _ _ (mul_mem_mul hm hn)

Compatibility of Scalar Multiplication with Submodule Multiplication: $(x \cdot y) \bullet (M \cdot N) = (x \bullet M) \cdot (y \bullet N)$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any elements $x, y \in R$ and submodules $M, N \subseteq A$, the following equality holds: $$(x \cdot y) \bullet (M \cdot N) = (x \bullet M) \cdot (y \bullet N)$$ where $\bullet$ denotes scalar multiplication and $\cdot$ denotes both ring multiplication and submodule multiplication.

Submodule.idemSemiring instance

: IdemSemiring (Submodule R A)

Full source

/-- Sub-R-modules of an R-algebra form an idempotent semiring. -/
instance idemSemiring : IdemSemiring (Submodule R A) where
  __ := instNonUnitalSemiring
  one_mul := Submodule.one_mul
  mul_one := Submodule.mul_one
  bot_le _ := bot_le

Submodules of an Algebra Form an Idempotent Semiring

Informal description

For any commutative semiring $R$ and $R$-algebra $A$, the collection of submodules $\text{Submodule } R A$ forms an idempotent semiring under the operations of addition (supremum of submodules) and multiplication (product of submodules). Specifically: 1. The addition operation is associative, commutative, and idempotent (i.e., $M + M = M$ for any submodule $M$). 2. The multiplication operation is associative and distributes over addition. 3. The zero submodule is the additive identity, and the submodule $R \cdot 1_A$ is the multiplicative identity. 4. The partial order defined by $M \leq N$ if and only if $M + N = N$ coincides with the inclusion order of submodules.

Submodule.span_pow theorem

(s : Set A) : ∀ n : ℕ, span R s ^ n = span R (s ^ n)

Full source

theorem span_pow (s : Set A) : ∀ n : ℕ, span R s ^ n = span R (s ^ n)
  | 0 => by rw [pow_zero, pow_zero, one_eq_span_one_set]
  | n + 1 => by rw [pow_succ, pow_succ, span_pow s n, span_mul_span]

Span-Power Equality for Submodules: $(\operatorname{span}_R s)^n = \operatorname{span}_R (s^n)$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any subset $s \subseteq A$ and natural number $n$, the $n$-th power of the submodule $\operatorname{span}_R s$ is equal to the span of the $n$-th pointwise power of $s$. That is: \[ (\operatorname{span}_R s)^n = \operatorname{span}_R (s^n) \] where $s^n$ denotes the set $\{x_1 \cdots x_n \mid x_i \in s\}$ of all $n$-fold products of elements from $s$.

Submodule.pow_eq_span_pow_set theorem

(n : ℕ) : M ^ n = span R ((M : Set A) ^ n)

Full source

theorem pow_eq_span_pow_set (n : ℕ) : M ^ n = span R ((M : Set A) ^ n) := by
  rw [← span_pow, span_eq]

Submodule Power Equals Span of Pointwise Power: $M^n = \operatorname{span}_R (M^n)$

Informal description

For any natural number $n$ and any submodule $M$ of an $R$-algebra $A$, the $n$-th power of $M$ is equal to the span of the $n$-th pointwise power of $M$ as a subset of $A$. That is, \[ M^n = \operatorname{span}_R (M^n), \] where $M^n$ on the right denotes the set $\{x_1 \cdots x_n \mid x_i \in M\}$ of all $n$-fold products of elements from $M$.

Submodule.pow_induction_on_left' theorem

 {C : ∀ (n : ℕ) (x), x ∈ M ^ n → Prop} (algebraMap : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
  (add : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
  (mem_mul : ∀ m (hm : m ∈ M), ∀ (i x hx), C i x hx → C i.succ (m * x) ((pow_succ' M i).symm ▸ (mul_mem_mul hm hx)))
  {n : ℕ} {x : A} (hx : x ∈ M ^ n) : C n x hx

Full source

/-- Dependent version of `Submodule.pow_induction_on_left`. -/
@[elab_as_elim]
protected theorem pow_induction_on_left' {C : ∀ (n : ℕ) (x), x ∈ M ^ n → Prop}
    (algebraMap : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
    (add : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
    (mem_mul : ∀ m (hm : m ∈ M), ∀ (i x hx), C i x hx → C i.succ (m * x)
      ((pow_succ' M i).symm ▸ (mul_mem_mul hm hx)))
    {n : ℕ} {x : A}
    (hx : x ∈ M ^ n) : C n x hx := by
  induction n generalizing x with
  | zero =>
    rw [pow_zero] at hx
    obtain ⟨r, rfl⟩ := mem_one.mp hx
    exact algebraMap r
  | succ n n_ih =>
    revert hx
    simp_rw [pow_succ']
    exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mem_mul _ hm _ _ _ (n_ih ih))
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

Left Induction Principle for Powers of Submodules in an Algebra

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For a submodule $M$ of $A$, consider a predicate $C(n, x)$ indexed by a natural number $n$ and an element $x \in M^n$. If: 1. For all $r \in R$, $C(0, \text{algebraMap}_R^A(r))$ holds, 2. For any $x, y \in M^i$ with $C(i, x)$ and $C(i, y)$, we have $C(i, x + y)$, and 3. For any $m \in M$ and $x \in M^i$ with $C(i, x)$, we have $C(i+1, m \cdot x)$, then for any $x \in M^n$, the predicate $C(n, x)$ holds.

Submodule.pow_induction_on_right' theorem

 {C : ∀ (n : ℕ) (x), x ∈ M ^ n → Prop} (algebraMap : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
  (add : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
  (mul_mem : ∀ i x hx, C i x hx → ∀ m (hm : m ∈ M), C i.succ (x * m) (mul_mem_mul hx hm)) {n : ℕ} {x : A}
  (hx : x ∈ M ^ n) : C n x hx

Full source

/-- Dependent version of `Submodule.pow_induction_on_right`. -/
@[elab_as_elim]
protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n → Prop}
    (algebraMap : ∀ r : R, C 0 (algebraMap _ _ r) (algebraMap_mem r))
    (add : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
    (mul_mem :
      ∀ i x hx, C i x hx →
        ∀ m (hm : m ∈ M), C i.succ (x * m) (mul_mem_mul hx hm))
    {n : ℕ} {x : A} (hx : x ∈ M ^ n) : C n x hx := by
  induction n generalizing x with
  | zero =>
    rw [pow_zero] at hx
    obtain ⟨r, rfl⟩ := mem_one.mp hx
    exact algebraMap r
  | succ n n_ih =>
    revert hx
    simp_rw [pow_succ]
    exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

Dependent Right Induction Principle for Powers of Submodules

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $M$ a submodule of $A$. Given a predicate $C(n, x)$ depending on a natural number $n$ and an element $x \in M^n$, if: 1. For any $r \in R$, $C(0, \text{algebraMap}_R^A(r))$ holds, 2. For any $x, y \in M^i$ and $i \in \mathbb{N}$, if $C(i, x)$ and $C(i, y)$ hold, then $C(i, x + y)$ holds, 3. For any $x \in M^i$ with $C(i, x)$, and any $m \in M$, $C(i+1, x \cdot m)$ holds, then for any $x \in M^n$, the predicate $C(n, x)$ holds.

Submodule.pow_induction_on_left theorem

 {C : A → Prop} (hr : ∀ r : R, C (algebraMap _ _ r)) (hadd : ∀ x y, C x → C y → C (x + y))
  (hmul : ∀ m ∈ M, ∀ (x), C x → C (m * x)) {x : A} {n : ℕ} (hx : x ∈ M ^ n) : C x

Full source

/-- To show a property on elements of `M ^ n` holds, it suffices to show that it holds for scalars,
is closed under addition, and holds for `m * x` where `m ∈ M` and it holds for `x` -/
@[elab_as_elim]
protected theorem pow_induction_on_left {C : A → Prop} (hr : ∀ r : R, C (algebraMap _ _ r))
    (hadd : ∀ x y, C x → C y → C (x + y)) (hmul : ∀ m ∈ M, ∀ (x), C x → C (m * x)) {x : A} {n : ℕ}
    (hx : x ∈ M ^ n) : C x :=
  Submodule.pow_induction_on_left' M (C := fun _ a _ => C a) hr
    (fun x y _i _hx _hy => hadd x y)
    (fun _m hm _i _x _hx => hmul _ hm _) hx

Left Induction Principle for Powers of Submodules

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $M$ a submodule of $A$. For a predicate $C$ on elements of $A$, if: 1. $C$ holds for all scalar multiples $\text{algebraMap}_R^A(r)$ where $r \in R$, 2. $C$ is closed under addition (i.e., if $C(x)$ and $C(y)$ hold, then $C(x + y)$ holds), 3. For any $m \in M$ and $x \in A$ with $C(x)$, we have $C(m \cdot x)$, then for any $x \in M^n$ (the $n$-th power of $M$ in the submodule semiring), the predicate $C(x)$ holds.

Submodule.pow_induction_on_right theorem

 {C : A → Prop} (hr : ∀ r : R, C (algebraMap _ _ r)) (hadd : ∀ x y, C x → C y → C (x + y))
  (hmul : ∀ x, C x → ∀ m ∈ M, C (x * m)) {x : A} {n : ℕ} (hx : x ∈ M ^ n) : C x

Full source

/-- To show a property on elements of `M ^ n` holds, it suffices to show that it holds for scalars,
is closed under addition, and holds for `x * m` where `m ∈ M` and it holds for `x` -/
@[elab_as_elim]
protected theorem pow_induction_on_right {C : A → Prop} (hr : ∀ r : R, C (algebraMap _ _ r))
    (hadd : ∀ x y, C x → C y → C (x + y)) (hmul : ∀ x, C x → ∀ m ∈ M, C (x * m)) {x : A} {n : ℕ}
    (hx : x ∈ M ^ n) : C x :=
  Submodule.pow_induction_on_right' (M := M) (C := fun _ a _ => C a) hr
    (fun x y _i _hx _hy => hadd x y)
    (fun _i _x _hx => hmul _) hx

Right Induction Principle for Powers of Submodules

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $M$ a submodule of $A$. Given a predicate $C$ on elements of $A$, if: 1. $C$ holds for all scalar multiples $\text{algebraMap}_R^A(r)$ where $r \in R$, 2. $C$ is closed under addition (i.e., if $C(x)$ and $C(y)$ hold, then $C(x + y)$ holds), 3. For any $x$ satisfying $C(x)$ and any $m \in M$, $C(x \cdot m)$ holds, then for any natural number $n$ and any $x \in M^n$, the predicate $C(x)$ holds.

Submodule.mapHom definition

{A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') : Submodule R A →+* Submodule R A'

Full source

/-- `Submonoid.map` as a `RingHom`, when applied to an `AlgHom`. -/
@[simps]
def mapHom {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
    SubmoduleSubmodule R A →+* Submodule R A' where
  toFun := map f.toLinearMap
  map_zero' := Submodule.map_bot _
  map_add' := (Submodule.map_sup · · _)
  map_one' := Submodule.map_one _
  map_mul' := (Submodule.map_mul · · _)

Semiring homomorphism induced by algebra homomorphism on submodules

Informal description

Given a commutative semiring $R$ and $R$-algebras $A$ and $A'$, for any $R$-algebra homomorphism $f \colon A \to A'$, the function $\text{mapHom}(f)$ is a semiring homomorphism from the semiring of submodules of $A$ to the semiring of submodules of $A'$. It maps a submodule $M \subseteq A$ to its image under the linear map associated to $f$, and satisfies: 1. $\text{mapHom}(f)(0) = 0$ (preservation of zero submodule) 2. $\text{mapHom}(f)(M + N) = \text{mapHom}(f)(M) + \text{mapHom}(f)(N)$ (preservation of addition) 3. $\text{mapHom}(f)(1) = 1$ (preservation of unit submodule) 4. $\text{mapHom}(f)(M \cdot N) = \text{mapHom}(f)(M) \cdot \text{mapHom}(f)(N)$ (preservation of multiplication)

Submodule.mapHom_id theorem

: mapHom (.id R A) = .id _

Full source

theorem mapHom_id : mapHom (.id R A) = .id _ := RingHom.ext map_id

Identity Algebra Homomorphism Induces Identity Semiring Homomorphism on Submodules

Informal description

The semiring homomorphism induced by the identity algebra homomorphism on submodules is equal to the identity semiring homomorphism. That is, for any commutative semiring $R$ and $R$-algebra $A$, we have $\text{mapHom}(\text{id}_A) = \text{id}_{\text{Submodule } R A}$.

Submodule.equivOpposite definition

: Submodule R Aᵐᵒᵖ ≃+* (Submodule R A)ᵐᵒᵖ

Full source

/-- The ring of submodules of the opposite algebra is isomorphic to the opposite ring of
submodules. -/
@[simps apply symm_apply]
def equivOpposite : SubmoduleSubmodule R Aᵐᵒᵖ ≃+* (Submodule R A)ᵐᵒᵖ where
  toFun p := op <| p.comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ)
  invFun p := p.unop.comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A)
  left_inv _ := SetLike.coe_injective <| rfl
  right_inv _ := unop_injective <| SetLike.coe_injective rfl
  map_add' p q := by simp [comap_equiv_eq_map_symm, ← op_add]
  map_mul' _ _ := congr_arg op <| comap_op_mul _ _

Ring isomorphism between submodules of opposite algebra and opposite ring of submodules

Informal description

The function establishes a ring isomorphism between the ring of submodules of the opposite algebra $A^\text{op}$ and the opposite ring of submodules of $A$. Specifically, it maps a submodule $p$ of $A^\text{op}$ to the submodule $\text{op}(p \cap A)$ of $A^\text{op}$, and its inverse maps a submodule $q$ of $A^\text{op}$ to the submodule $q \cap A$ of $A$.

Submodule.map_pow theorem

{A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (n : ℕ) : map f.toLinearMap (M ^ n) = map f.toLinearMap M ^ n

Full source

protected theorem map_pow {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (n : ℕ) :
    map f.toLinearMap (M ^ n) = map f.toLinearMap M ^ n :=
  map_pow (mapHom f) M n

Power Preservation under Algebra Homomorphism Images of Submodules

Informal description

Let $R$ be a commutative semiring, $A$ and $A'$ be $R$-algebras, and $f \colon A \to A'$ be an $R$-algebra homomorphism. For any submodule $M$ of $A$ and any natural number $n$, the image of the $n$-th power of $M$ under the linear map associated to $f$ equals the $n$-th power of the image of $M$ under the same linear map, i.e., \[ f(M^n) = (f(M))^n. \]

Submodule.comap_unop_pow theorem

 (n : ℕ) :
  comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M ^ n

Full source

theorem comap_unop_pow (n : ℕ) :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) (M ^ n) =
      comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) M ^ n :=
  (equivOpposite : SubmoduleSubmodule R Aᵐᵒᵖ ≃+* _).symm.map_pow (op M) n

Pullback of Submodule Powers under Opposite Algebra Equivalence

Informal description

For any natural number $n$ and any submodule $M$ of the $R$-algebra $A$, the pullback of the $n$-th power of $M$ under the canonical linear equivalence between $A$ and its multiplicative opposite $A^\text{op}$ is equal to the $n$-th power of the pullback of $M$ under the same equivalence. More precisely, if $\text{op} : A \simeq_{R} A^\text{op}$ is the canonical linear equivalence, then: \[ \text{comap}(\text{op}^{-1}, M^n) = (\text{comap}(\text{op}^{-1}, M))^n \]

Submodule.comap_op_pow theorem

 (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
  comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) =
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n

Full source

theorem comap_op_pow (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) =
      comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n :=
  op_injective <| (equivOpposite : SubmoduleSubmodule R Aᵐᵒᵖ ≃+* _).map_pow M n

Pullback of Powers in Opposite Algebra Submodules via Linear Equivalence

Informal description

For any natural number $n$ and any submodule $M$ of the opposite algebra $A^\text{op}$ over a commutative semiring $R$, the pullback of the $n$-th power of $M$ along the canonical linear equivalence $\text{op} : A \to A^\text{op}$ is equal to the $n$-th power of the pullback of $M$ along the same equivalence. In other words, if $\text{op} : A \to A^\text{op}$ denotes the canonical linear equivalence, then: \[ \text{comap}(\text{op}, M^n) = (\text{comap}(\text{op}, M))^n \]

Submodule.map_op_pow theorem

 (n : ℕ) :
  map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) =
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n

Full source

theorem map_op_pow (n : ℕ) :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) =
      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M ^ n := by
  rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]

Image of Submodule Powers under Opposite Algebra Equivalence

Informal description

For any natural number $n$ and any submodule $M$ of an $R$-algebra $A$, the image of the $n$-th power of $M$ under the canonical linear equivalence $\text{op} : A \to A^\text{op}$ is equal to the $n$-th power of the image of $M$ under the same equivalence. In other words, if $\text{op} : A \simeq_{R} A^\text{op}$ denotes the canonical linear equivalence, then: \[ \text{map}(\text{op}, M^n) = (\text{map}(\text{op}, M))^n \]

Submodule.map_unop_pow theorem

 (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
  map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M ^ n

Full source

theorem map_unop_pow (n : ℕ) (M : Submodule R Aᵐᵒᵖ) :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) (M ^ n) =
      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : AᵐᵒᵖAᵐᵒᵖ →ₗ[R] A) M ^ n := by
  rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]

Pushforward-Power Commutation for Opposite Algebra Submodules via Linear Equivalence

Informal description

For any natural number $n$ and any submodule $M$ of the opposite algebra $A^\text{op}$ over a commutative semiring $R$, the pushforward of the $n$-th power of $M$ along the inverse of the canonical linear equivalence $\text{op} : A \to A^\text{op}$ is equal to the $n$-th power of the pushforward of $M$ along the same inverse equivalence. In other words, if $\text{op}^{-1} : A^\text{op} \to A$ denotes the inverse of the canonical linear equivalence, then: \[ \text{map}(\text{op}^{-1}, M^n) = (\text{map}(\text{op}^{-1}, M))^n \]

Submodule.span.ringHom definition

: SetSemiring A →+* Submodule R A

Full source

/-- `span` is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets
on either side). -/
@[simps]
def span.ringHom : SetSemiringSetSemiring A →+* Submodule R A where
  toFun s := Submodule.span R (SetSemiring.down s)
  map_zero' := span_empty
  map_one' := one_eq_span.symm
  map_add' := span_union
  map_mul' s t := by simp_rw [SetSemiring.down_mul, span_mul_span]

Span as a semiring homomorphism from sets to submodules

Informal description

The function $\text{span}$ is a semiring homomorphism from the semiring of sets $\text{SetSemiring}\,A$ to the semiring of submodules $\text{Submodule}\,R\,A$, where: - The zero element is mapped to the zero submodule. - The multiplicative identity is mapped to the submodule generated by the multiplicative identity of $A$. - Addition (set union) is preserved, mapping to the span of the union. - Multiplication (pointwise product) is preserved, mapping to the span of the product of spans.

Submodule.pointwiseMulSemiringAction definition

: MulSemiringAction α (Submodule R A)

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`. -/
protected def pointwiseMulSemiringAction : MulSemiringAction α (Submodule R A) where
  __ := Submodule.pointwiseDistribMulAction
  smul_mul r x y := Submodule.map_mul x y <| MulSemiringAction.toAlgHom R A r
  smul_one r := Submodule.map_one <| MulSemiringAction.toAlgHom R A r

Multiplicative semiring action on submodules of an algebra

Informal description

Given a commutative semiring $R$, an $R$-algebra $A$, and a monoid $\alpha$ acting as a multiplicative semiring action on $A$, the structure `Submodule.pointwiseMulSemiringAction` defines a multiplicative semiring action of $\alpha$ on the submodules of $A$. For any $a \in \alpha$ and submodule $S \subseteq A$, the action $a \bullet S$ is defined as the image of $S$ under the algebra homomorphism induced by the action of $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 (S_1 \cdot S_2) = (a \bullet S_1) \cdot (a \bullet S_2)$ for any submodules $S_1, S_2 \subseteq A$, 4. $a \bullet 1 = 1$ for the multiplicative identity submodule $1 \subseteq A$. This is a stronger version of `Submodule.pointwiseDistribMulAction`, as it additionally preserves the multiplicative structure of submodules.

Submodule.mul_mem_mul_rev theorem

(hm : m ∈ M) (hn : n ∈ N) : n * m ∈ M * N

Full source

theorem mul_mem_mul_rev (hm : m ∈ M) (hn : n ∈ N) : n * m ∈ M * N :=
  mul_comm m n ▸ mul_mem_mul hm hn

Reversed Product of Submodule Elements Belongs to Submodule Product

Informal description

For any elements $m \in M$ and $n \in N$ of submodules $M$ and $N$ respectively in an $R$-algebra $A$, the product $n \cdot m$ belongs to the submodule product $M \cdot N$.

Submodule.mul_comm theorem

: M * N = N * M

Full source

protected theorem mul_comm : M * N = N * M :=
  le_antisymm (mul_le.2 fun _r hrm _s hsn => mul_mem_mul_rev hsn hrm)
    (mul_le.2 fun _r hrn _s hsm => mul_mem_mul_rev hsm hrn)

Commutativity of Submodule Multiplication: $M \cdot N = N \cdot M$

Informal description

For any two submodules $M$ and $N$ of an $R$-algebra $A$, the product submodule $M \cdot N$ is equal to $N \cdot M$.

Submodule.instIdemCommSemiring instance

: IdemCommSemiring (Submodule R A)

Full source

/-- Sub-R-modules of an R-algebra A form a semiring. -/
instance : IdemCommSemiring (Submodule R A) :=
  { Submodule.idemSemiring with mul_comm := Submodule.mul_comm }

Submodules of an Algebra Form an Idempotent Commutative Semiring

Informal description

For any commutative semiring $R$ and $R$-algebra $A$, the collection of submodules $\text{Submodule } R A$ forms an idempotent commutative semiring under the operations of addition (supremum of submodules) and multiplication (product of submodules). Specifically: 1. The addition operation is associative, commutative, and idempotent (i.e., $M + M = M$ for any submodule $M$). 2. The multiplication operation is associative, commutative, and distributes over addition. 3. The zero submodule is the additive identity, and the submodule $R \cdot 1_A$ is the multiplicative identity. 4. The partial order defined by $M \leq N$ if and only if $M + N = N$ coincides with the inclusion order of submodules.

Submodule.prod_span theorem

 {ι : Type*} (s : Finset ι) (M : ι → Set A) : (∏ i ∈ s, Submodule.span R (M i)) = Submodule.span R (∏ i ∈ s, M i)

Full source

theorem prod_span {ι : Type*} (s : Finset ι) (M : ι → Set A) :
    (∏ i ∈ s, Submodule.span R (M i)) = Submodule.span R (∏ i ∈ s, M i) := by
  letI := Classical.decEq ι
  refine Finset.induction_on s ?_ ?_
  · simp [one_eq_span, Set.singleton_one]
  · intro _ _ H ih
    rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]

Product of Spans Equals Span of Product Sets in Submodules

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any finite index set $\iota$ and any family of subsets $M_i \subseteq A$ indexed by $i \in \iota$, the product of the spans $\prod_{i \in \iota} \operatorname{span}_R M_i$ equals the span of the product set $\prod_{i \in \iota} M_i$. In other words: \[ \prod_{i \in \iota} \operatorname{span}_R M_i = \operatorname{span}_R \left(\prod_{i \in \iota} M_i\right). \]

Submodule.prod_span_singleton theorem

{ι : Type*} (s : Finset ι) (x : ι → A) : (∏ i ∈ s, span R ({x i} : Set A)) = span R {∏ i ∈ s, x i}

Full source

theorem prod_span_singleton {ι : Type*} (s : Finset ι) (x : ι → A) :
    (∏ i ∈ s, span R ({x i} : Set A)) = span R {∏ i ∈ s, x i} := by
  rw [prod_span, Set.finset_prod_singleton]

Product of Singleton Spans Equals Span of Product in Submodules

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any finite index set $\iota$ and any family of elements $x_i \in A$ indexed by $i \in \iota$, the product of the spans of the singleton sets $\{x_i\}$ equals the span of the singleton set containing the product of the elements $x_i$. In other words: \[ \prod_{i \in \iota} \operatorname{span}_R \{x_i\} = \operatorname{span}_R \left\{\prod_{i \in \iota} x_i\right\}. \]

Submodule.moduleSet instance

: Module (SetSemiring A) (Submodule R A)

Full source

/-- R-submodules of the R-algebra A are a module over `Set A`. -/
instance moduleSet : Module (SetSemiring A) (Submodule R A) where
  smul s P := span R (SetSemiring.down s) * P
  smul_add _ _ _ := mul_add _ _ _
  add_smul s t P := by
    simp_rw [HSMul.hSMul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]
  mul_smul s t P := by
    simp_rw [HSMul.hSMul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]
  one_smul P := by
    simp_rw [HSMul.hSMul, SetSemiring.down_one, ← one_eq_span_one_set, one_mul]
  zero_smul P := by
    simp_rw [HSMul.hSMul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]
  smul_zero _ := mul_bot _

Module Structure on Submodules over the Semiring of Sets

Informal description

For a commutative semiring $R$ and an $R$-algebra $A$, the collection of submodules $\text{Submodule}\,R\,A$ forms a module over the semiring of sets $\text{SetSemiring}\,A$. The scalar multiplication is defined by $s \bullet P = \text{span}_R(s) \cdot P$ for any $s \in \text{SetSemiring}\,A$ and submodule $P \subseteq A$, where $\text{span}_R(s)$ is the $R$-linear span of $s$ and $\cdot$ denotes the multiplication of submodules.

Submodule.setSemiring_smul_def theorem

(s : SetSemiring A) (P : Submodule R A) : s • P = span R (SetSemiring.down (α := A) s) * P

Full source

theorem setSemiring_smul_def (s : SetSemiring A) (P : Submodule R A) :
    s • P = span R (SetSemiring.down (α := A) s) * P :=
  rfl

Definition of Scalar Multiplication on Submodules via Span and Product

Informal description

For any subset $s$ in the semiring of sets $\text{SetSemiring}\,A$ and any submodule $P$ of an $R$-algebra $A$, the scalar multiplication $s \bullet P$ is equal to the product of the $R$-linear span of $s$ (viewed as a subset of $A$) and the submodule $P$. That is, \[ s \bullet P = \text{span}_R(s) \cdot P. \]

Submodule.smul_le_smul theorem

 {s t : SetSemiring A} {M N : Submodule R A} (h₁ : SetSemiring.down (α := A) s ⊆ SetSemiring.down (α := A) t)
  (h₂ : M ≤ N) : s • M ≤ t • N

Full source

theorem smul_le_smul {s t : SetSemiring A} {M N : Submodule R A}
    (h₁ : SetSemiring.downSetSemiring.down (α := A) s ⊆ SetSemiring.down (α := A) t)
    (h₂ : M ≤ N) : s • M ≤ t • N :=
  mul_le_mul (span_mono h₁) h₂

Monotonicity of Scalar Multiplication on Submodules: $s \subseteq t$ and $M \subseteq N$ implies $s \bullet M \subseteq t \bullet N$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any subsets $s, t$ of $A$ (viewed as elements of $\text{SetSemiring}\,A$) and submodules $M, N$ of $A$, if $s \subseteq t$ and $M \subseteq N$, then the scalar product $s \bullet M$ is contained in $t \bullet N$, where $s \bullet M$ denotes the submodule $\text{span}_R(s) \cdot M$.

Submodule.singleton_smul theorem

(a : A) (M : Submodule R A) : Set.up ({ a } : Set A) • M = M.map (LinearMap.mulLeft R a)

Full source

theorem singleton_smul (a : A) (M : Submodule R A) :
    Set.up ({a} : Set A) • M = M.map (LinearMap.mulLeft R a) := by
  conv_lhs => rw [← span_eq M]
  rw [setSemiring_smul_def, SetSemiring.down_up, span_mul_span, singleton_mul]
  exact (map (LinearMap.mulLeft R a) M).span_eq

Scalar multiplication of a submodule by a singleton: $\{a\} \bullet M = a \cdot M$

Informal description

For any element $a$ in an $R$-algebra $A$ and any submodule $M$ of $A$, the scalar multiplication of the singleton set $\{a\}$ (viewed as an element of $\text{SetSemiring}\,A$) with $M$ is equal to the image of $M$ under the left multiplication map $x \mapsto a \cdot x$. That is, \[ \{a\} \bullet M = \{a \cdot x \mid x \in M\}. \]

Submodule.instDiv instance

: Div (Submodule R A)

Full source

/-- The elements of `I / J` are the `x` such that `x • J ⊆ I`.

In fact, we define `x ∈ I / J` to be `∀ y ∈ J, x * y ∈ I` (see `mem_div_iff_forall_mul_mem`),
which is equivalent to `x • J ⊆ I` (see `mem_div_iff_smul_subset`), but nicer to use in proofs.

This is the general form of the ideal quotient, traditionally written $I : J$.
-/
instance : Div (Submodule R A) :=
  ⟨fun I J =>
    { carrier := { x | ∀ y ∈ J, x * y ∈ I }
      zero_mem' := fun y _ => by
        rw [zero_mul]
        apply Submodule.zero_mem
      add_mem' := fun ha hb y hy => by
        rw [add_mul]
        exact Submodule.add_mem _ (ha _ hy) (hb _ hy)
      smul_mem' := fun r x hx y hy => by
        rw [Algebra.smul_mul_assoc]
        exact Submodule.smul_mem _ _ (hx _ hy) }⟩

Division of Submodules in an Algebra

Informal description

For a commutative semiring $R$ and an $R$-algebra $A$, the collection of submodules of $A$ forms a division structure where the division $I / J$ of two submodules $I$ and $J$ consists of all elements $x \in A$ such that $x \cdot y \in I$ for every $y \in J$. This is equivalent to requiring that the scalar action $x \bullet J$ is contained in $I$.

Submodule.mem_div_iff_forall_mul_mem theorem

{x : A} {I J : Submodule R A} : x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

Full source

theorem mem_div_iff_forall_mul_mem {x : A} {I J : Submodule R A} : x ∈ I / Jx ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I :=
  Iff.refl _

Characterization of Submodule Division via Multiplication

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For any $x \in A$ and submodules $I, J \subseteq A$, we have $x \in I / J$ if and only if for every $y \in J$, the product $x \cdot y$ belongs to $I$.

Submodule.mem_div_iff_smul_subset theorem

{x : A} {I J : Submodule R A} : x ∈ I / J ↔ x • (J : Set A) ⊆ I

Full source

theorem mem_div_iff_smul_subset {x : A} {I J : Submodule R A} : x ∈ I / Jx ∈ I / J ↔ x • (J : Set A) ⊆ I :=
  ⟨fun h y ⟨y', hy', xy'_eq_y⟩ => by rw [← xy'_eq_y]; exact h _ hy',
    fun h _ hy => h (Set.smul_mem_smul_set hy)⟩

Characterization of Submodule Division via Scalar Multiplication

Informal description

For an element $x$ in an $R$-algebra $A$ and submodules $I, J$ of $A$, $x$ belongs to the quotient submodule $I / J$ if and only if the scalar multiplication of $x$ with every element of $J$ (viewed as a set) is contained in $I$. In other words, $x \in I / J \leftrightarrow x \bullet J \subseteq I$.

Submodule.le_div_iff theorem

{I J K : Submodule R A} : I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J

Full source

theorem le_div_iff {I J K : Submodule R A} : I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J :=
  Iff.refl _

Submodule Inclusion Characterization via Division: $I \subseteq J / K \leftrightarrow \forall x \in I, \forall z \in K, x \cdot z \in J$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For submodules $I, J, K$ of $A$, the inclusion $I \subseteq J / K$ holds if and only if for every $x \in I$ and $z \in K$, the product $x \cdot z$ belongs to $J$.

Submodule.le_div_iff_mul_le theorem

{I J K : Submodule R A} : I ≤ J / K ↔ I * K ≤ J

Full source

theorem le_div_iff_mul_le {I J K : Submodule R A} : I ≤ J / K ↔ I * K ≤ J := by
  rw [le_div_iff, mul_le]

Submodule Division-Multiplication Equivalence: $I \subseteq J / K \leftrightarrow I \cdot K \subseteq J$

Informal description

Let $R$ be a commutative semiring and $A$ an $R$-algebra. For submodules $I$, $J$, and $K$ of $A$, the inclusion $I \subseteq J / K$ holds if and only if the product submodule $I \cdot K$ is contained in $J$.

Submodule.one_le_one_div theorem

{I : Submodule R A} : 1 ≤ 1 / I ↔ I ≤ 1

Full source

theorem one_le_one_div {I : Submodule R A} : 1 ≤ 1 / I ↔ I ≤ 1 := by
  rw [le_div_iff_mul_le, one_mul]

Unit Submodule Inclusion Criterion: $1 \subseteq 1/I \leftrightarrow I \subseteq 1$

Informal description

For any submodule $I$ of an $R$-algebra $A$, the inclusion $1 \subseteq 1 / I$ holds if and only if $I \subseteq 1$, where $1$ denotes the unit submodule $R \cdot 1_A$ and $1 / I$ is the division of submodules.

Submodule.one_mem_div theorem

{I J : Submodule R A} : 1 ∈ I / J ↔ J ≤ I

Full source

@[simp]
theorem one_mem_div {I J : Submodule R A} : 1 ∈ I / J1 ∈ I / J ↔ J ≤ I := by
  rw [← one_le, le_div_iff_mul_le, one_mul]

Membership of 1 in Submodule Quotient: $1 \in I/J \leftrightarrow J \subseteq I$

Informal description

For any submodules $I$ and $J$ of an $R$-algebra $A$, the multiplicative identity $1_A$ belongs to the quotient submodule $I / J$ if and only if $J$ is contained in $I$. Here, $I / J$ is defined as the set of all $a \in A$ such that $a \cdot J \subseteq I$.

Submodule.le_self_mul_one_div theorem

{I : Submodule R A} (hI : I ≤ 1) : I ≤ I * (1 / I)

Full source

theorem le_self_mul_one_div {I : Submodule R A} (hI : I ≤ 1) : I ≤ I * (1 / I) := by
  refine (mul_one I).symm.trans_le ?_
  apply mul_le_mul_right (one_le_one_div.mpr hI)

Self-multiplication containment: $I \subseteq I \cdot (1/I)$ for $I \subseteq 1$

Informal description

For any submodule $I$ of an $R$-algebra $A$ such that $I$ is contained in the unit submodule $1$ (i.e., $I \subseteq R \cdot 1_A$), we have the inclusion $I \subseteq I \cdot (1 / I)$, where $1 / I$ denotes the division submodule consisting of all $a \in A$ such that $a \bullet I \subseteq 1$.

Submodule.mul_one_div_le_one theorem

{I : Submodule R A} : I * (1 / I) ≤ 1

Full source

theorem mul_one_div_le_one {I : Submodule R A} : I * (1 / I) ≤ 1 := by
  rw [Submodule.mul_le]
  intro m hm n hn
  rw [Submodule.mem_div_iff_forall_mul_mem] at hn
  rw [mul_comm]
  exact hn m hm

Containment of Product with Quotient in Unit Submodule: $I \cdot (1 / I) \subseteq 1$

Informal description

For any submodule $I$ of an $R$-algebra $A$, the product of $I$ with the quotient submodule $1 / I$ is contained in the unit submodule $1$. In other words, for all $x \in I$ and $y \in 1 / I$, the product $x \cdot y$ belongs to the unit submodule $1$.

Submodule.map_div theorem

 {B : Type*} [CommSemiring B] [Algebra R B] (I J : Submodule R A) (h : A ≃ₐ[R] B) :
  (I / J).map h.toLinearMap = I.map h.toLinearMap / J.map h.toLinearMap

Full source

@[simp]
protected theorem map_div {B : Type*} [CommSemiring B] [Algebra R B] (I J : Submodule R A)
    (h : A ≃ₐ[R] B) : (I / J).map h.toLinearMap = I.map h.toLinearMap / J.map h.toLinearMap := by
  ext x
  simp only [mem_map, mem_div_iff_forall_mul_mem, AlgEquiv.toLinearMap_apply]
  constructor
  · rintro ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
    exact ⟨x * y, hx _ hy, map_mul h x y⟩
  · rintro hx
    refine ⟨h.symm x, fun z hz => ?_, h.apply_symm_apply x⟩
    obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩
    convert xz_mem
    apply h.injective
    rw [map_mul, h.apply_symm_apply, hxz]

Preservation of Submodule Quotient under Algebra Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. For any submodules $I, J \subseteq A$ and any $R$-algebra isomorphism $h \colon A \to B$, the pushforward of the quotient submodule $I / J$ under the linear map associated to $h$ is equal to the quotient of the pushforwards of $I$ and $J$ under $h$. That is, \[ h(I / J) = h(I) / h(J), \] where $h(I / J)$ denotes the image of $I / J$ under the linear map associated to $h$, and $h(I) / h(J)$ denotes the quotient of the images of $I$ and $J$ under $h$.

Mathlib.Algebra.Algebra.Operations

Main definitions

Tags