Module

FieldTower.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Inertia.FieldTower

4 declarations indexed from sourceView source ↗

Module documentation

Inertia in a normal intermediate field

This file isolates the group-theoretic tower map used in the proof of SGA 1, Expose X, Lemma 3.6. A valuation subring A of a field E restricts to a valuation subring of every intermediate field M. When M / K is normal, restriction of automorphisms carries the inertia group of A over K to the inertia group of the restricted valuation.

The kernel is the relative inertia group of E / M, embedded by scalar restriction. No completeness, Henselianity, discreteness, or finiteness is needed for this kernel calculation.

Imports2

Imported by2

theorem

relativeInertiaInclusion_injective

L44 ↗

TameAbhyankar.SGA1.relativeInertiaInclusion_injective

Documentation

Forgetting the intermediate-field scalars embeds relative inertia into the inertia group over the ground field.

Source context 11 commands

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

noncomputable section
universe u v
namespace TameAbhyankar
namespace SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open HilbertRamification
open HilbertRamification.ValuationSubring
variable (K : Type u) {E : Type v} [Field K] [Field E] [Algebra K E]
section Intermediate
variable (M : IntermediateField K E)

Lean source · statement

theorem relativeInertiaInclusion_injective
    (A : _root_.ValuationSubring E) :
    Function.Injective
      (inertiaGroupRestrictScalars (K := K) (M := M) A)

def

inertiaRestriction

L65 ↗

TameAbhyankar.SGA1.inertiaRestriction

Documentation

Restriction from the inertia group over K to the inertia group on a normal intermediate field M.

Source context 11 commands

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

noncomputable section
universe u v
namespace TameAbhyankar
namespace SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open HilbertRamification
open HilbertRamification.ValuationSubring
variable (K : Type u) {E : Type v} [Field K] [Field E] [Algebra K E]
section NormalIntermediate
variable (M : IntermediateField K E) [Normal K M]

Lean source · statement

def inertiaRestriction
    (A : _root_.ValuationSubring E) :
    inertiaGroup K A →*
      inertiaGroup K (A.comap M.val.toRingHom)

theorem

inertiaRestriction_apply_coe

L81 ↗

TameAbhyankar.SGA1.inertiaRestriction_apply_coe

Documentation

The inertia restriction has the expected action on elements of the intermediate field.

Source context 11 commands

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

noncomputable section
universe u v
namespace TameAbhyankar
namespace SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open HilbertRamification
open HilbertRamification.ValuationSubring
variable (K : Type u) {E : Type v} [Field K] [Field E] [Algebra K E]
section NormalIntermediate
variable (M : IntermediateField K E) [Normal K M]

Lean source · statement

theorem inertiaRestriction_apply_coe
    (A : _root_.ValuationSubring E) (sigma : inertiaGroup K A) (x : M) :
    (((((inertiaRestriction K M A sigma :
          inertiaGroup K (A.comap M.val.toRingHom)) :
        decompositionGroup K (A.comap M.val.toRingHom)) :
      M ≃ₐ[K] M) x : M) : E) =
      ((((sigma : inertiaGroup K A) : decompositionGroup K A) :
        E ≃ₐ[K] E) (x : E))

theorem

inertiaRestriction_ker_eq_range_relative

L105 ↗

TameAbhyankar.SGA1.inertiaRestriction_ker_eq_range_relative

Documentation

The relative inertia group I(E/M) embeds into I(E/K) by forgetting scalars. Its range is exactly the kernel of restriction to M.

This is the inertia-group kernel identification in the tower K ⊆ M ⊆ E.

Source context 11 commands

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

noncomputable section
universe u v
namespace TameAbhyankar
namespace SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring
open HilbertRamification
open HilbertRamification.ValuationSubring
variable (K : Type u) {E : Type v} [Field K] [Field E] [Algebra K E]
section NormalIntermediate
variable (M : IntermediateField K E) [Normal K M]

Lean source · statement

theorem inertiaRestriction_ker_eq_range_relative
    (A : _root_.ValuationSubring E) :
    MonoidHom.ker (inertiaRestriction K M A) =
      (inertiaGroupRestrictScalars (K := K) (M := M) A).range

Module documentation

Inertia in a normal intermediate field

Declarations

relativeInertiaInclusion_injective

inertiaRestriction

inertiaRestriction_apply_coe

inertiaRestriction_ker_eq_range_relative