Module

Common.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.FieldNorm.Common

4 declarations indexed from sourceView source ↗

Module documentation

Field-norm common images

This file supplies the common-image containments used by the value-group frontier from the concrete tower transitivity of field norms.

Imports2

Imported by2

theorem

fieldNormSubgroup_le_valuedFieldNorm_normSubgroup_of_tower

L34 ↗

TameAbhyankar.FieldNormCommon.fieldNormSubgroup_le_valuedFieldNorm_normSubgroup_of_tower

Documentation

The norm subgroup from a common top field lies in the valued field-norm subgroup of any lower intermediate field in the tower.

Source context 9 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
namespace FieldNormCommon
section SingleTower
variable {K E M : Type _}
variable [Field K] [Field E] [Field M]
variable [Algebra K E] [Algebra K M] [Algebra E M]
variable [IsScalarTower K E M] [Module.Free E M]

Lean source · statement

theorem fieldNormSubgroup_le_valuedFieldNorm_normSubgroup_of_tower
    (vK : MultiplicativeIntegerValuation Kˣ)
    (vE : MultiplicativeIntegerValuation Eˣ)
    (residueDegree : ℕ)
    (hformula :
      ∀ x : Eˣ, vK.val (normUnits K E x) =
        (residueDegree : ℤ) * vE.val x) :
    fieldNormSubgroup K M ≤
      (valuedFieldNorm K E vK vE residueDegree hformula).normSubgroup

theorem

lcm_dvd_of_exists_mem_val_of_common_fieldNormSubgroup_le_towers

L62 ↗

TameAbhyankar.FieldNormCommon.lcm_dvd_of_exists_mem_val_of_common_fieldNormSubgroup_le_towers

Documentation

Common-top field-norm form of the lcm value step. The two lower norm containments are generated by field-norm transitivity from the common top field M.

Source context 12 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
namespace FieldNormCommon
section TwoLowerTowers
variable {K L L' M : Type _}
variable [Field K] [Field L] [Field L'] [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]

Lean source · statement

theorem lcm_dvd_of_exists_mem_val_of_common_fieldNormSubgroup_le_towers
    (vK : MultiplicativeIntegerValuation Kˣ)
    (vL : MultiplicativeIntegerValuation Lˣ)
    (vL' : MultiplicativeIntegerValuation L'ˣ)
    (residueDegree residueDegree' : ℕ)
    (hformula :
      ∀ x : Lˣ, vK.val (normUnits K L x) =
        (residueDegree : ℤ) * vL.val x)
    (hformula' :
      ∀ x : L'ˣ, vK.val (normUnits K L' x) =
        (residueDegree' : ℤ) * vL'.val x)
    {S : Subgroup Kˣ} {n : ℤ}
    (hn : ∃ x : Kˣ, x ∈ S ∧ vK.val x = n)
    (hS : S ≤ fieldNormSubgroup K M) :
    ((((residueDegree : ℤ).lcm (residueDegree' : ℤ) : ℕ) : ℤ) ∣ n)

theorem

lcm_dvd_val_fieldNormUnits_of_common_tower

L90 ↗

TameAbhyankar.FieldNormCommon.lcm_dvd_val_fieldNormUnits_of_common_tower

Documentation

Field-norm element form of the common-top lcm value step. Every element which is visibly a norm from the common top field has base valuation divisible by the lcm of the two lower valued field-norm residue degrees.

Source context 12 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
namespace FieldNormCommon
section TwoLowerTowers
variable {K L L' M : Type _}
variable [Field K] [Field L] [Field L'] [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]

Lean source · statement

theorem lcm_dvd_val_fieldNormUnits_of_common_tower
    (vK : MultiplicativeIntegerValuation Kˣ)
    (vL : MultiplicativeIntegerValuation Lˣ)
    (vL' : MultiplicativeIntegerValuation L'ˣ)
    (residueDegree residueDegree' : ℕ)
    (hformula :
      ∀ x : Lˣ, vK.val (normUnits K L x) =
        (residueDegree : ℤ) * vL.val x)
    (hformula' :
      ∀ x : L'ˣ, vK.val (normUnits K L' x) =
        (residueDegree' : ℤ) * vL'.val x)
    (y : Mˣ) :
    ((((residueDegree : ℤ).lcm (residueDegree' : ℤ) : ℕ) : ℤ) ∣
      vK.val (normUnits K M y))

theorem

lcm_dvd_val_of_mem_common_fieldNormSubgroup_towers

L115 ↗

TameAbhyankar.FieldNormCommon.lcm_dvd_val_of_mem_common_fieldNormSubgroup_towers

Documentation

Membership form of the common-top lcm value step. Once an element of the base unit group is known to lie in the common-top field-norm subgroup, its valuation satisfies the same lcm divisibility.

Source context 12 commands

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

noncomputable section
namespace TameAbhyankar
open LocalFieldTheory LocalFieldTheory.DiscreteValuationField
namespace FieldNormCommon
section TwoLowerTowers
variable {K L L' M : Type _}
variable [Field K] [Field L] [Field L'] [Field M]
variable [Algebra K L] [Algebra K L']
variable [Algebra K M]
variable [Algebra L M] [Algebra L' M]
variable [IsScalarTower K L M] [IsScalarTower K L' M]
variable [Module.Free L M] [Module.Free L' M]

Lean source · statement

theorem lcm_dvd_val_of_mem_common_fieldNormSubgroup_towers
    (vK : MultiplicativeIntegerValuation Kˣ)
    (vL : MultiplicativeIntegerValuation Lˣ)
    (vL' : MultiplicativeIntegerValuation L'ˣ)
    (residueDegree residueDegree' : ℕ)
    (hformula :
      ∀ x : Lˣ, vK.val (normUnits K L x) =
        (residueDegree : ℤ) * vL.val x)
    (hformula' :
      ∀ x : L'ˣ, vK.val (normUnits K L' x) =
        (residueDegree' : ℤ) * vL'.val x)
    {x : Kˣ} (hx : x ∈ fieldNormSubgroup K M) :
    ((((residueDegree : ℤ).lcm (residueDegree' : ℤ) : ℕ) : ℤ) ∣
      vK.val x)

Module documentation

Field-norm common images

Declarations

fieldNormSubgroup_le_valuedFieldNorm_normSubgroup_of_tower

lcm_dvd_of_exists_mem_val_of_common_fieldNormSubgroup_le_towers

lcm_dvd_val_fieldNormUnits_of_common_tower

lcm_dvd_val_of_mem_common_fieldNormSubgroup_towers