RamificationTheory.HilbertRamification.DiscreteValuationRing.inertiaResidueCharacter_eq_one_iff
The character kernel is exactly the actual principal-unit action on all ring elements. The ratios and their residue-one property are constructed.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]Lean source · statement
theorem inertiaResidueCharacter_eq_one_iff
(σ : (maximalIdeal R).inertia G) :
inertiaResidueCharacter R G σ = 1 ↔
∀ x : R, ∃ a : Rˣ,
(σ : G) • x = x * (a : R) ∧ residue R (a : R) = 1