ModuleMainTransferFrobenius.lean
Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.MainTransferFrobenius
25 declarations indexed from sourceView source ↗ Module documentation
The abstract reciprocity construction, transfer--norm naturality: Frobenius fibers
This module continues the geometric transfer construction with the chosen norm-orbit representatives, fiber calculations, fixed-field arithmetic, and the final Frobenius transfer formula.
Mathlib's Rep ℤ G requires its coefficient ring and acting group in the same universe, so this representation-bearing portion has G : Type 0.
Mathlib's Rep ℤ G requires its coefficient ring and acting group in the same universe, so this representation-bearing portion has G : Type 0.
Mathlib's Rep ℤ G requires its coefficient ring and acting group in the same universe, so this representation-bearing portion has G : Type 0.
Declarations
ClassFormation.Internal.chosenTransferNormNaturalityNormOrbitRepresentative
DocumentationThe chosen representative of a norm orbit is the inverse of the representative of the corresponding transfer orbit.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace Internal
ClassFormation.Internal.chosenTransferNormNaturalityNormOrbitRepresentative_spec
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusGeometry
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace Internal
ClassFormation.Internal.transferNormNaturalityNorm_eq_sum_transferOrbitRepresentatives
DocumentationThe relative norm from the Frobenius fixed field is the sum over the norm double cosets corresponding to the classical transfer orbits. The representative of the orbit paired with q is the inverse of the transfer representative selected by Quotient.out.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferOrbitNorms
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace Internal
ClassFormation.DegreeData.transferNormNaturalityFrobeniusIntermediateEquiv
DocumentationCanonical identification of the two realizations of G(\widetilde L/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
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityFrobeniusIntermediateEquiv_mk
DocumentationEstablishes the identity (D.transferNormNaturalityFrobeniusIntermediateEquiv E L hL (QuotientGroup.mk k')).1 = QuotientGroup.mk (Subgroup.inclusion E.below 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
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturality_zHat_positive_nat_of_nsmul_eq_nat
DocumentationA divisibility fact in ℤ̂ used to recognize every transfer term as a positive Frobenius element 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
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityFrobeniusTransferTerm
DocumentationThe element τ⁻¹ σ ^ f(τ) τ of H attached to one double coset in the transfer formula on G(\widetilde L/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
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityFrobeniusTransferTermPreimage
DocumentationThe transfer term pulled back from H to G(\widetilde L/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
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityFrobeniusTransferTermPreimage_degree
DocumentationThe pullback of each double-coset term has strictly positive integral normalized degree, as asserted.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityTransferFrobeniusLift
DocumentationThe actual Frobenius lift over K' represented by one term of the transfer product.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityTransferFrobeniusLift_coe
DocumentationEstablishes the identity (D.transferNormNaturalityTransferFrobeniusLift E L hL σ q).1 = D.transferNormNaturalityFrobeniusTransferTermPreimage E L hL σ q.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityTransferFrobeniusLift_towerMap
DocumentationThe Frobenius lift attached to a transfer orbit maps to the transfer term τ⁻¹ σ^f τ in G(\widetilde L/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
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityTransferFrobeniusLift_closure_map
DocumentationThe closed subgroup generated by a transfer Frobenius lift maps onto the closed subgroup generated by the corresponding transfer term.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityTransferFrobeniusLift_mem_fixedSubgroup_iff_stabilizer
DocumentationFor a transfer orbit represented by t, the absolute subgroup fixed by its Frobenius lift over K' is the stabilizer of the norm coset t⁻¹ G_Σ. This is the intersection G_K' ∩ t⁻¹ G_Σ t.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityTransferFrobeniusLift_fixedSubgroup_map
DocumentationThe pointwise fixed-subgroup calculation above, upgraded to the literal subgroup equality used to identify the stabilizer-coset fiber in the transfer formula with the norm fiber.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.Internal.chosenTransferNormNaturalityTransferNormFiberEquiv
DocumentationFor each transfer double coset, the quotient by the fixed subgroup of its Frobenius factor is the stabilizer-coset fiber in the corresponding norm double coset.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace Internal
ClassFormation.Internal.chosenTransferNormNaturalityTransferNormFiberEquiv_mk
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferFrobeniusFibers
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace Internal
ClassFormation.Internal.transferNormNaturalityTransferNormFiber_term
DocumentationUnder the fiber equivalence, a summand in the double-coset norm is literally the corresponding summand in N_{Σₜ/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
noncomputable section
open scoped BigOperators
open MulAction
section transferNormFibers
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace Internal
ClassFormation.Internal.transferNormNaturalityTransferNormFiber_sum
DocumentationThe inner double-coset sum for a transfer orbit is the relative norm N_{Σₜ/K'}(π^t) appearing.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferNormFibers
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace Internal
ClassFormation.DegreeData.transferNormNaturalityTransferFrobenius_fixedField_le_conjugate
DocumentationThe fixed field Σₜ of a transfer Frobenius factor is contained in the conjugate field Σ^t. On absolute groups this is G_{Σₜ} ⊆ G_{Σ^t} from.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferredFixedFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityTransferFrobenius_fixedField_isUnramified_conjugate
DocumentationThe extension Σₜ | Σ^t attached to one transfer orbit is unramified, as asserted.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferredFixedFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityTransferFrobenius_conjugatePrime_isPrime
DocumentationIf π is prime in Σ, its conjugate π^t, included into the unramified extension Σₜ, remains prime.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferNormArithmetic
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityNorm_eq_sum_transferNorms
DocumentationThe norm identity for transfer--norm naturality: N_{Σ/K}(π) is the sum, over transfer double cosets, of N_{Σₜ/K'}(π^t). The construction writes this identity multiplicatively.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section transferNormArithmetic
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityFrobeniusTransfer
DocumentationThe classical transfer on the groups G(\widetilde L/K) → G(\widetilde L/K'), before passage to the finite Galois quotient.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section frobeniusTransfer
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
ClassFormation.DegreeData.transferNormNaturalityFrobeniusTransfer_doubleCoset_formula
DocumentationThe double-coset formula for the preceding Frobenius-level transfer. Every factor is the positive Frobenius lift constructed above.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
open CategoryTheory
noncomputable section
open scoped BigOperators
open MulAction
section frobeniusTransfer
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData