Module

InfiniteUnitNormSubgroup.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.InfiniteUnitNormSubgroup

6 declarations indexed from sourceView source ↗

Module documentation

Infinite unit norm subgroups

This module defines the finite-level and infinite unit norm ranges, proves their tower compatibility, and compares them with the ambient norm subgroups.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.InfiniteUnitDescent

Imported by2

def

finiteIntermediateUnitNormRange

ClassFormation.ValuationData.finiteIntermediateUnitNormRange

Documentation

The image N_{M/K} U_M from one finite intermediate field.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}

Lean source · statement

def finiteIntermediateUnitNormRange
    (v : ValuationData D A) (E : ClosedSubgroup G)
    (K : FiniteAbstractField G)
    (M : FiniteIntermediateField E K.field) :
    AddSubgroup (ambientFixedAddSubgroup A K.field)

theorem

mem_finiteIntermediateUnitNormRange_of_overfield

ClassFormation.ValuationData.mem_finiteIntermediateUnitNormRange_of_overfield

Documentation

A unit norm obtained from a finite overfield of M already lies in the unit norm range attached to M, by transitivity of the actual norm.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}

Lean source · statement

theorem mem_finiteIntermediateUnitNormRange_of_overfield
    (v : ValuationData D A) (E : ClosedSubgroup G)
    (K : FiniteAbstractField G)
    (M P : FiniteIntermediateField E K.field)
    (hPM : P.field.toSubgroup ≤ M.field.toSubgroup)
    [hPfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field P.field P.below)]
    (uP : v.unitAddSubgroup (P.toFiniteAbstractField K))
    (aK : ambientFixedAddSubgroup A K.field)
    (haK : relativeNorm A K.field P.field P.below uP.1 = aK) :
    aK ∈ v.finiteIntermediateUnitNormRange E K M

def

infiniteUnitNormSubgroup

ClassFormation.ValuationData.infiniteUnitNormSubgroup

Documentation

The universal unit norm group N_{E/K} U_E = ⋂_M N_{M/K} U_M.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}

Lean source · statement

def infiniteUnitNormSubgroup
    (v : ValuationData D A) (E : ClosedSubgroup G)
    (K : FiniteAbstractField G) :
    AddSubgroup (ambientFixedAddSubgroup A K.field)

theorem

mem_infiniteUnitNormSubgroup_iff

ClassFormation.ValuationData.mem_infiniteUnitNormSubgroup_iff

Documentation

Characterizes a ∈ v.infiniteUnitNormSubgroup E K by the equivalent condition ∀ M : FiniteIntermediateField E K.field, a ∈ v.finiteIntermediateUnitNormRange E K M.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}

Lean source · statement

theorem mem_infiniteUnitNormSubgroup_iff
    (v : ValuationData D A) (E : ClosedSubgroup G)
    (K : FiniteAbstractField G)
    (a : ambientFixedAddSubgroup A K.field) :
    a ∈ v.infiniteUnitNormSubgroup E K ↔
      ∀ M : FiniteIntermediateField E K.field,
        a ∈ v.finiteIntermediateUnitNormRange E K M

theorem

finiteIntermediateUnitNormRange_le_normRange

ClassFormation.ValuationData.finiteIntermediateUnitNormRange_le_normRange

Documentation

Proves the bound v.finiteIntermediateUnitNormRange E K M ≤ finiteIntermediateNormRange A E K.field M.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}

Lean source · statement

theorem finiteIntermediateUnitNormRange_le_normRange
    (v : ValuationData D A) (E : ClosedSubgroup G)
    (K : FiniteAbstractField G)
    (M : FiniteIntermediateField E K.field) :
    v.finiteIntermediateUnitNormRange E K M ≤
      finiteIntermediateNormRange A E K.field M

theorem

infiniteUnitNormSubgroup_le_normSubgroup

ClassFormation.ValuationData.infiniteUnitNormSubgroup_le_normSubgroup

Documentation

Proves the bound v.infiniteUnitNormSubgroup E K ≤ infiniteNormSubgroup A E K.field.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}

Lean source · statement

theorem infiniteUnitNormSubgroup_le_normSubgroup
    (v : ValuationData D A) (E : ClosedSubgroup G)
    (K : FiniteAbstractField G) :
    v.infiniteUnitNormSubgroup E K ≤ infiniteNormSubgroup A E K.field