Cokernels commute with tensor products, heterobasically

Tensoring is right exact: for a linear map f : M' → M and a module N, the cokernel of f ⊗ 𝟙 N is (M ⧸ range f) ⊗ N. Mathlib proves this over a commutative ring, as the exactness of the tensored pair (rTensor_exact) and as the isomorphism LinearMap.rTensor.equiv. When M' and M are modules over an R-algebra A and f is A-linear, the comparison isomorphism is A-linear for the module structure of TensorProduct.AlgebraTensorModule on the left factor, and this file records that heterobasic form.

For the cokernel M ⧸ rM = QuotSMulTop r M of multiplication by a scalar r, the base change A ⊗[R] (M ⧸ rM) is the cokernel of multiplication by the image of r on A ⊗[R] M. When r maps to 0 in A that cokernel is all of A ⊗[R] M, so the base change of the quotient map M → M ⧸ rM is bijective (QuotSMulTop.baseChange_mkQ_bijective), and A ⊗[R] M is finitely generated over A as soon as M ⧸ rM is finitely generated over R (QuotSMulTop.finite_baseChange). For R = ℤ and a ring A of characteristic ℓ, this says that A ⊗[ℤ] M only depends on M ⧸ ℓM, and is finitely generated when M ⧸ ℓM is finite (TauCeti.finite_baseChange_of_finite_quotSMulTop), even when M is not finitely generated.

For a map of modules over a commutative ring, the same right exactness identifies scalar extension of its cokernel with the cokernel of its scalar extension. This is the module form of Stacks Project, Lemma 10.12.10, Tag 00DF.

The heterobasic version is what identifies the base change of a module presented by generators and relations over a noncommutative algebra A with the module presented by the base-changed relations, for instance the rationalisation of a module over an integral group ring ℤ_p[G].

Main definitions

• TensorProduct.AlgebraTensorModule.quotientRangeTensorEquiv: the A-linear isomorphism (M ⧸ range f) ⊗[R] N ≃ₗ[A] (M ⊗[R] N) ⧸ range (f ⊗ 𝟙 N).
• TensorProduct.AlgebraTensorModule.tensorQuotEquivQuotMapSMul: the S-linear isomorphism N ⊗[R] (R ⧸ I) ≃ N ⧸ I S • N for an S-module N.
• LinearMap.cokernelBaseChangeEquiv: the S-linear isomorphism S ⊗[R] cokernel f ≃ₗ[S] cokernel (S ⊗[R] f).

Main results

• TensorProduct.exists_one_tmul_eq: every element of (R ⧸ I) ⊗ M is 1 ⊗ x.
• TensorProduct.one_tmul_eq_zero_iff_exists_smul_eq: 1 ⊗ x vanishes in (R ⧸ (r)) ⊗ M exactly when x is a multiple of r.
• TensorProduct.mk_one_bijective_of_ker_le_annihilator: if R → S is surjective and its kernel annihilates M, then x ↦ 1 ⊗ x is a bijection M → S ⊗[R] M.
• LinearMap.exact_lTensor_quotient_span_singleton: if a : M → N and b : N → M compose in both orders to multiplication by r, and r is regular on M, then the reductions of b and a modulo r form an exact pair.
• LinearMap.exact_comp_baseChange_quotient_span_singleton: under the same hypotheses, with r regular on R and N projective, the R ⧸ (r)-duals of these reductions form an exact pair.
• TensorProduct.AlgebraTensorModule.ker_rTensor_mkQ: the kernel of the tensored quotient map mkQ ⊗ 𝟙 N is the range of f ⊗ 𝟙 N.
• TensorProduct.AlgebraTensorModule.rTensor_mkQ_surjective: the tensored quotient map is surjective.
• TensorProduct.AlgebraTensorModule.ker_lTensor_mkQ_smul_top and TensorProduct.AlgebraTensorModule.ker_rTensor_mkQ_smul_top: tensoring the quotient map by a scalar on either factor has kernel the multiples of that scalar.
• TensorProduct.AlgebraTensorModule.range_lTensor_subtype_smul_top_le: the image of N ⊗[R] I M in N ⊗[R] M lies in J (N ⊗[R] M) when I S ≤ J.
• Submodule.baseChange_eq_top_iff_subsingleton: the extension of scalars of p ≤ M to A is all of A ⊗[R] M exactly when A ⊗[R] (M ⧸ p) = 0.
• QuotSMulTop.baseChange_mkQ_bijective: if r maps to 0 in A, the base change of M → M ⧸ rM to A is bijective.
• QuotSMulTop.finite_baseChange: if r maps to 0 in A and M ⧸ rM is finitely generated, then so is A ⊗[R] M.
• TauCeti.finite_baseChange_of_finite_quotSMulTop: in characteristic ℓ, k ⊗_ℤ V is finitely generated over k when V ⧸ ℓV is finite.

theorem TensorProduct.exists_one_tmul_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (y : TensorProduct R (R ⧸ I) M) : ∃ (x : M), 1 ⊗ₜ[R] x = y

Every element of (R ⧸ I) ⊗[R] M is of the form 1 ⊗ x.

@[simp]

theorem TensorProduct.one_tmul_eq_zero_iff_exists_smul_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (r : R) (x : M) : 1 ⊗ₜ[R] x = 0 ↔ ∃ (y : M), r • y = x

In (R ⧸ (r)) ⊗[R] M, the element 1 ⊗ x vanishes exactly when x is a multiple of r.

theorem TensorProduct.mk_one_bijective_of_ker_le_annihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u_3} [CommRing S] [Algebra R S] (hS : Function.Surjective ⇑(algebraMap R S)) (hM : RingHom.ker (algebraMap R S) ≤ Module.annihilator R M) : Function.Bijective ⇑((mk R S M) 1)

Base change to a quotient ring that already acts. If R → S is surjective and its kernel annihilates M, then x ↦ 1 ⊗ x is a bijection M → S ⊗[R] M: writing S = R ⧸ I, the tensor product is M ⧸ I M = M.

theorem LinearMap.exact_lTensor_quotient_span_singleton {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {r : R} (a : M →ₗ[R] N) (b : N →ₗ[R] M) (hab : a ∘ₗ b = r • id) (hba : b ∘ₗ a = r • id) (hr : IsSMulRegular M r) : Function.Exact ⇑(lTensor (R ⧸ Ideal.span {r}) b) ⇑(lTensor (R ⧸ Ideal.span {r}) a)

Reductions of a factorization of a regular scalar are exact. Let a : M → N and b : N → M satisfy a ∘ b = r • id and b ∘ a = r • id, with r regular on M. Then the reductions (R ⧸ (r)) ⊗ b and (R ⧸ (r)) ⊗ a form an exact pair: if a x ∈ rN, say a x = r • n, then r • b n = b (a x) = r • x, so x = b n.

theorem LinearMap.exact_comp_baseChange_quotient_span_singleton {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Projective R N] {r : R} (a : M →ₗ[R] N) (b : N →ₗ[R] M) (hab : a ∘ₗ b = r • id) (hba : b ∘ₗ a = r • id) (hr : IsSMulRegular R r) : Function.Exact (fun (ψ : TensorProduct R (R ⧸ Ideal.span {r}) M →ₗ[R ⧸ Ideal.span {r}] R ⧸ Ideal.span {r}) => ψ ∘ₗ baseChange (R ⧸ Ideal.span {r}) b) fun (φ : TensorProduct R (R ⧸ Ideal.span {r}) N →ₗ[R ⧸ Ideal.span {r}] R ⧸ Ideal.span {r}) => φ ∘ₗ baseChange (R ⧸ Ideal.span {r}) a

Reductions of a factorization of a regular scalar are dually exact. Let a : M → N and b : N → M satisfy a ∘ b = r • id and b ∘ a = r • id, with r regular on R and N projective. Then the R ⧸ (r)-duals of the reductions of a and b modulo r form an exact pair: a functional on (R ⧸ (r)) ⊗ N vanishing on the image of the reduction of a factors through the reduction of b. Together with LinearMap.exact_lTensor_quotient_span_singleton, this says that reducing a matrix factorization modulo a non-zero-divisor gives a totally acyclic periodic complex.

theorem TensorProduct.AlgebraTensorModule.rTensor_mkQ_surjective {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (p : Submodule A M) : Function.Surjective ⇑((rTensor R N) p.mkQ)

The tensored quotient map mkQ ⊗ 𝟙 N is surjective.

theorem TensorProduct.AlgebraTensorModule.ker_rTensor_mkQ {R : Type u_1} {A : Type u_2} {M : Type u_3} {M' : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] [AddCommGroup N] [Module R N] (f : M' →ₗ[A] M) : ((rTensor R N) f.range.mkQ).ker = ((rTensor R N) f).range

Tensoring the exact pair M' → M → M ⧸ range f with N keeps it exact: the kernel of mkQ ⊗ 𝟙 N is the range of f ⊗ 𝟙 N, as A-submodules of M ⊗[R] N.

noncomputable def TensorProduct.AlgebraTensorModule.quotientRangeTensorEquiv {R : Type u_1} {A : Type u_2} {M : Type u_3} {M' : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] [AddCommGroup N] [Module R N] (f : M' →ₗ[A] M) : TensorProduct R (M ⧸ f.range) N ≃ₗ[A] TensorProduct R M N ⧸ ((rTensor R N) f).range

Cokernels commute with tensor products. For an A-linear map f : M' → M and an R-module N, the base change (M ⧸ range f) ⊗[R] N of the cokernel of f is the cokernel of f ⊗ 𝟙 N, as left A-modules.

@[simp]

theorem TensorProduct.AlgebraTensorModule.quotientRangeTensorEquiv_mk_tmul {R : Type u_1} {A : Type u_2} {M : Type u_3} {M' : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] [AddCommGroup N] [Module R N] (f : M' →ₗ[A] M) (x : M) (n : N) : (quotientRangeTensorEquiv f) (Submodule.Quotient.mk x ⊗ₜ[R] n) = Submodule.Quotient.mk (x ⊗ₜ[R] n)

@[simp]

theorem TensorProduct.AlgebraTensorModule.quotientRangeTensorEquiv_symm_mk_tmul {R : Type u_1} {A : Type u_2} {M : Type u_3} {M' : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup M'] [Module R M'] [Module A M'] [IsScalarTower R A M'] [AddCommGroup N] [Module R N] (f : M' →ₗ[A] M) (x : M) (n : N) : (quotientRangeTensorEquiv f).symm (Submodule.Quotient.mk (x ⊗ₜ[R] n)) = Submodule.Quotient.mk x ⊗ₜ[R] n

noncomputable def TensorProduct.AlgebraTensorModule.tensorQuotEquivQuotMapSMul {R : Type u_1} {S : Type u_2} {N : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (I : Ideal R) : TensorProduct R N (R ⧸ I) ≃ₗ[S] N ⧸ Ideal.map (algebraMap R S) I • ⊤

The S-linear isomorphism N ⊗[R] (R ⧸ I) ≃ N ⧸ I S • N for an S-module N and an ideal I of R. It upgrades Mathlib's TensorProduct.tensorQuotEquivQuotSMul, which is R-linear with target N ⧸ I • N.

@[simp]

theorem TensorProduct.AlgebraTensorModule.tensorQuotEquivQuotMapSMul_tmul_mk {R : Type u_1} {S : Type u_2} {N : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (I : Ideal R) (n : N) (r : R) : (tensorQuotEquivQuotMapSMul I) (n ⊗ₜ[R] (Ideal.Quotient.mk I) r) = Submodule.Quotient.mk (r • n)

@[simp]

theorem TensorProduct.AlgebraTensorModule.tensorQuotEquivQuotMapSMul_symm_mk {R : Type u_1} {S : Type u_2} {N : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (I : Ideal R) (n : N) : (tensorQuotEquivQuotMapSMul I).symm (Submodule.Quotient.mk n) = n ⊗ₜ[R] 1

The inverse of tensorQuotEquivQuotMapSMul sends the class of n to n ⊗ 1.

theorem TensorProduct.AlgebraTensorModule.lTensor_mkQ_surjective {R : Type u_1} {S : Type u_2} {N : Type u_3} {M : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] [AddCommGroup M] [Module R M] (p : Submodule R M) : Function.Surjective ⇑((lTensor S N) p.mkQ)

The tensored quotient map 𝟙 N ⊗ mkQ is surjective.

theorem TensorProduct.AlgebraTensorModule.ker_lTensor_mkQ_smul_top {R : Type u_1} {S : Type u_2} {N : Type u_3} {M : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] [AddCommGroup M] [Module R M] (x : R) : ((lTensor S N) (x • ⊤).mkQ).ker = (algebraMap R S) x • ⊤

Dividing M by x corresponds to dividing N ⊗[R] M by the image of x in S: the kernel of 𝟙 N ⊗ mkQ : N ⊗[R] M → N ⊗[R] (M ⧸ x M) is x (N ⊗[R] M).

theorem TensorProduct.AlgebraTensorModule.ker_rTensor_mkQ_smul_top {R : Type u_1} {S : Type u_2} {N : Type u_3} {M : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] [AddCommGroup M] [Module R M] (y : S) : ((rTensor R M) (y • ⊤).mkQ).ker = y • ⊤

The kernel of mkQ ⊗ 𝟙 M : N ⊗[R] M → (N ⧸ y N) ⊗[R] M is y (N ⊗[R] M).

theorem TensorProduct.AlgebraTensorModule.range_lTensor_subtype_smul_top_le {R : Type u_1} {S : Type u_2} {N : Type u_3} {M : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] [AddCommGroup M] [Module R M] {I : Ideal R} {J : Ideal S} (hIJ : Ideal.map (algebraMap R S) I ≤ J) : ((lTensor S N) (I • ⊤).subtype).range ≤ J • ⊤

If I S ≤ J, the image of N ⊗[R] I M in N ⊗[R] M lies in J (N ⊗[R] M).

noncomputable def LinearMap.cokernelBaseChangeEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : TensorProduct R S (N ⧸ f.range) ≃ₗ[S] TensorProduct R S N ⧸ (baseChange S f).range

Cokernels commute with scalar extension. The scalar extension of the cokernel of an R-linear map is canonically the cokernel of its scalar extension. No flatness hypothesis is needed.

@[simp]

theorem LinearMap.cokernelBaseChangeEquiv_tmul {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (s : S) (n : N) : f.cokernelBaseChangeEquiv (s ⊗ₜ[R] Submodule.Quotient.mk n) = Submodule.Quotient.mk (s ⊗ₜ[R] n)

The cokernel base-change equivalence sends a pure tensor represented by n to the class of the corresponding pure tensor.

@[simp]

theorem LinearMap.cokernelBaseChangeEquiv_symm_mk_tmul {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (s : S) (n : N) : f.cokernelBaseChangeEquiv.symm (Submodule.Quotient.mk (s ⊗ₜ[R] n)) = s ⊗ₜ[R] Submodule.Quotient.mk n

The inverse cokernel base-change equivalence sends the class of a pure tensor to the pure tensor represented by its class.

theorem LinearMap.cokernel_baseChange_square {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [AddCommMonoid M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : ↑f.cokernelBaseChangeEquiv ∘ₗ baseChange S f.range.mkQ = (baseChange S f).range.mkQ

The cokernel base-change equivalence intertwines the base-changed quotient map with the quotient map of the base-changed linear map.

theorem Submodule.baseChange_eq_top_iff_subsingleton {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [Ring A] [Algebra R A] (p : Submodule R M) : baseChange A p = ⊤ ↔ Subsingleton (TensorProduct R A (M ⧸ p))

The extension of scalars p.baseChange A of a submodule p ≤ M is all of A ⊗[R] M exactly when the base change A ⊗[R] (M ⧸ p) of the quotient vanishes.

theorem QuotSMulTop.baseChange_mkQ_bijective {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {r : R} (hr : (algebraMap R A) r = 0) : Function.Bijective ⇑(LinearMap.baseChange A (r • ⊤).mkQ)

Base change kills reduction modulo a vanishing scalar. If r : R maps to 0 in the R-algebra A, the base change A ⊗[R] M → A ⊗[R] (M ⧸ rM) of the quotient map is bijective.

theorem QuotSMulTop.finite_baseChange {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {r : R} (hr : (algebraMap R A) r = 0) [Module.Finite R (QuotSMulTop r M)] : Module.Finite A (TensorProduct R A M)

Finiteness of a base change killing a scalar. If r : R maps to 0 in the R-algebra A and M ⧸ rM is finitely generated over R, then A ⊗[R] M is finitely generated over A: it is isomorphic to A ⊗[R] (M ⧸ rM) (QuotSMulTop.baseChange_mkQ_bijective).

theorem TauCeti.finite_baseChange_of_finite_quotSMulTop (k : Type u_1) [Ring k] (ℓ : ℕ) [CharP k ℓ] (V : Type u_2) [AddCommGroup V] [Finite (QuotSMulTop (↑ℓ) V)] : Module.Finite k (TensorProduct ℤ k V)

Finiteness of the reduction in characteristic ℓ. If k has characteristic ℓ and V ⧸ ℓV is finite, then k ⊗_ℤ V is finitely generated over k, even when V is not.