Module

BaseChange.lean

Nyll.ValuedFieldTheory.Ramification.LocalField.BaseChange

4 declarations indexed from sourceView source ↗

Module documentation

Transport of upper ramification groups under an equivalent base field

The target field can carry two algebra structures whose base fields are identified by a valuation-preserving field equivalence. This file proves that the resulting Galois groups have the same upper filtration, after identifying their automorphisms by their common action on the target.

Imports1

Nyll.ValuedFieldTheory.Ramification.LocalField.Core

Imported by9

def

galoisGroupEquivOfBaseRingEquiv

L34 ↗

RamificationTheory.LocalField.galoisGroupEquivOfBaseRingEquiv

Documentation

If two base fields have the same image in a common extension, their Galois groups are identified by leaving the underlying target automorphism unchanged.

Source context 8 commands

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

noncomputable section
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel

Lean source · full declaration

def galoisGroupEquivOfBaseRingEquiv
    (B K E : Type)
    [Field B] [Field K] [Field E]
    [Algebra B E] [Algebra K E]
    (e : B ≃+* K)
    (he : ∀ b, algebraMap K E (e b) = algebraMap B E b) :
    Gal(E / B) ≃* Gal(E / K) where
  toFun σ :=
    { σ.toRingEquiv with
      commutes' := by
        intro k
        rw [← e.apply_symm_apply k, he]
        exact σ.commutes (e.symm k) }
  invFun τ :=
    { τ.toRingEquiv with
      commutes' := by
        intro b
        rw [← he b]
        exact τ.commutes (e b) }
  left_inv σ := by
    ext x
    rfl
  right_inv τ := by
    ext x
    rfl
  map_mul' σ τ := by
    ext x
    rfl

theorem

galoisGroupEquivOfBaseRingEquiv_apply

L64 ↗

RamificationTheory.LocalField.galoisGroupEquivOfBaseRingEquiv_apply

Source context 8 commands

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

noncomputable section
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel

Lean source · statement

theorem galoisGroupEquivOfBaseRingEquiv_apply
    (B K E : Type)
    [Field B] [Field K] [Field E]
    [Algebra B E] [Algebra K E]
    (e : B ≃+* K)
    (he : ∀ b, algebraMap K E (e b) = algebraMap B E b)
    (σ : Gal(E/B)) (x : E) :
    galoisGroupEquivOfBaseRingEquiv B K E e he σ x = σ x

theorem

upperRamificationGroup_map_baseChange

L76 ↗

RamificationTheory.LocalField.upperRamificationGroup_map_baseChange

Source context 9 commands

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

noncomputable section
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
  (herbrandFunction_eq_of_card_lower_eq) in

Lean source · statement

theorem upperRamificationGroup_map_baseChange
    (B K E : Type)
    [Field B] [Field K] [Field E]
    [Algebra B E] [Algebra K E]
    [FiniteDimensional B E] [FiniteDimensional K E]
    (baseB : DVF.{0, 0} B)
    (baseK : DVF.{0, 0} K)
    (target : DVF.{0, 0} E)
    [baseB.valuation.HasExtension target.valuation]
    [baseK.valuation.HasExtension target.valuation]
    (huniqB :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension
        (base := baseB) (target := target))
    (huniqK :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension
        (base := baseK) (target := target))
    (q : Gal(E/B) ≃* Gal(E/K))
    (hq : ∀ σ x, q σ x = σ x)
    (t : ℝ) :
    Subgroup.map q.toMonoidHom
        (upperRamificationGroupOfUniqueExtension
          (base := baseB) (target := target) huniqB t) =
      upperRamificationGroupOfUniqueExtension
        (base := baseK) (target := target) huniqK t

theorem

localUpperRamificationGroup_map_baseRingEquiv

L185 ↗

RamificationTheory.LocalField.localUpperRamificationGroup_map_baseRingEquiv

Documentation

A valuation-preserving base-field equivalence transports every actual local upper ramification group to the group for the transported algebra structure on the same target field.

Source context 8 commands

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

noncomputable section
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel

Lean source · statement

theorem localUpperRamificationGroup_map_baseRingEquiv
    (B K E : Type)
    [Field B] [Field K] [Field E]
    [Algebra B E] [Algebra K E]
    [FiniteDimensional B E] [FiniteDimensional K E]
    [IsGalois B E] [IsGalois K E]
    [ValuativeRel B] [TopologicalSpace B]
    [IsNonarchimedeanLocalField B]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (e : B ≃+* K)
    (he : ∀ b, algebraMap K E (e b) = algebraMap B E b)
    (hvaluation : ∀ b,
      ValuativeRel.valuation B b ≤ 1 ↔
        ValuativeRel.valuation K (e b) ≤ 1)
    (t : ℝ) :
    Subgroup.map
        (galoisGroupEquivOfBaseRingEquiv B K E e he).toMonoidHom
        (localUpperRamificationGroup B E t) =
      localUpperRamificationGroup K E t

Module documentation

Transport of upper ramification groups under an equivalent base field

Declarations

galoisGroupEquivOfBaseRingEquiv

galoisGroupEquivOfBaseRingEquiv_apply

upperRamificationGroup_map_baseChange

localUpperRamificationGroup_map_baseRingEquiv