ExistsUnique_pDigits_of_transcendental.lean

def frobeniusSubfield (M : Type*) [Field M] (p : ℕ) [ExpChar M p] : Subfield M

theorem mem_frobeniusSubfield_iff {M : Type*} [Field M] (p : ℕ) [ExpChar M p] {a : M} :
    a ∈ frobeniusSubfield M p ↔ ∃ b : M, b ^ p = a

theorem pow_mem_frobeniusSubfield {M : Type*} [Field M] (p : ℕ) [ExpChar M p] (a : M) :
    a ^ p ∈ frobeniusSubfield M p

def frobeniusRingEquivRange (M : Type*) [Field M] (p : ℕ) [ExpChar M p] :
    M ≃+* frobeniusSubfield M p

theorem frobeniusRingEquivRange_apply (M : Type*) [Field M] (p : ℕ) [ExpChar M p]
    (a : M) : ((frobeniusRingEquivRange M p a : frobeniusSubfield M p) : M) = a ^ p

abbrev frobeniusSubfieldImageInM : Subfield M

theorem frobeniusSubfieldImageInM_le_algebraMapRange :
    frobeniusSubfieldImageInM (E := E) (M := M) p ≤ (algebraMap E M).fieldRange

theorem frobeniusSubfieldImageInM_le_frobeniusSubfield :
    frobeniusSubfieldImageInM (E := E) (M := M) p ≤ frobeniusSubfield M p

theorem comap_frobenius_frobeniusSubfield :
    (frobeniusSubfield M p).comap (frobenius M p) = ⊤

theorem comap_frobenius_frobeniusSubfieldImageInM :
    (frobeniusSubfieldImageInM (E := E) (M := M) p).comap (frobenius M p) =
      (algebraMap E M).fieldRange

theorem finrank_algebraMapRange_eq :
    Module.finrank (↥(algebraMap E M).fieldRange) M = Module.finrank E M

theorem finrank_frobeniusSubfield_eq [FiniteDimensional E M]
    [FiniteDimensional (frobeniusSubfield E p) E] :
    Module.finrank (frobeniusSubfield M p) M = Module.finrank (frobeniusSubfield E p) E

theorem pDigits_linearIndependent {t : M} (htp : ∀ a : M, a ^ p ≠ t) :
    haveI : ExpChar M p := ExpChar.prime hp.out
    LinearIndependent (frobeniusSubfield M p)
      (fun i : Fin p ↦ (t ^ (i : ℕ) : M)) := by
  have : ExpChar M p := ExpChar.prime hp.out
  have htp' : ∀ c : frobeniusSubfield M p, c ^ p ≠
      (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ : frobeniusSubfield M p) := by
    rintro ⟨_, b, rfl⟩ hcp
    refine htp b ((frobenius M p).injective ?_)
    have hcp' := congrArg (fun z : frobeniusSubfield M p ↦ (z : M)) hcp
    push_cast at hcp'
    simpa only [frobenius_def] using hcp'
  have hirr : Irreducible (X ^ p - C (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ :
      frobeniusSubfield M p)) :=
    X_pow_sub_C_irreducible_of_prime hp.out htp'
  have hroot : (aeval (R := ↥(frobeniusSubfield M p)) t)
      (X ^ p - C (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ : frobeniusSubfield M p)) = 0 := by
    simp only [map_sub, map_pow, aeval_X, aeval_C]
    exact sub_self _
  have hmon : (X ^ p - C (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ :
      frobeniusSubfield M p)).Monic := monic_X_pow_sub_C _ hp.out.ne_zero
  have hmp : X ^ p - C (⟨t ^ p, pow_mem_frobeniusSubfield p t⟩ : frobeniusSubfield M p) =
      minpoly (↥(frobeniusSubfield M p)) t :=
    minpoly.eq_of_irreducible_of_monic hirr hroot hmon
  have hdeg : (minpoly (↥(frobeniusSubfield M p)) t).natDegree = p := by
    rw [← hmp, natDegree_X_pow_sub_C]
  have hli := linearIndependent_pow (K := ↥(frobeniusSubfield M p)) t
  rw [hdeg] at hli
  exact hli

abbrev genT (t : M) : ↥K⟮t⟯

theorem genT_not_pow (t : M) (htr : Transcendental K t) (a : ↥K⟮t⟯) :
    a ^ p ≠ genT t

theorem adjoin_genT_over_frobeniusSubfield [PerfectField K] (t : M) :
    haveI : ExpChar (↥K⟮t⟯) p :=
      expChar_of_injective_algebraMap (algebraMap K _).injective p
    (IntermediateField.adjoin (↥(frobeniusSubfield (↥K⟮t⟯) p)) {genT t} :
        IntermediateField _ (↥K⟮t⟯)) = ⊤ := by
  have : ExpChar (↥K⟮t⟯) p :=
    expChar_of_injective_algebraMap (algebraMap K _).injective p
  rw [eq_top_iff]
  intro x _
  obtain ⟨r, s, hrs⟩ := (IntermediateField.mem_adjoin_simple_iff K _).mp x.2
  have hrs' : x = aeval (genT t) r / aeval (genT t) s := by
    apply Subtype.ext
    rw [hrs]
    push_cast
    exact congrArg₂ _
      (IntermediateField.AdjoinSimple.coe_aeval_gen_apply (F := K) (α := t) r).symm
      (IntermediateField.AdjoinSimple.coe_aeval_gen_apply (F := K) (α := t) s).symm
  rw [hrs']
  have hK : ∀ c : K, (algebraMap K (↥K⟮t⟯)) c ∈ (frobeniusSubfield (↥K⟮t⟯) p : Subfield _) := by
    intro c
    obtain ⟨c', hc'⟩ := (frobeniusEquiv K p).surjective c
    exact ⟨algebraMap K _ c', by
      rw [← hc']; simp only [frobenius_def, map_pow, frobeniusEquiv_apply, frobenius_def]⟩
  have haeval : ∀ q : K[X], aeval (genT t) q ∈
      (IntermediateField.adjoin (↥(frobeniusSubfield (↥K⟮t⟯) p)) {genT t} :
        IntermediateField _ (↥K⟮t⟯)) := by
    intro q
    induction q using Polynomial.induction_on with
    | C c =>
      simp only [aeval_C]
      exact IntermediateField.algebraMap_mem _ (⟨_, hK c⟩ : ↥(frobeniusSubfield (↥K⟮t⟯) p))
    | add f g hf hg => simpa only [map_add] using add_mem hf hg
    | monomial n c _ =>
      simp only [map_mul, aeval_C, map_pow, aeval_X]
      exact mul_mem (IntermediateField.algebraMap_mem _
          (⟨_, hK c⟩ : ↥(frobeniusSubfield (↥K⟮t⟯) p)))
        (pow_mem (IntermediateField.mem_adjoin_simple_self _ _) _)
  exact div_mem (haeval r) (haeval s)

theorem finrank_frobeniusSubfield_adjoin_transcendental [PerfectField K]
    {t : M} (htr : Transcendental K t) :
    haveI : ExpChar (↥(IntermediateField.adjoin K ({t} : Set M))) p :=
      expChar_of_injective_algebraMap (algebraMap K _).injective p
    Module.finrank
      (frobeniusSubfield (↥(IntermediateField.adjoin K ({t} : Set M))) p)
      (↥(IntermediateField.adjoin K ({t} : Set M))) = p := by
  have : ExpChar (↥K⟮t⟯) p :=
    expChar_of_injective_algebraMap (algebraMap K _).injective p
  have : CharP (↥K⟮t⟯) p :=
    charP_of_injective_algebraMap (algebraMap K _).injective p
  let t' : ↥K⟮t⟯ := genT t
  let tp : ↥(frobeniusSubfield (↥K⟮t⟯) p) := ⟨t' ^ p, pow_mem_frobeniusSubfield p t'⟩
  have hint : IsIntegral (↥(frobeniusSubfield (↥K⟮t⟯) p)) t' := by
    refine ⟨X ^ p - C tp, monic_X_pow_sub_C _ hp.out.ne_zero, ?_⟩
    simp only [eval₂_sub, eval₂_X_pow, eval₂_C]
    exact sub_eq_zero.mpr rfl
  have hfd : FiniteDimensional (↥(frobeniusSubfield (↥K⟮t⟯) p)) (↥K⟮t⟯) := by
    have h1 := adjoin_genT_over_frobeniusSubfield (K := K) (M := M) p t
    have h2 := IntermediateField.adjoin.finiteDimensional hint
    rw [show t' = genT t from rfl, h1] at h2
    exact (IntermediateField.topEquiv (F := ↥(frobeniusSubfield (↥K⟮t⟯) p))
      (E := ↥K⟮t⟯)).toLinearEquiv.finiteDimensional
  have hli := pDigits_linearIndependent (M := ↥K⟮t⟯) p (t := t') (genT_not_pow p t htr)
  refine le_antisymm ?_
    (by simpa only [Fintype.card_fin] using hli.fintype_card_le_finrank)
  have htop := adjoin_genT_over_frobeniusSubfield (K := K) (M := M) p t
  calc Module.finrank _ (↥K⟮t⟯)
      = Module.finrank (↥(frobeniusSubfield (↥K⟮t⟯) p))
          (↥(IntermediateField.adjoin (↥(frobeniusSubfield (↥K⟮t⟯) p)) {t'} :
            IntermediateField _ (↥K⟮t⟯))) := by
        rw [show t' = genT t from rfl, htop, IntermediateField.finrank_top']
    _ = (minpoly (↥(frobeniusSubfield (↥K⟮t⟯) p)) t').natDegree :=
        IntermediateField.adjoin.finrank hint
    _ ≤ (X ^ p - C tp).natDegree :=
        Polynomial.natDegree_le_of_dvd (minpoly.dvd _ _ (by
          simp only [map_sub, map_pow, aeval_X, aeval_C]; exact sub_eq_zero.mpr rfl))
          (monic_X_pow_sub_C _ hp.out.ne_zero).ne_zero
    _ = p := natDegree_X_pow_sub_C

theorem finrank_frobeniusSubfield_eq_of_transcendental {K M : Type*} [Field K] [Field M]
    [Algebra K M] [PerfectField K] (p : ℕ) [hp : Fact p.Prime] [CharP K p]
    (t : M) (htr : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set M)) M] :
    haveI : ExpChar M p := expChar_of_injective_algebraMap (algebraMap K M).injective p
    Module.finrank (frobeniusSubfield M p) M = p := by
  have : ExpChar M p := expChar_of_injective_algebraMap (algebraMap K M).injective p
  have : ExpChar (↥(IntermediateField.adjoin K ({t} : Set M))) p :=
    expChar_of_injective_algebraMap (algebraMap K _).injective p
  have : FiniteDimensional
      (frobeniusSubfield (↥(IntermediateField.adjoin K ({t} : Set M))) p)
      (↥(IntermediateField.adjoin K ({t} : Set M))) :=
    FiniteDimensional.of_finrank_pos (by
      rw [finrank_frobeniusSubfield_adjoin_transcendental p htr]; exact hp.out.pos)
  rw [finrank_frobeniusSubfield_eq (E := ↥(IntermediateField.adjoin K ({t} : Set M))) p,
    finrank_frobeniusSubfield_adjoin_transcendental p htr]

theorem pDigits_exists_of_finrank_eq
    (hfr : haveI : ExpChar M p := ExpChar.prime hp.out
      Module.finrank (frobeniusSubfield M p) M = p)
    {t : M} (htp : ∀ a : M, a ^ p ≠ t) (g : M) :
    ∃ a : Fin p → M, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ) := by
  have : ExpChar M p := ExpChar.prime hp.out
  have hlin := pDigits_linearIndependent p htp
  let b : Module.Basis (Fin p) (frobeniusSubfield M p) M :=
    basisOfLinearIndependentOfCardEqFinrank hlin (by rw [hfr, Fintype.card_fin])
  have hbapply : ∀ i : Fin p, (b i : M) = t ^ (i : ℕ) := fun i ↦
    congrFun (coe_basisOfLinearIndependentOfCardEqFinrank hlin
      (by rw [hfr, Fintype.card_fin])) i
  refine ⟨fun i ↦ (frobeniusRingEquivRange M p).symm (b.repr g i), ?_⟩
  conv_lhs => rw [← b.sum_repr g]
  refine Finset.sum_congr rfl fun i _ ↦ ?_
  rw [hbapply i, ← frobeniusRingEquivRange_apply M p, RingEquiv.apply_symm_apply]
  rfl

theorem pDigits_existsUnique_of_transcendental {K M : Type*} [Field K] [Field M]
    [Algebra K M] [PerfectField K] (p : ℕ) [hp : Fact p.Prime] [CharP K p]
    (t : M) (htr : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set M)) M]
    (htp : ∀ a : M, a ^ p ≠ t) (g : M) :
    ∃! a : Fin p → M, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ)

theorem _root_.AlgebraicCurve.existsUnique_pDigits_of_transcendental {K M : Type*} [Field K] [Field
  M] [Algebra K M]
    [PerfectField K] (p : ℕ) [hp : Fact p.Prime] [CharP K p] (t : M) (htr : Transcendental K t)
    [FiniteDimensional (IntermediateField.adjoin K ({t} : Set M)) M] (htp : ∀ a : M, a ^ p ≠ t)
    (g : M) :
    ∃! a : Fin p → M, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ)