Module

FieldPrincipalWildOrder.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FieldPrincipalWildOrder

4 declarations indexed from sourceView source ↗

Module documentation

Orders of field automorphisms acting by principal units

For a valuation ring with finite decomposition group, a compatible surjective ring map acting by principal-unit multipliers gives a field automorphism of p-power order in positive residue characteristic p. In residue characteristic zero, that automorphism is trivial.

Imports2

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingPrincipalWildPrimary
Mathlib.RingTheory.Valuation.RamificationGroup

Imported by2

theorem

mem_decomposition_of_surjective_ring_square

L27 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.mem_decomposition_of_surjective_ring_square

Source context 5 commands

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

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

Lean source · statement

theorem mem_decomposition_of_surjective_ring_square
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) (σ : L ≃ₐ[K] L) (τ : V →+* V) (hτ : Function.Surjective τ)
    (hfield : V.subtype.comp τ = σ.toRingHom.comp V.subtype) :
    σ ∈ decompositionGroup K V

theorem

native_principalUnitMultipliers_of_ring_square

L48 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.native_principalUnitMultipliers_of_ring_square

Source context 5 commands

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

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

Lean source · statement

theorem native_principalUnitMultipliers_of_ring_square
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) (σ : decompositionGroup K V) (τ : V →+* V)
    (hfield : V.subtype.comp τ = (σ : L ≃ₐ[K] L).toRingHom.comp V.subtype)
    (hprincipal : ∀ x : V, ∃ a : Vˣ,
      τ x = x * (a : V) ∧ (a : V) - 1 ∈ IsLocalRing.maximalIdeal V) :
    ∀ x : V, ∃ a : Vˣ,
      σ • x = x * (a : V) ∧ (a : V) - 1 ∈ IsLocalRing.maximalIdeal V

theorem

fieldAutomorphism_pow_prime_eq_one_of_local_principal_units

L66 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.fieldAutomorphism_pow_prime_eq_one_of_local_principal_units

Documentation

The actual field automorphism has p-power order when its actual local ring automorphism acts by principal units. The native decomposition element and its Hilbert ramification membership are constructed from the square.

Source context 5 commands

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

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

Lean source · statement

theorem fieldAutomorphism_pow_prime_eq_one_of_local_principal_units
    (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)]
    (σ : L ≃ₐ[K] L) (τ : V →+* V) (hτ : Function.Surjective τ)
    (hfield : V.subtype.comp τ = σ.toRingHom.comp V.subtype)
    (hprincipal : ∀ x : V, ∃ a : Vˣ,
      τ x = x * (a : V) ∧ (a : V) - 1 ∈ IsLocalRing.maximalIdeal V) :
    ∃ n : ℕ, σ ^ (p ^ n) = 1

theorem

fieldAutomorphism_eq_one_of_local_principal_units_charZero

L86 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.fieldAutomorphism_eq_one_of_local_principal_units_charZero

Documentation

The actual field automorphism is trivial in residue characteristic zero when its actual local ring automorphism acts by principal units.

Source context 5 commands

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

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

Lean source · statement

theorem fieldAutomorphism_eq_one_of_local_principal_units_charZero
    (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)]
    (σ : L ≃ₐ[K] L) (τ : V →+* V) (hτ : Function.Surjective τ)
    (hfield : V.subtype.comp τ = σ.toRingHom.comp V.subtype)
    (hprincipal : ∀ x : V, ∃ a : Vˣ,
      τ x = x * (a : V) ∧ (a : V) - 1 ∈ IsLocalRing.maximalIdeal V) : σ = 1

Module documentation

Orders of field automorphisms acting by principal units

Declarations

mem_decomposition_of_surjective_ring_square

native_principalUnitMultipliers_of_ring_square

fieldAutomorphism_pow_prime_eq_one_of_local_principal_units

fieldAutomorphism_eq_one_of_local_principal_units_charZero