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
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.

Equations
    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 ā„.

      Equations
        Instances For
          source
          šŸ”ø coverage
          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.

          Equations
            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
              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.

              Equations
                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
                  def NumberField.Units.regulator (K : Type u_1) [Field K] [NumberField K] :
                  ā„

                  The regulator of a number field K.

                  Equations
                    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.