FinitePlacePowerIndex.lean

theorem card_finitePlace_nthPowerQuotient
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v₀ : HeightOneSpectrum (𝓞 K)) :
    let ν :
        Valuation (v₀.adicCompletion K)
          (WithZero (Multiplicative ℤ)) :=
      Valued.v
    let F :=
      LocalFieldTheory.DiscreteValuationField.LocalField.ofWithZeroValuation ν
    letI :
        LocalFieldTheory.DiscreteValuationField.LocalField.MixedWithZeroValuationContext
          ν :=
      LocalFieldTheory.DiscreteValuationField.LocalField.mixedWithZeroValuationContext ν
    letI :
        Valued (v₀.adicCompletion K)
          (WithZero (Multiplicative ℤ)) :=
      Valued.mk' ν
    let d :=
      Module.finrank ℚ_[F.residueCharacteristic]
        (v₀.adicCompletion K)
    Nat.card
        ((v₀.adicCompletion K)ˣ ⧸
          (powMonoidHom (n : ℕ) :
            (v₀.adicCompletion K)ˣ →*
              (v₀.adicCompletion K)ˣ).range) =
      (n : ℕ) *
        ((n : ℕ) *
          F.residueCharacteristic ^
            (d *
              padicValNat F.residueCharacteristic (n : ℕ))) := by
  let ν :
      Valuation (v₀.adicCompletion K)
        (WithZero (Multiplicative ℤ)) :=
    Valued.v
  let F :=
    LocalFieldTheory.DiscreteValuationField.LocalField.ofWithZeroValuation ν
  let : NeZero (n : ℕ) := ⟨n.ne_zero⟩
  have hν : Function.Surjective ν :=
    v₀.valuedAdicCompletion_surjective K
  let :
      LocalFieldTheory.DiscreteValuationField.LocalField.MixedWithZeroValuationContext
        ν :=
    LocalFieldTheory.DiscreteValuationField.LocalField.mixedWithZeroValuationContext ν
  let :
      Valued (v₀.adicCompletion K)
        (WithZero (Multiplicative ℤ)) :=
    Valued.mk' ν
  let d :=
    Module.finrank ℚ_[F.residueCharacteristic]
      (v₀.adicCompletion K)
  obtain ⟨a, e⟩ :=
    chosenMixed_firstPrincipalUnitStructure_ofWithZeroValuation
      ν hν
  let U :=
    LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
      F.toCompleteDVF 1
  let A :=
    ZMod (F.residueCharacteristic ^ a) ×
      (Fin d → ℤ_[F.residueCharacteristic])
  let : Finite
      (A ⧸ LocalFieldTheory.nsmulAddSubgroup A (n : ℕ)) := by
    infer_instance
  let emul : U ≃* Multiplicative A := by
    let direct :
        Valued (v₀.adicCompletion K)
          (WithZero (Multiplicative ℤ)) :=
      Valued.mk' ν
    letI : TopologicalSpace (v₀.adicCompletion K) :=
      direct.toTopologicalSpace
    exact e.symm.toMulEquiv
  let : Finite
      (U ⧸
        (powMonoidHom (n : ℕ) : U →* U).range) :=
    LocalFieldTheory.finite_nthPowerQuotient_of_mulEquiv
      U (Multiplicative A) (n : ℕ) emul
  let hex := F.toCompleteDVF.exists_uniformizer
  let π := Classical.choose hex
  have hπ :
      F.toCompleteDVF.valuation.IsUniformizer
        (π : v₀.adicCompletion K) :=
    Classical.choose_spec hex
  let : Finite
      ((v₀.adicCompletion K)ˣ ⧸
        (powMonoidHom (n : ℕ) :
          (v₀.adicCompletion K)ˣ →*
            (v₀.adicCompletion K)ˣ).range) :=
    finite_fieldUnits_nthPowerQuotient_of_finite_principalUnits
      F.toCompleteDVF hπ (n : ℕ)
  have hindex :=
    LocalFieldTheory.DiscreteValuationField.LocalField.mixed_fieldIndex
      ν hν (n := (n : ℕ))
  have hroots :
      Nat.card
          ((powMonoidHom (n : ℕ) :
            (v₀.adicCompletion K)ˣ →*
              (v₀.adicCompletion K)ˣ).ker) =
        (n : ℕ) := by
    rw [
      LocalFieldTheory.powMonoidHom_ker_units_eq_rootsOfUnity]
    obtain ⟨ζ, hζ⟩ := hmu
    have hζprim : IsPrimitiveRoot ζ (n : ℕ) :=
      (mem_primitiveRoots n.pos).mp hζ
    exact
      (hζprim.map_of_injective
        (algebraMap K (v₀.adicCompletion K)).injective).card_rootsOfUnity
  simpa only [hroots] using hindex

def finitePlaceNthPowerDefect
    (n : ℕ+)
    (v₀ : HeightOneSpectrum (𝓞 K)) : ℕ

theorem finitePlaceNthPowerDefect_eq_absNorm_maxPowDividing
    (n : ℕ+)
    (v : HeightOneSpectrum (𝓞 K)) :
    finitePlaceNthPowerDefect (K := K) n v =
      Ideal.absNorm
        (v.maxPowDividing
          (Ideal.span {((n : ℕ) : 𝓞 K)}))

theorem card_finitePlace_nthPowerQuotient_eq_defect
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v₀ : HeightOneSpectrum (𝓞 K)) :
    Nat.card
        ((v₀.adicCompletion K)ˣ ⧸
          (powMonoidHom (n : ℕ) :
            (v₀.adicCompletion K)ˣ →*
              (v₀.adicCompletion K)ˣ).range) =
      (n : ℕ) *
        ((n : ℕ) *
          finitePlaceNthPowerDefect (K := K) n v₀)