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 Ahas_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 productsm * n.has_div (submodule R A):I / Jis defined to be the submodule consisting of alla : Asuch thata • 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 submodules, submodule semiring
@[protected, instance]
1 : submodule R A is the submodule R of A.
Equations
- submodule.has_one = {one := (algebra.linear_map R A).range}
theorem
submodule.one_eq_range
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A] :
1 = (algebra.linear_map R A).range
theorem
submodule.algebra_map_mem
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(r : R) :
⇑(algebra_map R A) r ∈ 1
@[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] :
1 = submodule.span R {1}
theorem
submodule.one_le
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
{P : submodule R A} :
@[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') :
submodule.map f.to_linear_map 1 = 1
@[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] :
submodule.map ↑((mul_opposite.op_linear_equiv R).symm) 1 = 1
@[simp]
theorem
submodule.comap_unop_one
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A] :
submodule.comap ↑((mul_opposite.op_linear_equiv R).symm) 1 = 1
@[protected, instance]
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}
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} :
(M * N).to_add_submonoid = (M.to_add_submonoid) * N.to_add_submonoid
@[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 hx → C y hy → C (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) :
(submodule.span R S) * submodule.span R T = submodule.span R (S * T)
@[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) :
@[protected, simp]
theorem
submodule.mul_one
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(M : submodule R A) :
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) :
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) :
@[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') :
submodule.map f.to_linear_map (M * N) = (submodule.map f.to_linear_map M) * submodule.map f.to_linear_map N
theorem
submodule.map_op_mul
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(M N : submodule R A) :
theorem
submodule.comap_unop_mul
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(M N : submodule R A) :
submodule.comap ↑((mul_opposite.op_linear_equiv R).symm) (M * N) = (submodule.comap ↑((mul_opposite.op_linear_equiv R).symm) N) * submodule.comap ↑((mul_opposite.op_linear_equiv R).symm) M
theorem
submodule.map_unop_mul
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(M N : submodule R Aᵐᵒᵖ) :
submodule.map ↑((mul_opposite.op_linear_equiv R).symm) (M * N) = (submodule.map ↑((mul_opposite.op_linear_equiv R).symm) N) * submodule.map ↑((mul_opposite.op_linear_equiv R).symm) M
theorem
submodule.comap_op_mul
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(M N : submodule R Aᵐᵒᵖ) :
@[protected, instance]
def
submodule.has_distrib_pointwise_neg
{R : Type u}
[comm_semiring R]
{A : Type u_1}
[ring A]
[algebra R A] :
has_distrib_neg (submodule R A)
submodule.has_pointwise_neg distributes over multiplication.
This is available as an instance in the pointwise locale.
Equations
- submodule.has_distrib_pointwise_neg = {neg := has_neg.neg submodule.has_pointwise_neg, neg_neg := _, neg_mul := _, mul_neg := _}
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) :
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) :
@[protected, instance]
Sub-R-modules of an R-algebra form a semiring.
Equations
- submodule.semiring = {add := add_comm_monoid.add submodule.pointwise_add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero submodule.pointwise_add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul submodule.pointwise_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul submodule.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid_with_zero.npow._default 1 has_mul.mul submodule.one_mul submodule.mul_one, npow_zero' := _, npow_succ' := _}
@[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 hx → C i y hy → C i (x + y) _)
(hmul : ∀ (m : A) (H : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C 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 x → C y → C (x + y))
(hmul : ∀ (m : A), m ∈ M → ∀ (x : A), C x → C (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.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
- submodule.map_hom f = {to_fun := submodule.map f.to_linear_map, map_zero' := _, map_one' := _, map_mul' := _}
@[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) :
⇑(submodule.map_hom f) p = submodule.map f.to_linear_map p
@[simp]
theorem
submodule.equiv_opposite_apply
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra 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
- submodule.equiv_opposite = {to_fun := λ (p : submodule R Aᵐᵒᵖ), mul_opposite.op (submodule.comap ↑(mul_opposite.op_linear_equiv R) p), inv_fun := λ (p : (submodule R A)ᵐᵒᵖ), submodule.comap ↑((mul_opposite.op_linear_equiv R).symm) (mul_opposite.unop p), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
@[simp]
theorem
submodule.equiv_opposite_symm_apply
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(p : (submodule R A)ᵐᵒᵖ) :
@[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 : ℕ) :
submodule.map f.to_linear_map (M ^ n) = submodule.map f.to_linear_map M ^ n
theorem
submodule.comap_unop_pow
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(M : submodule R A)
(n : ℕ) :
submodule.comap ↑((mul_opposite.op_linear_equiv R).symm) (M ^ n) = submodule.comap ↑((mul_opposite.op_linear_equiv R).symm) M ^ n
theorem
submodule.comap_op_pow
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(n : ℕ)
(M : submodule R Aᵐᵒᵖ) :
submodule.comap ↑(mul_opposite.op_linear_equiv R) (M ^ n) = submodule.comap ↑(mul_opposite.op_linear_equiv R) M ^ n
theorem
submodule.map_op_pow
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(M : submodule R A)
(n : ℕ) :
submodule.map ↑(mul_opposite.op_linear_equiv R) (M ^ n) = submodule.map ↑(mul_opposite.op_linear_equiv R) M ^ n
theorem
submodule.map_unop_pow
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(n : ℕ)
(M : submodule R Aᵐᵒᵖ) :
submodule.map ↑((mul_opposite.op_linear_equiv R).symm) (M ^ n) = submodule.map ↑((mul_opposite.op_linear_equiv R).symm) M ^ n
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_module, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
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) :
@[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) :
@[protected, 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 := _, nsmul := semiring.nsmul submodule.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul submodule.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one submodule.semiring, one_mul := _, mul_one := _, npow := semiring.npow submodule.semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}
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] :
module (set.set_semiring A) (submodule R A)
R-submodules of the R-algebra A are a module over set A.
Equations
- submodule.module_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 := _}
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) :
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) M
@[protected, instance]
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$.
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} :
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} :
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} :
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} :
@[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} :
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) :
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} :
@[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) :
submodule.map h.to_linear_map (I / J) = submodule.map h.to_linear_map I / submodule.map h.to_linear_map J