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 / J
is defined to be the submodule consisting of alla : A
such 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
1 : submodule R A
is the submodule R of A.
Equations
- submodule.has_one = {one := (algebra.linear_map R A).range}
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}
A dependent version of mul_induction_on
.
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 := _}
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' := _}
Dependent version of submodule.pow_induction_on
.
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
submonoid.map
as a monoid_with_zero_hom
, when applied to alg_hom
s.
Equations
- submodule.map_hom f = {to_fun := submodule.map f.to_linear_map, map_zero' := _, map_one' := _, map_mul' := _}
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' := _}
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' := _}
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 := _}
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 := _}
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$.