KummerCorrespondenceFormula.lean

theorem kummerRadicalExtension_internalRoots_adjoin_eq_top
    (n : ℕ+) (Delta : KummerSubgroup K n) :
    IntermediateField.adjoin K
      (kummerRootSet
        (K := K)
        (Omega := kummerRadicalExtension
          (K := K) (Omega := Omega) n Delta.1)
        n Delta.1) = ⊤

def restrictedKummerTransposeMulEquivOfAdjoin
    {L : Type*} [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤
      finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (hgenerate : IntermediateField.adjoin K
      (kummerRootSet (K := K) (Omega := L) n Delta.1) = ⊤) :
    Gal(L/K) ≃*
      (RestrictedRadicalQuotient n Delta →*
        nthRootsSubgroup L (n : ℕ))

theorem exists_pairing_element_matching_finset
    {G R L : Type*} [Field L] [Algebra K L]
    [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [CommGroup R]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hRexponent : ∀ r : R, r ^ (n : ℕ) = 1)
    (f : R →* (G →* DiscreteNthRootsSubgroup L (n : ℕ)))
    (t : G →* (R →* DiscreteNthRootsSubgroup L (n : ℕ)))
    (hpair : ∀ g r, t g r = f r g)
    (hf : Function.Injective f)
    (hcontinuous : ∀ r,
      Continuous (fun g : G => f r g))
    (S : Finset R)
    (chi : R →* DiscreteNthRootsSubgroup L (n : ℕ)) :
    ∃ g : G, ∀ r ∈ S, t g r = chi r := by
  let H : Subgroup G := ⨅ r : S, MonoidHom.ker (f r.1)
  have hHopen : IsOpen (H : Set G) := by
    dsimp only [H]
    rw [Subgroup.coe_iInf]
    change IsOpen (⋂ r : S, (MonoidHom.ker (f r.1) : Set G))
    apply isOpen_iInter_of_finite
    intro r
    rw [MonoidHom.coe_ker]
    exact (isOpen_discrete ({1} :
      Set (DiscreteNthRootsSubgroup L (n : ℕ)))).preimage
        (hcontinuous r.1)
  let : H.Normal := H.normal_of_isMulCommutative
  let Q := G ⧸ H
  let : Finite Q := H.quotient_finite_of_isOpen hHopen
  let R0 := Subgroup.closure (S : Set R)
  have hR0exponent : ∀ r : R0, r ^ (n : ℕ) = 1 := by
    intro r
    apply Subtype.ext
    exact hRexponent r.1
  let : Finite R0 := CommGroup.finite_of_fg_isMulTorsion (G := R0) (fun r =>
    isOfFinOrder_iff_pow_eq_one.mpr ⟨(n : ℕ), n.pos, hR0exponent r⟩)
  have hHker (r : R0) : H ≤ MonoidHom.ker (f r.1) := by
    intro g hg
    have hclosure : R0 ≤ MonoidHom.ker (t g) := by
      rw [Subgroup.closure_le]
      intro x hx
      change t g x = 1
      rw [hpair]
      exact (show g ∈ MonoidHom.ker (f x) from
        (iInf_le (fun r : S => MonoidHom.ker (f r.1)) ⟨x, hx⟩) hg)
    rw [MonoidHom.mem_ker, ← hpair]
    exact hclosure r.property
  let f0 : R0 →* (Q →* DiscreteNthRootsSubgroup L (n : ℕ)) :=
    { toFun := fun r => QuotientGroup.lift H (f r.1) (hHker r)
      map_one' := by
        apply MonoidHom.ext
        intro q
        obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective H q
        simp
      map_mul' := by
        intro r s
        apply MonoidHom.ext
        intro q
        obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective H q
        simp }
  have hf0 : Function.Injective f0 := by
    intro r s hrs
    apply Subtype.ext
    apply hf
    apply MonoidHom.ext
    intro g
    have hvalue := DFunLike.congr_fun hrs (QuotientGroup.mk' H g)
    exact hvalue
  let t0 : Q →* (R0 →* DiscreteNthRootsSubgroup L (n : ℕ)) :=
    { toFun := fun q =>
        { toFun := fun r => f0 r q
          map_one' := by simp
          map_mul' := by intro r s; exact DFunLike.congr_fun (map_mul f0 r s) q }
      map_one' := by
        apply MonoidHom.ext
        intro r
        exact map_one (f0 r)
      map_mul' := by
        intro q p
        apply MonoidHom.ext
        intro r
        exact map_mul (f0 r) q p }
  have ht0 : Function.Injective t0 := by
    intro q p hqp
    obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective H q
    obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective H p
    apply (QuotientGroup.eq_iff_div_mem).2
    dsimp only [H]
    rw [Subgroup.mem_iInf]
    intro r
    rw [MonoidHom.mem_ker, map_div]
    have hvalue := DFunLike.congr_fun hqp
      (⟨r.1, Subgroup.subset_closure r.2⟩ : R0)
    change f r.1 g = f r.1 h at hvalue
    rw [hvalue]
    exact div_self' _
  have hQexponent : ∀ q : Q, q ^ (n : ℕ) = 1 := by
    intro q
    apply ht0
    rw [map_pow, map_one]
    apply MonoidHom.ext
    intro r
    apply Subtype.ext
    exact (t0 q r).2
  obtain ⟨dualQ⟩ := finiteNthRootsCharacterDuality
    (G := Q) (K := K) (L := L) n hmu hQexponent
  obtain ⟨dualR0⟩ := finiteNthRootsCharacterDuality
    (G := R0) (K := K) (L := L) n hmu hR0exponent
  let : NeZero (n : ℕ) := ⟨n.ne_zero⟩
  let : Finite (DiscreteNthRootsSubgroup L (n : ℕ)) :=
    inferInstanceAs (Finite (nthRootsSubgroup L (n : ℕ)))
  let : Fintype Q := Fintype.ofFinite Q
  let : Fintype R0 := Fintype.ofFinite R0
  let : Finite (R0 →* DiscreteNthRootsSubgroup L (n : ℕ)) :=
    Finite.of_injective
      (fun psi : R0 →* DiscreteNthRootsSubgroup L (n : ℕ) =>
        (psi : R0 → DiscreteNthRootsSubgroup L (n : ℕ)))
      DFunLike.coe_injective
  let : Fintype (R0 →* DiscreteNthRootsSubgroup L (n : ℕ)) :=
    Fintype.ofFinite _
  have hcardR0Q : Fintype.card R0 ≤ Fintype.card Q :=
    Fintype.card_le_of_injective
      (fun r : R0 => dualQ (f0 r)) (dualQ.injective.comp hf0)
  have hcardQR0 : Fintype.card Q ≤ Fintype.card R0 :=
    Fintype.card_le_of_injective
      (fun q : Q => dualR0 (t0 q)) (dualR0.injective.comp ht0)
  have hcardQTarget :
      Fintype.card Q =
        Fintype.card (R0 →* DiscreteNthRootsSubgroup L (n : ℕ)) := by
    calc
      Fintype.card Q = Fintype.card R0 := Nat.le_antisymm hcardQR0 hcardR0Q
      _ = Fintype.card (R0 →* DiscreteNthRootsSubgroup L (n : ℕ)) :=
        Fintype.card_congr dualR0.symm.toEquiv
  have ht0surjective : Function.Surjective t0 :=
    ht0.surjective_of_finite (Fintype.equivOfCardEq hcardQTarget)
  obtain ⟨q, hq⟩ := ht0surjective (chi.comp R0.subtype)
  obtain ⟨g, rfl⟩ := QuotientGroup.mk'_surjective H q
  refine ⟨g, ?_⟩
  intro r hr
  have hvalue := DFunLike.congr_fun hq
    (⟨r, Subgroup.subset_closure hr⟩ : R0)
  change f r g = chi r at hvalue
  rw [hpair]
  exact hvalue

def kummerRadicalExtensionRestrictedTranspose
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n) :
    Gal(kummerRadicalExtension
        (K := K) (Omega := Omega) n Delta.1/K) →*
      (RestrictedRadicalQuotient n Delta →*
        nthRootsSubgroup
          (kummerRadicalExtension
            (K := K) (Omega := Omega) n Delta.1) (n : ℕ))

theorem kummerRadicalExtensionRestrictedTranspose_injective
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n) :
    Function.Injective
      (kummerRadicalExtensionRestrictedTranspose
        (K := K) (Omega := Omega) n hn hmu Delta)

theorem restrictedKummerTranspose_evaluation_continuous
    {L : Type*} [Field L] [Algebra K L] [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤
      finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (q : RestrictedRadicalQuotient n Delta) :
    @Continuous (Gal(L/K)) (DiscreteNthRootsSubgroup L (n : ℕ))
      inferInstance
      (DiscreteNthRootsSubgroup.instTopologicalSpaceSubtypeUnitsMemSubgroup
        L (n : ℕ))
      (fun sigma => restrictedKummerTranspose n hmu Delta hDelta sigma q) := by
  let D := chosenFiniteKummerRadicalDatum (K := K) (L := L) n
  let hbase : NthRootsOfUnityInBase (K := K) (L := L) n :=
    nthRootsOfUnityInBase_of_primitiveRoots (K := K) (L := L) n hmu
  obtain ⟨a, rfl⟩ :=
    restrictedRadicalQuotientMk_surjective n Delta q
  let aD : D.carrier := restrictedRadicalInclusion n Delta hDelta a
  have hcontinuous := infiniteKummerRootCharacter_continuous n hbase aD
  exact hcontinuous.congr (fun _ => rfl)

def restrictedKummerEvaluationLocus
    {L : Type*} [Field L] [Algebra K L] [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤
      finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (chi : RestrictedRadicalQuotient n Delta →*
      nthRootsSubgroup L (n : ℕ))
    (q : RestrictedRadicalQuotient n Delta) : Set Gal(L/K)

theorem restrictedKummerEvaluationLocus_isClosed
    {L : Type*} [Field L] [Algebra K L] [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤
      finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (chi : RestrictedRadicalQuotient n Delta →*
      nthRootsSubgroup L (n : ℕ))
    (q : RestrictedRadicalQuotient n Delta) :
    IsClosed (restrictedKummerEvaluationLocus n hmu Delta hDelta chi q)

theorem restrictedKummerEvaluationLocus_isCompact
    {L : Type*} [Field L] [Algebra K L] [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤
      finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (chi : RestrictedRadicalQuotient n Delta →*
      nthRootsSubgroup L (n : ℕ))
    (q : RestrictedRadicalQuotient n Delta) :
    IsCompact (restrictedKummerEvaluationLocus n hmu Delta hDelta chi q)

theorem mem_iInter_restrictedKummerEvaluationLocus_iff
    {L : Type*} [Field L] [Algebra K L] [IsGalois K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (hDelta : Delta.1 ≤
      finiteKummerRadicalSubgroup (K := K) (L := L) n)
    (chi : RestrictedRadicalQuotient n Delta →*
      nthRootsSubgroup L (n : ℕ))
    (sigma : Gal(L/K)) :
    sigma ∈ ⋂ q, restrictedKummerEvaluationLocus
        n hmu Delta hDelta chi q ↔
      restrictedKummerTranspose n hmu Delta hDelta sigma = chi

theorem exists_kummerRadicalExtensionRestrictedTranspose_match_finset
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n)
    (S : Finset (RestrictedRadicalQuotient n Delta))
    (chi : RestrictedRadicalQuotient n Delta →*
      nthRootsSubgroup
        (kummerRadicalExtension
          (K := K) (Omega := Omega) n Delta.1) (n : ℕ)) :
    ∃ sigma : Gal(kummerRadicalExtension
        (K := K) (Omega := Omega) n Delta.1/K),
      ∀ q ∈ S,
        kummerRadicalExtensionRestrictedTranspose
          n hn hmu Delta sigma q = chi q

theorem kummerRadicalExtensionRestrictedTranspose_surjective
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n) :
    Function.Surjective
      (kummerRadicalExtensionRestrictedTranspose
        (K := K) (Omega := Omega) n hn hmu Delta)

def kummerRadicalExtensionRestrictedTransposeMulEquiv
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : KummerSubgroup K n) :
    Gal(kummerRadicalExtension
        (K := K) (Omega := Omega) n Delta.1/K) ≃*
      (RestrictedRadicalQuotient n Delta →*
        nthRootsSubgroup
          (kummerRadicalExtension
            (K := K) (Omega := Omega) n Delta.1) (n : ℕ))