NYLL
Module

RamificationField.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RamificationField
23 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: ramification field

This file contains the fixed-field part of the ramification-field definition, over the decomposition field Z_w. The base valuation-subring file owns the definitions of G_w, I_w, R_w, Z_w, T_w, and V_w; here we record the tower-level Galois correspondence for G(L / V_w) as a subgroup of G(L / Z_w).

Imports1
Imported by2

Declarations

def

inertiaGroupEquivGalInertiaField_of_finiteDimensional

L34 ↗
RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupEquivGalInertiaField_of_finiteDimensional
Documentation

Prime-decomposition statement: identify inertia with the Galois group over the inertia field.

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
def inertiaGroupEquivGalInertiaField_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    inertiaGroup K A ≃* (L ≃ₐ[inertiaField K A] L)
instance

inertiaField_isGalois

L41 ↗
RamificationTheory.HilbertRamification.ValuationSubring.inertiaField_isGalois
Documentation

L/T_w is Galois because T_w is the fixed field of the inertia group.

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
instance inertiaField_isGalois
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    IsGalois (inertiaField K A) L
theorem

inertiaGroupEquivGalInertiaField_of_finiteDimensional_apply

L47 ↗
RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupEquivGalInertiaField_of_finiteDimensional_apply
Documentation

States the theorem inertiaGroupEquivGalInertiaField_of_finiteDimensional_apply.

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 inertiaGroupEquivGalInertiaField_of_finiteDimensional_apply
    [FiniteDimensional K L] (A : _root_.ValuationSubring L)
    (σ : inertiaGroup K A) (x : L) :
    inertiaGroupEquivGalInertiaField_of_finiteDimensional (K := K) A σ x =
      ((σ : decompositionGroup K A) : L ≃ₐ[K] L) x
theorem

mem_ramificationFieldOverInertiaField_iff

L55 ↗
RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationFieldOverInertiaField_iff
Documentation

States the theorem mem_ramificationFieldOverInertiaField_iff.

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 mem_ramificationFieldOverInertiaField_iff
    (A : _root_.ValuationSubring L) (x : L) :
    x ∈ ramificationFieldOverInertiaField K A ↔
      ∀ σ : ramificationGroup K A,
        (((σ : inertiaGroup K A) : decompositionGroup K A) : L ≃ₐ[K] L) x = x
def

ramificationGroupToGalInertiaField

L65 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupToGalInertiaField
Documentation

The ramification field satisfies: view R_w as a subgroup of G(L/T_w).

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
def ramificationGroupToGalInertiaField
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    ramificationGroup K A →* (L ≃ₐ[inertiaField K A] L)
theorem

ramificationGroupToGalInertiaField_apply

L72 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupToGalInertiaField_apply
Documentation

States the theorem ramificationGroupToGalInertiaField_apply.

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 ramificationGroupToGalInertiaField_apply
    [FiniteDimensional K L] (A : _root_.ValuationSubring L)
    (σ : ramificationGroup K A) (x : L) :
    ramificationGroupToGalInertiaField (K := K) A σ x =
      (((σ : inertiaGroup K A) : decompositionGroup K A) : L ≃ₐ[K] L) x
abbrev

ramificationGroupOverInertiaField

L81 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupOverInertiaField
Documentation

The ramification field satisfies: the transported ramification subgroup inside G(L/T_w).

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
abbrev ramificationGroupOverInertiaField
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    Subgroup (L ≃ₐ[inertiaField K A] L)
theorem

mem_ramificationGroupOverInertiaField_iff

L87 ↗
RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroupOverInertiaField_iff
Documentation

States the theorem mem_ramificationGroupOverInertiaField_iff.

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 mem_ramificationGroupOverInertiaField_iff
    [FiniteDimensional K L] (A : _root_.ValuationSubring L)
    (σ : L ≃ₐ[inertiaField K A] L) :
    σ ∈ ramificationGroupOverInertiaField (K := K) A ↔
      ∃ τ : ramificationGroup K A,
        ramificationGroupToGalInertiaField (K := K) A τ = σ
theorem

ramificationGroupOverInertiaField_eq_map

L97 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupOverInertiaField_eq_map
Documentation

The transported subgroup agrees with the image of R_w under I_w = G(L/T_w).

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 ramificationGroupOverInertiaField_eq_map
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    Subgroup.map (inertiaGroupEquivGalInertiaField_of_finiteDimensional (K := K) A).toMonoidHom
        (ramificationGroup K A) =
      ramificationGroupOverInertiaField (K := K) A
instance

ramificationGroupOverInertiaField_normal

L111 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupOverInertiaField_normal
Documentation

The transported ramification subgroup is normal in G(L/T_w).

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
instance ramificationGroupOverInertiaField_normal
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (ramificationGroupOverInertiaField (K := K) A).Normal
theorem

ramificationFieldOverInertiaField_fixedField_eq_of_finiteDimensional

L123 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationFieldOverInertiaField_fixedField_eq_of_finiteDimensional
Documentation

The ramification field satisfies: the fixed field of the transported ramification subgroup over T_w is V_w.

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 ramificationFieldOverInertiaField_fixedField_eq_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    IntermediateField.fixedField
        (ramificationGroupOverInertiaField (K := K) A) =
      ramificationFieldOverInertiaField K A
theorem

ramificationFieldOverInertiaField_fixingSubgroup_eq_of_finiteDimensional

L148 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationFieldOverInertiaField_fixingSubgroup_eq_of_finiteDimensional
Documentation

The ramification field satisfies: G(L/V_w) over the inertia field is the transported ramification subgroup.

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 ramificationFieldOverInertiaField_fixingSubgroup_eq_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (ramificationFieldOverInertiaField K A).fixingSubgroup =
      ramificationGroupOverInertiaField (K := K) A
def

inertiaGroupQuotientRamificationEquivGalInertiaQuotient_of_finiteDimensional

L160 ↗
RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupQuotientRamificationEquivGalInertiaQuotient_of_finiteDimensional
Documentation

Inertia-character exactness: transport the quotient I_w/R_w along I_w = G(L/T_w).

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
def inertiaGroupQuotientRamificationEquivGalInertiaQuotient_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    inertiaGroup K A ⧸ ramificationGroup K A ≃*
      (L ≃ₐ[inertiaField K A] L) ⧸
        ramificationGroupOverInertiaField (K := K) A
def

galInertiaQuotientRamificationEquivGalRamificationFieldOverInertia_of_finiteDimensional

L173 ↗
RamificationTheory.HilbertRamification.ValuationSubring.galInertiaQuotientRamificationEquivGalRamificationFieldOverInertia_of_finiteDimensional
Documentation

Inertia-character exactness: the Galois correspondence gives G(L/T_w)/R_w ≃ G(V_w/T_w).

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
def galInertiaQuotientRamificationEquivGalRamificationFieldOverInertia_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (L ≃ₐ[inertiaField K A] L) ⧸
        ramificationGroupOverInertiaField (K := K) A ≃*
      (ramificationFieldOverInertiaField K A ≃ₐ[inertiaField K A]
        ramificationFieldOverInertiaField K A)
def

inertiaGroupQuotientRamificationEquivGalRamificationFieldOverInertia_of_finiteDimensional

L188 ↗
RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupQuotientRamificationEquivGalRamificationFieldOverInertia_of_finiteDimensional
Documentation

Inertia-character exactness: the quotient I_w/R_w is the Galois group of the ramification field over the inertia field.

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
def inertiaGroupQuotientRamificationEquivGalRamificationFieldOverInertia_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    inertiaGroup K A ⧸ ramificationGroup K A ≃*
      (ramificationFieldOverInertiaField K A ≃ₐ[inertiaField K A]
        ramificationFieldOverInertiaField K A)
theorem

mem_ramificationFieldOverDecompositionField_iff

L199 ↗
RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationFieldOverDecompositionField_iff
Documentation

States the theorem mem_ramificationFieldOverDecompositionField_iff.

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 mem_ramificationFieldOverDecompositionField_iff
    (A : _root_.ValuationSubring L) (x : L) :
    x ∈ ramificationFieldOverDecompositionField K A ↔
      ∀ σ : ramificationGroup K A,
        (((σ : inertiaGroup K A) : decompositionGroup K A) : L ≃ₐ[K] L) x = x
def

ramificationGroupToGalDecompositionField

L210 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupToGalDecompositionField
Documentation

The ramification field satisfies: view R_w as a subgroup of G(L/Z_w) through the decomposition-field identification G_w = G(L/Z_w).

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
def ramificationGroupToGalDecompositionField
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    ramificationGroup K A →* (L ≃ₐ[decompositionField K A] L)
theorem

ramificationGroupToGalDecompositionField_apply

L218 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupToGalDecompositionField_apply
Documentation

States the theorem ramificationGroupToGalDecompositionField_apply.

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 ramificationGroupToGalDecompositionField_apply
    [FiniteDimensional K L] (A : _root_.ValuationSubring L)
    (σ : ramificationGroup K A) :
    ramificationGroupToGalDecompositionField (K := K) A σ =
      decompositionGroupEquivGalDecompositionField_of_finiteDimensional
        (K := K) A ((σ : inertiaGroup K A) : decompositionGroup K A)
abbrev

ramificationGroupOverDecompositionField

L228 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupOverDecompositionField
Documentation

The ramification field satisfies: the transported ramification subgroup inside G(L/Z_w).

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
abbrev ramificationGroupOverDecompositionField
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    Subgroup (L ≃ₐ[decompositionField K A] L)
theorem

mem_ramificationGroupOverDecompositionField_iff

L234 ↗
RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroupOverDecompositionField_iff
Documentation

States the theorem mem_ramificationGroupOverDecompositionField_iff.

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 mem_ramificationGroupOverDecompositionField_iff
    [FiniteDimensional K L] (A : _root_.ValuationSubring L)
    (σ : L ≃ₐ[decompositionField K A] L) :
    σ ∈ ramificationGroupOverDecompositionField (K := K) A ↔
      ∃ τ : ramificationGroup K A,
        ramificationGroupToGalDecompositionField (K := K) A τ = σ
theorem

ramificationFieldOverDecompositionField_fixedField_eq_of_finiteDimensional

L245 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationFieldOverDecompositionField_fixedField_eq_of_finiteDimensional
Documentation

The ramification field satisfies: the fixed field of the transported ramification subgroup over Z_w is V_w.

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 ramificationFieldOverDecompositionField_fixedField_eq_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    IntermediateField.fixedField
        (ramificationGroupOverDecompositionField (K := K) A) =
      ramificationFieldOverDecompositionField K A
theorem

ramificationFieldOverDecompositionField_fixingSubgroup_eq_of_finiteDimensional

L270 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationFieldOverDecompositionField_fixingSubgroup_eq_of_finiteDimensional
Documentation

The ramification field satisfies: G(L/V_w) over the decomposition field is the transported ramification subgroup.

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 ramificationFieldOverDecompositionField_fixingSubgroup_eq_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (ramificationFieldOverDecompositionField K A).fixingSubgroup =
      ramificationGroupOverDecompositionField (K := K) A
def

ramificationGroupEquivGalOverDecompositionField

L283 ↗
RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupEquivGalOverDecompositionField
Documentation

The ramification field satisfies: the transported ramification group is the Galois group G(L/V_w) in the tower Z_w ⊆ V_w ⊆ L.

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
def ramificationGroupEquivGalOverDecompositionField
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    ramificationGroupOverDecompositionField (K := K) A ≃*
      (L ≃ₐ[ramificationFieldOverDecompositionField K A] L)

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