NYLL
Module

SeparableNormValuation.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.SeparableNormValuation
27 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: normalized valuation of field norms

This file supplies the local-field calculation used when the abstract class-formation framework is specialized to separable-closure units. All ramification and residue degrees below are the actual invariants of the valuation-ring extension; no packaged norm-valuation hypothesis is assumed.

Imports6
Imported by8

Declarations

instance

(anonymous instance)

L43 ↗
Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNorm
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
  [IsIntegrallyClosed R] [IsIntegrallyClosed S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
Lean source · statement
instance : Algebra (FractionRing R) (FractionRing S)
theorem

intermediateNormalClosure_isSeparable_of_isSeparable

L50 ↗
LocalClassFieldTheory.intermediateNormalClosure_isSeparable_of_isSeparable
Documentation

A normal closure inside a separable ambient field is separable over the base whenever the extension being closed is separable. Keeping this field-theoretic step separate prevents the integral-closure transport below from repeatedly elaborating the full iSup of embedding ranges.

Source context 9 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNorm
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
  [IsIntegrallyClosed R] [IsIntegrallyClosed S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
Lean source · statement
theorem intermediateNormalClosure_isSeparable_of_isSeparable
    (K : Type u) (L : Type v) (A : Type w)
    [Field K] [Field L] [Field A]
    [Algebra K L] [Algebra K A] [Algebra L A]
    [IsScalarTower K L A] [Algebra.IsSeparable K L] :
    Algebra.IsSeparable K (IntermediateField.normalClosure K L A)
theorem

intermediateNormalClosure_isGalois_of_isSeparable

L62 ↗
LocalClassFieldTheory.intermediateNormalClosure_isGalois_of_isSeparable
Documentation

The field-theoretic normal closure of a finite separable extension is Galois, with no perfectness assumption on the base.

Source context 9 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNorm
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
  [IsIntegrallyClosed R] [IsIntegrallyClosed S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
Lean source · statement
theorem intermediateNormalClosure_isGalois_of_isSeparable
    (K : Type u) (L : Type v) (A : Type w)
    [Field K] [Field L] [Field A]
    [Algebra K L] [Algebra K A] [Algebra L A]
    [IsScalarTower K L A] [FiniteDimensional K L]
    [Algebra.IsSeparable K L] [Normal K A] :
    IsGalois K (IntermediateField.normalClosure K L A)
theorem

intermediateNormalClosure_finiteDimensional_top

L76 ↗
LocalClassFieldTheory.intermediateNormalClosure_finiteDimensional_top
Documentation

A finite extension remains finite over the field-theoretic normal closure when viewed from the top of the tower.

Source context 9 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNorm
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
  [IsIntegrallyClosed R] [IsIntegrallyClosed S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
Lean source · full declaration
theorem intermediateNormalClosure_finiteDimensional_top
    (K : Type u) (L : Type v) (A : Type w)
    [Field K] [Field L] [Field A]
    [Algebra K L] [Algebra K A] [Algebra L A]
    [IsScalarTower K L A] [FiniteDimensional K L] :
    let E := IntermediateField.normalClosure K L A
    letI : Algebra L E := normalClosure.algebra K L A
    FiniteDimensional L E := by
  exact Module.Finite.right K L (IntermediateField.normalClosure K L A)
theorem

ringNormalClosure_isFractionRing

L89 ↗
LocalClassFieldTheory.ringNormalClosure_isFractionRing
Documentation

The integral normal closure has the field-theoretic normal closure as its fraction field.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNorm
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
  [IsIntegrallyClosed R] [IsIntegrallyClosed S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
omit [IsIntegrallyClosed R] [IsIntegrallyClosed S] in
Lean source · full declaration
theorem ringNormalClosure_isFractionRing :
    let K := FractionRing R
    let L := FractionRing S
    let A := AlgebraicClosure L
    let E := IntermediateField.normalClosure K L A
    let T := Ring.NormalClosure R S
    letI : Algebra L E := normalClosure.algebra K L A
    letI : Algebra S E := ((algebraMap L E).comp (algebraMap S L)).toAlgebra
    letI : Algebra T E := by
      change Algebra (integralClosure S E) E
      infer_instance
    IsFractionRing T E := by
  let K := FractionRing R
  let L := FractionRing S
  let A := AlgebraicClosure L
  let E := IntermediateField.normalClosure K L A
  let : Algebra L E := normalClosure.algebra K L A
  let T := Ring.NormalClosure R S
  let : Algebra S E := ((algebraMap L E).comp (algebraMap S L)).toAlgebra
  let : IsScalarTower S L E := by
    apply IsScalarTower.of_algebraMap_eq
    intro x
    rfl
  let : Algebra T E := by
    change Algebra (integralClosure S E) E
    infer_instance
  let : FiniteDimensional L E :=
    intermediateNormalClosure_finiteDimensional_top K L A
  change IsFractionRing (integralClosure S E) E
  exact integralClosure.isFractionRing_of_finite_extension L E
theorem

ringNormalClosure_isGalois_transport

L123 ↗
LocalClassFieldTheory.ringNormalClosure_isGalois_transport
Documentation

Transport Galoisness from the field-theoretic normal closure to the fraction field of the integral normal closure.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNorm
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
  [IsIntegrallyClosed R] [IsIntegrallyClosed S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
omit [IsIntegrallyClosed R] [IsIntegrallyClosed S] in
Lean source · full declaration
theorem ringNormalClosure_isGalois_transport :
    let K := FractionRing R
    let L := FractionRing S
    let A := AlgebraicClosure L
    let E := IntermediateField.normalClosure K L A
    let T := Ring.NormalClosure R S
    letI : Algebra K E := SubalgebraClass.toAlgebra E
    letI : Algebra K (FractionRing T) :=
      FractionRing.liftAlgebra R (FractionRing T)
    IsGalois K E → IsGalois K (FractionRing T) := by
  simp only
  let K := FractionRing R
  let L := FractionRing S
  let A := AlgebraicClosure L
  let E := IntermediateField.normalClosure K L A
  let : Algebra L E := normalClosure.algebra K L A
  let T := Ring.NormalClosure R S
  let : Algebra S E := ((algebraMap L E).comp (algebraMap S L)).toAlgebra
  let : IsScalarTower S L E := by
    apply IsScalarTower.of_algebraMap_eq
    intro x
    rfl
  let : Algebra T E := by
    change Algebra (integralClosure S E) E
    infer_instance
  let : IsScalarTower S T E :=
    IsScalarTower.subalgebra' S E E (integralClosure S E)
  let : IsScalarTower R L E := IsScalarTower.to₁₃₄ R K L E
  let : IsScalarTower R S E := IsScalarTower.to₁₂₄ R S L E
  let : IsScalarTower R T E := IsScalarTower.to₁₃₄ R S T E
  let : IsFractionRing T E := ringNormalClosure_isFractionRing R S
  intro hGalois
  refine IsGalois.of_equiv_equiv (F := K) («E» := E)
    (f := (FractionRing.algEquiv R K).symm.toRingEquiv)
    (g := (FractionRing.algEquiv T E).symm.toRingEquiv) ?_
  ext
  simpa using IsFractionRing.algEquiv_commutes
    (FractionRing.algEquiv R K).symm
    (FractionRing.algEquiv T E).symm _
theorem

ringNormalClosure_moduleFinite_of_isSeparable

L166 ↗
LocalClassFieldTheory.ringNormalClosure_moduleFinite_of_isSeparable
Documentation

Finiteness of the integral normal closure follows from separability of the original fraction-field extension.

Source context 10 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNorm
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
  [IsIntegrallyClosed R] [IsIntegrallyClosed S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
omit [IsIntegrallyClosed R] in
Lean source · statement
theorem ringNormalClosure_moduleFinite_of_isSeparable
    [IsNoetherianRing S]
    [Algebra.IsSeparable (FractionRing R) (FractionRing S)] :
    Module.Finite S (Ring.NormalClosure R S)
instance

(anonymous instance)

L204 ↗
Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNormDedekind
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDedekindDomain S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
Lean source · statement
instance : Algebra (FractionRing R) (FractionRing S)
theorem

ringNormalClosure_isDedekindDomain_of_isSeparable

L209 ↗
LocalClassFieldTheory.ringNormalClosure_isDedekindDomain_of_isSeparable
Documentation

The same separable normal-closure construction is Dedekind when the original rings are Dedekind.

Source context 9 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNormDedekind
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDedekindDomain S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
Lean source · statement
theorem ringNormalClosure_isDedekindDomain_of_isSeparable
    [Algebra.IsSeparable (FractionRing R) (FractionRing S)] :
    IsDedekindDomain (Ring.NormalClosure R S)
instance

(anonymous instance)

L246 ↗
Source context 8 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNormGalois
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
Lean source · statement
instance : Algebra (FractionRing R) (FractionRing S)
theorem

ringNormalClosure_isGalois_of_isSeparable

L253 ↗
LocalClassFieldTheory.ringNormalClosure_isGalois_of_isSeparable
Documentation

The normal closure of a finite separable extension of fraction fields is Galois without assuming that the base fraction field is perfect. Mathlib's default instance uses perfectness because it treats arbitrary finite extensions; here separability is precisely the available hypothesis.

Source context 9 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNormGalois
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
local instance : Algebra (FractionRing R) (FractionRing S) :=
  FractionRing.liftAlgebra R (FractionRing S)
Lean source · statement
theorem ringNormalClosure_isGalois_of_isSeparable
    [Algebra.IsSeparable (FractionRing R) (FractionRing S)] :
    IsGalois (FractionRing R)
      (FractionRing (Ring.NormalClosure R S))
theorem

relNorm_eq_pow_inertiaDeg_of_isSeparable

L279 ↗
LocalClassFieldTheory.relNorm_eq_pow_inertiaDeg_of_isSeparable
Documentation

Relative ideal norm of a maximal ideal in a finite separable extension. This is the separable replacement for mathlib's perfect-base theorem and is proved by the same normal-closure descent.

Source context 9 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
section SeparableIdealNormRelNorm
variable (R : Type u) (S : Type v)
  [CommRing R] [IsDedekindDomain R]
  [CommRing S] [IsDedekindDomain S]
  [Algebra R S] [Module.Finite R S] [Module.IsTorsionFree R S]
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem relNorm_eq_pow_inertiaDeg_of_isSeparable
    [Algebra.IsSeparable (FractionRing R) (FractionRing S)]
    (P : Ideal S) (p : Ideal R) [P.LiesOver p]
    [P.IsMaximal] [p.IsMaximal] :
    Ideal.relNorm R P = p ^ P.inertiaDeg R
theorem

maximalIdeal_map_eq_maximalIdeal_pow_ramificationIdx

L326 ↗
LocalClassFieldTheory.maximalIdeal_map_eq_maximalIdeal_pow_ramificationIdx
Documentation

The image of the base maximal ideal in a finite local-field extension is the power of the upstairs maximal ideal given by the actual Dedekind ramification index.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem maximalIdeal_map_eq_maximalIdeal_pow_ramificationIdx
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    Ideal.map (algebraMap 𝒪[K] 𝒪[L]) (𝓂[K] : Ideal 𝒪[K]) =
      (𝓂[L] : Ideal 𝒪[L]) ^
        (𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K]
theorem

maximalIdeal_map_eq_maximalIdeal_pow_ramificationIdx_of_isIntegralClosure

L354 ↗
LocalClassFieldTheory.maximalIdeal_map_eq_maximalIdeal_pow_ramificationIdx_of_isIntegralClosure
Documentation

Integral closure and separability produce the finite valuation-ring module needed by the preceding ideal factorization.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem maximalIdeal_map_eq_maximalIdeal_pow_ramificationIdx_of_isIntegralClosure
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    Ideal.map (algebraMap 𝒪[K] 𝒪[L]) (𝓂[K] : Ideal 𝒪[K]) =
      (𝓂[L] : Ideal 𝒪[L]) ^
        (𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K]
theorem

fractionRing_integerRing_isSeparable

L373 ↗
LocalClassFieldTheory.fractionRing_integerRing_isSeparable
Documentation

Separability of an actual field extension transfers to the canonical fraction fields of its valuation integer rings.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem fractionRing_integerRing_isSeparable
    (K : Type u) (L : Type v)
    [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L]
    [Algebra K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] :
    Algebra.IsSeparable (FractionRing 𝒪[K]) (FractionRing 𝒪[L])
theorem

relNorm_maximalIdeal_eq_pow_residue_finrank

L392 ↗
LocalClassFieldTheory.relNorm_maximalIdeal_eq_pow_residue_finrank
Documentation

In a finite separable local-field extension, the relative ideal norm of the upstairs maximal ideal is the residue-degree power of the base maximal ideal.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem relNorm_maximalIdeal_eq_pow_residue_finrank
    (K : Type u) (L : Type v)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    Ideal.relNorm 𝒪[K] (𝓂[L] : Ideal 𝒪[L]) =
      (𝓂[K] : Ideal 𝒪[K]) ^ Module.finrank 𝓀[K] 𝓀[L]
theorem

v_normUnits_integerRingUniformizerFieldUnit_of_isSeparable

L415 ↗
LocalClassFieldTheory.v_normUnits_integerRingUniformizerFieldUnit_of_isSeparable
Documentation

The norm of the chosen upstairs prime element has base normalized value the negative of the actual residue degree, for every finite separable extension (not only a Galois one).

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem v_normUnits_integerRingUniformizerFieldUnit_of_isSeparable
    (K : Type u) (L : Type v)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    v K (Additive.ofMul
        (normUnits K L (integerRingUniformizerFieldUnit L))) =
      -(Module.finrank 𝓀[K] 𝓀[L] : Int)
theorem

v_normUnits_inverseIntegerRingUniformizerFieldUnit_of_isSeparable

L475 ↗
LocalClassFieldTheory.v_normUnits_inverseIntegerRingUniformizerFieldUnit_of_isSeparable
Documentation

The norm of the positive generator (the inverse chosen prime element) has base normalized value equal to the actual residue degree.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem v_normUnits_inverseIntegerRingUniformizerFieldUnit_of_isSeparable
    (K : Type u) (L : Type v)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    v K (Additive.ofMul
        (normUnits K L (inverseIntegerRingUniformizerFieldUnit L))) =
      (Module.finrank 𝓀[K] 𝓀[L] : Int)
theorem

v_normUnits_eq_residue_finrank_mul_of_isSeparable

L495 ↗
LocalClassFieldTheory.v_normUnits_eq_residue_finrank_mul_of_isSeparable
Documentation

Finite local reciprocity, normalized norm calculation for every finite separable local-field extension: the normalized value of a field norm is the actual residue degree times the upstairs normalized value.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem v_normUnits_eq_residue_finrank_mul_of_isSeparable
    (K : Type u) (L : Type v)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (x : Lˣ) :
    v K (Additive.ofMul (normUnits K L x)) =
      (Module.finrank 𝓀[K] 𝓀[L] : Int) *
        v L (Additive.ofMul x)
theorem

v_mapBaseUnitsToExtensionUnits_integerRingUniformizerFieldUnit

L541 ↗
LocalClassFieldTheory.v_mapBaseUnitsToExtensionUnits_integerRingUniformizerFieldUnit
Documentation

The image of the chosen base prime element has upstairs normalized value the negative of the actual ramification index.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem v_mapBaseUnitsToExtensionUnits_integerRingUniformizerFieldUnit
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    v L (Additive.ofMul
        (mapBaseUnitsToExtensionUnits K L
          (integerRingUniformizerFieldUnit K))) =
      -((𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K] : Int)
theorem

v_mapBaseUnitsToExtensionUnits_integerRingUniformizerFieldUnit_of_isIntegralClosure

L596 ↗
LocalClassFieldTheory.v_mapBaseUnitsToExtensionUnits_integerRingUniformizerFieldUnit_of_isIntegralClosure
Documentation

Integral closure and separability produce the module-finiteness used in the uniformizer scaling calculation.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem v_mapBaseUnitsToExtensionUnits_integerRingUniformizerFieldUnit_of_isIntegralClosure
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    v L (Additive.ofMul
        (mapBaseUnitsToExtensionUnits K L
          (integerRingUniformizerFieldUnit K))) =
      -((𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K] : Int)
theorem

mapBaseUnitsToExtensionUnits_integerUnitsToFieldUnits

L617 ↗
LocalClassFieldTheory.mapBaseUnitsToExtensionUnits_integerUnitsToFieldUnits
Documentation

Base extension commutes with the two canonical inclusions of valuation integer units into field units.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem mapBaseUnitsToExtensionUnits_integerUnitsToFieldUnits
    (K L : Type u)
    [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    (x : 𝒪[K]ˣ) :
    mapBaseUnitsToExtensionUnits K L (integerUnitsToFieldUnits K x) =
      integerUnitsToFieldUnits L
        (Units.map (algebraMap 𝒪[K] 𝒪[L]).toMonoidHom x)
theorem

v_mapBaseUnitsToExtensionUnits_inverseIntegerRingUniformizerFieldUnit_of_isIntegralClosure

L633 ↗
LocalClassFieldTheory.v_mapBaseUnitsToExtensionUnits_inverseIntegerRingUniformizerFieldUnit_of_isIntegralClosure
Documentation

The positive generator (the inverse chosen prime element) scales by the actual ramification index under base extension.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem v_mapBaseUnitsToExtensionUnits_inverseIntegerRingUniformizerFieldUnit_of_isIntegralClosure
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    v L (Additive.ofMul
        (mapBaseUnitsToExtensionUnits K L
          (inverseIntegerRingUniformizerFieldUnit K))) =
      ((𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K] : Int)
theorem

v_mapBaseUnitsToExtensionUnits_eq_ramificationIdx_mul

L654 ↗
LocalClassFieldTheory.v_mapBaseUnitsToExtensionUnits_eq_ramificationIdx_mul
Documentation

Normalized valuations in a finite separable local-field extension scale under the base embedding by the actual ramification index.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem v_mapBaseUnitsToExtensionUnits_eq_ramificationIdx_mul
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (x : Kˣ) :
    v L (Additive.ofMul (mapBaseUnitsToExtensionUnits K L x)) =
      ((𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K] : Int) *
        v K (Additive.ofMul x)
theorem

v_normUnits_eq_residue_finrank_mul_of_isGalois

L703 ↗
LocalClassFieldTheory.v_normUnits_eq_residue_finrank_mul_of_isGalois
Documentation

The Galois specialization of the finite-separable normalized norm calculation in the finite local reciprocity construction.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem v_normUnits_eq_residue_finrank_mul_of_isGalois
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (x : Lˣ) :
    v K (Additive.ofMul (normUnits K L x)) =
      (Module.finrank 𝓀[K] 𝓀[L] : Int) *
        v L (Additive.ofMul x)
theorem

valuationMap_comp_normUnits_range_eq_zmultiples_of_isSeparable

L722 ↗
LocalClassFieldTheory.valuationMap_comp_normUnits_range_eq_zmultiples_of_isSeparable
Documentation

Finite local reciprocity, normalized norm range for every finite separable local-field extension. Surjectivity of the upstairs normalized valuation turns the pointwise norm formula into the exact subgroup fℤ.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem valuationMap_comp_normUnits_range_eq_zmultiples_of_isSeparable
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    ((valuationMap K).comp
      (MonoidHom.toAdditive (normUnits K L))).range =
        AddSubgroup.zmultiples (Module.finrank 𝓀[K] 𝓀[L] : Int)
theorem

valuationMap_comp_normUnits_range_eq_zmultiples_of_isGalois

L766 ↗
LocalClassFieldTheory.valuationMap_comp_normUnits_range_eq_zmultiples_of_isGalois
Documentation

The Galois specialization of the finite-separable norm-range theorem in the finite local reciprocity construction.

Source context 7 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u v w
open scoped BigOperators ValuativeRel
open IsNonarchimedeanLocalField
attribute [local instance] FractionRing.liftAlgebra
Lean source · statement
theorem valuationMap_comp_normUnits_range_eq_zmultiples_of_isGalois
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    ((valuationMap K).comp
      (MonoidHom.toAdditive (normUnits K L))).range =
        AddSubgroup.zmultiples (Module.finrank 𝓀[K] 𝓀[L] : Int)

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