NYLL
Module

NormDownPrimitive.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Galois.NormDownPrimitive
4 declarations indexed from sourceView source ↗

Module documentation

Primitive divisors from Galois norm-down lcm sources

This file contains the arithmetic cancellation layer on top of NAField.GaloisNormDown: once the norm-down construction has supplied an lcm divisor, these lemmas extract the primitive residue-degree factor by cancelling the visible lower residue degree.

Imports1
Imported by1

Declarations

theorem

residueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex

L54 ↗
TameAbhyankar.NAField.residueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex
Documentation

Cancelling the visible f(K,L) factor from the norm-down ramification step, the primitive part of the other lower residue degree divides the powered Galois ramification step.

Source context 24 commands

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

noncomputable section
universe u
namespace TameAbhyankar
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 residueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex :
    Module.finrank 𝓀[K] 𝓀[L'] /
        Nat.gcd (Module.finrank 𝓀[K] 𝓀[L])
          (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank L M *
        Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
theorem

galoisResidueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex

L103 ↗
TameAbhyankar.NAField.galoisResidueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex
Documentation

With both lower branches supplied by Neu1999 Galois valuation data, the primitive residue-degree divisor is sourced entirely from Galois data.

Source context 24 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisPrimitiveDivisors
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 galoisResidueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex :
    Module.finrank 𝓀[K] 𝓀[L'] /
        Nat.gcd
          (Module.finrank 𝓀[K] 𝓀[L])
          (Module.finrank 𝓀[K] 𝓀[L']) ∣
      Module.finrank L M *
        Ideal.ramificationIdx (𝓂[L] : Ideal 𝒪[L]) 𝒪[K]
theorem

galoisResidueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex_symm

L132 ↗
TameAbhyankar.NAField.galoisResidueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex_symm
Documentation

Symmetric Galois-data primitive divisor for the L' branch.

Source context 24 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section GaloisPrimitiveDivisors
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 galoisResidueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex_symm :
    Module.finrank 𝓀[K] 𝓀[L] /
        Nat.gcd
          (Module.finrank 𝓀[K] 𝓀[L'])
          (Module.finrank 𝓀[K] 𝓀[L]) ∣
      Module.finrank L' M *
        Ideal.ramificationIdx (𝓂[L'] : Ideal 𝒪[L']) 𝒪[K]
theorem

residueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex_symm

L169 ↗
TameAbhyankar.NAField.residueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex_symm
Documentation

Symmetric branch form: applying the norm-down construction to the L' branch gives the primitive residue-degree divisor for L.

Source context 24 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory.DiscreteValuationField
open scoped ValuativeRel
namespace NAField
section CommonTopSymm
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 residueDegreePrimitive_dvd_finrank_mul_galoisRamificationIndex_symm :
    Module.finrank 𝓀[K] 𝓀[L] /
        Nat.gcd (Module.finrank 𝓀[K] 𝓀[L'])
          (Module.finrank 𝓀[K] 𝓀[L]) ∣
      Module.finrank L' M *
        Ideal.ramificationIdx (𝓂[L'] : Ideal 𝒪[L']) 𝒪[K]

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