This file contains the final comparison step in the proof of the local reciprocity law. Once the actual absolute-Galois datum, henselian valuation, and class-field axiom have been constructed, the abstract reciprocity theorem is transported through the concrete finite Galois realization in a separable closure and through the actual field norm.
The coefficient module remains (SeparableClosure K)ˣ; this is essential in imperfect positive characteristic.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]abbrev G (K : Type) [Field K]Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]abbrev A (K : Type) [Field K] : Rep ℤ (G K)Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]abbrev B (K : Type) [Field K] : ClosedSubgroup (G K)Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]instance intrinsicAbsoluteGaloisT2 : T2Space (G K)The finite abstract extension object determined by an explicit embedding of L into the fixed separable closure.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]def finiteGaloisAbstractExtensionOfEmbedding
(i : L →ₐ[K] SeparableClosure K) : FiniteGaloisSubextension (B K) where
field := finiteGaloisClosedFixingSubgroupOfEmbedding K L i
below := fixingSubgroupLeBase K (SeparableClosure K)
(finiteGaloisFieldRangeOfEmbedding K L i)
normal := inferInstance
finite := baseFixingExtensionQuotient_finite K (SeparableClosure K)
(finiteGaloisFieldRangeOfEmbedding K L i)The concrete realization of L/K as the finite Galois extension object to which the abstract reciprocity theorem is applied.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]def finiteGaloisAbstractExtension : FiniteGaloisSubextension (B K)The additive reciprocity equivalence transported through an explicit realization of L/K in the separable closure.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]def concreteReciprocityAddEquivOfEmbedding
(i : L →ₐ[K] SeparableClosure K)
(D : DegreeData (G K)) (v : ValuationData D (A K))
(hcf : SatisfiesClassFieldAxiom (A K)) :
Additive (Abelianization Gal(L / K)) ≃+
Additive (NormQuotient K L)Multiplicative form of reciprocity transported through an explicit embedding.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]def concreteReciprocityEquivOfEmbedding
(i : L →ₐ[K] SeparableClosure K)
(D : DegreeData (G K)) (v : ValuationData D (A K))
(hcf : SatisfiesClassFieldAxiom (A K)) :
Abelianization Gal(L / K) ≃* NormQuotient K LNorm-residue symbol obtained from an explicit separable-closure realization.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]def concreteNormResidueSymbolOfEmbedding
(i : L →ₐ[K] SeparableClosure K)
(D : DegreeData (G K)) (v : ValuationData D (A K))
(hcf : SatisfiesClassFieldAxiom (A K)) :
Kˣ →* Abelianization Gal(L / K)The additive form of the concrete reciprocity isomorphism. The inputs are the three genuine structures constructed in the preceding part of the proof, not additional reciprocity hypotheses.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]def concreteReciprocityAddEquiv
(D : DegreeData (G K)) (v : ValuationData D (A K))
(hcf : SatisfiesClassFieldAxiom (A K)) :
Additive (Abelianization Gal(L / K)) ≃+
Additive (NormQuotient K L)The public multiplicative form of the transported reciprocity isomorphism G(L/K)ᵃᵇ ≃ Kˣ/N_{L/K}Lˣ.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]def concreteReciprocityEquiv
(D : DegreeData (G K)) (v : ValuationData D (A K))
(hcf : SatisfiesClassFieldAxiom (A K)) :
Abelianization Gal(L / K) ≃* NormQuotient K LThe local norm-residue symbol obtained by inverting reciprocity and precomposing with the quotient map on Kˣ.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]def concreteNormResidueSymbol
(D : DegreeData (G K)) (v : ValuationData D (A K))
(hcf : SatisfiesClassFieldAxiom (A K)) :
Kˣ →* Abelianization Gal(L / K)The local norm-residue symbol is onto.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]theorem concreteNormResidueSymbol_surjective
(D : DegreeData (G K)) (v : ValuationData D (A K))
(hcf : SatisfiesClassFieldAxiom (A K)) :
Function.Surjective (concreteNormResidueSymbol K L D v hcf)The kernel of the local norm-residue symbol is exactly the field norm subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsGalois K L]theorem concreteNormResidueSymbol_ker
(D : DegreeData (G K)) (v : ValuationData D (A K))
(hcf : SatisfiesClassFieldAxiom (A K)) :
(concreteNormResidueSymbol K L D v hcf).ker = localNormSubgroup K L