NYLL
Module

FixedFieldMaximality.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FixedFieldMaximality
6 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: fixed-field maximality

This file records the fixed-field maximality statements behind the inertia-field maximality theorem and the ramification-field maximality theorem. The valuation-theoretic words "unramified" and "tamely ramified" still require the unramified and tame ramification API; the purely Galois-theoretic part is already available: a subextension lies in Z_w, T_w, or V_w exactly when the corresponding canonical subgroup acts trivially on it.

Imports1
Imported by1

Declarations

theorem

le_decompositionField_iff

L37 ↗
RamificationTheory.HilbertRamification.ValuationSubring.le_decompositionField_iff
Documentation

The localization and decomposition comparison gives: Z_w is the largest intermediate field of L/K on which G_w acts trivially.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem le_decompositionField_iff
    (A : _root_.ValuationSubring L) (E : IntermediateField K L) :
    E ≤ decompositionField K A ↔
      ∀ σ : decompositionGroup K A, ∀ x : E,
        ((σ : L ≃ₐ[K] L) (x : L)) = x
theorem

le_inertiaField_iff

L54 ↗
RamificationTheory.HilbertRamification.ValuationSubring.le_inertiaField_iff
Documentation

The inertia field satisfies: T_w is the largest intermediate field of L/K on which I_w acts trivially.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem le_inertiaField_iff
    (A : _root_.ValuationSubring L) (E : IntermediateField K L) :
    E ≤ inertiaField K A ↔
      ∀ σ : inertiaGroup K A, ∀ x : E,
        ((σ : decompositionGroup K A) : L ≃ₐ[K] L) (x : L) = x
theorem

le_ramificationField_iff

L70 ↗
RamificationTheory.HilbertRamification.ValuationSubring.le_ramificationField_iff
Documentation

The ramification field satisfies: V_w is the largest intermediate field of L/K on which R_w acts trivially.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem le_ramificationField_iff
    (A : _root_.ValuationSubring L) (E : IntermediateField K L) :
    E ≤ ramificationField K A ↔
      ∀ σ : ramificationGroup K A, ∀ x : E,
        (((σ : inertiaGroup K A) : decompositionGroup K A) :
          L ≃ₐ[K] L) (x : L) = x
theorem

le_inertiaFieldOverDecompositionField_iff

L88 ↗
RamificationTheory.HilbertRamification.ValuationSubring.le_inertiaFieldOverDecompositionField_iff
Documentation

Inertia-field maximality: over the decomposition field Z_w, T_w is the largest subextension of L/Z_w on which I_w acts trivially.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem le_inertiaFieldOverDecompositionField_iff
    (A : _root_.ValuationSubring L)
    (E : IntermediateField (decompositionField K A) L) :
    E ≤ inertiaFieldOverDecompositionField K A ↔
      ∀ σ : inertiaGroup K A, ∀ x : E,
        ((σ : decompositionGroup K A) : L ≃ₐ[K] L) (x : L) = x
theorem

le_ramificationFieldOverInertiaField_iff

L107 ↗
RamificationTheory.HilbertRamification.ValuationSubring.le_ramificationFieldOverInertiaField_iff
Documentation

Ramification-field maximality: over the inertia field T_w, V_w is the largest subextension of L/T_w on which R_w acts trivially.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem le_ramificationFieldOverInertiaField_iff
    (A : _root_.ValuationSubring L)
    (E : IntermediateField (inertiaField K A) L) :
    E ≤ ramificationFieldOverInertiaField K A ↔
      ∀ σ : ramificationGroup K A, ∀ x : E,
        (((σ : inertiaGroup K A) : decompositionGroup K A) :
          L ≃ₐ[K] L) (x : L) = x
theorem

le_ramificationFieldOverDecompositionField_iff

L127 ↗
RamificationTheory.HilbertRamification.ValuationSubring.le_ramificationFieldOverDecompositionField_iff
Documentation

Ramification-field maximality: over the decomposition field Z_w, V_w is the largest subextension of L/Z_w on which R_w acts trivially.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem le_ramificationFieldOverDecompositionField_iff
    (A : _root_.ValuationSubring L)
    (E : IntermediateField (decompositionField K A) L) :
    E ≤ ramificationFieldOverDecompositionField K A ↔
      ∀ σ : ramificationGroup K A, ∀ x : E,
        (((σ : inertiaGroup K A) : decompositionGroup K A) :
          L ≃ₐ[K] L) (x : L) = x

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