NYLL
Module

IntegralLattice.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.MixedCharacteristicStructure.IntegralLattice
63 declarations indexed from sourceView source ↗

Module documentation

The integral lattice of a mixed-characteristic local field

This file identifies the integer ring of a mixed-characteristic local field with the integral closure of the p-adic integers. In particular it supplies the finite free Z_p lattice of rank [K : Q_p] used in the proof of the mixed-characteristic field-unit structure theorem. The comparison is made for the canonical copy of Q_p constructed in the local-field structure classification, not for a separately assumed scalar action.

Canonical mixed-characteristic scalar context

the canonical Z_p integral basis

The canonical Z_p action on U^r

Imports10
Imported by4

Declarations

class

MixedQPadicContext

L48 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.MixedQPadicContext
Documentation

The canonical Q_p scalar context supplied by a mixed-characteristic local field. It carries the residue-characteristic prime witness; installing it also installs the coherent algebra and finite-dimensional structures.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
class MixedQPadicContext (F : LocalField.{u, v} K) : Prop where
  /-- The residue characteristic of a mixed-characteristic local field is prime. -/
  residueCharacteristic_prime : F.residueCharacteristic.Prime
theorem

mixedQPadicContext

L53 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedQPadicContext
Documentation

The canonical Q_p scalar context attached to F.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
theorem mixedQPadicContext (F : LocalField.{u, v} K) :
    MixedQPadicContext F
instance

mixedQPadicContextFact

L58 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedQPadicContextFact
Documentation

Registers the mathematical fact Fact F.residueCharacteristic.Prime for typeclass inference.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedQPadicContextFact
    (F : LocalField.{u, v} K) [ctx : MixedQPadicContext F] :
    Fact F.residueCharacteristic.Prime
instance

mixedQPadicContextAlgebra

L67 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedQPadicContextAlgebra
Documentation

Equips the target with its canonical Algebra structure, namely Algebra ℚ_[F.residueCharacteristic] K.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedQPadicContextAlgebra
    (F : LocalField.{u, v} K) [CharZero K] [MixedQPadicContext F] :
    Algebra ℚ_[F.residueCharacteristic] K
instance

mixedQPadicContextFiniteDimensional

L76 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedQPadicContextFiniteDimensional
Documentation

Equips the target with its canonical FiniteDimensional structure, namely FiniteDimensional ℚ_[F.residueCharacteristic] K.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedQPadicContextFiniteDimensional
    (F : LocalField.{u, v} K) [CharZero K] [MixedQPadicContext F] :
    FiniteDimensional ℚ_[F.residueCharacteristic] K
theorem

padicDVRValuation_le_one_iff_norm_le_one

L83 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.padicDVRValuation_le_one_iff_norm_le_one
Documentation

The DVR valuation on Q_p has closed unit ball equal to the usual subring Z_p.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
theorem padicDVRValuation_le_one_iff_norm_le_one
    (p : ℕ) [Fact p.Prime] (x : ℚ_[p]) :
    Examples.Qp.padicDVRValuation p x ≤ 1 ↔ ‖x‖ ≤ 1
theorem

qpadicInt_algebraMap_mem_valuationSubring

L105 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.qpadicInt_algebraMap_mem_valuationSubring
Documentation

The canonical embedding Q_p → K takes Z_p into the valuation subring. This is proved by density of the ordinary natural numbers and closedness of the valuation subring.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem qpadicInt_algebraMap_mem_valuationSubring
    (F : LocalField.{u, v} K) [CharZero K]
    (z : ℤ_[F.residueCharacteristic]) :
    letI : MixedQPadicContext F := mixedQPadicContext F
    algebraMap ℚ_[F.residueCharacteristic] K (z : ℚ_[F.residueCharacteristic]) ∈
      F.toCompleteDVF.valuation.valuationSubring := by
  let p : ℕ := F.residueCharacteristic
  let : MixedQPadicContext F := mixedQPadicContext F
  let : Fact p.Prime := ⟨F.residueCharacteristic_prime⟩
  let : Valued K F.mrangeValueGroup :=
    _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F.toCompleteDVF
  let : NontriviallyNormedField K :=
    CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  have hcontinuous : Continuous (algebraMap ℚ_[p] K) := by
    change Continuous
      (fun x : ℚ_[p] =>
        ((F.qpadicNumbersEquivQpadicClosureSubfield x :
          F.qpadicClosureSubfield) : K))
    exact continuous_subtype_val.comp
      F.qpadicNumbersToQpadicClosureSubfield_isUniformInducing.uniformContinuous.continuous
  have hclosed : IsClosed
      {x : ℤ_[p] |
        _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F.toCompleteDVF
            (algebraMap ℚ_[p] K (x : ℚ_[p])) ≤ 1} := by
    have hvclosed : IsClosed
        {x : K | CompleteDVF.mrangeRestrict F.toCompleteDVF x ≤ 1} := by
      have hset :
          {x : K |
              _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
                F.toCompleteDVF x ≤ 1} =
            ((Valued.v : Valuation K
              (MonoidHom.mrange
                F.toCompleteDVF.valuation.toMonoidWithZeroHom)).valuationSubring :
              Set K) := by
        ext x
        change
          _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
                F.toCompleteDVF x ≤ 1 ↔
            (Valued.v : Valuation K
              (MonoidHom.mrange
                F.toCompleteDVF.valuation.toMonoidWithZeroHom)) x ≤ 1
        rfl
      rw [hset]
      exact Valued.isClosed_valuationSubring K
    exact hvclosed.preimage
      (hcontinuous.comp continuous_subtype_val)
  have hz' :
      _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F.toCompleteDVF
          (algebraMap ℚ_[p] K (z : ℚ_[p])) ≤ 1 := by
    refine PadicInt.denseRange_natCast.induction_on z hclosed ?_
    intro n
    change _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F.toCompleteDVF
        (algebraMap ℚ_[p] K ((n : ℤ_[p]) : ℚ_[p])) ≤ 1
    rw [← Subtype.coe_le_coe]
    simpa [_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_apply] using
      F.valuation_natCast_le_one n
  rw [← Subtype.coe_le_coe] at hz'
  simpa [CompleteDVF.mrangeRestrict_apply, p] using hz'
theorem

qpadicNumbersAlgebra_mem_valuationSubring_iff

L167 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.qpadicNumbersAlgebra_mem_valuationSubring_iff
Documentation

Pulling the valuation ring of K back along the canonical Q_p map recovers precisely Z_p. The reverse implication uses the DVR identity m_(Z_p) = p Z_p and the strict inequality v_K(p) < 1.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem qpadicNumbersAlgebra_mem_valuationSubring_iff
    (F : LocalField.{u, v} K) [CharZero K]
    (x : ℚ_[F.residueCharacteristic]) :
    letI : MixedQPadicContext F := mixedQPadicContext F
    algebraMap ℚ_[F.residueCharacteristic] K x ∈
        F.toCompleteDVF.valuation.valuationSubring ↔
      ‖x‖ ≤ 1 := by
  let p : ℕ := F.residueCharacteristic
  let : MixedQPadicContext F := mixedQPadicContext F
  let : Fact p.Prime := ⟨F.residueCharacteristic_prime⟩
  constructor
  · intro hx
    by_contra hxnorm
    have hnorm : 1 < ‖x‖ := lt_of_not_ge hxnorm
    have hx0 : x ≠ 0 := by
      intro hzero
      have : ¬ (1 : ℝ) < 0 := not_lt_of_ge zero_le_one
      exact this (by simpa [hzero] using hnorm)
    have hinvnorm : ‖x⁻¹‖ < 1 := by
      rw [norm_inv]
      exact inv_lt_one_of_one_lt₀ hnorm
    let y : ℤ_[p] := ⟨x⁻¹, hinvnorm.le⟩
    have hymax : y ∈ IsLocalRing.maximalIdeal ℤ_[p] := by
      rw [IsLocalRing.mem_maximalIdeal, PadicInt.mem_nonunits]
      exact hinvnorm
    rw [PadicInt.maximalIdeal_eq_span_p,
      Ideal.mem_span_singleton] at hymax
    obtain ⟨c, hc⟩ := hymax
    have hcmem :
        algebraMap ℚ_[p] K (c : ℚ_[p]) ∈
          F.toCompleteDVF.valuation.valuationSubring := by
      simpa [p] using
        F.qpadicInt_algebraMap_mem_valuationSubring c
    have hcval :
        F.toCompleteDVF.valuation
            (algebraMap ℚ_[p] K (c : ℚ_[p])) ≤ 1 :=
      (F.toCompleteDVF.mem_valuationSubring_iff _).1 hcmem
    have hpval :
        F.toCompleteDVF.valuation
            (algebraMap ℚ_[p] K (p : ℚ_[p])) < 1 := by
      simpa [p] using
        F.valuation_natCast_residueCharacteristic_lt_one
    have hyfield : (y : ℚ_[p]) = (p : ℚ_[p]) * (c : ℚ_[p]) := by
      simpa [mul_comm] using congrArg (fun z : ℤ_[p] => (z : ℚ_[p])) hc
    have hyval :
        F.toCompleteDVF.valuation
            (algebraMap ℚ_[p] K (y : ℚ_[p])) < 1 := by
      rw [hyfield, map_mul, F.toCompleteDVF.valuation.map_mul]
      exact mul_lt_one_of_lt_of_le hpval hcval
    have hprod :
        F.toCompleteDVF.valuation (algebraMap ℚ_[p] K x) *
            F.toCompleteDVF.valuation
              (algebraMap ℚ_[p] K (x⁻¹)) < 1 := by
      apply Right.mul_lt_one_of_le_of_lt
      · exact (F.toCompleteDVF.mem_valuationSubring_iff _).1 hx
      · simpa [y] using hyval
    have hone_lt :
        F.toCompleteDVF.valuation
            (algebraMap ℚ_[p] K (x * x⁻¹)) < 1 := by
      simpa only [map_mul, F.toCompleteDVF.valuation.map_mul] using hprod
    rw [mul_inv_cancel₀ hx0, map_one,
      F.toCompleteDVF.valuation.map_one] at hone_lt
    exact (lt_irrefl (1 : F.toCompleteDVF.ValueGroup)) hone_lt
  · intro hx
    let z : ℤ_[p] := ⟨x, hx⟩
    simpa [z, p] using
      F.qpadicInt_algebraMap_mem_valuationSubring z
theorem

qpadicDVRValuation_hasExtension

L237 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.qpadicDVRValuation_hasExtension
Documentation

The actual valuation of a mixed-characteristic local field extends the DVR valuation on the canonical Q_p subfield.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem qpadicDVRValuation_hasExtension
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : MixedQPadicContext F := mixedQPadicContext F
    (Examples.Qp.padicDVRValuation F.residueCharacteristic).HasExtension
      F.toCompleteDVF.valuation := by
  let p : ℕ := F.residueCharacteristic
  let : MixedQPadicContext F := mixedQPadicContext F
  refine ⟨(_root_.Valuation.isEquiv_iff_val_le_one).2 ?_⟩
  intro x
  have htarget :
      F.toCompleteDVF.valuation (algebraMap ℚ_[p] K x) ≤ 1 ↔
        ‖x‖ ≤ 1 :=
    (F.toCompleteDVF.mem_valuationSubring_iff _).symm.trans
      (by simpa [p] using
        F.qpadicNumbersAlgebra_mem_valuationSubring_iff x)
  exact
    (padicDVRValuation_le_one_iff_norm_le_one p x).trans
      htarget.symm
instance

mixedQPadicContextValuationExtension

L257 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedQPadicContextValuationExtension
Documentation

The p-adic valuation extends to the valuation on the mixed-characteristic local field.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedQPadicContextValuationExtension
    (F : LocalField.{u, v} K) [CharZero K] [MixedQPadicContext F] :
    (Examples.Qp.padicCompleteDVF F.residueCharacteristic).valuation.HasExtension
      F.toCompleteDVF.valuation
instance

mixedQPadicContextValuationSubringTower

L268 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedQPadicContextValuationSubringTower
Documentation

Equips the target with its canonical IsScalarTower structure, namely IsScalarTower (Examples.Qp.padicCompleteDVF F.residueCharacteristic).valuationSubring F.toCompleteDVF.valuationSubring K.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedQPadicContextValuationSubringTower
    (F : LocalField.{u, v} K) [CharZero K] [MixedQPadicContext F] :
    IsScalarTower
      (Examples.Qp.padicCompleteDVF F.residueCharacteristic).valuationSubring
      F.toCompleteDVF.valuationSubring K
theorem

valuationSubring_isIntegralClosure_over_qpadicIntegers

L280 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_isIntegralClosure_over_qpadicIntegers
Documentation

The integer ring of K is the integral closure of the integer ring of the canonical Q_p. This is the integral-basis input used in the mixed-characteristic field-unit proof of the mixed-characteristic field-unit structure theorem.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension
  (target_valuationSubring_isIntegralClosure_of_finite_separable) in
Lean source · full declaration
theorem valuationSubring_isIntegralClosure_over_qpadicIntegers
    (F : LocalField.{u, v} K) [CharZero K] :
    let p := F.residueCharacteristic
    letI : MixedQPadicContext F := mixedQPadicContext F
    IsIntegralClosure F.toCompleteDVF.valuationSubring
      (Examples.Qp.padicCompleteDVF p).valuationSubring K := by
  let p : ℕ := F.residueCharacteristic
  let : MixedQPadicContext F := mixedQPadicContext F
  let : Algebra.IsSeparable ℚ_[p] K := by infer_instance
  exact
    target_valuationSubring_isIntegralClosure_of_finite_separable
    (Examples.Qp.padicCompleteDVF p) F.toCompleteDVF
theorem

valuationSubring_moduleFinite_over_qpadicIntegers

L297 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_moduleFinite_over_qpadicIntegers
Documentation

Consequently the integer ring of K is finite over the integer ring of the canonical Q_p.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension
  (moduleFinite_target_valuationSubring_of_finite_separable) in
Lean source · full declaration
theorem valuationSubring_moduleFinite_over_qpadicIntegers
    (F : LocalField.{u, v} K) [CharZero K] :
    let p := F.residueCharacteristic
    letI : MixedQPadicContext F := mixedQPadicContext F
    Module.Finite (Examples.Qp.padicCompleteDVF p).valuationSubring
      F.toCompleteDVF.valuationSubring := by
  let p : ℕ := F.residueCharacteristic
  let : MixedQPadicContext F := mixedQPadicContext F
  let : Algebra.IsSeparable ℚ_[p] K := by infer_instance
  exact
    moduleFinite_target_valuationSubring_of_finite_separable
    (Examples.Qp.padicCompleteDVF p) F.toCompleteDVF
theorem

valuationSubring_moduleFree_over_qpadicIntegers

L314 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_moduleFree_over_qpadicIntegers
Documentation

The same integer ring is free over the canonical Q_p integer ring.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension
  (moduleFinite_target_valuationSubring_of_finite_separable
   target_valuationSubring_isIntegralClosure_of_finite_separable) in
Lean source · full declaration
theorem valuationSubring_moduleFree_over_qpadicIntegers
    (F : LocalField.{u, v} K) [CharZero K] :
    let p := F.residueCharacteristic
    letI : MixedQPadicContext F := mixedQPadicContext F
    Module.Free (Examples.Qp.padicCompleteDVF p).valuationSubring
      F.toCompleteDVF.valuationSubring := by
  let p : ℕ := F.residueCharacteristic
  let : MixedQPadicContext F := mixedQPadicContext F
  let : Algebra.IsSeparable ℚ_[p] K := by infer_instance
  let : Module.Finite
      (Examples.Qp.padicCompleteDVF p).valuationSubring
      F.toCompleteDVF.valuationSubring :=
    moduleFinite_target_valuationSubring_of_finite_separable
      (Examples.Qp.padicCompleteDVF p) F.toCompleteDVF
  let : IsIntegralClosure F.toCompleteDVF.valuationSubring
      (Examples.Qp.padicCompleteDVF p).valuationSubring K :=
    target_valuationSubring_isIntegralClosure_of_finite_separable
      (Examples.Qp.padicCompleteDVF p) F.toCompleteDVF
  let : IsFractionRing
      (Examples.Qp.padicCompleteDVF p).valuationSubring ℚ_[p] :=
    ValuationTheory.DiscreteValuationField.ValuedExtension.base_valuationSubring_isFractionRing
      (K := ℚ_[p]) (Examples.Qp.padicCompleteDVF p)
  let : FaithfulSMul
      (Examples.Qp.padicCompleteDVF p).valuationSubring K :=
    FaithfulSMul.of_field_isFractionRing
      (Examples.Qp.padicCompleteDVF p).valuationSubring K ℚ_[p] K
  let : Module.IsTorsionFree
      (Examples.Qp.padicCompleteDVF p).valuationSubring K := inferInstance
  let : Module.IsTorsionFree
      (Examples.Qp.padicCompleteDVF p).valuationSubring
      F.toCompleteDVF.valuationSubring :=
    IsIntegralClosure.isTorsionFree
      (Examples.Qp.padicCompleteDVF p).valuationSubring K
  exact Module.free_of_finite_type_torsion_free'
theorem

valuationSubring_finrank_over_qpadicIntegers

L352 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_finrank_over_qpadicIntegers
Documentation

Integral-basis rank formula over the canonical valuation ring.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension
  (target_valuationSubring_isIntegralClosure_of_finite_separable) in
Lean source · full declaration
theorem valuationSubring_finrank_over_qpadicIntegers
    (F : LocalField.{u, v} K) [CharZero K] :
    let p := F.residueCharacteristic
    letI : MixedQPadicContext F := mixedQPadicContext F
    Module.finrank (Examples.Qp.padicCompleteDVF p).valuationSubring
        F.toCompleteDVF.valuationSubring =
      Module.finrank ℚ_[p] K := by
  let p : ℕ := F.residueCharacteristic
  let : MixedQPadicContext F := mixedQPadicContext F
  let : Algebra.IsSeparable ℚ_[p] K := by infer_instance
  let : IsIntegralClosure F.toCompleteDVF.valuationSubring
      (Examples.Qp.padicCompleteDVF p).valuationSubring K :=
    target_valuationSubring_isIntegralClosure_of_finite_separable
      (Examples.Qp.padicCompleteDVF p) F.toCompleteDVF
  let : IsFractionRing
      (Examples.Qp.padicCompleteDVF p).valuationSubring ℚ_[p] :=
    ValuationTheory.DiscreteValuationField.ValuedExtension.base_valuationSubring_isFractionRing
      (K := ℚ_[p]) (Examples.Qp.padicCompleteDVF p)
  let : FaithfulSMul
      (Examples.Qp.padicCompleteDVF p).valuationSubring K :=
    FaithfulSMul.of_field_isFractionRing
      (Examples.Qp.padicCompleteDVF p).valuationSubring K ℚ_[p] K
  let : Module.IsTorsionFree
      (Examples.Qp.padicCompleteDVF p).valuationSubring K :=
    inferInstance
  exact IsIntegralClosure.rank
    (Examples.Qp.padicCompleteDVF p).valuationSubring ℚ_[p] K
      F.toCompleteDVF.valuationSubring
def

padicIntToValuationSubring

L385 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.padicIntToValuationSubring
Documentation

The canonical ring map Z_p → O_K, obtained by restricting the canonical Q_p → K map proved above.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
def padicIntToValuationSubring
    (F : LocalField.{u, v} K) [CharZero K] :
    ℤ_[F.residueCharacteristic] →+* F.toCompleteDVF.valuationSubring
theorem

padicIntToValuationSubring_coe

L401 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.padicIntToValuationSubring_coe
Documentation

The embedding of ℤ_p into the valuation ring has underlying field value given by the ℚ_p algebra map.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem padicIntToValuationSubring_coe
    (F : LocalField.{u, v} K) [CharZero K]
    (z : ℤ_[F.residueCharacteristic]) :
    letI : MixedQPadicContext F := mixedQPadicContext F
    ((F.padicIntToValuationSubring z : F.toCompleteDVF.valuationSubring) : K) =
      algebraMap ℚ_[F.residueCharacteristic] K
        (z : ℚ_[F.residueCharacteristic]) := by
  rfl
def

padicIntValuationSubringAlgebra

L412 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.padicIntValuationSubringAlgebra
Documentation

The corresponding Z_p-algebra structure on O_K.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
def padicIntValuationSubringAlgebra
    (F : LocalField.{u, v} K) [CharZero K] :
    Algebra ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring
def

padicIntFieldAlgebra

L420 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.padicIntFieldAlgebra
Documentation

The corresponding Z_p-algebra structure on K.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
def padicIntFieldAlgebra
    (F : LocalField.{u, v} K) [CharZero K] :
    Algebra ℤ_[F.residueCharacteristic] K
theorem

padicIntValuationSubring_isScalarTower

L430 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.padicIntValuationSubring_isScalarTower
Documentation

The restricted algebra structures form the expected tower Z_p → O_K → K.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem padicIntValuationSubring_isScalarTower
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : Algebra ℤ_[F.residueCharacteristic]
        F.toCompleteDVF.valuationSubring :=
      F.padicIntValuationSubringAlgebra
    letI : Algebra ℤ_[F.residueCharacteristic] K :=
      F.padicIntFieldAlgebra
    IsScalarTower ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring K := by
  let : Algebra ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring :=
    F.padicIntValuationSubringAlgebra
  let : Algebra ℤ_[F.residueCharacteristic] K :=
    F.padicIntFieldAlgebra
  exact IsScalarTower.of_algebraMap_eq (by intro z; rfl)
class

MixedIntegralAlgebraContext

L449 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.MixedIntegralAlgebraContext
Documentation

The coherent canonical Z_p → O_K → K algebra model. The bundle retains its canonical Q_p context and installs both integral algebra structures and their scalar towers.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
class MixedIntegralAlgebraContext (F : LocalField.{u, v} K) : Prop where
  /-- The canonical `Q_p` scalar context underlying the integral algebra structure. -/
  qpadic : MixedQPadicContext F
theorem

mixedIntegralAlgebraContext

L454 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralAlgebraContext
Documentation

The canonical integral algebra context attached to F.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
theorem mixedIntegralAlgebraContext (F : LocalField.{u, v} K) :
    MixedIntegralAlgebraContext F
instance

mixedIntegralAlgebraContextQPadic

L462 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralAlgebraContextQPadic
Documentation

Equips the target with its canonical MixedQPadicContext structure, namely MixedQPadicContext F.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedIntegralAlgebraContextQPadic
    (F : LocalField.{u, v} K) [ctx : MixedIntegralAlgebraContext F] :
    MixedQPadicContext F
instance

mixedIntegralAlgebraContextValuationSubringAlgebra

L471 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralAlgebraContextValuationSubringAlgebra
Documentation

Equips the target with its canonical Algebra structure, namely Algebra ℤ_[F.residueCharacteristic] F.toCompleteDVF.valuationSubring.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedIntegralAlgebraContextValuationSubringAlgebra
    (F : LocalField.{u, v} K) [CharZero K]
    [MixedIntegralAlgebraContext F] :
    Algebra ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring
instance

mixedIntegralAlgebraContextFieldAlgebra

L482 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralAlgebraContextFieldAlgebra
Documentation

Equips the target with its canonical Algebra structure, namely Algebra ℤ_[F.residueCharacteristic] K.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedIntegralAlgebraContextFieldAlgebra
    (F : LocalField.{u, v} K) [CharZero K]
    [MixedIntegralAlgebraContext F] :
    Algebra ℤ_[F.residueCharacteristic] K
instance

mixedIntegralAlgebraContextQPadicTower

L492 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralAlgebraContextQPadicTower
Documentation

Equips the target with its canonical IsScalarTower structure, namely IsScalarTower ℤ_[F.residueCharacteristic] ℚ_[F.residueCharacteristic] K.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedIntegralAlgebraContextQPadicTower
    (F : LocalField.{u, v} K) [CharZero K]
    [MixedIntegralAlgebraContext F] :
    IsScalarTower ℤ_[F.residueCharacteristic]
      ℚ_[F.residueCharacteristic] K
instance

mixedIntegralAlgebraContextValuationSubringTower

L503 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralAlgebraContextValuationSubringTower
Documentation

Equips the target with its canonical IsScalarTower structure, namely IsScalarTower ℤ_[F.residueCharacteristic] F.toCompleteDVF.valuationSubring K.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedIntegralAlgebraContextValuationSubringTower
    (F : LocalField.{u, v} K) [CharZero K]
    [MixedIntegralAlgebraContext F] :
    IsScalarTower ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring K
theorem

valuationSubring_isIntegralClosure_over_padicInt

L514 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuationSubring_isIntegralClosure_over_padicInt
Documentation

canonical integral-closure form: O_K is the integral closure of Z_p in K for the canonical Q_p-algebra structure.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension
  (target_valuationSubring_isIntegralClosure_of_finite_separable) in
Lean source · full declaration
theorem valuationSubring_isIntegralClosure_over_padicInt
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : MixedIntegralAlgebraContext F :=
      mixedIntegralAlgebraContext F
    IsIntegralClosure F.toCompleteDVF.valuationSubring
      ℤ_[F.residueCharacteristic] K := by
  let p : ℕ := F.residueCharacteristic
  let : MixedIntegralAlgebraContext F :=
    mixedIntegralAlgebraContext F
  let : Algebra.IsSeparable ℚ_[p] K := by infer_instance
  let hclosure : IsIntegralClosure F.toCompleteDVF.valuationSubring
      (Examples.Qp.padicCompleteDVF p).valuationSubring K :=
    target_valuationSubring_isIntegralClosure_of_finite_separable
      (Examples.Qp.padicCompleteDVF p) F.toCompleteDVF
  let e : ℤ_[p] ≃+* (Examples.Qp.padicCompleteDVF p).valuationSubring :=
    Examples.Qp.padicIntEquivValuationSubring p
  have hcompat :
      (algebraMap (Examples.Qp.padicCompleteDVF p).valuationSubring K).comp
          e.toRingHom =
        algebraMap ℤ_[p] K := by
    ext z
    rfl
  refine
    { algebraMap_injective := by
        intro a b hab
        exact Subtype.ext hab
      isIntegral_iff := ?_ }
  intro x
  exact (e.isIntegral_iff hcompat x).trans hclosure.isIntegral_iff
theorem

mixed_valuationSubring_moduleFinite

L547 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_valuationSubring_moduleFinite
Documentation

The mixed-characteristic field-unit structure theorem, integral-basis finiteness: O_K is a finite Z_p-module, with no separately assumed module structure.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem mixed_valuationSubring_moduleFinite
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : MixedIntegralAlgebraContext F :=
      mixedIntegralAlgebraContext F
    Module.Finite ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring := by
  let p : ℕ := F.residueCharacteristic
  let : MixedIntegralAlgebraContext F :=
    mixedIntegralAlgebraContext F
  let : IsIntegralClosure F.toCompleteDVF.valuationSubring ℤ_[p] K :=
    F.valuationSubring_isIntegralClosure_over_padicInt
  exact IsIntegralClosure.finite ℤ_[p] ℚ_[p] K
    F.toCompleteDVF.valuationSubring
theorem

mixed_valuationSubring_moduleFree

L562 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_valuationSubring_moduleFree
Documentation

The mixed-characteristic field-unit structure theorem, integral-basis freeness.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem mixed_valuationSubring_moduleFree
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : MixedIntegralAlgebraContext F :=
      mixedIntegralAlgebraContext F
    Module.Free ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring := by
  let p : ℕ := F.residueCharacteristic
  let : MixedIntegralAlgebraContext F :=
    mixedIntegralAlgebraContext F
  let : IsIntegralClosure F.toCompleteDVF.valuationSubring ℤ_[p] K :=
    F.valuationSubring_isIntegralClosure_over_padicInt
  let : FaithfulSMul ℤ_[p] K :=
    FaithfulSMul.of_field_isFractionRing ℤ_[p] K ℚ_[p] K
  let : Module.IsTorsionFree ℤ_[p] K := inferInstance
  exact IsIntegralClosure.module_free
    ℤ_[p] ℚ_[p] K F.toCompleteDVF.valuationSubring
theorem

mixed_valuationSubring_finrank

L580 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_valuationSubring_finrank
Documentation

The mixed-characteristic field-unit structure theorem, exact integral-basis rank.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem mixed_valuationSubring_finrank
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : MixedIntegralAlgebraContext F :=
      mixedIntegralAlgebraContext F
    Module.finrank ℤ_[F.residueCharacteristic]
        F.toCompleteDVF.valuationSubring =
      Module.finrank ℚ_[F.residueCharacteristic] K := by
  let p : ℕ := F.residueCharacteristic
  let : MixedIntegralAlgebraContext F :=
    mixedIntegralAlgebraContext F
  let : IsIntegralClosure F.toCompleteDVF.valuationSubring ℤ_[p] K :=
    F.valuationSubring_isIntegralClosure_over_padicInt
  let : FaithfulSMul ℤ_[p] K :=
    FaithfulSMul.of_field_isFractionRing ℤ_[p] K ℚ_[p] K
  let : Module.IsTorsionFree ℤ_[p] K := inferInstance
  exact IsIntegralClosure.rank
    ℤ_[p] ℚ_[p] K F.toCompleteDVF.valuationSubring
class

MixedIntegralLatticeContext

L600 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.MixedIntegralLatticeContext
Documentation

The finite free canonical Z_p lattice model of O_K. It retains the integral algebra context and installs the finite and free module instances.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
class MixedIntegralLatticeContext (F : LocalField.{u, v} K) : Prop where
  /-- The canonical `Z_p → O_K → K` algebra context underlying the lattice. -/
  integralAlgebra : MixedIntegralAlgebraContext F
theorem

mixedIntegralLatticeContext

L605 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralLatticeContext
Documentation

The canonical finite free integral-lattice context attached to F.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
theorem mixedIntegralLatticeContext (F : LocalField.{u, v} K) :
    MixedIntegralLatticeContext F
instance

mixedIntegralLatticeContextAlgebra

L610 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralLatticeContextAlgebra
Documentation

The valued field carries the integral algebra context MixedIntegralAlgebraContext F.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedIntegralLatticeContextAlgebra
    (F : LocalField.{u, v} K) [ctx : MixedIntegralLatticeContext F] :
    MixedIntegralAlgebraContext F
instance

mixedIntegralLatticeContextModuleFinite

L619 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralLatticeContextModuleFinite
Documentation

Equips the target with its canonical Module.Finite structure, namely Module.Finite ℤ_[F.residueCharacteristic] F.toCompleteDVF.valuationSubring.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedIntegralLatticeContextModuleFinite
    (F : LocalField.{u, v} K) [CharZero K]
    [MixedIntegralLatticeContext F] :
    Module.Finite ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring
instance

mixedIntegralLatticeContextModuleFree

L630 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedIntegralLatticeContextModuleFree
Documentation

Equips the target with its canonical Module.Free structure, namely Module.Free ℤ_[F.residueCharacteristic] F.toCompleteDVF.valuationSubring.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedIntegralLatticeContextModuleFree
    (F : LocalField.{u, v} K) [CharZero K]
    [MixedIntegralLatticeContext F] :
    Module.Free ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring
def

mixed_integralBasis

L638 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_integralBasis
Documentation

A concrete integral basis indexed by the field degree d = [K:Q_p].

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
def mixed_integralBasis
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : MixedIntegralLatticeContext F :=
      mixedIntegralLatticeContext F
    Basis (Fin (Module.finrank ℚ_[F.residueCharacteristic] K))
      ℤ_[F.residueCharacteristic] F.toCompleteDVF.valuationSubring := by
  let p : ℕ := F.residueCharacteristic
  letI : MixedIntegralLatticeContext F :=
    mixedIntegralLatticeContext F
  exact Module.finBasisOfFinrankEq ℤ_[p] F.toCompleteDVF.valuationSubring
    F.mixed_valuationSubring_finrank
def

mixed_valuationSubringLinearEquivPi

L652 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_valuationSubringLinearEquivPi
Documentation

Coordinate form of the integral basis used in the free factor of the mixed-characteristic field-unit structure theorem.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
def mixed_valuationSubringLinearEquivPi
    (F : LocalField.{u, v} K) [CharZero K] :
    letI : MixedIntegralLatticeContext F :=
      mixedIntegralLatticeContext F
    F.toCompleteDVF.valuationSubring ≃ₗ[ℤ_[F.residueCharacteristic]]
      (Fin (Module.finrank ℚ_[F.residueCharacteristic] K) →
        ℤ_[F.residueCharacteristic]) := by
  let p : ℕ := F.residueCharacteristic
  letI : MixedIntegralLatticeContext F :=
    mixedIntegralLatticeContext F
  exact F.mixed_integralBasis.equivFun
theorem

mixed_maximalIdealPow_moduleFinite

L665 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_maximalIdealPow_moduleFinite
Documentation

Every power of the maximal ideal is a finite Z_p-module.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem mixed_maximalIdealPow_moduleFinite
    (F : LocalField.{u, v} K) [CharZero K] (n : ℕ) :
    letI : MixedIntegralLatticeContext F :=
      mixedIntegralLatticeContext F
    Module.Finite ℤ_[F.residueCharacteristic]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) := by
  let p : ℕ := F.residueCharacteristic
  let : MixedIntegralLatticeContext F :=
    mixedIntegralLatticeContext F
  exact Module.Finite.of_injective
    (((F.toCompleteDVF.maximalIdeal ^ n :
      Ideal F.toCompleteDVF.valuationSubring).subtype).restrictScalars ℤ_[p])
    Subtype.val_injective
theorem

mixed_maximalIdealPow_moduleFree

L681 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_maximalIdealPow_moduleFree
Documentation

Every maximal-ideal power is free over Z_p.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem mixed_maximalIdealPow_moduleFree
    (F : LocalField.{u, v} K) [CharZero K] (n : ℕ) :
    letI : MixedIntegralLatticeContext F :=
      mixedIntegralLatticeContext F
    Module.Free ℤ_[F.residueCharacteristic]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) := by
  let p : ℕ := F.residueCharacteristic
  let : MixedIntegralLatticeContext F :=
    mixedIntegralLatticeContext F
  let : Module.Finite ℤ_[p]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) :=
    F.mixed_maximalIdealPow_moduleFinite n
  let : Module.IsTorsionFree ℤ_[p] F.toCompleteDVF.valuationSubring :=
    inferInstance
  let : Module.IsTorsionFree ℤ_[p]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) := by
    refine Module.IsTorsionFree.of_smul_eq_zero ?_
    intro r x hrx
    have hrx' : r • (x : F.toCompleteDVF.valuationSubring) = 0 := by
      simpa using congrArg Subtype.val hrx
    rcases (smul_eq_zero.mp hrx') with hr | hx
    · exact Or.inl hr
    · exact Or.inr (Subtype.ext hx)
  exact Module.free_of_finite_type_torsion_free'
class

MixedMaximalIdealPowContext

L712 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.MixedMaximalIdealPowContext
Documentation

The finite free Z_p model of one maximal-ideal power. The ambient integral-lattice context is an explicit dependency, while the indexed bundle owns the finite and free witnesses for the selected power.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
class MixedMaximalIdealPowContext
    (F : LocalField.{u, v} K) [CharZero K] (n : ℕ)
    [MixedIntegralLatticeContext F] : Prop where
  /-- The `n`th maximal-ideal power is finitely generated over `Z_p`. -/
  moduleFinite : Module.Finite ℤ_[F.residueCharacteristic]
    ((F.toCompleteDVF.maximalIdeal ^ n :
      Ideal F.toCompleteDVF.valuationSubring))
  /-- The `n`th maximal-ideal power is free over `Z_p`. -/
  moduleFree : Module.Free ℤ_[F.residueCharacteristic]
    ((F.toCompleteDVF.maximalIdeal ^ n :
      Ideal F.toCompleteDVF.valuationSubring))
theorem

mixedMaximalIdealPowContext

L725 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedMaximalIdealPowContext
Documentation

The canonical maximal-ideal-power context.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem mixedMaximalIdealPowContext
    (F : LocalField.{u, v} K) [CharZero K] (n : ℕ) :
    letI : MixedIntegralLatticeContext F :=
      mixedIntegralLatticeContext F
    MixedMaximalIdealPowContext F n := by
  let : MixedIntegralLatticeContext F :=
    mixedIntegralLatticeContext F
  exact
    ⟨F.mixed_maximalIdealPow_moduleFinite n,
      F.mixed_maximalIdealPow_moduleFree n⟩
instance

mixedMaximalIdealPowContextModuleFinite

L741 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedMaximalIdealPowContextModuleFinite
Documentation

Equips the target with its canonical Module.Finite structure, namely Module.Finite ℤ_[F.residueCharacteristic] ((F.toCompleteDVF.maximalIdeal ^ n : Ideal F.toCompleteDVF.valuationSubring)).

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedMaximalIdealPowContextModuleFinite
    (F : LocalField.{u, v} K) [CharZero K] (n : ℕ)
    [MixedIntegralLatticeContext F]
    [ctx : MixedMaximalIdealPowContext F n] :
    Module.Finite ℤ_[F.residueCharacteristic]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring))
instance

mixedMaximalIdealPowContextModuleFree

L755 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedMaximalIdealPowContextModuleFree
Documentation

Equips the target with its canonical Module.Free structure, namely Module.Free ℤ_[F.residueCharacteristic] ((F.toCompleteDVF.maximalIdeal ^ n : Ideal F.toCompleteDVF.valuationSubring)).

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedMaximalIdealPowContextModuleFree
    (F : LocalField.{u, v} K) [CharZero K] (n : ℕ)
    [MixedIntegralLatticeContext F]
    [ctx : MixedMaximalIdealPowContext F n] :
    Module.Free ℤ_[F.residueCharacteristic]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring))
theorem

mixed_maximalIdealPow_finrank

L766 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_maximalIdealPow_finrank
Documentation

A nonzero maximal-ideal power has the same Z_p rank as O_K, hence rank exactly [K:Q_p].

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem mixed_maximalIdealPow_finrank
    (F : LocalField.{u, v} K) [CharZero K] (n : ℕ) :
    letI : MixedIntegralLatticeContext F :=
      mixedIntegralLatticeContext F
    letI : MixedMaximalIdealPowContext F n :=
      mixedMaximalIdealPowContext F n
    Module.finrank ℤ_[F.residueCharacteristic]
        ((F.toCompleteDVF.maximalIdeal ^ n :
          Ideal F.toCompleteDVF.valuationSubring)) =
      Module.finrank ℚ_[F.residueCharacteristic] K := by
  let p : ℕ := F.residueCharacteristic
  let : MixedIntegralLatticeContext F :=
    mixedIntegralLatticeContext F
  let : MixedMaximalIdealPowContext F n :=
    mixedMaximalIdealPowContext F n
  calc
    Module.finrank ℤ_[p]
        ((F.toCompleteDVF.maximalIdeal ^ n :
          Ideal F.toCompleteDVF.valuationSubring)) =
        Module.finrank ℤ_[p] F.toCompleteDVF.valuationSubring := by
          exact Ideal.finrank_eq_finrank
            F.mixed_integralBasis
            (F.toCompleteDVF.maximalIdeal ^ n)
            (pow_ne_zero n F.toCompleteDVF.maximalIdeal_ne_bot)
    _ = Module.finrank ℚ_[p] K :=
      F.mixed_valuationSubring_finrank
def

mixed_maximalIdealPowLinearEquivPi

L795 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_maximalIdealPowLinearEquivPi
Documentation

Coordinate form for a deep additive ideal, the source side of the deep exponential–logarithm equivalence.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
def mixed_maximalIdealPowLinearEquivPi
    (F : LocalField.{u, v} K) [CharZero K] (n : ℕ) :
    letI : MixedIntegralLatticeContext F :=
      mixedIntegralLatticeContext F
    letI : MixedMaximalIdealPowContext F n :=
      mixedMaximalIdealPowContext F n
    ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring))
      ≃ₗ[ℤ_[F.residueCharacteristic]]
        (Fin (Module.finrank ℚ_[F.residueCharacteristic] K) →
          ℤ_[F.residueCharacteristic]) := by
  let p : ℕ := F.residueCharacteristic
  letI : MixedIntegralLatticeContext F :=
    mixedIntegralLatticeContext F
  letI : MixedMaximalIdealPowContext F n :=
    mixedMaximalIdealPowContext F n
  exact
    (Module.finBasisOfFinrankEq ℤ_[p]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring))
      (F.mixed_maximalIdealPow_finrank n)).equivFun
def

higherPrincipalUnitToFirst

L820 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitToFirst
Documentation

Inclusion of a higher principal-unit group into U^1.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
def higherPrincipalUnitToFirst
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r) :
    CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r →*
      CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1 where
  toFun x := ⟨(x : F.toCompleteDVF.valuationSubringˣ),
    CompleteDVF.higherPrincipalUnitGroup.antitone F.toCompleteDVF hr x.property⟩
  map_one' := rfl
  map_mul' _ _ := rfl
theorem

higherPrincipalUnitToFirst_injective

L830 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitToFirst_injective
Documentation

The specified map is injective: Function.Injective (F.higherPrincipalUnitToFirst hr).

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
theorem higherPrincipalUnitToFirst_injective
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r) :
    Function.Injective (F.higherPrincipalUnitToFirst hr)
def

higherPrincipalUnitAddToFirst

L840 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitAddToFirst
Documentation

Additive form of the inclusion U^r → U^1.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
def higherPrincipalUnitAddToFirst
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r) :
    Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r) →+
      Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1)
theorem

higherPrincipalUnitAddToFirst_injective

L847 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitAddToFirst_injective
Documentation

The specified map is injective: Function.Injective (F.higherPrincipalUnitAddToFirst hr).

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
theorem higherPrincipalUnitAddToFirst_injective
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r) :
    Function.Injective (F.higherPrincipalUnitAddToFirst hr)
def

higherPrincipalUnitPadicSMul

L858 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitPadicSMul
Documentation

Restrict the canonical p-adic scalar action on U^1 to the stable subgroup U^r.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
def higherPrincipalUnitPadicSMul
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r) :
    SMul ℤ_[F.residueCharacteristic]
      (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) where
  smul a x := by
    let x1 : CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1 :=
      F.higherPrincipalUnitToFirst hr (Additive.toMul x)
    let y1 : CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1 :=
      Additive.toMul (a • Additive.ofMul x1)
    exact Additive.ofMul ⟨(y1 : F.toCompleteDVF.valuationSubringˣ),
      CompleteDVF.higherPrincipalUnitGroup.principalUnitPadic_smul_mem_higher
        F hr a x1 (by simp [x1, higherPrincipalUnitToFirst])⟩
theorem

higherPrincipalUnitAddToFirst_smul

L873 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitAddToFirst_smul
Documentation

The additive inclusion U^r → U^1 commutes with the canonical ℤ_p-scalar action.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem higherPrincipalUnitAddToFirst_smul
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r)
    (a : ℤ_[F.residueCharacteristic])
    (x : Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) :
    letI : SMul ℤ_[F.residueCharacteristic]
        (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) :=
      F.higherPrincipalUnitPadicSMul hr
    F.higherPrincipalUnitAddToFirst hr (a • x) =
      a • F.higherPrincipalUnitAddToFirst hr x := by
  rfl
def

higherPrincipalUnitPadicModule

L886 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitPadicModule
Documentation

The stable subgroup U^r with its canonical Z_p-module structure.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
def higherPrincipalUnitPadicModule
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r) :
    Module ℤ_[F.residueCharacteristic]
      (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r))
theorem

higherPrincipalUnitPadic_natCast_smul

L916 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitPadic_natCast_smul
Documentation

Natural scalars on U^r are the ordinary group powers.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem higherPrincipalUnitPadic_natCast_smul
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r)
    (m : ℕ) (x : CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r) :
    letI : Module ℤ_[F.residueCharacteristic]
        (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) :=
      F.higherPrincipalUnitPadicModule hr
    (m : ℤ_[F.residueCharacteristic]) • Additive.ofMul x =
      Additive.ofMul (x ^ m) := by
  let : Module ℤ_[F.residueCharacteristic]
      (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) :=
    F.higherPrincipalUnitPadicModule hr
  apply F.higherPrincipalUnitAddToFirst_injective hr
  rw [F.higherPrincipalUnitAddToFirst_smul]
  exact
    CompleteDVF.higherPrincipalUnitGroup.principalUnitPadic_natCast_smul
      F m (F.higherPrincipalUnitToFirst hr x)
def

higherPrincipalUnitLinearToFirst

L935 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitLinearToFirst
Documentation

The inclusion U^r \hookrightarrow U^1 is linear for the canonical Z_p-actions.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
def higherPrincipalUnitLinearToFirst
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r) :
    letI : Module ℤ_[F.residueCharacteristic]
        (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) :=
      F.higherPrincipalUnitPadicModule hr
    Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r) →ₗ[
        ℤ_[F.residueCharacteristic]]
      Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1) := by
  letI : Module ℤ_[F.residueCharacteristic]
      (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) :=
    F.higherPrincipalUnitPadicModule hr
  exact
    { F.higherPrincipalUnitAddToFirst hr with
      map_smul' := fun a x => F.higherPrincipalUnitAddToFirst_smul hr a x }
def

higherPrincipalUnitPadicSubmodule

L951 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitPadicSubmodule
Documentation

The deep principal units, regarded as a Z_p-submodule of U^1.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
def higherPrincipalUnitPadicSubmodule
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r) :
    Submodule ℤ_[F.residueCharacteristic]
      (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1)) where
  carrier := {x | ((Additive.toMul x :
      CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1) :
        F.toCompleteDVF.valuationSubringˣ) ∈
      CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r}
  zero_mem' := by
    change (1 : F.toCompleteDVF.valuationSubringˣ) ∈
      CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r
    exact Subgroup.one_mem _
  add_mem' {x y} hx hy := by
    change (((Additive.toMul x :
        CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1) :
          F.toCompleteDVF.valuationSubringˣ) *
      ((Additive.toMul y :
        CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1) :
          F.toCompleteDVF.valuationSubringˣ)) ∈
        CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r
    exact Subgroup.mul_mem _ hx hy
  smul_mem' a x hx :=
    CompleteDVF.higherPrincipalUnitGroup.principalUnitPadic_smul_mem_higher
      F hr a (Additive.toMul x) hx
def

higherPrincipalUnitLinearEquivPadicSubmodule

L979 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitLinearEquivPadicSubmodule
Documentation

A higher principal-unit group is linearly equivalent to its image in U^1. This is the submodule used in the finite-index argument in the proof of the mixed-characteristic field-unit structure theorem.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
def higherPrincipalUnitLinearEquivPadicSubmodule
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r) :
    letI : Module ℤ_[F.residueCharacteristic]
        (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) :=
      F.higherPrincipalUnitPadicModule hr
    Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r) ≃ₗ[
        ℤ_[F.residueCharacteristic]] F.higherPrincipalUnitPadicSubmodule hr := by
  letI : Module ℤ_[F.residueCharacteristic]
      (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) :=
    F.higherPrincipalUnitPadicModule hr
  exact
    { toFun := fun x => ⟨F.higherPrincipalUnitAddToFirst hr x,
        (Additive.toMul x).property⟩
      invFun := fun x => Additive.ofMul
        ⟨((Additive.toMul x.1 :
          CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1) :
            F.toCompleteDVF.valuationSubringˣ), x.2⟩
      left_inv := fun x => by
        apply Additive.toMul.injective
        apply Subtype.ext
        rfl
      right_inv := fun x => by
        apply Subtype.ext
        apply Additive.toMul.injective
        apply Subtype.ext
        rfl
      map_add' := fun x y => by
        apply Subtype.ext
        exact map_add (F.higherPrincipalUnitAddToFirst hr) x y
      map_smul' := fun a x => by
        apply Subtype.ext
        exact F.higherPrincipalUnitAddToFirst_smul hr a x }
def

principalUnitQuotientProjectionLinear

L1014 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.principalUnitQuotientProjectionLinear
Documentation

Projection of U^1 to the wrapped quotient U^1/U^(n+1), as a Z_p-linear map.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
def principalUnitQuotientProjectionLinear
    (F : LocalField.{u, v} K) (n : ℕ) :
    Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1) →ₗ[
        ℤ_[F.residueCharacteristic]]
      CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient
        F.toCompleteDVF n
def

principalUnitSuccPadicSubmodule

L1026 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.principalUnitSuccPadicSubmodule
Documentation

The canonically indexed image of U^(n+1) inside U^1.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
def principalUnitSuccPadicSubmodule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Submodule ℤ_[F.residueCharacteristic]
      (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) 1))
theorem

principalUnitQuotientProjectionLinear_ker

L1035 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.principalUnitQuotientProjectionLinear_ker
Documentation

The kernel of the finite projection is exactly the image of U^(n+1) \hookrightarrow U^1.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
theorem principalUnitQuotientProjectionLinear_ker
    (F : LocalField.{u, v} K) (n : ℕ) :
    LinearMap.ker (F.principalUnitQuotientProjectionLinear n) =
      F.principalUnitSuccPadicSubmodule n
theorem

discretePrincipalUnitQuotient_moduleIsTorsion

L1092 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.discretePrincipalUnitQuotient_moduleIsTorsion
Documentation

Every wrapped local-field coordinate U^1/U^(n+1) is a torsion Z_p-module.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (discretePrincipalUnitQuotient_nsmul_residueCharacteristic_pow_eq_zero) in
Lean source · statement
theorem discretePrincipalUnitQuotient_moduleIsTorsion
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module.IsTorsion ℤ_[F.residueCharacteristic]
      (CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient
        F.toCompleteDVF n)
theorem

discretePrincipalUnitQuotient_isPGroup

L1117 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.discretePrincipalUnitQuotient_isPGroup
Documentation

The same finite coordinate is a p-group, with its exact cardinality coming from the principal-unit filtration.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (card_discretePrincipalUnitQuotient_eq_residueCharacteristic_pow) in
Lean source · statement
theorem discretePrincipalUnitQuotient_isPGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsPGroup F.residueCharacteristic
      (Multiplicative
        (CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient
          F.toCompleteDVF n))
theorem

higherPrincipalUnitPadicSubmodule_moduleFinite

L1141 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.higherPrincipalUnitPadicSubmodule_moduleFinite
Documentation

Finite generation passes from a higher principal-unit group to its image as a submodule of U^1.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
theorem higherPrincipalUnitPadicSubmodule_moduleFinite
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r)
    (hfinite : @Module.Finite ℤ_[F.residueCharacteristic]
      (Additive (CompleteDVF.higherPrincipalUnitGroup (F.toCompleteDVF) r)) _ _
      (F.higherPrincipalUnitPadicModule hr)) :
    Module.Finite ℤ_[F.residueCharacteristic]
      (F.higherPrincipalUnitPadicSubmodule hr)

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