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.

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.

Tags

multiplication of submodules, division of subodules, submodule semiring

source

@[instance]

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

has_one (submodule R A)

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

Equations

submodule.has_one = {one := submodule.map (algebra.of_id R A).to_linear_map ⊤}

source

theorem submodule.one_eq_map_top {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

1 = submodule.map (algebra.of_id R A).to_linear_map ⊤

source

theorem submodule.one_eq_span {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

1 = submodule.span R {1}

source

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

source

@[instance]

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

has_mul (submodule 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

submodule.has_mul = {mul := λ (M N : submodule R A), ⨆ (s : ↥M), submodule.map (⇑(algebra.lmul R A) s.val) N}

source

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

source

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 ∈ N → m * n ∈ P

source

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 ∈ N → C (m * n)) (h0 : C 0) (ha : ∀ (x y : A), C x → C y → C (x + y)) (hs : ∀ (r : R) (x : A), C x → C (r • x)) :

C r

source

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

(submodule.span R S) * submodule.span R T = submodule.span R (S * T)

source

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

source

@[simp]

theorem submodule.mul_bot {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :

M * ⊥ = ⊥

source

@[simp]

theorem submodule.bot_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :

⊥ * M = ⊥

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

submodule.map f.to_linear_map (M * N) = (submodule.map f.to_linear_map M) * submodule.map f.to_linear_map N

source

@[instance]

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

semiring (submodule R A)

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

Equations

submodule.semiring = {add := add_comm_monoid.add submodule.add_comm_monoid_submodule, add_assoc := _, zero := add_comm_monoid.zero submodule.add_comm_monoid_submodule, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul submodule.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

source

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)

source

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

set.set_semiring A →+* submodule R A

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

Equations

submodule.span.ring_hom = {to_fun := submodule.span R algebra.to_semimodule, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

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

source

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

source

@[instance]

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

comm_semiring (submodule R A)

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

Equations

submodule.comm_semiring = {add := semiring.add submodule.semiring, add_assoc := _, zero := semiring.zero submodule.semiring, zero_add := _, add_zero := _, add_comm := _, mul := semiring.mul submodule.semiring, mul_assoc := _, one := semiring.one submodule.semiring, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

@[instance]

def submodule.semimodule_set (R : Type u) [comm_semiring R] (A : Type v) [comm_semiring A] [algebra R A] :

semimodule (set.set_semiring A) (submodule R A)

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

Equations

submodule.semimodule_set R A = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (s : set.set_semiring A) (P : submodule R A), (submodule.span R s) * P}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}

source

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

source

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

source

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

{a}.up • M = submodule.map (algebra.lmul_left R A a) M

source

@[instance]

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

has_div (submodule 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

submodule.has_div = {div := λ (I J : submodule R A), {carrier := {x : A | ∀ (y : A), y ∈ J → x * y ∈ I}, zero_mem' := _, add_mem' := _, smul_mem' := _}}

source

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 ∈ J → x * y ∈ I

source

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

source

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 ∈ K → x * z ∈ J

source

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

source

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

submodule.map h.to_linear_map (I / J) = submodule.map h.to_linear_map I / submodule.map h.to_linear_map J