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.
Equations
- LinearMap.fst R M M₂ = { toFun := Prod.fst, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The second projection of a product is a linear map.
Equations
- LinearMap.snd R M M₂ = { toFun := Prod.snd, map_add' := ⋯, map_smul' := ⋯ }
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left injection into a product is a linear map.
Equations
- LinearMap.inl R M M₂ = LinearMap.id.prod 0
Instances For
The right injection into a product is a linear map.
Equations
- LinearMap.inr R M M₂ = LinearMap.prod 0 LinearMap.id
Instances For
The coprod function x : M × M₂ ↦ f x.1 + g x.2
is a linear map.
Equations
- f.coprod g = f ∘ₗ LinearMap.fst R M M₂ + g ∘ₗ LinearMap.snd R M M₂
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- f.prodMap g = (f ∘ₗ LinearMap.fst R M M₂).prod (g ∘ₗ LinearMap.snd R M M₂)
Instances For
LinearMap.prodMap
as a LinearMap
Equations
Instances For
LinearMap.prodMap
as a RingHom
Equations
Instances For
LinearMap.prodMap
as an AlgHom
Equations
- LinearMap.prodMapAlgHom R M M₂ = { toRingHom := LinearMap.prodMapRingHom R M M₂, commutes' := ⋯ }
Instances For
M
as a submodule of M × N
.
Equations
- Submodule.fst R M M₂ = Submodule.comap (LinearMap.snd R M M₂) ⊥
Instances For
M
as a submodule of M × N
is isomorphic to M
.
Equations
- Submodule.fstEquiv R M M₂ = { toFun := fun (x : ↥(Submodule.fst R M M₂)) => (↑x).1, map_add' := ⋯, map_smul' := ⋯, invFun := fun (m : M) => ⟨(m, 0), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
N
as a submodule of M × N
.
Equations
- Submodule.snd R M M₂ = Submodule.comap (LinearMap.fst R M M₂) ⊥
Instances For
N
as a submodule of M × N
is isomorphic to N
.
Equations
- Submodule.sndEquiv R M M₂ = { toFun := fun (x : ↥(Submodule.snd R M M₂)) => (↑x).2, map_add' := ⋯, map_smul' := ⋯, invFun := fun (n : M₂) => ⟨(0, n), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
Product of modules is commutative up to linear isomorphism.
Equations
- LinearEquiv.prodComm R M N = { toFun := Prod.swap, map_add' := ⋯, map_smul' := ⋯, invFun := AddEquiv.prodComm.invFun, left_inv := ⋯, right_inv := ⋯ }
Instances For
Four-way commutativity of prod
. The name matches mul_mul_mul_comm
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Product of linear equivalences; the maps come from Equiv.prodCongr
.
Equations
- e₁.prod e₂ = { toFun := (e₁.toAddEquiv.prodCongr e₂.toAddEquiv).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (e₁.toAddEquiv.prodCongr e₂.toAddEquiv).invFun, left_inv := ⋯, right_inv := ⋯ }
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.
Equations
- One or more equations did not get rendered due to their size.
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 #
NOTE: The proof of strong rank condition for noetherian rings is changed.
LinearMap.tunnel
and LinearMap.tailing
are not used in mathlib anymore.
These are marked as deprecated with no replacements.
If you use them in external projects, please consider using other arguments instead.
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
.
Equations
- f.tunnelAux Kφ = (Kφ.fst.subtype ∘ₗ ↑Kφ.snd.symm) ∘ₗ f
Instances For
Auxiliary definition for tunnel
.
Equations
- One or more equations did not get rendered due to their size.
- f.tunnel' i 0 = ⟨⊤, 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
.
Equations
Instances For
Give an injective map f : M × N →ₗ[R] M
we can find a sequence of submodules
all isomorphic to N
.
Equations
- f.tailing i n = Submodule.map (f.tunnelAux (f.tunnel' i n)) (Submodule.snd R M N)
Instances For
Each tailing f i n
is a copy of N
.
Equations
- f.tailingLinearEquiv i n = (Submodule.equivMapOfInjective (f.tunnelAux (f.tunnel' i n)) ⋯ (Submodule.snd R M N)).symm.trans (Submodule.sndEquiv R M N)
Instances For
The supremum of all the copies of N
found inside the tunnel.
Equations
- f.tailings i = ⇑(partialSups (f.tailing i))
Instances For
Graph of a linear map.