NYLL
Module

NormRestriction.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FinitePlaceArtin.NormRestriction
53 declarations indexed from sourceView source ↗

Module documentation

Norm--restriction for finite-place Artin homomorphisms

This module proves norm--restriction naturality for finite-place Artin maps in an actual square of number fields and their chosen completed local extensions.

Imports2
Imported by2

Declarations

theorem

finitePlaceArtinNormUnits_map_ringEquiv

L37 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceArtinNormUnits_map_ringEquiv
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem finitePlaceArtinNormUnits_map_ringEquiv
    {F M F' M' : Type}
    [Field F] [Field M] [Field F'] [Field M']
    [Algebra F M] [Algebra F' M']
    (eF : F ≃+* F') (eM : M ≃+* M')
    (he :
      RingHom.comp (algebraMap F' M') eF =
        RingHom.comp eM (algebraMap F M))
    (x : Mˣ) :
    Units.mapEquiv eF.toMulEquiv
        (LocalFieldTheory.normUnits F M x) =
      LocalFieldTheory.normUnits F' M'
        (Units.mapEquiv eM.toMulEquiv x)
abbrev

finitePlaceNormCompletion

L57 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormCompletion
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
abbrev finitePlaceNormCompletion
    (F : Type) [Field F] [NumberField F]
    (v : HeightOneSpectrum (𝓞 F))
abbrev

finitePlaceNormLocalizedCompletion

L62 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLocalizedCompletion
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
abbrev finitePlaceNormLocalizedCompletion
    (F M : Type) [Field F] [Field M] [Algebra F M]
    [NumberField F]
    (v : HeightOneSpectrum (𝓞 F))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv F v) M)
def

finitePlaceRelativeNormUnits

L71 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceRelativeNormUnits
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
def finitePlaceRelativeNormUnits
    {K' : Type}
    [Field K'] [NumberField K'] [Algebra K K']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v) :
    (finitePlaceNormCompletion K' W)ˣ →*
      (finitePlaceNormCompletion K v)ˣ
def

finitePlaceConcreteNormUnits

L88 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceConcreteNormUnits
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
def finitePlaceConcreteNormUnits
    {K' : Type}
    [Field K'] [NumberField K'] [Algebra K K']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v) :
    (W.adicCompletion K')ˣ →* (v.adicCompletion K)ˣ
theorem

finitePlaceArtinConcreteNormUnits

L101 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceArtinConcreteNormUnits
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem finitePlaceArtinConcreteNormUnits
    {K' : Type}
    [Field K'] [NumberField K'] [Algebra K K']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v)
    (x : (W.adicCompletion K')ˣ) :
      finitePlaceCompletionUnitsContinuousMulEquiv v
        (finitePlaceRelativeNormUnits
          (K := K) (K' := K') v W hW
          ((finitePlaceCompletionUnitsContinuousMulEquiv W).symm x)) =
      finitePlaceConcreteNormUnits
        (K := K) (K' := K') v W hW x
theorem

finitePlaceArtinHasExtension_of_norm

L195 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceArtinHasExtension_of_norm
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem finitePlaceArtinHasExtension_of_norm
    {A B C D : Type}
    [NormedField A] [NormedField B]
    [NormedField C] [NormedField D]
    [Algebra C D]
    [Valued C ℝ≥0] [Valued D ℝ≥0]
    [ValuativeRel C] [ValuativeRel D]
    [(Valued.v : Valuation C ℝ≥0).Compatible]
    [(Valued.v : Valuation D ℝ≥0).Compatible]
    (eC : C ≃+* A) (eD : D ≃+* B)
    (baseMap : A →+* B)
    (hAlgebraMap : ∀ x : C,
      algebraMap C D x =
        eD.symm (baseMap (eC x)))
    (hDNorm : ∀ y : B, ‖eD.symm y‖ = ‖y‖)
    (hCNorm : ∀ x : C, ‖eC x‖ = ‖x‖)
    (hBaseNorm : ∀ x : A,
      ‖baseMap x‖ ≤ 1 ↔ ‖x‖ ≤ 1)
    (hDValuation : ∀ x : D,
      (Valued.v : Valuation D ℝ≥0) x = ‖x‖₊)
    (hCValuation : ∀ x : C,
      (Valued.v : Valuation C ℝ≥0) x = ‖x‖₊) :
    (ValuativeRel.valuation C).HasExtension
      (ValuativeRel.valuation D)
theorem

finitePlaceArtinCompletionHasExtension

L247 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceArtinCompletionHasExtension
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
theorem finitePlaceArtinCompletionHasExtension
    {K' : Type}
    [Field K'] [NumberField K'] [Algebra K K']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v) :
    let vK := NumberField.HeightOneSpectrum.adicAbv K v
    let vK' := NumberField.HeightOneSpectrum.adicAbv K' W
    let C := vK.Completion
    let D := vK'.Completion
    let hvKna : IsNonarchimedean (vK : K → ℝ) :=
      NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v
    let hvK'na : IsNonarchimedean (vK' : K' → ℝ) :=
      NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W
    letI : IsUltrametricDist C :=
      finitePlaceArtinCompletionIsUltrametricDist vK hvKna
    letI : Valued C ℝ≥0 :=
      finitePlaceArtinCompletionValued vK hvKna
    letI : ValuativeRel C :=
      finitePlaceArtinCompletionValuativeRel vK hvKna
    let vC : Valuation C ℝ≥0 := Valued.v
    letI : vC.Compatible :=
      Valuation.Compatible.ofValuation vC
    letI : IsUltrametricDist D :=
      finitePlaceArtinCompletionIsUltrametricDist vK' hvK'na
    letI : Valued D ℝ≥0 :=
      finitePlaceArtinCompletionValued vK' hvK'na
    letI : ValuativeRel D :=
      finitePlaceArtinCompletionValuativeRel vK' hvK'na
    let vD : Valuation D ℝ≥0 := Valued.v
    letI : vD.Compatible :=
      Valuation.Compatible.ofValuation vD
    letI : Algebra C D :=
      (finitePlaceArtinRelativeCompletionRingHom
        (K := K) (K' := K') v W hW).toAlgebra
    (ValuativeRel.valuation C).HasExtension
      (ValuativeRel.valuation D) := by
  let vK := NumberField.HeightOneSpectrum.adicAbv K v
  let vK' := NumberField.HeightOneSpectrum.adicAbv K' W
  let C := vK.Completion
  let D := vK'.Completion
  let eC :
      C ≃+* v.adicCompletion K :=
    (relativeFinitePlaceCompletionAlgEquiv v).toRingEquiv
  let eD :
      D ≃+* W.adicCompletion K' :=
    (relativeFinitePlaceCompletionAlgEquiv W).toRingEquiv
  let concreteBaseMap :
      v.adicCompletion K →+* W.adicCompletion K' :=
    finitePlaceAdicCompletionMap K K' v ⟨W, hW⟩
  let : Algebra (v.adicCompletion K) (W.adicCompletion K') :=
    concreteBaseMap.toAlgebra
  let : Algebra C D :=
    (finitePlaceArtinRelativeCompletionRingHom
      (K := K) (K' := K') v W hW).toAlgebra
  let hvKna : IsNonarchimedean (vK : K → ℝ) :=
    NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v
  let : IsUltrametricDist C :=
    finitePlaceArtinCompletionIsUltrametricDist vK hvKna
  let : Valued C ℝ≥0 :=
    finitePlaceArtinCompletionValued vK hvKna
  let vC : Valuation C ℝ≥0 := Valued.v
  let : ValuativeRel C :=
    finitePlaceArtinCompletionValuativeRel vK hvKna
  let : vC.Compatible :=
    Valuation.Compatible.ofValuation vC
  let hvK'na : IsNonarchimedean (vK' : K' → ℝ) :=
    NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W
  let : IsUltrametricDist D :=
    finitePlaceArtinCompletionIsUltrametricDist vK' hvK'na
  let : Valued D ℝ≥0 :=
    finitePlaceArtinCompletionValued vK' hvK'na
  let vD : Valuation D ℝ≥0 := Valued.v
  let : ValuativeRel D :=
    finitePlaceArtinCompletionValuativeRel vK' hvK'na
  let : vD.Compatible :=
    Valuation.Compatible.ofValuation vD
  exact
    finitePlaceArtinHasExtension_of_norm
      eC eD concreteBaseMap
      (by intro x; rfl)
      (relativeFinitePlaceCompletionAlgEquiv_symm_norm W)
      (fun x =>
        (relativeFinitePlaceCompletionRingHom_isometry
          v).norm_map_of_map_zero
            (map_zero
              (relativeFinitePlaceCompletionRingHom v)) x)
      (finitePlaceAdicCompletionMap_norm_le_one_iff
        K K' v ⟨W, hW⟩)
      (fun _ => rfl)
      (fun _ => rfl)
theorem

finitePlaceLocalArtin_norm_restriction_apply

L339 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtin_norm_restriction_apply
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
theorem finitePlaceLocalArtin_norm_restriction_apply
    {C D E E' : Type}
    [Field C] [ValuativeRel C] [TopologicalSpace C]
    [IsNonarchimedeanLocalField C]
    [Field D] [ValuativeRel D] [TopologicalSpace D]
    [IsNonarchimedeanLocalField D]
    [Field E] [Field E']
    [Algebra C D] [Algebra C E] [Algebra C E']
    [Algebra D E'] [Algebra E E']
    [IsScalarTower C D E'] [IsScalarTower C E E']
    [FiniteDimensional C D] [Algebra.IsSeparable C D]
    [Valuation.HasExtension
      (ValuativeRel.valuation C) (ValuativeRel.valuation D)]
    [FiniteDimensional C E] [IsAbelianGalois C E]
    [FiniteDimensional D E'] [IsAbelianGalois D E']
    (y : Dˣ) :
    AlgEquiv.restrictNormalHom E
        ((AlgEquiv.restrictScalarsHom C)
          (LocalClassFieldTheory.abelianLocalArtinMonoidHom
            D E' y)) =
      LocalClassFieldTheory.abelianLocalArtinMonoidHom C E
        (LocalFieldTheory.normUnits C D y)
abbrev

finitePlaceNormLocalizedAut

L365 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLocalizedAut
Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
abbrev finitePlaceNormLocalizedAut
    (F M : Type) [Field F] [Field M] [Algebra F M]
    [NumberField F]
    (v : HeightOneSpectrum (𝓞 F))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv F v) M)
instance

finitePlaceNormLowerExtensionAlgebra

L411 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerExtensionAlgebra
Source context 18 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
Lean source · statement
instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion
instance

finitePlaceNormLowerExtensionSMul

L416 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerExtensionSMul
Source context 19 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
Lean source · statement
instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion
instance

finitePlaceNormLowerCompletionAlgebra

L420 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerCompletionAlgebra
Source context 20 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
Lean source · statement
instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion
instance

finitePlaceNormLowerGlobalAlgebra

L424 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerGlobalAlgebra
Source context 21 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
Lean source · statement
instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ
instance

finitePlaceNormUpperExtensionAlgebra

L428 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperExtensionAlgebra
Source context 22 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
Lean source · statement
instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion
instance

finitePlaceNormUpperExtensionSMul

L433 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperExtensionSMul
Source context 23 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
Lean source · statement
instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion
instance

finitePlaceNormUpperCompletionAlgebra

L437 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperCompletionAlgebra
Source context 24 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
Lean source · statement
instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion
instance

finitePlaceNormUpperGlobalAlgebra

L441 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperGlobalAlgebra
Source context 25 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
Lean source · statement
instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ'
instance

finitePlaceNormLowerNontriviallyNormedField

L445 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerNontriviallyNormedField
Source context 26 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
Lean source · statement
instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ
instance

finitePlaceNormLowerLocallyCompactSpace

L450 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerLocallyCompactSpace
Source context 27 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
Lean source · statement
instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ
instance

finitePlaceNormUpperNontriviallyNormedField

L455 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperNontriviallyNormedField
Source context 28 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
Lean source · statement
instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ
instance

finitePlaceNormUpperLocallyCompactSpace

L460 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperLocallyCompactSpace
Source context 29 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
Lean source · statement
instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ
instance

finitePlaceNormLowerLocalizedFiniteDimensional

L465 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerLocalizedFiniteDimensional
Source context 30 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
Lean source · statement
instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ
instance

finitePlaceNormLowerLocalizedAbelianGalois

L470 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerLocalizedAbelianGalois
Source context 31 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
Lean source · statement
instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ
instance

finitePlaceNormUpperLocalizedFiniteDimensional

L475 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperLocalizedFiniteDimensional
Source context 32 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
Lean source · statement
instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ'
instance

finitePlaceNormUpperLocalizedAbelianGalois

L480 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperLocalizedAbelianGalois
Source context 33 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
Lean source · statement
instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ'
instance

finitePlaceNormLowerUltrametric

L485 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerUltrametric
Source context 34 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
Lean source · statement
instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ
instance

finitePlaceNormLowerValued

L490 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerValued
Source context 35 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
Lean source · statement
instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0
instance

finitePlaceNormLowerValuationNontrivial

L495 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerValuationNontrivial
Source context 36 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
Lean source · statement
instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial
instance

finitePlaceNormLowerValuativeRel

L500 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerValuativeRel
Source context 37 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
Lean source · statement
instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ
instance

finitePlaceNormLowerValuationCompatible

L505 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerValuationCompatible
Source context 38 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
Lean source · statement
instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible
instance

finitePlaceNormLowerValuativeRelNontrivial

L510 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerValuativeRelNontrivial
Source context 39 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
Lean source · statement
instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ
instance

finitePlaceNormLowerLocalField

L515 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerLocalField
Source context 40 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
Lean source · statement
instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ
instance

finitePlaceNormUpperUltrametric

L520 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperUltrametric
Source context 41 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
Lean source · statement
instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ
instance

finitePlaceNormUpperValued

L525 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperValued
Source context 42 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0
instance

finitePlaceNormUpperValuationNontrivial

L530 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperValuationNontrivial
Source context 43 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial
instance

finitePlaceNormUpperValuativeRel

L535 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperValuativeRel
Source context 44 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
Lean source · statement
instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ
instance

finitePlaceNormUpperValuationCompatible

L540 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperValuationCompatible
Source context 45 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible
instance

finitePlaceNormUpperValuativeRelNontrivial

L545 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperValuativeRelNontrivial
Source context 46 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
Lean source · statement
instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ
instance

finitePlaceNormUpperLocalField

L550 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperLocalField
Source context 47 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
Lean source · statement
instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ
def

finitePlaceNormRestrictedArtin

L555 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormRestrictedArtin
Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
def finitePlaceNormRestrictedArtin
    [NumberField L]
    (hW : finitePlaceBelow (K := K) W = v)
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w)
    (y : Dₙˣ) :
    finitePlaceNormLocalizedAut K L v w
def

finitePlaceNormLowerArtin

L574 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerArtin
Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
def finitePlaceNormLowerArtin
    (hW : finitePlaceBelow (K := K) W = v)
    (y : Dₙˣ) :
    finitePlaceNormLocalizedAut K L v w
def

finitePlaceNormUpperRawArtin

L585 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperRawArtin
Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
def finitePlaceNormUpperRawArtin
    (y : Dₙˣ) :
    finitePlaceNormLocalizedAut K' L' W w'
def

finitePlaceNormLowerRawArtin

L591 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerRawArtin
Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
def finitePlaceNormLowerRawArtin
    (hW : finitePlaceBelow (K := K) W = v)
    (y : Dₙˣ) :
    finitePlaceNormLocalizedAut K L v w
theorem

finitePlaceNormUpperArtin_eq_raw

L600 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormUpperArtin_eq_raw
Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
theorem finitePlaceNormUpperArtin_eq_raw
    (y : Dₙˣ) :
    finitePlaceLocalArtinMonoidHom
        (K := K') (L := L') W w'
        (finitePlaceCompletionUnitsContinuousMulEquiv W y) =
      finitePlaceNormUpperRawArtin
        (K' := K') (L' := L') W w' y
theorem

finitePlaceNormLowerArtin_eq_raw

L620 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLowerArtin_eq_raw
Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
theorem finitePlaceNormLowerArtin_eq_raw
    (hW : finitePlaceBelow (K := K) W = v)
    (y : Dₙˣ) :
    finitePlaceNormLowerArtin
        (K := K) (L := L) (K' := K')
        v W w hW y =
      finitePlaceNormLowerRawArtin
        (K := K) (L := L) (K' := K')
        v W w hW y
theorem

finitePlaceNormRawArtin_naturality

L648 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormRawArtin_naturality
Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
theorem finitePlaceNormRawArtin_naturality
    [NumberField L]
    (hW : finitePlaceBelow (K := K) W = v)
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w)
    (y : Dₙˣ) :
    finitePlaceCrossLocalRestrictionMonoidHom
        (K := K) (L := L) (K' := K') (L' := L')
        v W hW w w' hcentres
        (finitePlaceNormUpperRawArtin
          (K' := K') (L' := L') W w' y) =
      finitePlaceNormLowerRawArtin
        (K := K) (L := L) (K' := K')
        v W w hW y
theorem

finitePlaceNormLocalizedArtin_naturality

L721 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormLocalizedArtin_naturality
Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
theorem finitePlaceNormLocalizedArtin_naturality
    [NumberField L]
    (hW : finitePlaceBelow (K := K) W = v)
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w)
    (y : Dₙˣ) :
    finitePlaceNormRestrictedArtin
        (K := K) (L := L) (K' := K') (L' := L')
        v W w w' hW hcentres y =
      finitePlaceNormLowerArtin
        (K := K) (L := L) (K' := K')
        v W w hW y
theorem

finitePlaceLocalArtinMonoidHom_norm_restriction_localized

L766 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinMonoidHom_norm_restriction_localized
Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · statement
theorem
    finitePlaceLocalArtinMonoidHom_norm_restriction_localized
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [NumberField L]
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v)
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w)
    (y : (finitePlaceNormCompletion K' W)ˣ) :
    finitePlaceCrossLocalRestrictionMonoidHom
        (K := K) (L := L) (K' := K') (L' := L')
        v W hW w w' hcentres
        (finitePlaceLocalArtinMonoidHom
          (K := K') (L := L') W w'
          (finitePlaceCompletionUnitsContinuousMulEquiv W y)) =
      finitePlaceLocalArtinMonoidHom
        (K := K) (L := L) v w
        (finitePlaceCompletionUnitsContinuousMulEquiv v
          (finitePlaceRelativeNormUnits
            (K := K) (K' := K') v W hW y))
theorem

finitePlaceLocalArtinMonoidHom_norm_restriction

L819 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinMonoidHom_norm_restriction
Documentation

The local Artin maps attached to specified finite places commute with the norm between their concrete adic completions.

Source context 48 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
section FinitePlaceNormRestrictionInstances
variable {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
local notation "vKₙ" =>
  NumberField.HeightOneSpectrum.adicAbv K v
local notation "vKₙ'" =>
  NumberField.HeightOneSpectrum.adicAbv K' W
local notation "Cₙ" =>
  finitePlaceNormCompletion K v
local notation "Dₙ" =>
  finitePlaceNormCompletion K' W
local notation "Eₙ" =>
  finitePlaceNormLocalizedCompletion K L v w
local notation "Eₙ'" =>
  finitePlaceNormLocalizedCompletion K' L' W w'
local instance finitePlaceNormLowerExtensionAlgebra :
    Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K) w.1
local instance finitePlaceNormLowerExtensionSMul :
    SMul K w.1.Completion :=
  (finitePlaceNormLowerExtensionAlgebra v w).toSMul
local instance finitePlaceNormLowerCompletionAlgebra :
    Algebra Cₙ w.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ w.1 w.2
local instance finitePlaceNormLowerGlobalAlgebra :
    Algebra K Eₙ :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ w
local instance finitePlaceNormUpperExtensionAlgebra :
    Algebra K' w'.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra
    (K := K') w'.1
local instance finitePlaceNormUpperExtensionSMul :
    SMul K' w'.1.Completion :=
  (finitePlaceNormUpperExtensionAlgebra W w').toSMul
local instance finitePlaceNormUpperCompletionAlgebra :
    Algebra Dₙ w'.1.Completion :=
  AbsoluteValue.completionAlgebra vKₙ' w'.1 w'.2
local instance finitePlaceNormUpperGlobalAlgebra :
    Algebra K' Eₙ' :=
  LocalClassFieldTheory.localizedCompletionGlobalAlgebra vKₙ' w'
local instance finitePlaceNormLowerNontriviallyNormedField :
    NontriviallyNormedField Cₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ (RayClass.adicAbv_isNontrivial v)
local instance finitePlaceNormLowerLocallyCompactSpace :
    LocallyCompactSpace Cₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry v)
local instance finitePlaceNormUpperNontriviallyNormedField :
    NontriviallyNormedField Dₙ :=
  absoluteValueExtension_completionNontriviallyNormedField
    vKₙ' (RayClass.adicAbv_isNontrivial W)
local instance finitePlaceNormUpperLocallyCompactSpace :
    LocallyCompactSpace Dₙ :=
  AbsoluteValue.Completion.locallyCompactSpace
    (finitePlaceCompletionBaseMap_isometry W)
local instance finitePlaceNormLowerLocalizedFiniteDimensional :
    FiniteDimensional Cₙ Eₙ :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormLowerLocalizedAbelianGalois :
    IsAbelianGalois Cₙ Eₙ :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ (RayClass.adicAbv_isNontrivial v) w
local instance finitePlaceNormUpperLocalizedFiniteDimensional :
    FiniteDimensional Dₙ Eₙ' :=
  AlgebraicNumberTheory.Valuations.localizedCompletionModuleFinite
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormUpperLocalizedAbelianGalois :
    IsAbelianGalois Dₙ Eₙ' :=
  LocalClassFieldTheory.localizedCompletion_isAbelianGalois
    vKₙ' (RayClass.adicAbv_isNontrivial W) w'
local instance finitePlaceNormLowerUltrametric :
    IsUltrametricDist Cₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValued :
    Valued Cₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationNontrivial :
    (Valued.v : Valuation Cₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Cₙ)).IsNontrivial)
local instance finitePlaceNormLowerValuativeRel :
    ValuativeRel Cₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormLowerValuationCompatible :
    (Valued.v : Valuation Cₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Cₙ ℝ≥0)
local instance finitePlaceNormLowerValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Cₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Cₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormLowerLocalField :
    IsNonarchimedeanLocalField Cₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K v)
local instance finitePlaceNormUpperUltrametric :
    IsUltrametricDist Dₙ :=
  finitePlaceArtinCompletionIsUltrametricDist vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValued :
    Valued Dₙ ℝ≥0 :=
  finitePlaceArtinCompletionValued vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationNontrivial :
    (Valued.v : Valuation Dₙ ℝ≥0).IsNontrivial :=
  (inferInstance :
    (NormedField.valuation (K := Dₙ)).IsNontrivial)
local instance finitePlaceNormUpperValuativeRel :
    ValuativeRel Dₙ :=
  finitePlaceArtinCompletionValuativeRel vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
local instance finitePlaceNormUpperValuationCompatible :
    (Valued.v : Valuation Dₙ ℝ≥0).Compatible :=
  Valuation.Compatible.ofValuation
    (Valued.v : Valuation Dₙ ℝ≥0)
local instance finitePlaceNormUpperValuativeRelNontrivial :
    ValuativeRel.IsNontrivial Dₙ :=
  (ValuativeRel.isNontrivial_iff_isNontrivial
    (Valued.v : Valuation Dₙ ℝ≥0)).2 inferInstance
local instance finitePlaceNormUpperLocalField :
    IsNonarchimedeanLocalField Dₙ :=
  finitePlaceArtinCompletionIsNonarchimedeanLocalField vKₙ'
    (NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv K' W)
Lean source · full declaration
theorem finitePlaceLocalArtinMonoidHom_norm_restriction
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [NumberField L]
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v)
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
    (hcentres :
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w)
    (x : (W.adicCompletion K')ˣ) :
    letI : Algebra (v.adicCompletion K) (W.adicCompletion K') :=
      (finitePlaceAdicCompletionMap
        K K' v ⟨W, hW⟩).toAlgebra
    finitePlaceCrossLocalRestrictionMonoidHom
        (K := K) (L := L) (K' := K') (L' := L')
        v W hW w w' hcentres
        (finitePlaceLocalArtinMonoidHom
          (K := K') (L := L') W w' x) =
      finitePlaceLocalArtinMonoidHom
        (K := K) (L := L) v w
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.adicCompletion K') x) := by
  let vK := NumberField.HeightOneSpectrum.adicAbv K v
  let vK' := NumberField.HeightOneSpectrum.adicAbv K' W
  let C := vK.Completion
  let D := vK'.Completion
  let eCUnits :
      Cˣ ≃* (v.adicCompletion K)ˣ :=
    finitePlaceCompletionUnitsContinuousMulEquiv v
  let eDUnits :
      Dˣ ≃* (W.adicCompletion K')ˣ :=
    finitePlaceCompletionUnitsContinuousMulEquiv W
  let : Algebra (v.adicCompletion K) (W.adicCompletion K') :=
    (finitePlaceAdicCompletionMap
      K K' v ⟨W, hW⟩).toAlgebra
  let : Algebra C D :=
    (finitePlaceArtinRelativeCompletionRingHom
      (K := K) (K' := K') v W hW).toAlgebra
  calc
    finitePlaceCrossLocalRestrictionMonoidHom
        (K := K) (L := L) (K' := K') (L' := L')
        v W hW w w' hcentres
        (finitePlaceLocalArtinMonoidHom
          (K := K') (L := L') W w' x) =
      finitePlaceLocalArtinMonoidHom
        (K := K) (L := L) v w
        (eCUnits
          (finitePlaceRelativeNormUnits
            (K := K) (K' := K') v W hW
            (eDUnits.symm x))) :=
      by
        have h :=
          finitePlaceLocalArtinMonoidHom_norm_restriction_localized
            (K := K) (L := L) (K' := K') (L' := L')
            v W hW w w' hcentres (eDUnits.symm x)
        change
          finitePlaceCrossLocalRestrictionMonoidHom
              (K := K) (L := L) (K' := K') (L' := L')
              v W hW w w' hcentres
              (finitePlaceLocalArtinMonoidHom
                (K := K') (L := L') W w'
                (eDUnits (eDUnits.symm x))) =
            finitePlaceLocalArtinMonoidHom
              (K := K) (L := L) v w
              (eCUnits
                (finitePlaceRelativeNormUnits
                  (K := K) (K' := K') v W hW
                  (eDUnits.symm x))) at h
        rw [eDUnits.apply_symm_apply] at h
        exact h
    _ =
      finitePlaceLocalArtinMonoidHom
        (K := K) (L := L) v w
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.adicCompletion K') x) :=
      congrArg
        (finitePlaceLocalArtinMonoidHom
          (K := K) (L := L) v w)
        (finitePlaceArtinConcreteNormUnits
          (K := K) (K' := K') v W hW x)
theorem

finitePlaceArtinMonoidHomOfExtension_norm_restriction

L917 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceArtinMonoidHomOfExtension_norm_restriction
Documentation

The local Artin map attached to specified finite places carries a local norm to the restriction of the upper Artin element.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
theorem
    finitePlaceArtinMonoidHomOfExtension_norm_restriction
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v)
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K' W) L')
    (hcentres :
      letI : NumberField L :=
        NumberField.of_module_finite K L
      finitePlaceBelow (K := L)
          (finitePlaceExtensionCentre
            (K := K') (L := L') W w') =
        finitePlaceExtensionCentre
          (K := K) (L := L) v w) :
    letI : Algebra (v.adicCompletion K) (W.adicCompletion K') :=
      (finitePlaceAdicCompletionMap
        K K' v ⟨W, hW⟩).toAlgebra
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (finitePlaceArtinMonoidHomOfExtension
          (K := K') (L := L') W w') =
      (finitePlaceArtinMonoidHomOfExtension
        (K := K) (L := L) v w).comp
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.adicCompletion K')) := by
  let : NumberField L := NumberField.of_module_finite K L
  let : Algebra (v.adicCompletion K) (W.adicCompletion K') :=
    (finitePlaceAdicCompletionMap
      K K' v ⟨W, hW⟩).toAlgebra
  let globalRestriction :
      (L' ≃ₐ[K'] L') →* (L ≃ₐ[K] L) :=
    (AlgEquiv.restrictNormalHom L).comp
      (AlgEquiv.restrictScalarsHom K)
  let localUpper :=
    finitePlaceLocalArtinMonoidHom
      (K := K') (L := L') W w'
  let localLower :=
    finitePlaceLocalArtinMonoidHom
      (K := K) (L := L) v w
  let localRestriction :=
    finitePlaceCrossLocalRestrictionMonoidHom
      (K := K) (L := L) (K' := K') (L' := L')
      v W hW w w' hcentres
  let norm :=
    LocalFieldTheory.normUnits
      (v.adicCompletion K) (W.adicCompletion K')
  calc
    globalRestriction.comp
        (finitePlaceArtinMonoidHomOfExtension
          (K := K') (L := L') W w') =
      globalRestriction.comp
        ((finitePlaceLocalToGlobalMonoidHom
          (K := K') (L := L') W w').comp localUpper) :=
      congrArg
        (fun f => globalRestriction.comp f)
        (finitePlaceArtinMonoidHomOfExtension_factor
          (K := K') (L := L') W w')
    _ =
        (globalRestriction.comp
          (finitePlaceLocalToGlobalMonoidHom
            (K := K') (L := L') W w')).comp localUpper := by
      rfl
    _ =
        ((finitePlaceLocalToGlobalMonoidHom
          (K := K) (L := L) v w).comp
          localRestriction).comp localUpper :=
      congrArg
        (fun f :
            finitePlaceNormLocalizedAut K' L' W w' →*
              (L ≃ₐ[K] L) =>
          f.comp localUpper)
        (by
          apply MonoidHom.ext
          intro tau
          exact
            finitePlaceCrossDecompositionTransport
              (K := K) (L := L) (K' := K') (L' := L')
              v W hW w w' hcentres tau)
    _ =
        (finitePlaceLocalToGlobalMonoidHom
          (K := K) (L := L) v w).comp
          (localRestriction.comp localUpper) := by
      rfl
    _ =
        (finitePlaceLocalToGlobalMonoidHom
          (K := K) (L := L) v w).comp
          (localLower.comp norm) :=
      congrArg
        (fun f => (finitePlaceLocalToGlobalMonoidHom
          (K := K) (L := L) v w).comp f)
        (by
          apply MonoidHom.ext
          intro x
          exact
            finitePlaceLocalArtinMonoidHom_norm_restriction
              (K := K) (L := L) (K' := K') (L' := L')
              v W hW w w' hcentres x)
    _ =
        ((finitePlaceLocalToGlobalMonoidHom
          (K := K) (L := L) v w).comp localLower).comp norm := by
      rfl
    _ =
        (finitePlaceArtinMonoidHomOfExtension
          (K := K) (L := L) v w).comp norm :=
      congrArg
        (fun f => f.comp norm)
        (finitePlaceArtinMonoidHomOfExtension_factor
          (K := K) (L := L) v w).symm
theorem

chosenFinitePlaceArtinMonoidHom_norm_restriction

L1040 ↗
GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceArtinMonoidHom_norm_restriction
Documentation

Finite-place norm--restriction compatibility. Restriction of the upper local Artin factor is the lower local Artin factor after the norm between the corresponding concrete adic completions.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
theorem chosenFinitePlaceArtinMonoidHom_norm_restriction
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (W : HeightOneSpectrum (𝓞 K')) :
    let v := finitePlaceBelow (K := K) W
    letI : Algebra (v.adicCompletion K) (W.adicCompletion K') :=
      (finitePlaceAdicCompletionMap
        K K' v ⟨W, rfl⟩).toAlgebra
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (chosenFinitePlaceArtinMonoidHom
          (K := K') (L := L') W) =
      (chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v).comp
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.adicCompletion K')) := by
  let : NumberField L := NumberField.of_module_finite K L
  dsimp only
  let v :=
    finitePlaceBelow (K := K) W
  let w' :=
    chosenFinitePlaceExtension
      (L := L') W
  let U' :=
    finitePlaceExtensionCentre
      (K := K') (L := L') W w'
  let U :=
    finitePlaceBelow (K := L) U'
  have hUK : finitePlaceBelow (K := K) U = v := by
    calc
      finitePlaceBelow (K := K) U =
          finitePlaceBelow (K := K) U' := by
        exact
          finitePlaceBelow_finitePlaceBelow
            (K := K) (M := L) (L := L') U'
      _ =
          finitePlaceBelow (K := K)
            (finitePlaceBelow (K := K') U') := by
        symm
        exact
          finitePlaceBelow_finitePlaceBelow
            (K := K) (M := K') (L := L') U'
      _ = finitePlaceBelow (K := K) W := by
        rw [
          finitePlaceBelow_finitePlaceExtensionCentre
            (K := K') (L := L') W w']
      _ = v := rfl
  let Uv :
      {Q : HeightOneSpectrum (𝓞 L) //
        finitePlaceBelow (K := K) Q = v} :=
    ⟨U, hUK⟩
  let w :
      AbsoluteValueExtension
        (NumberField.HeightOneSpectrum.adicAbv K v) L :=
    (finitePlaceExtensionEquivAbove
      (K := K) (L := L) v).symm Uv
  have hwCentre :
      finitePlaceExtensionCentre
          (K := K) (L := L) v w = U := by
    have h :=
      congrArg Subtype.val
        ((finitePlaceExtensionEquivAbove
          (K := K) (L := L) v).apply_symm_apply Uv)
    simpa only [
      finitePlaceExtensionEquivAbove_coe
    ] using h
  let : Algebra (v.adicCompletion K) (W.adicCompletion K') :=
    (finitePlaceAdicCompletionMap
      K K' v ⟨W, rfl⟩).toAlgebra
  calc
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (chosenFinitePlaceArtinMonoidHom
          (K := K') (L := L') W) =
      (finitePlaceArtinMonoidHomOfExtension
        (K := K) (L := L) v w).comp
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.adicCompletion K')) := by
      exact
        finitePlaceArtinMonoidHomOfExtension_norm_restriction
          (K := K) (L := L) v W rfl w w'
          (by
            change
              finitePlaceBelow (K := L) U' =
                finitePlaceExtensionCentre
                  (K := K) (L := L) v w
            rw [hwCentre])
    _ =
      (chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v).comp
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.adicCompletion K')) := by
      change
        (finitePlaceArtinMonoidHomOfExtension
          (K := K) (L := L) v w).comp
            (LocalFieldTheory.normUnits
              (v.adicCompletion K) (W.adicCompletion K')) =
          (finitePlaceArtinMonoidHomOfExtension
            (K := K) (L := L) v
              (chosenFinitePlaceExtension
                (L := L) v)).comp
            (LocalFieldTheory.normUnits
              (v.adicCompletion K) (W.adicCompletion K'))
      exact congrArg
        (fun f : (v.adicCompletion K)ˣ →* (L ≃ₐ[K] L) =>
          f.comp
            (LocalFieldTheory.normUnits
              (v.adicCompletion K) (W.adicCompletion K')))
        (finitePlaceArtinMonoidHomOfExtension_eq
          (K := K) (L := L) v w
          (chosenFinitePlaceExtension
            (L := L) v))
theorem

chosenFinitePlaceArtinMonoidHom_norm_restriction_of_below_eq

L1162 ↗
GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceArtinMonoidHom_norm_restriction_of_below_eq
Documentation

Finite-place norm--restriction with the lower place supplied explicitly. This form keeps the equality proof in the completion algebra and avoids dependent elimination through adic-completion types.

Source context 10 commands

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

open scoped IsMulCommutative NNReal NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
theorem chosenFinitePlaceArtinMonoidHom_norm_restriction_of_below_eq
    {K' L' : Type}
    [Field K'] [NumberField K']
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K' L'] [Algebra K L']
    [IsScalarTower K K' L']
    [Algebra L L'] [IsScalarTower K L L']
    [IsAbelianGalois K' L']
    (v : HeightOneSpectrum (𝓞 K))
    (W : HeightOneSpectrum (𝓞 K'))
    (hW : finitePlaceBelow (K := K) W = v) :
    letI : Algebra (v.adicCompletion K) (W.adicCompletion K') :=
      (finitePlaceAdicCompletionMap
        K K' v ⟨W, hW⟩).toAlgebra
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K)).comp
        (chosenFinitePlaceArtinMonoidHom
          (K := K') (L := L') W) =
      (chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v).comp
        (LocalFieldTheory.normUnits
          (v.adicCompletion K) (W.adicCompletion K')) := by
  subst v
  exact
    chosenFinitePlaceArtinMonoidHom_norm_restriction
      (K := K) (L := L) (K' := K') (L' := L') W

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