Documentation

Mathlib.NumberTheory.NumberField.Units.Regulator

Regulator of a number field #

We define and prove basic results about the regulator of a number field K.

Main definitions and results #

Tags #

number field, units, regulator

source
šŸ”ø coverage
noncomputable def NumberField.Units.equivFinRank (K : Type u_1) [Field K] [NumberField K] :
Fin (rank K) ā‰ƒ { w : InfinitePlace K // w ā‰  dirichletUnitTheorem.wā‚€ }

An equiv between Fin (rank K), used to index the family of units, and {w // w ā‰  wā‚€} the index of the logSpace.

Instances For
    source
    šŸ”¹ coverage
    @[reducible, inline]
    abbrev NumberField.Units.IsMaxRank {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£) :
    Prop

    A family of units is of maximal rank if its image by logEmbedding is linearly independent over ā„.

    Instances For
      source
      šŸ”ø coverage
      noncomputable def NumberField.Units.basisOfIsMaxRank {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} (hu : IsMaxRank u) :
      Module.Basis (Fin (rank K)) ā„ (dirichletUnitTheorem.logSpace K)

      The images by logEmbedding of a family of units of maximal rank form a basis of logSpace K.

      Instances For
        source
        šŸ“ coverage
        @[simp]
        theorem NumberField.Units.basisOfIsMaxRank_apply {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} (hu : IsMaxRank u) (i : Fin (rank K)) :
        (basisOfIsMaxRank hu) i = (logEmbedding K) (Additive.ofMul (u i))
        source
        šŸ“ coverage
        theorem NumberField.Units.span_basisOfIsMaxRank {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} (hu : IsMaxRank u) :
        (Submodule.span ā„¤ (Set.range ā‡‘(basisOfIsMaxRank hu))).toAddSubgroup = AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)))
        source
        šŸ“ coverage
        theorem NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex {K : Type u_1} [Field K] [NumberField K] (s : Subgroup (RingOfIntegers K)Ė£) :
        s.FiniteIndex ā†” (s āŠ” torsion K).FiniteIndex
        source
        šŸ“ coverage
        theorem NumberField.Units.isMaxRank_iff_closure_finiteIndex {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} :
        IsMaxRank u ā†” (Subgroup.closure (Set.range u)).FiniteIndex

        A family of units is of maximal rank iff the index of the subgroup it generates has finite index.

        source
        šŸ”ø coverage
        noncomputable def NumberField.Units.regOfFamily {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£) :
        ā„

        The regulator of a family of units of K.

        Instances For
          source
          šŸ“ coverage
          theorem NumberField.Units.regOfFamily_eq_zero {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} (hu : Ā¬IsMaxRank u) :
          regOfFamily u = 0
          source
          šŸ“ coverage
          theorem NumberField.Units.regOfFamily_of_isMaxRank {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} (hu : IsMaxRank u) :
          regOfFamily u = ZLattice.covolume (Submodule.span ā„¤ (Set.range ā‡‘(basisOfIsMaxRank hu))) MeasureTheory.volume
          source
          šŸ“ coverage
          theorem NumberField.Units.regOfFamily_pos {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} (hu : IsMaxRank u) :
          0 < regOfFamily u
          source
          theorem NumberField.Units.regOfFamily_ne_zero {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} (hu : IsMaxRank u) :
          regOfFamily u ā‰  0
          source
          šŸ“ coverage
          theorem NumberField.Units.regOfFamily_ne_zero_iff {K : Type u_1} [Field K] [NumberField K] {u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} :
          regOfFamily u ā‰  0 ā†” IsMaxRank u
          source
          šŸ“ coverage
          theorem NumberField.Units.regOfFamily_eq_det' {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£) :
          regOfFamily u = |(Matrix.of fun (i : { w : InfinitePlace K // w ā‰  dirichletUnitTheorem.wā‚€ }) => (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))).det|
          source
          šŸ“ coverage
          theorem NumberField.Units.abs_det_eq_abs_det {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£) {wā‚ wā‚‚ : InfinitePlace K} (eā‚ : { w : InfinitePlace K // w ā‰  wā‚ } ā‰ƒ Fin (rank K)) (eā‚‚ : { w : InfinitePlace K // w ā‰  wā‚‚ } ā‰ƒ Fin (rank K)) :
          |(Matrix.of fun (i w : { w : InfinitePlace K // w ā‰  wā‚ }) => ā†‘(ā†‘w).mult * Real.log (ā†‘w ((algebraMap (RingOfIntegers K) K) ā†‘(u (eā‚ i))))).det| = |(Matrix.of fun (i w : { w : InfinitePlace K // w ā‰  wā‚‚ }) => ā†‘(ā†‘w).mult * Real.log (ā†‘w ((algebraMap (RingOfIntegers K) K) ā†‘(u (eā‚‚ i))))).det|

          Let u : Fin (rank K) ā†’ (š“ž K)Ė£ be a family of units and let wā‚ and wā‚‚ be two infinite places. Then, the two square matrices with entries (mult w * log w (u i))_i where w ā‰  w_j for j = 1, 2 have the same determinant in absolute value.

          source
          šŸ“ coverage
          theorem NumberField.Units.regOfFamily_eq_det {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£) (w' : InfinitePlace K) (e : { w : InfinitePlace K // w ā‰  w' } ā‰ƒ Fin (rank K)) :
          regOfFamily u = |(Matrix.of fun (i w : { w : InfinitePlace K // w ā‰  w' }) => ā†‘(ā†‘w).mult * Real.log (ā†‘w ((algebraMap (RingOfIntegers K) K) ā†‘(u (e i))))).det|

          For any infinite place w', the regulator of the family u is equal to the absolute value of the determinant of the matrix with entries (mult w * log w (u i))_i for w ā‰  w'.

          source
          šŸ“ coverage
          theorem NumberField.Units.finrank_mul_regOfFamily_eq_det {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£) (w' : InfinitePlace K) (e : { w : InfinitePlace K // w ā‰  w' } ā‰ƒ Fin (rank K)) :
          ā†‘(Module.finrank ā„š K) * regOfFamily u = |(Matrix.of fun (i w : InfinitePlace K) => if h : i = w' then ā†‘w.mult else ā†‘w.mult * Real.log (w ((algebraMap (RingOfIntegers K) K) ā†‘(u (e āŸØi, hāŸ©))))).det|

          The degree of K times the regulator of the family u is equal to the absolute value of the determinant of the matrix whose columns are (mult w * log w (fundSystem K i))_i, w and the column (mult w)_w.

          source
          šŸ”ø coverage
          noncomputable def NumberField.Units.regulator (K : Type u_1) [Field K] [NumberField K] :
          ā„

          The regulator of a number field K.

          Instances For
            source
            šŸ“ coverage
            theorem NumberField.Units.isMaxRank_fundSystem (K : Type u_1) [Field K] [NumberField K] :
            IsMaxRank (fundSystem K)
            source
            šŸ“ coverage
            theorem NumberField.Units.basisOfIsMaxRank_fundSystem (K : Type u_1) [Field K] [NumberField K] :
            basisOfIsMaxRank ā‹Æ = Module.Basis.ofZLatticeBasis ā„ (unitLattice K) (basisUnitLattice K)
            source
            šŸ“ coverage
            theorem NumberField.Units.regulator_eq_regOfFamily_fundSystem (K : Type u_1) [Field K] [NumberField K] :
            regulator K = regOfFamily (fundSystem K)
            source
            šŸ“ coverage
            theorem NumberField.Units.regulator_pos (K : Type u_1) [Field K] [NumberField K] :
            0 < regulator K
            source
            theorem NumberField.Units.regulator_ne_zero (K : Type u_1) [Field K] [NumberField K] :
            regulator K ā‰  0
            source
            šŸ“ coverage
            theorem NumberField.Units.regulator_eq_det' (K : Type u_1) [Field K] [NumberField K] :
            regulator K = |(Matrix.of fun (i : { w : InfinitePlace K // w ā‰  dirichletUnitTheorem.wā‚€ }) => (logEmbedding K) (Additive.ofMul (fundSystem K ((equivFinRank K).symm i)))).det|
            source
            šŸ“ coverage
            theorem NumberField.Units.regulator_eq_det (K : Type u_1) [Field K] [NumberField K] (w' : InfinitePlace K) (e : { w : InfinitePlace K // w ā‰  w' } ā‰ƒ Fin (rank K)) :
            regulator K = |(Matrix.of fun (i w : { w : InfinitePlace K // w ā‰  w' }) => ā†‘(ā†‘w).mult * Real.log (ā†‘w ((algebraMap (RingOfIntegers K) K) ā†‘(fundSystem K (e i))))).det|

            For any infinite place w', the regulator is equal to the absolute value of the determinant of the matrix with entries (mult w * log w (fundSystem K i))_i for w ā‰  w'.

            source
            šŸ“ coverage
            theorem NumberField.Units.finrank_mul_regulator_eq_det (K : Type u_1) [Field K] [NumberField K] (w' : InfinitePlace K) (e : { w : InfinitePlace K // w ā‰  w' } ā‰ƒ Fin (rank K)) :
            ā†‘(Module.finrank ā„š K) * regulator K = |(Matrix.of fun (i w : InfinitePlace K) => if h : i = w' then ā†‘w.mult else ā†‘w.mult * Real.log (w ((algebraMap (RingOfIntegers K) K) ā†‘(fundSystem K (e āŸØi, hāŸ©))))).det|

            The degree of K times the regulator of K is equal to the absolute value of the determinant of the matrix whose columns are (mult w * log w (fundSystem K i))_i, w and the column (mult w)_w.

            source
            šŸ“ coverage
            theorem NumberField.Units.regOfFamily_div_regOfFamily {K : Type u_1} [Field K] [NumberField K] {u v : Fin (rank K) ā†’ (RingOfIntegers K)Ė£} (hv : IsMaxRank v) (h : Subgroup.closure (Set.range u) āŠ” torsion K ā‰¤ Subgroup.closure (Set.range v) āŠ” torsion K) :
            regOfFamily u / regOfFamily v = ā†‘((Subgroup.closure (Set.range u) āŠ” torsion K).relIndex (Subgroup.closure (Set.range v) āŠ” torsion K))

            Let u and v be two families of units. Assume that the subgroup U generated by u and torsion K is contained in the subgroup V generated by v and torsion K. Then the ratio regOfFamily u / regOfFamily v is equal to the index of U inside V.

            source
            šŸ“ coverage
            theorem NumberField.Units.regOfFamily_div_regulator {K : Type u_1} [Field K] [NumberField K] (u : Fin (rank K) ā†’ (RingOfIntegers K)Ė£) :
            regOfFamily u / regulator K = ā†‘(Subgroup.closure (Set.range u) āŠ” torsion K).index

            Let u be a family of units. Then the ratio regOfFamily u / regulator K is equal to the index of the subgroup generated by u and torsion K inside the group of units of K.