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 let A
be an R
-algebra.
1 : Submodule R A
: the R-submodule R of the R-algebra AMul (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
.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
.
Additionally, in the pointwise
locale we promote Submodule.pointwiseDistribMulAction
to a
MulSemiringAction
as Submodule.pointwiseMulSemiringAction
.
Tags #
multiplication of submodules, division of submodules, submodule semiring
1 : Submodule R A
is the submodule R of 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
.
A dependent version of mul_induction_on
.
Submodule.pointwiseNeg
distributes over multiplication.
This is available as an instance in the Pointwise
locale.
Instances For
Sub-R-modules of an R-algebra form an idempotent semiring.
Dependent version of Submodule.pow_induction_on_left
.
Dependent version of Submodule.pow_induction_on_right
.
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
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
Submonoid.map
as a MonoidWithZeroHom
, when applied to AlgHom
s.
Instances For
span
is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets
on either side).
Instances For
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.pointwiseDistribMulAction
.
Instances For
Sub-R-modules of an R-algebra A form a semiring.
R-submodules of the R-algebra A are a module over Set 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$.