Module

Factorization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.LocalGlobalArtinCompatibility.Factorization

18 declarations indexed from sourceView source ↗

Module documentation

Factorization of the global Artin map through local Artin maps

This module completes the auxiliary-field argument, factors the global norm-residue map through each local Artin quotient, and proves the finite-place local-global compatibility theorem.

Imports2

Imported by9

theorem

numberFieldTowerFiniteQuotientCoordinate_mem_primary

L45 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteQuotientCoordinate_mem_primary

Documentation

The finite quotient coordinate remains primary after transport to the relative Galois group.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem numberFieldTowerFiniteQuotientCoordinate_mem_primary
    (p : Nat.Primes) (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (σ' : Gal(L/K))
    (hτσ :
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          (numberFieldTowerFiniteQuotientCoordinate
            (K := K) (L := L) τ) = σ')
    (hprimary :
      σ' ∈ CommGroup.primaryComponent (Gal(L/K)) p.1) :
    numberFieldTowerFiniteQuotientCoordinate
        (K := K) (L := L) τ ∈
      CommGroup.primaryComponent
        ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
        p.1

theorem

exists_finitePlacePrimary_localGlobalRepresentative

L81 ↗

GlobalClassFieldTheory.Reciprocity.exists_finitePlacePrimary_localGlobalRepresentative

Documentation

The cyclotomic auxiliary-field construction supplies a local representative on which the local and global Artin values agree.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem exists_finitePlacePrimary_localGlobalRepresentative
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (σ :
      absoluteValueDecompositionGroup K
        (chosenFinitePlaceExtension (L := L) v).1)
    (hgenerate :
      Subgroup.closure
          ({σ.1} : Set (Gal(L/K))) =
        ⊤)
    (hprimary :
      σ.1 ∈
        CommGroup.primaryComponent
          (Gal(L/K)) p.1) :
    ∃ z : (v.adicCompletion K)ˣ,
      chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v z = σ.1 ∧
      globalNormResidueMonoidHom K L
          (IdeleGroup.finitePlaceIdeleClass v z) = σ.1

theorem

chosenFinitePlaceArtinMonoidHom_eq_one_iff_chosenLocalNorm

L137 ↗

GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceArtinMonoidHom_eq_one_iff_chosenLocalNorm

Documentation

Triviality of the actual chosen finite-place Artin symbol is equivalent to membership in the actual chosen local norm subgroup.

Source context 13 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField L] in

Lean source · statement

theorem chosenFinitePlaceArtinMonoidHom_eq_one_iff_chosenLocalNorm
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v x = 1 ↔
      x ∈ chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v

theorem

globalNormResidueMonoidHom_finitePlaceIdeleClass_eq_one_of_localArtin_eq_one

L153 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_finitePlaceIdeleClass_eq_one_of_localArtin_eq_one

Documentation

A finite-place element killed by the actual local Artin homomorphism is also killed by the global norm-residue homomorphism after insertion as a one-place idele class.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHom_finitePlaceIdeleClass_eq_one_of_localArtin_eq_one
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ)
    (hx :
      chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v x = 1) :
    globalNormResidueMonoidHom K L
        (IdeleGroup.finitePlaceIdeleClass v x) = 1

theorem

chosenFinitePlaceLocalNormSubgroup_le_globalNormResidueKernel

L171 ↗

GlobalClassFieldTheory.Reciprocity.chosenFinitePlaceLocalNormSubgroup_le_globalNormResidueKernel

Documentation

The chosen local norm subgroup lies in the kernel of the global norm-residue homomorphism restricted to the one-place finite idele class map.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem chosenFinitePlaceLocalNormSubgroup_le_globalNormResidueKernel
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v ≤
      ((globalNormResidueMonoidHom K L).comp
        (IdeleGroup.finitePlaceIdeleClass v)).ker

theorem

globalNormResidue_finitePlaceIdeleClass_eq_of_localArtin_eq

L191 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidue_finitePlaceIdeleClass_eq_of_localArtin_eq

Documentation

The restriction of the global norm-residue homomorphism to one finite-place idele class depends only on the corresponding local Artin symbol.

This is the exact quotient step used in the prime-primary reduction: the already proved inclusion of the local norm subgroup in the global norm kernel makes the value independent of the chosen local preimage.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidue_finitePlaceIdeleClass_eq_of_localArtin_eq
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (x y : (v.adicCompletion K)ˣ)
    (hxy :
      chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v x =
        chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v y) :
    globalNormResidueMonoidHom K L
        (IdeleGroup.finitePlaceIdeleClass v x) =
      globalNormResidueMonoidHom K L
        (IdeleGroup.finitePlaceIdeleClass v y)

theorem

globalNormResidueMonoidHom_finitePlaceIdeleClass_eq_of_primary_generator

L228 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_finitePlaceIdeleClass_eq_of_primary_generator

Documentation

Finite-place local--global compatibility for a p-primary decomposition automorphism which generates the whole relative Galois group. The auxiliary-field construction is isolated in an opaque representative lemma, so consumers only see this short quotient step.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem
    globalNormResidueMonoidHom_finitePlaceIdeleClass_eq_of_primary_generator
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (σ :
      absoluteValueDecompositionGroup K
        (chosenFinitePlaceExtension (L := L) v).1)
    (hgenerate :
      Subgroup.closure ({σ.1} : Set (Gal(L/K))) = ⊤)
    (hprimary :
      σ.1 ∈ CommGroup.primaryComponent (Gal(L/K)) p.1)
    (x : (v.adicCompletion K)ˣ)
    (hx :
      chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v x = σ.1) :
    globalNormResidueMonoidHom K L
        (IdeleGroup.finitePlaceIdeleClass v x) = σ.1

def

finitePlaceGlobalNormResidueFactor

L258 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceGlobalNormResidueFactor

Documentation

The global norm-residue symbol at one finite place, factored through the actual image of the chosen local Artin homomorphism.

The definition uses a preimage only to specify the value. Its well-definedness and multiplicativity are consequences of the genuine one-place norm-kernel theorem above.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

def finitePlaceGlobalNormResidueFactor
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    (chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v).range →*
      (L ≃ₐ[K] L)

theorem

finitePlaceGlobalNormResidueFactor_comp_rangeRestrict

L282 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceGlobalNormResidueFactor_comp_rangeRestrict

Documentation

Factoring and then evaluating the actual local Artin symbol gives the original one-place global norm-residue value.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem finitePlaceGlobalNormResidueFactor_comp_rangeRestrict
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    (finitePlaceGlobalNormResidueFactor
        (K := K) (L := L) v).comp
        (chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v).rangeRestrict =
      (globalNormResidueMonoidHom K L).comp
        (IdeleGroup.finitePlaceIdeleClass v)

theorem

globalNormResidueMonoidHomOfEmbedding_norm_restriction_apply

L317 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHomOfEmbedding_norm_restriction_apply

Documentation

Pointwise norm/restriction naturality, with the coercion from the homomorphism equality normalized once outside the descent construction.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHomOfEmbedding_norm_restriction_apply
    (K K' L L' : Type)
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L]
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K L] [Algebra K L']
    [Algebra K' L'] [Algebra L L']
    [IsScalarTower K K' L'] [IsScalarTower K L L']
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L']
    [FiniteDimensional K K'] [IsGalois K K']
    (j : L' →ₐ[ℚ] SeparableClosure ℚ)
    (c : IdeleClassGroup K') :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K))
          (globalNormResidueMonoidHomOfEmbedding K' L' j c) =
      globalNormResidueMonoidHomOfEmbedding K L
        (j.comp (IsScalarTower.toAlgHom ℚ L L'))
        (_root_.ideleClassNorm K K' c)

opaque

exists_finitePlaceNormDescent_localGlobalRepresentative

L346 ↗

GlobalClassFieldTheory.Reciprocity.exists_finitePlaceNormDescent_localGlobalRepresentative

Documentation

Norming one upper representative down a finite Galois base-change transports both its chosen local Artin value and its global norm-residue value. All fields and places are explicit here, so no constructed fixed-field tower occurs in the declaration type.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

opaque exists_finitePlaceNormDescent_localGlobalRepresentative
    {M : Type}
    [Field M] [NumberField M]
    [Algebra K M] [FiniteDimensional K M] [IsGalois K M]
    [Algebra M L] [FiniteDimensional M L] [IsAbelianGalois M L]
    [IsScalarTower K M L]
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (W : IsDedekindDomain.HeightOneSpectrum (𝓞 M))
    (hWbelow : finitePlaceBelow (K := K) W = v)
    (σM : Gal(L/M)) (σG : Gal(L/K))
    (hrestrict :
      ((AlgEquiv.restrictNormalHom L).comp
          (AlgEquiv.restrictScalarsHom K)) σM = σG)
    (y : (W.adicCompletion M)ˣ)
    (hy :
      chosenFinitePlaceArtinMonoidHom
          (K := M) (L := L) W y = σM)
    (hglobalM :
      globalNormResidueMonoidHom M L
          (IdeleGroup.finitePlaceIdeleClass W y) = σM) :
    ∃ z : (v.adicCompletion K)ˣ,
      chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v z = σG ∧
      globalNormResidueMonoidHom K L
          (IdeleGroup.finitePlaceIdeleClass v z) = σG

opaque

exists_finitePlacePrimaryNormDescent_localGlobalRepresentative

L473 ↗

GlobalClassFieldTheory.Reciprocity.exists_finitePlacePrimaryNormDescent_localGlobalRepresentative

Documentation

A primary generator at an explicit upper place can first be realized by the auxiliary construction and then normed through an explicit base change. This short bridge keeps the auxiliary witness out of the cyclic-fixed-field construction.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

opaque exists_finitePlacePrimaryNormDescent_localGlobalRepresentative
    {M : Type}
    [Field M] [NumberField M]
    [Algebra K M] [FiniteDimensional K M] [IsGalois K M]
    [Algebra M L] [FiniteDimensional M L] [IsAbelianGalois M L]
    [IsScalarTower K M L]
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (W : IsDedekindDomain.HeightOneSpectrum (𝓞 M))
    (hWbelow : finitePlaceBelow (K := K) W = v)
    (p : Nat.Primes)
    (δM :
      absoluteValueDecompositionGroup M
        (chosenFinitePlaceExtension (L := L) W).1)
    (hgenerate :
      Subgroup.closure ({δM.1} : Set (Gal(L/M))) = ⊤)
    (hprimary :
      δM.1 ∈ CommGroup.primaryComponent (Gal(L/M)) p.1)
    (σG : Gal(L/K))
    (hrestrict :
      ((AlgEquiv.restrictNormalHom L).comp
          (AlgEquiv.restrictScalarsHom K)) δM.1 = σG) :
    ∃ z : (v.adicCompletion K)ˣ,
      chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v z = σG ∧
      globalNormResidueMonoidHom K L
          (IdeleGroup.finitePlaceIdeleClass v z) = σG

opaque

exists_finitePlacePrimary_cyclicFixedFieldRepresentative

L510 ↗

GlobalClassFieldTheory.Reciprocity.exists_finitePlacePrimary_cyclicFixedFieldRepresentative

Documentation

Cyclic fixed-field descent turns a primary decomposition automorphism into a lower representative without exposing the constructed field tower in the declaration type.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

opaque exists_finitePlacePrimary_cyclicFixedFieldRepresentative
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (δ :
      absoluteValueDecompositionGroup K
        (chosenFinitePlaceExtension (L := L) v).1)
    (hprimary :
      δ.1 ∈ CommGroup.primaryComponent (Gal(L/K)) p.1) :
    ∃ z : (v.adicCompletion K)ˣ,
      chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v z = δ.1 ∧
      globalNormResidueMonoidHom K L
          (IdeleGroup.finitePlaceIdeleClass v z) = δ.1

theorem

finitePlaceGlobalNormResidueFactor_eq_subtype_on_primary

L582 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceGlobalNormResidueFactor_eq_subtype_on_primary

Documentation

On every primary component of the actual decomposition-group image, the one-place global norm-residue factor is the tautological inclusion. An arbitrary primary element is reduced to the cyclic extension cut out by that element, where the auxiliary-field theorem above applies to its genuine generator.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem finitePlaceGlobalNormResidueFactor_eq_subtype_on_primary
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K))
    (p : ℕ) (hp : Fact p.Prime)
    (σ :
      CommGroup.primaryComponent
        (chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v).range p) :
    finitePlaceGlobalNormResidueFactor
        (K := K) (L := L) v σ =
      (σ :
        (chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v).range)

theorem

globalNormResidueMonoidHom_comp_finitePlaceIdeleClass_iff

L657 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_comp_finitePlaceIdeleClass_iff

Documentation

The desired finite-place local--global compatibility is equivalent to saying that the factor induced on the actual decomposition-group image is its inclusion into the global Galois group.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHom_comp_finitePlaceIdeleClass_iff
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    (globalNormResidueMonoidHom K L).comp
          (IdeleGroup.finitePlaceIdeleClass v) =
        chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v ↔
      finitePlaceGlobalNormResidueFactor
          (K := K) (L := L) v =
        (chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v).range.subtype

theorem

finitePlaceGlobalNormResidueFactor_eq_subtype_iff_primary

L721 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceGlobalNormResidueFactor_eq_subtype_iff_primary

Documentation

Equality of the induced decomposition-group map with the inclusion is characterized by equality on every primary component. This is the exact finite-group reduction in the proof of finite-place local--global compatibility.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem finitePlaceGlobalNormResidueFactor_eq_subtype_iff_primary
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    finitePlaceGlobalNormResidueFactor
          (K := K) (L := L) v =
        (chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v).range.subtype ↔
      ∀ (p : ℕ) (_hp : Fact p.Prime)
        (σ :
          CommGroup.primaryComponent
            (chosenFinitePlaceArtinMonoidHom
              (K := K) (L := L) v).range p),
        finitePlaceGlobalNormResidueFactor
            (K := K) (L := L) v σ =
          (σ :
            (chosenFinitePlaceArtinMonoidHom
              (K := K) (L := L) v).range)

theorem

finitePlaceGlobalNormResidueFactor_eq_subtype

L752 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceGlobalNormResidueFactor_eq_subtype

Documentation

The factor of the one-place global norm-residue map through the actual local Artin image is exactly the inclusion of that decomposition subgroup into the global Galois group.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem finitePlaceGlobalNormResidueFactor_eq_subtype
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    finitePlaceGlobalNormResidueFactor
          (K := K) (L := L) v =
        (chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v).range.subtype

theorem

globalNormResidueMonoidHom_comp_finitePlaceIdeleClass

L768 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_comp_finitePlaceIdeleClass

Documentation

The global norm-residue symbol restricted to a genuine one-place finite idele class is the actual chosen local Artin symbol.

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open CyclicCohomology
open KummerTheory
attribute [local instance]
  finitePadicAuxiliaryExtensionQuotientIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalNormResidueMonoidHom_comp_finitePlaceIdeleClass
    (v : IsDedekindDomain.HeightOneSpectrum (𝓞 K)) :
    (globalNormResidueMonoidHom K L).comp
          (IdeleGroup.finitePlaceIdeleClass v) =
        chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v

Module documentation

Factorization of the global Artin map through local Artin maps

Declarations