Module

AbsoluteValueConjugacy.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.AbsoluteValueConjugacy

8 declarations indexed from sourceView source ↗

Module documentation

Valuation conjugacy

For a possibly infinite Galois extension L/K, the Galois group acts transitively on the extensions to L of a nontrivial absolute value of K.

Imports22

Imported by4

def

absoluteValueConjugate_extends

L59 ↗

AlgebraicNumberTheory.Valuations.absoluteValueConjugate_extends

Documentation

Conjugating an extension by a ground-field automorphism gives another exact extension of the same base absolute value.

Source context 4 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem absoluteValueConjugate_extends
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (w : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L) :
    AbsoluteValue.Extends vK (absoluteValueConjugate w.1 σ)

def

absoluteValueExtensionConjugate

L68 ↗

AlgebraicNumberTheory.Valuations.absoluteValueExtensionConjugate

Documentation

The conjugated extension as an element of the exact-extension type.

Source context 4 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

def absoluteValueExtensionConjugate
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (w : AbsoluteValueExtension vK L)
    (σ : L ≃ₐ[K] L) : AbsoluteValueExtension vK L

theorem

equivalent_exactExtensions_eq

L78 ↗

AlgebraicNumberTheory.Valuations.equivalent_exactExtensions_eq

Documentation

Equivalent exact extensions of a nontrivial base absolute value are equal. Thus AbsoluteValueExtension vK L is a faithful normalized model for the absolute-value classes lying over the class of vK.

Source context 4 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem equivalent_exactExtensions_eq
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w w' : AbsoluteValueExtension vK L)
    (h : LubinTate.Valuations.EquivalentAbsoluteValues w.1 w'.1) :
    w = w'

theorem

absoluteValueConjugacy_exists_conjugatingAlgEquiv

L100 ↗

AlgebraicNumberTheory.Valuations.absoluteValueConjugacy_exists_conjugatingAlgEquiv

Documentation

Normality descent for the embeddings supplied by the valuation-extension theorem: two exact extensions differ by an actual K-automorphism of L, not merely by an automorphism of the ambient algebraic closure.

Source context 4 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem absoluteValueConjugacy_exists_conjugatingAlgEquiv
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [IsGalois K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w w' : AbsoluteValueExtension vK L) :
    ∃ σ : L ≃ₐ[K] L, w'.1 = absoluteValueConjugate w.1 σ

theorem