Module

DecompositionFieldExtension.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.DecompositionFieldExtension

5 declarations indexed from sourceView source ↗

Module documentation

Decomposition-field extension comparison

This file starts with clause (i): the restriction of w to its decomposition field has a unique extension back to L. The proof works for finite or infinite Galois extensions and for archimedean or nonarchimedean valuations.

Imports1

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.DecompositionField

Imported by2

def

absoluteValueRestrictIntermediateField

L27 ↗

AlgebraicNumberTheory.Valuations.absoluteValueRestrictIntermediateField

Documentation

Restriction of an absolute value on L to an intermediate field.

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 absoluteValueRestrictIntermediateField
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (w : AbsoluteValue L ℝ) (E : IntermediateField K L) : AbsoluteValue E ℝ

theorem

absoluteValueRestrictIntermediateField_apply

L32 ↗

AlgebraicNumberTheory.Valuations.absoluteValueRestrictIntermediateField_apply

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 absoluteValueRestrictIntermediateField_apply
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (w : AbsoluteValue L ℝ) (E : IntermediateField K L) (x : E) :
    absoluteValueRestrictIntermediateField w E x = w (x : L)

theorem

absoluteValueRestrictIntermediateField_isNontrivial

L40 ↗

AlgebraicNumberTheory.Valuations.absoluteValueRestrictIntermediateField_isNontrivial

Documentation

Restricting an extension to an intermediate field that contains the base preserves nontriviality.

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 absoluteValueRestrictIntermediateField_isNontrivial
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L) (E : IntermediateField K L) :
    (absoluteValueRestrictIntermediateField w.1 E).IsNontrivial

def

absoluteValueExtensionOverRestriction

L57 ↗

AlgebraicNumberTheory.Valuations.absoluteValueExtensionOverRestriction

Documentation

Regard w as an exact extension of its restriction to an intermediate field.

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 absoluteValueExtensionOverRestriction
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    (w : AbsoluteValue L ℝ) (E : IntermediateField K L) :
    AbsoluteValueExtension
      (absoluteValueRestrictIntermediateField w E) L

theorem

decompositionField_unique_extension_over_decompositionField

L66 ↗

AlgebraicNumberTheory.Valuations.decompositionField_unique_extension_over_decompositionField

Documentation

The decomposition-field extension comparison: w|Z_w has exactly one extension to L.

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 decompositionField_unique_extension_over_decompositionField
    {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
    [IsGalois K L]
    (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
    (w : AbsoluteValueExtension vK L)
    (w' : AbsoluteValueExtension
      (absoluteValueRestrictIntermediateField w.1
        (HilbertRamification.absoluteValueDecompositionField K w.1)) L) :
    w' = absoluteValueExtensionOverRestriction w.1
      (HilbertRamification.absoluteValueDecompositionField K w.1)

Module documentation

Decomposition-field extension comparison

Declarations

absoluteValueRestrictIntermediateField

absoluteValueRestrictIntermediateField_apply

absoluteValueRestrictIntermediateField_isNontrivial

absoluteValueExtensionOverRestriction

decompositionField_unique_extension_over_decompositionField