mathlib documentation

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 aet A be an R-algebra.

It is proved that submodule R A is a semiring, and also an algebra over set A.

Tags #

multiplication of submodules, division of subodules, submodule semiring

@[protected, instance]
def submodule.has_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

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

Equations
theorem submodule.one_eq_range {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :
theorem submodule.algebra_map_mem {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (r : R) :
@[simp]
theorem submodule.mem_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {x : A} :
x 1 ∃ (y : R), (algebra_map R A) y = x
theorem submodule.one_eq_span {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :
theorem submodule.one_le {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {P : submodule R A} :
1 P 1 P
@[protected, instance]
def submodule.has_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R 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} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N : submodule R A} {m n : A} (hm : m M) (hn : n N) :
m * n M * N
theorem submodule.mul_le {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N P : submodule R A} :
M * N P ∀ (m : A), m M∀ (n : A), n Nm * n P
theorem submodule.mul_to_add_submonoid {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N : submodule R A} :
@[protected]
theorem submodule.mul_induction_on {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N : submodule R 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} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N : submodule R 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) [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (S T : set A) :
@[protected]
theorem submodule.mul_assoc {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N P : submodule R A) :
(M * N) * P = M * N * P
@[simp]
theorem submodule.mul_bot {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :
@[simp]
theorem submodule.bot_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :
@[protected, simp]
theorem submodule.one_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :
1 * M = M
@[protected, simp]
theorem submodule.mul_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :
M * 1 = M
theorem submodule.mul_le_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N P Q : submodule R A} (hmp : M P) (hnq : N Q) :
M * N P * Q
theorem submodule.mul_le_mul_left {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N P : submodule R A} (h : M N) :
M * P N * P
theorem submodule.mul_le_mul_right {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N P : submodule R A} (h : N P) :
M * N M * P
theorem submodule.mul_sup {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N P : submodule R A) :
M * (N P) = M * N M * P
theorem submodule.sup_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N P : submodule R A) :
(M N) * P = M * P N * P
theorem submodule.mul_subset_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N : submodule R A) :
(M) * N M * N
theorem submodule.map_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N : submodule R A) {A' : Type u_1} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') :
theorem submodule.mem_span_mul_finite_of_mem_span_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {S S' : set A} {x : A} (hx : x submodule.span R (S * S')) :
∃ (T T' : finset A), T S T' S' x submodule.span R ((T) * T')
theorem submodule.mul_eq_span_mul_set {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (s t : submodule R A) :
s * t = submodule.span R ((s) * t)
theorem submodule.supr_mul {ι : Sort uι} {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (s : ι → submodule R A) (t : submodule R A) :
(⨆ (i : ι), s i) * t = ⨆ (i : ι), (s i) * t
theorem submodule.mul_supr {ι : Sort uι} {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (t : submodule R A) (s : ι → submodule R A) :
(t * ⨆ (i : ι), s i) = ⨆ (i : ι), t * s i
theorem submodule.mem_span_mul_finite_of_mem_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {P Q : submodule R A} {x : A} (hx : x P * Q) :
∃ (T T' : finset A), T P T' Q x submodule.span R ((T) * T')
theorem submodule.pow_subset_pow {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) {n : } :
M ^ n (M ^ n)
@[protected]
theorem submodule.pow_induction_on' {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) {C : Π (n : ) (x : A), x M ^ n → Prop} (hr : ∀ (r : R), C 0 ((algebra_map R 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.

@[protected]
theorem submodule.pow_induction_on {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) {C : A → Prop} (hr : ∀ (r : R), C ((algebra_map R 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

def submodule.span.ring_hom {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

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

Equations
theorem submodule.mul_mem_mul_rev {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {M N : submodule R A} {m n : A} (hm : m M) (hn : n N) :
n * m M * N
@[protected]
theorem submodule.mul_comm {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] (M N : submodule R A) :
M * N = N * M
theorem submodule.prod_span {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {ι : Type u_1} (s : finset ι) (M : ι → set A) :
∏ (i : ι) in s, submodule.span R (M i) = submodule.span R (∏ (i : ι) in s, M i)
theorem submodule.prod_span_singleton {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {ι : Type u_1} (s : finset ι) (x : ι → A) :
∏ (i : ι) in s, submodule.span R {x i} = submodule.span R {∏ (i : ι) in s, x i}
@[protected, instance]
def submodule.module_set (R : Type u) [comm_semiring R] (A : Type v) [comm_semiring A] [algebra R A] :

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

Equations
theorem submodule.smul_def {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {s : set.set_semiring A} {P : submodule R A} :
s P = (submodule.span R s) * P
theorem submodule.smul_le_smul {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {s t : set.set_semiring A} {M N : submodule R A} (h₁ : s.down t.down) (h₂ : M N) :
s M t N
theorem submodule.smul_singleton {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] (a : A) (M : submodule R A) :
@[protected, instance]
def submodule.has_div {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R 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} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {x : A} {I J : submodule R A} :
x I / J ∀ (y : A), y Jx * y I
theorem submodule.mem_div_iff_smul_subset {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {x : A} {I J : submodule R A} :
x I / J x J I
theorem submodule.le_div_iff {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {I J K : submodule R A} :
I J / K ∀ (x : A), x I∀ (z : A), z Kx * z J
theorem submodule.le_div_iff_mul_le {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {I J K : submodule R A} :
I J / K I * K J
@[simp]
theorem submodule.one_le_one_div {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {I : submodule R A} :
1 1 / I I 1
theorem submodule.le_self_mul_one_div {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {I : submodule R A} (hI : I 1) :
I I * (1 / I)
theorem submodule.mul_one_div_le_one {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {I : submodule R A} :
I * (1 / I) 1
@[simp]
theorem submodule.map_div {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {B : Type u_1} [comm_ring B] [algebra R B] (I J : submodule R A) (h : A ≃ₐ[R] B) :