Products of modules #
This file defines constructors for linear maps whose domains or codomains are products.
It contains theorems relating these to each other, as well as to Submodule.prod
, Submodule.map
,
Submodule.comap
, LinearMap.range
, and LinearMap.ker
.
Main definitions #
- products in the domain:
- products in the codomain:
- products in both domain and codomain:
LinearMap.prodMap
LinearEquiv.prodMap
LinearEquiv.skewProd
The first projection of a product is a linear map.
Instances For
The second projection of a product is a linear map.
Instances For
The prod of two linear maps is a linear map.
Instances For
Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.
See note [bundled maps over different rings] for why separate R
and S
semirings are used.
Instances For
The left injection into a product is a linear map.
Instances For
The right injection into a product is a linear map.
Instances For
The coprod function x : M × M₂ ↦ f x.1 + g x.2
is a linear map.
Instances For
Taking the product of two maps with the same codomain is equivalent to taking the product of their domains.
See note [bundled maps over different rings] for why separate R
and S
semirings are used.
Instances For
Split equality of linear maps from a product into linear maps over each component, to allow ext
to apply lemmas specific to M →ₗ M₃
and M₂ →ₗ M₃
.
See note [partially-applied ext lemmas].
prod.map
of two linear maps.
Instances For
LinearMap.prodMap
as a LinearMap
Instances For
LinearMap.prodMap
as an AlgHom
Instances For
M
as a submodule of M × N
.
Instances For
M
as a submodule of M × N
is isomorphic to M
.
Instances For
N
as a submodule of M × N
.
Instances For
N
as a submodule of M × N
is isomorphic to N
.
Instances For
Product of modules is commutative up to linear isomorphism.
Instances For
Four-way commutativity of prod
. The name matches mul_mul_mul_comm
.
Instances For
Product of linear equivalences; the maps come from Equiv.prodCongr
.
Instances For
Equivalence given by a block lower diagonal matrix. e₁
and e₂
are diagonal square blocks,
and f
is a rectangular block below the diagonal.
Instances For
If the union of the kernels ker f
and ker g
spans the domain, then the range of
Prod f g
is equal to the product of range f
and range g
.
Tunnels and tailings #
Some preliminary work for establishing the strong rank condition for noetherian rings.
Given a morphism f : M × N →ₗ[R] M
which is i : Injective f
,
we can find an infinite decreasing tunnel f i n
of copies of M
inside M
,
and sitting beside these, an infinite sequence of copies of N
.
We picturesquely name these as tailing f i n
for each individual copy of N
,
and tailings f i n
for the supremum of the first n+1
copies:
they are the pieces left behind, sitting inside the tunnel.
By construction, each tailing f i (n+1)
is disjoint from tailings f i n
;
later, when we assume M
is noetherian, this implies that N
must be trivial,
and establishes the strong rank condition for any left-noetherian ring.
An auxiliary construction for tunnel
.
The composition of f
, followed by the isomorphism back to K
,
followed by the inclusion of this submodule back into M
.
Instances For
Auxiliary definition for tunnel
.
Equations
- One or more equations did not get rendered due to their size.
- LinearMap.tunnel' f i 0 = { fst := ⊤, snd := LinearEquiv.ofTop ⊤ (_ : ⊤ = ⊤) }
Instances For
Give an injective map f : M × N →ₗ[R] M
we can find a nested sequence of submodules
all isomorphic to M
.
Instances For
Give an injective map f : M × N →ₗ[R] M
we can find a sequence of submodules
all isomorphic to N
.
Instances For
Each tailing f i n
is a copy of N
.
Instances For
The supremum of all the copies of N
found inside the tunnel.
Instances For
Graph of a linear map.