PrimeExponentCharacters.lean

theorem exists_prime_character_finite
    {A : Type*} [CommGroup A] [Finite A]
    (hA : ∀ a : A, a ^ q = 1) {x : A} (hx : x ≠ 1) :
    ∃ χ : A →* Multiplicative (ZMod q), χ x ≠ 1

theorem exists_prime_character_profinite
    {A : Type*} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
    [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
    (hA : ∀ a : A, a ^ q = 1) {x : A} (hx : x ≠ 1) :
    ∃ χ : A →ₜ* Multiplicative (ZMod q), χ x ≠ 1

theorem exists_prime_character_abelianModPower
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    {x : abelianModPower G q} (hx : x ≠ 1) :
    ∃ χ : abelianModPower G q →ₜ* Multiplicative (ZMod q), χ x ≠ 1

theorem injective_prod_abelianModPowerMap_of_character_surjective
    {ι : Type*} [Fintype ι]
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (H : ι → Type*) [∀ i, Group (H i)] [∀ i, TopologicalSpace (H i)]
    [∀ i, IsTopologicalGroup (H i)] [∀ i, CompactSpace (H i)]
    [∀ i, T2Space (H i)] [∀ i, TotallyDisconnectedSpace (H i)]
    (f : ∀ i, H i →ₜ* G)
    (hchar : Function.Surjective (fun χ : G →ₜ* Multiplicative (ZMod q) =>
      fun i => χ.comp (f i))) :
    Function.Injective (fun z : ∀ i, abelianModPower (H i) q =>
      ∏ i, abelianModPowerMap q (f i) (z i)) := by
  classical
  have hpow : ∀ a : Multiplicative (ZMod q), a ^ q = 1 := by
    intro a
    apply Multiplicative.toAdd.injective
    change q • a.toAdd = (0 : ZMod q)
    simp only [nsmul_eq_mul, ZMod.natCast_self, zero_mul]
  have hker : ∀ z : (∀ i, abelianModPower (H i) q),
      (∏ i, abelianModPowerMap q (f i) (z i)) = 1 → z = 1 := by
    intro z hz
    funext i
    by_contra hzi
    obtain ⟨χi, hχi⟩ := exists_prime_character_abelianModPower hzi
    let ψ : ∀ j, H j →ₜ* Multiplicative (ZMod q) :=
      Function.update 1 i (χi.comp (abelianModPowerMk (H i) q))
    obtain ⟨χ, hχ⟩ := hchar ψ
    let χbar := abelianModPowerLift q χ hpow
    have hi : χbar (abelianModPowerMap q (f i) (z i)) = χi (z i) := by
      obtain ⟨a, ha⟩ := abelianModPowerMk_surjective (G := H i) q (z i)
      rw [← ha]
      change χ (f i a) = χi (abelianModPowerMk (H i) q a)
      have h := DFunLike.congr_fun (congrFun hχ i) a
      simp only [ψ, Function.update_self] at h
      exact h
    have hj (j : ι) (hji : j ≠ i) : χbar (abelianModPowerMap q (f j) (z j)) = 1 := by
      obtain ⟨a, ha⟩ := abelianModPowerMk_surjective (G := H j) q (z j)
      rw [← ha]
      change χ (f j a) = 1
      have h := DFunLike.congr_fun (congrFun hχ j) a
      simp only [ψ, Function.update_of_ne hji, Pi.one_apply] at h
      exact h
    have hprod : (∏ j, χbar (abelianModPowerMap q (f j) (z j))) = χi (z i) := by
      rw [Finset.prod_eq_single i]
      · exact hi
      · intro j _ hji
        exact hj j hji
      · intro h
        exact False.elim (h (Finset.mem_univ i))
    apply hχi
    rw [← hprod, ← map_prod, hz, map_one]
  intro x y hxy
  have hdiv : (∏ i, abelianModPowerMap q (f i) ((x / y) i)) = 1 := by
    change (∏ i, abelianModPowerMap q (f i) (x i / y i)) = 1
    simp only [map_div, Finset.prod_div_distrib]
    exact div_eq_one.mpr hxy
  exact div_eq_one.mp (hker (x / y) hdiv)