Module

RamificationGroup.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.CyclicInertia.RamificationGroup

3 declarations indexed from sourceView source ↗

Module documentation

Wild ramification groups

This file contains the orbit-sum argument controlling the wild ramification group. The same field calculation supplies both branches needed by tame inertia: the ramification group is trivial in residue characteristic zero, and it is a p-group in positive residue characteristic p.

Imports7

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.CharacterMap
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ResidueField
Mathlib.Algebra.CharP.Lemmas
Mathlib.Algebra.BigOperators.Field
Mathlib.Data.Nat.Factors
Mathlib.GroupTheory.PGroup
Mathlib.GroupTheory.Perm.Cycle.Type

Imported by2

theorem

residue_natCast_eq_zero_of_ramification_prime_order

L38 ↗

TameAbhyankar.SGA1.TameInertiaRamification.residue_natCast_eq_zero_of_ramification_prime_order

Documentation

The orbit sum of a nontrivial ramification automorphism of prime order forces that prime to vanish in the residue field.

Source context 5 commands

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

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

Lean source · statement

theorem residue_natCast_eq_zero_of_ramification_prime_order
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L)
    (ell : ℕ) (sigma : ramificationGroup K V)
    (hsigmaOrder : orderOf sigma = ell) (hsigma : sigma ≠ 1) :
    (ell : IsLocalRing.ResidueField V) = 0

theorem

ramificationGroup_eq_bot_of_residue_charZero

L127 ↗

TameAbhyankar.SGA1.TameInertiaRamification.ramificationGroup_eq_bot_of_residue_charZero

Documentation

In residue characteristic zero the ramification group is trivial.

Source context 5 commands

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

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

Lean source · statement

theorem ramificationGroup_eq_bot_of_residue_charZero
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [CharZero (IsLocalRing.ResidueField V)]
    [Finite (ramificationGroup K V)] :
    ramificationGroup K V = ⊥

theorem

ramificationGroup_isPGroup_of_residue_charP

L151 ↗

TameAbhyankar.SGA1.TameInertiaRamification.ramificationGroup_isPGroup_of_residue_charP

Documentation

A finite ramification group is a p-group when the residue field has positive prime characteristic p.

Source context 5 commands

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

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

Lean source · statement

theorem ramificationGroup_isPGroup_of_residue_charP
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) (p : ℕ)
    [Fact p.Prime] [CharP (IsLocalRing.ResidueField V) p]
    [Finite (ramificationGroup K V)] :
    IsPGroup p (ramificationGroup K V)

Module documentation

Wild ramification groups

Declarations

residue_natCast_eq_zero_of_ramification_prime_order

ramificationGroup_eq_bot_of_residue_charZero

ramificationGroup_isPGroup_of_residue_charP