RootCharacter.lean

theorem exists_zmod_of_pow_eq {x : Ω} (hx : x ^ p = x) :
    ∃ z : ZMod p, (ZMod.castHom (dvd_refl p) Ω) z = x

theorem exists_root [IsSepClosed Ω] (a : Ω) : ∃ β : Ω, β ^ p - β = a

theorem rootDifference_pow_eq (a : K) (β : Ω)
    (hβ : β ^ p - β = algebraMap K Ω a) (σ : Gal(Ω/K)) :
    (σ β - β) ^ p = σ β - β

def rootCharacterValue (a : K) (β : Ω)
    (hβ : β ^ p - β = algebraMap K Ω a) (σ : Gal(Ω/K)) : ZMod p

theorem rootCharacterValue_cast (a : K) (β : Ω)
    (hβ : β ^ p - β = algebraMap K Ω a) (σ : Gal(Ω/K)) :
    (ZMod.castHom (dvd_refl p) Ω) (rootCharacterValue p Ω a β hβ σ) = σ β - β

def rootCharacter (a : K) (β : Ω)
    (hβ : β ^ p - β = algebraMap K Ω a) :
    Gal(Ω/K) →ₜ* Multiplicative (ZMod p) where
  toFun σ := Multiplicative.ofAdd (rootCharacterValue p Ω a β hβ σ)
  map_one' := by
    change rootCharacterValue p Ω a β hβ 1 = 0
    apply (ZMod.castHom (dvd_refl p) Ω).injective
    rw [rootCharacterValue_cast, map_zero]
    exact sub_self β
  map_mul' σ τ := by
    change rootCharacterValue p Ω a β hβ (σ * τ) =
      rootCharacterValue p Ω a β hβ σ + rootCharacterValue p Ω a β hβ τ
    apply (ZMod.castHom (dvd_refl p) Ω).injective
    rw [map_add, rootCharacterValue_cast, rootCharacterValue_cast, rootCharacterValue_cast]
    have hfix : σ (τ β - β) = τ β - β := by
      rw [← rootCharacterValue_cast p Ω a β hβ τ]
      simp only [ZMod.castHom_apply, ZMod.cast_eq_val, map_natCast]
    change σ (τ β) - β = (σ β - β) + (τ β - β)
    rw [map_sub] at hfix
    linear_combination hfix
  continuous_toFun := by
    apply IsLocallyConstant.continuous
    apply (IsLocallyConstant.iff_exists_open _).mpr
    intro σ
    obtain ⟨U, hU, hσ, hconst⟩ :=
      (GaloisCohomology.isLocallyConstant_galois_apply (K := K) β).exists_open σ
    refine ⟨U, hU, hσ, ?_⟩
    intro τ hτ
    apply congrArg Multiplicative.ofAdd
    apply (ZMod.castHom (dvd_refl p) Ω).injective
    rw [rootCharacterValue_cast, rootCharacterValue_cast, hconst τ hτ]

theorem rootCharacter_cast (a : K) (β : Ω)
    (hβ : β ^ p - β = algebraMap K Ω a) (σ : Gal(Ω/K)) :
    (ZMod.castHom (dvd_refl p) Ω) ((rootCharacter p Ω a β hβ σ).toAdd) = σ β - β

theorem rootCharacter_eq (a : K) (β γ : Ω)
    (hβ : β ^ p - β = algebraMap K Ω a)
    (hγ : γ ^ p - γ = algebraMap K Ω a) :
    rootCharacter p Ω a β hβ = rootCharacter p Ω a γ hγ