# mathlibdocumentation

algebra.algebra.operations

# 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
• has_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.
• has_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.pointwise_distrib_mul_action to a mul_semiring_action as submodule.pointwise_mul_semiring_action.

## Tags #

multiplication of submodules, division of submodules, submodule semiring

theorem sub_mul_action.algebra_map_mem {R : Type u} {A : Type v} [semiring A] [ A] (r : R) :
A) r 1
theorem sub_mul_action.mem_one' {R : Type u} {A : Type v} [semiring A] [ A] {x : A} :
x 1 ∃ (y : R), A) y = x
@[protected, instance]
def submodule.has_one {R : Type u} {A : Type v} [semiring A] [ A] :

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

Equations
theorem submodule.one_eq_range {R : Type u} {A : Type v} [semiring A] [ A] :
theorem submodule.le_one_to_add_submonoid {R : Type u} {A : Type v} [semiring A] [ A] :
theorem submodule.algebra_map_mem {R : Type u} {A : Type v} [semiring A] [ A] (r : R) :
A) r 1
@[simp]
theorem submodule.mem_one {R : Type u} {A : Type v} [semiring A] [ A] {x : A} :
x 1 ∃ (y : R), A) y = x
@[simp]
theorem submodule.to_sub_mul_action_one {R : Type u} {A : Type v} [semiring A] [ A] :
theorem submodule.one_eq_span {R : Type u} {A : Type v} [semiring A] [ A] :
1 = {1}
theorem submodule.one_eq_span_one_set {R : Type u} {A : Type v} [semiring A] [ A] :
1 =
theorem submodule.one_le {R : Type u} {A : Type v} [semiring A] [ A] {P : A} :
1 P 1 P
@[protected]
theorem submodule.map_one {R : Type u} {A : Type v} [semiring A] [ A] {A' : Type u_1} [semiring A'] [ A'] (f : A →ₐ[R] A') :
@[simp]
theorem submodule.map_op_one {R : Type u} {A : Type v} [semiring A] [ A] :
@[simp]
theorem submodule.comap_op_one {R : Type u} {A : Type v} [semiring A] [ A] :
@[simp]
theorem submodule.map_unop_one {R : Type u} {A : Type v} [semiring A] [ A] :
@[simp]
theorem submodule.comap_unop_one {R : Type u} {A : Type v} [semiring A] [ A] :
@[protected, instance]
def submodule.has_mul {R : Type u} {A : Type v} [semiring A] [ A] :

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
theorem submodule.mul_mem_mul {R : Type u} {A : Type v} [semiring A] [ A] {M N : A} {m n : A} (hm : m M) (hn : n N) :
m * n M * N
theorem submodule.mul_le {R : Type u} {A : Type v} [semiring A] [ A] {M N P : A} :
M * N P ∀ (m : A), m M∀ (n : A), n Nm * n P
theorem submodule.mul_to_add_submonoid {R : Type u} {A : Type v} [semiring A] [ A] (M N : A) :
@[protected]
theorem submodule.mul_induction_on {R : Type u} {A : Type v} [semiring A] [ A] {M N : A} {C : A → Prop} {r : A} (hr : r M * N) (hm : ∀ (m : A), m M∀ (n : A), n NC (m * n)) (ha : ∀ (x y : A), C xC yC (x + y)) :
C r
@[protected]
theorem submodule.mul_induction_on' {R : Type u} {A : Type v} [semiring A] [ A] {M N : A} {C : Π (r : A), r M * N → Prop} (hm : ∀ (m : A) (H : m M) (n : A) (H_1 : n N), C (m * n) _) (ha : ∀ (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} [semiring A] [ A] (S T : set A) :
* = (S * T)
@[simp]
theorem submodule.mul_bot {R : Type u} {A : Type v} [semiring A] [ A] (M : A) :
@[simp]
theorem submodule.bot_mul {R : Type u} {A : Type v} [semiring A] [ A] (M : A) :
@[protected, simp]
theorem submodule.one_mul {R : Type u} {A : Type v} [semiring A] [ A] (M : A) :
1 * M = M
@[protected, simp]
theorem submodule.mul_one {R : Type u} {A : Type v} [semiring A] [ A] (M : A) :
M * 1 = M
theorem submodule.mul_le_mul {R : Type u} {A : Type v} [semiring A] [ A] {M N P Q : A} (hmp : M P) (hnq : N Q) :
M * N P * Q
theorem submodule.mul_le_mul_left {R : Type u} {A : Type v} [semiring A] [ A] {M N P : A} (h : M N) :
M * P N * P
theorem submodule.mul_le_mul_right {R : Type u} {A : Type v} [semiring A] [ A] {M N P : A} (h : N P) :
M * N M * P
theorem submodule.mul_sup {R : Type u} {A : Type v} [semiring A] [ A] (M N P : A) :
M * (N P) = M * N M * P
theorem submodule.sup_mul {R : Type u} {A : Type v} [semiring A] [ A] (M N P : A) :
(M N) * P = M * P N * P
theorem submodule.mul_subset_mul {R : Type u} {A : Type v} [semiring A] [ A] (M N : A) :
M * N (M * N)
@[protected]
theorem submodule.map_mul {R : Type u} {A : Type v} [semiring A] [ A] (M N : A) {A' : Type u_1} [semiring A'] [ A'] (f : A →ₐ[R] A') :
(M * N) =
theorem submodule.map_op_mul {R : Type u} {A : Type v} [semiring A] [ A] (M N : A) :
theorem submodule.comap_unop_mul {R : Type u} {A : Type v} [semiring A] [ A] (M N : A) :
(M * N) =
theorem submodule.map_unop_mul {R : Type u} {A : Type v} [semiring A] [ A] (M N : Aᵐᵒᵖ) :
(M * N) =
theorem submodule.comap_op_mul {R : Type u} {A : Type v} [semiring A] [ A] (M N : Aᵐᵒᵖ) :
@[protected]
def submodule.has_distrib_pointwise_neg {R : Type u} {A : Type u_1} [ring A] [ A] :

submodule.has_pointwise_neg distributes over multiplication.

This is available as an instance in the pointwise locale.

Equations
theorem submodule.mem_span_mul_finite_of_mem_span_mul {R : Type u_1} {A : Type u_2} [semiring R] [has_mul A] [ A] {S S' : set A} {x : A} (hx : x (S * S')) :
∃ (T T' : finset A), T S T' S' x (T * T')
theorem submodule.mul_eq_span_mul_set {R : Type u} {A : Type v} [semiring A] [ A] (s t : A) :
s * t = (s * t)
theorem submodule.supr_mul {ι : Sort uι} {R : Type u} {A : Type v} [semiring A] [ A] (s : ι → A) (t : A) :
(⨆ (i : ι), s i) * t = ⨆ (i : ι), s i * t
theorem submodule.mul_supr {ι : Sort uι} {R : Type u} {A : Type v} [semiring A] [ A] (t : A) (s : ι → A) :
(t * ⨆ (i : ι), s i) = ⨆ (i : ι), t * s i
theorem submodule.mem_span_mul_finite_of_mem_mul {R : Type u} {A : Type v} [semiring A] [ A] {P Q : A} {x : A} (hx : x P * Q) :
∃ (T T' : finset A), T P T' Q x (T * T')
@[protected, instance]
def submodule.semiring {R : Type u} {A : Type v} [semiring A] [ A] :

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

Equations
theorem submodule.span_pow {R : Type u} {A : Type v} [semiring A] [ A] (s : set A) (n : ) :
^ n = (s ^ n)
theorem submodule.pow_eq_span_pow_set {R : Type u} {A : Type v} [semiring A] [ A] (M : A) (n : ) :
M ^ n = (M ^ n)
theorem submodule.pow_subset_pow {R : Type u} {A : Type v} [semiring A] [ A] (M : A) {n : } :
M ^ n (M ^ n)
theorem submodule.pow_mem_pow {R : Type u} {A : Type v} [semiring A] [ A] (M : A) {x : A} (hx : x M) (n : ) :
x ^ n M ^ n
theorem submodule.pow_to_add_submonoid {R : Type u} {A : Type v} [semiring A] [ A] (M : A) {n : } (h : n 0) :
theorem submodule.le_pow_to_add_submonoid {R : Type u} {A : Type v} [semiring A] [ A] (M : A) {n : } :
@[protected]
theorem submodule.pow_induction_on_left' {R : Type u} {A : Type v} [semiring A] [ A] (M : A) {C : Π (n : ) (x : A), x M ^ n → Prop} (hr : ∀ (r : R), C 0 ( A) r) _) (hadd : ∀ (x y : A) (i : ) (hx : x M ^ i) (hy : y M ^ i), C i x hxC i y hyC i (x + y) _) (hmul : ∀ (m : A) (H : m M) (i : ) (x : A) (hx : x M ^ i), C i x hxC i.succ (m * x) _) {x : A} {n : } (hx : x M ^ n) :
C n x hx

Dependent version of submodule.pow_induction_on_left.

@[protected]
theorem submodule.pow_induction_on_right' {R : Type u} {A : Type v} [semiring A] [ A] (M : A) {C : Π (n : ) (x : A), x M ^ n → Prop} (hr : ∀ (r : R), C 0 ( A) r) _) (hadd : ∀ (x y : A) (i : ) (hx : x M ^ i) (hy : y M ^ i), C i x hxC i y hyC i (x + y) _) (hmul : ∀ (i : ) (x : A) (hx : x M ^ i), C i x hx∀ (m : A) (H : m M), C i.succ (x * m) _) {x : A} {n : } (hx : x M ^ n) :
C n x hx

Dependent version of submodule.pow_induction_on_right.

@[protected]
theorem submodule.pow_induction_on_left {R : Type u} {A : Type v} [semiring A] [ A] (M : A) {C : A → Prop} (hr : ∀ (r : R), C ( A) r)) (hadd : ∀ (x y : A), C xC yC (x + y)) (hmul : ∀ (m : A), m M∀ (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

@[protected]
theorem submodule.pow_induction_on_right {R : Type u} {A : Type v} [semiring A] [ A] (M : A) {C : A → Prop} (hr : ∀ (r : R), C ( A) r)) (hadd : ∀ (x y : A), C xC yC (x + y)) (hmul : ∀ (x : A), C x∀ (m : A), m MC (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

def submodule.map_hom {R : Type u} {A : Type v} [semiring A] [ A] {A' : Type u_1} [semiring A'] [ A'] (f : A →ₐ[R] A') :
A →*₀ A'

submonoid.map as a monoid_with_zero_hom, when applied to alg_homs.

Equations
@[simp]
theorem submodule.map_hom_apply {R : Type u} {A : Type v} [semiring A] [ A] {A' : Type u_1} [semiring A'] [ A'] (f : A →ₐ[R] A') (p : A) :
@[simp]
theorem submodule.equiv_opposite_apply {R : Type u} {A : Type v} [semiring A] [ A] (p : Aᵐᵒᵖ) :
def submodule.equiv_opposite {R : Type u} {A : Type v} [semiring A] [ A] :

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

Equations
@[simp]
theorem submodule.equiv_opposite_symm_apply {R : Type u} {A : Type v} [semiring A] [ A] (p : A)ᵐᵒᵖ) :
@[protected]
theorem submodule.map_pow {R : Type u} {A : Type v} [semiring A] [ A] (M : A) {A' : Type u_1} [semiring A'] [ A'] (f : A →ₐ[R] A') (n : ) :
(M ^ n) =
theorem submodule.comap_unop_pow {R : Type u} {A : Type v} [semiring A] [ A] (M : A) (n : ) :
(M ^ n) =
theorem submodule.comap_op_pow {R : Type u} {A : Type v} [semiring A] [ A] (n : ) (M : Aᵐᵒᵖ) :
theorem submodule.map_op_pow {R : Type u} {A : Type v} [semiring A] [ A] (M : A) (n : ) :
(M ^ n) =
theorem submodule.map_unop_pow {R : Type u} {A : Type v} [semiring A] [ A] (n : ) (M : Aᵐᵒᵖ) :
(M ^ n) =
def submodule.span.ring_hom {R : Type u} {A : Type v} [semiring A] [ A] :

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

Equations
@[protected]
def submodule.pointwise_mul_semiring_action {R : Type u} {A : Type v} [semiring A] [ A] {α : Type u_1} [monoid α] [ A] [ A] :
A)

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

Equations
theorem submodule.mul_mem_mul_rev {R : Type u} {A : Type v} [ A] {M N : A} {m n : A} (hm : m M) (hn : n N) :
n * m M * N
@[protected]
theorem submodule.mul_comm {R : Type u} {A : Type v} [ A] (M N : A) :
M * N = N * M
@[protected, instance]
def submodule.comm_semiring {R : Type u} {A : Type v} [ A] :

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

Equations
theorem submodule.prod_span {R : Type u} {A : Type v} [ A] {ι : Type u_1} (s : finset ι) (M : ι → set A) :
s.prod (λ (i : ι), (M i)) = (s.prod (λ (i : ι), M i))
theorem submodule.prod_span_singleton {R : Type u} {A : Type v} [ A] {ι : Type u_1} (s : finset ι) (x : ι → A) :
s.prod (λ (i : ι), {x i}) = {s.prod (λ (i : ι), x i)}
@[protected, instance]
def submodule.module_set (R : Type u) (A : Type v) [ A] :
A)

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

Equations
theorem submodule.smul_def {R : Type u} {A : Type v} [ A] {s : set_semiring A} {P : A} :
s P = * P
theorem submodule.smul_le_smul {R : Type u} {A : Type v} [ A] {s t : set_semiring A} {M N : A} (h₁ : ) (h₂ : M N) :
s M t N
theorem submodule.smul_singleton {R : Type u} {A : Type v} [ A] (a : A) (M : A) :
set.up {a} M = M
@[protected, instance]
def submodule.has_div {R : Type u} {A : Type v} [ A] :

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
theorem submodule.mem_div_iff_forall_mul_mem {R : Type u} {A : Type v} [ A] {x : A} {I J : A} :
x I / J ∀ (y : A), y Jx * y I
theorem submodule.mem_div_iff_smul_subset {R : Type u} {A : Type v} [ A] {x : A} {I J : A} :
x I / J x J I
theorem submodule.le_div_iff {R : Type u} {A : Type v} [ A] {I J K : A} :
I J / K ∀ (x : A), x I∀ (z : A), z Kx * z J
theorem submodule.le_div_iff_mul_le {R : Type u} {A : Type v} [ A] {I J K : A} :
I J / K I * K J
@[simp]
theorem submodule.one_le_one_div {R : Type u} {A : Type v} [ A] {I : A} :
1 1 / I I 1
theorem submodule.le_self_mul_one_div {R : Type u} {A : Type v} [ A] {I : A} (hI : I 1) :
I I * (1 / I)
theorem submodule.mul_one_div_le_one {R : Type u} {A : Type v} [ A] {I : A} :
I * (1 / I) 1
@[protected, simp]
theorem submodule.map_div {R : Type u} {A : Type v} [ A] {B : Type u_1} [ B] (I J : A) (h : A ≃ₐ[R] B) :
(I / J) =