NYLL
Module

FieldNormBase.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.FieldNormBase
18 declarations indexed from sourceView source ↗

Module documentation

Base-unit norm images in field towers

This file isolates the purely algebraic source for the Abhyankar norm-image argument: embedded base units, their powered image in a lower branch, and the image obtained after applying the lower norm. The only theorem used is field norm transitivity.

Imports1
Imported by3

Declarations

def

baseUnitsMap

L34 ↗
LocalFieldTheory.DiscreteValuationField.baseUnitsMap
Documentation

The unit-group map induced by the algebra map.

Source context 7 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section BaseUnits
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
def baseUnitsMap : Kˣ →* Lˣ
theorem

baseUnitsMap_apply

L41 ↗
LocalFieldTheory.DiscreteValuationField.baseUnitsMap_apply
Documentation

The defining evaluation formula for baseUnitsMap is baseUnitsMap (K := K) (L := L) x = Units.map (algebraMap K L).toMonoidHom x.

Source context 7 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section BaseUnits
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem baseUnitsMap_apply (x : Kˣ) :
    baseUnitsMap (K := K) (L := L) x =
      Units.map (algebraMap K L).toMonoidHom x
theorem

coe_baseUnitsMap_apply

L50 ↗
LocalFieldTheory.DiscreteValuationField.coe_baseUnitsMap_apply
Documentation

The defining evaluation formula for coe_baseUnitsMap is ((baseUnitsMap (K := K) (L := L) x : Lˣ) : L) = algebraMap K L (x : K).

Source context 7 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section BaseUnits
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem coe_baseUnitsMap_apply (x : Kˣ) :
    ((baseUnitsMap (K := K) (L := L) x : Lˣ) : L) =
      algebraMap K L (x : K)
def

baseUnitsImageSubgroup

L56 ↗
LocalFieldTheory.DiscreteValuationField.baseUnitsImageSubgroup
Documentation

The subgroup of extension units generated by embedded base units.

Source context 7 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section BaseUnits
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
def baseUnitsImageSubgroup : Subgroup Lˣ
theorem

mem_baseUnitsImageSubgroup_iff

L63 ↗
LocalFieldTheory.DiscreteValuationField.mem_baseUnitsImageSubgroup_iff
Documentation

Characterizes x ∈ baseUnitsImageSubgroup (K := K) (L := L) by the equivalent condition ∃ y : Kˣ, baseUnitsMap (K := K) (L := L) y = x.

Source context 7 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section BaseUnits
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem mem_baseUnitsImageSubgroup_iff (x : Lˣ) :
    x ∈ baseUnitsImageSubgroup (K := K) (L := L) ↔
      ∃ y : Kˣ, baseUnitsMap (K := K) (L := L) y = x
theorem

baseUnitsMap_mem_baseUnitsImageSubgroup

L72 ↗
LocalFieldTheory.DiscreteValuationField.baseUnitsMap_mem_baseUnitsImageSubgroup
Documentation

Establishes the membership statement baseUnitsMap (K := K) (L := L) x ∈ baseUnitsImageSubgroup (K := K) (L := L).

Source context 7 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section BaseUnits
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem baseUnitsMap_mem_baseUnitsImageSubgroup (x : Kˣ) :
    baseUnitsMap (K := K) (L := L) x ∈
      baseUnitsImageSubgroup (K := K) (L := L)
theorem

baseUnitsMap_tower

L87 ↗
LocalFieldTheory.DiscreteValuationField.baseUnitsMap_tower
Documentation

Embedded base units are compatible with field towers.

Source context 9 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section Tower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra K M] [Algebra L M]
variable [IsScalarTower K L M]
Lean source · statement
theorem baseUnitsMap_tower (x : Kˣ) :
    baseUnitsMap (K := L) (L := M)
        (baseUnitsMap (K := K) (L := L) x) =
      baseUnitsMap (K := K) (L := M) x
theorem

baseUnitsMap_mem_baseUnitsImageSubgroup_tower

L96 ↗
LocalFieldTheory.DiscreteValuationField.baseUnitsMap_mem_baseUnitsImageSubgroup_tower
Documentation

Elementwise tower transport for the subgroup of embedded base units.

Source context 9 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section Tower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra K M] [Algebra L M]
variable [IsScalarTower K L M]
Lean source · statement
theorem baseUnitsMap_mem_baseUnitsImageSubgroup_tower
    {x : Lˣ} (hx : x ∈ baseUnitsImageSubgroup (K := K) (L := L)) :
    baseUnitsMap (K := L) (L := M) x ∈
      baseUnitsImageSubgroup (K := K) (L := M)
theorem

baseUnitsImageSubgroup_map_le_tower

L106 ↗
LocalFieldTheory.DiscreteValuationField.baseUnitsImageSubgroup_map_le_tower
Documentation

Subgroup-level tower transport for embedded base units.

Source context 9 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section Tower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra K M] [Algebra L M]
variable [IsScalarTower K L M]
Lean source · statement
theorem baseUnitsImageSubgroup_map_le_tower :
    (baseUnitsImageSubgroup (K := K) (L := L)).map
        (baseUnitsMap (K := L) (L := M)) ≤
      baseUnitsImageSubgroup (K := K) (L := M)
def

finrankPowerUnitsHom

L125 ↗
LocalFieldTheory.DiscreteValuationField.finrankPowerUnitsHom
Documentation

The [M : L]-power endomorphism on lower-branch units.

Source context 8 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section LowerNormTower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
Lean source · full declaration
def finrankPowerUnitsHom : Lˣ →* Lˣ where
  toFun x := x ^ Module.finrank L M
  map_one' := by
    simp
  map_mul' x y := by
    simpa using mul_pow x y (Module.finrank L M)
def

poweredBaseUnitsImageSubgroup

L134 ↗
LocalFieldTheory.DiscreteValuationField.poweredBaseUnitsImageSubgroup
Documentation

The subgroup of lower-branch units obtained by taking [M : L]-th powers of embedded base units.

Source context 8 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section LowerNormTower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
Lean source · statement
def poweredBaseUnitsImageSubgroup : Subgroup Lˣ
theorem

pow_mem_poweredBaseUnitsImageSubgroup_of_mem

L139 ↗
LocalFieldTheory.DiscreteValuationField.pow_mem_poweredBaseUnitsImageSubgroup_of_mem
Documentation

A powered embedded base unit lies in the powered image subgroup.

Source context 8 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section LowerNormTower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
Lean source · statement
theorem pow_mem_poweredBaseUnitsImageSubgroup_of_mem
    {x : Lˣ} (hx : x ∈ baseUnitsImageSubgroup (K := K) (L := L)) :
    x ^ Module.finrank L M ∈
      poweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)
theorem

baseUnitsMap_pow_finrank_mem_fieldNormSubgroup_tower

L147 ↗
LocalFieldTheory.DiscreteValuationField.baseUnitsMap_pow_finrank_mem_fieldNormSubgroup_tower
Documentation

A base unit embedded from K to L has its [M : L]-th power in the norm subgroup for M/L.

Source context 8 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section LowerNormTower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
Lean source · statement
theorem baseUnitsMap_pow_finrank_mem_fieldNormSubgroup_tower
    (x : Kˣ) :
    baseUnitsMap (K := K) (L := L) x ^ Module.finrank L M ∈
      fieldNormSubgroup L M
theorem

pow_finrank_mem_fieldNormSubgroup_of_mem_baseUnitsImage_tower

L157 ↗
LocalFieldTheory.DiscreteValuationField.pow_finrank_mem_fieldNormSubgroup_of_mem_baseUnitsImage_tower
Documentation

Elementwise comparison with the norm subgroup: every element of the K-base-unit image inside L becomes a norm from M/L after taking the [M : L]-th power.

Source context 8 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section LowerNormTower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
Lean source · statement
theorem pow_finrank_mem_fieldNormSubgroup_of_mem_baseUnitsImage_tower
    {x : Lˣ} (hx : x ∈ baseUnitsImageSubgroup (K := K) (L := L)) :
    x ^ Module.finrank L M ∈ fieldNormSubgroup L M
theorem

poweredBaseUnitsImageSubgroup_le_fieldNormSubgroup

L167 ↗
LocalFieldTheory.DiscreteValuationField.poweredBaseUnitsImageSubgroup_le_fieldNormSubgroup
Documentation

The powered embedded-base-unit image is contained in the field-norm subgroup for M/L.

Source context 8 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section LowerNormTower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
Lean source · statement
theorem poweredBaseUnitsImageSubgroup_le_fieldNormSubgroup :
    poweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M) ≤
      fieldNormSubgroup L M
def

normPoweredBaseUnitsImageSubgroup

L186 ↗
LocalFieldTheory.DiscreteValuationField.normPoweredBaseUnitsImageSubgroup
Documentation

The K-norm image of the powered embedded-base-unit subgroup in the lower branch.

Source context 8 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section NormDownTower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
Lean source · statement
def normPoweredBaseUnitsImageSubgroup : Subgroup Kˣ
theorem

fieldNormUnits_pow_mem_normPoweredBaseUnitsImageSubgroup_of_mem

L192 ↗
LocalFieldTheory.DiscreteValuationField.fieldNormUnits_pow_mem_normPoweredBaseUnitsImageSubgroup_of_mem
Documentation

A powered embedded base unit, after applying N_{L/K}, lies in the normed powered image subgroup.

Source context 8 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section NormDownTower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
Lean source · statement
theorem fieldNormUnits_pow_mem_normPoweredBaseUnitsImageSubgroup_of_mem
    {x : Lˣ} (hx : x ∈ baseUnitsImageSubgroup (K := K) (L := L)) :
    normUnits K L (x ^ Module.finrank L M) ∈
      normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)
theorem

normPoweredBaseUnitsImageSubgroup_le_fieldNormSubgroup_top

L205 ↗
LocalFieldTheory.DiscreteValuationField.normPoweredBaseUnitsImageSubgroup_le_fieldNormSubgroup_top
Documentation

Norm transitivity sends the normed powered embedded-base-unit image into the common-top field-norm subgroup N_{M/K}(Mˣ).

Source context 9 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
section NormDownTower
variable {K L M : Type u}
variable [Field K] [Field L] [Field M]
variable [Algebra K L] [Algebra L M]
variable [Algebra K M] [IsScalarTower K L M] [Module.Free L M]
Lean source · statement
theorem normPoweredBaseUnitsImageSubgroup_le_fieldNormSubgroup_top :
    normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M) ≤
      fieldNormSubgroup K M

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