Reducing a module modulo an element of the ring #
Given a commutative ring R
and an element r : R
, the association
M ↦ M ⧸ rM
extends to a functor on the category of R
-modules. This functor
is isomorphic to the functor of tensoring by R ⧸ (r)
on either side, but can
be more convenient to work with since we can work with quotient types instead
of fiddling with simple tensors.
Tags #
module, commutative algebra
An abbreviation for M⧸rM
that keeps us from having to write
(⊤ : Submodule R M)
over and over to satisfy the typechecker.
Equations
- QuotSMulTop r M = (M ⧸ r • ⊤)
Instances For
If M'
is isomorphic to M''
as R
-modules, then M'⧸rM'
is isomorphic to M''⧸rM''
.
Equations
- QuotSMulTop.congr r e = Submodule.Quotient.equiv (r • ⊤) (r • ⊤) e ⋯
Instances For
Reducing a module modulo r
is the same as left tensoring with R/(r)
.
Equations
- QuotSMulTop.equivQuotTensor r M = ((r • ⊤).quotEquivOfEq (Ideal.span {r} • ⊤) ⋯).trans (TensorProduct.quotTensorEquivQuotSMul M (Ideal.span {r})).symm
Instances For
Reducing a module modulo r
is the same as right tensoring with R/(r)
.
Equations
- QuotSMulTop.equivTensorQuot r M = ((r • ⊤).quotEquivOfEq (Ideal.span {r} • ⊤) ⋯).trans (TensorProduct.tensorQuotEquivQuotSMul M (Ideal.span {r})).symm
Instances For
The action of the functor QuotSMulTop r
on morphisms.
Equations
- QuotSMulTop.map r = (r • ⊤).mapQLinear (r • ⊤) ∘ₗ LinearMap.codRestrict ((r • ⊤).compatibleMaps (r • ⊤)) LinearMap.id ⋯
Instances For
Tensoring on the left and applying QuotSMulTop · r
commute.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Tensoring on the right and applying QuotSMulTop · r
commute.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Let R
be a commutative ring, M
be an R
-module, S
be an R
-algebra, then
S ⊗[R] (M/rM)
is isomorphic to (S ⊗[R] M)⧸r(S ⊗[R] M)
as S
-modules.
Equations
- One or more equations did not get rendered due to their size.