NYLL
Module

UnitDecomposition.lean

Nyll.ValuedFieldTheory.LocalField.Padic.UnitDecomposition
24 declarations indexed from sourceView source ↗

Module documentation

Unit decomposition of the p-adic integers

This file constructs the reusable topological decomposition of ℤ_[p]ˣ into its finite factor and its principal p-adic factor.

Imports7
Imported by2

Declarations

theorem

padicDVRValuation_surjective

L36 ↗
LocalFieldTheory.Padic.padicDVRValuation_surjective
Source context 8 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
theorem padicDVRValuation_surjective
    (p : ℕ) [Fact p.Prime] :
    Function.Surjective (padicDVRValuation p)
instance

padicDVRResidueFinite

L56 ↗
LocalFieldTheory.Padic.padicDVRResidueFinite
Source context 8 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring)
def

padicResidueEquivZMod

L66 ↗
LocalFieldTheory.Padic.padicResidueEquivZMod
Documentation

The residue field of the valuation-theoretic presentation of ℚ_[p] is canonically ZMod p.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
def padicResidueEquivZMod
    (p : ℕ) [Fact p.Prime] :
    (LocalField.ofWithZeroValuation
      (padicDVRValuation p)).residueField ≃+* ZMod p
theorem

padic_residueCharacteristic_eq

L74 ↗
LocalFieldTheory.Padic.padic_residueCharacteristic_eq
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
theorem padic_residueCharacteristic_eq
    (p : ℕ) [Fact p.Prime] :
    (LocalField.ofWithZeroValuation
      (padicDVRValuation p)).residueCharacteristic = p
theorem

padicDVRValued_uniformSpace_eq_standard

L90 ↗
LocalFieldTheory.Padic.padicDVRValued_uniformSpace_eq_standard
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
theorem padicDVRValued_uniformSpace_eq_standard
    (p : ℕ) [Fact p.Prime] :
    (Valued.mk' (padicDVRValuation p)).toUniformSpace =
      (inferInstance : UniformSpace ℚ_[p])
theorem

padic_finrank_eq_one

L122 ↗
LocalFieldTheory.Padic.padic_finrank_eq_one
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · full declaration
theorem padic_finrank_eq_one
    (p : ℕ) [Fact p.Prime] :
    let v := padicDVRValuation p
    let F := LocalField.ofWithZeroValuation v
    letI : LocalField.MixedWithZeroValuationContext v :=
      LocalField.mixedWithZeroValuationContext v
    Module.finrank ℚ_[F.residueCharacteristic] ℚ_[p] = 1 := by
  let v := padicDVRValuation p
  let F := LocalField.ofWithZeroValuation v
  let : LocalField.MixedWithZeroValuationContext v :=
    LocalField.mixedWithZeroValuationContext v
  dsimp only
  apply Algebra.finrank_eq_one_iff_bijective_algebraMap.mpr
  refine ⟨RingHom.injective _, ?_⟩
  let direct : Valued ℚ_[p] (WithZero (Multiplicative ℤ)) :=
    Valued.mk' v
  let restricted : Valued ℚ_[p] F.mrangeValueGroup :=
    CompleteDVF.mrangeRestrictValued F.toCompleteDVF
  have hrestricted :
      @IsUniformInducing
        ℚ_[F.residueCharacteristic] ℚ_[p]
        inferInstance restricted.toUniformSpace
        (algebraMap ℚ_[F.residueCharacteristic] ℚ_[p]) := by
    let : Valued ℚ_[p] F.mrangeValueGroup := restricted
    change IsUniformInducing
      (fun x : ℚ_[F.residueCharacteristic] =>
        ((F.qpadicNumbersEquivQpadicClosureSubfield x :
          F.qpadicClosureSubfield) : ℚ_[p]))
    exact isUniformEmbedding_subtype_val.isUniformInducing.comp
      F.qpadicNumbersToQpadicClosureSubfield_isUniformInducing
  have huniform :
      direct.toUniformSpace = restricted.toUniformSpace := by
    change
      (Valued.mk' v).toUniformSpace =
        (CompleteDVF.mrangeRestrictValued
          (WithZeroValuationTopology.completeDVF v)).toUniformSpace
    exact WithZeroValuationTopology.valuedMk_uniformSpace_eq_mrangeRestrict v
  have hUR :
      (PseudoMetricSpace.toUniformSpace : UniformSpace ℚ_[p]) =
        restricted.toUniformSpace :=
    (padicDVRValued_uniformSpace_eq_standard p).symm.trans huniform
  have hclosed :
      @IsClosed ℚ_[p] restricted.toTopologicalSpace
        (Set.range
          (algebraMap ℚ_[F.residueCharacteristic] ℚ_[p])) := by
    have hembedding :
        @IsUniformEmbedding
          ℚ_[F.residueCharacteristic] ℚ_[p]
          inferInstance restricted.toUniformSpace
          (algebraMap ℚ_[F.residueCharacteristic] ℚ_[p]) :=
      ⟨hrestricted, RingHom.injective _⟩
    exact hembedding.isClosedEmbedding.isClosed_range
  have hratDense :
      @DenseRange ℚ_[p] restricted.toTopologicalSpace
        ℚ ((↑) : ℚ → ℚ_[p]) := by
    have htop :
        (PseudoMetricSpace.toUniformSpace :
          UniformSpace ℚ_[p]).toTopologicalSpace =
            restricted.toTopologicalSpace :=
      congrArg (fun U : UniformSpace ℚ_[p] => U.toTopologicalSpace) hUR
    let P := fun T : TopologicalSpace ℚ_[p] =>
      @DenseRange ℚ_[p] T ℚ ((↑) : ℚ → ℚ_[p])
    exact (congrArg P htop).mp (Padic.denseRange_ratCast p)
  have hdense :
      @DenseRange ℚ_[p] restricted.toTopologicalSpace
        ℚ_[F.residueCharacteristic]
        (algebraMap ℚ_[F.residueCharacteristic] ℚ_[p]) := by
    apply DenseRange.of_comp
      (g := ((↑) : ℚ → ℚ_[F.residueCharacteristic]))
    have hcomp :
        (algebraMap ℚ_[F.residueCharacteristic] ℚ_[p]) ∘
            ((↑) : ℚ → ℚ_[F.residueCharacteristic]) =
          ((↑) : ℚ → ℚ_[p]) := by
      funext q
      simpa only [Function.comp_apply] using
        (map_ratCast
          (algebraMap ℚ_[F.residueCharacteristic] ℚ_[p]) q)
    rw [hcomp]
    exact hratDense
  rw [← Set.range_eq_univ]
  exact hclosed.closure_eq.symm.trans hdense.closure_range
def

padicFreeContinuousAddEquivOfEq

L206 ↗
LocalFieldTheory.Padic.padicFreeContinuousAddEquivOfEq
Documentation

After identifying the residue characteristic with p and the relative degree with one, the free additive factor is canonically ℤ_[p].

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
def padicFreeContinuousAddEquivOfEq
    (p q d : ℕ) [Fact p.Prime] [Fact q.Prime]
    (hq : q = p) (hd : d = 1) :
    (Fin d → ℤ_[q]) ≃ₜ+ ℤ_[p]
def

padicFreeContinuousAddEquiv

L219 ↗
LocalFieldTheory.Padic.padicFreeContinuousAddEquiv
Documentation

The free additive factor in the mixed-characteristic structure theorem for ℚ_[p] is continuously equivalent to ℤ_[p].

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · full declaration
def padicFreeContinuousAddEquiv
    (p : ℕ) [Fact p.Prime] :
    let v := padicDVRValuation p
    let F := LocalField.ofWithZeroValuation v
    letI : LocalField.MixedWithZeroValuationContext v :=
      LocalField.mixedWithZeroValuationContext v
    let d := Module.finrank ℚ_[F.residueCharacteristic] ℚ_[p]
    (Fin d → ℤ_[F.residueCharacteristic]) ≃ₜ+ ℤ_[p] := by
  let v := padicDVRValuation p
  let F := LocalField.ofWithZeroValuation v
  letI : LocalField.MixedWithZeroValuationContext v :=
    LocalField.mixedWithZeroValuationContext v
  let q := F.residueCharacteristic
  let d := Module.finrank ℚ_[q] ℚ_[p]
  change (Fin d → ℤ_[q]) ≃ₜ+ ℤ_[p]
  have hq : q = p := by
    simpa [q, F, v] using padic_residueCharacteristic_eq p
  have hd : d = 1 := by
    simpa [d, F, v] using padic_finrank_eq_one p
  exact padicFreeContinuousAddEquivOfEq p q d hq hd
theorem

padicIntEquivValuationSubring_coe

L240 ↗
LocalFieldTheory.Padic.padicIntEquivValuationSubring_coe
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
theorem padicIntEquivValuationSubring_coe
    (p : ℕ) [Fact p.Prime] (z : ℤ_[p]) :
    ((padicIntEquivValuationSubring p z :
      (padicDVRValuation p).valuationSubring) : ℚ_[p]) =
        (z : ℚ_[p])
theorem

padicIntEquivValuationSubring_symm_coe

L247 ↗
LocalFieldTheory.Padic.padicIntEquivValuationSubring_symm_coe
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
theorem padicIntEquivValuationSubring_symm_coe
    (p : ℕ) [Fact p.Prime]
    (z : (padicDVRValuation p).valuationSubring) :
    (((padicIntEquivValuationSubring p).symm z : ℤ_[p]) : ℚ_[p]) =
      (z : ℚ_[p])
def

padicIntValuationSubringContinuousMulEquiv

L264 ↗
LocalFieldTheory.Padic.padicIntValuationSubringContinuousMulEquiv
Documentation

The standard p-adic integers and the valuation subring of ℚ_[p] are continuously multiplicatively equivalent.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · full declaration
def padicIntValuationSubringContinuousMulEquiv
    (p : ℕ) [Fact p.Prime] :
    let v := padicDVRValuation p
    ℤ_[p] ≃ₜ* v.valuationSubring := by
  let v := padicDVRValuation p
  let e := padicIntEquivValuationSubring p
  exact
    { e.toMulEquiv with
      continuous_toFun := by
        apply Continuous.subtype_mk
        exact isometry_subtype_coe.continuous.congr fun z =>
          padicIntEquivValuationSubring_coe p z
      continuous_invFun := by
        apply Continuous.subtype_mk
        exact isometry_subtype_coe.continuous.congr fun z =>
          (padicIntEquivValuationSubring_symm_coe p z).symm }
def

continuousMultiplicativeEquivOfAddEquiv

L283 ↗
LocalFieldTheory.Padic.continuousMultiplicativeEquivOfAddEquiv
Documentation

Multiplicative tagging turns a continuous additive equivalence into a continuous multiplicative equivalence.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
def continuousMultiplicativeEquivOfAddEquiv
    {A B : Type*} [AddZeroClass A] [AddZeroClass B]
    [TopologicalSpace A] [TopologicalSpace B]
    (e : A ≃ₜ+ B) :
    Multiplicative A ≃ₜ* Multiplicative B
def

prodMultiplicativeContinuousMulEquiv

L293 ↗
LocalFieldTheory.Padic.prodMultiplicativeContinuousMulEquiv
Documentation

Multiplicative tagging commutes continuously with binary products.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
def prodMultiplicativeContinuousMulEquiv
    (A B : Type*) [AddZeroClass A] [AddZeroClass B]
    [TopologicalSpace A] [TopologicalSpace B] :
    Multiplicative (A × B) ≃ₜ*
      Multiplicative A × Multiplicative B
def

continuousMulEquivProdCongr

L303 ↗
LocalFieldTheory.Padic.continuousMulEquivProdCongr
Documentation

The product of two continuous multiplicative equivalences.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
def continuousMulEquivProdCongr
    {A B C D : Type*}
    [TopologicalSpace A] [TopologicalSpace B]
    [TopologicalSpace C] [TopologicalSpace D]
    [MulOneClass A] [MulOneClass B] [MulOneClass C] [MulOneClass D]
    (e : A ≃ₜ* B) (f : C ≃ₜ* D) :
    A × C ≃ₜ* B × D
def

continuousMulEquivProdAssoc

L319 ↗
LocalFieldTheory.Padic.continuousMulEquivProdAssoc
Documentation

Continuous multiplicative reassociation of a triple product.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
def continuousMulEquivProdAssoc
    (A B C : Type*) [TopologicalSpace A] [TopologicalSpace B]
    [TopologicalSpace C] [MulOneClass A] [MulOneClass B] [MulOneClass C] :
    (A × B) × C ≃ₜ* A × (B × C)
def

padicPrincipalUnitDirectTopology

L334 ↗
LocalFieldTheory.Padic.padicPrincipalUnitDirectTopology
Documentation

The topology on the first principal-unit group induced directly from the valuation topology on ℚ_[p].

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · full declaration
def padicPrincipalUnitDirectTopology
    (p : ℕ) [Fact p.Prime] :
    let v := padicDVRValuation p
    let F := LocalField.ofWithZeroValuation v
    TopologicalSpace
      (CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF 1) := by
  let v := padicDVRValuation p
  let F := LocalField.ofWithZeroValuation v
  letI : Valued ℚ_[p] (WithZero (Multiplicative ℤ)) :=
    Valued.mk' v
  exact inferInstance
def

padicPrincipalUnitStandardTopology

L348 ↗
LocalFieldTheory.Padic.padicPrincipalUnitStandardTopology
Documentation

The standard topology on the first principal-unit group of ℚ_[p].

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · full declaration
def padicPrincipalUnitStandardTopology
    (p : ℕ) [Fact p.Prime] :
    let v := padicDVRValuation p
    let F := LocalField.ofWithZeroValuation v
    TopologicalSpace
      (CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF 1) := by
  exact inferInstance
theorem

padicPrincipalUnitDirectTopology_eq_standard

L358 ↗
LocalFieldTheory.Padic.padicPrincipalUnitDirectTopology_eq_standard
Documentation

The directly induced valuation topology agrees with the standard topology on the first principal-unit group of ℚ_[p].

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
theorem padicPrincipalUnitDirectTopology_eq_standard
    (p : ℕ) [Fact p.Prime] :
    padicPrincipalUnitDirectTopology p =
      padicPrincipalUnitStandardTopology p
def

padicPrincipalDataDirect

L379 ↗
LocalFieldTheory.Padic.padicPrincipalDataDirect
Documentation

The mixed-characteristic structure data for the first principal units, using the valuation-induced topology directly.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · full declaration
def padicPrincipalDataDirect
    (p : ℕ) [Fact p.Prime] :
    let v := padicDVRValuation p
    let F := LocalField.ofWithZeroValuation v
    letI : LocalField.MixedWithZeroValuationContext v :=
      LocalField.mixedWithZeroValuationContext v
    letI : Valued ℚ_[p] (WithZero (Multiplicative ℤ)) :=
      Valued.mk' v
    let d := Module.finrank ℚ_[F.residueCharacteristic] ℚ_[p]
    Σ a : ℕ,
      Multiplicative
          (ZMod (F.residueCharacteristic ^ a) ×
            (Fin d → ℤ_[F.residueCharacteristic])) ≃ₜ*
        CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF 1 := by
  let v := padicDVRValuation p
  let F := LocalField.ofWithZeroValuation v
  letI : LocalField.MixedWithZeroValuationContext v :=
    LocalField.mixedWithZeroValuationContext v
  letI : Valued ℚ_[p] (WithZero (Multiplicative ℤ)) :=
    Valued.mk' v
  exact LocalField.chosenMixed_firstPrincipalUnitStructure_ofWithZeroValuation
    v (padicDVRValuation_surjective p)
def

padicPrincipalMulData

L404 ↗
LocalFieldTheory.Padic.padicPrincipalMulData
Documentation

The multiplicative equivalence underlying the first-principal-unit structure data for ℚ_[p].

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · full declaration
def padicPrincipalMulData
    (p : ℕ) [Fact p.Prime] :
    let v := padicDVRValuation p
    let F := LocalField.ofWithZeroValuation v
    letI : LocalField.MixedWithZeroValuationContext v :=
      LocalField.mixedWithZeroValuationContext v
    let d := Module.finrank ℚ_[F.residueCharacteristic] ℚ_[p]
    Σ a : ℕ,
      Multiplicative
          (ZMod (F.residueCharacteristic ^ a) ×
            (Fin d → ℤ_[F.residueCharacteristic])) ≃*
        CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF 1 := by
  let v := padicDVRValuation p
  let F := LocalField.ofWithZeroValuation v
  letI : LocalField.MixedWithZeroValuationContext v :=
    LocalField.mixedWithZeroValuationContext v
  letI : Valued ℚ_[p] (WithZero (Multiplicative ℤ)) :=
    Valued.mk' v
  exact ⟨(padicPrincipalDataDirect p).1,
    (padicPrincipalDataDirect p).2.toMulEquiv⟩
def

padicPrincipalData

L427 ↗
LocalFieldTheory.Padic.padicPrincipalData
Documentation

The first-principal-unit structure data transported to the standard p-adic topology.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · full declaration
def padicPrincipalData
    (p : ℕ) [Fact p.Prime] :
    let v := padicDVRValuation p
    let F := LocalField.ofWithZeroValuation v
    letI : LocalField.MixedWithZeroValuationContext v :=
      LocalField.mixedWithZeroValuationContext v
    let d := Module.finrank ℚ_[F.residueCharacteristic] ℚ_[p]
    Σ a : ℕ,
      Multiplicative
          (ZMod (F.residueCharacteristic ^ a) ×
            (Fin d → ℤ_[F.residueCharacteristic])) ≃ₜ*
        CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF 1 := by
  let v := padicDVRValuation p
  let F := LocalField.ofWithZeroValuation v
  letI : LocalField.MixedWithZeroValuationContext v :=
    LocalField.mixedWithZeroValuationContext v
  let d := Module.finrank ℚ_[F.residueCharacteristic] ℚ_[p]
  let U := CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF 1
  let direct : Valued ℚ_[p] (WithZero (Multiplicative ℤ)) :=
    Valued.mk' v
  letI : Valued ℚ_[p] (WithZero (Multiplicative ℤ)) := direct
  let raw :=
    LocalField.chosenMixed_firstPrincipalUnitStructure_ofWithZeroValuation
      v (padicDVRValuation_surjective p)
  let directTopology : TopologicalSpace U := inferInstance
  let standardTopology : TopologicalSpace U :=
    padicPrincipalUnitStandardTopology p
  have hdirect :
      directTopology = padicPrincipalUnitDirectTopology p := by
    unfold directTopology padicPrincipalUnitDirectTopology
    rfl
  have htop : directTopology = standardTopology :=
    hdirect.trans (padicPrincipalUnitDirectTopology_eq_standard p)
  let P := fun T : TopologicalSpace U => by
    letI : TopologicalSpace U := T
    exact Σ a : ℕ,
      Multiplicative
          (ZMod (F.residueCharacteristic ^ a) ×
            (Fin d → ℤ_[F.residueCharacteristic])) ≃ₜ* U
  have hraw : P directTopology := raw
  have hstandard : P standardTopology :=
    (congrArg P htop).mp hraw
  exact hstandard
abbrev

padicUnitFiniteFactor

L472 ↗
LocalFieldTheory.Padic.padicUnitFiniteFactor
Documentation

The finite factor in the topological decomposition of ℤ_pˣ.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
abbrev padicUnitFiniteFactor
    (p : ℕ) [Fact p.Prime] : Type
def

padicUnitDecomposition

L493 ↗
LocalFieldTheory.Padic.padicUnitDecomposition
Documentation

The standard topological decomposition ℤ_pˣ ≃ finite × ℤ_p used in the local reciprocity calculation.

Source context 10 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup (
  continuousMulEquivOfCompactToT2
  residueRootsOfUnityContinuousMulEquivZMod
  residueRootsOfUnityEquivResidueFieldUnits
  valuationSubringUnitsEquivRootsTimesPrincipalUnits
  valuationSubringUnitsEquivRootsTimesPrincipalUnits_apply
) in
Lean source · statement
def padicUnitDecomposition
    (p : ℕ) [Fact p.Prime] :
    padicUnitFiniteFactor p × Multiplicative ℤ_[p] ≃ₜ*
      ℤ_[p]ˣ
instance

padicUnitFiniteFactor_finite

L592 ↗
LocalFieldTheory.Padic.padicUnitFiniteFactor_finite
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace LocalFieldTheory
namespace Padic
open scoped WithZero
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance padicDVRResidueFinite
    (p : ℕ) [Fact p.Prime] :
    Finite
      (IsLocalRing.ResidueField
        (padicDVRValuation p).valuationSubring) := by
  simpa [padicCompleteDVF] using
    padicCompleteDVF_residueField_finite p
Lean source · statement
instance padicUnitFiniteFactor_finite
    (p : ℕ) [Fact p.Prime] :
    Finite (padicUnitFiniteFactor p)

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