ModuleMainFiniteReciprocity.lean
Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.MainFiniteReciprocity
35 declarations indexed from sourceView source ↗ Module documentation
The abstract reciprocity construction, the finite reciprocity equivalence
This file carries out the descent preparation. The reciprocity value on the Frobenius semigroup is first mapped to the finite norm quotient. We then compare two lifts by their positive Frobenius exponents, construct the degree-zero quotient between unequal lifts, and prove that this quotient has zero finite reciprocity value. Finally reciprocity multiplicativity supplies additivity on the Frobenius semigroup, so the lift supplied by the finite degree-quotient decomposition descends to the additive reciprocity homomorphism of the finite reciprocity equivalence.
Mathlib's Rep ℤ G forces its representation-bearing group G to Type 0.
Mathlib's Rep ℤ G forces its representation-bearing group G to Type 0.
Mathlib's Rep ℤ G forces its representation-bearing group G to Type 0.
Mathlib's Rep ℤ G forces its representation-bearing group G to Type 0.
The abstract reciprocity construction, the unramified norm-quotient equivalence
This file proves the generator calculation in the unramified case: the finite reciprocity equivalence sends arithmetic Frobenius to the prime class. That class generates the finite norm quotient, so the resulting reciprocity homomorphism is promoted to an additive equivalence.
Mathlib's Rep ℤ G forces its representation-bearing group G to Type 0.
Declarations
ClassFormation.DegreeData.finiteReciprocityValue
DocumentationThe reciprocity value of a Frobenius element after passage from the universal norm quotient to the finite quotient by N_{L/K} A_L.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityValues
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityValue_mul
Documentationreciprocity multiplicativity remains additive after passage from the universal norm quotient to the finite quotient by N_{L/K} A_L.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityValues
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityValue_eq_primeNormClass
DocumentationFormula for the finite Frobenius value using the chosen prime element of its fixed field.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityValues
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityValue_eq_primeNormClass_of_isPrime
DocumentationThe same formula for any prime element of the fixed field. Prime-choice independence is exactly the reciprocity construction's consequence of the unit-cohomology axiom.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityValues
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.frobeniusLiftDifference
DocumentationThe quotient between two Frobenius lifts when the exponent of the first is strictly smaller. Its exponent is the positive difference.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section frobeniusLiftAlgebra
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.frobeniusLiftDifference_coe
DocumentationThe difference of two Frobenius lifts coerces to their ambient quotient difference.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section frobeniusLiftAlgebra
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.mul_frobeniusLiftDifference
DocumentationMultiplying the smaller lift by its quotient recovers the larger lift.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section frobeniusLiftAlgebra
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.frobeniusRestriction_frobeniusLiftDifference
DocumentationIf the two lifts have the same restriction, their quotient restricts trivially.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section frobeniusLiftAlgebra
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityValue_eq_zero_of_restriction_eq_one
DocumentationA Frobenius lift restricting trivially to L has zero value in the finite norm quotient. Its fixed field contains L, so its norm to K factors through N_{L/K}.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section trivialRestrictionValues
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.frobenius_eq_of_restriction_eq_of_exponent_eq
DocumentationEqual restrictions and equal positive degrees give equal Frobenius lifts. This is the first case in the lift-independence proof.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section equalFrobeniusLifts
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityHom_lift_comparison
DocumentationThe complete degree comparison. Two lifts of the same finite automorphism are either equal, or the larger-degree lift is the smaller one times a positive Frobenius lift which restricts trivially and therefore has zero value in the finite norm quotient.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section liftComparison
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.chosenFiniteReciprocityFrobeniusLift
DocumentationA specified Frobenius lift of a finite Galois automorphism, chosen from the surjectivity in the finite degree-quotient decomposition.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section chosenFrobeniusLifts
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.frobeniusRestriction_chosenFiniteReciprocityFrobeniusLift
DocumentationThe chosen finite-reciprocity Frobenius lift restricts to the prescribed Frobenius element.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section chosenFrobeniusLifts
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityCandidate
DocumentationThe canonical candidate underlying the finite reciprocity equivalence, obtained by choosing the finite degree-quotient decomposition lift and evaluating in the finite norm quotient. Lift-independence and additivity are reduced to the concrete steps above and reciprocity multiplicativity, respectively.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityCandidate_apply
DocumentationThe finite reciprocity candidate evaluates a norm class through its chosen Frobenius lift.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityCandidate_eq_primeNormClass
DocumentationFormula for the candidate using the fixed field of its specified the finite degree-quotient decomposition lift.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityCandidate_zero
DocumentationThe finite reciprocity candidate sends the zero norm class to the identity.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityHom_product_lift_comparison
DocumentationFor two finite automorphisms, the chosen lift of their product and the product of their chosen lifts have the same restriction. Applying the degree comparison gives exactly the remaining lift-independence obligation in the additivity proof of the finite reciprocity equivalence.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityValue_eq_of_same_restriction_of_mul
DocumentationOnce reciprocity multiplicativity supplies additivity on the Frobenius semigroup, the degree comparison proves that the finite reciprocity value is independent of the chosen lift. This is the full three-case argument.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityCandidate_add_of_mul
DocumentationThe finite degree-quotient decomposition candidate is additive as soon as reciprocity multiplicativity is available. Lift-independence is invoked for the chosen lift of a product and the product of the two chosen lifts.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityHom_of_mul
DocumentationThe finite reciprocity equivalence with the semigroup-additivity input isolated. The final theorem discharges this input directly from reciprocity multiplicativity.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityHom_of_mul_apply_of_frobeniusLift
DocumentationEvaluation of the conditional finite reciprocity homomorphism using any Frobenius lift of the specified finite automorphism.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityHom_of_mul_apply_eq_primeNormClass
DocumentationPrime-norm formula for the conditional finite reciprocity equivalence map, using an arbitrary Frobenius lift and an arbitrary prime of its fixed field.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityHom
Documentationthe finite reciprocity equivalence. The prime-norm construction descends from positive Frobenius lifts to an additive reciprocity homomorphism on the finite Galois group.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.finiteReciprocityHom_apply_eq_primeNormClass
DocumentationPrime-norm evaluation formula for the finite reciprocity equivalence, using any prime element in the fixed field of a chosen Frobenius lift.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
section finiteReciprocityHom
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.unramifiedFrobenius_fixedField_isUnramified
DocumentationFor an unramified L / K, the fixed field of the degree-one Frobenius lift is itself unramified over K.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedFixedFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.unramifiedFrobenius_fixedField_degree
DocumentationThe fixed field of the degree-one lift has degree one over K in the unramified case. This is f_{Σ/K}=d_K(φ_K)=1 together with [Σ:K]=f_{Σ/K}.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedFixedFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.ValuationData.unramifiedFrobenius_primeNorm
DocumentationThe prime-norm calculation in the unramified norm-quotient equivalence: the prime element of K, included into the fixed field of the degree-one lift, has norm equal to the original prime element.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedReciprocity
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
ClassFormation.ValuationData.unramifiedFrobenius_includedPrime_isPrime
DocumentationThe included prime element is a prime element in the fixed field used for the degree-one Frobenius lift.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedReciprocity
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
ClassFormation.ValuationData.unramifiedReciprocity_bijective_of_generator
DocumentationThe last generator-and-order argument in the unramified norm-quotient equivalence. Any homomorphism which sends the arithmetic Frobenius generator to the prime class is bijective: the prime class generates the norm quotient, and both finite groups have order [L : K].
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedReciprocity
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
ClassFormation.ValuationData.unramifiedReciprocity_equiv_of_generator
DocumentationAdditive-equivalence form of the generator criterion for the unramified norm-quotient equivalence. This is useful independently of the particular construction of the reciprocity homomorphism: a homomorphism with the required Frobenius value is canonically promoted to an equivalence.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedReciprocity
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
ClassFormation.ValuationData.unramifiedReciprocity_equiv_of_generator_apply
DocumentationThe generator-dependent unramified reciprocity equivalence has the expected value on each class.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedReciprocity
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
ClassFormation.ValuationData.unramifiedReciprocity_frobenius_image
DocumentationThe finite reciprocity equivalence sends arithmetic Frobenius to the class of a prime element when L / K is unramified. This is the generator calculation.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedReciprocity
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
ClassFormation.ValuationData.unramifiedReciprocityEquiv
Documentationthe unramified norm-quotient equivalence. For a finite unramified Galois extension, the reciprocity homomorphism of the finite reciprocity equivalence is an additive equivalence.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedReciprocity
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
ClassFormation.ValuationData.unramifiedReciprocityEquiv_apply
DocumentationThe canonical unramified reciprocity equivalence evaluates by the normalized valuation class.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
open scoped BigOperators
noncomputable section
noncomputable section
section unramifiedReciprocity
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData