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
.
When R
is not necessarily commutative, and A
is merely a R
-module with a ring structure
such that IsScalarTower R A A
holds (equivalent to the data of a ring homomorphism R →+* A
by ringHomEquivModuleIsScalarTower
), we can still define 1 : Submodule R A
and
Mul (Submodule R A)
, but 1
is only a left identity, not necessarily a right one.
Tags #
multiplication of submodules, division of submodules, submodule semiring
1 : Submodule R A
is the submodule R ∙ 1
of A.
TODO: potentially change this back to LinearMap.range (Algebra.linearMap R A)
once a version of Algebra
without the commutes'
field is introduced.
See issue https://github.com/leanprover-community/mathlib4/issues/18110.
Equations
- Submodule.one = { one := LinearMap.range (LinearMap.toSpanSingleton R A 1) }
Equations
- One or more equations did not get rendered due to their size.
Dependent version of Submodule.smul_induction_on
.
Multiplication of sub-R-modules of an R-module A that is also a semiring. The submodule M * N
consists of finite sums of elements m * n
for m ∈ M
and n ∈ N
.
Equations
- Submodule.mul = { mul := fun (x1 x2 : Submodule R A) => x1 • x2 }
A dependent version of mul_induction_on
.
Sub-R
-modules of an R
-module form an idempotent semiring.
Equations
Submodule.pointwiseNeg
distributes over multiplication.
This is available as an instance in the Pointwise
locale.
Equations
Instances For
Sub-R-modules of an R-algebra form an idempotent semiring.
Equations
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 RingHom
, when applied to an AlgHom
.
Equations
- Submodule.mapHom f = { toFun := Submodule.map f.toLinearMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The ring of submodules of the opposite algebra is isomorphic to the opposite ring of submodules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
span
is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets
on either side).
Equations
- Submodule.span.ringHom = { toFun := fun (s : SetSemiring A) => Submodule.span R (SetSemiring.down s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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
.
Equations
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
.
Equations
- Submodule.moduleSet R A = Module.mk ⋯ ⋯
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$.