Nyll.ValuedFieldTheory.Ramification.HilbertRamification.ResidueLift

Module documentation

Lifting residue automorphisms through a decomposition group

For a chosen valuation on a Galois extension, every automorphism of its residue field over the residue field of the decomposition field lifts to an ambient Galois automorphism stabilizing the chosen valuation. This is the elementwise form of the residue-action exact sequence.

theorem

exists_galoisAutomorphism_stabilizing_of_residueAutomorphism

L30 ↗

RamificationTheory.HilbertRamification.ValuationSubring.exists_galoisAutomorphism_stabilizing_of_residueAutomorphism

Documentation

Every residue-field automorphism over the residue field of the decomposition field is induced by an ambient Galois automorphism stabilizing the selected valuation ring.

Source context 5 commands

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

noncomputable section
universe u v
namespace RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

theorem exists_galoisAutomorphism_stabilizing_of_residueAutomorphism
    (A : _root_.ValuationSubring L)
    (tau : selectedResidueField A ≃ₐ[decompositionResidueField K A]
      selectedResidueField A) :
    ∃ sigma : L ≃ₐ[K] L,
      ∃ hsigma : sigma ∈ decompositionGroup K A,
        decompositionGroupResidueAction (K := K) A ⟨sigma, hsigma⟩ = tau

Module documentation

Lifting residue automorphisms through a decomposition group

Declarations

exists_galoisAutomorphism_stabilizing_of_residueAutomorphism