Documentation

TauCeti.NumberTheory.NumberField.Global.Places.ScalarExtension

Scalar extension at places of a number field #

This file defines the scalar extension of a vector space over a number field to a finite completion, to ℝ through a real place, and to ℂ through a chosen infinite-place embedding.

These are the local vector spaces K_v ⊗[K] V attached to a global vector space V. They are shared by the localization of quadratic forms at the places of K and by weak approximation of vectors at finite and real places, so that both speak about the same local spaces. Their finite dimensions are preserved by each scalar extension.

Main results #

source
@[reducible, inline]
abbrev IsDedekindDomain.HeightOneSpectrum.FiniteScalarExtension {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
Type (max u v)

The scalar extension of V to the finite completion of K at v.

Instances For
    source
    @[simp]
    theorem IsDedekindDomain.HeightOneSpectrum.finrank_FiniteScalarExtension {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [NumberField K] [FiniteDimensional K V] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    Module.finrank (adicCompletion K v) v.FiniteScalarExtension = Module.finrank K V

    The finite rank of V is unchanged by extension to a finite-place completion.

    source
    @[reducible, inline]
    abbrev TauCeti.RealScalarExtension {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (w : { w : NumberField.InfinitePlace K // w.IsReal }) :
    Type v

    The scalar extension of V to ℝ through the embedding belonging to a real place.

    Instances For
      source
      @[reducible, inline]
      abbrev NumberField.InfinitePlace.ComplexScalarExtension {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] (w : InfinitePlace K) :
      Type v

      The scalar extension of V to ℂ through the chosen embedding of an infinite place.

      Instances For
        source
        @[simp]
        theorem NumberField.InfinitePlace.finrank_ComplexScalarExtension {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (w : InfinitePlace K) :
        Module.finrank ℂ w.ComplexScalarExtension = Module.finrank K V

        The finite rank of V is unchanged by extension through a complex embedding.

        source
        @[simp]
        theorem TauCeti.finrank_atRealPlace {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (w : { w : NumberField.InfinitePlace K // w.IsReal }) :
        Module.finrank ℝ (RealScalarExtension w) = Module.finrank K V

        The finite rank of V is unchanged by extension through a real place.