The rank of a module tensored with a localization

Localizing a module at a submonoid of non-zero-divisors does not change its rank over the base ring (IsLocalizedModule.finrank_eq), and tensoring with the localization A of R is such a localization (IsLocalization.tensorProduct_isLocalizedModule). Mathlib states this for A ⊗[R] M; this file records the same formula for M ⊗[R] A, the form in which a rationalization M ⊗[ℤ_p] ℚ_p of a ℤ_p-module is written. Since M ⊗[R] A is an A-module on which R acts through A, its R-rank is also its A-rank; for A a field this is the dimension of the vector space M ⊗[R] A.

Conversely, over a domain the rank detects isomorphisms after passing to the field of fractions: an injective linear map between finite modules of the same rank becomes an injective map between vector spaces of the same finite dimension after tensoring with the field of fractions, hence an isomorphism. This is how an integral lattice of full rank in a module computes its rationalization. The map may be linear over any R-algebra A, and its rationalization is then A-linear for the module structure of TensorProduct.AlgebraTensorModule on the left factor.

In the other direction, an A-linear map of rationalizations M ⊗ Q → N ⊗ Q becomes integral after multiplying by a non-zero-divisor of R, provided M is finitely generated over A and N is torsion-free. So a rational embedding of lattices restricts, after scaling, to an integral embedding.

A finitely generated module over a domain contains a free submodule of full rank whose quotient is torsion. This repackages Mathlib's exists_linearIndepOn_smul_mem_span, which selects a linearly independent subfamily of a generating family, with Fin n-indexing and the rank equality, the latter read off rank_quotient_add_rank_of_isDomain.

Main results

• TauCeti.IsLocalization.finrank_tensorProduct: finrank R (M ⊗[R] A) = finrank R M for a localization A of R at a submonoid of non-zero-divisors.
• TauCeti.IsFractionRing.rTensor_bijective_of_injective_of_finrank_eq: an injective linear map f : M → N with N finite and finrank R M = finrank R N over a domain R becomes bijective after tensoring with the field of fractions of R.
• TauCeti.IsFractionRing.tmul_one_injective: a torsion-free module embeds in its rationalization.
• TauCeti.IsFractionRing.exists_linearMap_tmul_one_eq_smul: a multiple of an A-linear map of rationalizations by a non-zero-divisor is the rationalization of an A-linear map.
• TauCeti.IsFractionRing.exists_injective_linearMap_of_injective: an injective A-linear map of rationalizations of torsion-free modules gives an injective A-linear map of the modules.
• TauCeti.exists_linearIndependent_smul_mem_span: a finitely generated module over a domain contains a free submodule of full rank with torsion quotient.

theorem TauCeti.IsLocalization.finrank_tensorProduct {R : Type u_1} [CommRing R] (S : Submonoid R) (A : Type u_2) [CommRing A] [Algebra R A] [IsLocalization S A] (hS : S ≤ nonZeroDivisors R) (M : Type u_3) [AddCommGroup M] [Module R M] : Module.finrank R (TensorProduct R M A) = Module.finrank R M

Tensoring with a localization at a submonoid of non-zero-divisors does not change the rank over the base ring.

theorem TauCeti.IsFractionRing.rTensor_bijective_of_injective_of_finrank_eq {R : Type u_1} [CommRing R] [IsDomain R] (Q : Type u_2) [CommRing Q] [Algebra R Q] [IsFractionRing R Q] {A : Type u_3} [Ring A] [Algebra R A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] [Module.Finite R N] (f : M →ₗ[A] N) (hf : Function.Injective ⇑f) (h : Module.finrank R M = Module.finrank R N) : Function.Bijective ⇑((TensorProduct.AlgebraTensorModule.rTensor R Q) f)

Full-rank injections become isomorphisms over the field of fractions. Let R be a domain with field of fractions Q, and f : M → N an injective A-linear map, for an R-algebra A, where N is finite over R and M has the same rank as N. Then f ⊗ 𝟙 Q is bijective: it is injective because Q is flat over R, and it is an injective map between Q-vector spaces of the same finite dimension.

theorem TauCeti.IsFractionRing.tmul_one_injective {R : Type u_1} [CommRing R] (Q : Type u_2) [CommRing Q] [Algebra R Q] [IsFractionRing R Q] {M : Type u_4} [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] : Function.Injective fun (m : M) => m ⊗ₜ[R] 1

A torsion-free module embeds in its rationalization: m ↦ m ⊗ 1 is injective, since it is the localization of M at the non-zero-divisors of R.

theorem TauCeti.IsFractionRing.exists_linearMap_tmul_one_eq_smul {R : Type u_1} [CommRing R] (Q : Type u_2) [CommRing Q] [Algebra R Q] [IsFractionRing R Q] {A : Type u_3} [Ring A] [Algebra R A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] [Module.Finite A M] [Module.IsTorsionFree R N] (φ : TensorProduct R M Q →ₗ[A] TensorProduct R N Q) : ∃ s ∈ nonZeroDivisors R, ∃ (f : M →ₗ[A] N), ∀ (m : M), f m ⊗ₜ[R] 1 = s • φ (m ⊗ₜ[R] 1)

Clearing denominators of a rational map. Let R have field of fractions Q, let A be an R-algebra, and let φ : M ⊗ Q → N ⊗ Q be A-linear, where M is finitely generated over A and N is torsion-free over R. Then some multiple s • φ by a non-zero-divisor s of R is the rationalization of an A-linear map f : M → N, in the sense that f m ⊗ 1 = s • φ (m ⊗ 1).

theorem TauCeti.IsFractionRing.exists_injective_linearMap_of_injective {R : Type u_1} [CommRing R] (Q : Type u_2) [CommRing Q] [Algebra R Q] [IsFractionRing R Q] {A : Type u_3} [Ring A] [Algebra R A] {M : Type u_4} {N : Type u_5} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] [Module.Finite A M] [Module.IsTorsionFree R M] [Module.IsTorsionFree R N] (φ : TensorProduct R M Q →ₗ[A] TensorProduct R N Q) (hφ : Function.Injective ⇑φ) : ∃ (f : M →ₗ[A] N), Function.Injective ⇑f

Rational embeddings of lattices come from integral ones. If M is finitely generated over the R-algebra A, both M and N are torsion-free over R, and some A-linear map of rationalizations M ⊗ Q → N ⊗ Q is injective, then so is some A-linear map M → N.

theorem TauCeti.exists_linearIndependent_smul_mem_span {A : Type u_1} {M : Type u_2} [CommRing A] [IsDomain A] [AddCommGroup M] [Module A M] [Module.Finite A M] : ∃ (n : ℕ) (v : Fin n → M) (c : A), LinearIndependent A v ∧ c ≠ 0 ∧ (∀ (m : M), c • m ∈ Submodule.span A (Set.range v)) ∧ Module.finrank A M = n

A finitely generated module M over a domain contains a free submodule F of the rank of M with M ⧸ F torsion: some nonzero c multiplies M into F.

This repackages Mathlib's exists_linearIndepOn_smul_mem_span with Fin n-indexing and the rank equality.