Module

LocalTameCharacterExactness.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.LocalTameCharacterExactness

2 declarations indexed from sourceView source ↗

Module documentation

Surjectivity and kernel of the local tame character

Proves that the local tame character group map is surjective and that its kernel is the principal-unit inertia subgroup.

Imports3

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.LocalTameCharacterGroupMap
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingInertiaCharacterKernel
Mathlib.Algebra.Group.Subgroup.Ker

Imported by2

theorem

localTameCharacterGroupMap_surjective

L26 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.localTameCharacterGroupMap_surjective

Documentation

The native map retains the actual finite character's surjectivity.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
  (G : Type u) [Group G] [Finite G] [MulSemiringAction G R]

Lean source · statement

theorem localTameCharacterGroupMap_surjective :
    Function.Surjective (localTameCharacterGroupMap R G).toFun

theorem

localTameCharacterGroupMap_ker

L31 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.localTameCharacterGroupMap_ker