IdealPowerRadicalRank.lean

theorem card_pClassGroup_eq_pow_pClassRank :
    Nat.card (PClassGroup F p) = p ^ pClassRank F p

theorem finrank_idealPowerRadicalModP :
    Module.finrank (ZMod p) (idealPowerRadicalModP F p) =
      pClassRank F p +
        (NumberField.InfinitePlace.nrRealPlaces F +
          NumberField.InfinitePlace.nrComplexPlaces F - 1 +
            (if (primitiveRoots p F).Nonempty then 1 else 0)) := by
  apply Nat.pow_right_injective (Fact.out : p.Prime).two_le
  calc
    p ^ Module.finrank (ZMod p) (idealPowerRadicalModP F p) =
        p ^ (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1 +
              (if (primitiveRoots p F).Nonempty then 1 else 0)) *
          Nat.card (PClassGroup F p) :=
      pow_finrank_idealPowerRadicalModP F p
    _ = p ^ (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1 +
              (if (primitiveRoots p F).Nonempty then 1 else 0)) *
          p ^ pClassRank F p := by
      rw [card_pClassGroup_eq_pow_pClassRank F p]
    _ = p ^ (pClassRank F p +
          (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1 +
              (if (primitiveRoots p F).Nonempty then 1 else 0))) := by
      rw [← pow_add, Nat.add_comm]

theorem finrank_idealPowerRadicalModP_eq_pClassRank_add_infinitePlaces :
    (open Classical in
      Module.finrank (ZMod p) (idealPowerRadicalModP F p) =
        pClassRank F p +
          (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) := by
  classical
  have hroots :
      (primitiveRoots p F).Nonempty ↔ ∃ ζ : F, IsPrimitiveRoot ζ p := by
    constructor
    · rintro ⟨ζ, hζ⟩
      exact ⟨ζ, (mem_primitiveRoots (Fact.out : p.Prime).pos).mp hζ⟩
    · rintro ⟨ζ, hζ⟩
      exact ⟨ζ, (mem_primitiveRoots (Fact.out : p.Prime).pos).mpr hζ⟩
  rw [finrank_idealPowerRadicalModP F p]
  simp only [hroots]
  rw [Nat.add_assoc]

theorem finrank_idealPowerRadicalModPDual :
    (open Classical in
      Module.finrank (ZMod p)
          (Module.Dual (ZMod p) (idealPowerRadicalModP F p)) =
        pClassRank F p +
          (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) := by
  classical
  let _ : FiniteDimensional (ZMod p) (idealPowerRadicalModP F p) :=
    idealPowerRadicalModP_finiteDimensional F p
  rw [Subspace.dual_finrank_eq,
    finrank_idealPowerRadicalModP_eq_pClassRank_add_infinitePlaces F p]