Module

Conjugation.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.CyclicInertia.Conjugation

11 declarations indexed from sourceView source ↗

Module documentation

Conjugation on tame inertia over a discrete valuation ring

This file records the finite-level equivariance of the residue-unit inertia character under the decomposition group. In residue characteristic zero the character is faithful, so an element whose residue action inverts the character values conjugates inertia to its inverse.

Imports2

Imported by2

def

inertiaToValueTrivialOfDVR

L30 ↗

TameAbhyankar.SGA1.inertiaToValueTrivialOfDVR

Documentation

The inclusion of DVR inertia into the value-trivial inertia group.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · full declaration

def inertiaToValueTrivialOfDVR
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V] :
    inertiaGroup K V →* valueTrivialInertiaGroup K V where
  toFun sigma :=
    ⟨sigma, inertia_mem_valueTrivialInertiaGroup_of_dvr K V sigma⟩
  map_one' := rfl
  map_mul' _ _ := rfl

def

dvrInertiaCharacter

L40 ↗

TameAbhyankar.SGA1.dvrInertiaCharacter

Documentation

The residue-unit character of inertia over a DVR.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

def dvrInertiaCharacter
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V] :
    inertiaGroup K V →*
      (((Lˣ ⧸ V.unitGroup) ⧸ baseUnitValueClassSubgroup K V) →*
        (IsLocalRing.ResidueField V)ˣ)

def

inertiaConjugate

L50 ↗

TameAbhyankar.SGA1.inertiaConjugate

Documentation

Conjugation by a decomposition element, restricted to inertia.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · full declaration

def inertiaConjugate
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) (g : decompositionGroup K V) :
    inertiaGroup K V →* inertiaGroup K V where
  toFun sigma :=
    ⟨g * (sigma : decompositionGroup K V) * g⁻¹, by
      exact (inertiaGroup_normal (K := K) V).conj_mem
        (sigma : decompositionGroup K V) sigma.property g⟩
  map_one' := by
    ext
    simp
  map_mul' sigma tau := by
    ext
    simp [mul_assoc]

theorem

dvrInertiaCharacter_conjugate_apply_mk_mk

L68 ↗

TameAbhyankar.SGA1.dvrInertiaCharacter_conjugate_apply_mk_mk

Documentation

The finite-level inertia character is equivariant for conjugation: the decomposition element acts on the residue-unit value, while its inverse acts on the field-unit argument.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem dvrInertiaCharacter_conjugate_apply_mk_mk
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    (g : decompositionGroup K V) (sigma : inertiaGroup K V) (x : Lˣ) :
    dvrInertiaCharacter K V (inertiaConjugate K V g sigma)
        (QuotientGroup.mk' (baseUnitValueClassSubgroup K V)
          (QuotientGroup.mk' V.unitGroup x)) =
      Units.mapEquiv (residueAction K V g).toMulEquiv
        (dvrInertiaCharacter K V sigma
          (QuotientGroup.mk' (baseUnitValueClassSubgroup K V)
            (QuotientGroup.mk' V.unitGroup
              (Units.mapEquiv
                (((g⁻¹ : decompositionGroup K V) : L ≃ₐ[K] L).toMulEquiv) x))))

theorem

dvrInertiaCharacter_mapEquiv_inv_argument

L105 ↗

TameAbhyankar.SGA1.dvrInertiaCharacter_mapEquiv_inv_argument

Documentation

A decomposition automorphism does not change the relative value-class argument of the DVR inertia character.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem dvrInertiaCharacter_mapEquiv_inv_argument
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    (g : decompositionGroup K V) (sigma : inertiaGroup K V) (x : Lˣ) :
    dvrInertiaCharacter K V sigma
        (QuotientGroup.mk' (baseUnitValueClassSubgroup K V)
          (QuotientGroup.mk' V.unitGroup
            (Units.mapEquiv
              (((g⁻¹ : decompositionGroup K V) : L ≃ₐ[K] L).toMulEquiv) x))) =
      dvrInertiaCharacter K V sigma
        (QuotientGroup.mk' (baseUnitValueClassSubgroup K V)
          (QuotientGroup.mk' V.unitGroup x))

theorem

dvrInertiaCharacter_conjugate_apply

L125 ↗

TameAbhyankar.SGA1.dvrInertiaCharacter_conjugate_apply

Documentation

Equivariance with the unchanged DVR value-class argument.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem dvrInertiaCharacter_conjugate_apply
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    (g : decompositionGroup K V) (sigma : inertiaGroup K V) (x : Lˣ) :
    dvrInertiaCharacter K V (inertiaConjugate K V g sigma)
        (QuotientGroup.mk' (baseUnitValueClassSubgroup K V)
          (QuotientGroup.mk' V.unitGroup x)) =
      Units.mapEquiv (residueAction K V g).toMulEquiv
        (dvrInertiaCharacter K V sigma
          (QuotientGroup.mk' (baseUnitValueClassSubgroup K V)
            (QuotientGroup.mk' V.unitGroup x)))

theorem

dvrInertiaCharacter_injective_of_residue_charZero

L140 ↗

TameAbhyankar.SGA1.dvrInertiaCharacter_injective_of_residue_charZero

Documentation

In residue characteristic zero, the DVR inertia character is faithful.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem dvrInertiaCharacter_injective_of_residue_charZero
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [CharZero (IsLocalRing.ResidueField V)]
    [Finite (inertiaGroup K V)] :
    Function.Injective (dvrInertiaCharacter K V)

theorem

dvrInertiaCharacter_value_isOfFinOrder

L159 ↗

TameAbhyankar.SGA1.dvrInertiaCharacter_value_isOfFinOrder

Documentation

Every value of a finite DVR inertia character has finite multiplicative order in the residue field.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem dvrInertiaCharacter_value_isOfFinOrder
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [Finite (inertiaGroup K V)]
    (sigma : inertiaGroup K V)
    (q : (Lˣ ⧸ V.unitGroup) ⧸ baseUnitValueClassSubgroup K V) :
    IsOfFinOrder (dvrInertiaCharacter K V sigma q)

theorem

inertiaConjugate_eq_inv_of_character_inversion

L181 ↗

TameAbhyankar.SGA1.inertiaConjugate_eq_inv_of_character_inversion

Documentation

If a decomposition element acts by inversion on all values of the DVR inertia character, it conjugates every inertia element to its inverse.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem inertiaConjugate_eq_inv_of_character_inversion
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [CharZero (IsLocalRing.ResidueField V)]
    [Finite (inertiaGroup K V)]
    (g : decompositionGroup K V)
    (hinv : ∀ sigma : inertiaGroup K V,
      dvrInertiaCharacter K V (inertiaConjugate K V g sigma) =
        (dvrInertiaCharacter K V sigma)⁻¹)
    (sigma : inertiaGroup K V) :
    inertiaConjugate K V g sigma = sigma⁻¹

theorem

inertiaConjugate_eq_inv_of_residue_inversion

L198 ↗

TameAbhyankar.SGA1.inertiaConjugate_eq_inv_of_residue_inversion

Documentation

A decomposition element that inverts every residue-unit value of the DVR inertia character conjugates inertia elementwise to inversion.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem inertiaConjugate_eq_inv_of_residue_inversion
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [CharZero (IsLocalRing.ResidueField V)]
    [Finite (inertiaGroup K V)]
    (g : decompositionGroup K V)
    (hinv : ∀ (sigma : inertiaGroup K V) (x : Lˣ),
      Units.mapEquiv (residueAction K V g).toMulEquiv
          (dvrInertiaCharacter K V sigma
            (QuotientGroup.mk' (baseUnitValueClassSubgroup K V)
              (QuotientGroup.mk' V.unitGroup x))) =
        (dvrInertiaCharacter K V sigma
          (QuotientGroup.mk' (baseUnitValueClassSubgroup K V)
            (QuotientGroup.mk' V.unitGroup x)))⁻¹)
    (sigma : inertiaGroup K V) :
    inertiaConjugate K V g sigma = sigma⁻¹

theorem

inertiaConjugate_eq_inv_of_torsion_residue_inversion

L231 ↗

TameAbhyankar.SGA1.inertiaConjugate_eq_inv_of_torsion_residue_inversion

Documentation

It is enough that the residue action invert finite-order units: all finite-level tame-inertia character values are such units.

Source context 5 commands

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

noncomputable section
universe u v
namespace TameAbhyankar.SGA1
open RamificationTheory.HilbertRamification
open RamificationTheory.HilbertRamification.ValuationSubring

Lean source · statement

theorem inertiaConjugate_eq_inv_of_torsion_residue_inversion
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [CharZero (IsLocalRing.ResidueField V)]
    [Finite (inertiaGroup K V)]
    (g : decompositionGroup K V)
    (hinv : ∀ z : (IsLocalRing.ResidueField V)ˣ,
      IsOfFinOrder z →
        Units.mapEquiv (residueAction K V g).toMulEquiv z = z⁻¹)
    (sigma : inertiaGroup K V) :
    inertiaConjugate K V g sigma = sigma⁻¹

Module documentation

Conjugation on tame inertia over a discrete valuation ring

Declarations