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

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} [comm_semiring R] [semiring A] [algebra R A] (r : R) :
theorem sub_mul_action.mem_one' {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {x : A} :
x 1 ∃ (y : R), (algebra_map R A) y = x
@[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.le_one_to_add_submonoid {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
@[simp]
theorem submodule.to_sub_mul_action_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :
theorem submodule.one_eq_span {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :
theorem submodule.one_eq_span_one_set {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]
theorem submodule.map_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {A' : Type u_1} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') :
@[simp]
theorem submodule.map_op_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :
@[simp]
theorem submodule.comap_op_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :
@[simp]
theorem submodule.map_unop_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :
@[simp]
theorem submodule.comap_unop_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :
@[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) :
@[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)
@[protected]
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') :
@[protected]
def submodule.has_distrib_pointwise_neg {R : Type u} [comm_semiring R] {A : Type u_1} [ring A] [algebra R 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] [add_comm_monoid A] [has_mul A] [module 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) :
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.span_pow {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (s : set A) (n : ) :
theorem submodule.pow_eq_span_pow_set {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) (n : ) :
M ^ n = submodule.span R (M ^ n)
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)
theorem submodule.pow_mem_pow {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) {x : A} (hx : x M) (n : ) :
x ^ n M ^ n
theorem submodule.pow_to_add_submonoid {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) {n : } (h : n 0) :
theorem submodule.le_pow_to_add_submonoid {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) {n : } :
@[protected]
theorem submodule.pow_induction_on_left' {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_left.

@[protected]
theorem submodule.pow_induction_on_right' {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 : ∀ (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} [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

@[protected]
theorem submodule.pow_induction_on_right {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 : ∀ (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} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {A' : Type u_1} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') :

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

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

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

Equations
@[protected]
theorem submodule.map_pow {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) {A' : Type u_1} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') (n : ) :
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
@[protected]
def submodule.pointwise_mul_semiring_action {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {α : Type u_1} [monoid α] [mul_semiring_action α A] [smul_comm_class α R 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} [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) :
s.prod (λ (i : ι), submodule.span R (M i)) = submodule.span R (s.prod (λ (i : ι), 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) :
s.prod (λ (i : ι), submodule.span R {x i}) = submodule.span R {s.prod (λ (i : ι), 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_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_semiring A} {M N : submodule R A} (h₁ : set_semiring.down s set_semiring.down t) (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
@[protected, 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_semiring B] [algebra R B] (I J : submodule R A) (h : A ≃ₐ[R] B) :