Module

RingPrincipalWildPrimary.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingPrincipalWildPrimary

5 declarations indexed from sourceView source ↗

Module documentation

The actual ring-character wild kernel is primary

The ring predicate is first put in actual ideal inertia. The native Hilbert predicate comparison then supplies the ramification element and its p-power order. The final ring-kernel scope consumes this proved order statement and does not simultaneously open the two Hilbert subgroup types.

Imports5

Imported by2

theorem

principalUnitMultipliers_mem_inertia

L28 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.principalUnitMultipliers_mem_inertia

Source context 3 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v

Lean source · statement

theorem principalUnitMultipliers_mem_inertia
    (R : Type u) [CommRing R] [IsLocalRing R]
    (G : Type v) [Group G] [MulSemiringAction G R] (σ : G)
    (hσ : ∀ x : R, ∃ a : Rˣ,
      σ • x = x * (a : R) ∧ (a : R) - 1 ∈ IsLocalRing.maximalIdeal R) :
    σ ∈ (IsLocalRing.maximalIdeal R).inertia G

theorem

principalUnitMultipliers_pow_prime_eq_one

L42 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.principalUnitMultipliers_pow_prime_eq_one

Documentation

A decomposition element acting by principal units has prime-power order in residue characteristic p.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
open _root_.RamificationTheory.HilbertRamification.ValuationSubring in

Lean source · statement

theorem principalUnitMultipliers_pow_prime_eq_one
    (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 (decompositionGroup K V)]
    (σ : decompositionGroup K V)
    (hσ : ∀ x : V, ∃ a : Vˣ,
      σ • x = x * (a : V) ∧ (a : V) - 1 ∈ IsLocalRing.maximalIdeal V) :
    ∃ n : ℕ, σ ^ (p ^ n) = 1

theorem

principalUnitMultipliers_eq_one_of_residueCharZero

L66 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.principalUnitMultipliers_eq_one_of_residueCharZero

Documentation

A decomposition element acting by principal units is trivial in residue characteristic zero.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
open _root_.RamificationTheory.HilbertRamification.ValuationSubring in

Lean source · statement

theorem principalUnitMultipliers_eq_one_of_residueCharZero
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L)
    [CharZero (IsLocalRing.ResidueField V)] [Finite (decompositionGroup K V)]
    (σ : decompositionGroup K V)
    (hσ : ∀ x : V, ∃ a : Vˣ,
      σ • x = x * (a : V) ∧ (a : V) - 1 ∈ IsLocalRing.maximalIdeal V) : σ = 1

theorem

principalUnitInertia_isPGroup_of_residueChar

L87 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.principalUnitInertia_isPGroup_of_residueChar

Documentation

The literal ring-character kernel for the native finite decomposition action is a p-group. Actual Hilbert ramification supplies the p-power order.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
open _root_.RamificationTheory.HilbertRamification.ValuationSubring in

Lean source · statement

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

theorem

principalUnitInertia_eq_bot_of_residueCharZero

L107 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.principalUnitInertia_eq_bot_of_residueCharZero

Documentation

In residue characteristic zero, the actual ring-character wild kernel for a finite decomposition action is trivial.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
open _root_.RamificationTheory.HilbertRamification.ValuationSubring in

Lean source · statement

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

Module documentation

The actual ring-character wild kernel is primary

Declarations

principalUnitMultipliers_mem_inertia

principalUnitMultipliers_pow_prime_eq_one

principalUnitMultipliers_eq_one_of_residueCharZero

principalUnitInertia_isPGroup_of_residueChar

principalUnitInertia_eq_bot_of_residueCharZero