Cancellation after tensoring with a field localization

Let R be a commutative semiring, let K be a localization of R that is a field, and let A be an R-algebra semiring. For an A-semimodule M, the localization M ⊗[R] K is again an A-semimodule. If P is finitely generated over R, then P ⊗[R] K cancels from A-linear equivalences of localizations: (M × P) ⊗[R] K ≃ (N × P) ⊗[R] K gives M ⊗[R] K ≃ N ⊗[R] K.

As an A-module P ⊗[R] K need not have finite length: for R = A = P = ℤ and K = ℚ, it is ℚ, which has infinite length over ℤ. Instead the localizations are modules over the ring K ⊗[R] A, with K acting on the right factor, and over this ring P ⊗[R] K has finite length because it is finite-dimensional over K. An A-linear map of localizations is R-linear, hence K-linear because K is a localization of R, hence K ⊗[R] A-linear; so cancellation of a summand of finite length over K ⊗[R] A applies.

For R = ℤ_p, K = ℚ_p and A = ℤ_p[G] this is the cancellation of rational representations of a finite group used to pass from a stable isomorphism of ℤ_p[G]-lattices to an isomorphism.

Main results

• TauCeti.IsLocalization.nonempty_tensor_linearEquiv_of_prod_tensor_linearEquiv: the localization of a semimodule that is finitely generated over R cancels from an A-linear equivalence of localizations at a field.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Proposition (5.6.11).

theorem TauCeti.IsLocalization.nonempty_tensor_linearEquiv_of_prod_tensor_linearEquiv {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (S : Submonoid R) (K : Type u_3) [Field K] [Algebra R K] [IsLocalization S K] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module.Finite R P] (h : Nonempty (TensorProduct R (M × P) K ≃ₗ[A] TensorProduct R (N × P) K)) : Nonempty (TensorProduct R M K ≃ₗ[A] TensorProduct R N K)

Cancellation after localization to a field. Let K be a localization of R at S that is a field, and let A be an R-algebra semiring. If P is finitely generated over R, an A-linear equivalence (M × P) ⊗[R] K ≃ (N × P) ⊗[R] K induces an A-linear equivalence M ⊗[R] K ≃ N ⊗[R] K. No finiteness is required of M and N. The semimodules M, N and P need only be additive commutative monoids; their localizations acquire additive inverses from the field action.