PrimeToIndexCharacterExtension.lean

theorem cyclicCharacterRestriction_injective_of_index_coprime
    (H : Subgroup G) [H.Normal] (n : ℕ) (hcop : H.index.Coprime n) :
    Function.Injective
      (fun φ : G →* Multiplicative (ZMod n) => φ.comp H.subtype) := by
  intro φ ψ hres
  apply MonoidHom.ext
  intro g
  have hpow : g ^ H.index ∈ H := by
    apply (QuotientGroup.eq_one_iff (g ^ H.index)).mp
    change (QuotientGroup.mk' H) (g ^ H.index) = 1
    rw [map_pow, Subgroup.index_eq_card]
    exact pow_card_eq_one'
  have heq := DFunLike.congr_fun hres (⟨g ^ H.index, hpow⟩ : H)
  change φ (g ^ H.index) = ψ (g ^ H.index) at heq
  rw [map_pow, map_pow] at heq
  have hunit : IsUnit (H.index : ZMod n) :=
    (ZMod.isUnit_iff_coprime H.index n).mpr hcop
  apply Multiplicative.toAdd.injective
  apply hunit.mul_left_cancel
  simpa only [toAdd_pow, nsmul_eq_mul] using
    congrArg (fun z : Multiplicative (ZMod n) => z.toAdd) heq

def primeToIndexCharacterExtension
    (H : OpenSubgroup G) [H.toSubgroup.FiniteIndex] (n : ℕ)
    (φ : H →ₜ* Multiplicative (ZMod n)) : G →ₜ* Multiplicative (ZMod n) where
  toFun g := Multiplicative.ofAdd
    ((H.toSubgroup.index : ZMod n)⁻¹ * (openSubgroupTransfer H φ g).toAdd)
  map_one' := by
    change (H.toSubgroup.index : ZMod n)⁻¹ * (openSubgroupTransfer H φ 1).toAdd = 0
    rw [map_one, toAdd_one, mul_zero]
  map_mul' := by
    intro x y
    change (H.toSubgroup.index : ZMod n)⁻¹ *
      (openSubgroupTransfer H φ (x * y)).toAdd = _
    rw [map_mul, toAdd_mul]
    exact mul_add _ _ _
  continuous_toFun := by
    change Continuous fun g =>
      (H.toSubgroup.index : ZMod n)⁻¹ * (openSubgroupTransfer H φ g).toAdd
    exact continuous_const.mul (openSubgroupTransfer H φ).continuous_toFun

theorem primeToIndexCharacterExtension_subtype
    (H : OpenSubgroup G) [H.toSubgroup.Normal] [H.toSubgroup.FiniteIndex]
    (n : ℕ) (hindex : H.toSubgroup.index.Coprime n)
    (φ : H →ₜ* Multiplicative (ZMod n))
    (hinv : ∀ (g : G) (h : H), φ (MulAut.conjNormal g h) = φ h) (h : H) :
    primeToIndexCharacterExtension H n φ (h : G) = φ h