NYLL
Module

FiniteOrderValuation.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteOrderValuation
3 declarations indexed from sourceView source ↗

Module documentation

Finite-order decomposition and valuation values

A finite-order decomposition element fixes the original valuation's values. Consequently every finite inertia element lies in the value-trivial subgroup.

Imports3
Imported by5

Declarations

theorem

valuation_decomposition_apply_eq_of_isOfFinOrder

L29 ↗
RamificationTheory.HilbertRamification.ValuationSubring.valuation_decomposition_apply_eq_of_isOfFinOrder
Documentation

A finite-order element of the valuation-subring decomposition group fixes all values. The induced map on the canonical value group is monotone, and a positive iterate equal to the identity forces a monotone map to be the identity.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
noncomputable section
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem valuation_decomposition_apply_eq_of_isOfFinOrder
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A)
    (hσ : IsOfFinOrder σ) (x : L) :
    A.valuation ((σ : L ≃ₐ[K] L) x) = A.valuation x
theorem

mem_valueTrivialInertiaGroup_of_isOfFinOrder

L75 ↗
RamificationTheory.HilbertRamification.ValuationSubring.mem_valueTrivialInertiaGroup_of_isOfFinOrder
Documentation

Each finite-order inertia element lies in the actual value-trivial subgroup.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
noncomputable section
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem mem_valueTrivialInertiaGroup_of_isOfFinOrder
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A)
    (hσ : IsOfFinOrder σ) : σ ∈ valueTrivialInertiaGroup K A
theorem

valueTrivialInertiaGroup_eq_top_of_finite

L92 ↗
RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaGroup_eq_top_of_finite
Documentation

Finite inertia acts trivially on the actual value group, without any finiteness assumption on the full group of field automorphisms.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
noncomputable section
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem valueTrivialInertiaGroup_eq_top_of_finite
    (A : _root_.ValuationSubring L) [Finite (inertiaGroup K A)] :
    valueTrivialInertiaGroup K A = ⊤

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.