Module

PowerIndex.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PowerIndex

33 declarations indexed from sourceView source ↗

Module documentation

Power-index computations for complete discrete valuation fields

This LubinTate consumer specializes the public commutative-group power-index API to the unit and principal-unit decompositions of a complete discrete valuation field.

Imports3

Mathlib.SetTheory.Cardinal.Finite
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.FieldUnitDecomposition
Nyll.ValuedFieldTheory.LocalField.GroupTheory.PowerIndex

Imported by2

instance

finite_residueRootsOfUnityGroup

L37 ↗

LocalFieldTheory.DiscreteValuationField.finite_residueRootsOfUnityGroup

Documentation

The Teichmüller root factor is finite because it is equivalent to the unit group of the finite residue field.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

instance finite_residueRootsOfUnityGroup
    (F : CompleteDVF.{u, v} K) [Finite F.residueField] :
    Finite
      (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)

instance

finite_valuationSubringUnits_nthPowerKernel

L47 ↗

LocalFieldTheory.DiscreteValuationField.finite_valuationSubringUnits_nthPowerKernel

Documentation

A nonzero power has only finitely many roots in the valuation-ring unit group, by injectivity of O_Kˣ → Kˣ.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

instance finite_valuationSubringUnits_nthPowerKernel
    (F : CompleteDVF.{u, v} K) (n : ℕ) [NeZero n] :
    Finite ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker)

instance

finite_principalUnits_nthPowerKernel

L59 ↗

LocalFieldTheory.DiscreteValuationField.finite_principalUnits_nthPowerKernel

Documentation

A nonzero power has finite kernel on the first principal-unit subgroup.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

instance finite_principalUnits_nthPowerKernel
    (F : CompleteDVF.{u, v} K) (n : ℕ) [NeZero n] :
    Finite
      ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
        ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker)

instance

finite_valuationSubringUnits_nthPowerQuotient

L73 ↗

LocalFieldTheory.DiscreteValuationField.finite_valuationSubringUnits_nthPowerQuotient

Documentation

Finiteness of the principal-unit power quotient implies finiteness of the full valuation-ring unit quotient through the root/principal product decomposition.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

instance finite_valuationSubringUnits_nthPowerQuotient
    (F : CompleteDVF.{u, v} K) [Finite F.residueField] (n : ℕ)
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)] :
    Finite (F.valuationSubringˣ ⧸ (powMonoidHom n : F.valuationSubringˣ →*
      F.valuationSubringˣ).range)

theorem

finite_fieldUnits_nthPowerQuotient_of_finite_principalUnits

L99 ↗

LocalFieldTheory.DiscreteValuationField.finite_fieldUnits_nthPowerQuotient_of_finite_principalUnits

Documentation

Finiteness of the principal-unit power quotient, together with a chosen uniformizer, explicitly yields finiteness of the full field-unit quotient. This remains a constructor rather than a global instance so the analytic finite boundary stays visible to callers.

Source context 9 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF) in

Lean source · statement

theorem finite_fieldUnits_nthPowerQuotient_of_finite_principalUnits
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (n : ℕ) [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)] :
    Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)

theorem

card_fieldUnits_nthPowerQuotient_eq_mul_unit_nthPowerQuotient

L131 ↗

LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_eq_mul_unit_nthPowerQuotient

Documentation

The local-field power-index formula, first equality: after choosing a uniformizer, the field-unit n-th-power quotient has the unit quotient as a factor and the uniformizer direction contributes exactly n.

Source context 9 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF) in

Lean source · statement

theorem card_fieldUnits_nthPowerQuotient_eq_mul_unit_nthPowerQuotient
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (n : ℕ) [NeZero n]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite (F.valuationSubringˣ ⧸ (powMonoidHom n : F.valuationSubringˣ →*
      F.valuationSubringˣ).range)] :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n * Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range)

theorem

card_unit_nthPowerQuotient_eq_mul_roots_principalUnit_nthPowerQuotient

L163 ↗

LocalFieldTheory.DiscreteValuationField.card_unit_nthPowerQuotient_eq_mul_roots_principalUnit_nthPowerQuotient

Documentation

The local-field power-index formula, unit-decomposition reduction: the unit n-th-power quotient splits into the residue root-of-unity factor and the first principal-unit factor.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_unit_nthPowerQuotient_eq_mul_roots_principalUnit_nthPowerQuotient
    (F : CompleteDVF.{u, v} K) [Finite F.residueField] (n : ℕ)
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)] :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card
          (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F ⧸
            (powMonoidHom n : (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)
              →* (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)).range) *
        Nat.card
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
            (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
              ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)

theorem

card_residueRoots_nthPowerQuotient_eq_nthPowerKernel

L193 ↗

LocalFieldTheory.DiscreteValuationField.card_residueRoots_nthPowerQuotient_eq_nthPowerKernel

Documentation

On the finite Teichmuller root factor, the n-th-power quotient has the same size as the subgroup killed by n.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_residueRoots_nthPowerQuotient_eq_nthPowerKernel
    (F : CompleteDVF.{u, v} K) [Finite F.residueField] (n : ℕ) :
    Nat.card
        (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F ⧸
          (powMonoidHom n : (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F) →*
            (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)).range) =
      Nat.card
        ((powMonoidHom n : (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F) →*
          (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)).ker)

theorem

card_unit_nthPowerKernel_eq_mul_roots_principalUnit_nthPowerKernel

L217 ↗

LocalFieldTheory.DiscreteValuationField.card_unit_nthPowerKernel_eq_mul_roots_principalUnit_nthPowerKernel

Documentation

The n-torsion kernel of the full unit group splits into the finite Teichmuller root factor and the first principal-unit factor.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_unit_nthPowerKernel_eq_mul_roots_principalUnit_nthPowerKernel
    (F : CompleteDVF.{u, v} K) [Finite F.residueField] (n : ℕ) [NeZero n] :
    Nat.card
        ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker) =
      Nat.card
          ((powMonoidHom n : (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)
            →* (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)).ker) *
        Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker)

theorem

card_fieldUnits_nthPowerKernel_eq_unit_nthPowerKernel

L244 ↗

LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerKernel_eq_unit_nthPowerKernel

Documentation

For nonzero n, the field-unit n-torsion kernel is the unit n-torsion kernel; the uniformizer direction has no nontrivial finite n-torsion.

Source context 9 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF) in

Lean source · statement

theorem card_fieldUnits_nthPowerKernel_eq_unit_nthPowerKernel
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (n : ℕ) [NeZero n] :
    Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) =
      Nat.card ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker)

theorem

card_fieldUnits_nthPowerKernel_eq_mul_roots_principalUnit_nthPowerKernel

L273 ↗

LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerKernel_eq_mul_roots_principalUnit_nthPowerKernel

Documentation

For nonzero n, the field-unit n-torsion kernel is the product of the Teichmuller n-torsion kernel and the first principal-unit n-torsion kernel. This is the group-theoretic μ_n(K) decomposition behind the local-field power-index formula.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_fieldUnits_nthPowerKernel_eq_mul_roots_principalUnit_nthPowerKernel
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (n : ℕ) [NeZero n] :
    Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) =
      Nat.card
          ((powMonoidHom n : (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)
            →* (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)).ker) *
        Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker)

theorem

card_unit_nthPowerQuotient_eq_mul_rootsKernel_principalUnit_nthPowerQuotient

L292 ↗

LocalFieldTheory.DiscreteValuationField.card_unit_nthPowerQuotient_eq_mul_rootsKernel_principalUnit_nthPowerQuotient

Documentation

The local-field power-index formula, unit-index reduction after identifying the finite root-of-unity quotient with its n-torsion kernel. The remaining analytic input is the principal-unit factor, supplied by the field-unit structure theorem.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_unit_nthPowerQuotient_eq_mul_rootsKernel_principalUnit_nthPowerQuotient
    (F : CompleteDVF.{u, v} K) [Finite F.residueField] (n : ℕ)
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)] :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card
          ((powMonoidHom n : (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)
            →* (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)).ker) *
        Nat.card
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
            (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
              ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)

theorem

card_unit_nthPowerQuotient_eq_mul_unitKernel_of_principalUnit_index

L314 ↗

LocalFieldTheory.DiscreteValuationField.card_unit_nthPowerQuotient_eq_mul_unitKernel_of_principalUnit_index

Documentation

The local-field power-index formula, unit-index form reduced to the analytic principal-unit input. If the field-unit structure theorem supplies the principal-unit quotient as its n-torsion kernel times a defect factor c, then the same defect multiplies the full unit n-torsion kernel.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_unit_nthPowerQuotient_eq_mul_unitKernel_of_principalUnit_index
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {n c : ℕ} [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hprincipal :
      Nat.card
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
            (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
              ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
        Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) * c) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker) * c

theorem

card_unit_nthPowerQuotient_eq_mul_unitKernel_residue_pow

L340 ↗

LocalFieldTheory.DiscreteValuationField.card_unit_nthPowerQuotient_eq_mul_unitKernel_residue_pow

Documentation

The local-field power-index formula, unit-index residue-power specialization. This is the unit-index formula once the analytic principal-unit input identifies the defect factor with the appropriate residue-cardinality power.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_unit_nthPowerQuotient_eq_mul_unitKernel_residue_pow
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {n a : ℕ} [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hprincipal :
      Nat.card
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
            (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
              ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
        Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) *
          Nat.card F.residueField ^ a) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker) *
        Nat.card F.residueField ^ a

theorem

card_unit_nthPowerQuotient_eq_mul_fieldKernel_of_principalUnit_index

L366 ↗

LocalFieldTheory.DiscreteValuationField.card_unit_nthPowerQuotient_eq_mul_fieldKernel_of_principalUnit_index

Documentation

Unit-index form with the kernel rewritten as the full field-unit n-torsion kernel. For nonzero n, the uniformizer direction contributes no torsion, so this is the exact kernel appearing in the local-field power-index formula.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_unit_nthPowerQuotient_eq_mul_fieldKernel_of_principalUnit_index
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {n c : ℕ} [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hprincipal :
      Nat.card
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
            (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
              ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
        Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) * c) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) * c

theorem

card_unit_nthPowerQuotient_eq_mul_fieldKernel_residue_pow

L392 ↗

LocalFieldTheory.DiscreteValuationField.card_unit_nthPowerQuotient_eq_mul_fieldKernel_residue_pow

Documentation

Residue-power specialization of the unit-index formula with the kernel written as the full field-unit n-torsion kernel.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_unit_nthPowerQuotient_eq_mul_fieldKernel_residue_pow
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {n a : ℕ} [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hprincipal :
      Nat.card
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
            (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
              ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
        Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) *
          Nat.card F.residueField ^ a) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) *
        Nat.card F.residueField ^ a

theorem

card_fieldUnits_nthPowerQuotient_eq_mul_rootsKernel_principalUnit_nthPowerQuotient

L419 ↗

LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_eq_mul_rootsKernel_principalUnit_nthPowerQuotient

Documentation

The local-field power-index formula, field-unit index reduced to the finite root factor and the principal-unit factor. The uniformizer contributes n; the finite root-of-unity factor is already expressed as its n-torsion kernel.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_fieldUnits_nthPowerQuotient_eq_mul_rootsKernel_principalUnit_nthPowerQuotient
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (n : ℕ) [NeZero n]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)] :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n *
        (Nat.card
            ((powMonoidHom n : (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)
              →* (CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F)).ker) *
          Nat.card
            ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
              (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
                ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range))

theorem

card_principalUnit_nthPowerQuotient_eq_subquotient_of_image_eq

L445 ↗

LocalFieldTheory.DiscreteValuationField.card_principalUnit_nthPowerQuotient_eq_subquotient_of_image_eq

Documentation

Principal-unit index reduction from an explicit n-th-power image level: if the n-th powers in U^1 are exactly U^m, then the principal-unit n-th-power quotient has the same cardinality as U^1/U^m.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_principalUnit_nthPowerQuotient_eq_subquotient_of_image_eq
    (F : CompleteDVF.{u, v} K) (n m : ℕ)
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    [Finite
      ((CompleteDVF.higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubquotient
        1 m)]
    (hpow :
      (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
        ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range =
        ((CompleteDVF.higherPrincipalUnitGroup F) m).subgroupOf
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)) :
    Nat.card
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
          (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
    Nat.card
        ((CompleteDVF.higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubquotient
          1 m)

theorem

card_principalUnit_nthPowerQuotient_eq_residue_pow_of_image_eq

L495 ↗

LocalFieldTheory.DiscreteValuationField.card_principalUnit_nthPowerQuotient_eq_residue_pow_of_image_eq

Documentation

Cardinality form of the preceding reduction after the finite-filtration counting of U^1/U^m: once the analytic input identifies the image of the n-th-power map on U^1 with U^m, the quotient has size #k^(m-1).

Source context 9 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (card_principalUnitSubquotient_one_eq_residue_pow_of_uniformizer) in

Lean source · statement

theorem card_principalUnit_nthPowerQuotient_eq_residue_pow_of_image_eq
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {n m : ℕ} (hm : 1 ≤ m)
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hpow :
      (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
        ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range =
        ((CompleteDVF.higherPrincipalUnitGroup F) m).subgroupOf
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)) :
    Nat.card
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
          (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
      Nat.card F.residueField ^ (m - 1)

theorem

card_principalUnit_nthPowerQuotient_eq_additive_nsmulQuotient_of_logEquiv

L528 ↗

LocalFieldTheory.DiscreteValuationField.card_principalUnit_nthPowerQuotient_eq_additive_nsmulQuotient_of_logEquiv

Documentation

The field-unit structure theorem logarithmic transport, principal-unit form: any multiplicative logarithm equivalence from U¹ to an additive group identifies the principal-unit n-th-power quotient with the additive quotient by n-fold multiples.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_principalUnit_nthPowerQuotient_eq_additive_nsmulQuotient_of_logEquiv
    (F : CompleteDVF.{u, v} K)
    (A : Type*) [AddCommGroup A]
    (n : ℕ)
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    [Finite (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)]
    (e : (CompleteDVF.higherPrincipalUnitGroup F) 1 ≃* Multiplicative A) :
    Nat.card
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
          (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
      Nat.card (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)

theorem

card_principalUnit_nthPowerKernel_eq_additive_nsmulKernel_of_logEquiv

L549 ↗

LocalFieldTheory.DiscreteValuationField.card_principalUnit_nthPowerKernel_eq_additive_nsmulKernel_of_logEquiv

Documentation

The field-unit structure theorem logarithmic transport, kernel form: under the same principal-unit logarithm equivalence, the principal-unit n-torsion kernel has the same cardinality as the additive kernel of x ↦ n • x.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_principalUnit_nthPowerKernel_eq_additive_nsmulKernel_of_logEquiv
    (F : CompleteDVF.{u, v} K)
    (A : Type*) [AddCommGroup A]
    (n : ℕ) [NeZero n]
    [Finite (LocalFieldTheory.nsmulAddKernel A n)]
    (e : (CompleteDVF.higherPrincipalUnitGroup F) 1 ≃* Multiplicative A) :
    Nat.card ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
      ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) =
      Nat.card (LocalFieldTheory.nsmulAddKernel A n)

theorem

card_principalUnit_nthPowerQuotient_eq_additive_quotient_of_logEquiv_nsmulAddSubgroup_eq

L564 ↗

LocalFieldTheory.DiscreteValuationField.card_principalUnit_nthPowerQuotient_eq_additive_quotient_of_logEquiv_nsmulAddSubgroup_eq

Documentation

The field-unit structure theorem logarithmic transport with a named additive image: if additive n-fold multiples are identified with a subgroup B, then the principal-unit quotient is the corresponding additive quotient.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_principalUnit_nthPowerQuotient_eq_additive_quotient_of_logEquiv_nsmulAddSubgroup_eq
    (F : CompleteDVF.{u, v} K)
    (A : Type*) [AddCommGroup A]
    (n : ℕ)
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    [Finite (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)]
    (e : (CompleteDVF.higherPrincipalUnitGroup F) 1 ≃* Multiplicative A)
    (B : AddSubgroup A)
    [Finite (A ⧸ B)]
    (hB : LocalFieldTheory.nsmulAddSubgroup A n = B) :
    Nat.card
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
          (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
      Nat.card (A ⧸ B)

theorem

card_principalUnit_nthPowerQuotient_eq_mul_kernel_of_logEquiv

L590 ↗

LocalFieldTheory.DiscreteValuationField.card_principalUnit_nthPowerQuotient_eq_mul_kernel_of_logEquiv

Documentation

The field-unit structure theorem logarithmic transport in kernel-factor form: after a principal-unit logarithm equivalence, a finite additive kernel/cokernel calculation immediately supplies the kernel times defect factor used by the local-field power-index formula.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_principalUnit_nthPowerQuotient_eq_mul_kernel_of_logEquiv
    (F : CompleteDVF.{u, v} K)
    (A : Type*) [AddCommGroup A]
    (n c : ℕ) [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    [Finite (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)]
    [Finite (LocalFieldTheory.nsmulAddKernel A n)]
    (e : (CompleteDVF.higherPrincipalUnitGroup F) 1 ≃* Multiplicative A)
    (hadd :
      Nat.card (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n) =
        Nat.card (LocalFieldTheory.nsmulAddKernel A n) * c) :
    Nat.card
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
          (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
      Nat.card ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
        ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) * c

theorem

card_principalUnit_nthPowerQuotient_eq_mul_kernel_residue_pow_of_logEquiv

L620 ↗

LocalFieldTheory.DiscreteValuationField.card_principalUnit_nthPowerQuotient_eq_mul_kernel_residue_pow_of_logEquiv

Documentation

The field-unit structure theorem logarithmic transport in the residue-defect form used in the local-field power-index formula: after a logarithm identifies U¹ with an additive group, an additive kernel/cokernel calculation with defect #k^a gives the principal-unit kernel times the same residue-power defect.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_principalUnit_nthPowerQuotient_eq_mul_kernel_residue_pow_of_logEquiv
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    (A : Type*) [AddCommGroup A]
    (n a : ℕ) [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    [Finite (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)]
    [Finite (LocalFieldTheory.nsmulAddKernel A n)]
    (e : (CompleteDVF.higherPrincipalUnitGroup F) 1 ≃* Multiplicative A)
    (hadd :
      Nat.card (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n) =
        Nat.card (LocalFieldTheory.nsmulAddKernel A n) * Nat.card F.residueField ^ a) :
    Nat.card
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
          (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
      Nat.card ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
        ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) *
        Nat.card F.residueField ^ a

theorem

card_principalUnit_nthPowerQuotient_eq_mul_kernel_residue_pow_of_image_eq_succ_of_kernel_one

L648 ↗

LocalFieldTheory.DiscreteValuationField.card_principalUnit_nthPowerQuotient_eq_mul_kernel_residue_pow_of_image_eq_succ_of_kernel_one

Documentation

The field-unit structure theorem defect-level wrapper in the kernel-factor form needed by the local-field power-index formula, in the common case where the principal-unit n-torsion kernel is trivial. The remaining input is the analytic image calculation (U¹)^n = U^(a+1).

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_principalUnit_nthPowerQuotient_eq_mul_kernel_residue_pow_of_image_eq_succ_of_kernel_one
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {n a : ℕ} [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hkernel :
      Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) = 1)
    (hpow :
      (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
        ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range =
        ((CompleteDVF.higherPrincipalUnitGroup F) (a + 1)).subgroupOf
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)) :
    Nat.card
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
          (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
        Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) *
        Nat.card F.residueField ^ a

theorem

unitQuotient_residuePow_of_principalImage

L681 ↗

LocalFieldTheory.DiscreteValuationField.PowerIndex.unitQuotient_residuePow_of_principalImage

Documentation

The local-field power-index formula unit-index specialization from an explicit principal-unit image level and a trivial principal-unit n-torsion kernel.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem PowerIndex.unitQuotient_residuePow_of_principalImage
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {n a : ℕ} [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hkernel :
      Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) = 1)
    (hpow :
      (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
        ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range =
        ((CompleteDVF.higherPrincipalUnitGroup F) (a + 1)).subgroupOf
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker) *
        Nat.card F.residueField ^ a

theorem

card_unit_nthPowerQuotient_eq_mul_unitKernel_of_logEquiv

L710 ↗

LocalFieldTheory.DiscreteValuationField.card_unit_nthPowerQuotient_eq_mul_unitKernel_of_logEquiv

Documentation

The local-field power-index formula, unit-index form fed directly by a principal-unit logarithm equivalence and an additive kernel/cokernel calculation.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_unit_nthPowerQuotient_eq_mul_unitKernel_of_logEquiv
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    (A : Type*) [AddCommGroup A]
    {n c : ℕ} [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    [Finite (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)]
    [Finite (LocalFieldTheory.nsmulAddKernel A n)]
    (e : (CompleteDVF.higherPrincipalUnitGroup F) 1 ≃* Multiplicative A)
    (hadd :
      Nat.card (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n) =
        Nat.card (LocalFieldTheory.nsmulAddKernel A n) * c) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker) * c

theorem

card_unit_nthPowerQuotient_eq_mul_unitKernel_residue_pow_of_logEquiv

L735 ↗

LocalFieldTheory.DiscreteValuationField.card_unit_nthPowerQuotient_eq_mul_unitKernel_residue_pow_of_logEquiv

Documentation

The local-field power-index formula, residue-power unit-index form fed directly by a principal-unit logarithm equivalence.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_unit_nthPowerQuotient_eq_mul_unitKernel_residue_pow_of_logEquiv
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    (A : Type*) [AddCommGroup A]
    {n a : ℕ} [NeZero n]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    [Finite (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)]
    [Finite (LocalFieldTheory.nsmulAddKernel A n)]
    (e : (CompleteDVF.higherPrincipalUnitGroup F) 1 ≃* Multiplicative A)
    (hadd :
      Nat.card (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n) =
        Nat.card (LocalFieldTheory.nsmulAddKernel A n) * Nat.card F.residueField ^ a) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker) *
        Nat.card F.residueField ^ a

theorem

card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_of_principalUnit_index

L760 ↗

LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_of_principalUnit_index

Documentation

The local-field power-index formula reduced to the analytic principal-unit index statement. If the field-unit structure theorem supplies the principal-unit quotient as its n-torsion kernel times a defect factor c, then the field-unit quotient is n times the field-unit n-torsion kernel times the same defect.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_of_principalUnit_index
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {n c : ℕ} [NeZero n]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hprincipal :
      Nat.card
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
            (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
              ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
        Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) * c) :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n * (Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) * c)

theorem

card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_of_logEquiv

L788 ↗

LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_of_logEquiv

Documentation

The local-field power-index formula, field-index form fed directly by a principal-unit logarithm equivalence and an additive kernel/cokernel calculation.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_of_logEquiv
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (A : Type*) [AddCommGroup A]
    {n c : ℕ} [NeZero n]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    [Finite (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)]
    [Finite (LocalFieldTheory.nsmulAddKernel A n)]
    (e : (CompleteDVF.higherPrincipalUnitGroup F) 1 ≃* Multiplicative A)
    (hadd :
      Nat.card (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n) =
        Nat.card (LocalFieldTheory.nsmulAddKernel A n) * c) :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n * (Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) * c)

theorem

card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_residue_pow

L816 ↗

LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_residue_pow

Documentation

The local-field power-index formula in the residue-power defect form expected from the field-unit structure theorem: once the principal-unit quotient is known to be its n-torsion kernel times #k^a, the field-unit quotient has the same defect factor and the additional uniformizer factor n.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_residue_pow
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {n a : ℕ} [NeZero n]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hprincipal :
      Nat.card
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
            (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
              ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range) =
        Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) *
          Nat.card F.residueField ^ a) :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n *
        (Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) *
          Nat.card F.residueField ^ a)

theorem

card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_residue_pow_of_logEquiv

L844 ↗

LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_residue_pow_of_logEquiv

Documentation

The local-field power-index formula, residue-power field-index form fed directly by a principal-unit logarithm equivalence. This is the public bridge from the additive principal-unit calculation to the final field-unit index formula.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem card_fieldUnits_nthPowerQuotient_eq_mul_fieldKernel_residue_pow_of_logEquiv
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (A : Type*) [AddCommGroup A]
    {n a : ℕ} [NeZero n]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    [Finite (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)]
    [Finite (LocalFieldTheory.nsmulAddKernel A n)]
    (e : (CompleteDVF.higherPrincipalUnitGroup F) 1 ≃* Multiplicative A)
    (hadd :
      Nat.card (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n) =
        Nat.card (LocalFieldTheory.nsmulAddKernel A n) * Nat.card F.residueField ^ a) :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n *
        (Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) *
          Nat.card F.residueField ^ a)

theorem

fieldQuotient_residuePow_of_principalImage

L870 ↗

LocalFieldTheory.DiscreteValuationField.PowerIndex.fieldQuotient_residuePow_of_principalImage

Documentation

The local-field power-index formula field-index specialization from an explicit principal-unit image level and a trivial principal-unit n-torsion kernel.

Source context 8 commands

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

noncomputable section
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
section CompleteDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem PowerIndex.fieldQuotient_residuePow_of_principalImage
    (F : CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {n a : ℕ} [NeZero n]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
          ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range)]
    (hkernel :
      Nat.card
          ((powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
            ((CompleteDVF.higherPrincipalUnitGroup F) 1)).ker) = 1)
    (hpow :
      (powMonoidHom n : ((CompleteDVF.higherPrincipalUnitGroup F) 1) →*
        ((CompleteDVF.higherPrincipalUnitGroup F) 1)).range =
        ((CompleteDVF.higherPrincipalUnitGroup F) (a + 1)).subgroupOf
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)) :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n *
        (Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) *
          Nat.card F.residueField ^ a)

Module documentation

Power-index computations for complete discrete valuation fields

Declarations