Module

Rank.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.SUnit.Rank

34 declarations indexed from sourceView source ↗

Module documentation

Torsion and rank sources for `S`-units

This file supplies the algebraic rank and torsion input for S-units. The finite set S contains the finite places; all infinite places are understood to be present.

Imports7

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.SPlaces
Mathlib.Algebra.Exact.Basic
Mathlib.LinearAlgebra.Dimension.Torsion.Finite
Mathlib.LinearAlgebra.StdBasis
Mathlib.NumberTheory.NumberField.ClassNumber
Mathlib.NumberTheory.NumberField.Units.Regulator
Mathlib.RingTheory.DedekindDomain.Factorization

Imported by3

def

emptyEquivNumberFieldUnits

L36 ↗

SUnitGroup.emptyEquivNumberFieldUnits

Documentation

The group of ordinary units, expressed as S-units for the empty set.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup

Lean source · statement

def emptyEquivNumberFieldUnits :
    ((∅ : Set (HeightOneSpectrum (𝓞 K))).unit K) ≃* (𝓞 K)ˣ

def

fromNumberFieldUnits

L56 ↗

SUnitGroup.fromNumberFieldUnits

Documentation

The canonical embedding of ordinary units into the S-unit group.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup

Lean source · full declaration

def fromNumberFieldUnits
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (𝓞 K)ˣ →* SUnitGroup (K := K) S where
  toFun u :=
    ⟨((emptyEquivNumberFieldUnits (K := K)).symm u : Kˣ),
      fun v _ =>
        Set.unit_valuation_eq_one
          (∅ : Set (HeightOneSpectrum (𝓞 K))) K
          ((emptyEquivNumberFieldUnits (K := K)).symm u) (by simp)⟩
  map_one' := by
    ext
    simp
  map_mul' u v := by
    ext
    simp

theorem

fromNumberFieldUnits_injective

L72 ↗

SUnitGroup.fromNumberFieldUnits_injective

Source context 5 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup

Lean source · statement

theorem fromNumberFieldUnits_injective
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Injective (fromNumberFieldUnits (K := K) S)

theorem

torsion_eq_rootsOfUnity_range

L82 ↗

SUnitGroup.torsion_eq_rootsOfUnity_range

Documentation

Torsion in an S-unit group consists exactly of the ordinary roots of unity.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup

Lean source · statement

theorem torsion_eq_rootsOfUnity_range
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    CommGroup.torsion (SUnitGroup (K := K) S) =
      Subgroup.map (fromNumberFieldUnits (K := K) S)
        (NumberField.Units.torsion K)

def

divisorCoordinate

L132 ↗

SUnitGroup.divisorCoordinate

Documentation

The exponent of the principal fractional ideal of an S-unit at a finite place in S.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

def divisorCoordinate
    (x : SUnitGroup (K := K) S) (v : S) : ℤ

theorem

valuation_mk'_eq_exp_neg_count

L139 ↗

SUnitGroup.valuation_mk'_eq_exp_neg_count

Documentation

The valuation of a localization fraction is the exponential of the negative exponent of its principal fractional ideal.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem valuation_mk'_eq_exp_neg_count
    (v : HeightOneSpectrum (𝓞 K)) {n : 𝓞 K} (hn : n ≠ 0)
    (d : (𝓞 K)⁰) :
    v.valuation K (IsLocalization.mk' K n d) =
      WithZero.exp
        (-FractionalIdeal.count K v
          (FractionalIdeal.spanSingleton (𝓞 K)⁰
            (IsLocalization.mk' K n d)))

theorem

valuation_eq_exp_neg_count

L185 ↗

SUnitGroup.valuation_eq_exp_neg_count

Documentation

The adic valuation of a field unit is the exponential of the negative exponent of its principal fractional ideal.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem valuation_eq_exp_neg_count
    (x : Kˣ) (v : HeightOneSpectrum (𝓞 K)) :
    v.valuation K (x : K) =
      WithZero.exp
        (-FractionalIdeal.count K v
          (FractionalIdeal.spanSingleton (𝓞 K)⁰ (x : K)))

theorem

valuation_eq_one_iff_count_eq_zero

L202 ↗

SUnitGroup.valuation_eq_one_iff_count_eq_zero

Documentation

A field unit has valuation one exactly when its principal fractional ideal has exponent zero at the place.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem valuation_eq_one_iff_count_eq_zero
    (x : Kˣ) (v : HeightOneSpectrum (𝓞 K)) :
    v.valuation K (x : K) = 1 ↔
      FractionalIdeal.count K v
        (FractionalIdeal.spanSingleton (𝓞 K)⁰ (x : K)) = 0

theorem

divisorCoordinate_eq_zero_iff

L214 ↗

SUnitGroup.divisorCoordinate_eq_zero_iff

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem divisorCoordinate_eq_zero_iff
    (x : SUnitGroup (K := K) S) (v : S) :
    divisorCoordinate (K := K) S x v = 0 ↔
      (v : HeightOneSpectrum (𝓞 K)).valuation K ((x : Kˣ) : K) = 1

theorem

divisorCoordinate_mul

L221 ↗

SUnitGroup.divisorCoordinate_mul

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem divisorCoordinate_mul
    (x y : SUnitGroup (K := K) S) (v : S) :
    divisorCoordinate (K := K) S (x * y) v =
      divisorCoordinate (K := K) S x v +
        divisorCoordinate (K := K) S y v

theorem

divisorCoordinate_one

L241 ↗

SUnitGroup.divisorCoordinate_one

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem divisorCoordinate_one (v : S) :
    divisorCoordinate (K := K) S 1 v = 0

def

divisor

L246 ↗

SUnitGroup.divisor

Documentation

The additive principal-divisor map on S-units.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · full declaration

def divisor :
    Additive (SUnitGroup (K := K) S) →+
      (S → ℤ) where
  toFun x v := divisorCoordinate (K := K) S (Additive.toMul x) v
  map_zero' := by
    ext v
    exact divisorCoordinate_one (K := K) S v
  map_add' x y := by
    ext v
    exact divisorCoordinate_mul (K := K) S
      (Additive.toMul x) (Additive.toMul y) v

def

divisorLinearMap

L259 ↗

SUnitGroup.divisorLinearMap

Documentation

The ℤ-linear principal-divisor map on S-units.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

def divisorLinearMap :
    Additive (SUnitGroup (K := K) S) →ₗ[ℤ] (S → ℤ)

def

fromNumberFieldUnitsLinearMap

L264 ↗

SUnitGroup.fromNumberFieldUnitsLinearMap

Documentation

The additive linearization of the ordinary-unit embedding.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

def fromNumberFieldUnitsLinearMap :
    Additive (𝓞 K)ˣ →ₗ[ℤ]
      Additive (SUnitGroup (K := K) S)

theorem

fromNumberFieldUnitsLinearMap_injective

L270 ↗

SUnitGroup.fromNumberFieldUnitsLinearMap_injective

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem fromNumberFieldUnitsLinearMap_injective :
    Function.Injective (fromNumberFieldUnitsLinearMap (K := K) S)

theorem

valuation_eq_one_of_mem_ker_divisorLinearMap

L279 ↗

SUnitGroup.valuation_eq_one_of_mem_ker_divisorLinearMap

Documentation

An S-unit in the kernel of the divisor map has valuation one at every finite place.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem valuation_eq_one_of_mem_ker_divisorLinearMap
    {x : Additive (SUnitGroup (K := K) S)}
    (hx : x ∈ LinearMap.ker (divisorLinearMap (K := K) S))
    (v : HeightOneSpectrum (𝓞 K)) :
    v.valuation K
      ((((Additive.toMul x :
        SUnitGroup (K := K) S) : Kˣ) : K)) = 1

def

kerDivisorToEmptySUnits

L299 ↗

SUnitGroup.kerDivisorToEmptySUnits

Documentation

An S-unit in the divisor kernel, regarded as an S-unit for the empty set.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

def kerDivisorToEmptySUnits
    (x : LinearMap.ker (divisorLinearMap (K := K) S)) :
    ((∅ : Set (HeightOneSpectrum (𝓞 K))).unit K)

theorem

range_fromNumberFieldUnitsLinearMap_eq_ker_divisorLinearMap

L309 ↗

SUnitGroup.range_fromNumberFieldUnitsLinearMap_eq_ker_divisorLinearMap

Documentation

Ordinary units are exactly the kernel of the S-unit divisor map.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section DivisorMap
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem range_fromNumberFieldUnitsLinearMap_eq_ker_divisorLinearMap :
    LinearMap.range (fromNumberFieldUnitsLinearMap (K := K) S) =
      LinearMap.ker (divisorLinearMap (K := K) S)

theorem

primeIdealPower_classNumber_isPrincipal

L345 ↗

SUnitGroup.primeIdealPower_classNumber_isPrincipal

Documentation

The class-number power of a prime ideal is principal.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section PrimePowerSources
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem primeIdealPower_classNumber_isPrincipal (v : S) :
    ((v : HeightOneSpectrum (𝓞 K)).asIdeal ^
      NumberField.classNumber K).IsPrincipal

def

primePowerGenerator

L380 ↗

SUnitGroup.primePowerGenerator

Documentation

A generator of the principal classNumber K-th power of a prime ideal.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section PrimePowerSources
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

def primePowerGenerator (v : S) : 𝓞 K

theorem

span_primePowerGenerator

L388 ↗

SUnitGroup.span_primePowerGenerator

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section PrimePowerSources
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem span_primePowerGenerator (v : S) :
    Ideal.span {primePowerGenerator (K := K) S v} =
      (v : HeightOneSpectrum (𝓞 K)).asIdeal ^
        NumberField.classNumber K

theorem

primePowerGenerator_ne_zero

L399 ↗

SUnitGroup.primePowerGenerator_ne_zero

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section PrimePowerSources
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem primePowerGenerator_ne_zero (v : S) :
    primePowerGenerator (K := K) S v ≠ 0

theorem

spanSingleton_primePowerGenerator

L410 ↗

SUnitGroup.spanSingleton_primePowerGenerator

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section PrimePowerSources
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem spanSingleton_primePowerGenerator (v : S) :
    FractionalIdeal.spanSingleton (𝓞 K)⁰
        (algebraMap (𝓞 K) K (primePowerGenerator (K := K) S v)) =
      ((v : HeightOneSpectrum (𝓞 K)).asIdeal :
        FractionalIdeal (𝓞 K)⁰ K) ^ NumberField.classNumber K

def

primePowerSUnit

L421 ↗

SUnitGroup.primePowerSUnit

Documentation

An S-unit whose divisor is classNumber K times the basis divisor at v.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section PrimePowerSources
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

def primePowerSUnit (v : S) :
    SUnitGroup (K := K) S

def

classNumberBasisVector

L449 ↗

SUnitGroup.classNumberBasisVector

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section PrimePowerSources
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

def classNumberBasisVector (v : S) : S → ℤ

theorem

divisorCoordinate_primePowerSUnit

L454 ↗

SUnitGroup.divisorCoordinate_primePowerSUnit

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section PrimePowerSources
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem divisorCoordinate_primePowerSUnit
    (v w : S) :
    divisorCoordinate (K := K) S (primePowerSUnit (K := K) S v) w =
      classNumberBasisVector (K := K) S v w

def

divisorRangeVector

L489 ↗

SUnitGroup.divisorRangeVector

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section Rank
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

def divisorRangeVector (v : S) :
    LinearMap.range (divisorLinearMap (K := K) S)

theorem

divisorRangeVector_linearIndependent

L496 ↗

SUnitGroup.divisorRangeVector_linearIndependent

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section Rank
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem divisorRangeVector_linearIndependent :
    LinearIndependent ℤ (divisorRangeVector (K := K) S)

theorem

finrank_divisor_range

L509 ↗

SUnitGroup.finrank_divisor_range

Documentation

The divisor-map range on S-units has rank equal to the number of places in S.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section Rank
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem finrank_divisor_range :
    Module.finrank ℤ
        (LinearMap.range (divisorLinearMap (K := K) S)) =
      S.card

theorem

moduleFinite

L531 ↗

SUnitGroup.moduleFinite

Documentation

The additive group of S-units is finitely generated over ℤ.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section Rank
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem moduleFinite :
    Module.Finite ℤ (Additive (SUnitGroup (K := K) S))

theorem

finrank_divisor_ker

L552 ↗

SUnitGroup.finrank_divisor_ker

Documentation

The kernel of the S-unit divisor map has the ordinary unit rank.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section Rank
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem finrank_divisor_ker :
    Module.finrank ℤ
        (LinearMap.ker (divisorLinearMap (K := K) S)) =
      NumberField.Units.rank K

theorem

finrank

L574 ↗

SUnitGroup.finrank

Documentation

The free rank of the S-unit group is the ordinary Dirichlet rank plus the number of finite places in S.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section Rank
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem finrank :
    Module.finrank ℤ (Additive (SUnitGroup (K := K) S)) =
      NumberField.Units.rank K + S.card

theorem

finrank_modTorsion

L630 ↗

SUnitGroup.finrank_modTorsion

Documentation

The S-unit rank in quotient-by-torsion form.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section Rank
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem finrank_modTorsion :
    Module.finrank ℤ
        (Additive
          (SUnitGroup (K := K) S ⧸
            CommGroup.torsion (SUnitGroup (K := K) S))) =
      NumberField.Units.rank K + S.card

theorem

finrank_modTorsion_eq_card_infinitePlaces_add_card_sub_one

L650 ↗

SUnitGroup.finrank_modTorsion_eq_card_infinitePlaces_add_card_sub_one

Documentation

Cardinality form of the S-unit rank: #S_infinite + #S_finite - 1.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField nonZeroDivisors
variable {K : Type*} [Field K] [NumberField K]
namespace SUnitGroup
section Rank
variable (S : Finset (HeightOneSpectrum (𝓞 K)))

Lean source · statement

theorem finrank_modTorsion_eq_card_infinitePlaces_add_card_sub_one :
    Module.finrank ℤ
        (Additive
          (SUnitGroup (K := K) S ⧸
            CommGroup.torsion (SUnitGroup (K := K) S))) =
      Fintype.card (NumberField.InfinitePlace K) + S.card - 1

Module documentation

Torsion and rank sources for S-units

Declarations

Torsion and rank sources for `S`-units