Documentation

TauCeti.RingTheory.Subring.RationalBaseChange

Extending the scalars of a subring of a rational algebra #

Let A be a ℚ-algebra and R a subring of A. Because R is a ring and not a ℚ-subalgebra, it can be a genuine lattice: an integral structure whose rational span is all of A. This file builds the comparison map

ratBaseChange R : ℚ ⊗[ℤ] R →ₐ[ℚ] A,     q ⊗ₜ r ↦ q • r

records that its range is exactly the ℚ-span of R, and proves that it is always injective. Consequently it is an isomorphism exactly when that span is everything, which is what it means for R to be a ℤ-form of A.

Injectivity holds with no hypothesis on R and is the reason the file exists: every element of ℚ ⊗[ℤ] M, for any additive group M, has a common denominator, so it is a single elementary tensor (n : ℚ)⁻¹ ⊗ₜ m rather than a sum of them. That normal form, TauCeti.exists_tmul_inv_natCast, is proved first and is purely module-theoretic. It also turns the spanning hypothesis into the concrete statement Subring.exists_natCast_smul_mem, that every element of A is carried into R by some nonzero natural number.

Main definitions #

Main results #

A common denominator in ℚ ⊗[ℤ] M #

source
theorem TauCeti.exists_tmul_inv_natCast {M : Type u_1} [AddCommGroup M] (z : TensorProduct ℤ ℚ M) :
∃ (n : ℕ) (m : M), n ≠ 0 ∧ z = (↑n)⁻¹ ⊗ₜ[ℤ] m

Every element of ℚ ⊗[ℤ] M is a single elementary tensor with a natural-number denominator: the rational coefficients of a finite sum can be put over a common denominator, and the numerators absorbed into the right-hand factor.

This is IsLocalizedModule.mk'_surjective read through IsLocalization.tensorProduct_isLocalizedModule, which exhibits ℚ ⊗[ℤ] M as the localization of M at the positive integers; the denominator produced there is a positive integer, and its absolute value is the natural number below.

The comparison map #

source
noncomputable def Subring.ratBaseChange {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) :
TensorProduct ℤ ℚ ↥R →ₐ[ℚ] A

The canonical ℚ-algebra map ℚ ⊗[ℤ] R → A extending the inclusion of a subring of a ℚ-algebra. It sends q ⊗ₜ r to q • r.

Equations
Instances For
    source
    @[simp]
    theorem Subring.ratBaseChange_tmul {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) (q : ℚ) (r : ↥R) :
    R.ratBaseChange (q ⊗ₜ[ℤ] r) = q • ↑r
    source
    theorem Subring.ratBaseChange_injective {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) :
    Function.Injective ⇑R.ratBaseChange

    The comparison map is injective for every subring: a common denominator can be cleared, and a nonzero rational scalar acts injectively on the ℚ-algebra A.

    source
    theorem Subring.range_ratBaseChange {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) :
    R.ratBaseChange.toLinearMap.range = Submodule.span ℚ ↑R

    The range of the comparison map is the ℚ-span of the subring: the map is the base change of the inclusion of R, whose range is R itself.

    source
    theorem Subring.ratBaseChange_surjective_iff {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) :
    Function.Surjective ⇑R.ratBaseChange ↔ Submodule.span ℚ ↑R = ⊤

    The comparison map is surjective exactly when the subring spans the ambient algebra over ℚ.

    source
    theorem Subring.ratBaseChange_bijective {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) (h : Submodule.span ℚ ↑R = ⊤) :
    Function.Bijective ⇑R.ratBaseChange

    The comparison map is bijective for a spanning subring.

    source
    noncomputable def Subring.ratBaseChangeEquiv {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) (h : Submodule.span ℚ ↑R = ⊤) :
    TensorProduct ℤ ℚ ↥R ≃ₐ[ℚ] A

    A spanning subring is a ℤ-form of the ambient ℚ-algebra: extending its scalars to ℚ recovers that algebra.

    Equations
    Instances For
      source
      @[simp]
      theorem Subring.ratBaseChangeEquiv_tmul {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) (h : Submodule.span ℚ ↑R = ⊤) (q : ℚ) (r : ↥R) :
      (R.ratBaseChangeEquiv h) (q ⊗ₜ[ℤ] r) = q • ↑r
      source
      theorem Subring.exists_natCast_smul_mem {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) (h : Submodule.span ℚ ↑R = ⊤) (a : A) :
      ∃ (n : ℕ), n ≠ 0 ∧ ↑n • a ∈ R

      Denominators can be cleared in a spanning subring: every element of the ambient algebra is carried into it by some nonzero natural number.

      source
      theorem Subring.span_eq_top_iff_exists_natCast_smul_mem {A : Type u_1} [Ring A] [Algebra ℚ A] (R : Subring A) :
      Submodule.span ℚ ↑R = ⊤ ↔ ∀ (a : A), ∃ (n : ℕ), n ≠ 0 ∧ ↑n • a ∈ R

      A subring spans its ambient ℚ-algebra exactly when denominators can be cleared: every element is carried into the subring by some nonzero natural number. This is the form of the spanning hypothesis that a consumer checks in practice.