Module

ValuationSubring.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.ValuationSubring

63 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: valuation-subring layer

This file manages the ordinary valuation-subring decomposition/inertia exact sequence. For an arbitrary valuation subring the residue action need not be onto the full residue automorphism group; the canonical theorem is the exact sequence with target equal to the range of the residue action.

Imports6

Mathlib.Algebra.Exact.Basic
Mathlib.Algebra.Group.Units.Equiv
Mathlib.Algebra.Group.Subgroup.Map
Mathlib.FieldTheory.Galois.Basic
Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.RingTheory.Valuation.RamificationGroup

Imported by11

abbrev

decompositionGroup

L36 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup

Documentation

finite Galois ramification theory: the decomposition group of a valuation subring.

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 decompositionGroup (A : _root_.ValuationSubring L) :
    Subgroup (L ≃ₐ[K] L)

abbrev

inertiaGroup

L42 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup

Documentation

finite Galois ramification theory: the inertia group of a valuation subring.

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 inertiaGroup (A : _root_.ValuationSubring L) :
    Subgroup (decompositionGroup K A)

abbrev

residueAction

L47 ↗

RamificationTheory.HilbertRamification.ValuationSubring.residueAction

Documentation

The residue action of the decomposition group on the residue 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

abbrev residueAction (A : _root_.ValuationSubring L) :
    decompositionGroup K A →*
      (IsLocalRing.ResidueField A ≃+* IsLocalRing.ResidueField A)

theorem

residueAction_ker

L54 ↗

RamificationTheory.HilbertRamification.ValuationSubring.residueAction_ker

Documentation

The inertia group is the kernel of the residue action.

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 residueAction_ker (A : _root_.ValuationSubring L) :
    MonoidHom.ker (residueAction K A) = inertiaGroup K A

instance

inertiaGroup_normal

L59 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup_normal

Documentation

Provides the instance inertiaGroup_normal.

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 inertiaGroup_normal (A : _root_.ValuationSubring L) :
    (inertiaGroup K A).Normal

def

automorphismUnitQuotient

L68 ↗

RamificationTheory.HilbertRamification.ValuationSubring.automorphismUnitQuotient

Documentation

finite Galois ramification theory: the unit quotient σ x / x attached to an automorphism in the decomposition group. This is the expression used in the definition of the ramification 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

def automorphismUnitQuotient
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A) (x : Lˣ) :
    Lˣ

theorem

automorphismUnitQuotient_one

L74 ↗

RamificationTheory.HilbertRamification.ValuationSubring.automorphismUnitQuotient_one

Documentation

States the theorem automorphismUnitQuotient_one.

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 automorphismUnitQuotient_one
    (A : _root_.ValuationSubring L) (x : Lˣ) :
    automorphismUnitQuotient K A 1 x = 1

theorem

automorphismUnitQuotient_mul

L81 ↗

RamificationTheory.HilbertRamification.ValuationSubring.automorphismUnitQuotient_mul

Documentation

States the theorem automorphismUnitQuotient_mul.

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 automorphismUnitQuotient_mul
    (A : _root_.ValuationSubring L) (σ τ : decompositionGroup K A) (x : Lˣ) :
    automorphismUnitQuotient K A (σ * τ) x =
      automorphismUnitQuotient K A σ
        (Units.mapEquiv ((τ : L ≃ₐ[K] L).toMulEquiv) x) *
      automorphismUnitQuotient K A τ x

def

ramificationGroup

L93 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup

Documentation

The decomposition and inertia subgroup definitions: the ramification group R_w, as the subgroup of inertia whose unit quotients σ x / x are principal units for every x : 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 · full declaration

def ramificationGroup (A : _root_.ValuationSubring L) :
    Subgroup (inertiaGroup K A) where
  carrier :=
    {σ | ∀ x : Lˣ,
      automorphismUnitQuotient K A (σ : decompositionGroup K A) x ∈
        A.principalUnitGroup}
  one_mem' := by
    intro x
    have hmap : Units.mapEquiv (AlgEquiv.toMulEquiv (1 : L ≃ₐ[K] L)) x = x := by
      ext
      rfl
    simp [automorphismUnitQuotient, hmap]
  mul_mem' := by
    intro σ τ hσ hτ x
    change
      automorphismUnitQuotient K A ((σ * τ : inertiaGroup K A) : decompositionGroup K A) x ∈
        A.principalUnitGroup
    have hx :
        automorphismUnitQuotient K A (σ : decompositionGroup K A)
            (Units.mapEquiv (((τ : decompositionGroup K A) : L ≃ₐ[K] L).toMulEquiv) x) *
          automorphismUnitQuotient K A (τ : decompositionGroup K A) x ∈
          A.principalUnitGroup :=
      A.principalUnitGroup.mul_mem
      (hσ (Units.mapEquiv (((τ : decompositionGroup K A) : L ≃ₐ[K] L).toMulEquiv) x))
      (hτ x)
    simpa [automorphismUnitQuotient_mul] using hx
  inv_mem' := by
    intro σ hσ x
    let y : Lˣ :=
      Units.mapEquiv
        ((((σ : decompositionGroup K A)⁻¹ : decompositionGroup K A) :
          L ≃ₐ[K] L).toMulEquiv) x
    have hy :
        automorphismUnitQuotient K A (σ : decompositionGroup K A) y ∈
          A.principalUnitGroup :=
      hσ y
    have hyinv :
        (automorphismUnitQuotient K A (σ : decompositionGroup K A) y)⁻¹ ∈
          A.principalUnitGroup :=
      A.principalUnitGroup.inv_mem hy
    have hquot :
        automorphismUnitQuotient K A
            ((σ⁻¹ : inertiaGroup K A) : decompositionGroup K A) x =
          (automorphismUnitQuotient K A (σ : decompositionGroup K A) y)⁻¹ := by
      ext
      simp [automorphismUnitQuotient, y, div_eq_mul_inv]
    rw [hquot]
    exact hyinv

theorem

mem_ramificationGroup_iff

L143 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroup_iff

Documentation

States the theorem mem_ramificationGroup_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_ramificationGroup_iff
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    σ ∈ ramificationGroup K A ↔
      ∀ x : Lˣ,
        automorphismUnitQuotient K A (σ : decompositionGroup K A) x ∈
          A.principalUnitGroup

abbrev

decompositionField

L154 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionField

Documentation

finite Galois ramification theory: the decomposition field Z_w is the fixed field of the decomposition 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

abbrev decompositionField (A : _root_.ValuationSubring L) :
    IntermediateField K L

theorem

mem_decompositionField_iff

L159 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_decompositionField_iff

Documentation

States the theorem mem_decompositionField_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_decompositionField_iff
    (A : _root_.ValuationSubring L) (x : L) :
    x ∈ decompositionField K A ↔
      ∀ σ ∈ decompositionGroup K A, σ x = x

abbrev

inertiaGroupInAut

L168 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut

Documentation

The inertia group as a subgroup of the full K-automorphism group of L. This is the subgroup whose fixed field is the classical 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

abbrev inertiaGroupInAut (A : _root_.ValuationSubring L) :
    Subgroup (L ≃ₐ[K] L)

def

inertiaGroupToAut

L173 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupToAut

Documentation

The canonical inclusion I_w -> G(L/K).

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 inertiaGroupToAut (A : _root_.ValuationSubring L) :
    inertiaGroup K A →* (L ≃ₐ[K] L)

theorem

inertiaGroupToAut_apply

L178 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupToAut_apply

Documentation

States the theorem inertiaGroupToAut_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 inertiaGroupToAut_apply
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    inertiaGroupToAut (K := K) A σ =
      ((σ : decompositionGroup K A) : L ≃ₐ[K] L)

abbrev

inertiaField

L186 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaField

Documentation

The inertia-field definition: the inertia field 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

abbrev inertiaField (A : _root_.ValuationSubring L) :
    IntermediateField K L

theorem

mem_inertiaField_iff

L191 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_inertiaField_iff

Documentation

States the theorem mem_inertiaField_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_inertiaField_iff
    (A : _root_.ValuationSubring L) (x : L) :
    x ∈ inertiaField K A ↔
      ∀ σ : inertiaGroup K A, ((σ : decompositionGroup K A) : L ≃ₐ[K] L) x = x

theorem

inertiaGroupInAut_le_decompositionGroup

L206 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAut_le_decompositionGroup

Documentation

The inertia subgroup, viewed inside the full automorphism group, lies in the decomposition 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

theorem inertiaGroupInAut_le_decompositionGroup
    (A : _root_.ValuationSubring L) :
    inertiaGroupInAut K A ≤ decompositionGroup K A

abbrev

ramificationGroupInAut

L213 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInAut

Documentation

The ramification group as a subgroup of the full automorphism 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

abbrev ramificationGroupInAut (A : _root_.ValuationSubring L) :
    Subgroup (L ≃ₐ[K] L)

abbrev

ramificationField

L219 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationField

Documentation

The ramification-field definition: the ramification field V_w is the fixed field of the ramification 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

abbrev ramificationField (A : _root_.ValuationSubring L) :
    IntermediateField K L

theorem

mem_ramificationField_iff

L224 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationField_iff

Documentation

States the theorem mem_ramificationField_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_ramificationField_iff
    (A : _root_.ValuationSubring L) (x : L) :
    x ∈ ramificationField K A ↔
      ∀ σ : ramificationGroup K A,
        (((σ : inertiaGroup K A) : decompositionGroup K A) : L ≃ₐ[K] L) x = x

theorem

ramificationGroupInAut_le_inertiaGroupInAut

L239 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInAut_le_inertiaGroupInAut

Documentation

The ramification subgroup, viewed in G(L/K), lies in inertia.

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 ramificationGroupInAut_le_inertiaGroupInAut
    (A : _root_.ValuationSubring L) :
    ramificationGroupInAut K A ≤ inertiaGroupInAut K A

theorem

inertiaField_le_ramificationField

L247 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaField_le_ramificationField

Documentation

finite Galois ramification theory: the inertia field is contained in the ramification 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

theorem inertiaField_le_ramificationField
    (A : _root_.ValuationSubring L) :
    inertiaField K A ≤ ramificationField K A

abbrev

ramificationFieldOverInertiaField

L256 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationFieldOverInertiaField

Documentation

The ramification-field definition source: the ramification field, viewed as an intermediate field over the inertia field 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 ramificationFieldOverInertiaField
    (A : _root_.ValuationSubring L) :
    IntermediateField (inertiaField K A) L

theorem

ramificationFieldOverInertiaField_restrictScalars

L263 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationFieldOverInertiaField_restrictScalars

Documentation

States the theorem ramificationFieldOverInertiaField_restrictScalars.

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_restrictScalars
    (A : _root_.ValuationSubring L) :
    (ramificationFieldOverInertiaField K A).restrictScalars K =
      ramificationField K A

def

ramificationGroupEquivInAut

L271 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupEquivInAut

Documentation

The ramification group is canonically equivalent to its image in G(L/K).

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 ramificationGroupEquivInAut
    (A : _root_.ValuationSubring L) :
    ramificationGroup K A ≃* ramificationGroupInAut K A

theorem

ramificationField_fixingSubgroup_eq_of_finiteDimensional

L285 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationField_fixingSubgroup_eq_of_finiteDimensional

Documentation

The ramification-field definition source: G(L/V_w) = R_w after viewing ramification inside the full automorphism 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

theorem ramificationField_fixingSubgroup_eq_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (ramificationField K A).fixingSubgroup = ramificationGroupInAut K A

def

ramificationGroupEquivGalRamificationField_of_finiteDimensional

L292 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupEquivGalRamificationField_of_finiteDimensional

Documentation

The ramification-field definition source: the ramification group is the Galois group over its fixed 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 ramificationGroupEquivGalRamificationField_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    ramificationGroup K A ≃* (L ≃ₐ[ramificationField K A] L)

theorem

decompositionField_le_inertiaField

L300 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionField_le_inertiaField

Documentation

finite Galois ramification theory: the decomposition field is contained in 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

theorem decompositionField_le_inertiaField
    (A : _root_.ValuationSubring L) :
    decompositionField K A ≤ inertiaField K A

theorem

decompositionField_le_ramificationField

L308 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionField_le_ramificationField

Documentation

finite Galois ramification theory: the decomposition field is contained in the ramification 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

theorem decompositionField_le_ramificationField
    (A : _root_.ValuationSubring L) :
    decompositionField K A ≤ ramificationField K A

abbrev

ramificationFieldOverDecompositionField

L317 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationFieldOverDecompositionField

Documentation

The ramification-field definition source: the ramification field, viewed as an intermediate field over the decomposition field Z_w. This is the field appearing in V_w | 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 ramificationFieldOverDecompositionField
    (A : _root_.ValuationSubring L) :
    IntermediateField (decompositionField K A) L

theorem

ramificationFieldOverDecompositionField_restrictScalars

L324 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationFieldOverDecompositionField_restrictScalars

Documentation

States the theorem ramificationFieldOverDecompositionField_restrictScalars.

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_restrictScalars
    (A : _root_.ValuationSubring L) :
    (ramificationFieldOverDecompositionField K A).restrictScalars K =
      ramificationField K A

abbrev

inertiaFieldOverDecompositionField

L333 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaFieldOverDecompositionField

Documentation

The inertia-field definition source: the inertia field, viewed as an intermediate field over the decomposition field Z_w. This is the field appearing in G(T_w/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 inertiaFieldOverDecompositionField
    (A : _root_.ValuationSubring L) :
    IntermediateField (decompositionField K A) L

theorem

mem_inertiaFieldOverDecompositionField_iff

L340 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_inertiaFieldOverDecompositionField_iff

Documentation

States the theorem mem_inertiaFieldOverDecompositionField_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_inertiaFieldOverDecompositionField_iff
    (A : _root_.ValuationSubring L) (x : L) :
    x ∈ inertiaFieldOverDecompositionField K A ↔
      ∀ σ : inertiaGroup K A, ((σ : decompositionGroup K A) : L ≃ₐ[K] L) x = x

theorem

inertiaFieldOverDecompositionField_restrictScalars

L348 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaFieldOverDecompositionField_restrictScalars

Documentation

States the theorem inertiaFieldOverDecompositionField_restrictScalars.

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 inertiaFieldOverDecompositionField_restrictScalars
    (A : _root_.ValuationSubring L) :
    (inertiaFieldOverDecompositionField K A).restrictScalars K =
      inertiaField K A

theorem

decompositionField_fixingSubgroup_eq_of_finiteDimensional

L356 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionField_fixingSubgroup_eq_of_finiteDimensional

Documentation

The fixed-field description of decomposition source: G(L/Z_w) = G_w for the decomposition 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

theorem decompositionField_fixingSubgroup_eq_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (decompositionField K A).fixingSubgroup = decompositionGroup K A

def

decompositionGroupEquivGalDecompositionField_of_finiteDimensional

L363 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupEquivGalDecompositionField_of_finiteDimensional

Documentation

The fixed-field description of decomposition source: the decomposition group is the Galois group over its fixed 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 decompositionGroupEquivGalDecompositionField_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    decompositionGroup K A ≃* (L ≃ₐ[decompositionField K A] L)

instance

decompositionField_isGalois

L371 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionField_isGalois

Documentation

The fixed-field description of decomposition source: L/Z_w is Galois because Z_w is the fixed field of the finite decomposition group action.

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 decompositionField_isGalois
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    IsGalois (decompositionField K A) L

theorem

decompositionGroupEquivGalDecompositionField_of_finiteDimensional_apply

L379 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupEquivGalDecompositionField_of_finiteDimensional_apply

Documentation

States the theorem decompositionGroupEquivGalDecompositionField_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 decompositionGroupEquivGalDecompositionField_of_finiteDimensional_apply
    [FiniteDimensional K L] (A : _root_.ValuationSubring L)
    (σ : decompositionGroup K A) (x : L) :
    decompositionGroupEquivGalDecompositionField_of_finiteDimensional (K := K) A σ x =
      ((σ : L ≃ₐ[K] L) x)

abbrev

inertiaGroupOverDecompositionField

L389 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupOverDecompositionField

Documentation

The inertia-field definition source: the inertia subgroup transported to Gal(L/Z_w) through 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

abbrev inertiaGroupOverDecompositionField
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    Subgroup (L ≃ₐ[decompositionField K A] L)

theorem

mem_inertiaGroupOverDecompositionField_iff

L398 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_inertiaGroupOverDecompositionField_iff

Documentation

States the theorem mem_inertiaGroupOverDecompositionField_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_inertiaGroupOverDecompositionField_iff
    [FiniteDimensional K L] (A : _root_.ValuationSubring L)
    (σ : L ≃ₐ[decompositionField K A] L) :
    σ ∈ inertiaGroupOverDecompositionField (K := K) A ↔
      ∃ τ : inertiaGroup K A,
        decompositionGroupEquivGalDecompositionField_of_finiteDimensional
          (K := K) A (τ : decompositionGroup K A) = σ

instance

inertiaGroupOverDecompositionField_normal

L412 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupOverDecompositionField_normal

Documentation

The transported inertia subgroup is normal in Gal(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

instance inertiaGroupOverDecompositionField_normal
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (inertiaGroupOverDecompositionField (K := K) A).Normal

theorem

inertiaFieldOverDecompositionField_fixedField_eq_of_finiteDimensional

L424 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaFieldOverDecompositionField_fixedField_eq_of_finiteDimensional

Documentation

The inertia-field definition source: the fixed field of the transported inertia subgroup over Z_w is 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 inertiaFieldOverDecompositionField_fixedField_eq_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    IntermediateField.fixedField
        (inertiaGroupOverDecompositionField (K := K) A) =
      inertiaFieldOverDecompositionField K A

theorem

inertiaFieldOverDecompositionField_fixingSubgroup_eq_of_finiteDimensional

L451 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaFieldOverDecompositionField_fixingSubgroup_eq_of_finiteDimensional

Documentation

The inertia-field definition source: G(L/T_w) over the decomposition field is the transported inertia 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 inertiaFieldOverDecompositionField_fixingSubgroup_eq_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (inertiaFieldOverDecompositionField K A).fixingSubgroup =
      inertiaGroupOverDecompositionField (K := K) A

def

inertiaGroupOverDecompositionFieldEquivGalInertiaFieldOverDecompositionField_of_finiteDimensional

L464 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupOverDecompositionFieldEquivGalInertiaFieldOverDecompositionField_of_finiteDimensional

Documentation

The inertia-field definition source: the transported inertia group is the Galois group G(L/T_w) in the tower Z_w ⊆ T_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
inertiaGroupOverDecompositionFieldEquivGalInertiaFieldOverDecompositionField_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    inertiaGroupOverDecompositionField (K := K) A ≃*
      (L ≃ₐ[inertiaFieldOverDecompositionField K A] L)

def

decompositionQuotientInertiaEquivGalInertiaFieldOverDecomposition_of_finiteDimensional

L478 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionQuotientInertiaEquivGalInertiaFieldOverDecomposition_of_finiteDimensional

Documentation

The inertia-field definition: the Galois correspondence gives G(L/Z_w)/I_w ≃ G(T_w/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 decompositionQuotientInertiaEquivGalInertiaFieldOverDecomposition_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (L ≃ₐ[decompositionField K A] L) ⧸
        inertiaGroupOverDecompositionField (K := K) A ≃*
      (inertiaFieldOverDecompositionField K A ≃ₐ[decompositionField K A]
        inertiaFieldOverDecompositionField K A)

def

decompositionGroupQuotientInertiaEquivGalDecompositionQuotient_of_finiteDimensional

L492 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupQuotientInertiaEquivGalDecompositionQuotient_of_finiteDimensional

Documentation

The inertia-field definition source: transport the quotient G_w/I_w along 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 decompositionGroupQuotientInertiaEquivGalDecompositionQuotient_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    decompositionGroup K A ⧸ inertiaGroup K A ≃*
      (L ≃ₐ[decompositionField K A] L) ⧸
        inertiaGroupOverDecompositionField (K := K) A

def

decompositionGroupQuotientInertiaEquivGalInertiaFieldOverDecomposition_of_finiteDimensional

L507 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupQuotientInertiaEquivGalInertiaFieldOverDecomposition_of_finiteDimensional

Documentation

The inertia-field definition: G_w/I_w ≃ G(T_w/Z_w), the group-theoretic part of the isomorphism obtained from the residue-action exact sequence.

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 decompositionGroupQuotientInertiaEquivGalInertiaFieldOverDecomposition_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    decompositionGroup K A ⧸ inertiaGroup K A ≃*
      (inertiaFieldOverDecompositionField K A ≃ₐ[decompositionField K A]
        inertiaFieldOverDecompositionField K A)

theorem

inertiaField_fixingSubgroup_eq_of_finiteDimensional

L519 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaField_fixingSubgroup_eq_of_finiteDimensional

Documentation

The inertia-field definition source: G(L/T_w) = I_w after viewing inertia inside the full automorphism 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

theorem inertiaField_fixingSubgroup_eq_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (inertiaField K A).fixingSubgroup = inertiaGroupInAut K A

def

inertiaGroupInAutEquivGalInertiaField_of_finiteDimensional

L526 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupInAutEquivGalInertiaField_of_finiteDimensional

Documentation

The inertia-field definition source: the inertia group is the Galois group over its fixed 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 inertiaGroupInAutEquivGalInertiaField_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    inertiaGroupInAut K A ≃* (L ≃ₐ[inertiaField K A] L)

def

restrictAutomorphismScalars

L540 ↗

RamificationTheory.HilbertRamification.ValuationSubring.restrictAutomorphismScalars

Documentation

Restrict scalars on automorphisms along an intermediate field K ⊆ M ⊆ L. This is the inclusion G(L/M) -> G(L/K) used in scalar-restriction compatibility of ramification subgroups.

Source context 8 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]
section IntermediateFieldFunctoriality
variable {M : Type*} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · full declaration

def restrictAutomorphismScalars : (L ≃ₐ[M] L) →* (L ≃ₐ[K] L) where
  toFun σ :=
    { σ with
      commutes' := by
        intro a
        simp [IsScalarTower.algebraMap_eq K M L, σ.commutes (algebraMap K M a)] }
  map_one' := by
    ext x
    rfl
  map_mul' σ τ := by
    ext x
    rfl

theorem

mem_decompositionGroup_restrictScalars_iff

L556 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_decompositionGroup_restrictScalars_iff

Documentation

scalar-restriction compatibility of ramification subgroups, decomposition-group membership form: an M-automorphism stabilizes A exactly when the same automorphism, viewed over K, stabilizes A.

Source context 8 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]
section IntermediateFieldFunctoriality
variable {M : Type*} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem mem_decompositionGroup_restrictScalars_iff
    (A : _root_.ValuationSubring L) (σ : L ≃ₐ[M] L) :
    restrictAutomorphismScalars (K := K) (M := M) σ ∈ decompositionGroup K A ↔
      σ ∈ decompositionGroup M A

theorem

decompositionGroup_range_eq_inf

L565 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup_range_eq_inf

Documentation

scalar-restriction compatibility of ramification subgroups: G_w(L/M) maps onto G_w(L/K) ∩ G(L/M) under the scalar-restriction inclusion.

Source context 8 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]
section IntermediateFieldFunctoriality
variable {M : Type*} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem decompositionGroup_range_eq_inf
    (A : _root_.ValuationSubring L) :
    Subgroup.map (restrictAutomorphismScalars (K := K) (M := M))
        (decompositionGroup M A) =
      decompositionGroup K A ⊓
        (restrictAutomorphismScalars (K := K) (M := M)).range

def

decompositionGroupRestrictScalars

L586 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupRestrictScalars

Documentation

Scalar restriction on decomposition groups along an intermediate field.

Source context 8 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]
section IntermediateFieldFunctoriality
variable {M : Type*} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · full declaration

def decompositionGroupRestrictScalars
    (A : _root_.ValuationSubring L) :
    decompositionGroup M A →* decompositionGroup K A where
  toFun σ :=
    ⟨restrictAutomorphismScalars (K := K) (M := M) σ,
      (mem_decompositionGroup_restrictScalars_iff
        (K := K) (M := M) A σ).mpr σ.property⟩
  map_one' := by
    ext x
    rfl
  map_mul' σ τ := by
    ext x
    rfl

theorem

mem_inertiaGroup_restrictScalars_iff

L602 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_inertiaGroup_restrictScalars_iff

Documentation

scalar-restriction compatibility of ramification subgroups, inertia-group membership form: the residue action is unchanged by scalar restriction from M to K.

Source context 8 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]
section IntermediateFieldFunctoriality
variable {M : Type*} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem mem_inertiaGroup_restrictScalars_iff
    (A : _root_.ValuationSubring L) (σ : decompositionGroup M A) :
    decompositionGroupRestrictScalars (K := K) (M := M) A σ ∈ inertiaGroup K A ↔
      σ ∈ inertiaGroup M A

theorem

inertiaGroup_range_eq_inf

L610 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup_range_eq_inf

Documentation

scalar-restriction compatibility of ramification subgroups: I_w(L/M) maps onto I_w(L/K) ∩ G_w(L/M) inside the decomposition group.

Source context 8 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]
section IntermediateFieldFunctoriality
variable {M : Type*} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem inertiaGroup_range_eq_inf
    (A : _root_.ValuationSubring L) :
    Subgroup.map (decompositionGroupRestrictScalars (K := K) (M := M) A)
        (inertiaGroup M A) =
      inertiaGroup K A ⊓
        (decompositionGroupRestrictScalars (K := K) (M := M) A).range

def

inertiaGroupRestrictScalars

L631 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroupRestrictScalars

Documentation

Scalar restriction on inertia groups along an intermediate field.

Source context 8 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]
section IntermediateFieldFunctoriality
variable {M : Type*} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · full declaration

def inertiaGroupRestrictScalars
    (A : _root_.ValuationSubring L) :
    inertiaGroup M A →* inertiaGroup K A where
  toFun σ :=
    ⟨decompositionGroupRestrictScalars (K := K) (M := M) A
        (σ : decompositionGroup M A),
      (mem_inertiaGroup_restrictScalars_iff
        (K := K) (M := M) A (σ : decompositionGroup M A)).mpr σ.property⟩
  map_one' := by
    ext x
    rfl
  map_mul' σ τ := by
    ext x
    rfl

theorem

mem_ramificationGroup_restrictScalars_iff

L649 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroup_restrictScalars_iff

Documentation

scalar-restriction compatibility of ramification subgroups, ramification-group membership form: the condition defining R_w is unchanged by scalar restriction from M to K.

Source context 8 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]
section IntermediateFieldFunctoriality
variable {M : Type*} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem mem_ramificationGroup_restrictScalars_iff
    (A : _root_.ValuationSubring L) (σ : inertiaGroup M A) :
    inertiaGroupRestrictScalars (K := K) (M := M) A σ ∈ ramificationGroup K A ↔
      σ ∈ ramificationGroup M A

theorem

ramificationGroup_range_eq_inf

L687 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup_range_eq_inf

Documentation

scalar-restriction compatibility of ramification subgroups: R_w(L/M) maps onto R_w(L/K) ∩ I_w(L/M) under scalar restriction. Since R_w ≤ I_w, this is the ramification-group part of the classical intersection formula.

Source context 8 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]
section IntermediateFieldFunctoriality
variable {M : Type*} [Field M] [Algebra K M] [Algebra M L]
  [IsScalarTower K M L]

Lean source · statement

theorem ramificationGroup_range_eq_inf
    (A : _root_.ValuationSubring L) :
    Subgroup.map (inertiaGroupRestrictScalars (K := K) (M := M) A)
        (ramificationGroup M A) =
      ramificationGroup K A ⊓
        (inertiaGroupRestrictScalars (K := K) (M := M) A).range

theorem

inertia_subtype_mulExact_residueAction

L711 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertia_subtype_mulExact_residueAction

Documentation

The residue-action exact sequence, exact-at-decomposition form: I -> D -> Aut(k_A) is exact for every valuation subring.

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 inertia_subtype_mulExact_residueAction
    (A : _root_.ValuationSubring L) :
    Function.MulExact (inertiaGroup K A).subtype (residueAction K A)

def

quotientInertiaEquivResidueActionRange

L719 ↗

RamificationTheory.HilbertRamification.ValuationSubring.quotientInertiaEquivResidueActionRange

Documentation

The ordinary valuation-subring first-isomorphism form: D/I is the range of the residue action.

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 quotientInertiaEquivResidueActionRange
    (A : _root_.ValuationSubring L) :
    decompositionGroup K A ⧸ inertiaGroup K A ≃*
      (residueAction K A).range

theorem

quotientInertiaEquivResidueActionRange_mk

L728 ↗

RamificationTheory.HilbertRamification.ValuationSubring.quotientInertiaEquivResidueActionRange_mk

Documentation

States the theorem quotientInertiaEquivResidueActionRange_mk.

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 quotientInertiaEquivResidueActionRange_mk
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A) :
    quotientInertiaEquivResidueActionRange (K := K) A
        (QuotientGroup.mk' (inertiaGroup K A) σ) =
      (residueAction K A).rangeRestrict σ

def

galInertiaFieldOverDecompositionEquivResidueActionRange_of_finiteDimensional

L739 ↗

RamificationTheory.HilbertRamification.ValuationSubring.galInertiaFieldOverDecompositionEquivResidueActionRange_of_finiteDimensional

Documentation

The inertia-field definition / the residue-action exact sequence source: without surjectivity onto the whole residue automorphism group, the canonical residue-field comparison is G(T_w/Z_w) ≃ range(G_w -> Aut(lambda)).

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 galInertiaFieldOverDecompositionEquivResidueActionRange_of_finiteDimensional
    [FiniteDimensional K L] (A : _root_.ValuationSubring L) :
    (inertiaFieldOverDecompositionField K A ≃ₐ[decompositionField K A]
        inertiaFieldOverDecompositionField K A) ≃*
      (residueAction K A).range

Module documentation

Hilbert ramification theory: valuation-subring layer

Declarations