The characteristice predicate of tensor product #
Main definitions #
is_tensor_product
: A predicate onf : M₁ →ₗ[R] M₂ →ₗ[R] M
expressing thatf
realizesM
as the tensor product ofM₁ ⊗[R] M₂
. This is defined by requiring the liftM₁ ⊗[R] M₂ → M
to be bijective.is_base_change
: A predicate on anR
-algebraS
and a mapf : M →ₗ[R] N
withN
being aS
-module, expressing thatf
realizesN
as the base change ofM
alongR → S
.
Main results #
tensor_product.is_base_change
:S ⊗[R] M
is the base change ofM
alongR → S
.
Given a bilinear map f : M₁ →ₗ[R] M₂ →ₗ[R] M
, is_tensor_product f
means that
M
is the tensor product of M₁
and M₂
via f
.
This is defined by requiring the lift M₁ ⊗[R] M₂ → M
to be bijective.
Equations
If M
is the tensor product of M₁
and M₂
, it is linearly equivalent to M₁ ⊗[R] M₂
.
Equations
- h.equiv = linear_equiv.of_bijective (tensor_product.lift f) _ _
If M
is the tensor product of M₁
and M₂
, we may lift a bilinear map M₁ →ₗ[R] M₂ →ₗ[R] M'
to a M →ₗ[R] M'
.
Equations
- h.lift f' = (tensor_product.lift f').comp h.equiv.symm.to_linear_map
The tensor product of a pair of linear maps between modules.
Equations
- hf.map hg i₁ i₂ = hg.equiv.to_linear_map.comp ((tensor_product.map i₁ i₂).comp hf.equiv.symm.to_linear_map)
Given an R
-algebra S
and an R
-module M
, an S
-module N
together with a map
f : M →ₗ[R] N
is the base change of M
to S
if the map S × M → N, (s, m) ↦ s • f m
is the
tensor product.
Equations
- is_base_change S f = is_tensor_product (linear_map.restrict_scalars R (⇑((algebra.of_id S (module.End S (M →ₗ[R] N))).to_linear_map.flip) f))
Suppose f : M →ₗ[R] N
is the base change of M
along R → S
. Then any R
-linear map from
M
to an S
-module factors thorugh f
.
Equations
- h.lift g = {to_fun := (is_tensor_product.lift h (linear_map.restrict_scalars R (⇑((algebra.of_id S (module.End S (M →ₗ[R] Q))).to_linear_map.flip) g))).to_fun, map_add' := _, map_smul' := _}
The base change of M
along R → S
is linearly equivalent to S ⊗[R] M
.