ModuleIdeleClassDirectLimitFiniteTowerNormStatement.lean
Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitFiniteTowerNormStatement
4 declarations indexed from sourceView source ↗ Module documentation
Ordinary norms in finite towers of rational fixed fields
This leaf compares the abstract relative norm in the rational idèle-class direct limit with the ordinary idèle-class norm for a finite fixed-field tower. The upper field need not be Galois over the lower field.
The construction is kept separate from the foundational direct-limit norm module so that the normal-closure and coset-product proof elaborates in a fresh command environment.
Declarations
GlobalClassFieldTheory.Reciprocity.rationalFixedFieldAbsoluteQuotient
DocumentationThe finite absolute quotient attached to a rational fixed field.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
GlobalClassFieldTheory.Reciprocity.rationalFixedFieldRelativeQuotient
DocumentationThe finite relative quotient attached to an inclusion of rational fixed fields.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
GlobalClassFieldTheory.Reciprocity.rationalAbstractRelativeFixedFieldNormStatement
DocumentationThe proposition that the abstract relative norm agrees with the ordinary idele-class norm on a finite tower of rational fixed fields.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore
GlobalClassFieldTheory.Reciprocity.rationalRelativeFixedFieldCosetActionStatement
DocumentationThe pointwise comparison between the abstract coset action and the ordinary class embedding into a common rational normal closure.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open LocalClassFieldTheory
open CyclicCohomology
open FiniteTowerNormCore