ModuleGaloisInvariants.lean
Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.GaloisInvariants
2 declarations indexed from sourceView source ↗ Module documentation
Galois valued-extension invariant bridges
This file records the field-degree identities for finite Galois extensions whose canonical valuations form an extension. These identities keep the later ramification-image comparison tied to the actual ramification index and residue-field degree instead of assuming a separate endpoint comparison.
Declarations
TameAbhyankar.NAField.galoisNormDownRamificationStepNat
DocumentationThe explicit norm-down step built from Galois valuation data: the Galois residue degree of L/K, then the upper field degree [M : L], then the Galois ramification index of L/K.
Source context 17 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace TameAbhyankar
open scoped ValuativeRel
namespace NAField
section GaloisData
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] [Algebra K M]
variable [IsScalarTower K L M]
variable [FiniteDimensional K L] [FiniteDimensional L M]
variable [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
(ValuativeRel.valuation L)]
TameAbhyankar.NAField.galoisNormDownRamificationStepNat_eq_finrank
DocumentationThe explicit Galois norm-down ramification step is the whole top field degree [M : K].
Source context 17 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace TameAbhyankar
open scoped ValuativeRel
namespace NAField
section GaloisData
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] [Algebra K M]
variable [IsScalarTower K L M]
variable [FiniteDimensional K L] [FiniteDimensional L M]
variable [IsGalois K L]
variable [Valuation.HasExtension (ValuativeRel.valuation K)
(ValuativeRel.valuation L)]