Module

NormDown.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.NormDown

18 declarations indexed from sourceView source ↗

Module documentation

Normed Galois ramification images

This file studies the image obtained by applying N_{L/K} to the powered embedded-base-unit ramification image. It keeps the common-top norm containment and its valuation generator in a separate source layer.

Imports5

Imported by3

def

normDownRamificationStepNat

L48 ↗

TameAbhyankar.NAField.normDownRamificationStepNat

Documentation

The base valuation step generated after applying N_{L/K} to the powered embedded-base-unit ramification image from L.

Source context 17 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section NormDownValue
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

def normDownRamificationStepNat : ℕ

theorem

exists_mem_normPoweredBaseUnitsImageSubgroup_val_normDownRamificationStep

L55 ↗

TameAbhyankar.NAField.exists_mem_normPoweredBaseUnitsImageSubgroup_val_normDownRamificationStep

Documentation

The normed powered embedded-base-unit subgroup contains an element whose base valuation is the norm-down ramification step.

Source context 17 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section NormDownValue
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_mem_normPoweredBaseUnitsImageSubgroup_val_normDownRamificationStep :
    ∃ x : Kˣ,
      x ∈ normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M) ∧
        (multiplicativeIntegerValuation K).val x =
          (normDownRamificationStepNat (K := K) (L := L) (M := M) : ℤ)

theorem

integerMultipleSubgroup_normDownRamificationStep_le_normPowered

L69 ↗

TameAbhyankar.NAField.integerMultipleSubgroup_normDownRamificationStep_le_normPowered

Documentation

The norm-down ramification step generates values inside the normed powered embedded-base-unit subgroup.

Source context 17 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section NormDownValue
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem integerMultipleSubgroup_normDownRamificationStep_le_normPowered :
    integerMultipleSubgroup
        (normDownRamificationStepNat (K := K) (L := L) (M := M) : ℤ) ≤
      (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M))

theorem

normPoweredBaseUnitsImageSubgroup_valueImage_le_normDownRamificationStep

L81 ↗

TameAbhyankar.NAField.normPoweredBaseUnitsImageSubgroup_valueImage_le_normDownRamificationStep

Documentation

Every value appearing in the normed powered embedded-base-unit subgroup is a multiple of the norm-down ramification step.

Source context 17 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section NormDownValue
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem normPoweredBaseUnitsImageSubgroup_valueImage_le_normDownRamificationStep :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)) ≤
      integerMultipleSubgroup
        (normDownRamificationStepNat (K := K) (L := L) (M := M) : ℤ)

theorem

normPoweredBaseUnitsImageSubgroup_valueImage_eq_normDownRamificationStep

L119 ↗

TameAbhyankar.NAField.normPoweredBaseUnitsImageSubgroup_valueImage_eq_normDownRamificationStep

Documentation

Exact value image of the normed powered embedded-base-unit subgroup.

Source context 17 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section NormDownValue
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem normPoweredBaseUnitsImageSubgroup_valueImage_eq_normDownRamificationStep :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)) =
      integerMultipleSubgroup
        (normDownRamificationStepNat (K := K) (L := L) (M := M) : ℤ)

theorem

exists_mem_normPoweredBaseUnitsImageSubgroup_val_galoisNormDownRamificationStep

L146 ↗

TameAbhyankar.NAField.exists_mem_normPoweredBaseUnitsImageSubgroup_val_galoisNormDownRamificationStep

Documentation

Galois-data form of the normed powered embedded-base-unit generator.

Source context 17 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisNormDownValue
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_mem_normPoweredBaseUnitsImageSubgroup_val_galoisNormDownRamificationStep :
    ∃ x : Kˣ,
      x ∈ normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M) ∧
        (multiplicativeIntegerValuation K).val x =
          (galoisNormDownRamificationStepNat (K := K) (L := L) (M := M) :
            ℤ)

theorem

integerMultipleSubgroup_galoisNormDownRamificationStep_le_normPowered

L158 ↗

TameAbhyankar.NAField.integerMultipleSubgroup_galoisNormDownRamificationStep_le_normPowered

Documentation

The Galois norm-down step generates values in the normed powered embedded-base-unit subgroup.

Source context 17 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisNormDownValue
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem integerMultipleSubgroup_galoisNormDownRamificationStep_le_normPowered :
    integerMultipleSubgroup
        (galoisNormDownRamificationStepNat (K := K) (L := L) (M := M) :
          ℤ) ≤
      (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M))

theorem

normPoweredBaseUnitsImageSubgroup_valueImage_le_galoisNormDownRamificationStep

L171 ↗

TameAbhyankar.NAField.normPoweredBaseUnitsImageSubgroup_valueImage_le_galoisNormDownRamificationStep

Documentation

Every value in the normed powered subgroup is a multiple of the Galois norm-down ramification step.

Source context 17 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisNormDownValue
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem normPoweredBaseUnitsImageSubgroup_valueImage_le_galoisNormDownRamificationStep :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)) ≤
      integerMultipleSubgroup
        (galoisNormDownRamificationStepNat (K := K) (L := L) (M := M) :
          ℤ)

theorem

normPoweredBaseUnitsImageSubgroup_valueImage_eq_galoisNormDownRamificationStep

L183 ↗

TameAbhyankar.NAField.normPoweredBaseUnitsImageSubgroup_valueImage_eq_galoisNormDownRamificationStep

Documentation

Exact Galois-data value image of the normed powered embedded-base-unit subgroup.

Source context 17 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisNormDownValue
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem normPoweredBaseUnitsImageSubgroup_valueImage_eq_galoisNormDownRamificationStep :
    (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (normPoweredBaseUnitsImageSubgroup (K := K) (L := L) (M := M)) =
      integerMultipleSubgroup
        (galoisNormDownRamificationStepNat (K := K) (L := L) (M := M) :
          ℤ)

theorem

exists_mem_fieldNormSubgroup_val_normDownRamificationStep

L213 ↗

TameAbhyankar.NAField.exists_mem_fieldNormSubgroup_val_normDownRamificationStep

Documentation

The common-top field-norm subgroup contains the concrete norm-down ramification-image generator.

Source context 18 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section CommonTopNormDownGenerator
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra K M] [Algebra L M]
variable [IsScalarTower K L M] [Module.Free L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_mem_fieldNormSubgroup_val_normDownRamificationStep :
    ∃ x : Kˣ,
      x ∈ fieldNormSubgroup K M ∧
        (multiplicativeIntegerValuation K).val x =
          (normDownRamificationStepNat (K := K) (L := L) (M := M) : ℤ)

theorem

integerMultipleSubgroup_normDownRamificationStep_le_fieldNormSubgroup

L227 ↗

TameAbhyankar.NAField.integerMultipleSubgroup_normDownRamificationStep_le_fieldNormSubgroup

Documentation

Subgroup-value form of the common-top raw norm-down generator.

Source context 18 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section CommonTopNormDownGenerator
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra K M] [Algebra L M]
variable [IsScalarTower K L M] [Module.Free L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem integerMultipleSubgroup_normDownRamificationStep_le_fieldNormSubgroup :
    integerMultipleSubgroup
        (normDownRamificationStepNat (K := K) (L := L) (M := M) : ℤ) ≤
      (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (fieldNormSubgroup K M)

theorem

exists_mem_fieldNormSubgroup_val_galoisNormDownRamificationStep

L254 ↗

TameAbhyankar.NAField.exists_mem_fieldNormSubgroup_val_galoisNormDownRamificationStep

Documentation

Galois-data form of the concrete common-top norm-down generator.

Source context 18 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisCommonTopNormDownGenerator
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra K M] [Algebra L M]
variable [IsScalarTower K L M] [Module.Free L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem exists_mem_fieldNormSubgroup_val_galoisNormDownRamificationStep :
    ∃ x : Kˣ,
      x ∈ fieldNormSubgroup K M ∧
        (multiplicativeIntegerValuation K).val x =
          (galoisNormDownRamificationStepNat (K := K) (L := L) (M := M) :
            ℤ)

theorem

integerMultipleSubgroup_galoisNormDownRamificationStep_le_fieldNormSubgroup

L265 ↗

TameAbhyankar.NAField.integerMultipleSubgroup_galoisNormDownRamificationStep_le_fieldNormSubgroup

Documentation

Subgroup-value form of the common-top Galois norm-down generator.

Source context 18 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisCommonTopNormDownGenerator
variable {K L M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field M]
variable [Algebra K L] [Algebra K M] [Algebra L M]
variable [IsScalarTower K L M] [Module.Free L M]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem integerMultipleSubgroup_galoisNormDownRamificationStep_le_fieldNormSubgroup :
    integerMultipleSubgroup
        (galoisNormDownRamificationStepNat (K := K) (L := L) (M := M) :
          ℤ) ≤
      (multiplicativeIntegerValuation K).subgroupValueSubgroup
        (fieldNormSubgroup K M)

theorem

nat_lcm_residueDegree_dvd_normDownRamificationStep

L302 ↗

TameAbhyankar.NAField.nat_lcm_residueDegree_dvd_normDownRamificationStep

Documentation

Common-top norm containment forces the lower residue-degree lcm to divide the norm-down Galois ramification step.

Source context 25 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section CommonTop
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [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]
variable [FiniteDimensional K L] [IsGalois K L]
variable [FiniteDimensional K L'] [Algebra.IsSeparable K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]

Lean source · statement

theorem nat_lcm_residueDegree_dvd_normDownRamificationStep :
    Nat.lcm (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      normDownRamificationStepNat (K := K) (L := L) (M := M)

theorem

nat_lcm_galoisResidueDegree_dvd_galoisNormDownRamificationStep

L341 ↗

TameAbhyankar.NAField.nat_lcm_galoisResidueDegree_dvd_galoisNormDownRamificationStep

Documentation

The concrete norm-down ramification-image generator already carries the lcm of the two lower Galois residue degrees.

Source context 25 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisNormDownLcm
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [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]
variable [FiniteDimensional K L] [IsGalois K L]
variable [FiniteDimensional K L'] [IsGalois K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]

Lean source · statement

theorem nat_lcm_galoisResidueDegree_dvd_galoisNormDownRamificationStep :
    Nat.lcm
        (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      galoisNormDownRamificationStepNat (K := K) (L := L) (M := M)

theorem

nat_lcm_galoisResidueDegree_dvd_finrank

L381 ↗

TameAbhyankar.NAField.nat_lcm_galoisResidueDegree_dvd_finrank

Documentation

With the lower L/K invariants supplied by Galois valuation data, the norm-down value-image lcm comparison becomes a field-degree divisibility.

Source context 26 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section CanonicalGaloisInvariants
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [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]
variable [FiniteDimensional K L] [FiniteDimensional L M]
variable [IsGalois K L]
variable [FiniteDimensional K L'] [Algebra.IsSeparable K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]

Lean source · statement

theorem nat_lcm_galoisResidueDegree_dvd_finrank :
    Nat.lcm
        (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank K M

theorem

nat_lcm_galoisResidueDegree_dvd_finrank_both

L427 ↗

TameAbhyankar.NAField.nat_lcm_galoisResidueDegree_dvd_finrank_both

Documentation

If both lower branches are supplied by Neu1999 Galois valuation data, the common-top norm-down comparison gives a top-degree divisibility by the lcm of the two Galois residue degrees.

Source context 26 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section CanonicalGaloisInvariantsBoth
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [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]
variable [FiniteDimensional K L] [FiniteDimensional L M]
variable [IsGalois K L]
variable [FiniteDimensional K L'] [IsGalois K L']
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]

Lean source · statement

theorem nat_lcm_galoisResidueDegree_dvd_finrank_both :
    Nat.lcm
        (Module.finrank 𝓀[K] 𝓀[L])
        (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank K M

theorem

nat_lcm_galoisResidueDegree_dvd_finrank_symm

L468 ↗

TameAbhyankar.NAField.nat_lcm_galoisResidueDegree_dvd_finrank_symm

Documentation

Symmetric field-degree form with the L'/K invariants supplied by Galois valuation data.

Source context 26 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section CanonicalGaloisInvariantsSymm
variable {K L L' M : Type u}
variable [Field K] [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L]
variable [IsNonarchimedeanLocalField L]
variable [Field L'] [ValuativeRel L'] [TopologicalSpace L']
variable [IsNonarchimedeanLocalField L']
variable [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]
variable [FiniteDimensional K L'] [FiniteDimensional L' M]
variable [IsGalois K L']
variable [FiniteDimensional K L] [Algebra.IsSeparable K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L')]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
  (ValuativeRel.valuation L)]

Lean source · statement

theorem nat_lcm_galoisResidueDegree_dvd_finrank_symm :
    Nat.lcm
        (Module.finrank 𝓀[K] 𝓀[L'])
        (Module.finrank 𝓀[K] 𝓀[L]) ∣
      Module.finrank K M

Module documentation

Normed Galois ramification images

Declarations