Definitions/Def_ModularCurve_LevelBaseRing.lean

import Definitions.Def_ModularCurve_CharPReduction
import Definitions.Def_ModularCurve_LaurentDescent
import Mathlib.RingTheory.Polynomial.IsIntegral ↗

noncomputable section

open HahnSeries IntermediateField Polynomial

namespace ModularCurve

section LevelBaseRing

universe uE'

variable {E L : Type*} [Field E] [Field L] [Algebra ℚ E] [Algebra ℚ L]
variable (𝒪 : Subring E) (F₀ : IntermediateField ℚ (LaurentSeries ℚ)) (G : Set F₀)

def levelConst : 𝒪 →+* laurentBaseChange E F₀ :=
  (algebraMap E (laurentBaseChange E F₀)).comp 𝒪.subtype

@[simp]
theorem levelConst_apply (a : 𝒪) : levelConst 𝒪 F₀ a = algebraMap E (laurentBaseChange E F₀) (a : E) :=
  rfl

def levelGen (E : Type*) [Field E] [Algebra ℚ E] (g : G) : laurentBaseChange E F₀ :=
  ⟨coeffEmb E ((g : F₀) : LaurentSeries ℚ), coeffEmb_mem_laurentBaseChange E (g : F₀).2⟩

theorem coe_levelGen (g : G) : (levelGen F₀ G E g : LaurentSeries E) = coeffEmb E ((g : F₀) : LaurentSeries ℚ) :=
  rfl

def levelBaseRing : Subring (laurentBaseChange E F₀) :=
  Subring.closure (Set.range (levelConst 𝒪 F₀) ∪ Set.range (levelGen F₀ G E))

theorem levelConst_mem (a : 𝒪) : levelConst 𝒪 F₀ a ∈ levelBaseRing 𝒪 F₀ G :=
  Subring.subset_closure (Or.inl ⟨a, rfl⟩)

theorem levelGen_mem (g : G) : levelGen F₀ G E g ∈ levelBaseRing 𝒪 F₀ G :=
  Subring.subset_closure (Or.inr ⟨g, rfl⟩)

variable (ι : E →+* L) (𝒪' : Subring L)

theorem laurentDescent_levelConst (a : 𝒪'.comap ι) :
    laurentDescent ι F₀ (levelConst (𝒪'.comap ι) F₀ a) = levelConst 𝒪' F₀ ⟨ι a, a.2⟩ :=
  laurentDescent_algebraMap ι F₀ a

theorem laurentDescent_levelGen (g : G) : laurentDescent ι F₀ (levelGen F₀ G E g) = levelGen F₀ G L g :=
  laurentDescent_coeffEmb ι F₀ (g : F₀).2

theorem map_laurentDescent_levelBaseRing_le :
    (levelBaseRing (𝒪'.comap ι) F₀ G).map (laurentDescent ι F₀) ≤ levelBaseRing 𝒪' F₀ G := by
  rw [levelBaseRing, RingHom.map_closure, Subring.closure_le]
  rintro _ ⟨y, (⟨a, rfl⟩ | ⟨g, rfl⟩), rfl⟩
  · rw [laurentDescent_levelConst]
    exact levelConst_mem _ _ _ _
  · rw [laurentDescent_levelGen]
    exact levelGen_mem _ _ _ _

def levelBaseRingDescent : levelBaseRing (𝒪'.comap ι) F₀ G →+* levelBaseRing 𝒪' F₀ G :=
  ((laurentDescent ι F₀).comp (levelBaseRing (𝒪'.comap ι) F₀ G).subtype).codRestrict (levelBaseRing 𝒪' F₀ G)
    fun x => map_laurentDescent_levelBaseRing_le F₀ G ι 𝒪' ⟨x, x.2, rfl⟩

@[simp]
theorem coe_levelBaseRingDescent_apply (x : levelBaseRing (𝒪'.comap ι) F₀ G) :
    (levelBaseRingDescent F₀ G ι 𝒪' x : laurentBaseChange L F₀) = laurentDescent ι F₀ x :=
  rfl

theorem exists_finset_forall_exists_mem_levelBaseRing (y : laurentBaseChange L F₀) (hy : y ∈ levelBaseRing 𝒪' F₀ G) :
    ∃ s : Finset L, ∀ (E : Type uE') [Field E] [Algebra ℚ E] (ι : E →+* L), (↑s ⊆ Set.range ι) →
      ∃ x : laurentBaseChange E F₀, x ∈ levelBaseRing (𝒪'.comap ι) F₀ G ∧ laurentDescent ι F₀ x = y := by
  classical
  induction hy using Subring.closure_induction with
  | mem z hz =>
      rcases hz with ⟨a, rfl⟩ | ⟨g, rfl⟩
      · refine ⟨{(a : L)}, fun E _ _ ι hsub => ?_⟩
        obtain ⟨b, hb⟩ := hsub (Finset.mem_coe.mpr (Finset.mem_singleton_self (a : L)))
        have hb' : b ∈ 𝒪'.comap ι := by
          change ι b ∈ 𝒪'
          rw [hb]; exact a.2
        refine ⟨levelConst (𝒪'.comap ι) F₀ ⟨b, hb'⟩, levelConst_mem _ _ _ _, ?_⟩
        rw [laurentDescent_levelConst]
        exact congrArg (levelConst 𝒪' F₀) (Subtype.ext hb)
      · exact ⟨∅, fun E _ _ ι _ => ⟨levelGen F₀ G E g, levelGen_mem _ _ _ _, laurentDescent_levelGen F₀ G ι g⟩⟩
  | zero => exact ⟨∅, fun E _ _ ι _ => ⟨0, zero_mem _, map_zero _⟩⟩
  | one => exact ⟨∅, fun E _ _ ι _ => ⟨1, one_mem _, map_one _⟩⟩
  | add u v _ _ ihu ihv =>
      obtain ⟨s, hs⟩ := ihu
      obtain ⟨t, ht⟩ := ihv
      refine ⟨s ∪ t, fun E _ _ ι hsub => ?_⟩
      rw [Finset.coe_union] at hsub
      obtain ⟨a, ha, hau⟩ := hs E ι (Set.subset_union_left.trans hsub)
      obtain ⟨b, hb, hbv⟩ := ht E ι (Set.subset_union_right.trans hsub)
      exact ⟨a + b, add_mem ha hb, by rw [map_add, hau, hbv]⟩
  | neg u _ ihu =>
      obtain ⟨s, hs⟩ := ihu
      refine ⟨s, fun E _ _ ι hsub => ?_⟩
      obtain ⟨a, ha, hau⟩ := hs E ι hsub
      exact ⟨-a, neg_mem ha, by rw [map_neg, hau]⟩
  | mul u v _ _ ihu ihv =>
      obtain ⟨s, hs⟩ := ihu
      obtain ⟨t, ht⟩ := ihv
      refine ⟨s ∪ t, fun E _ _ ι hsub => ?_⟩
      rw [Finset.coe_union] at hsub
      obtain ⟨a, ha, hau⟩ := hs E ι (Set.subset_union_left.trans hsub)
      obtain ⟨b, hb, hbv⟩ := ht E ι (Set.subset_union_right.trans hsub)
      exact ⟨a * b, mul_mem ha hb, by rw [map_mul, hau, hbv]⟩

theorem exists_finset_forall_integral_laurentDescent (y : laurentBaseChange L F₀)
    (hy : ∃ p : Polynomial (levelBaseRing 𝒪' F₀ G), p.Monic ∧
      Polynomial.eval₂ (levelBaseRing 𝒪' F₀ G).subtype y p = 0) :
    ∃ s : Finset L, ∀ (E : Type uE') [Field E] [Algebra ℚ E] (ι : E →+* L), (↑s ⊆ Set.range ι) →
      ∃ x : laurentBaseChange E F₀, laurentDescent ι F₀ x = y ∧
        ∃ q : Polynomial (levelBaseRing (𝒪'.comap ι) F₀ G), q.Monic ∧
          Polynomial.eval₂ (levelBaseRing (𝒪'.comap ι) F₀ G).subtype x q = 0 := by
  classical
  obtain ⟨p, hp, hpy⟩ := hy

  obtain ⟨s₀, hs₀⟩ := exists_finset_forall_exists_laurentDescent_eq F₀ y
  choose sc hsc using fun n : ℕ => exists_finset_forall_exists_mem_levelBaseRing F₀ G 𝒪' (p.coeff n : laurentBaseChange L F₀)
    (p.coeff n).2
  refine ⟨s₀ ∪ p.support.biUnion sc, fun E _ _ ι hsub => ?_⟩
  rw [Finset.coe_union] at hsub
  obtain ⟨x, hx⟩ := hs₀ E ι (Set.subset_union_left.trans hsub)

  let φ := levelBaseRingDescent F₀ G ι 𝒪'
  have hlift : p ∈ Polynomial.lifts φ := by
    rw [Polynomial.lifts_iff_coeff_lifts]
    intro n
    by_cases hn : n ∈ p.support
    · have hsub' : ↑(sc n) ⊆ Set.range ι :=
        (Finset.coe_subset.mpr (Finset.subset_biUnion_of_mem sc hn)).trans (Set.subset_union_right.trans hsub)
      obtain ⟨c, hc, hcy⟩ := hsc n E ι hsub'
      exact ⟨⟨c, hc⟩, Subtype.ext hcy⟩
    · rw [Polynomial.notMem_support_iff.mp hn]
      exact ⟨0, map_zero _⟩
  obtain ⟨q, hqp, -, hq⟩ := Polynomial.lifts_and_degree_eq_and_monic hlift hp
  refine ⟨x, hx, q, hq, laurentDescent_injective ι F₀ ?_⟩
  rw [map_zero, Polynomial.hom_eval₂, ← hpy, ← hqp, Polynomial.eval₂_map, hx]
  rfl

theorem integral_laurentDescent_of_integral (x : laurentBaseChange E F₀)
    (hx : ∃ q : Polynomial (levelBaseRing (𝒪'.comap ι) F₀ G), q.Monic ∧
      Polynomial.eval₂ (levelBaseRing (𝒪'.comap ι) F₀ G).subtype x q = 0) :
    ∃ p : Polynomial (levelBaseRing 𝒪' F₀ G), p.Monic ∧
      Polynomial.eval₂ (levelBaseRing 𝒪' F₀ G).subtype (laurentDescent ι F₀ x) p = 0 := by
  obtain ⟨q, hq, hqx⟩ := hx
  refine ⟨q.map (levelBaseRingDescent F₀ G ι 𝒪'), hq.map _, ?_⟩
  have h : (levelBaseRing 𝒪' F₀ G).subtype.comp (levelBaseRingDescent F₀ G ι 𝒪') =
      (laurentDescent ι F₀).comp (levelBaseRing (𝒪'.comap ι) F₀ G).subtype := RingHom.ext fun _ => rfl
  rw [Polynomial.eval₂_map, h, ← Polynomial.hom_eval₂, hqx, map_zero]

theorem laurentDescent_mem_integralCoeffs_iff (x : laurentBaseChange E F₀) :
    (laurentDescent ι F₀ x : LaurentSeries L) ∈ CharPReduction.integralCoeffs 𝒪' ↔ (x : LaurentSeries E) ∈ CharPReduction.integralCoeffs (𝒪'.comap ι) :=
  Iff.rfl

end LevelBaseRing

section PolynomialStructure

variable {E L : Type*} [Field E] [Field L] [Algebra ℚ E] [Algebra ℚ L]
variable (𝒪 : Subring E) (F₀ : IntermediateField ℚ (LaurentSeries ℚ)) (g : F₀)

def levelGen₁ (E : Type*) [Field E] [Algebra ℚ E] : laurentBaseChange E F₀ :=
  levelGen F₀ ({g} : Set F₀) E ⟨g, rfl⟩

theorem coe_levelGen₁ : (levelGen₁ F₀ g E : LaurentSeries E) = coeffEmb E (g : LaurentSeries ℚ) :=
  rfl

theorem range_levelGen_singleton : Set.range (levelGen F₀ ({g} : Set F₀) E) = {levelGen₁ F₀ g E} := by
  ext y
  simp only [Set.mem_range, Set.mem_singleton_iff, levelGen₁]
  constructor
  · rintro ⟨⟨g', hg'⟩, rfl⟩
    rw [Set.mem_singleton_iff] at hg'
    subst hg'
    rfl
  · rintro rfl
    exact ⟨⟨g, rfl⟩, rfl⟩

theorem laurentDescent_levelGen₁ (ι : E →+* L) : laurentDescent ι F₀ (levelGen₁ F₀ g E) = levelGen₁ F₀ g L :=
  laurentDescent_levelGen F₀ {g} ι ⟨g, rfl⟩

theorem transcendental_of_laurentDescent (ι : E →+* L) (h : Transcendental L (levelGen₁ F₀ g L)) :
    Transcendental E (levelGen₁ F₀ g E) := by
  refine Transcendental.of_ringHom_of_comp_eq (f := ι) (g := laurentDescent ι F₀) ?_ ι.injective ?_
  · rwa [laurentDescent_levelGen₁]
  · exact RingHom.ext fun c => (laurentDescent_algebraMap ι F₀ c).symm

def levelEval : Polynomial 𝒪 →+* laurentBaseChange E F₀ :=
  Polynomial.eval₂RingHom (levelConst 𝒪 F₀) (levelGen₁ F₀ g E)

theorem levelEval_C (a : 𝒪) : levelEval 𝒪 F₀ g (Polynomial.C a) = levelConst 𝒪 F₀ a :=
  Polynomial.eval₂_C _ _

theorem levelEval_X : levelEval 𝒪 F₀ g Polynomial.X = levelGen₁ F₀ g E :=
  Polynomial.eval₂_X _ _

theorem levelBaseRing_singleton_eq_range : levelBaseRing 𝒪 F₀ {g} = (levelEval 𝒪 F₀ g).range := by
  apply le_antisymm
  · rw [levelBaseRing, range_levelGen_singleton, Subring.closure_le]
    rintro y (⟨a, rfl⟩ | rfl)
    · exact ⟨Polynomial.C a, levelEval_C 𝒪 F₀ g a⟩
    · exact ⟨Polynomial.X, levelEval_X 𝒪 F₀ g⟩
  · rintro _ ⟨p, rfl⟩
    induction p using Polynomial.induction_on with
    | C a => rw [levelEval_C]; exact levelConst_mem _ _ _ _
    | add p q hp hq => rw [map_add]; exact add_mem hp hq
    | monomial n a _ =>
        rw [pow_succ, ← mul_assoc, map_mul, levelEval_X]
        refine mul_mem ?_ ?_
        · rw [map_mul, map_pow, levelEval_C, levelEval_X]
          exact mul_mem (levelConst_mem _ _ _ _) (pow_mem (by exact levelGen_mem 𝒪 F₀ {g} ⟨g, rfl⟩) _)
        · exact levelGen_mem 𝒪 F₀ {g} ⟨g, rfl⟩

theorem levelEval_injective (hx : Transcendental E (levelGen₁ F₀ g E)) : Function.Injective (levelEval 𝒪 F₀ g) := by
  rw [injective_iff_map_eq_zero]
  intro p hp
  haveI : IsScalarTower 𝒪 E (laurentBaseChange E F₀) := IsScalarTower.of_algebraMap_eq fun _ => rfl
  have h1 : Polynomial.aeval (levelGen₁ F₀ g E) (p.map (algebraMap 𝒪 E)) = 0 := by
    rw [Polynomial.aeval_map_algebraMap]
    exact hp
  have h2 : p.map (algebraMap 𝒪 E) = 0 :=
    (injective_iff_map_eq_zero _).mp (transcendental_iff_injective.mp hx) _ h1
  exact Polynomial.map_injective (algebraMap 𝒪 E) Subtype.val_injective (by rw [h2, Polynomial.map_zero])

def levelPolynomialEquiv (hx : Transcendental E (levelGen₁ F₀ g E)) : Polynomial 𝒪 ≃+* levelBaseRing 𝒪 F₀ {g} :=
  (RingEquiv.ofBijective ((levelEval 𝒪 F₀ g).rangeRestrict)
    ⟨fun _ _ h => levelEval_injective 𝒪 F₀ g hx (Subtype.ext_iff.mp h), (levelEval 𝒪 F₀ g).rangeRestrict_surjective⟩).trans
    (RingEquiv.subringCongr (levelBaseRing_singleton_eq_range 𝒪 F₀ g).symm)

@[simp]
theorem coe_levelPolynomialEquiv_apply (hx : Transcendental E (levelGen₁ F₀ g E)) (p : Polynomial 𝒪) :
    (levelPolynomialEquiv 𝒪 F₀ g hx p : laurentBaseChange E F₀) = levelEval 𝒪 F₀ g p :=
  rfl

theorem levelPolynomialEquiv_C (hx : Transcendental E (levelGen₁ F₀ g E)) (a : 𝒪) :
    (levelPolynomialEquiv 𝒪 F₀ g hx (Polynomial.C a) : laurentBaseChange E F₀) = levelConst 𝒪 F₀ a :=
  levelEval_C 𝒪 F₀ g a

theorem levelPolynomialEquiv_X (hx : Transcendental E (levelGen₁ F₀ g E)) :
    (levelPolynomialEquiv 𝒪 F₀ g hx Polynomial.X : laurentBaseChange E F₀) = levelGen₁ F₀ g E :=
  levelEval_X 𝒪 F₀ g

theorem isIntegrallyClosed_levelBaseRing [IsDomain 𝒪] [IsIntegrallyClosed 𝒪]
    (hx : Transcendental E (levelGen₁ F₀ g E)) : IsIntegrallyClosed (levelBaseRing 𝒪 F₀ {g}) :=
  IsIntegrallyClosed.of_equiv (levelPolynomialEquiv 𝒪 F₀ g hx)

theorem isNoetherianRing_levelBaseRing [IsNoetherianRing 𝒪] (hx : Transcendental E (levelGen₁ F₀ g E)) :
    IsNoetherianRing (levelBaseRing 𝒪 F₀ {g}) :=
  isNoetherianRing_of_ringEquiv _ (levelPolynomialEquiv 𝒪 F₀ g hx)

theorem uniqueFactorizationMonoid_levelBaseRing [IsDomain 𝒪] [UniqueFactorizationMonoid 𝒪]
    (hx : Transcendental E (levelGen₁ F₀ g E)) : UniqueFactorizationMonoid (levelBaseRing 𝒪 F₀ {g}) :=
  (levelPolynomialEquiv 𝒪 F₀ g hx).toMulEquiv.uniqueFactorizationMonoid inferInstance

theorem prime_levelConst (hx : Transcendental E (levelGen₁ F₀ g E)) {ϖ : 𝒪} (hϖ : Prime ϖ) :
    Prime (⟨levelConst 𝒪 F₀ ϖ, levelConst_mem 𝒪 F₀ {g} ϖ⟩ : levelBaseRing 𝒪 F₀ {g}) := by
  have h : levelPolynomialEquiv 𝒪 F₀ g hx (Polynomial.C ϖ) = ⟨levelConst 𝒪 F₀ ϖ, levelConst_mem 𝒪 F₀ {g} ϖ⟩ :=
    Subtype.ext (levelPolynomialEquiv_C 𝒪 F₀ g hx ϖ)
  rw [← h, MulEquiv.prime_iff]
  exact Polynomial.prime_C_iff.mpr hϖ

end PolynomialStructure

end ModularCurve

end

#check @ModularCurve.levelBaseRing
#check @ModularCurve.exists_finset_forall_integral_laurentDescent
#print axioms ModularCurve.exists_finset_forall_integral_laurentDescent
#check @ModularCurve.integral_laurentDescent_of_integral
#check @ModularCurve.laurentDescent_mem_integralCoeffs_iff
#check @ModularCurve.levelPolynomialEquiv
#check @ModularCurve.prime_levelConst
#print axioms ModularCurve.prime_levelConst
#print axioms ModularCurve.uniqueFactorizationMonoid_levelBaseRing