Module

Core.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.CyclicInertia.Core

3 declarations indexed from sourceView source ↗

Module documentation

Tame-inertia cyclicity core

The production inertia character embeds tame inertia into the residue field after coprimality kills the wild ramification kernel. This file contains that character argument and the comparison with ideal inertia.

Imports2

Nyll.SchemeTheory.AbhyankarLemma.Geometry.CyclicInertia.RamificationGroup
Mathlib.RingTheory.IntegralDomain

Imported by3

theorem

character_evaluation_injective_of_isCyclic

L29 ↗

TameAbhyankar.SGA1.TameInertiaCyclicCore.character_evaluation_injective_of_isCyclic

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1.TameInertiaCyclicCore
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem character_evaluation_injective_of_isCyclic
    (X k : Type*) [Group X] [IsCyclic X] [Field k] :
    ∃ x : X, Function.Injective
      (((MonoidHom.eval : X →* (X →* kˣ) →* kˣ) x))

theorem

inertiaGroup_isCyclic_of_card_coprime_ringExpChar

L46 ↗

TameAbhyankar.SGA1.TameInertiaCyclicCore.inertiaGroup_isCyclic_of_card_coprime_ringExpChar

Documentation

The production inertia character embeds tame inertia into the residue field once ringExpChar coprimality kills its ramification kernel.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1.TameInertiaCyclicCore
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem inertiaGroup_isCyclic_of_card_coprime_ringExpChar
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L)
    [Finite (inertiaGroup K V)]
    (hvalue : valueTrivialInertiaGroup K V = ⊤)
    [IsCyclic
      ((Lˣ ⧸ V.unitGroup) ⧸ baseUnitValueClassSubgroup K V)]
    (hcop : Nat.Coprime (Nat.card (inertiaGroup K V))
      (ringExpChar (IsLocalRing.ResidueField V))) :
    IsCyclic (inertiaGroup K V)

theorem

valuationSubring_maximalIdeal_inertia_eq

L122 ↗

TameAbhyankar.SGA1.TameInertiaCyclicCore.valuationSubring_maximalIdeal_inertia_eq

Documentation

Ideal inertia at the maximal ideal of a valuation subring agrees with the kernel-of-residue-action inertia group.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1.TameInertiaCyclicCore
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem valuationSubring_maximalIdeal_inertia_eq
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) :
    (IsLocalRing.maximalIdeal V).toAddSubgroup.inertia
        (decompositionGroup K V) = inertiaGroup K V

Module documentation

Tame-inertia cyclicity core

Declarations

character_evaluation_injective_of_isCyclic

inertiaGroup_isCyclic_of_card_coprime_ringExpChar

valuationSubring_maximalIdeal_inertia_eq