NYLL
Module

Basic.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.Ramification.Basic
15 declarations indexed from sourceView source ↗

Module documentation

Basic Galois ramification-image subgroups

This file contains the subgroup constructions used by the Neu1999 Galois ramification source: embedded base units, their tower transport, their [M : L]-powered lower image, and the norm-down image in the base field.

Imports1
Imported by3

Declarations

def

baseUnitsImageSubgroup

L32 ↗
TameAbhyankar.NAField.baseUnitsImageSubgroup
Documentation

The subgroup of extension units generated by embedded base units.

Source context 8 commands

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

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

mem_baseUnitsImageSubgroup_iff

L35 ↗
TameAbhyankar.NAField.mem_baseUnitsImageSubgroup_iff
Source context 8 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
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ˣ,
        LocalFieldTheory.IsNonarchimedeanLocalField.mapBaseUnitsToExtensionUnits K L y = x
theorem

mapBaseUnitsToExtensionUnits_mem_baseUnitsImageSubgroup

L41 ↗
TameAbhyankar.NAField.mapBaseUnitsToExtensionUnits_mem_baseUnitsImageSubgroup
Source context 8 commands

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

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

mapBaseUnitsToExtensionUnits_tower

L53 ↗
TameAbhyankar.NAField.mapBaseUnitsToExtensionUnits_tower
Documentation

Embedded base units are compatible with field towers.

Source context 11 commands

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

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

mapBaseUnitsToExtensionUnits_mem_baseUnitsImageSubgroup_tower

L63 ↗
TameAbhyankar.NAField.mapBaseUnitsToExtensionUnits_mem_baseUnitsImageSubgroup_tower
Documentation

Elementwise tower transport for the subgroup of embedded base units.

Source context 11 commands

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

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

baseUnitsImageSubgroup_map_le_tower

L74 ↗
TameAbhyankar.NAField.baseUnitsImageSubgroup_map_le_tower
Documentation

Subgroup-level tower transport for embedded base units.

Source context 11 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
section Tower
variable {M : Type u} [Field M] [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
        (LocalFieldTheory.IsNonarchimedeanLocalField.mapBaseUnitsToExtensionUnits L M) ≤
      baseUnitsImageSubgroup (K := K) (L := M)
def

finrankPowerUnitsHom

L91 ↗
TameAbhyankar.NAField.finrankPowerUnitsHom
Documentation

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

Source context 10 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
section LowerNormTower
variable {M : Type u} [Field M] [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

L100 ↗
TameAbhyankar.NAField.poweredBaseUnitsImageSubgroup
Documentation

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

Source context 10 commands

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

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

pow_mem_poweredBaseUnitsImageSubgroup_of_mem

L105 ↗
TameAbhyankar.NAField.pow_mem_poweredBaseUnitsImageSubgroup_of_mem
Documentation

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

Source context 10 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
section LowerNormTower
variable {M : Type u} [Field M] [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

mapBase_pow_finrank_mem_fieldNormSubgroup_tower

L113 ↗
TameAbhyankar.NAField.mapBase_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 10 commands

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

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

pow_finrank_mem_fieldNormSubgroup_of_mem_baseUnitsImage_tower

L125 ↗
TameAbhyankar.NAField.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 10 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
section LowerNormTower
variable {M : Type u} [Field M] [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

L135 ↗
TameAbhyankar.NAField.poweredBaseUnitsImageSubgroup_le_fieldNormSubgroup
Documentation

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

Source context 10 commands

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

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

normPoweredBaseUnitsImageSubgroup

L155 ↗
TameAbhyankar.NAField.normPoweredBaseUnitsImageSubgroup
Documentation

The K-norm image of the powered embedded-base-unit subgroup in the lower branch. This is a concrete candidate for the common-top ramification image inside Kˣ.

Source context 11 commands

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

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

fieldNormUnits_pow_mem_normPoweredBaseUnitsImageSubgroup_of_mem

L162 ↗
TameAbhyankar.NAField.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 12 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
section NormDownTower
variable {M : Type u} [Field M] [Algebra K M] [Algebra L M]
variable [IsScalarTower K L M] [Module.Free L M]
omit [Algebra K M] [IsScalarTower K L M] [Module.Free L M] in
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

L173 ↗
TameAbhyankar.NAField.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 11 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
section NormDownTower
variable {M : Type u} [Field M] [Algebra K M] [Algebra L M]
variable [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.