NormalRestrictionCharacterExtension.lean

theorem character_map_algebraMap_eq
    {A : Type*} [CommGroup A] [TopologicalSpace A]
    (e : AlgebraicClosure K ≃ₐ[K] AlgebraicClosure E)
    (χ : Gal(AlgebraicClosure K/K) →ₜ* A)
    (σ : Gal(AlgebraicClosure E/E)) :
    χ (Field.absoluteGaloisGroup.map (algebraMap K E) σ) =
      χ ((galoisClosureTransport e).symm (σ.restrictScalars K))

theorem finiteExtensionGaloisOpenSubgroup_index
    (K E Ω : Type*) [Field K] [Field E] [Field Ω]
    [Algebra K E] [Algebra E Ω] [Algebra K Ω] [IsScalarTower K E Ω]
    [FiniteDimensional K E] [IsGalois K E] [IsAlgClosure E Ω] :
    (GaloisCohomology.finiteExtensionGaloisOpenSubgroup K E Ω).toSubgroup.index =
      Module.finrank K E

theorem absoluteCharacterRestriction_injective_of_coprime_finrank
    [FiniteDimensional K E] [IsGalois K E]
    (n : ℕ) (hn : (Module.finrank K E).Coprime n) :
    Function.Injective (fun χ : Gal(AlgebraicClosure K/K) →ₜ* Multiplicative (ZMod n) =>
      (χ.comp (Field.absoluteGaloisGroup.map (algebraMap K E)) :
        Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod n))) := by
  have : IsAlgClosure K (AlgebraicClosure E) := IsAlgClosure.ofAlgebraic K E _
  let e := IsAlgClosure.equiv K (AlgebraicClosure K) (AlgebraicClosure E)
  let c := galoisClosureTransport e
  let c' : Gal(AlgebraicClosure E/K) →ₜ* Gal(AlgebraicClosure K/K) :=
    ⟨c.symm.toMonoidHom, c.symm.continuous⟩
  let H := GaloisCohomology.finiteExtensionGaloisOpenSubgroup K E (AlgebraicClosure E)
  let d := GaloisCohomology.finiteExtensionGaloisOpenSubgroupEquiv K E (AlgebraicClosure E)
  have : H.toSubgroup.Normal := by
    change (AlgEquiv.restrictScalarsHom K :
      Gal(AlgebraicClosure E/E) →* Gal(AlgebraicClosure E/K)).range.Normal
    rw [restrictScalarsHom_range_eq_normalRestrictionKer K E (AlgebraicClosure E)]
    infer_instance
  have hindex : H.toSubgroup.index.Coprime n := by
    rw [finiteExtensionGaloisOpenSubgroup_index K E (AlgebraicClosure E)]
    exact hn
  intro φ ψ hres
  have h : (φ.comp c').toMonoidHom =
      (ψ.comp c').toMonoidHom := by
    apply ClassFieldTower.Cohomology.cyclicCharacterRestriction_injective_of_index_coprime
      H.toSubgroup n hindex
    apply MonoidHom.ext
    intro h
    obtain ⟨σ, rfl⟩ := d.surjective h
    change φ (c.symm (σ.restrictScalars K)) = ψ (c.symm (σ.restrictScalars K))
    exact (character_map_algebraMap_eq e φ σ).symm.trans
      ((DFunLike.congr_fun hres σ).trans (character_map_algebraMap_eq e ψ σ))
  apply ContinuousMonoidHom.ext
  intro σ
  have heq := DFunLike.congr_fun h (c σ)
  change φ (c.symm (c σ)) = ψ (c.symm (c σ)) at heq
  simpa only [c.symm_apply_apply] using heq

theorem exists_absoluteCharacter_extension_of_coprime_finrank
    [FiniteDimensional K E] [IsGalois K E]
    (n : ℕ) (hn : (Module.finrank K E).Coprime n)
    (χ : Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod n))
    (hinv : ∀ (δ : Gal(E/K)) (σ : Gal(AlgebraicClosure E/E)),
      χ (absoluteGaloisConjugate δ.toRingEquiv σ) = χ σ) :
    ∃ ψ : Gal(AlgebraicClosure K/K) →ₜ* Multiplicative (ZMod n),
      (ψ.comp (Field.absoluteGaloisGroup.map (algebraMap K E)) :
        Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod n)) = χ