NYLL
Module

PadicPowerIndex.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PadicPowerIndex
35 declarations indexed from sourceView source ↗

Module documentation

The n-fold multiple quotient of Z_p

This is the free p-adic factor in the local-field structure theory, the local-field power-index formula.

The exact equal-characteristic specialization, with no artificial finite factor in the principal-unit product.

Imports3
Imported by4

Declarations

def

normalizedLocalNatAbs

L35 ↗
LocalFieldTheory.DiscreteValuationField.normalizedLocalNatAbs
Documentation

The normalized local absolute value of a natural number in a degree-d mixed-characteristic local field. Since d = ef and q = p^f, this is exactly q^(-e v_p(n)), the normalized factor |n|_𝔭.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
def normalizedLocalNatAbs (p d n : ℕ) : ℚ
theorem

one_div_normalizedLocalNatAbs

L41 ↗
LocalFieldTheory.DiscreteValuationField.one_div_normalizedLocalNatAbs
Documentation

The reciprocal of the normalized local absolute value is the integral defect factor occurring in the local-field power-index formula.

Source context 8 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
omit [Fact p.Prime] in
Lean source · statement
theorem one_div_normalizedLocalNatAbs (d n : ℕ) :
    1 / normalizedLocalNatAbs p d n =
      (p ^ (d * padicValNat p n) : ℕ)
theorem

nsmulAddSubgroup_padicInt_eq_span

L49 ↗
LocalFieldTheory.DiscreteValuationField.nsmulAddSubgroup_padicInt_eq_span
Documentation

Additive n-fold multiples in Z_p are the principal ideal generated by the natural number n.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem nsmulAddSubgroup_padicInt_eq_span (n : ℕ) :
    LocalFieldTheory.nsmulAddSubgroup ℤ_[p] n =
      (Ideal.span ({(n : ℤ_[p])} : Set ℤ_[p])).toAddSubgroup
theorem

padicInt_valuation_natCast

L66 ↗
LocalFieldTheory.DiscreteValuationField.padicInt_valuation_natCast
Documentation

The valuation of a nonzero natural number in Z_p is v_p(n).

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem padicInt_valuation_natCast (n : ℕ) :
    (n : ℤ_[p]).valuation = padicValNat p n
theorem

padicInt_span_natCast_eq_span_p_pow_padicValNat

L77 ↗
LocalFieldTheory.DiscreteValuationField.padicInt_span_natCast_eq_span_p_pow_padicValNat
Documentation

A nonzero natural number generates the same ideal in Z_p as the corresponding power of p.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem padicInt_span_natCast_eq_span_p_pow_padicValNat
    (n : ℕ) (hn : n ≠ 0) :
    Ideal.span ({(n : ℤ_[p])} : Set ℤ_[p]) =
      Ideal.span ({(p : ℤ_[p]) ^ padicValNat p n} : Set ℤ_[p])
theorem

nsmulAddSubgroup_padicInt_eq_ker_toZModPow

L90 ↗
LocalFieldTheory.DiscreteValuationField.nsmulAddSubgroup_padicInt_eq_ker_toZModPow
Documentation

The subgroup of n-fold multiples is the kernel of reduction modulo p ^ v_p(n).

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem nsmulAddSubgroup_padicInt_eq_ker_toZModPow
    (n : ℕ) (hn : n ≠ 0) :
    LocalFieldTheory.nsmulAddSubgroup ℤ_[p] n =
      (PadicInt.toZModPow (p := p) (padicValNat p n)).toAddMonoidHom.ker
def

padicIntNsmulQuotientEquivZMod

L101 ↗
LocalFieldTheory.DiscreteValuationField.padicIntNsmulQuotientEquivZMod
Documentation

The additive quotient Z_p / n Z_p is the expected finite cyclic group of order p ^ v_p(n).

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
def padicIntNsmulQuotientEquivZMod
    (n : ℕ) (hn : n ≠ 0) :
    ℤ_[p] ⧸ LocalFieldTheory.nsmulAddSubgroup ℤ_[p] n ≃+
      ZMod (p ^ padicValNat p n)
instance

finite_padicInt_nsmulQuotient

L118 ↗
LocalFieldTheory.DiscreteValuationField.finite_padicInt_nsmulQuotient
Documentation

The quotient Z_p / n Z_p is finite for nonzero n, transported from its canonical ZMod model.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
instance finite_padicInt_nsmulQuotient
    (n : ℕ) [NeZero n] :
    Finite (ℤ_[p] ⧸ LocalFieldTheory.nsmulAddSubgroup ℤ_[p] n)
theorem

card_padicInt_nsmulQuotient

L125 ↗
LocalFieldTheory.DiscreteValuationField.card_padicInt_nsmulQuotient
Documentation

Cardinality of the one-dimensional p-adic free-factor quotient.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem card_padicInt_nsmulQuotient
    (n : ℕ) [NeZero n] :
    Nat.card (ℤ_[p] ⧸ LocalFieldTheory.nsmulAddSubgroup ℤ_[p] n) =
      p ^ padicValNat p n
def

padicIntPiNsmulQuotientEquiv

L135 ↗
LocalFieldTheory.DiscreteValuationField.padicIntPiNsmulQuotientEquiv
Documentation

Coordinatewise reduction identifies the quotient of an arbitrary product of copies of Z_p by n-fold multiples with a product of finite cyclic groups.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
def padicIntPiNsmulQuotientEquiv
    {ι : Type u} (n : ℕ) (hn : n ≠ 0) :
    (ι → ℤ_[p]) ⧸ LocalFieldTheory.nsmulAddSubgroup (ι → ℤ_[p]) n ≃+
      (ι → ZMod (p ^ padicValNat p n))
instance

finite_padicInt_finPi_nsmulQuotient

L187 ↗
LocalFieldTheory.DiscreteValuationField.finite_padicInt_finPi_nsmulQuotient
Documentation

A finite product of nonzero scalar quotients of Z_p is finite.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
instance finite_padicInt_finPi_nsmulQuotient
    (d n : ℕ) [NeZero n] :
    Finite ((Fin d → ℤ_[p]) ⧸
      LocalFieldTheory.nsmulAddSubgroup (Fin d → ℤ_[p]) n)
theorem

card_padicInt_finPi_nsmulQuotient

L198 ↗
LocalFieldTheory.DiscreteValuationField.card_padicInt_finPi_nsmulQuotient
Documentation

A finite product of d copies contributes the expected p^(d v_p(n)) factor.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem card_padicInt_finPi_nsmulQuotient
    (d n : ℕ) [NeZero n] :
    Nat.card ((Fin d → ℤ_[p]) ⧸
        LocalFieldTheory.nsmulAddSubgroup (Fin d → ℤ_[p]) n) =
      p ^ (d * padicValNat p n)
instance

finite_padicInt_pi_nsmulQuotient_of_coprime

L213 ↗
LocalFieldTheory.DiscreteValuationField.finite_padicInt_pi_nsmulQuotient_of_coprime
Documentation

If n is nonzero and prime to p, the quotient of an arbitrary product of copies of Z_p is finite (indeed, a singleton).

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
instance finite_padicInt_pi_nsmulQuotient_of_coprime
    {ι : Type u} (n : ℕ) [NeZero n] [Fact (Nat.Coprime n p)] :
    Finite ((ι → ℤ_[p]) ⧸ LocalFieldTheory.nsmulAddSubgroup (ι → ℤ_[p]) n)
theorem

card_padicInt_pi_nsmulQuotient_of_coprime

L235 ↗
LocalFieldTheory.DiscreteValuationField.card_padicInt_pi_nsmulQuotient_of_coprime
Documentation

If n is prime to p, multiplication by n is surjective on an arbitrary product of copies of Z_p; hence the quotient is trivial.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem card_padicInt_pi_nsmulQuotient_of_coprime
    {ι : Type u} (n : ℕ) [NeZero n] [Fact (Nat.Coprime n p)] :
    Nat.card ((ι → ℤ_[p]) ⧸
        LocalFieldTheory.nsmulAddSubgroup (ι → ℤ_[p]) n) = 1
theorem

nsmulAddKernel_padicInt_pi_eq_bot

L250 ↗
LocalFieldTheory.DiscreteValuationField.nsmulAddKernel_padicInt_pi_eq_bot
Documentation

A nonzero natural scalar has trivial kernel on any product of Z_p.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem nsmulAddKernel_padicInt_pi_eq_bot
    {ι : Type u} (n : ℕ) (hn : n ≠ 0) :
    LocalFieldTheory.nsmulAddKernel (ι → ℤ_[p]) n = ⊥
instance

finite_nsmulAddKernel_padicInt_pi

L269 ↗
LocalFieldTheory.DiscreteValuationField.finite_nsmulAddKernel_padicInt_pi
Documentation

Nonzero scalar multiplication has a finite (trivial) kernel on any product of copies of Z_p.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
instance finite_nsmulAddKernel_padicInt_pi
    {ι : Type u} (n : ℕ) [NeZero n] :
    Finite (LocalFieldTheory.nsmulAddKernel (ι → ℤ_[p]) n)
theorem

card_nsmulAddKernel_padicInt_pi

L276 ↗
LocalFieldTheory.DiscreteValuationField.card_nsmulAddKernel_padicInt_pi
Documentation

Cardinal form of the preceding torsion-freeness statement.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem card_nsmulAddKernel_padicInt_pi
    {ι : Type u} (n : ℕ) [NeZero n] :
    Nat.card (LocalFieldTheory.nsmulAddKernel (ι → ℤ_[p]) n) = 1
theorem

card_nsmulAddQuotient_product

L288 ↗
LocalFieldTheory.DiscreteValuationField.card_nsmulAddQuotient_product
Documentation

Additive quotients by n-fold multiples commute with binary products at the level of cardinality.

Source context 9 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section Product
variable (A B : Type*) [AddCommGroup A] [AddCommGroup B]
Lean source · statement
theorem card_nsmulAddQuotient_product (n : ℕ)
    [Finite (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n)]
    [Finite (B ⧸ LocalFieldTheory.nsmulAddSubgroup B n)] :
    Nat.card ((A × B) ⧸ LocalFieldTheory.nsmulAddSubgroup (A × B) n) =
      Nat.card (A ⧸ LocalFieldTheory.nsmulAddSubgroup A n) *
        Nat.card (B ⧸ LocalFieldTheory.nsmulAddSubgroup B n)
theorem

card_nsmulAddKernel_product

L314 ↗
LocalFieldTheory.DiscreteValuationField.card_nsmulAddKernel_product
Documentation

Kernels of n-fold multiplication commute with binary products at the level of cardinality.

Source context 9 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section Product
variable (A B : Type*) [AddCommGroup A] [AddCommGroup B]
Lean source · statement
theorem card_nsmulAddKernel_product (n : ℕ)
    [Finite (LocalFieldTheory.nsmulAddKernel A n)]
    [Finite (LocalFieldTheory.nsmulAddKernel B n)] :
    Nat.card (LocalFieldTheory.nsmulAddKernel (A × B) n) =
      Nat.card (LocalFieldTheory.nsmulAddKernel A n) * Nat.card (LocalFieldTheory.nsmulAddKernel
        B n)
theorem

card_finite_prod_padicInt_finPi_nsmulQuotient_eq_kernel_mul

L344 ↗
LocalFieldTheory.DiscreteValuationField.card_finite_prod_padicInt_finPi_nsmulQuotient_eq_kernel_mul
Documentation

Mixed-characteristic free-factor calculation in the exact kernel-times- defect form used by the local-field power-index formula.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem card_finite_prod_padicInt_finPi_nsmulQuotient_eq_kernel_mul
    (T : Type*) [AddCommGroup T] [Finite T]
    (d n : ℕ) [NeZero n] :
    Nat.card ((T × (Fin d → ℤ_[p])) ⧸
        LocalFieldTheory.nsmulAddSubgroup (T × (Fin d → ℤ_[p])) n) =
      Nat.card (LocalFieldTheory.nsmulAddKernel (T × (Fin d → ℤ_[p])) n) *
        p ^ (d * padicValNat p n)
theorem

card_finite_prod_padicInt_pi_nsmulQuotient_eq_kernel_of_coprime

L360 ↗
LocalFieldTheory.DiscreteValuationField.card_finite_prod_padicInt_pi_nsmulQuotient_eq_kernel_of_coprime
Documentation

Equal-characteristic free-factor calculation: when p ∤ n, an arbitrary product of copies of Z_p contributes neither kernel nor cokernel.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
theorem card_finite_prod_padicInt_pi_nsmulQuotient_eq_kernel_of_coprime
    {ι : Type u} (T : Type*) [AddCommGroup T] [Finite T]
    (n : ℕ) [NeZero n] [Fact (Nat.Coprime n p)] :
    Nat.card ((T × (ι → ℤ_[p])) ⧸
        LocalFieldTheory.nsmulAddSubgroup (T × (ι → ℤ_[p])) n) =
      Nat.card (LocalFieldTheory.nsmulAddKernel (T × (ι → ℤ_[p])) n)
theorem

card_fieldUnits_nthPowerQuotient_of_mixedPrincipalUnitStructure

L381 ↗
LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_of_mixedPrincipalUnitStructure
Documentation

The local-field power-index formula, mixed-characteristic field-index formula supplied directly by a principal-unit structure theorem.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_fieldUnits_nthPowerQuotient_of_mixedPrincipalUnitStructure
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (T : Type*) [AddCommGroup T] [Finite T]
    (d : ℕ) {n : ℕ} [NeZero n]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (Fin d → ℤ_[p]))) :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n * (Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) *
        p ^ (d * padicValNat p n))
theorem

card_fieldUnits_nthPowerQuotient_of_mixedPrincipalUnitStructure_rationalFormula

L406 ↗
LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_of_mixedPrincipalUnitStructure_rationalFormula
Documentation

Literal rational form of the mixed-characteristic field formula: (Kˣ : Kˣⁿ) = n #μ_n(K) / |n|_𝔭.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_fieldUnits_nthPowerQuotient_of_mixedPrincipalUnitStructure_rationalFormula
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (T : Type*) [AddCommGroup T] [Finite T]
    (d : ℕ) {n : ℕ} [NeZero n]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (Fin d → ℤ_[p]))) :
    (Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) : ℚ) =
      (n * Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) : ℕ) /
        normalizedLocalNatAbs p d n
theorem

card_units_nthPowerQuotient_of_mixedPrincipalUnitStructure

L440 ↗
LocalFieldTheory.DiscreteValuationField.card_units_nthPowerQuotient_of_mixedPrincipalUnitStructure
Documentation

The local-field power-index formula, mixed-characteristic unit-index formula from the same principal-unit structure theorem.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_units_nthPowerQuotient_of_mixedPrincipalUnitStructure
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    (T : Type*) [AddCommGroup T] [Finite T]
    (d : ℕ) {n : ℕ} [NeZero n]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (Fin d → ℤ_[p]))) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker) *
        p ^ (d * padicValNat p n)
theorem

card_units_nthPowerQuotient_of_mixedPrincipalUnitStructure_fieldKernel

L464 ↗
LocalFieldTheory.DiscreteValuationField.card_units_nthPowerQuotient_of_mixedPrincipalUnitStructure_fieldKernel
Documentation

The same mixed-characteristic unit formula with the finite kernel written as the full field root group μ_n(K).

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_units_nthPowerQuotient_of_mixedPrincipalUnitStructure_fieldKernel
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (T : Type*) [AddCommGroup T] [Finite T]
    (d : ℕ) {n : ℕ} [NeZero n]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (Fin d → ℤ_[p]))) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) *
        p ^ (d * padicValNat p n)
theorem

card_units_nthPowerQuotient_of_mixedPrincipalUnitStructure_rationalFormula

L489 ↗
LocalFieldTheory.DiscreteValuationField.card_units_nthPowerQuotient_of_mixedPrincipalUnitStructure_rationalFormula
Documentation

Literal rational form of the mixed-characteristic unit formula: (U : Uⁿ) = #μ_n(K) / |n|_𝔭.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_units_nthPowerQuotient_of_mixedPrincipalUnitStructure_rationalFormula
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (T : Type*) [AddCommGroup T] [Finite T]
    (d : ℕ) {n : ℕ} [NeZero n]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (Fin d → ℤ_[p]))) :
    (Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) : ℚ) =
      Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) /
        normalizedLocalNatAbs p d n
theorem

card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitStructure

L523 ↗
LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitStructure
Documentation

The local-field power-index formula obtained in equal characteristic from the field-unit structure theorem, the principal-unit product, and the hypothesis p ∤ n.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitStructure
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {ι : Type u} (T : Type*) [AddCommGroup T] [Finite T]
    {n : ℕ} [NeZero n] [Fact (Nat.Coprime n p)]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (ι → ℤ_[p]))) :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n * Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker)
theorem

card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitStructure_rationalFormula

L552 ↗
LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitStructure_rationalFormula
Documentation

Literal rational form of the equal-characteristic field formula. Here the permitted hypothesis (n,p)=1 makes the local absolute value equal to one, represented uniformly as normalizedLocalNatAbs p 0 n.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitStructure_rationalFormula
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {ι : Type u} (T : Type*) [AddCommGroup T] [Finite T]
    {n : ℕ} [NeZero n] [Fact (Nat.Coprime n p)]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (ι → ℤ_[p]))) :
    (Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) : ℚ) =
      (n * Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) : ℕ) /
        normalizedLocalNatAbs p 0 n
theorem

card_units_nthPowerQuotient_of_equalPrincipalUnitStructure

L575 ↗
LocalFieldTheory.DiscreteValuationField.card_units_nthPowerQuotient_of_equalPrincipalUnitStructure
Documentation

The local-field power-index formula, equal-characteristic unit-index formula.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_units_nthPowerQuotient_of_equalPrincipalUnitStructure
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {ι : Type u} (T : Type*) [AddCommGroup T] [Finite T]
    {n : ℕ} [NeZero n] [Fact (Nat.Coprime n p)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (ι → ℤ_[p]))) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).ker)
theorem

card_units_nthPowerQuotient_of_equalPrincipalUnitStructure_fieldKernel

L602 ↗
LocalFieldTheory.DiscreteValuationField.card_units_nthPowerQuotient_of_equalPrincipalUnitStructure_fieldKernel
Documentation

The equal-characteristic unit formula with its kernel written as μ_n(K).

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_units_nthPowerQuotient_of_equalPrincipalUnitStructure_fieldKernel
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {ι : Type u} (T : Type*) [AddCommGroup T] [Finite T]
    {n : ℕ} [NeZero n] [Fact (Nat.Coprime n p)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (ι → ℤ_[p]))) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker)
theorem

card_units_nthPowerQuotient_of_equalPrincipalUnitStructure_rationalFormula

L625 ↗
LocalFieldTheory.DiscreteValuationField.card_units_nthPowerQuotient_of_equalPrincipalUnitStructure_rationalFormula
Documentation

Literal rational form of the equal-characteristic unit formula.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_units_nthPowerQuotient_of_equalPrincipalUnitStructure_rationalFormula
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {ι : Type u} (T : Type*) [AddCommGroup T] [Finite T]
    {n : ℕ} [NeZero n] [Fact (Nat.Coprime n p)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (T × (ι → ℤ_[p]))) :
    (Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) : ℚ) =
      Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) /
        normalizedLocalNatAbs p 0 n
theorem

card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitProduct

L652 ↗
LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitProduct
Documentation

Equal-characteristic field index from the literal the field-unit structure theorem product U^1 ≃ Z_p^ι.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitProduct
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {ι : Type u} {n : ℕ} [NeZero n] [Fact (Nat.Coprime n p)]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (ι → ℤ_[p])) :
    Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) =
      n * Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker)
theorem

card_units_nthPowerQuotient_of_equalPrincipalUnitProduct

L678 ↗
LocalFieldTheory.DiscreteValuationField.card_units_nthPowerQuotient_of_equalPrincipalUnitProduct
Documentation

Equal-characteristic unit index from the literal principal-unit product, with its torsion kernel written as the field root group μ_n(K).

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_units_nthPowerQuotient_of_equalPrincipalUnitProduct
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {ι : Type u} {n : ℕ} [NeZero n] [Fact (Nat.Coprime n p)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (ι → ℤ_[p])) :
    Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) =
      Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker)
theorem

card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitProduct_rationalFormula

L711 ↗
LocalFieldTheory.DiscreteValuationField.card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitProduct_rationalFormula
Documentation

Literal rational field formula in equal characteristic.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_fieldUnits_nthPowerQuotient_of_equalPrincipalUnitProduct_rationalFormula
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {ι : Type u} {n : ℕ} [NeZero n] [Fact (Nat.Coprime n p)]
    [Finite (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (ι → ℤ_[p])) :
    (Nat.card (Kˣ ⧸ (powMonoidHom n : Kˣ →* Kˣ).range) : ℚ) =
      (n * Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) : ℕ) /
        normalizedLocalNatAbs p 0 n
theorem

card_units_nthPowerQuotient_of_equalPrincipalUnitProduct_rationalFormula

L733 ↗
LocalFieldTheory.DiscreteValuationField.card_units_nthPowerQuotient_of_equalPrincipalUnitProduct_rationalFormula
Documentation

Literal rational unit formula in equal characteristic.

Source context 10 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
namespace LocalFieldTheory.DiscreteValuationField
variable {p : ℕ} [Fact p.Prime]
section LocalFieldIndex
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem card_units_nthPowerQuotient_of_equalPrincipalUnitProduct_rationalFormula
    (F : CompleteDVF.{u, 0} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {ι : Type u} {n : ℕ} [NeZero n] [Fact (Nat.Coprime n p)]
    [Finite
      ((higherPrincipalUnitGroup F) 1 ⧸
        (powMonoidHom n : ((higherPrincipalUnitGroup F) 1) →* ((higherPrincipalUnitGroup F) 1)
          ).range)]
    (e : (higherPrincipalUnitGroup F) 1 ≃*
      Multiplicative (ι → ℤ_[p])) :
    (Nat.card (F.valuationSubringˣ ⧸
        (powMonoidHom n : F.valuationSubringˣ →* F.valuationSubringˣ).range) : ℚ) =
      Nat.card ((powMonoidHom n : Kˣ →* Kˣ).ker) /
        normalizedLocalNatAbs p 0 n

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