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

@[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_map_top {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_le {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {P : submodule R A} :
1 P 1 P

@[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_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)) (h0 : C 0) (ha : ∀ (x y : A), C xC yC (x + y)) (hs : ∀ (r : R) (x : A), C xC (r x)) :
C r

theorem submodule.span_mul_span (R : Type u) [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (S T : set A) :

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) :

@[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

@[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') :

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

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

Equations
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)

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

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

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

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

Equations
@[instance]
def submodule.semimodule_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) :

@[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) :