ModuleFixedFieldNormResidueNaturality.lean
Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldNormResidueNaturality
26 declarations indexed from sourceView source ↗ Module documentation
Naturality of fixed-field norm-residue symbols
This file transports norm-restriction and transfer-inclusion naturality from the closed-subgroup class formation to actual fixed fields in a single Galois ambient field.
Canonical local-field specializations
Declarations
LocalClassFieldTheory.abstractFixedFieldUnitsInclusion
DocumentationInclusion of the units of the lower concrete fixed field in the units of the larger concrete fixed field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
LocalClassFieldTheory.abstractFixedFieldUnitsEquiv_inclusion
DocumentationThe concrete fixed-field unit equivalences identify actual unit inclusion with inclusion of fixed coefficients.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
omit [IsGalois k Ω] in
LocalClassFieldTheory.abstractFixedFieldNormResidueSymbol
DocumentationThe norm-residue symbol on the actual units of a concrete fixed field, obtained from the abstract class-formation symbol through the canonical fixed-unit and relative-Galois identifications.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
LocalClassFieldTheory.abstractFixedFieldNormUnits
DocumentationThe ordinary field norm on units between two concrete fixed fields.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
LocalClassFieldTheory.abstractFixedFieldAbelianizedRestriction
DocumentationRestriction between the abelianized actual relative Galois groups in a fixed-field square, transported through the canonical quotient/Galois equivalences.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
LocalClassFieldTheory.abstractFixedFieldAbelianizedRestriction_on_representative
DocumentationOn an ambient representative, the transported actual restriction is restriction of that same automorphism to the smaller upper fixed field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
LocalClassFieldTheory.abstractFixedFieldNormResidueSymbol_norm_restriction
DocumentationNorm-restriction naturality for actual fixed fields. Actual Galois restriction is compatible with the ordinary unit norm and the unit-level norm-residue symbols. No normality of the intermediate extension K'/K is assumed.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
LocalClassFieldTheory.abstractFixedFieldAbelianizedTransfer
DocumentationTransfer between the abelianized actual relative Galois groups in a fixed-field tower, transported through the two canonical quotient/Galois equivalences.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
LocalClassFieldTheory.abstractFixedFieldNormResidueSymbol_transfer_inclusion
DocumentationTransfer-inclusion naturality for actual fixed fields. Transfer of the actual relative Galois abelianizations is compatible with inclusion of actual fixed-field units and the unit-level norm-residue symbols.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare
DocumentationA finite fixed-field square encoding norm-restriction naturality inside the separable closure of a local field.
The two horizontal extensions are finite Galois. The vertical base extension is finite but need not be normal.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.upperAbsoluteFinite
DocumentationThe quotient from the absolute subgroup to the upper fixed-field subgroup is finite.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.lowerNormResidueSymbol
DocumentationThe fixed-field norm-residue symbol for the lower horizontal extension, induced by the canonical local class formation.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.upperNormResidueSymbol
DocumentationThe fixed-field norm-residue symbol for the upper horizontal extension, induced by the canonical local class formation.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.normUnits
DocumentationThe ordinary field norm on units along the vertical base extension.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.abelianizedRestriction
DocumentationRestriction between the abelianized actual relative Galois groups.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldNormRestrictionSquare.norm_restriction_commutes
DocumentationCanonical norm-restriction naturality for a local fixed-field square. Restriction commutes with the ordinary field norm and the fixed-field norm-residue symbols induced by the canonical local class formation for the finite Galois square bundled by T; no normality of the vertical base extension is required.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldNormRestrictionSquare
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldTransferTower
DocumentationA finite fixed-field tower encoding transfer-inclusion naturality inside the separable closure of a local field.
The total extension is finite Galois. Normality and finiteness of the upper part of the tower are derived internally.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
LocalClassFieldTheory.LocalFixedFieldTransferTower.intermediateNormal
DocumentationThe top extension subgroup is normal inside the intermediate subgroup.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldTransferTower.intermediateFinite
DocumentationThe quotient of the intermediate subgroup by the top extension subgroup is finite.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldTransferTower.baseIntermediateFinite
DocumentationThe quotient of the base subgroup by the intermediate extension subgroup is finite.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldTransferTower.intermediateAbsoluteFinite
DocumentationThe absolute quotient determined by the intermediate fixed field is finite.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldTransferTower.baseNormResidueSymbol
DocumentationThe fixed-field norm-residue symbol for the total extension, induced by the canonical local class formation.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldTransferTower.intermediateNormResidueSymbol
DocumentationThe fixed-field norm-residue symbol after changing the base to the intermediate fixed field, induced by the canonical local class formation.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldTransferTower.unitsInclusion
DocumentationInclusion of actual fixed-field units along the base change.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldTransferTower.abelianizedTransfer
DocumentationTransfer between the abelianized actual relative Galois groups.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]
LocalClassFieldTheory.LocalFixedFieldTransferTower.transfer_inclusion_commutes
DocumentationCanonical transfer-inclusion naturality for a local fixed-field tower. Transfer commutes with inclusion of fixed-field units and the fixed-field norm-residue symbols induced by the canonical local class formation for the finite Galois tower bundled by T.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
open scoped ValuativeRel
namespace LocalFixedFieldTransferTower
variable {k : Type} [Field k] [ValuativeRel k] [TopologicalSpace k]
[IsNonarchimedeanLocalField k]