KummerNormPowerClassDegree.lean

theorem kummerAlgebraNormSubgroup_index_eq_chosenRadicalDegree
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
    (kummerAlgebraNormSubgroup K n a).index =
      Module.finrank K (KummerTheory.chosenSimpleKummerExtension K n hnK a)

theorem chosenRoot_pow_mem_base_iff_powerClass_pow_eq_one
    (K : Type) [Field K] (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) (m : ℕ) :
    let E := KummerTheory.chosenSimpleKummerExtension K n hnK a
    let β := KummerTheory.chosenSimpleKummerRootUnit K n hnK a
    ((β ^ m : Eˣ) : E) ∈ Set.range (algebraMap K E) ↔
      (powerClass K n a) ^ m = 1 := by
  let E := KummerTheory.chosenSimpleKummerExtension K n hnK a
  let β : Eˣ := KummerTheory.chosenSimpleKummerRootUnit K n hnK a
  let ι : Kˣ →* Eˣ := Units.map (algebraMap K E).toMonoidHom
  have hβ : β ^ (n : ℕ) = ι a :=
    KummerTheory.chosenSimpleKummerRootUnit_pow K n hnK a
  have hι : Function.Injective ι :=
    Units.map_injective (algebraMap K E).injective
  constructor
  · rintro ⟨b, hb⟩
    have hbne : b ≠ 0 := by
      intro hz
      have hzero : ((β ^ m : Eˣ) : E) = 0 := by
        simpa only [hz, map_zero] using hb.symm
      exact (β ^ m).ne_zero hzero
    let bu : Kˣ := Units.mk0 b hbne
    have hβm : β ^ m = ι bu := by
      apply Units.ext
      exact hb.symm
    have ha : a ^ m = bu ^ (n : ℕ) := by
      apply hι
      calc
        ι (a ^ m) = (ι a) ^ m := map_pow ι a m
        _ = (β ^ (n : ℕ)) ^ m := by rw [hβ]
        _ = (β ^ m) ^ (n : ℕ) := pow_right_comm β (n : ℕ) m
        _ = (ι bu) ^ (n : ℕ) := by rw [hβm]
        _ = ι (bu ^ (n : ℕ)) := (map_pow ι bu (n : ℕ)).symm
    rw [← map_pow (powerClass K n) a m]
    exact (QuotientGroup.eq_one_iff (a ^ m)).2 ⟨bu, ha.symm⟩
  · intro hclass
    have ha : a ^ m ∈ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range :=
      (QuotientGroup.eq_one_iff (a ^ m)).1
        ((map_pow (powerClass K n) a m).symm.trans hclass)
    obtain ⟨bu, hbu⟩ := ha
    have hbu' : bu ^ (n : ℕ) = a ^ m := hbu
    let u : Eˣ := β ^ m / ι bu
    have hu : u ^ (n : ℕ) = 1 := by
      have hnum : (β ^ m) ^ (n : ℕ) = ι (a ^ m) := by
        calc
          (β ^ m) ^ (n : ℕ) = (β ^ (n : ℕ)) ^ m := pow_right_comm β m (n : ℕ)
          _ = (ι a) ^ m := by rw [hβ]
          _ = ι (a ^ m) := (map_pow ι a m).symm
      have hden : (ι bu) ^ (n : ℕ) = ι (a ^ m) := by
        rw [← map_pow, hbu']
      change (β ^ m / ι bu) ^ (n : ℕ) = 1
      rw [div_pow, hnum, hden, div_self']
    obtain ⟨ζ, hζ⟩ :=
      KummerTheory.nthRootsOfUnityInBase_of_primitiveRoots
        (K := K) (L := E) n hmu u hu
    refine ⟨(ζ * bu : Kˣ), ?_⟩
    have hβm : β ^ m = ι (ζ * bu) := by
      calc
        β ^ m = u * ι bu := by
          dsimp only [u]
          exact (div_mul_cancel (β ^ m) (ι bu)).symm
        _ = ι ζ * ι bu := by rw [hζ]
        _ = ι (ζ * bu) := (map_mul ι ζ bu).symm
    exact (congrArg Units.val hβm).symm

theorem chosenSimpleKummerExtension_finrank_eq_powerClassOrder
    (K : Type) [Field K] (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
    Module.finrank K (KummerTheory.chosenSimpleKummerExtension K n hnK a) =
      orderOf (powerClass K n a)