FiniteKummerNormalizedGenerator.lean

theorem nthRootsSubgroup_natCard_of_primitiveRoots
    (E : Type) [Field E] (p : ℕ+)
    (hmu : (primitiveRoots (p : ℕ) E).Nonempty) :
    Nat.card (nthRootsSubgroup E (p : ℕ)) = (p : ℕ)

theorem chosenSimpleKummerRootCharacter_surjective_of_nontrivial
    (K : Type) [Field K] (p : ℕ+) [Fact ((p : ℕ).Prime)]
    (hnK : ((p : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) (b : Kˣ)
    (hNT : Nontrivial
      Gal((chosenSimpleKummerExtension K p hnK b)/K)) :
    Function.Surjective
      (chosenSimpleKummerRootCharacter K p hnK hmu b)

theorem exists_chosenSimpleKummerGenerator_rootCharacter_eq
    (K : Type) [Field K] (p : ℕ+) [Fact ((p : ℕ).Prime)]
    (hnK : ((p : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) (b : Kˣ)
    (hNT : Nontrivial
      Gal((chosenSimpleKummerExtension K p hnK b)/K)) :
    let E := chosenSimpleKummerExtension K p hnK b
    let zetaUnit := finiteKummerCoefficientRootUnit K E p hmu
    let zeta : nthRootsSubgroup E (p : ℕ) :=
      ⟨zetaUnit,
        (finiteKummerCoefficientRootUnit_isPrimitiveRoot K E p hmu).pow_eq_one⟩
    ∃ g : Gal(E/K),
      (∀ sigma : Gal(E/K), sigma ∈ Subgroup.zpowers g) ∧
      chosenSimpleKummerRootCharacter K p hnK hmu b g = zeta := by
  dsimp only
  let E := chosenSimpleKummerExtension K p hnK b
  let chi := chosenSimpleKummerRootCharacter K p hnK hmu b
  let zetaUnit := finiteKummerCoefficientRootUnit K E p hmu
  have hzetaUnit : IsPrimitiveRoot zetaUnit (p : ℕ) :=
    finiteKummerCoefficientRootUnit_isPrimitiveRoot K E p hmu
  let zeta : nthRootsSubgroup E (p : ℕ) :=
    ⟨zetaUnit, hzetaUnit.pow_eq_one⟩
  obtain ⟨g, hg⟩ :=
    chosenSimpleKummerRootCharacter_surjective_of_nontrivial
      K p hnK hmu b hNT zeta
  refine ⟨g, ?_, hg⟩
  intro sigma
  have hcard : Nat.card (nthRootsSubgroup E (p : ℕ)) = (p : ℕ) := by
    let zetaE : E := algebraMap K E hmu.choose
    have hzetaE : IsPrimitiveRoot zetaE (p : ℕ) :=
      ((mem_primitiveRoots p.pos).mp hmu.choose_spec).map_of_injective
        (algebraMap K E).injective
    apply nthRootsSubgroup_natCard_of_primitiveRoots E p
    exact ⟨zetaE, (mem_primitiveRoots p.pos).mpr hzetaE⟩
  have hzeta : zeta ≠ 1 := by
    intro h
    apply hzetaUnit.ne_one (Fact.out : (p : ℕ).Prime).one_lt
    exact congrArg Subtype.val h
  have hmem : chi sigma ∈ Subgroup.zpowers zeta :=
    mem_zpowers_of_prime_card hcard hzeta
  obtain ⟨i, hi⟩ := Subgroup.mem_zpowers_iff.mp hmem
  apply Subgroup.mem_zpowers_iff.mpr
  refine ⟨i, ?_⟩
  apply chosenSimpleKummerRootCharacter_injective K p hnK hmu b
  rw [map_zpow, hg, hi]

theorem exists_chosenSimpleKummerGenerator_rootCharacter_eq_inv
    (K : Type) [Field K] (p : ℕ+) [Fact ((p : ℕ).Prime)]
    (hnK : ((p : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) (b : Kˣ)
    (hNT : Nontrivial
      Gal((chosenSimpleKummerExtension K p hnK b)/K)) :
    let E := chosenSimpleKummerExtension K p hnK b
    let zetaUnit := finiteKummerCoefficientRootUnit K E p hmu
    let zeta : nthRootsSubgroup E (p : ℕ) :=
      ⟨zetaUnit,
        (finiteKummerCoefficientRootUnit_isPrimitiveRoot K E p hmu).pow_eq_one⟩
    ∃ g : Gal(E/K),
      (∀ sigma : Gal(E/K), sigma ∈ Subgroup.zpowers g) ∧
      chosenSimpleKummerRootCharacter K p hnK hmu b g = zeta⁻¹ := by
  dsimp only
  obtain ⟨g, hg, hchi⟩ :=
    exists_chosenSimpleKummerGenerator_rootCharacter_eq
      K p hnK hmu b hNT
  refine ⟨g⁻¹, ?_, ?_⟩
  · intro sigma
    rw [Subgroup.zpowers_inv]
    exact hg sigma
  · rw [map_inv, hchi]

def intermediateFieldUnitsRepHom
    (E F : IntermediateField K Ω) (hEF : E ≤ F)
    [Normal K E] :
    Rep.res (intermediateFieldRestrictNormalHom E F hEF)
        (Rep.ofAlgebraAutOnUnits K E) ⟶
      Rep.ofAlgebraAutOnUnits K F