NYLL
Module

FiniteFieldUnitMaps.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FiniteFieldUnitMaps
11 declarations indexed from sourceView source ↗

Module documentation

Finite-field unit maps

This module proves valuation invariance on Frobenius fixed fields and constructs the induced actions, inclusions, and relative norms on the corresponding finite unit groups.

Imports3
Imported by3

Declarations

instance

toFiniteResidueAbstractField_extensionNormal

L38 ↗
ClassFormation.FiniteAbstractField.toFiniteResidueAbstractField_extensionNormal
Documentation

Normality transports across the canonical residue-field enrichment.

Source context 9 commands

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

universe u v
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbstractField
Lean source · statement
instance toFiniteResidueAbstractField_extensionNormal
    (K : FiniteAbstractField G) (D : DegreeData G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hnormal : (extensionSubgroup K.field L hLK).Normal] :
    (extensionSubgroup (K.toFiniteResidueAbstractField D).field L hLK).Normal
instance

toFiniteResidueAbstractField_extensionFinite

L47 ↗
ClassFormation.FiniteAbstractField.toFiniteResidueAbstractField_extensionFinite
Documentation

Relative finiteness transports across the canonical residue-field enrichment.

Source context 9 commands

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

universe u v
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace FiniteAbstractField
Lean source · statement
instance toFiniteResidueAbstractField_extensionFinite
    (K : FiniteAbstractField G) (D : DegreeData G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)] :
    Finite ((K.toFiniteResidueAbstractField D).field.toSubgroup ⧸
      extensionSubgroup (K.toFiniteResidueAbstractField D).field L hLK)
theorem

ambientFixedAddSubgroup_transport_coe

L64 ↗
ClassFormation.ValuationData.ambientFixedAddSubgroup_transport_coe
Source context 10 commands

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

universe u v
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 ambientFixedAddSubgroup_transport_coe
    (K L : FiniteAbstractField G) (h : K = L)
    (a : ambientFixedAddSubgroup A K.field) :
    (((h ▸ a : ambientFixedAddSubgroup A L.field) : A.V)) = a.1
theorem

valuationAt_transport

L71 ↗
ClassFormation.ValuationData.valuationAt_transport
Source context 10 commands

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

universe u v
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 valuationAt_transport
    (v : ValuationData D A) (K L : FiniteAbstractField G) (h : K = L)
    (a : ambientFixedAddSubgroup A K.field) :
    v.valuationAt L (h ▸ a) = v.valuationAt K a
theorem

valuationAt_frobeniusFixedFieldAction

L80 ↗
ClassFormation.ValuationData.valuationAt_frobeniusFixedFieldAction
Documentation

A quotient element stabilizing a Frobenius fixed field preserves its normalized valuation.

Source context 10 commands

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

universe u v
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 valuationAt_frobeniusFixedFieldAction
    (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : DegreeData.FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK)
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q)
    [Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G)
        (D.frobeniusFixedField K L hLK σ)
        (le_baseField (D.frobeniusFixedField K L hLK σ)))]
    (a : ambientFixedAddSubgroup A
      (D.frobeniusFixedField K L hLK σ)) :
    v.valuationAt (D.frobeniusFixedAbstractField K L hLK σ)
        (D.frobeniusFixedFieldAction A K L hLK σ q hq a) =
      v.valuationAt (D.frobeniusFixedAbstractField K L hLK σ) a
def

frobeniusFixedFieldUnitAction

L134 ↗
ClassFormation.ValuationData.frobeniusFixedFieldUnitAction
Documentation

The stabilizing action restricted to the unit group of a Frobenius fixed field.

Source context 10 commands

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

universe u v
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 · full declaration
def frobeniusFixedFieldUnitAction
    (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : DegreeData.FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ : D.FrobeniusElements K L hLK)
    (q : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hq : q * σ.1 = σ.1 * q)
    [Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G)
        (D.frobeniusFixedField K L hLK σ)
        (le_baseField (D.frobeniusFixedField K L hLK σ)))] :
    v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σ) →+
      v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σ) where
  toFun u := ⟨D.frobeniusFixedFieldAction A K L hLK σ q hq u.1, by
    exact (v.mem_unitAddSubgroup_iff
      (D.frobeniusFixedAbstractField K L hLK σ)
      (D.frobeniusFixedFieldAction A K L hLK σ q hq u.1)).2
        ((v.valuationAt_frobeniusFixedFieldAction K L hLK σ q hq u.1).trans u.2)⟩
  map_zero' := by apply Subtype.ext; exact map_zero _
  map_add' _ _ := by apply Subtype.ext; exact map_add _ _ _
theorem

fixedFieldInclusion_mem_unitAddSubgroup

L161 ↗
ClassFormation.ValuationData.fixedFieldInclusion_mem_unitAddSubgroup
Documentation

Units stay units after inclusion into any finite extension. The construction uses this silently when all finitely many terms of (*) are placed in one finite Galois field.

Source context 10 commands

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

universe u v
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 fixedFieldInclusion_mem_unitAddSubgroup
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (u : v.unitAddSubgroup E.base) :
    fixedFieldInclusion A E.base.field E.field.field E.below u.1 ∈
      v.unitAddSubgroup E.field
def

finiteUnitInclusion

L198 ↗
ClassFormation.ValuationData.finiteUnitInclusion
Documentation

Inclusion of units along an arbitrary finite extension.

Source context 10 commands

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

universe u v
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 · full declaration
def finiteUnitInclusion
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G) :
    v.unitAddSubgroup E.base →+ v.unitAddSubgroup E.field where
  toFun u := ⟨fixedFieldInclusion A E.base.field E.field.field E.below u.1,
    v.fixedFieldInclusion_mem_unitAddSubgroup E u⟩
  map_zero' := by apply Subtype.ext; rfl
  map_add' _ _ := by apply Subtype.ext; rfl
theorem

finiteUnitInclusion_transport_coe

L208 ↗
ClassFormation.ValuationData.finiteUnitInclusion_transport_coe
Documentation

Transporting a finite-unit inclusion along equality of its target field does not change its ambient coefficient.

Source context 10 commands

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

universe u v
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 finiteUnitInclusion_transport_coe
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (F : FiniteAbstractField G) (h : E.field = F)
    (u : v.unitAddSubgroup E.base) :
    (((h ▸ v.finiteUnitInclusion E u : v.unitAddSubgroup F).1 :
        ambientFixedAddSubgroup A F.field) : A.V) = u.1.1
theorem

relativeNorm_mem_unitAddSubgroup

L220 ↗
ClassFormation.ValuationData.relativeNorm_mem_unitAddSubgroup
Documentation

The norm of a unit through an arbitrary finite extension is a unit. This is the valuation-theoretic step used when a finite Galois refinement is pushed back down to the originally prescribed intermediate field.

Source context 10 commands

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

universe u v
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 relativeNorm_mem_unitAddSubgroup
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (u : v.unitAddSubgroup E.field) :
    relativeNorm A E.base.field E.field.field E.below u.1 ∈
      v.unitAddSubgroup E.base
def

finiteUnitNorm

L238 ↗
ClassFormation.ValuationData.finiteUnitNorm
Documentation

Relative norm restricted to the finite unit groups.

Source context 10 commands

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

universe u v
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 · full declaration
def finiteUnitNorm
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G) :
    v.unitAddSubgroup E.field →+ v.unitAddSubgroup E.base where
  toFun u := ⟨relativeNorm A E.base.field E.field.field E.below u.1,
    v.relativeNorm_mem_unitAddSubgroup E u⟩
  map_zero' := by apply Subtype.ext; exact map_zero _
  map_add' _ _ := by apply Subtype.ext; exact map_add _ _ _

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.