# Multiplication and division of submodules of an algebra. #

An interface for multiplication and division of sub-R-modules of an R-algebra A is developed.

## Main definitions #

Let R be a commutative ring (or semiring) and let A be an R-algebra.

• 1 : Submodule R A : the R-submodule R of the R-algebra A
• Mul (Submodule R A) : multiplication of two sub-R-modules M and N of A is defined to be the smallest submodule containing all the products m * n.
• Div (Submodule R A) : I / J is defined to be the submodule consisting of all a : A such that a • J ⊆ I

It is proved that Submodule R A is a semiring, and also an algebra over Set A.

Additionally, in the Pointwise locale we promote Submodule.pointwiseDistribMulAction to a MulSemiringAction as Submodule.pointwiseMulSemiringAction.

## Tags #

multiplication of submodules, division of submodules, submodule semiring

theorem SubMulAction.algebraMap_mem {R : Type u} {A : Type v} [] [] [Algebra R A] (r : R) :
() r 1
theorem SubMulAction.mem_one' {R : Type u} {A : Type v} [] [] [Algebra R A] {x : A} :
x 1 ∃ (y : R), () y = x
instance Submodule.one {R : Type u} [] {A : Type v} [] [Algebra R A] :
One ()

1 : Submodule R A is the submodule R of A.

Equations
• Submodule.one = { one := }
theorem Submodule.one_eq_range {R : Type u} [] {A : Type v} [] [Algebra R A] :
theorem Submodule.le_one_toAddSubmonoid {R : Type u} [] {A : Type v} [] [Algebra R A] :
theorem Submodule.algebraMap_mem {R : Type u} [] {A : Type v} [] [Algebra R A] (r : R) :
() r 1
@[simp]
theorem Submodule.mem_one {R : Type u} [] {A : Type v} [] [Algebra R A] {x : A} :
x 1 ∃ (y : R), () y = x
@[simp]
theorem Submodule.toSubMulAction_one {R : Type u} [] {A : Type v} [] [Algebra R A] :
theorem Submodule.one_eq_span {R : Type u} [] {A : Type v} [] [Algebra R A] :
theorem Submodule.one_eq_span_one_set {R : Type u} [] {A : Type v} [] [Algebra R A] :
1 =
theorem Submodule.one_le {R : Type u} [] {A : Type v} [] [Algebra R A] {P : } :
1 P 1 P
theorem Submodule.map_one {R : Type u} [] {A : Type v} [] [Algebra R A] {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
Submodule.map f.toLinearMap 1 = 1
@[simp]
theorem Submodule.map_op_one {R : Type u} [] {A : Type v} [] [Algebra R A] :
= 1
@[simp]
theorem Submodule.comap_op_one {R : Type u} [] {A : Type v} [] [Algebra R A] :
= 1
@[simp]
theorem Submodule.map_unop_one {R : Type u} [] {A : Type v} [] [Algebra R A] :
Submodule.map (.symm) 1 = 1
@[simp]
theorem Submodule.comap_unop_one {R : Type u} [] {A : Type v} [] [Algebra R A] :
Submodule.comap (.symm) 1 = 1
instance Submodule.mul {R : Type u} [] {A : Type v} [] [Algebra R A] :
Mul ()

Multiplication of sub-R-modules of an R-algebra A. The submodule M * N is the smallest R-submodule of A containing the elements m * n for m ∈ M and n ∈ N.

Equations
• Submodule.mul = { mul := }
theorem Submodule.mul_mem_mul {R : Type u} [] {A : Type v} [] [Algebra R A] {M : } {N : } {m : A} {n : A} (hm : m M) (hn : n N) :
m * n M * N
theorem Submodule.mul_le {R : Type u} [] {A : Type v} [] [Algebra R A] {M : } {N : } {P : } :
M * N P mM, nN, m * n P
theorem Submodule.mul_toAddSubmonoid {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) :
theorem Submodule.mul_induction_on {R : Type u} [] {A : Type v} [] [Algebra R A] {M : } {N : } {C : AProp} {r : A} (hr : r M * N) (hm : mM, nN, C (m * n)) (ha : ∀ (x y : A), C xC yC (x + y)) :
C r
theorem Submodule.mul_induction_on' {R : Type u} [] {A : Type v} [] [Algebra R A] {M : } {N : } {C : (r : A) → r M * NProp} (mem_mul_mem : ∀ (m : A) (hm : m M) (n : A) (hn : n N), C (m * n) ) (add : ∀ (x : A) (hx : x M * N) (y : A) (hy : y M * N), C x hxC y hyC (x + y) ) {r : A} (hr : r M * N) :
C r hr

A dependent version of mul_induction_on.

theorem Submodule.span_mul_span (R : Type u) [] {A : Type v} [] [Algebra R A] (S : Set A) (T : Set A) :
* = Submodule.span R (S * T)
@[simp]
theorem Submodule.mul_bot {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) :
@[simp]
theorem Submodule.bot_mul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) :
theorem Submodule.one_mul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) :
1 * M = M
theorem Submodule.mul_one {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) :
M * 1 = M
theorem Submodule.mul_le_mul {R : Type u} [] {A : Type v} [] [Algebra R A] {M : } {N : } {P : } {Q : } (hmp : M P) (hnq : N Q) :
M * N P * Q
theorem Submodule.mul_le_mul_left {R : Type u} [] {A : Type v} [] [Algebra R A] {M : } {N : } {P : } (h : M N) :
M * P N * P
theorem Submodule.mul_le_mul_right {R : Type u} [] {A : Type v} [] [Algebra R A] {M : } {N : } {P : } (h : N P) :
M * N M * P
theorem Submodule.mul_sup {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) (P : ) :
M * (N P) = M * N M * P
theorem Submodule.sup_mul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) (P : ) :
(M N) * P = M * P N * P
theorem Submodule.mul_subset_mul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) :
M * N (M * N)
theorem Submodule.map_mul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
Submodule.map f.toLinearMap (M * N) = Submodule.map f.toLinearMap M * Submodule.map f.toLinearMap N
theorem Submodule.map_op_mul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) :
Submodule.map () (M * N) = *
theorem Submodule.comap_unop_mul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) :
Submodule.comap (.symm) (M * N) = Submodule.comap (.symm) N * Submodule.comap (.symm) M
theorem Submodule.map_unop_mul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) :
Submodule.map (.symm) (M * N) = Submodule.map (.symm) N * Submodule.map (.symm) M
theorem Submodule.comap_op_mul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) :
Submodule.comap () (M * N) =
theorem Submodule.restrictScalars_mul {A : Type u_1} {B : Type u_2} {C : Type u_3} [] [] [] [Algebra A B] [Algebra A C] [Algebra B C] [] {I : } {J : } :
def Submodule.hasDistribPointwiseNeg {R : Type u} [] {A : Type u_1} [Ring A] [Algebra R A] :

Submodule.pointwiseNeg distributes over multiplication.

This is available as an instance in the Pointwise locale.

Equations
Instances For
theorem Submodule.mem_span_mul_finite_of_mem_span_mul {R : Type u_1} {A : Type u_2} [] [] [Mul A] [Module R A] {S : Set A} {S' : Set A} {x : A} (hx : x Submodule.span R (S * S')) :
∃ (T : ) (T' : ), T S T' S' x Submodule.span R (T * T')
theorem Submodule.mul_eq_span_mul_set {R : Type u} [] {A : Type v} [] [Algebra R A] (s : ) (t : ) :
s * t = Submodule.span R (s * t)
theorem Submodule.iSup_mul {ι : Sort uι} {R : Type u} [] {A : Type v} [] [Algebra R A] (s : ι) (t : ) :
(⨆ (i : ι), s i) * t = ⨆ (i : ι), s i * t
theorem Submodule.mul_iSup {ι : Sort uι} {R : Type u} [] {A : Type v} [] [Algebra R A] (t : ) (s : ι) :
t * ⨆ (i : ι), s i = ⨆ (i : ι), t * s i
theorem Submodule.mem_span_mul_finite_of_mem_mul {R : Type u} [] {A : Type v} [] [Algebra R A] {P : } {Q : } {x : A} (hx : x P * Q) :
∃ (T : ) (T' : ), T P T' Q x Submodule.span R (T * T')
theorem Submodule.mem_span_singleton_mul {R : Type u} [] {A : Type v} [] [Algebra R A] {P : } {x : A} {y : A} :
x Submodule.span R {y} * P zP, y * z = x
theorem Submodule.mem_mul_span_singleton {R : Type u} [] {A : Type v} [] [Algebra R A] {P : } {x : A} {y : A} :
x P * Submodule.span R {y} zP, z * y = x
theorem Submodule.span_singleton_mul {R : Type u} [] {A : Type v} [] [Algebra R A] {x : A} {p : } :
Submodule.span R {x} * p = x p
theorem Submodule.mem_smul_iff_inv_mul_mem {R : Type u} [] {S : Type u_1} [] [Algebra R S] {x : S} {p : } {y : S} (hx : x 0) :
y x p x⁻¹ * y p
theorem Submodule.mul_mem_smul_iff {R : Type u} [] {S : Type u_1} [] [Algebra R S] {x : S} {p : } {y : S} (hx : ) :
x * y x p y p
theorem Submodule.mul_smul_mul_eq_smul_mul_smul {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) (x : R) (y : R) :
(x * y) (M * N) = x M * y N
instance Submodule.idemSemiring {R : Type u} [] {A : Type v} [] [Algebra R A] :

Sub-R-modules of an R-algebra form an idempotent semiring.

Equations
• One or more equations did not get rendered due to their size.
theorem Submodule.span_pow {R : Type u} [] {A : Type v} [] [Algebra R A] (s : Set A) (n : ) :
^ n = Submodule.span R (s ^ n)
theorem Submodule.pow_eq_span_pow_set {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (n : ) :
M ^ n = Submodule.span R (M ^ n)
theorem Submodule.pow_subset_pow {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) {n : } :
M ^ n (M ^ n)
theorem Submodule.pow_mem_pow {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) {x : A} (hx : x M) (n : ) :
x ^ n M ^ n
theorem Submodule.pow_toAddSubmonoid {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) {n : } (h : n 0) :
theorem Submodule.le_pow_toAddSubmonoid {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) {n : } :
theorem Submodule.pow_induction_on_left' {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) {C : (n : ) → (x : A) → x M ^ nProp} (algebraMap : ∀ (r : R), C 0 (() r) ) (add : ∀ (x y : A) (i : ) (hx : x M ^ i) (hy : y M ^ i), C i x hxC i y hyC i (x + y) ) (mem_mul : ∀ (m : A) (hm : m M) (i : ) (x : A) (hx : x M ^ i), C i x hxC i.succ (m * x) ) {n : } {x : A} (hx : x M ^ n) :
C n x hx

Dependent version of Submodule.pow_induction_on_left.

theorem Submodule.pow_induction_on_right' {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) {C : (n : ) → (x : A) → x M ^ nProp} (algebraMap : ∀ (r : R), C 0 (() r) ) (add : ∀ (x y : A) (i : ) (hx : x M ^ i) (hy : y M ^ i), C i x hxC i y hyC i (x + y) ) (mul_mem : ∀ (i : ) (x : A) (hx : x M ^ i), C i x hx∀ (m : A) (hm : m M), C i.succ (x * m) ) {n : } {x : A} (hx : x M ^ n) :
C n x hx

Dependent version of Submodule.pow_induction_on_right.

theorem Submodule.pow_induction_on_left {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) {C : AProp} (hr : ∀ (r : R), C (() r)) (hadd : ∀ (x y : A), C xC yC (x + y)) (hmul : mM, ∀ (x : A), C xC (m * x)) {x : A} {n : } (hx : x M ^ n) :
C x

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

theorem Submodule.pow_induction_on_right {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) {C : AProp} (hr : ∀ (r : R), C (() r)) (hadd : ∀ (x y : A), C xC yC (x + y)) (hmul : ∀ (x : A), C xmM, C (x * m)) {x : A} {n : } (hx : x M ^ n) :
C x

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

@[simp]
theorem Submodule.mapHom_apply {R : Type u} [] {A : Type v} [] [Algebra R A] {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (p : ) :
() p = Submodule.map f.toLinearMap p
def Submodule.mapHom {R : Type u} [] {A : Type v} [] [Algebra R A] {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :

Submonoid.map as a MonoidWithZeroHom, when applied to AlgHoms.

Equations
• = { toFun := Submodule.map f.toLinearMap, map_zero' := , map_one' := , map_mul' := }
Instances For
@[simp]
theorem Submodule.equivOpposite_symm_apply {R : Type u} [] {A : Type v} [] [Algebra R A] (p : ()ᵐᵒᵖ) :
Submodule.equivOpposite.symm p = Submodule.comap (.symm) ()
@[simp]
theorem Submodule.equivOpposite_apply {R : Type u} [] {A : Type v} [] [Algebra R A] (p : ) :
Submodule.equivOpposite p =
def Submodule.equivOpposite {R : Type u} [] {A : Type v} [] [Algebra R A] :

The ring of submodules of the opposite algebra is isomorphic to the opposite ring of submodules.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Submodule.map_pow {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) {A' : Type u_1} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (n : ) :
Submodule.map f.toLinearMap (M ^ n) = Submodule.map f.toLinearMap M ^ n
theorem Submodule.comap_unop_pow {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (n : ) :
Submodule.comap (.symm) (M ^ n) = Submodule.comap (.symm) M ^ n
theorem Submodule.comap_op_pow {R : Type u} [] {A : Type v} [] [Algebra R A] (n : ) (M : ) :
Submodule.comap () (M ^ n) = ^ n
theorem Submodule.map_op_pow {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (n : ) :
Submodule.map () (M ^ n) = ^ n
theorem Submodule.map_unop_pow {R : Type u} [] {A : Type v} [] [Algebra R A] (n : ) (M : ) :
Submodule.map (.symm) (M ^ n) = Submodule.map (.symm) M ^ n
@[simp]
theorem Submodule.span.ringHom_apply {R : Type u} [] {A : Type v} [] [Algebra R A] (s : ) :
Submodule.span.ringHom s = Submodule.span R (SetSemiring.down s)
def Submodule.span.ringHom {R : Type u} [] {A : Type v} [] [Algebra R A] :

span is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets on either side).

Equations
• Submodule.span.ringHom = { toFun := fun (s : ) => Submodule.span R (SetSemiring.down s), map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
def Submodule.pointwiseMulSemiringAction {R : Type u} [] {A : Type v} [] [Algebra R A] {α : Type u_1} [] [] [] :

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.

Equations
• Submodule.pointwiseMulSemiringAction = let __src := Submodule.pointwiseDistribMulAction;
Instances For
theorem Submodule.mul_mem_mul_rev {R : Type u} [] {A : Type v} [] [Algebra R A] {M : } {N : } {m : A} {n : A} (hm : m M) (hn : n N) :
n * m M * N
theorem Submodule.mul_comm {R : Type u} [] {A : Type v} [] [Algebra R A] (M : ) (N : ) :
M * N = N * M
instance Submodule.instIdemCommSemiring {R : Type u} [] {A : Type v} [] [Algebra R A] :

Sub-R-modules of an R-algebra A form a semiring.

Equations
• Submodule.instIdemCommSemiring = let __src := Submodule.idemSemiring; IdemCommSemiring.mk IdemSemiring.bot
theorem Submodule.prod_span {R : Type u} [] {A : Type v} [] [Algebra R A] {ι : Type u_1} (s : ) (M : ιSet A) :
is, Submodule.span R (M i) = Submodule.span R (is, M i)
theorem Submodule.prod_span_singleton {R : Type u} [] {A : Type v} [] [Algebra R A] {ι : Type u_1} (s : ) (x : ιA) :
is, Submodule.span R {x i} = Submodule.span R {is, x i}
instance Submodule.moduleSet (R : Type u) [] (A : Type v) [] [Algebra R A] :
Module () ()

R-submodules of the R-algebra A are a module over Set A.

Equations
theorem Submodule.smul_def {R : Type u} [] {A : Type v} [] [Algebra R A] (s : ) (P : ) :
s P = Submodule.span R (SetSemiring.down s) * P
theorem Submodule.smul_le_smul {R : Type u} [] {A : Type v} [] [Algebra R A] {s : } {t : } {M : } {N : } (h₁ : SetSemiring.down s SetSemiring.down t) (h₂ : M N) :
s M t N
theorem Submodule.singleton_smul {R : Type u} [] {A : Type v} [] [Algebra R A] (a : A) (M : ) :
Set.up {a} M =
instance Submodule.instDiv {R : Type u} [] {A : Type v} [] [Algebra R A] :
Div ()

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$.

Equations
• Submodule.instDiv = { div := fun (I J : ) => { carrier := {x : A | yJ, x * y I}, add_mem' := , zero_mem' := , smul_mem' := } }
theorem Submodule.mem_div_iff_forall_mul_mem {R : Type u} [] {A : Type v} [] [Algebra R A] {x : A} {I : } {J : } :
x I / J yJ, x * y I
theorem Submodule.mem_div_iff_smul_subset {R : Type u} [] {A : Type v} [] [Algebra R A] {x : A} {I : } {J : } :
x I / J x J I
theorem Submodule.le_div_iff {R : Type u} [] {A : Type v} [] [Algebra R A] {I : } {J : } {K : } :
I J / K xI, zK, x * z J
theorem Submodule.le_div_iff_mul_le {R : Type u} [] {A : Type v} [] [Algebra R A] {I : } {J : } {K : } :
I J / K I * K J
@[simp]
theorem Submodule.one_le_one_div {R : Type u} [] {A : Type v} [] [Algebra R A] {I : } :
1 1 / I I 1
theorem Submodule.le_self_mul_one_div {R : Type u} [] {A : Type v} [] [Algebra R A] {I : } (hI : I 1) :
I I * (1 / I)
theorem Submodule.mul_one_div_le_one {R : Type u} [] {A : Type v} [] [Algebra R A] {I : } :
I * (1 / I) 1
@[simp]
theorem Submodule.map_div {R : Type u} [] {A : Type v} [] [Algebra R A] {B : Type u_1} [] [Algebra R B] (I : ) (J : ) (h : A ≃ₐ[R] B) :
Submodule.map h.toLinearMap (I / J) = Submodule.map h.toLinearMap I / Submodule.map h.toLinearMap J