Kernel of a tensor product

Stream: Is there code for X?

[Wenrong Zou]

Hi, there is a result in math saying that: Let R be a commutative ring, the canonical map R → R ⊗[ℤ] ℚ is r ↦ r ⊗[ℤ] (1 : ℚ). Its kernel is precisely the ℤ-torsion submodule of R, i.e. the elements annihilated by some nonzero integer. I was wondering that is there a theorem in Mathlib related to this result. Thanks in advance!

import Mathlib

open TensorProduct LinearMap Submodule

-- Let R be any commutative ring.
variable (R : Type*) [CommRing R]

/--
The canonical `ℤ`-linear map from a ring `R` to `R ⊗[ℤ] ℚ`
that sends an element `r` to `r ⊗ 1`.
-/
def canonicalMapToTensorRat : R →ₗ[ℤ] (R ⊗[ℤ] ℚ) :=
  -- This is a curried form of the tensor product's universal bilinear map.
  (TensorProduct.mk ℤ R ℚ).flip 1

/--
The kernel of the canonical map `r ↦ r ⊗ 1` from a ring `R` to `R ⊗[ℤ] ℚ`
is precisely the `ℤ`-torsion submodule of `R`.
-/
theorem kernel_canonicalMapToTensorRat_eq_torsion :
    ker (canonicalMapToTensorRat R) = torsion ℤ R := by sorry

[Kenny Lau]

you can generalise from ring to AddCommGrp

[Kenny Lau]

you can gneralise from (Z, Q, torsion) to any ring R with (R, non zero divisors, R-torsion)

[Aaron Liu]

Kenny Lau said:

you can gneralise from (Z, Q, torsion) to any ring R with (R, non zero divisors, R-torsion)

I think it needs to be divisible by R

[Kenny Lau]

sorry i meant (Z, Q, torsion, AbGrp) to (R, Frac(R), R-torsion, R-Mod)

[Kenny Lau]

i forgot to say "localize"

[Wenrong Zou]

Thank you for help!

[Wenrong Zou]

I formalized part of proof in the version of (Z, Q, torsion, AbGrp), but I cannot solve one sorry.

import Mathlib

open TensorProduct LinearMap Submodule

-- Let R be any additive commutative group.
variable (R : Type*) [AddCommGroup R]

/--
The canonical `ℤ`-linear map from a ring `R` to `R ⊗[ℤ] ℚ`
that sends an element `r` to `r ⊗ 1`.
-/
def canonicalMapToTensorRat : R →ₗ[ℤ] (R ⊗[ℤ] ℚ) :=
  {
      toFun := fun r => r ⊗ₜ[ℤ] (1 : ℚ)
      map_add' := by
        intros x y
        simp [TensorProduct.add_tmul]
      map_smul' := by
        intros n x
        simp [TensorProduct.smul_tmul']
    }

/--
The kernel of the canonical map `r ↦ r ⊗ 1` from a ring `R` to `R ⊗[ℤ] ℚ`
is precisely the `ℤ`-torsion submodule of `R`.
-/
theorem kernel_canonicalMapToTensorRat_eq_torsion :
  ker (canonicalMapToTensorRat R) = torsion ℤ R := by
  refine Submodule.ext ?_
  intro x
  constructor
  · intro hx
    refine (mem_torsion_iff x).mpr ?_
    have aux : (canonicalMapToTensorRat R) x = 0 := by
      exact hx
    simp [canonicalMapToTensorRat] at aux

    sorry
  · intro hx
    simp [canonicalMapToTensorRat]
    obtain ⟨a, ha⟩ := (mem_torsion_iff x).mp hx
    calc
      _ = (a • x) ⊗ₜ (1 / (a : ℚ)) := by
        rw [smul_tmul]
        have aux : (a • (1 / (a : ℚ))) = 1 := by
          calc
            _ = a * (a : ℚ)⁻¹ := by
              aesop
            _ = 1 := by
              simp
        rw [aux]
      _ = 0 := by
        simp only [ha, one_div, zero_tmul]

[Aaron Liu]

Try the contrapositive

[Kenny Lau]

Wenrong Zou said:

AbGrp

your code still says CommRing

[Wenrong Zou]

Kenny Lau said:

Wenrong Zou said:

AbGrp

your code still says CommRing

Here, I want to use CommRing is because I also want to say the ring characteristics of

$$R \otimes_{\mathbb{Z}} \mathbb{Q}$$

is zero. We cannot define ringChar for R is AbGrp.

[Wenrong Zou]

Aaron Liu said:

Try the contrapositive

Thanks. I will try it.

[Antoine Chambert-Loir]

Just a remark that people will likely be tempted to request the analogous result in the context of an arbitrary docs#IsLocalization (your case will then follow from docs#Rat.IsFractionRing and docs#instIsLocalizationIntPosRat).

[Wenrong Zou]

Antoine Chambert-Loir said:

Just a remark that people will likely be tempted to request the analogous result in the context of an arbitrary docs#IsLocalization (your case will then follow from docs#Rat.IsFractionRing and docs#instIsLocalizationIntPosRat).

Thank you for your help! Using localization to describe it will be much better. Thanks.