IdealPowerRadicalH2Bound.lean

theorem finiteDimensional_and_finrank_le_idealPowerRadicalModPDual_of_injective
    {V : Type u} [AddCommGroup V] [Module (ZMod p) V]
    (f : V →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealPowerRadicalModP F p))
    (hf : Function.Injective f) :
    FiniteDimensional (ZMod p) V ∧
      (open Classical in
        Module.finrank (ZMod p) V ≤
          pClassRank F p +
            (NumberField.InfinitePlace.nrRealPlaces F +
              NumberField.InfinitePlace.nrComplexPlaces F - 1) +
            (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) := by
  classical
  let _ : AddCommGroup (ZMod p) :=
    (ZMod.instField p).toDivisionRing.toAddCommGroup
  let _ : Module (ZMod p) (ZMod p) := Semiring.toModule
  let : FiniteDimensional (ZMod p)
      (Module.Dual (ZMod p) (idealPowerRadicalModP F p)) :=
    idealPowerRadicalModPDual_finiteDimensional F p
  let : FiniteDimensional (ZMod p) V :=
    FiniteDimensional.of_injective f hf
  refine ⟨inferInstance, ?_⟩
  calc
    Module.finrank (ZMod p) V ≤
        Module.finrank (ZMod p)
          (Module.Dual (ZMod p) (idealPowerRadicalModP F p)) :=
      f.finrank_le_finrank_of_injective hf
    _ = pClassRank F p +
          (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0) :=
      finrank_idealPowerRadicalModPDual F p

theorem h2_finiteDimensional_and_rank_le_idealPowerRadicalModPDual_of_injective
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (f : continuousCohomologyZModPLifted p G 2 →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealPowerRadicalModP F p))
    (hf : Function.Injective f) :
    FiniteDimensional (ZMod p) (continuousCohomologyZModPLifted p G 2) ∧
      (open Classical in
        Module.finrank (ZMod p) (continuousCohomologyZModPLifted p G 2) ≤
          pClassRank F p +
            (NumberField.InfinitePlace.nrRealPlaces F +
              NumberField.InfinitePlace.nrComplexPlaces F - 1) +
            (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) :=
  finiteDimensional_and_finrank_le_idealPowerRadicalModPDual_of_injective
    F p f hf

theorem maxEverywhereUnramified_h2_numerical_bound_of_finrank_le_radicalDual
    (hpOdd : Odd p)
    (hfinite : FiniteDimensional (ZMod p)
      (continuousCohomologyZModPLifted p
        (MaxEverywhereUnramifiedProPGaloisGroup F p) 2))
    (hle : Module.finrank (ZMod p)
        (continuousCohomologyZModPLifted p
          (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
      Module.finrank (ZMod p)
        (Module.Dual (ZMod p) (idealPowerRadicalModP F p))) :
    FiniteDimensional (ZMod p)
        (continuousCohomologyZModPLifted p
          (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ∧
      (open Classical in
        Module.finrank (ZMod p)
            (continuousCohomologyZModPLifted p
              (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
          topologicalGeneratorRank
              (MaxEverywhereUnramifiedProPGaloisGroup F p) +
            (NumberField.InfinitePlace.nrRealPlaces F +
              NumberField.InfinitePlace.nrComplexPlaces F - 1) +
            (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) := by
  classical
  refine ⟨hfinite, ?_⟩
  calc
    Module.finrank (ZMod p)
        (continuousCohomologyZModPLifted p
          (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
        Module.finrank (ZMod p)
          (Module.Dual (ZMod p) (idealPowerRadicalModP F p)) := hle
    _ = pClassRank F p +
          (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0) :=
      finrank_idealPowerRadicalModPDual F p
    _ = topologicalGeneratorRank
            (MaxEverywhereUnramifiedProPGaloisGroup F p) +
          (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0) := by
      rw [generatorRank_maxUnramified_eq_pClassRank F p hpOdd]

theorem maxEverywhereUnramified_h2_numerical_bound_of_injective
    (hpOdd : Odd p)
    (f : continuousCohomologyZModPLifted p
        (MaxEverywhereUnramifiedProPGaloisGroup F p) 2 →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealPowerRadicalModP F p))
    (hf : Function.Injective f) :
    FiniteDimensional (ZMod p)
        (continuousCohomologyZModPLifted p
          (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ∧
      (open Classical in
        Module.finrank (ZMod p)
            (continuousCohomologyZModPLifted p
              (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
          topologicalGeneratorRank
              (MaxEverywhereUnramifiedProPGaloisGroup F p) +
            (NumberField.InfinitePlace.nrRealPlaces F +
              NumberField.InfinitePlace.nrComplexPlaces F - 1) +
            (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) := by
  classical
  obtain ⟨hfinite, hle⟩ :=
    h2_finiteDimensional_and_rank_le_idealPowerRadicalModPDual_of_injective
      F p f hf
  apply maxEverywhereUnramified_h2_numerical_bound_of_finrank_le_radicalDual
    F p hpOdd hfinite
  rw [finrank_idealPowerRadicalModPDual F p]
  exact hle