Module

FiniteRamificationPrimary.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteRamificationPrimary

2 declarations indexed from sourceView source ↗

Module documentation

Finite ramification groups in positive and zero residue characteristic

In positive residue characteristic p, factoring a finite annihilating order as p^a times a prime-to-p integer reduces the assertion to prime-to-residue torsion triviality. In residue characteristic zero, every positive finite order is nonzero in the residue field, so the ramification group is trivial.

All groups and principal-unit conditions are the actual valuation-subring constructions. Only finiteness of the ramification group is used; no normality, Henselianity, discreteness, perfectness, or finite residue field is required.

Imports6

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RamificationPrimeToResidueTorsion
Mathlib.Algebra.Group.Subgroup.Finite
Mathlib.Algebra.CharP.Defs
Mathlib.Data.Nat.Factorization.Basic
Mathlib.GroupTheory.OrderOfElement
Mathlib.GroupTheory.PGroup

Imported by7

theorem

ramificationGroup_isPGroup_of_residueChar

L36 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup_isPGroup_of_residueChar

Documentation

The actual finite ramification group is a p-group in residue characteristic p.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem ramificationGroup_isPGroup_of_residueChar
    (A : _root_.ValuationSubring L) (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField A) p] [Finite (ramificationGroup K A)] :
    IsPGroup p (ramificationGroup K A)

theorem

ramificationGroup_eq_bot_of_residueCharZero

L50 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup_eq_bot_of_residueCharZero