Multiplication and division of submodules of an algebra. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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.
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) :
⇑(algebra_map R A) r ∈ 1
theorem
sub_mul_action.mem_one'
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{x : A} :
@[protected, instance]
1 : submodule R A is the submodule R of A.
Equations
- submodule.has_one = {one := linear_map.range (algebra.linear_map R A)}
theorem
submodule.one_eq_range
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A] :
1 = linear_map.range (algebra.linear_map R A)
theorem
submodule.le_one_to_add_submonoid
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A] :
1 ≤ 1.to_add_submonoid
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} :
@[simp]
theorem
submodule.to_sub_mul_action_one
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A] :
1.to_sub_mul_action = 1
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_eq_span_one_set
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A] :
1 = submodule.span R 1
@[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 := submodule.map₂ (linear_map.mul R A)}
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)
@[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) :
@[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]
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 = function.injective.has_distrib_neg submodule.to_add_submonoid submodule.has_distrib_pointwise_neg._proof_1 submodule.has_distrib_pointwise_neg._proof_2 submodule.has_distrib_pointwise_neg._proof_3
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) :
@[protected, instance]
def
submodule.idem_semiring
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A] :
idem_semiring (submodule R A)
Sub-R-modules of an R-algebra form an idempotent semiring.
Equations
- submodule.idem_semiring = {add := add_monoid_with_one.add add_monoid_with_one.unary, add_assoc := _, zero := add_monoid_with_one.zero add_monoid_with_one.unary, zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul add_monoid_with_one.unary, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semigroup.mul (function.injective.semigroup submodule.to_add_submonoid submodule.idem_semiring._proof_7 submodule.idem_semiring._proof_8), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := add_monoid_with_one.one add_monoid_with_one.unary, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast add_monoid_with_one.unary, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow._default add_monoid_with_one.one semigroup.mul submodule.one_mul submodule.mul_one, npow_zero' := _, npow_succ' := _, sup := lattice.sup (conditionally_complete_lattice.to_lattice (submodule R A)), le := lattice.le (conditionally_complete_lattice.to_lattice (submodule R A)), lt := lattice.lt (conditionally_complete_lattice.to_lattice (submodule R A)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := order_bot.bot submodule.order_bot, bot_le := _}
theorem
submodule.span_pow
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(s : set A)
(n : ℕ) :
submodule.span R s ^ n = submodule.span R (s ^ 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_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) :
(M ^ n).to_add_submonoid = M.to_add_submonoid ^ n
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 : ℕ} :
M.to_add_submonoid ^ n ≤ (M ^ n).to_add_submonoid
@[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 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_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 hx → C i y hy → C 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 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
@[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 x → C y → C (x + y))
(hmul : ∀ (x : A), C x → ∀ (m : A), m ∈ M → C (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
- 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_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 := λ (s : set_semiring A), submodule.span R (⇑set_semiring.down s), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
submodule.span.ring_hom_apply
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
(s : set_semiring A) :
@[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] :
mul_semiring_action α (submodule 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) :
@[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.idem_comm_semiring
{R : Type u}
[comm_semiring R]
{A : Type v}
[comm_semiring A]
[algebra R A] :
idem_comm_semiring (submodule R A)
Sub-R-modules of an R-algebra A form a semiring.
Equations
- submodule.idem_comm_semiring = {add := idem_semiring.add submodule.idem_semiring, add_assoc := _, zero := idem_semiring.zero submodule.idem_semiring, zero_add := _, add_zero := _, nsmul := idem_semiring.nsmul submodule.idem_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := idem_semiring.mul submodule.idem_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := idem_semiring.one submodule.idem_semiring, one_mul := _, mul_one := _, nat_cast := idem_semiring.nat_cast submodule.idem_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := idem_semiring.npow submodule.idem_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _, sup := idem_semiring.sup submodule.idem_semiring, le := idem_semiring.le submodule.idem_semiring, lt := idem_semiring.lt submodule.idem_semiring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, add_eq_sup := _, bot := idem_semiring.bot submodule.idem_semiring, bot_le := _}
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] :
module (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_smul := {smul := λ (s : set_semiring A) (P : submodule R A), submodule.span R (⇑set_semiring.down s) * P}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, 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_semiring A)
(P : submodule R A) :
s • P = submodule.span R (⇑set_semiring.down 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) :
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) :
⇑set.up {a} • M = submodule.map (linear_map.mul_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_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_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