Module

FiniteResidueCharacterScaling.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteResidueCharacterScaling

4 declarations indexed from sourceView source ↗

Module documentation

Scaling finite residue characters by characteristic powers

Proves injectivity of exponential-characteristic-power maps on field units and surjectivity on finite subgroups. Scaling a character by such a power preserves its kernel and, for a finite source group, its range.

Imports4

Mathlib.Algebra.CharP.Reduced
Mathlib.Algebra.CharP.Frobenius
Mathlib.Algebra.Group.Subgroup.Finite
Mathlib.Data.Fintype.Card

Imported by2

theorem

residueUnits_expCharPow_injective

L27 ↗

RamificationTheory.HilbertRamification.residueUnits_expCharPow_injective

Documentation

Residue-characteristic-power maps are injective on field units.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]

Lean source · full declaration

theorem residueUnits_expCharPow_injective (p a : ℕ) [ExpChar k p] :
    Function.Injective (fun x : kˣ => x ^ (p ^ a)) := by
  intro x y h
  apply Units.ext
  apply iterateFrobenius_inj k p a
  exact congrArg (fun z : kˣ => (z : k)) h

theorem

finiteSubgroup_expCharPow_surjective

L35 ↗

RamificationTheory.HilbertRamification.finiteSubgroup_expCharPow_surjective

Documentation

Such power maps are onto every actual finite subgroup of field units.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]

Lean source · full declaration

theorem finiteSubgroup_expCharPow_surjective
    (H : Subgroup kˣ) [Finite H] (p a : ℕ) [ExpChar k p] :
    Function.Surjective (fun x : H => x ^ (p ^ a)) := by
  apply Finite.surjective_of_injective
  intro x y h
  apply Subtype.ext
  apply residueUnits_expCharPow_injective p a
  exact congrArg (fun z : H => (z : kˣ)) h

theorem

residueCharacter_expCharPow_ker

L48 ↗

RamificationTheory.HilbertRamification.residueCharacter_expCharPow_ker

Documentation

Scaling an actual residue-unit character by a residue-characteristic power preserves its actual kernel.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]
variable {G : Type v} [Group G]

Lean source · statement

theorem residueCharacter_expCharPow_ker (f : G →* kˣ) (p a : ℕ) [ExpChar k p] :
    ((powMonoidHom (p ^ a)).comp f).ker = f.ker

theorem

finiteResidueCharacter_expCharPow_range

L61 ↗

RamificationTheory.HilbertRamification.finiteResidueCharacter_expCharPow_range

Documentation

Scaling an actual finite residue-unit character preserves its entire image.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification
universe u v
variable {k : Type u} [Field k]
variable {G : Type v} [Group G]

Lean source · statement

theorem finiteResidueCharacter_expCharPow_range
    [Finite G] (f : G →* kˣ) (p a : ℕ) [ExpChar k p] :
    ((powMonoidHom (p ^ a)).comp f).range = f.range

Module documentation

Scaling finite residue characters by characteristic powers

Declarations

residueUnits_expCharPow_injective

finiteSubgroup_expCharPow_surjective

residueCharacter_expCharPow_ker

finiteResidueCharacter_expCharPow_range