Module

InertiaCharacterConjugation.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.InertiaCharacterConjugation

3 declarations indexed from sourceView source ↗

Module documentation

Conjugation of inertia characters

Relate the residue-unit inertia character to decomposition and residue actions. Finite inertia characters are injective in residue characteristic zero.

Imports3

Imported by2

theorem

valueTrivialInertiaResidueUnitHom_decomposition_arg

L25 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaResidueUnitHom_decomposition_arg

Documentation

A finite-order decomposition automorphism does not change the argument of an inertia character, because it preserves the value of every field element.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaResidueUnitHom_decomposition_arg
    (A : _root_.ValuationSubring L) (τ : valueTrivialInertiaGroup K A)
    (g : decompositionGroup K A) (hg : IsOfFinOrder g) (x : Lˣ) :
    valueTrivialInertiaResidueUnitHom K A τ
      (Units.mapEquiv (g : Gal(L/K)).toMulEquiv x) =
      valueTrivialInertiaResidueUnitHom K A τ x

theorem

valueTrivialInertiaResidueUnitHom_conj

L45 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaResidueUnitHom_conj

Documentation

The actual residue-unit character intertwines conjugation with residue action.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

theorem valueTrivialInertiaResidueUnitHom_conj
    (A : _root_.ValuationSubring L) [Finite (inertiaGroup K A)]
    (g : decompositionGroup K A) (τ : inertiaGroup K A) (x : Lˣ) :
    let htop := valueTrivialInertiaGroup_eq_top_of_finite K A
    let s : valueTrivialInertiaGroup K A := ⟨τ, htop.symm ▸ Subgroup.mem_top τ⟩
    let t : valueTrivialInertiaGroup K A :=
      ⟨MulAut.conjNormal g τ, htop.symm ▸ Subgroup.mem_top _⟩
    (valueTrivialInertiaResidueUnitHom K A t x : IsLocalRing.ResidueField A) =
      residueAction K A g
        (valueTrivialInertiaResidueUnitHom K A s
          (Units.mapEquiv (g : Gal(L/K)).symm.toMulEquiv x) : IsLocalRing.ResidueField A) := by
  dsimp only
  rw [valueTrivialInertiaResidueUnitHom_apply, valueTrivialInertiaResidueUnitHom_apply,
    _root_.ValuationSubring.coe_unitGroupToResidueFieldUnits_apply,
    _root_.ValuationSubring.coe_unitGroupToResidueFieldUnits_apply]
  change IsLocalRing.residue A _ = IsLocalRing.residue A (g • _)
  apply congrArg (IsLocalRing.residue A)
  apply Subtype.ext
  change _ = (g : Gal(L/K)) (_ : L)
  simp only [_root_.ValuationSubring.coe_unitGroupMulEquiv_apply,
    valueTrivialAutomorphismUnit_coe, automorphismUnitQuotient, Units.val_div_eq_div_val]
  change ((g : Gal(L/K)) (((τ : decompositionGroup K A) : Gal(L/K))
      ((g : Gal(L/K)).symm (x : L))) / (x : L)) =
    (g : Gal(L/K))
      ((((τ : decompositionGroup K A) : Gal(L/K)) ((g : Gal(L/K)).symm (x : L))) /
        ((g : Gal(L/K)).symm (x : L)))
  rw [map_div₀, AlgEquiv.apply_symm_apply]

theorem

valueTrivialInertiaCharacterHom_injective_of_residueCharZero

L74 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaCharacterHom_injective_of_residueCharZero

Documentation

In residue characteristic zero the finite inertia character is injective.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaCharacterHom_injective_of_residueCharZero
    (A : _root_.ValuationSubring L) [Finite (inertiaGroup K A)]
    [CharZero (IsLocalRing.ResidueField A)] :
    Function.Injective (valueTrivialInertiaCharacterHom K A)

Module documentation

Conjugation of inertia characters

Declarations

valueTrivialInertiaResidueUnitHom_decomposition_arg

valueTrivialInertiaResidueUnitHom_conj

valueTrivialInertiaCharacterHom_injective_of_residueCharZero