NYLL
Module

HenselianDecomposition.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.HenselianDecomposition
2 declarations indexed from sourceView source ↗

Module documentation

Decomposition over a Henselian valuation ring

Henselianity identifies the selected extension valuation ring with the integral closure, so every base-field automorphism preserves it. Consequently the fixed integers in the residue exact sequence over an intermediate field come from that intermediate field's actual pulled-back valuation ring.

Imports5
Imported by5

Declarations

theorem

decompositionGroup_eq_top_of_henselianRing

L32 ↗
RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup_eq_top_of_henselianRing
Documentation

The decomposition group of an algebraic extension of a Henselian valuation ring is the full automorphism group.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
open scoped Pointwise
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem decompositionGroup_eq_top_of_henselianRing
    [Algebra.IsAlgebraic K L]
    (V : _root_.ValuationSubring K)
    [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (A : _root_.ValuationSubring L) [V.valuation.HasExtension A.valuation] :
    decompositionGroup K A = ⊤
theorem

exists_comap_integer_of_decompositionFixedSubring_of_henselianRing

L59 ↗
RamificationTheory.HilbertRamification.ValuationSubring.exists_comap_integer_of_decompositionFixedSubring_of_henselianRing
Documentation

Every fixed integer used in the residue exact sequence over an intermediate field is the image of an integer in the actual comap valuation ring. No normality or finiteness of the intermediate field is needed.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
open scoped Pointwise
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exists_comap_integer_of_decompositionFixedSubring_of_henselianRing
    [IsGalois K L]
    (V : _root_.ValuationSubring K)
    [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (A : _root_.ValuationSubring L) [V.valuation.HasExtension A.valuation]
    (E : IntermediateField K L) (a : decompositionFixedSubring E A) :
    ∃ b : A.comap E.val.toRingHom, ((b : E) : L) = ((a : A) : L)

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