OrdinaryUnitModP.lean

def emptySUnitEquivNumberFieldUnits :
    SUnitGroup (K := K) (∅ : Finset (HeightOneSpectrum (𝓞 K))) ≃*
      (𝓞 K)ˣ

abbrev OrdinaryUnitNthPowerQuotient (n : ℕ)

theorem ordinaryUnitNthPowerQuotient_pow_eq_one
    (p : ℕ) (x : OrdinaryUnitNthPowerQuotient K p) :
    x ^ p = 1

def ordinaryUnitModPModule (p : ℕ) :
    Module (ZMod p) (Additive (OrdinaryUnitNthPowerQuotient K p))

def emptySUnitNthPowerQuotientEquiv
    (n : ℕ) :
    SUnitGroup (K := K) (∅ : Finset (HeightOneSpectrum (𝓞 K))) ⧸
        (powMonoidHom n :
          SUnitGroup (K := K) (∅ : Finset (HeightOneSpectrum (𝓞 K))) →*
            SUnitGroup (K := K) (∅ : Finset (HeightOneSpectrum (𝓞 K)))).range ≃*
      OrdinaryUnitNthPowerQuotient K n

theorem finite_ordinaryUnitNthPowerQuotient (n : ℕ+) :
    Finite (OrdinaryUnitNthPowerQuotient K (n : ℕ))

theorem card_numberFieldTorsion_pthPowerQuotient_of_no_primitiveRoot
    (p : ℕ) (hp : p.Prime)
    (hμ : ¬ ∃ ζ : K, IsPrimitiveRoot ζ p) :
    Nat.card
        (NumberField.Units.torsion K ⧸
          (powMonoidHom p : NumberField.Units.torsion K →*
            NumberField.Units.torsion K).range) = 1

theorem card_ordinaryUnitNthPowerQuotient_of_no_primitiveRoot
    (p : ℕ) (hp : p.Prime)
    (hμ : ¬ ∃ ζ : K, IsPrimitiveRoot ζ p) :
    Nat.card (OrdinaryUnitNthPowerQuotient K p) =
      p ^ (NumberField.InfinitePlace.nrRealPlaces K +
        NumberField.InfinitePlace.nrComplexPlaces K - 1)

theorem card_ordinaryUnitNthPowerQuotient_of_primitiveRoot
    (p : ℕ) (hp : p.Prime)
    (hμ : ∃ ζ : K, IsPrimitiveRoot ζ p) :
    Nat.card (OrdinaryUnitNthPowerQuotient K p) =
      p ^ (NumberField.InfinitePlace.nrRealPlaces K +
        NumberField.InfinitePlace.nrComplexPlaces K)

theorem card_ordinaryUnitNthPowerQuotient
    (p : ℕ) (hp : p.Prime) :
    Nat.card (OrdinaryUnitNthPowerQuotient K p) =
      p ^ (NumberField.InfinitePlace.nrRealPlaces K +
        NumberField.InfinitePlace.nrComplexPlaces K - 1 +
          (if (primitiveRoots p K).Nonempty then 1 else 0)) := by
  by_cases hroots : (primitiveRoots p K).Nonempty
  · have hμ : ∃ ζ : K, IsPrimitiveRoot ζ p := by
      obtain ⟨ζ, hζ⟩ := hroots
      exact ⟨ζ, (mem_primitiveRoots hp.pos).mp hζ⟩
    rw [card_ordinaryUnitNthPowerQuotient_of_primitiveRoot K p hp hμ]
    simp only [ite_eq_left hroots]
    congr 1
    have hplaces :
        0 < NumberField.InfinitePlace.nrRealPlaces K +
          NumberField.InfinitePlace.nrComplexPlaces K := by
      rw [← NumberField.InfinitePlace.card_eq_nrRealPlaces_add_nrComplexPlaces]
      exact Fintype.card_pos
    omega
  · have hμ : ¬ ∃ ζ : K, IsPrimitiveRoot ζ p := by
      rintro ⟨ζ, hζ⟩
      exact hroots ⟨ζ, (mem_primitiveRoots hp.pos).mpr hζ⟩
    rw [card_ordinaryUnitNthPowerQuotient_of_no_primitiveRoot K p hp hμ]
    simp [hroots]

def ordinaryUnitModPFinrank (p : ℕ) : ℕ

theorem finrank_ordinaryUnitModP
    (p : ℕ) (hp : p.Prime) :
    ordinaryUnitModPFinrank K p =
      NumberField.InfinitePlace.nrRealPlaces K +
        NumberField.InfinitePlace.nrComplexPlaces K - 1 +
          (if (primitiveRoots p K).Nonempty then 1 else 0) := by
  unfold ordinaryUnitModPFinrank
  let _ : Fact p.Prime := ⟨hp⟩
  let _ : Module (ZMod p)
      (Additive (OrdinaryUnitNthPowerQuotient K p)) :=
    ordinaryUnitModPModule K p
  let _ : Finite (Additive (OrdinaryUnitNthPowerQuotient K p)) :=
    finite_ordinaryUnitNthPowerQuotient K (p.toPNat hp.pos)
  let _ : Module.Finite (ZMod p)
      (Additive (OrdinaryUnitNthPowerQuotient K p)) :=
    Module.Finite.of_finite
  apply Nat.pow_right_injective hp.two_le
  calc
    p ^ Module.finrank (ZMod p)
        (Additive (OrdinaryUnitNthPowerQuotient K p)) =
        Nat.card (Additive (OrdinaryUnitNthPowerQuotient K p)) := by
      rw [Module.natCard_eq_pow_finrank
        (K := ZMod p)
        (V := Additive (OrdinaryUnitNthPowerQuotient K p)), Nat.card_zmod]
    _ = Nat.card (OrdinaryUnitNthPowerQuotient K p) := rfl
    _ = p ^ (NumberField.InfinitePlace.nrRealPlaces K +
          NumberField.InfinitePlace.nrComplexPlaces K - 1 +
            (if (primitiveRoots p K).Nonempty then 1 else 0)) :=
      card_ordinaryUnitNthPowerQuotient K p hp