Module

FiniteInertiaStructure.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteInertiaStructure

4 declarations indexed from sourceView source ↗

Module documentation

Structure of finite inertia

The actual residue-unit character has ramification kernel. Finite inertia fixes values, so this character is defined on all inertia. In residue characteristic zero its kernel is trivial and inertia is commutative. In residue characteristic p every p-subgroup lies in the ramification kernel, which is itself a p-group.

Imports5

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteRamificationPrimary
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteOrderValuation
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.CharacterMap
Mathlib.Algebra.CharP.Reduced
Mathlib.GroupTheory.Sylow

Imported by6

theorem

inertiaGroup_isMulCommutative_of_residueCharZero

L29 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup_isMulCommutative_of_residueCharZero

Documentation

Finite inertia is commutative in residue characteristic zero.

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 inertiaGroup_isMulCommutative_of_residueCharZero
    (A : _root_.ValuationSubring L) [Finite (inertiaGroup K A)]
    [CharZero (IsLocalRing.ResidueField A)] :
    IsMulCommutative (inertiaGroup K A)

theorem

pSubgroup_le_ramificationGroup_of_residueChar

L54 ↗

RamificationTheory.HilbertRamification.ValuationSubring.pSubgroup_le_ramificationGroup_of_residueChar

Documentation

Every p-subgroup of inertia lies in the actual ramification group.

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 pSubgroup_le_ramificationGroup_of_residueChar
    (A : _root_.ValuationSubring L) (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField A) p]
    (P : Subgroup (inertiaGroup K A)) (hP : IsPGroup p P) :
    P ≤ ramificationGroup K A

theorem

sylow_eq_ramificationGroup_of_residueChar

L86 ↗

RamificationTheory.HilbertRamification.ValuationSubring.sylow_eq_ramificationGroup_of_residueChar

Documentation

The actual ramification group is the unique Sylow p-subgroup of finite inertia.

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 sylow_eq_ramificationGroup_of_residueChar
    (A : _root_.ValuationSubring L) (p : ℕ) [Fact p.Prime]
    [Finite (inertiaGroup K A)] [CharP (IsLocalRing.ResidueField A) p]
    (P : Sylow p (inertiaGroup K A)) :
    (P : Subgroup (inertiaGroup K A)) = ramificationGroup K A

theorem

ramificationGroup_eq_bot_iff_residueChar_not_dvd_inertia_card

L97 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup_eq_bot_iff_residueChar_not_dvd_inertia_card

Documentation

In positive residue characteristic, the actual finite ramification group is trivial exactly when the residue characteristic does not divide the order of inertia.

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_eq_bot_iff_residueChar_not_dvd_inertia_card
    (A : _root_.ValuationSubring L) (p : ℕ) [Fact p.Prime]
    [Finite (inertiaGroup K A)]
    [CharP (IsLocalRing.ResidueField A) p] :
    ramificationGroup K A = ⊥ ↔
      ¬ p ∣ Nat.card (inertiaGroup K A)

Module documentation

Structure of finite inertia

Declarations

inertiaGroup_isMulCommutative_of_residueCharZero

pSubgroup_le_ramificationGroup_of_residueChar

sylow_eq_ramificationGroup_of_residueChar

ramificationGroup_eq_bot_iff_residueChar_not_dvd_inertia_card