FiniteKummerNormalizedCoordinate.lean

theorem finiteKummerCoefficientRoot_generates_nthRootsSubgroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    (p : ℕ+) [Fact ((p : ℕ).Prime)]
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) :
    let zetaUnit := finiteKummerCoefficientRootUnit K L p hmu
    let zeta : nthRootsSubgroup L (p : ℕ) :=
      ⟨zetaUnit,
        (finiteKummerCoefficientRootUnit_isPrimitiveRoot K L p hmu).pow_eq_one⟩
    ∀ x : nthRootsSubgroup L (p : ℕ), x ∈ Subgroup.zpowers zeta := by
  dsimp only
  let zetaUnit := finiteKummerCoefficientRootUnit K L p hmu
  have hzetaUnit : IsPrimitiveRoot zetaUnit (p : ℕ) :=
    finiteKummerCoefficientRootUnit_isPrimitiveRoot K L p hmu
  let zeta : nthRootsSubgroup L (p : ℕ) :=
    ⟨zetaUnit, hzetaUnit.pow_eq_one⟩
  intro x
  have hcard : Nat.card (nthRootsSubgroup L (p : ℕ)) = (p : ℕ) := by
    apply nthRootsSubgroup_natCard_of_primitiveRoots
    exact ⟨algebraMap K L hmu.choose,
      (mem_primitiveRoots p.pos).mpr
        (((mem_primitiveRoots p.pos).mp hmu.choose_spec).map_of_injective
          (algebraMap K L).injective)⟩
  have hcardPrime : (Nat.card (nthRootsSubgroup L (p : ℕ))).Prime := by
    rw [hcard]
    exact Fact.out
  let : Fact (Nat.card (nthRootsSubgroup L (p : ℕ))).Prime :=
    ⟨hcardPrime⟩
  apply mem_zpowers_of_prime_card hcard
  intro h
  apply hzetaUnit.ne_one (Fact.out : (p : ℕ).Prime).one_lt
  exact congrArg Subtype.val h

theorem finiteCyclicGeneratorCoordinate_eq_neg_characterCoordinate
    {G M : Type} [Group G] [Fintype G] [Group M]
    (chi : G →* M) (g : G)
    (hg : ∀ sigma : G, sigma ∈ Subgroup.zpowers g)
    (zeta : M) (hzeta : ∀ x : M, x ∈ Subgroup.zpowers zeta)
    (hcard : Nat.card M = Nat.card G) (hchi : chi g = zeta⁻¹)
    (sigma : G) :
    finiteCyclicGeneratorCoordinate g hg sigma =
      -Multiplicative.toAdd
        ((zmodMulEquivOfGenerator hzeta hcard).symm (chi sigma))

def chosenSimpleKummerGeneratorCoordinate
    (K : Type) [Field K] (p : ℕ+)
    (hnK : ((p : ℕ) : K) ≠ 0) (b : Kˣ)
    (g : Gal((chosenSimpleKummerExtension K p hnK b)/K))
    (hg : ∀ sigma : Gal((chosenSimpleKummerExtension K p hnK b) / K),
      sigma ∈ Subgroup.zpowers g)
    (sigma : Gal((chosenSimpleKummerExtension K p hnK b) / K)) :
    ZMod (Nat.card Gal((chosenSimpleKummerExtension K p hnK b) / K))

def chosenSimpleKummerRootCharacterCoordinate
    (K : Type) [Field K] (p : ℕ+) [Fact ((p : ℕ).Prime)]
    (hnK : ((p : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (p : ℕ) K).Nonempty) (b : Kˣ)
    (hcardG : Nat.card
      Gal((chosenSimpleKummerExtension K p hnK b)/K) = (p : ℕ))
    (sigma : Gal((chosenSimpleKummerExtension K p hnK b)/K)) :
    ZMod (Nat.card Gal((chosenSimpleKummerExtension K p hnK b) / K))

theorem exists_chosenSimpleKummerNormalizedGeneratorCoordinate
    (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))
        (hg : ∀ sigma : Gal(E / K), sigma ∈ Subgroup.zpowers g)
        (hcardG : Nat.card Gal(E / K) = (p : ℕ)),
      chosenSimpleKummerRootCharacter K p hnK hmu b g = zeta⁻¹ ∧
      ∀ sigma : Gal(E / K),
        chosenSimpleKummerGeneratorCoordinate K p hnK b g hg sigma =
          -chosenSimpleKummerRootCharacterCoordinate
            K p hnK hmu b hcardG sigma := 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
  let zeta : nthRootsSubgroup E (p : ℕ) :=
    ⟨zetaUnit,
      (finiteKummerCoefficientRootUnit_isPrimitiveRoot K E p hmu).pow_eq_one⟩
  obtain ⟨g, hg, hchiG⟩ :=
    exists_chosenSimpleKummerGenerator_rootCharacter_eq_inv
      K p hnK hmu b hNT
  have hmuE : (primitiveRoots (p : ℕ) E).Nonempty :=
    ⟨algebraMap K E hmu.choose,
      (mem_primitiveRoots p.pos).mpr
        (((mem_primitiveRoots p.pos).mp hmu.choose_spec).map_of_injective
          (algebraMap K E).injective)⟩
  have hrootCard : Nat.card (nthRootsSubgroup E (p : ℕ)) = (p : ℕ) :=
    nthRootsSubgroup_natCard_of_primitiveRoots E p hmuE
  have hcardG : Nat.card Gal(E / K) = (p : ℕ) := by
    calc
      Nat.card Gal(E / K) = Nat.card (nthRootsSubgroup E (p : ℕ)) := by
        apply Nat.card_congr
        exact Equiv.ofBijective chi ⟨
          chosenSimpleKummerRootCharacter_injective K p hnK hmu b,
          chosenSimpleKummerRootCharacter_surjective_of_nontrivial
            K p hnK hmu b hNT⟩
      _ = (p : ℕ) := hrootCard
  refine ⟨g, hg, hcardG, hchiG, ?_⟩
  intro sigma
  let : FiniteDimensional K E :=
    chosenSimpleKummerExtension_finiteDimensional K p hnK b
  change finiteCyclicGeneratorCoordinate g hg sigma = _
  exact finiteCyclicGeneratorCoordinate_eq_neg_characterCoordinate
    chi g hg zeta
    (finiteKummerCoefficientRoot_generates_nthRootsSubgroup K E p hmu)
    (hrootCard.trans hcardG.symm) hchiG sigma

theorem finiteCyclic_one_generates_of_subsingleton
    {G : Type} [Group G] [Subsingleton G] (x : G) :
    x ∈ Subgroup.zpowers (1 : G)

theorem finiteCyclicGeneratorCoordinate_eq_zero_of_subsingleton
    {G : Type} [Group G] [Fintype G] [Subsingleton G] (x : G) :
    finiteCyclicGeneratorCoordinate 1
      finiteCyclic_one_generates_of_subsingleton x = 0

theorem finiteCyclicCarryTwoCocycle_eq_zero_of_subsingleton
    {R G : Type} [CommRing R] [CommGroup G] [Fintype G] [Subsingleton G]
    (A : Rep R G)
    (a : LinearMap.ker
      (Rep.applyAsHom A (1 : G) - 𝟙 A).hom.toLinearMap)
    (x : G × G) :
    finiteCyclicCarryTwoCocycle A 1
      finiteCyclic_one_generates_of_subsingleton a x = 0