NYLL
Module

LogLattice.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.SUnit.LogLattice
59 declarations indexed from sourceView source ↗

Module documentation

The logarithmic lattice of S-units

This file develops the logarithmic lattice of S-units. The finite set S consists of the finite places; all infinite places are understood to belong to the set of places used in the theorem.

The first construction uses the usual reduced archimedean logarithmic space (one infinite coordinate is omitted) together with the integral principal-divisor coordinates at S. Its image is proved directly to be a complete ℤ-lattice. The normalized, all-place logarithmic map and its coordinate-sum-zero hyperplane are constructed below from this lattice.

Imports4
Imported by3

Declarations

abbrev

ReducedLogSpace

L44 ↗
SUnitGroup.ReducedLogSpace
Documentation

The reduced logarithmic space for S-units. It consists of the Dirichlet logarithmic space and one real divisor coordinate for every finite place in S.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
abbrev ReducedLogSpace
def

reducedLog

L51 ↗
SUnitGroup.reducedLog
Documentation

The reduced logarithmic embedding. At an infinite place it is the usual multiplicity-weighted logarithm. At a finite place it is the integer exponent of the principal fractional ideal, regarded as a real number.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · full declaration
def reducedLog :
    Additive (SUnitGroup (K := K) S) →+
      ReducedLogSpace (K := K) S where
  toFun x :=
    (fun w =>
      w.1.mult *
        Real.log
          (w.1
            (((Additive.toMul x :
              SUnitGroup (K := K) S) : Kˣ) : K)),
      fun v =>
        (divisorCoordinate (K := K) S
          (Additive.toMul x) v : ℝ))
  map_zero' := by
    apply Prod.ext
    · ext w
      simp
    · ext v
      change
        (divisorCoordinate (K := K) S 1 v : ℝ) = 0
      exact_mod_cast divisorCoordinate_one (K := K) S v
  map_add' x y := by
    apply Prod.ext
    · ext w
      simp [Real.log_mul, mul_add]
    · ext v
      change
        (divisorCoordinate (K := K) S
          (Additive.toMul x * Additive.toMul y) v : ℝ) =
          (divisorCoordinate (K := K) S
            (Additive.toMul x) v : ℝ) +
          (divisorCoordinate (K := K) S
            (Additive.toMul y) v : ℝ)
      exact_mod_cast
        divisorCoordinate_mul (K := K) S
          (Additive.toMul x) (Additive.toMul y) v
theorem

adicAbv_eq_zpow_neg_divisorCoordinate

L90 ↗
SUnitGroup.adicAbv_eq_zpow_neg_divisorCoordinate
Documentation

The normalized finite absolute value is the norm of the prime raised to minus the corresponding principal-divisor exponent.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
theorem adicAbv_eq_zpow_neg_divisorCoordinate
    (x : SUnitGroup (K := K) S) (v : S) :
    NumberField.HeightOneSpectrum.adicAbv K
        (v : HeightOneSpectrum (𝓞 K)) (((x : Kˣ) : K)) =
      (Ideal.absNorm
        (v : HeightOneSpectrum (𝓞 K)).asIdeal : ℝ) ^
          (-divisorCoordinate (K := K) S x v)
theorem

log_adicAbv_eq_neg_divisorCoordinate_mul_log_absNorm

L105 ↗
SUnitGroup.log_adicAbv_eq_neg_divisorCoordinate_mul_log_absNorm
Documentation

The logarithm of a normalized finite absolute value is the divisor coordinate times -log Nv.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
theorem log_adicAbv_eq_neg_divisorCoordinate_mul_log_absNorm
    (x : SUnitGroup (K := K) S) (v : S) :
    Real.log
        (NumberField.HeightOneSpectrum.adicAbv K
          (v : HeightOneSpectrum (𝓞 K)) (((x : Kˣ) : K))) =
      -(divisorCoordinate (K := K) S x v : ℝ) *
        Real.log
          (Ideal.absNorm
            (v : HeightOneSpectrum (𝓞 K)).asIdeal : ℝ)
def

reducedLogLinearMap

L120 ↗
SUnitGroup.reducedLogLinearMap
Documentation

The ℤ-linear form of the reduced logarithmic embedding.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
def reducedLogLinearMap :
    Additive (SUnitGroup (K := K) S) →ₗ[ℤ]
      ReducedLogSpace (K := K) S
theorem

reducedLog_fst_fromNumberFieldUnits

L126 ↗
SUnitGroup.reducedLog_fst_fromNumberFieldUnits
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
theorem reducedLog_fst_fromNumberFieldUnits
    (u : (𝓞 K)ˣ) :
    (reducedLog (K := K) S
      (Additive.ofMul
        (fromNumberFieldUnits (K := K) S u))).1 =
      NumberField.Units.logEmbedding K (Additive.ofMul u)
theorem

reducedLog_snd_fromNumberFieldUnits

L136 ↗
SUnitGroup.reducedLog_snd_fromNumberFieldUnits
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
theorem reducedLog_snd_fromNumberFieldUnits
    (u : (𝓞 K)ˣ) :
    (reducedLog (K := K) S
      (Additive.ofMul
        (fromNumberFieldUnits (K := K) S u))).2 = 0
theorem

reducedLog_eq_zero_iff

L161 ↗
SUnitGroup.reducedLog_eq_zero_iff
Documentation

The reduced logarithm vanishes precisely on the roots of unity.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
theorem reducedLog_eq_zero_iff
    (x : Additive (SUnitGroup (K := K) S)) :
    reducedLog (K := K) S x = 0 ↔
      x ∈ AddCommGroup.torsion
        (Additive (SUnitGroup (K := K) S))
theorem

reducedLogLinearMap_ker

L223 ↗
SUnitGroup.reducedLogLinearMap_ker
Documentation

The kernel of the reduced logarithmic map is the additive torsion submodule.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
theorem reducedLogLinearMap_ker :
    LinearMap.ker (reducedLogLinearMap (K := K) S) =
      (AddCommGroup.torsion
        (Additive (SUnitGroup (K := K) S))).toIntSubmodule
def

reducedLogLattice

L232 ↗
SUnitGroup.reducedLogLattice
Documentation

The reduced S-unit lattice.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
def reducedLogLattice :
    Submodule ℤ (ReducedLogSpace (K := K) S)
theorem

norm_reducedLog_finite_lt_one_implies_zero

L239 ↗
SUnitGroup.norm_reducedLog_finite_lt_one_implies_zero
Documentation

A reduced logarithmic vector in the lattice vanishes when all of its finite coordinates have norm less than one.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
open scoped Classical in
Lean source · statement
theorem norm_reducedLog_finite_lt_one_implies_zero
    {x : Additive (SUnitGroup (K := K) S)}
    (hx :
      ‖reducedLog (K := K) S x‖ < 1) :
    (reducedLog (K := K) S x).2 = 0
instance

instDiscreteTopology_reducedLogLattice

L263 ↗
SUnitGroup.instDiscreteTopology_reducedLogLattice
Documentation

The reduced logarithmic image is discrete. Near the origin the integral finite coordinates must vanish, reducing the assertion to the ordinary Dirichlet unit lattice.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
instance instDiscreteTopology_reducedLogLattice :
    DiscreteTopology (reducedLogLattice (K := K) S)
theorem

finrank_reducedLogLattice

L361 ↗
SUnitGroup.finrank_reducedLogLattice
Documentation

The integral rank of the reduced logarithmic lattice is the Dirichlet unit rank plus the number of finite places in S.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
theorem finrank_reducedLogLattice :
    Module.finrank ℤ (reducedLogLattice (K := K) S) =
      NumberField.Units.rank K + S.card
theorem

finrank_reducedLogSpace

L389 ↗
SUnitGroup.finrank_reducedLogSpace
Documentation

The reduced logarithmic space has dimension equal to the Dirichlet unit rank plus the number of finite places in S.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
theorem finrank_reducedLogSpace :
    Module.finrank ℝ (ReducedLogSpace (K := K) S) =
      NumberField.Units.rank K + S.card
theorem

reducedLogLattice_span_eq_top

L397 ↗
SUnitGroup.reducedLogLattice_span_eq_top
Documentation

The reduced logarithmic lattice spans its whole real ambient space.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
Lean source · statement
theorem reducedLogLattice_span_eq_top :
    Submodule.span ℝ
      (reducedLogLattice (K := K) S :
        Set (ReducedLogSpace (K := K) S)) = ⊤
instance

instIsZLattice_reducedLogLattice

L435 ↗
SUnitGroup.instIsZLattice_reducedLogLattice
Documentation

The reduced logarithmic image of the S-units is a complete ℤ-lattice.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
open scoped Classical in
Lean source · full declaration
instance instIsZLattice_reducedLogLattice :
    IsZLattice ℝ (reducedLogLattice (K := K) S) where
  span_top := reducedLogLattice_span_eq_top (K := K) S
abbrev

LogPlace

L443 ↗
SUnitGroup.LogPlace
Documentation

The places occurring in the S-unit theorem: every infinite place and the finite places belonging to S.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
abbrev LogPlace
abbrev

FullLogSpace

L448 ↗
SUnitGroup.FullLogSpace
Documentation

The ambient real coordinate space indexed by all places occurring in the S-unit theorem.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
abbrev FullLogSpace
def

coordinateSum

L452 ↗
SUnitGroup.coordinateSum
Documentation

Sum of all logarithmic coordinates.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · full declaration
def coordinateSum :
    FullLogSpace (K := K) S →ₗ[ℝ] ℝ where
  toFun z := ∑ p, z p
  map_add' x y := by
    simp [Finset.sum_add_distrib]
  map_smul' c x := by
    change
      (∑ p : LogPlace (K := K) S, c * x p) =
        c * ∑ p : LogPlace (K := K) S, x p
    rw [Finset.mul_sum]
abbrev

LogHyperplane

L465 ↗
SUnitGroup.LogHyperplane
Documentation

The coordinate-sum-zero hyperplane in the full logarithmic space.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
abbrev LogHyperplane
def

fullLogAmbient

L470 ↗
SUnitGroup.fullLogAmbient
Documentation

The normalized logarithmic absolute-value map at all places in the S-unit theorem.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · full declaration
def fullLogAmbient :
    Additive (SUnitGroup (K := K) S) →+
      FullLogSpace (K := K) S where
  toFun x p :=
    match p with
    | Sum.inl w =>
        w.mult *
          Real.log
            (w
              (((Additive.toMul x :
                SUnitGroup (K := K) S) : Kˣ) : K))
    | Sum.inr v =>
        Real.log
          (NumberField.HeightOneSpectrum.adicAbv K
            (v : HeightOneSpectrum (𝓞 K))
            (((Additive.toMul x :
              SUnitGroup (K := K) S) : Kˣ) : K))
  map_zero' := by
    ext p
    cases p <;> simp
  map_add' x y := by
    ext p
    cases p <;> simp [Real.log_mul, mul_add]
theorem

fullLogAmbient_infinite

L495 ↗
SUnitGroup.fullLogAmbient_infinite
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem fullLogAmbient_infinite
    (x : Additive (SUnitGroup (K := K) S))
    (w : NumberField.InfinitePlace K) :
    fullLogAmbient (K := K) S x (Sum.inl w) =
      w.mult *
        Real.log
          (w
            (((Additive.toMul x :
              SUnitGroup (K := K) S) : Kˣ) : K))
theorem

fullLogAmbient_finite

L507 ↗
SUnitGroup.fullLogAmbient_finite
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem fullLogAmbient_finite
    (x : Additive (SUnitGroup (K := K) S)) (v : S) :
    fullLogAmbient (K := K) S x (Sum.inr v) =
      Real.log
        (NumberField.HeightOneSpectrum.adicAbv K
          (v : HeightOneSpectrum (𝓞 K))
          (((Additive.toMul x :
            SUnitGroup (K := K) S) : Kˣ) : K))
theorem

adicAbv_eq_one_of_not_mem

L518 ↗
SUnitGroup.adicAbv_eq_one_of_not_mem
Documentation

An S-unit has normalized finite absolute value one outside S.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem adicAbv_eq_one_of_not_mem
    (x : SUnitGroup (K := K) S)
    (v : HeightOneSpectrum (𝓞 K)) (hv : v ∉ S) :
    NumberField.HeightOneSpectrum.adicAbv K v
        (((x : Kˣ) : K)) = 1
theorem

finprod_finitePlace_eq_prod_adicAbv

L529 ↗
SUnitGroup.finprod_finitePlace_eq_prod_adicAbv
Documentation

For an S-unit the finite part of the global product formula is the product over the finite places in S.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem finprod_finitePlace_eq_prod_adicAbv
    (x : SUnitGroup (K := K) S) :
    (∏ᶠ w : NumberField.FinitePlace K,
        w (((x : Kˣ) : K))) =
      ∏ v : S,
        NumberField.HeightOneSpectrum.adicAbv K
          (v : HeightOneSpectrum (𝓞 K))
          (((x : Kˣ) : K))
theorem

sum_log_absoluteValues_eq_zero

L558 ↗
SUnitGroup.sum_log_absoluteValues_eq_zero
Documentation

Logarithmic form of the product formula, restricted to the places of the S-unit theorem.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem sum_log_absoluteValues_eq_zero
    (x : SUnitGroup (K := K) S) :
    (∑ w : NumberField.InfinitePlace K,
        w.mult * Real.log (w (((x : Kˣ) : K)))) +
      ∑ v : S,
        Real.log
          (NumberField.HeightOneSpectrum.adicAbv K
            (v : HeightOneSpectrum (𝓞 K))
            (((x : Kˣ) : K))) = 0
theorem

fullLogAmbient_mem_logHyperplane

L616 ↗
SUnitGroup.fullLogAmbient_mem_logHyperplane
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem fullLogAmbient_mem_logHyperplane
    (x : Additive (SUnitGroup (K := K) S)) :
    fullLogAmbient (K := K) S x ∈
      LogHyperplane (K := K) S
def

fullLog

L631 ↗
SUnitGroup.fullLog
Documentation

The normalized all-place logarithmic map with codomain restricted to the coordinate-sum-zero hyperplane.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
def fullLog :
    Additive (SUnitGroup (K := K) S) →+
      LogHyperplane (K := K) S
def

finiteLogWeight

L640 ↗
SUnitGroup.finiteLogWeight
Documentation

The nonzero scale converting an integral divisor coordinate into the logarithm of the corresponding normalized finite absolute value.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
def finiteLogWeight (v : S) : ℝ
theorem

finiteLogWeight_ne_zero

L645 ↗
SUnitGroup.finiteLogWeight_ne_zero
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem finiteLogWeight_ne_zero (v : S) :
    finiteLogWeight (K := K) S v ≠ 0
def

forgetDistinguishedLog

L658 ↗
SUnitGroup.forgetDistinguishedLog
Documentation

Forget the distinguished infinite coordinate and divide the finite logarithmic coordinates by their nonzero normalizing weights.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · full declaration
def forgetDistinguishedLog :
    LogHyperplane (K := K) S →ₗ[ℝ]
      ReducedLogSpace (K := K) S where
  toFun z :=
    (fun w => (z : FullLogSpace (K := K) S) (Sum.inl w.1),
      fun v =>
        (z : FullLogSpace (K := K) S) (Sum.inr v) /
          finiteLogWeight (K := K) S v)
  map_add' x y := by
    apply Prod.ext
    · ext w
      rfl
    · ext v
      simp [add_div]
  map_smul' c x := by
    apply Prod.ext
    · ext w
      rfl
    · ext v
      change
        (c *
            (x : FullLogSpace (K := K) S) (Sum.inr v)) /
            finiteLogWeight (K := K) S v =
          c *
            ((x : FullLogSpace (K := K) S) (Sum.inr v) /
              finiteLogWeight (K := K) S v)
      ring
theorem

forgetDistinguishedLog_injective

L689 ↗
SUnitGroup.forgetDistinguishedLog_injective
Documentation

Forgetting the distinguished logarithmic coordinate is injective on the product-formula hyperplane.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
open scoped Classical in
Lean source · statement
theorem forgetDistinguishedLog_injective :
    Function.Injective (forgetDistinguishedLog (K := K) S)
theorem

forgetDistinguishedLog_surjective

L793 ↗
SUnitGroup.forgetDistinguishedLog_surjective
Documentation

Every reduced logarithmic vector has a lift to the product-formula hyperplane.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
open scoped Classical in
Lean source · statement
theorem forgetDistinguishedLog_surjective :
    Function.Surjective (forgetDistinguishedLog (K := K) S)
def

logHyperplaneEquivReduced

L867 ↗
SUnitGroup.logHyperplaneEquivReduced
Documentation

Removing the distinguished infinite coordinate and rescaling the finite coordinates is a real linear equivalence.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
def logHyperplaneEquivReduced :
    LogHyperplane (K := K) S ≃ₗ[ℝ]
      ReducedLogSpace (K := K) S
theorem

logHyperplaneEquivReduced_fullLog

L877 ↗
SUnitGroup.logHyperplaneEquivReduced_fullLog
Documentation

Under the coordinate equivalence, the normalized all-place logarithm is exactly the reduced logarithm.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem logHyperplaneEquivReduced_fullLog
    (x : Additive (SUnitGroup (K := K) S)) :
    logHyperplaneEquivReduced (K := K) S
        (fullLog (K := K) S x) =
      reducedLog (K := K) S x
theorem

fullLog_eq_zero_iff

L908 ↗
SUnitGroup.fullLog_eq_zero_iff
Documentation

The kernel of the normalized all-place logarithm is the group of roots of unity.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem fullLog_eq_zero_iff
    (x : Additive (SUnitGroup (K := K) S)) :
    fullLog (K := K) S x = 0 ↔
      x ∈ AddCommGroup.torsion
        (Additive (SUnitGroup (K := K) S))
def

logHyperplaneContinuousEquivReduced

L925 ↗
SUnitGroup.logHyperplaneContinuousEquivReduced
Documentation

The coordinate equivalence as a continuous linear equivalence (both spaces are finite-dimensional).

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
def logHyperplaneContinuousEquivReduced :
    LogHyperplane (K := K) S ≃L[ℝ]
      ReducedLogSpace (K := K) S
def

fullLogLattice

L932 ↗
SUnitGroup.fullLogLattice
Documentation

The complete lattice in the coordinate-sum-zero hyperplane.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
open scoped Classical in
Lean source · statement
def fullLogLattice :
    Submodule ℤ (LogHyperplane (K := K) S)
theorem

fullLogLattice_eq_range

L941 ↗
SUnitGroup.fullLogLattice_eq_range
Documentation

The complete lattice just defined is exactly the image of the normalized all-place logarithmic map.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
Lean source · statement
theorem fullLogLattice_eq_range :
    fullLogLattice (K := K) S =
      LinearMap.range
        (fullLog (K := K) S).toIntLinearMap
instance

instDiscreteTopology_fullLogLattice

L969 ↗
SUnitGroup.instDiscreteTopology_fullLogLattice
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
open scoped Classical in
Lean source · statement
instance instDiscreteTopology_fullLogLattice :
    DiscreteTopology (fullLogLattice (K := K) S)
instance

instIsZLattice_fullLogLattice

L983 ↗
SUnitGroup.instIsZLattice_fullLogLattice
Documentation

The image of the normalized all-place logarithmic embedding is a complete ℤ-lattice in the coordinate-sum-zero hyperplane.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section FullLogarithmicSpace
open scoped Classical in
Lean source · statement
instance instIsZLattice_fullLogLattice :
    IsZLattice ℝ (fullLogLattice (K := K) S)
def

logRank

L1000 ↗
SUnitGroup.logRank
Documentation

The logarithmic rank: the number of places in the S-unit theorem minus one.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
Lean source · statement
def logRank : ℕ
abbrev

RootsOfUnityAdditive

L1004 ↗
SUnitGroup.RootsOfUnityAdditive
Documentation

The additive realization of the roots of unity of K.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
Lean source · statement
abbrev RootsOfUnityAdditive
abbrev

TorsionAdditive

L1008 ↗
SUnitGroup.TorsionAdditive
Documentation

The additive torsion submodule of the S-unit group.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
Lean source · statement
abbrev TorsionAdditive
theorem

torsionAdditive_eq

L1012 ↗
SUnitGroup.torsionAdditive_eq
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
Lean source · statement
theorem torsionAdditive_eq :
    TorsionAdditive (K := K) S =
      (AddCommGroup.torsion
        (Additive
          (SUnitGroup (K := K) S))).toIntSubmodule
abbrev

FreeQuotient

L1022 ↗
SUnitGroup.FreeQuotient
Documentation

The torsion-free quotient of the additive S-unit group.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
Lean source · statement
abbrev FreeQuotient
instance

instModuleFinite_additiveSUnit

L1026 ↗
SUnitGroup.instModuleFinite_additiveSUnit
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
Lean source · statement
instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S))
instance

instModule_freeQuotient

L1030 ↗
SUnitGroup.instModule_freeQuotient
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
Lean source · statement
instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S)
instance

instModuleFinite_freeQuotient

L1035 ↗
SUnitGroup.instModuleFinite_freeQuotient
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
Lean source · statement
instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S)
instance

instModuleFree_freeQuotient

L1040 ↗
SUnitGroup.instModuleFree_freeQuotient
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
Lean source · statement
instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S)
theorem

finrank_freeQuotient

L1046 ↗
SUnitGroup.finrank_freeQuotient
Documentation

The free quotient has rank #S - 1, where S here includes all infinite places.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
local instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S) :=
  Module.free_of_finite_type_torsion_free'
Lean source · statement
theorem finrank_freeQuotient :
    Module.finrank ℤ (FreeQuotient (K := K) S) =
      logRank (K := K) S
def

basisFreeQuotient

L1067 ↗
SUnitGroup.basisFreeQuotient
Documentation

A basis of the free quotient, indexed by its logarithmic rank.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
local instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S) :=
  Module.free_of_finite_type_torsion_free'
Lean source · statement
def basisFreeQuotient :
    Basis (Fin (logRank (K := K) S)) ℤ
      (FreeQuotient (K := K) S)
def

rootsOfUnityEquivTorsion

L1080 ↗
SUnitGroup.rootsOfUnityEquivTorsion
Documentation

The ordinary roots of unity map linearly and bijectively onto the torsion in the S-unit group.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
local instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S) :=
  Module.free_of_finite_type_torsion_free'
Lean source · statement
def rootsOfUnityEquivTorsion :
    RootsOfUnityAdditive (K := K) ≃ₗ[ℤ]
      TorsionAdditive (K := K) S
def

torsionQuotientSection

L1142 ↗
SUnitGroup.torsionQuotientSection
Documentation

A linear section of the quotient by torsion. It exists because the quotient is a free, hence projective, ℤ-module.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
local instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S) :=
  Module.free_of_finite_type_torsion_free'
Lean source · statement
def torsionQuotientSection :
    FreeQuotient (K := K) S →ₗ[ℤ]
      Additive (SUnitGroup (K := K) S)
theorem

torsionQuotientSection_spec

L1150 ↗
SUnitGroup.torsionQuotientSection_spec
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
local instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S) :=
  Module.free_of_finite_type_torsion_free'
Lean source · statement
theorem torsionQuotientSection_spec :
    (TorsionAdditive (K := K) S).mkQ.comp
        (torsionQuotientSection (K := K) S) =
      LinearMap.id
def

torsionProdFreeQuotientEquiv

L1161 ↗
SUnitGroup.torsionProdFreeQuotientEquiv
Documentation

Splitting the exact sequence consisting of torsion, the S-unit group, and its torsion-free quotient.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
local instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S) :=
  Module.free_of_finite_type_torsion_free'
Lean source · statement
def torsionProdFreeQuotientEquiv :
    Additive (SUnitGroup (K := K) S) ≃ₗ[ℤ]
      TorsionAdditive (K := K) S ×
        FreeQuotient (K := K) S
def

decompositionLinearEquiv

L1174 ↗
SUnitGroup.decompositionLinearEquiv
Documentation

`S`-unit theorem, decomposition form. Additively, the S-unit group is the product of the roots of unity and a free ℤ-module of rank #S - 1.

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
local instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S) :=
  Module.free_of_finite_type_torsion_free'
Lean source · statement
def decompositionLinearEquiv :
    Additive (SUnitGroup (K := K) S) ≃ₗ[ℤ]
      RootsOfUnityAdditive (K := K) ×
        (Fin (logRank (K := K) S) →₀ ℤ)
def

multiplicativeRootsOfUnityEquiv

L1184 ↗
SUnitGroup.multiplicativeRootsOfUnityEquiv
Documentation

The multiplicative realization of the additive roots-of-unity submodule is canonically the usual group μ(K).

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
local instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S) :=
  Module.free_of_finite_type_torsion_free'
Lean source · full declaration
def multiplicativeRootsOfUnityEquiv :
    Multiplicative (RootsOfUnityAdditive (K := K)) ≃*
      NumberField.Units.torsion K where
  toFun x :=
    ⟨Additive.toMul
      ((Multiplicative.toAdd x :
        RootsOfUnityAdditive (K := K)) :
        Additive (𝓞 K)ˣ),
      (Multiplicative.toAdd x :
        RootsOfUnityAdditive (K := K)).property⟩
  invFun u :=
    Multiplicative.ofAdd
      (⟨Additive.ofMul (u : (𝓞 K)ˣ), u.property⟩ :
        RootsOfUnityAdditive (K := K))
  left_inv x := by
    rfl
  right_inv u := by
    rfl
  map_mul' x y := by
    rfl
def

decomposition

L1209 ↗
SUnitGroup.decomposition
Documentation

`S`-unit theorem, group form.

Writing S for all infinite places together with the supplied finite places, the S-unit group is μ(K) × ℤ^(#S-1).

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open IsDedekindDomain Module
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
variable (S : Finset (HeightOneSpectrum (𝓞 K)))
section Decomposition
local instance instModuleFinite_additiveSUnit :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S)) :=
  moduleFinite (K := K) S
local instance instModule_freeQuotient :
    Module ℤ (FreeQuotient (K := K) S) :=
  Submodule.Quotient.module
    (TorsionAdditive (K := K) S)
local instance instModuleFinite_freeQuotient :
    Module.Finite ℤ (FreeQuotient (K := K) S) :=
  Module.Finite.quotient ℤ
    (TorsionAdditive (K := K) S)
local instance instModuleFree_freeQuotient :
    Module.Free ℤ (FreeQuotient (K := K) S) :=
  Module.free_of_finite_type_torsion_free'
Lean source · statement
def decomposition :
    SUnitGroup (K := K) S ≃*
      NumberField.Units.torsion K ×
        Multiplicative
          (Fin (logRank (K := K) S) →₀ ℤ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.