import Definitions.Def_ModularCurve_JqCoeff import Definitions.Def_ModularCurve_LaurentCoeff import Definitions.Def_ModularCurve_PhiGen import Definitions.Def_AlgebraicCurve_DivisorClassGroup import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure import Mathlib.RingTheory.IntegralClosure.GoingDown import Mathlib.RingTheory.Polynomial.IsIntegral import Mathlib.RingTheory.Valuation.LocalSubring import Mathlib.RingTheory.Algebraic.Basic import Definitions.Def_AlgebraicCurve_PlacesOverDVR import Mathlib.FieldTheory.IsAlgClosed.Basic import Mathlib.Algebra.Polynomial.Lifts import Mathlib.RingTheory.Ideal.Quotient.Operations import Mathlib.RingTheory.Localization.AtPrime.Basic import Mathlib.RingTheory.Valuation.ValuationSubring import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.Algebra.CharP.Basic import Mathlib.Data.Int.CharZero import Mathlib.Data.Nat.Prime.Int import Mathlib.RingTheory.DedekindDomain.IntegralClosure import Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra import Mathlib.RingTheory.Ideal.Maps import Mathlib.RingTheory.Ideal.Maximal import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic import Definitions.Def_ModularCurve_FibreModel import Definitions.Def_ModularCurve_ArithmeticGalois import Definitions.Def_ModularCurve_PlaceSpecialization set_option autoImplicit false noncomputable section namespace ModularCurve namespace CharPModel open AlgebraicCurve variable (N : ℕ) [NeZero N] variable (A : ValuationSubring (AlgebraicClosure ℚ)) end CharPModel end ModularCurve set_option autoImplicit false noncomputable section namespace ModularCurve namespace CharPModel section LaurentMap variable {R S : Type*} [CommRing R] [CommRing S] private def laurentMapRingHom (f : R →+* S) : LaurentSeries R →+* LaurentSeries S where toFun x := x.map f map_one' := by ext g rw [HahnSeries.map_coeff, HahnSeries.coeff_one, HahnSeries.coeff_one, apply_ite f, map_one, map_zero] map_mul' x y := HahnSeries.map_mul f.toNonUnitalRingHom map_zero' := by ext g rw [HahnSeries.map_coeff, HahnSeries.coeff_zero, HahnSeries.coeff_zero, map_zero] map_add' x y := HahnSeries.map_add f.toAddMonoidHom @[simp] private theorem laurentMapRingHom_apply (f : R →+* S) (x : LaurentSeries R) : laurentMapRingHom f x = x.map f := rfl private theorem laurentMap_injective {f : R →+* S} (hf : Function.Injective f) {x y : LaurentSeries R} (h : x.map f = y.map f) : x = y := by ext g have hg := congrArg (fun z : LaurentSeries S => z.coeff g) h simpa only [HahnSeries.map_coeff] using hf hg private theorem map_eval₂Bivar (Φ : Polynomial (Polynomial ℤ)) (f : R →+* S) (u v : LaurentSeries R) : (Φ.eval₂ (Polynomial.aeval (R := ℤ) u).toRingHom v).map f = Φ.eval₂ (Polynomial.aeval (R := ℤ) (u.map f)).toRingHom (v.map f) := by have hcomp : (laurentMapRingHom f).comp (Polynomial.aeval (R := ℤ) u).toRingHom = (Polynomial.aeval (R := ℤ) (u.map f)).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X, laurentMapRingHom_apply] have h := Polynomial.hom_eval₂ Φ (Polynomial.aeval (R := ℤ) u).toRingHom (laurentMapRingHom f) v rw [← laurentMapRingHom_apply, h, hcomp, laurentMapRingHom_apply] end LaurentMap section FibreEval variable {R S : Type*} [CommRing R] [CommRing S] private theorem qExpand_map (N : ℕ) [NeZero N] (f : R →+* S) (x : LaurentSeries R) : (qExpand R N x).map f = qExpand S N (x.map f) := by ext k rw [HahnSeries.map_coeff] by_cases hk : (N : ℤ) ∣ k · obtain ⟨m, rfl⟩ := hk rw [qExpand_coeff_mul, qExpand_coeff_mul, HahnSeries.map_coeff] · have h1 := qExpand_coeff_of_not_dvd (R := R) (N := N) x hk have h2 := qExpand_coeff_of_not_dvd (R := S) (N := N) (x.map f) hk rw [h1, h2, map_zero] private theorem map_jqNModC (N : ℕ) [NeZero N] {K K' : Type*} [CommRing K] [CommRing K'] (f : K →+* K') : (jqNModC K N).map f = jqNModC K' N := by show (qExpand K N (jqModC K)).map f = qExpand K' N (jqModC K') rw [qExpand_map, map_jqModC] variable (N : ℕ) [NeZero N] (data : ModularPolynomialData N) private theorem intEval_eq_zero : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jqModC ℤ)).toRingHom (jqNModC ℤ N) = 0 := by refine laurentMap_injective (f := Int.castRingHom ℚ) (Int.castRingHom ℚ).injective_int ?_ rw [map_eval₂Bivar, map_jqModC, map_jqNModC, show (0 : LaurentSeries ℤ).map (Int.castRingHom ℚ) = 0 from map_zero (laurentMapRingHom (Int.castRingHom ℚ))] exact data.eval_eq_zero private theorem fibreEval_eq_zero (k : Type*) [CommRing k] : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jqModC k)).toRingHom (jqNModC k N) = 0 := by have h := congrArg (fun x : LaurentSeries ℤ => x.map (Int.castRingHom k)) (intEval_eq_zero N data) simpa only [map_eval₂Bivar, map_jqModC, map_jqNModC, show (0 : LaurentSeries ℤ).map (Int.castRingHom k) = 0 from map_zero (laurentMapRingHom (Int.castRingHom k))] using h private theorem intEvalSwap_eq_zero (hsym : EvalSymm data.Φ) : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jqNModC ℤ N)).toRingHom (jqModC ℤ) = 0 := by refine laurentMap_injective (f := Int.castRingHom ℚ) (Int.castRingHom ℚ).injective_int ?_ rw [map_eval₂Bivar, map_jqModC, map_jqNModC, show (0 : LaurentSeries ℤ).map (Int.castRingHom ℚ) = 0 from map_zero (laurentMapRingHom (Int.castRingHom ℚ))] rw [show jqModC ℚ = jq from rfl, show jqNModC ℚ N = jqN N from rfl] rw [hsym (jqN N) jq] exact data.eval_eq_zero private theorem fibreEvalSwap_eq_zero (hsym : EvalSymm data.Φ) (k : Type*) [CommRing k] : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jqNModC k N)).toRingHom (jqModC k) = 0 := by have h := congrArg (fun x : LaurentSeries ℤ => x.map (Int.castRingHom k)) (intEvalSwap_eq_zero N data hsym) simpa only [map_eval₂Bivar, map_jqModC, map_jqNModC, show (0 : LaurentSeries ℤ).map (Int.castRingHom k) = 0 from map_zero (laurentMapRingHom (Int.castRingHom k))] using h end FibreEval end CharPModel end ModularCurve noncomputable section namespace ModularCurve namespace CharPModel section LineTier private theorem transcendental_subtype {K L : Type*} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) {x : L} (hx : x ∈ S) (h : Transcendental K x) : Transcendental K (⟨x, hx⟩ : S) := by intro halg apply h obtain ⟨p, hp0, hp⟩ := halg refine ⟨p, hp0, ?_⟩ have h2 := congrArg S.val hp rw [map_zero, ← Polynomial.aeval_algHom_apply] at h2 simpa using h2 private theorem tjq_pow (K : Type*) [CommRing K] (n : ℕ) : (jqModC K) ^ n = HahnSeries.single (-(n : ℤ)) 1 * HahnSeries.ofPowerSeries ℤ K ((jNum.map (Int.castRingHom K)) ^ n) := by have h : n • (-1 : ℤ) = -(n : ℤ) := by simp rw [jqModC, mul_pow, HahnSeries.single_pow, one_pow, h, ← map_pow] private theorem tjq_constantCoeff_map (K : Type*) [CommRing K] : PowerSeries.constantCoeff (jNum.map (Int.castRingHom K)) = 1 := by rw [← PowerSeries.coeff_zero_eq_constantCoeff, PowerSeries.coeff_map, PowerSeries.coeff_zero_eq_constantCoeff, constantCoeff_jNum, map_one] private theorem tjq_coeff_pow_self (K : Type*) [CommRing K] (n : ℕ) : ((jqModC K) ^ n).coeff (-(n : ℤ)) = 1 := by rw [tjq_pow, HahnSeries.coeff_single_mul, one_mul, sub_neg_eq_add, neg_add_cancel, show (0 : ℤ) = ((0 : ℕ) : ℤ) from rfl, HahnSeries.ofPowerSeries_apply_coeff, PowerSeries.coeff_zero_eq_constantCoeff, map_pow, tjq_constantCoeff_map, one_pow] private theorem tjq_coeff_pow_of_lt (K : Type*) [CommRing K] {n : ℕ} {m : ℤ} (hm : m < -(n : ℤ)) : ((jqModC K) ^ n).coeff m = 0 := by rw [tjq_pow, HahnSeries.coeff_single_mul, one_mul] exact ofPowerSeries_coeff_of_neg _ (by omega) private theorem tjq_algebraMap_eq_single (K : Type*) [CommRing K] (c : K) : algebraMap K (LaurentSeries K) c = HahnSeries.single 0 c := by have h1 : algebraMap K (PowerSeries K) c = PowerSeries.C c := by simp rw [HahnSeries.algebraMap_apply', h1, HahnSeries.ofPowerSeries_C] rfl private theorem tjq_aeval_eq_zero (K : Type*) [CommRing K] {p : Polynomial K} (hp : Polynomial.aeval (jqModC K) p = 0) : p = 0 := by by_contra hp0 set n := p.natDegree with hn have hcoeff : (Polynomial.aeval (jqModC K) p).coeff (-(n : ℤ)) = p.coeff n := by rw [Polynomial.aeval_def, Polynomial.eval₂_eq_sum_range, HahnSeries.coeff_sum, Finset.sum_eq_single n] · rw [tjq_algebraMap_eq_single, HahnSeries.coeff_single_zero_mul, tjq_coeff_pow_self, mul_one] · intro i hi hin have hilt : i < n := lt_of_le_of_ne (Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)) hin rw [tjq_algebraMap_eq_single, HahnSeries.coeff_single_zero_mul, tjq_coeff_pow_of_lt, mul_zero] omega · intro hn' exact absurd (Finset.self_mem_range_succ n) hn' rw [hp] at hcoeff simp only [HahnSeries.coeff_zero] at hcoeff exact hp0 (Polynomial.leadingCoeff_eq_zero.mp hcoeff.symm) private theorem tjq_transcendental (K : Type*) [CommRing K] : Transcendental K (jqModC K) := transcendental_iff.mpr fun _ hp => tjq_aeval_eq_zero K hp private theorem coeffEmb_jq_eq_jqModC : coeffEmb (AlgebraicClosure ℚ) jq = jqModC (AlgebraicClosure ℚ) := by have hmap : jNumQ.map (algebraMap ℚ (AlgebraicClosure ℚ)) = jNum.map (Int.castRingHom (AlgebraicClosure ℚ)) := by ext n simp [jNumQ, PowerSeries.coeff_map] rw [jq, jqModC, map_mul] congr 1 · ext k rw [coeffEmb_coeff] by_cases hk : k = (-1 : ℤ) <;> simp [hk] · ext k rw [coeffEmb_coeff] by_cases hk : 0 ≤ k · lift k to ℕ using hk rw [HahnSeries.ofPowerSeries_apply_coeff, HahnSeries.ofPowerSeries_apply_coeff, ← hmap, PowerSeries.coeff_map] · rw [ofPowerSeries_coeff_of_neg _ (by omega), ofPowerSeries_coeff_of_neg _ (by omega), map_zero] section ResidueFieldInline variable {K₀ F₀ F₀' : Type*} [Field K₀] [Field F₀] [Field F₀'] [Algebra K₀ F₀] [Algebra K₀ F₀'] [Algebra F₀ F₀'] [IsScalarTower K₀ F₀ F₀'] [FiniteDimensional F₀ F₀'] open IsLocalRing in private theorem rf_linearIndependent_lift (w : AlgebraicCurve.Place K₀ F₀') {ι : Type*} [Fintype ι] (x : ι → w.toValuationSubring) (hx : LinearIndependent (w.restrict F₀).ResidueField fun i => (residue w.toValuationSubring (x i) : w.ResidueField)) : LinearIndependent F₀ fun i => ((x i : w.toValuationSubring) : F₀') := by classical rw [Fintype.linearIndependent_iff] intro g hg by_contra hne obtain ⟨i₀, hi₀⟩ : ∃ i, g i ≠ 0 := not_forall.mp hne set O : ValuationSubring F₀ := (w.restrict F₀).toValuationSubring have hne' : (Finset.univ.filter fun i => g i ≠ 0).Nonempty := ⟨i₀, by simpa using hi₀⟩ obtain ⟨m, hm, hmmax⟩ := Finset.exists_max_image _ (fun i => O.valuation (g i)) hne' have hgm : g m ≠ 0 := by simpa using hm have hb : ∀ i, g i / g m ∈ O := by intro i by_cases hi : g i = 0 · simp [hi] · apply O.mem_of_valuation_le_one rw [map_div₀] have hm0 : (0 : O.ValueGroup) < O.valuation (g m) := by rw [zero_lt_iff]; exact (map_ne_zero _).mpr hgm exact (div_le_one₀ hm0).mpr (hmmax i (by simpa using hi)) let b : ι → O := fun i => ⟨g i / g m, hb i⟩ have hrel : ∑ i, AlgebraicCurve.Place.restrictInclusion F₀ w (b i) * x i = 0 := by apply Subtype.ext have hcoe : ((∑ i, AlgebraicCurve.Place.restrictInclusion F₀ w (b i) * x i : w.toValuationSubring) : F₀') = ∑ i, algebraMap F₀ F₀' (g i / g m) * (x i : F₀') := by rw [AddSubmonoidClass.coe_finsetSum] refine Finset.sum_congr rfl fun i _ => ?_ rw [MulMemClass.coe_mul, AlgebraicCurve.Place.coe_restrictInclusion] rw [hcoe] have : ∑ i, algebraMap F₀ F₀' (g i / g m) * (x i : F₀') = algebraMap F₀ F₀' (g m)⁻¹ * ∑ i, g i • ((x i : w.toValuationSubring) : F₀') := by rw [Finset.mul_sum] refine Finset.sum_congr rfl fun i _ => ?_ rw [Algebra.smul_def, div_eq_inv_mul, map_mul, mul_assoc] rw [this, hg, mul_zero] rfl have hres : ∑ i, (residue O (b i) : (w.restrict F₀).ResidueField) • (residue w.toValuationSubring (x i) : w.ResidueField) = 0 := by have h := congrArg (residue w.toValuationSubring) hrel rw [map_sum, map_zero] at h rw [← h] refine Finset.sum_congr rfl fun i _ => ?_ rw [Algebra.smul_def, AlgebraicCurve.Place.algebraMap_residueField_eq, AlgebraicCurve.Place.restrictResidueMap_residue, map_mul] have hm1 := (Fintype.linearIndependent_iff.mp hx) _ hres m have hbm : b m = 1 := Subtype.ext (div_self hgm) rw [hbm, map_one] at hm1 exact one_ne_zero hm1 open IsLocalRing in private theorem rf_finite_residueField (w : AlgebraicCurve.Place K₀ F₀') : Module.Finite (w.restrict F₀).ResidueField w.ResidueField := by classical rw [← Module.rank_lt_aleph0_iff] refine lt_of_le_of_lt (rank_le (n := Module.finrank F₀ F₀') fun s hs => ?_) Cardinal.natCast_lt_aleph0 choose x hx using fun y : s => residue_surjective (R := w.toValuationSubring) (y : w.ResidueField) have hs' : LinearIndependent (w.restrict F₀).ResidueField fun i : s => (residue w.toValuationSubring (x i) : w.ResidueField) := by simpa only [hx] using hs have := rf_linearIndependent_lift (F₀ := F₀) w x hs' simpa [Fintype.card_coe] using this.fintype_card_le_finrank end ResidueFieldInline private theorem transcendental_jBar (N : ℕ) [NeZero N] : Transcendental (AlgebraicClosure ℚ) (jBar N) := by have h := tjq_transcendental (AlgebraicClosure ℚ) rw [← coeffEmb_jq_eq_jqModC] at h exact transcendental_subtype _ (coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full N (jq_mem N))) h private theorem transcendental_jC (k : Type*) [Field k] (N : ℕ) [NeZero N] : Transcendental k (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) := transcendental_subtype _ (jqModC_mem k N) (tjq_transcendental k) private theorem fibreEval_subtype (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) = 0 := by have hcomp : ((modularFunctionFieldC k N).val.toRingHom).comp (Polynomial.aeval (R := ℤ) (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom = (Polynomial.aeval (R := ℤ) (jqModC k)).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X] rfl have h := Polynomial.hom_eval₂ data.Φ (Polynomial.aeval (R := ℤ) (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom ((modularFunctionFieldC k N).val.toRingHom) (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) apply Subtype.val_injective have h0 : (modularFunctionFieldC k N).val.toRingHom (data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)) = 0 := by rw [h, hcomp] exact fibreEval_eq_zero N data k simpa using h0 private theorem adjoin_pair_subtype_eq_top {K L : Type*} [Field K] [Field L] [Algebra K L] (x y : L) : IntermediateField.adjoin K ({⟨x, IntermediateField.subset_adjoin K {x, y} (Set.mem_insert x {y})⟩, ⟨y, IntermediateField.subset_adjoin K {x, y} (Set.mem_insert_of_mem x rfl)⟩} : Set (IntermediateField.adjoin K ({x, y} : Set L))) = ⊤ := by rw [eq_top_iff] rintro ⟨z, hz⟩ - induction hz using IntermediateField.adjoin_induction with | mem z hzm => rcases hzm with rfl | hzm · exact IntermediateField.subset_adjoin _ _ (Set.mem_insert _ _) · rcases hzm with rfl exact IntermediateField.subset_adjoin _ _ (Set.mem_insert_of_mem _ rfl) | algebraMap a => exact IntermediateField.algebraMap_mem _ a | add a b ha hb hia hib => exact add_mem hia hib | mul a b ha hb hia hib => exact mul_mem hia hib | inv a ha hia => exact inv_mem hia private theorem isIntegral_adjoin_of_bivar_monic {K L : Type*} [Field K] [Field L] [Algebra K L] {Φ : Polynomial (Polynomial ℤ)} (hΦ : Φ.Monic) {x y : L} (h : Φ.eval₂ (Polynomial.aeval (R := ℤ) x).toRingHom y = 0) : IsIntegral (IntermediateField.adjoin K ({x} : Set L)) y := by set g : Polynomial ℤ →+* IntermediateField.adjoin K ({x} : Set L) := (Polynomial.aeval (R := ℤ) (⟨x, IntermediateField.mem_adjoin_simple_self K x⟩ : IntermediateField.adjoin K ({x} : Set L))).toRingHom with hg have hcomp : (algebraMap (IntermediateField.adjoin K ({x} : Set L)) L).comp g = (Polynomial.aeval (R := ℤ) x).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [hg, RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X] rfl refine ⟨Φ.map g, hΦ.map g, ?_⟩ rw [Polynomial.eval₂_map, hcomp] exact h private theorem barEval_laurent (N : ℕ) [NeZero N] (data : ModularPolynomialData N) : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (coeffEmb (AlgebraicClosure ℚ) jq)).toRingHom (coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq)) = 0 := by have hcomp : ((coeffEmb (AlgebraicClosure ℚ)).comp (Polynomial.aeval (R := ℤ) jq).toRingHom) = (Polynomial.aeval (R := ℤ) (coeffEmb (AlgebraicClosure ℚ) jq)).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X] have h := Polynomial.hom_eval₂ data.Φ (Polynomial.aeval (R := ℤ) jq).toRingHom (coeffEmb (AlgebraicClosure ℚ)) (qExpand ℚ N jq) have h0 := data.eval_eq_zero rw [show evalAtJ = (Polynomial.aeval (R := ℤ) jq).toRingHom from rfl, show jqN N = qExpand ℚ N jq from rfl] at h0 rw [h0, map_zero, hcomp] at h exact h.symm private theorem barEval_subtype (N : ℕ) [NeZero N] (data : ModularPolynomialData N) : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom (jNBar N) = 0 := by have hcomp : (((laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom).comp (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom) = (Polynomial.aeval (R := ℤ) (coeffEmb (AlgebraicClosure ℚ) jq)).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X] rfl have h := Polynomial.hom_eval₂ data.Φ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom ((laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom) (jNBar N) apply Subtype.val_injective have h0 : (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom (data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom (jNBar N)) = 0 := by rw [h, hcomp] exact barEval_laurent N data simpa using h0 set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 200000 in private theorem finiteDimensional_adjoin_jC (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) : FiniteDimensional (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) (modularFunctionFieldC k N) := by have hint : IsIntegral (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) := isIntegral_adjoin_of_bivar_monic data.monic (fibreEval_subtype k N data) have htop := adjoin_pair_subtype_eq_top (K := k) (jqModC k) (jqNModC k N) have htower := IntermediateField.adjoin_adjoin_left k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)) {⟨jqNModC k N, jqNModC_mem k N⟩} rw [Set.singleton_union] at htower have hpair : IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩, ⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N)) = ⊤ := htop rw [hpair] at htower have hFD : FiniteDimensional (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) (IntermediateField.adjoin (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N))) := IntermediateField.adjoin.finiteDimensional hint have h2 : IntermediateField.adjoin (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N)) = ⊤ := IntermediateField.restrictScalars_injective k (htower.trans IntermediateField.restrictScalars_top.symm) rw [h2] at hFD exact (IntermediateField.topEquiv (F := IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)))).toLinearEquiv.finiteDimensional private theorem algebraMap_comp_aeval_adjoin_self {K L : Type*} [Field K] [Field L] [Algebra K L] (x : L) : (algebraMap (IntermediateField.adjoin K ({x} : Set L)) L).comp (Polynomial.aeval (R := ℤ) (IntermediateField.AdjoinSimple.gen K x)).toRingHom = (Polynomial.aeval (R := ℤ) x).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X] rfl set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private def jLine (k : Type*) [Field k] (N : ℕ) [NeZero N] : modularFunctionFieldC k N := ⟨jqModC k, jqModC_mem k N⟩ set_option synthInstance.maxHeartbeats 400000 in private def jNLine (k : Type*) [Field k] (N : ℕ) [NeZero N] : modularFunctionFieldC k N := ⟨jqNModC k N, jqNModC_mem k N⟩ private theorem transcendental_jLine (k : Type*) [Field k] (N : ℕ) [NeZero N] : Transcendental k (jLine k N) := transcendental_jC k N set_option synthInstance.maxHeartbeats 400000 in private noncomputable def lineEquivC (k : Type*) [Field k] (N : ℕ) [NeZero N] : RatFunc k ≃ₐ[k] (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) := RatFunc.algEquivOfTranscendental _ (transcendental_jLine k N) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem lineEquivC_algebraMap (k : Type*) [Field k] (N : ℕ) [NeZero N] (g : Polynomial k) : lineEquivC k N (algebraMap (Polynomial k) (RatFunc k) g) = Polynomial.aeval (IntermediateField.AdjoinSimple.gen k (jLine k N)) g := RatFunc.algEquivOfTranscendental_algebraMap _ (transcendental_jLine k N) g set_option maxSynthPendingDepth 3 in set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem lineX (k : Type*) [Field k] (N : ℕ) [NeZero N] : lineEquivC k N (algebraMap (Polynomial k) (RatFunc k) Polynomial.X) = IntermediateField.AdjoinSimple.gen k (jLine k N) := by rw [lineEquivC_algebraMap, Polynomial.aeval_X] set_option maxSynthPendingDepth 3 in set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem lineConst (k : Type*) [Field k] (N : ℕ) [NeZero N] (a : ℤ) : Polynomial.aeval (R := ℤ) (IntermediateField.AdjoinSimple.gen k (jLine k N)) (Polynomial.C a) = lineEquivC k N (algebraMap (Polynomial k) (RatFunc k) ((Polynomial.C a).map (Int.castRingHom k))) := by rw [Polynomial.aeval_C, Polynomial.map_C, show Polynomial.C ((Int.castRingHom k) a) = algebraMap k (Polynomial k) ((Int.castRingHom k) a) from rfl, ← IsScalarTower.algebraMap_apply k (Polynomial k) (RatFunc k), AlgEquiv.commutes] simp only [eq_intCast, map_intCast] set_option maxSynthPendingDepth 3 in set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem lineFun (k : Type*) [Field k] (N : ℕ) [NeZero N] (p : Polynomial ℤ) : Polynomial.aeval (R := ℤ) (IntermediateField.AdjoinSimple.gen k (jLine k N)) p = lineEquivC k N (algebraMap (Polynomial k) (RatFunc k) (p.map (Int.castRingHom k))) := by induction p using Polynomial.induction_on with | C a => exact lineConst k N a | add p q hp hq => rw [Polynomial.map_add, map_add, map_add, map_add, hp, hq] | monomial n a _ => simp only [Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_X, map_mul, map_pow, lineX, Polynomial.aeval_X] rw [lineConst k N a] set_option maxSynthPendingDepth 3 in set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem lineMapEq (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) : data.Φ.map ((Polynomial.aeval (R := ℤ) (IntermediateField.AdjoinSimple.gen k (jLine k N))).toRingHom) = ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).map (lineEquivC k N).toAlgHom.toRingHom := by apply Polynomial.ext intro n rw [Polynomial.coeff_map, Polynomial.coeff_map, Polynomial.coeff_map, Polynomial.coeff_map] exact lineFun k N (data.Φ.coeff n) set_option maxSynthPendingDepth 3 in set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem linePsep (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) : (data.Φ.map ((Polynomial.aeval (R := ℤ) (IntermediateField.AdjoinSimple.gen k (jLine k N))).toRingHom)).Separable := by rw [lineMapEq k N data] exact hsep.map set_option maxSynthPendingDepth 3 in set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem lineAevalZero (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) : Polynomial.aeval (R := IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (jNLine k N) (data.Φ.map ((Polynomial.aeval (R := ℤ) (IntermediateField.AdjoinSimple.gen k (jLine k N))).toRingHom)) = 0 := by rw [Polynomial.aeval_def, Polynomial.eval₂_map, algebraMap_comp_aeval_adjoin_self (jLine k N)] exact fibreEval_subtype k N data set_option maxSynthPendingDepth 3 in set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem lineDvd (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) : minpoly (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (jNLine k N) ∣ data.Φ.map ((Polynomial.aeval (R := ℤ) (IntermediateField.AdjoinSimple.gen k (jLine k N))).toRingHom) := minpoly.dvd (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (jNLine k N) (lineAevalZero k N data) set_option maxSynthPendingDepth 3 in set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem isSeparable_jNC (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) : IsSeparable (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) := (linePsep k N data hsep).of_dvd (lineDvd k N data) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem isSeparable_line_fibre (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) : Algebra.IsSeparable (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) (modularFunctionFieldC k N) := by have hadj : Algebra.IsSeparable (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) (IntermediateField.adjoin (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N))) := (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable _ _).mpr (isSeparable_jNC k N data hsep) have htower := IntermediateField.adjoin_adjoin_left k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N)) {⟨jqNModC k N, jqNModC_mem k N⟩} rw [Set.singleton_union] at htower have hpair : IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩, ⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N)) = ⊤ := adjoin_pair_subtype_eq_top (K := k) (jqModC k) (jqNModC k N) rw [hpair] at htower have h2 : IntermediateField.adjoin (IntermediateField.adjoin k ({⟨jqModC k, jqModC_mem k N⟩} : Set (modularFunctionFieldC k N))) ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N)) = ⊤ := IntermediateField.restrictScalars_injective k (htower.trans IntermediateField.restrictScalars_top.symm) rw [h2] at hadj haveI := hadj exact AlgEquiv.Algebra.isSeparable IntermediateField.topEquiv end LineTier section BarFinDim private def jdBar (N : ℕ) [NeZero N] (d : ℕ) [NeZero d] (hd : d ∣ N) : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N) := ⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ d jq), coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jqd_mem_full N hd)⟩ set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem barEvalD_subtype (N : ℕ) [NeZero N] (d : ℕ) [NeZero d] (hd : d ∣ N) (data : ModularPolynomialData d) : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom (jdBar N d hd) = 0 := by have hcomp : (((laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom).comp (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom) = (Polynomial.aeval (R := ℤ) (coeffEmb (AlgebraicClosure ℚ) jq)).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X] rfl have h := Polynomial.hom_eval₂ data.Φ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom ((laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom) (jdBar N d hd) apply Subtype.val_injective have h0 : (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom (data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jBar N)).toRingHom (jdBar N d hd)) = 0 := by rw [h, hcomp] exact barEval_laurent d data simpa using h0 set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem lbc_eq_adjoin_divisors (N : ℕ) [NeZero N] : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N) = IntermediateField.adjoin (AlgebraicClosure ℚ) (⇑(coeffEmb (AlgebraicClosure ℚ)) '' divisorExpansions N) := by refine le_antisymm (IntermediateField.adjoin_le_iff.mpr ?_) (IntermediateField.adjoin_le_iff.mpr ?_) · rintro x ⟨y, hy, rfl⟩ have hy' : y ∈ IntermediateField.adjoin ℚ (divisorExpansions N) := hy induction hy' using IntermediateField.adjoin_induction with | mem z hz => exact IntermediateField.subset_adjoin _ _ ⟨z, hz, rfl⟩ | algebraMap a => rw [eq_ratCast, map_ratCast] simp | add a b ha hb hia hib => rw [map_add]; exact add_mem (hia ha) (hib hb) | mul a b ha hb hia hib => rw [map_mul]; exact mul_mem (hia ha) (hib hb) | inv a ha hia => rw [map_inv₀]; exact inv_mem (hia ha) · rintro x ⟨y, hy, rfl⟩ exact coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (IntermediateField.subset_adjoin ℚ _ hy) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem adjoin_val_preimage_eq_top {K L : Type*} [Field K] [Field L] [Algebra K L] {F : IntermediateField K L} {S : Set L} (hF : F = IntermediateField.adjoin K S) : IntermediateField.adjoin K (Subtype.val ⁻¹' S : Set F) = ⊤ := by subst hF rw [eq_top_iff] rintro ⟨z, hz⟩ - induction hz using IntermediateField.adjoin_induction with | mem w hw => exact IntermediateField.subset_adjoin _ _ hw | algebraMap a => exact IntermediateField.algebraMap_mem _ a | add a b ha hb hia hib => exact add_mem hia hib | mul a b ha hb hia hib => exact mul_mem hia hib | inv a ha hia => exact inv_mem hia private def barGenSet (N : ℕ) [NeZero N] : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := Subtype.val ⁻¹' (⇑(coeffEmb (AlgebraicClosure ℚ)) '' divisorExpansions N) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem adjoin_barGenSet_eq_top (N : ℕ) [NeZero N] : IntermediateField.adjoin (AlgebraicClosure ℚ) (barGenSet N) = ⊤ := adjoin_val_preimage_eq_top (lbc_eq_adjoin_divisors N) private theorem barGenSet_finite (N : ℕ) [NeZero N] : (barGenSet N).Finite := by apply Set.Finite.preimage Subtype.val_injective.injOn apply Set.Finite.image have hsub : divisorExpansions N ⊆ (fun d : {d // d ∈ N.divisors} => @qExpand ℚ _ d.1 ⟨(Nat.pos_of_mem_divisors d.2).ne'⟩ jq) '' Set.univ := by rintro x ⟨d, hne, hd, hx⟩ haveI := hne exact ⟨⟨d, Nat.mem_divisors.mpr ⟨hd, NeZero.ne N⟩⟩, Set.mem_univ _, hx.symm⟩ exact ((Set.finite_univ (α := {d // d ∈ N.divisors})).image _).subset hsub private theorem jBar_mem_barGenSet (N : ℕ) [NeZero N] : jBar N ∈ barGenSet N := ⟨qExpand ℚ 1 jq, mem_divisorExpansions N (one_dvd N), by rw [qExpand_one_apply]; rfl⟩ set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem barGenSet_integral (N : ℕ) [NeZero N] (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) : ∀ x ∈ barGenSet N, IsIntegral (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) x := by rintro ⟨xv, hxF⟩ hx obtain ⟨y, hy, hxy⟩ := hx obtain ⟨d, hdne, hd, rfl⟩ := hy haveI := hdne have hxel : (⟨xv, hxF⟩ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) = jdBar N d hd := Subtype.ext hxy.symm rw [hxel] exact isIntegral_adjoin_of_bivar_monic (dataAll d hd).monic (barEvalD_subtype N d hd (dataAll d hd)) set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem finiteDimensional_lineBar_of_dataAll (N : ℕ) [NeZero N] (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) : FiniteDimensional (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := by haveI : Finite ↥(barGenSet N) := (barGenSet_finite N).to_subtype have hint := barGenSet_integral N dataAll have htower := IntermediateField.adjoin_adjoin_left (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (barGenSet N) rw [Set.singleton_union, Set.insert_eq_self.mpr (jBar_mem_barGenSet N), adjoin_barGenSet_eq_top N] at htower have h2 : IntermediateField.adjoin (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (barGenSet N) = ⊤ := IntermediateField.restrictScalars_injective (AlgebraicClosure ℚ) (htower.trans IntermediateField.restrictScalars_top.symm) have hFD : FiniteDimensional (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (IntermediateField.adjoin (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (barGenSet N)) := IntermediateField.finiteDimensional_adjoin hint rw [h2] at hFD exact (IntermediateField.topEquiv (F := IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))))).toLinearEquiv.finiteDimensional end BarFinDim end CharPModel end ModularCurve set_option autoImplicit false open Polynomial namespace ValuationSubring variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K) private theorem closureConstantsAdjoin_eq_range_aeval (x : F) : Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x}) = (aeval (R := A) x).toRingHom.range := by apply le_antisymm · rw [Subring.closure_le] rintro y (⟨a, rfl⟩ | rfl) · refine ⟨C a, ?_⟩ simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, aeval_C, RingHom.coe_comp, Function.comp_apply] rfl · exact ⟨X, by simp⟩ · rintro y ⟨p, rfl⟩ simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe] induction p using Polynomial.induction_on with | C a => rw [aeval_C] exact Subring.subset_closure (Or.inl ⟨a, rfl⟩) | add p q hp hq => rw [map_add] exact Subring.add_mem _ hp hq | monomial n a h => rw [pow_succ, ← mul_assoc, map_mul, aeval_X] exact Subring.mul_mem _ h (Subring.subset_closure (Or.inr rfl)) private theorem aeval_injective_of_transcendental {x : F} (hx : Transcendental K x) : Function.Injective (aeval (R := A) x) := by rw [injective_iff_map_eq_zero] intro p hp have hK : aeval x (p.map (algebraMap A K)) = 0 := by rwa [aeval_map_algebraMap] have hp' : p.map (algebraMap A K) = 0 := (injective_iff_map_eq_zero _).mp (transcendental_iff_injective.mp hx) _ hK exact (Polynomial.map_injective (algebraMap A K) Subtype.val_injective) (by rw [hp', Polynomial.map_zero]) private theorem aeval_mem_closure (x : F) (p : A[X]) : aeval x p ∈ Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x}) := by rw [closureConstantsAdjoin_eq_range_aeval] exact ⟨p, rfl⟩ private noncomputable def polynomialEquivClosure {x : F} (hx : Transcendental K x) : A[X] ≃+* Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x}) := RingEquiv.ofBijective ((aeval (R := A) x).toRingHom.codRestrict _ (A.aeval_mem_closure x)) ⟨fun p q h => A.aeval_injective_of_transcendental hx (Subtype.ext_iff.mp h), fun y => by obtain ⟨p, hp⟩ : (y : F) ∈ (aeval (R := A) x).toRingHom.range := by rw [← closureConstantsAdjoin_eq_range_aeval] exact y.2 exact ⟨p, Subtype.ext hp⟩⟩ @[simp] private theorem polynomialEquivClosure_apply {x : F} (hx : Transcendental K x) (p : A[X]) : (A.polynomialEquivClosure hx p : F) = aeval x p := rfl private theorem isIntegrallyClosed_closure {x : F} (hx : Transcendental K x) : IsIntegrallyClosed (Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x})) := IsIntegrallyClosed.of_equiv (A.polynomialEquivClosure hx) end ValuationSubring namespace Subring variable {F : Type*} [Field F] private theorem isIntegral_iff_exists_monic_eval₂ (S : Subring F) (b : F) : IsIntegral S b ↔ ∃ p : Polynomial S, p.Monic ∧ Polynomial.eval₂ S.subtype b p = 0 := Iff.rfl private theorem exists_ideal_le_comap_eq_of_isIntegral {S B : Subring F} (hSB : S ≤ B) [IsIntegrallyClosed S] (hint : ∀ b : B, IsIntegral S (b : F)) {p q : Ideal S} [p.IsPrime] [q.IsPrime] (hpq : p ≤ q) (Q : Ideal B) [Q.IsPrime] (hQ : Q.comap (Subring.inclusion hSB) = q) : ∃ P : Ideal B, P ≤ Q ∧ P.IsPrime ∧ P.comap (Subring.inclusion hSB) = p := by letI : Algebra S B := (Subring.inclusion hSB).toAlgebra have halg : ∀ s : S, algebraMap S B s = Subring.inclusion hSB s := fun _ => rfl haveI : FaithfulSMul S B := (faithfulSMul_iff_algebraMap_injective S B).mpr fun a b h => by rw [halg, halg] at h have h' : (a : F) = (b : F) := congrArg (fun y : B => (y : F)) h exact Subtype.ext h' haveI : Algebra.IsIntegral S B := ⟨fun b => by obtain ⟨f, hf, hfb⟩ := hint b refine ⟨f, hf, ?_⟩ apply Subtype.val_injective change B.subtype (Polynomial.eval₂ (algebraMap S B) b f) = ((0 : B) : F) have hc : B.subtype.comp (algebraMap S B) = S.subtype := RingHom.ext fun _ => rfl rw [Polynomial.hom_eval₂, hc] exact hfb⟩ haveI : Q.LiesOver q := ⟨by rw [Ideal.under_def, ← hQ]; rfl⟩ obtain ⟨P, hPQ, hP, hPp⟩ := Ideal.exists_ideal_le_liesOver_of_le (p := p) (q := q) Q hpq exact ⟨P, hPQ, hP, by rw [hPp.over, Ideal.under_def]; rfl⟩ end Subring set_option autoImplicit false noncomputable section open IsLocalRing namespace AlgebraicCurve namespace Place variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F) private theorem algebraMap_mem (a : K) : algebraMap K F a ∈ w.toValuationSubring := w.algebraMap_mem' a private theorem algebraMap_mem_nonunits_iff (a : K) : algebraMap K F a ∈ w.toValuationSubring.nonunits ↔ a = 0 := by constructor · intro h rcases (ValuationSubring.mem_nonunits_iff_or _).mp h with h0 | hinv · exact (map_eq_zero _).mp h0 · exact absurd (by simpa using w.algebraMap_mem a⁻¹) hinv · rintro rfl simp [ZeroMemClass.zero_mem] private theorem mul_mem_nonunits {x y : F} (hx : x ∈ w.toValuationSubring.nonunits) (hy : y ∈ w.toValuationSubring) : x * y ∈ w.toValuationSubring.nonunits := by rw [ValuationSubring.mem_nonunits_iff] at hx ⊢ rw [← ValuationSubring.valuation_le_one_iff] at hy calc w.toValuationSubring.valuation (x * y) = w.toValuationSubring.valuation x * w.toValuationSubring.valuation y := map_mul _ _ _ _ ≤ w.toValuationSubring.valuation x * 1 := by gcongr _ = w.toValuationSubring.valuation x := mul_one _ _ < 1 := hx private theorem mem_of_ord_pos {f : F} (h : 0 < w.ord f) : f ∈ w.toValuationSubring := by have hf : f ≠ 0 := by rintro rfl; simp at h obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible w.toValuationSubring obtain ⟨u, hu⟩ := w.exists_unit_mul_zpow hf hπ rw [hu, show w.ord f = (((w.ord f).toNat : ℕ) : ℤ) from (Int.toNat_of_nonneg h.le).symm, zpow_natCast] exact mul_mem (u : w.toValuationSubring).2 (pow_mem (π : w.toValuationSubring).2 _) private theorem mem_nonunits_iff_ord_pos {f : F} (hf : f ≠ 0) : f ∈ w.toValuationSubring.nonunits ↔ 0 < w.ord f := by constructor · intro h have hmem : f ∈ w.toValuationSubring := w.toValuationSubring.nonunits_subset h have h' : ((⟨f, hmem⟩ : w.toValuationSubring) : F) ∈ w.toValuationSubring.nonunits := h rw [ValuationSubring.coe_mem_nonunits_iff] at h' exact (w.mem_maximalIdeal_iff_ord_pos hf hmem).mp h' · intro h have hmem : f ∈ w.toValuationSubring := w.mem_of_ord_pos h have h' := (w.mem_maximalIdeal_iff_ord_pos hf hmem).mpr h rw [← ValuationSubring.coe_mem_nonunits_iff] at h' exact h' private def HasValueAt (f : F) (a : K) : Prop := f - algebraMap K F a ∈ w.toValuationSubring.nonunits private theorem hasValueAt_iff (f : F) (a : K) : w.HasValueAt f a ↔ f - algebraMap K F a ∈ w.toValuationSubring.nonunits := Iff.rfl private theorem hasValueAt_iff_ord_pos {f : F} {a : K} (h : f ≠ algebraMap K F a) : w.HasValueAt f a ↔ 0 < w.ord (f - algebraMap K F a) := w.mem_nonunits_iff_ord_pos (sub_ne_zero.mpr h) private theorem hasValueAt_of_ord_pos {f : F} {a : K} (h : 0 < w.ord (f - algebraMap K F a)) : w.HasValueAt f a := by have hne : f ≠ algebraMap K F a := by intro hfa; rw [hfa, sub_self] at h; simp at h exact (w.hasValueAt_iff_ord_pos hne).mpr h private theorem hasValueAt_algebraMap (a : K) : w.HasValueAt (algebraMap K F a) a := by simp [HasValueAt, ZeroMemClass.zero_mem] private theorem hasValueAt_zero_iff (f : F) : w.HasValueAt f 0 ↔ f ∈ w.toValuationSubring.nonunits := by simp [HasValueAt] private theorem mem_of_hasValueAt {f : F} {a : K} (h : w.HasValueAt f a) : f ∈ w.toValuationSubring := by have h1 : f - algebraMap K F a ∈ w.toValuationSubring := w.toValuationSubring.nonunits_subset h simpa using add_mem h1 (w.algebraMap_mem a) variable {w} in private theorem HasValueAt.unique {f : F} {a b : K} (ha : w.HasValueAt f a) (hb : w.HasValueAt f b) : a = b := by have h : algebraMap K F (a - b) ∈ w.toValuationSubring.nonunits := by have := sub_mem hb ha rwa [sub_sub_sub_cancel_left, ← map_sub] at this exact sub_eq_zero.mp ((w.algebraMap_mem_nonunits_iff _).mp h) variable {w} in private theorem HasValueAt.add {f g : F} {a b : K} (hf : w.HasValueAt f a) (hg : w.HasValueAt g b) : w.HasValueAt (f + g) (a + b) := by have := add_mem hf hg rw [HasValueAt, map_add] convert this using 1 ring variable {w} in private theorem HasValueAt.neg {f : F} {a : K} (hf : w.HasValueAt f a) : w.HasValueAt (-f) (-a) := by have := neg_mem hf rw [HasValueAt, map_neg] convert this using 1 ring variable {w} in private theorem HasValueAt.mul {f g : F} {a b : K} (hf : w.HasValueAt f a) (hg : w.HasValueAt g b) : w.HasValueAt (f * g) (a * b) := by have h1 : (f - algebraMap K F a) * g ∈ w.toValuationSubring.nonunits := w.mul_mem_nonunits hf (w.mem_of_hasValueAt hg) have h2 : (g - algebraMap K F b) * algebraMap K F a ∈ w.toValuationSubring.nonunits := w.mul_mem_nonunits hg (w.algebraMap_mem a) have := add_mem h1 h2 rw [HasValueAt, map_mul] convert this using 1 ring variable {w} in private theorem HasValueAt.inv {f : F} {a : K} (hf : w.HasValueAt f a) (ha : a ≠ 0) : w.HasValueAt f⁻¹ a⁻¹ := by have hf0 : f ≠ 0 := by rintro rfl have : w.HasValueAt (0 : F) 0 := by simpa using w.hasValueAt_algebraMap 0 exact ha (hf.unique this) have hfu : f ∉ w.toValuationSubring.nonunits := fun hfn => ha (hf.unique ((w.hasValueAt_zero_iff f).mpr hfn)) have hfinv : f⁻¹ ∈ w.toValuationSubring := by by_contra hne exact hfu ((ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inr (by simpa using hne))) have hprod : (f - algebraMap K F a) * (f⁻¹ * algebraMap K F a⁻¹) ∈ w.toValuationSubring.nonunits := w.mul_mem_nonunits hf (mul_mem hfinv (w.algebraMap_mem _)) have := neg_mem hprod change f⁻¹ - algebraMap K F a⁻¹ ∈ w.toValuationSubring.nonunits convert this using 1 have haF : algebraMap K F a ≠ 0 := by simpa using ha rw [map_inv₀] field_simp ring variable {w} in private theorem HasValueAt.div {f g : F} {a b : K} (hf : w.HasValueAt f a) (hg : w.HasValueAt g b) (hb : b ≠ 0) : w.HasValueAt (f / g) (a / b) := by rw [div_eq_mul_inv, div_eq_mul_inv] exact hf.mul (hg.inv hb) private theorem hasValueAt_iff_residue {f : F} (hf : f ∈ w.toValuationSubring) (a : K) : w.HasValueAt f a ↔ residue w.toValuationSubring ⟨f, hf⟩ = algebraMap K w.ResidueField a := by have e : algebraMap K w.ResidueField a = residue w.toValuationSubring (algebraMap K w.toValuationSubring a) := rfl rw [e, ← sub_eq_zero, ← map_sub, residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff] rfl private theorem exists_hasValueAt (hw : Function.Surjective (algebraMap K w.ResidueField)) {f : F} (hf : f ∈ w.toValuationSubring) : ∃ a : K, w.HasValueAt f a := by obtain ⟨a, ha⟩ := hw (residue w.toValuationSubring ⟨f, hf⟩) exact ⟨a, (w.hasValueAt_iff_residue hf a).mpr ha.symm⟩ private theorem surjective_algebraMap_residueField_of_isAlgClosed [IsAlgClosed K] [Module.Finite K w.ResidueField] : Function.Surjective (algebraMap K w.ResidueField) := haveI : Algebra.IsIntegral K w.ResidueField := Algebra.IsIntegral.of_finite K w.ResidueField (IsAlgClosed.algebraMap_bijective_of_isIntegral (k := K) (K := w.ResidueField)).2 private theorem surjective_algebraMap_residueField_of_deg_eq_one [IsAlgClosed K] (h : w.deg = 1) : Function.Surjective (algebraMap K w.ResidueField) := haveI : Module.Finite K w.ResidueField := Module.finite_of_finrank_eq_succ (n := 0) h w.surjective_algebraMap_residueField_of_isAlgClosed variable (A : ValuationSubring K) private def compSubring : Subring F where carrier := {f | ∃ a : A, w.HasValueAt f a} mul_mem' := by rintro f g ⟨a, ha⟩ ⟨b, hb⟩ exact ⟨a * b, by simpa using ha.mul hb⟩ one_mem' := ⟨1, by simpa using w.hasValueAt_algebraMap 1⟩ add_mem' := by rintro f g ⟨a, ha⟩ ⟨b, hb⟩ exact ⟨a + b, by simpa using ha.add hb⟩ zero_mem' := ⟨0, by simpa using w.hasValueAt_algebraMap 0⟩ neg_mem' := by rintro f ⟨a, ha⟩ exact ⟨-a, by simpa using ha.neg⟩ variable {A} in private theorem mem_compSubring_iff {f : F} : f ∈ w.compSubring A ↔ ∃ a : A, w.HasValueAt f a := Iff.rfl variable {A} in private theorem mem_compSubring_of_hasValueAt {f : F} {a : K} (ha : a ∈ A) (h : w.HasValueAt f a) : f ∈ w.compSubring A := ⟨⟨a, ha⟩, h⟩ private theorem compSubring_le : w.compSubring A ≤ w.toValuationSubring.toSubring := by rintro f ⟨a, ha⟩ exact w.mem_of_hasValueAt ha private theorem mem_compSubring_of_mem_nonunits {f : F} (hf : f ∈ w.toValuationSubring.nonunits) : f ∈ w.compSubring A := ⟨0, by simpa [w.hasValueAt_zero_iff] using hf⟩ private theorem algebraMap_mem_compSubring_iff (a : K) : algebraMap K F a ∈ w.compSubring A ↔ a ∈ A := by constructor · rintro ⟨b, hb⟩ rw [(w.hasValueAt_algebraMap a).unique hb] exact b.2 · intro ha exact ⟨⟨a, ha⟩, w.hasValueAt_algebraMap a⟩ private def value : w.compSubring A →+* A where toFun f := Classical.choose f.2 map_one' := Subtype.ext <| (Classical.choose_spec (w.compSubring A).one_mem).unique (by simpa using w.hasValueAt_algebraMap 1) map_mul' f g := Subtype.ext <| (Classical.choose_spec (mul_mem f.2 g.2)).unique (by simpa using (Classical.choose_spec f.2).mul (Classical.choose_spec g.2)) map_zero' := Subtype.ext <| (Classical.choose_spec (w.compSubring A).zero_mem).unique (by simpa using w.hasValueAt_algebraMap 0) map_add' f g := Subtype.ext <| (Classical.choose_spec (add_mem f.2 g.2)).unique (by simpa using (Classical.choose_spec f.2).add (Classical.choose_spec g.2)) private theorem hasValueAt_value (f : w.compSubring A) : w.HasValueAt (f : F) (w.value A f : K) := Classical.choose_spec f.2 variable {A} in private theorem value_eq_of_hasValueAt {f : w.compSubring A} {a : A} (h : w.HasValueAt (f : F) a) : w.value A f = a := Subtype.ext ((w.hasValueAt_value A f).unique h) variable {A} in private theorem ord_sub_value_pos {f : w.compSubring A} (hf : (f : F) ≠ algebraMap K F (w.value A f)) : 0 < w.ord ((f : F) - algebraMap K F (w.value A f)) := (w.hasValueAt_iff_ord_pos hf).mp (w.hasValueAt_value A f) variable {A} in private theorem value_eq_of_ord_pos {f : w.compSubring A} {a : A} (h : 0 < w.ord ((f : F) - algebraMap K F a)) : w.value A f = a := w.value_eq_of_hasValueAt (w.hasValueAt_of_ord_pos h) private theorem value_algebraMap (a : A) : w.value A ⟨algebraMap K F a, (w.algebraMap_mem_compSubring_iff A a).mpr a.2⟩ = a := w.value_eq_of_hasValueAt (w.hasValueAt_algebraMap (a : K)) private theorem value_surjective : Function.Surjective (w.value A) := fun a => ⟨_, w.value_algebraMap A a⟩ variable {A} in private theorem value_eq_zero_of_mem_nonunits {f : w.compSubring A} (hf : (f : F) ∈ w.toValuationSubring.nonunits) : w.value A f = 0 := w.value_eq_of_hasValueAt (by simpa [w.hasValueAt_zero_iff] using hf) private def centre : Ideal (w.compSubring A) := (maximalIdeal A).comap (w.value A) private instance centre_isPrime : (w.centre A).IsPrime := Ideal.comap_isPrime _ _ private instance centre_isMaximal : (w.centre A).IsMaximal := Ideal.comap_isMaximal_of_surjective _ (w.value_surjective A) variable {A} in private theorem mem_centre_iff (f : w.compSubring A) : f ∈ w.centre A ↔ w.value A f ∈ maximalIdeal A := Iff.rfl variable {A} in private theorem mem_centre_iff_of_hasValueAt {f : w.compSubring A} {a : A} (h : w.HasValueAt (f : F) a) : f ∈ w.centre A ↔ a ∈ maximalIdeal A := by rw [mem_centre_iff, w.value_eq_of_hasValueAt h] variable {A} in private theorem mem_centre_iff_of_ord_pos {f : w.compSubring A} {a : A} (h : 0 < w.ord ((f : F) - algebraMap K F a)) : f ∈ w.centre A ↔ a ∈ maximalIdeal A := w.mem_centre_iff_of_hasValueAt (w.hasValueAt_of_ord_pos h) variable {A} in private theorem mem_centre_of_mem_nonunits {f : w.compSubring A} (hf : (f : F) ∈ w.toValuationSubring.nonunits) : f ∈ w.centre A := by rw [mem_centre_iff, w.value_eq_zero_of_mem_nonunits hf] exact Ideal.zero_mem _ variable {A} in private theorem mem_centre_of_ord_pos {f : w.compSubring A} (hf : 0 < w.ord (f : F)) : f ∈ w.centre A := w.mem_centre_of_mem_nonunits ((w.mem_nonunits_iff_ord_pos (by rintro h; simp [h] at hf)).mpr hf) private theorem algebraMap_mem_centre_iff (a : A) : (⟨algebraMap K F a, (w.algebraMap_mem_compSubring_iff A a).mpr a.2⟩ : w.compSubring A) ∈ w.centre A ↔ a ∈ maximalIdeal A := by rw [mem_centre_iff, value_algebraMap] private theorem mem_compSubring_or_inv_mem (hw : Function.Surjective (algebraMap K w.ResidueField)) (f : F) : f ∈ w.compSubring A ∨ f⁻¹ ∈ w.compSubring A := by by_cases hf : f ∈ w.toValuationSubring · obtain ⟨c, hc⟩ := w.exists_hasValueAt hw hf by_cases hcA : c ∈ A · exact Or.inl ⟨⟨c, hcA⟩, hc⟩ · right have hcA' : c⁻¹ ∈ A := (A.mem_or_inv_mem c).resolve_left hcA have hc0 : c ≠ 0 := fun h => hcA (h ▸ A.zero_mem) have hf0 : f ≠ 0 := by rintro rfl have : w.HasValueAt (0 : F) 0 := by simpa using w.hasValueAt_algebraMap 0 exact hc0 (hc.unique this) have hfu : f ∉ w.toValuationSubring.nonunits := by intro hfn exact hc0 (hc.unique ((w.hasValueAt_zero_iff f).mpr hfn)) have hfinv : f⁻¹ ∈ w.toValuationSubring := by by_contra hne exact hfu ((ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inr (by simpa using hne))) refine ⟨⟨c⁻¹, hcA'⟩, ?_⟩ have hprod : (f - algebraMap K F c) * (f⁻¹ * algebraMap K F c⁻¹) ∈ w.toValuationSubring.nonunits := w.mul_mem_nonunits hc (mul_mem hfinv (w.algebraMap_mem _)) have := neg_mem hprod show f⁻¹ - algebraMap K F (c⁻¹ : K) ∈ w.toValuationSubring.nonunits convert this using 1 have hcF : algebraMap K F c ≠ 0 := by simpa using hc0 rw [map_inv₀] field_simp ring · right refine w.mem_compSubring_of_mem_nonunits A ?_ exact (ValuationSubring.inv_mem_nonunits_iff _).mpr (Or.inr hf) private def compValuationSubring (hw : Function.Surjective (algebraMap K w.ResidueField)) : ValuationSubring F := ValuationSubring.ofSubring (w.compSubring A) (w.mem_compSubring_or_inv_mem A hw) @[simp] private theorem compValuationSubring_toSubring (hw : Function.Surjective (algebraMap K w.ResidueField)) : (w.compValuationSubring A hw).toSubring = w.compSubring A := rfl private theorem mem_compValuationSubring_iff (hw : Function.Surjective (algebraMap K w.ResidueField)) (f : F) : f ∈ w.compValuationSubring A hw ↔ f ∈ w.compSubring A := Iff.rfl private theorem mem_compSubring_of_isIntegral (hw : Function.Surjective (algebraMap K w.ResidueField)) {S : Subring F} (hS : S ≤ w.compSubring A) {f : F} (hf : IsIntegral S f) : f ∈ w.compSubring A := by obtain ⟨p, hp, hpf⟩ := hf let V := w.compValuationSubring A hw let i : S →+* V := Subring.inclusion hS have hint : IsIntegral V f := by refine ⟨p.map i, hp.map i, ?_⟩ rw [Polynomial.eval₂_map] exact hpf obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint rw [← hy] exact y.2 private theorem mem_compSubring_of_isIntegral' [IsAlgClosed K] {S : Subring F} (hS : S ≤ w.compSubring A) {f : F} (hf : IsIntegral S f) : f ∈ w.compSubring A := by obtain ⟨p, hp, hpf⟩ := hf have hSO : ∀ s : S, (s : F) ∈ w.toValuationSubring := fun s => w.compSubring_le A (hS s.2) have hfO : f ∈ w.toValuationSubring := by refine w.mem_of_eval_monic_eq_zero (P := p.map S.subtype) (hp.map _) (fun i => ?_) ?_ · rw [Polynomial.coeff_map] exact hSO _ · rw [Polynomial.eval_map] exact hpf let vS : S →+* A := (w.value A).comp (Subring.inclusion hS) let ιS : S →+* w.toValuationSubring := S.subtype.codRestrict _ hSO have hres : (residue w.toValuationSubring).comp ιS = ((algebraMap K w.ResidueField).comp (algebraMap A K)).comp vS := by ext s change residue w.toValuationSubring ⟨s, hSO s⟩ = algebraMap K w.ResidueField ((w.value A ⟨s, hS s.2⟩ : A) : K) exact (w.hasValueAt_iff_residue (hSO s) _).mp (w.hasValueAt_value A ⟨s, hS s.2⟩) set r : w.ResidueField := residue w.toValuationSubring ⟨f, hfO⟩ with hr let Q : Polynomial A := p.map vS have hQ : Q.Monic := hp.map _ have hzero : Polynomial.eval₂ ιS ⟨f, hfO⟩ p = 0 := by apply Subtype.val_injective change w.toValuationSubring.subtype (Polynomial.eval₂ ιS ⟨f, hfO⟩ p) = ((0 : w.toValuationSubring) : F) rw [Polynomial.hom_eval₂] exact hpf have hrootκ : Polynomial.eval₂ (algebraMap K w.ResidueField) r (Q.map (algebraMap A K)) = 0 := by rw [Polynomial.eval₂_map, Polynomial.eval₂_map, ← hres, hr, ← Polynomial.hom_eval₂, hzero, map_zero] have hint : IsIntegral K r := ⟨Q.map (algebraMap A K), hQ.map _, hrootκ⟩ obtain ⟨c, hc⟩ : r ∈ (algebraMap K w.ResidueField).range := minpoly.mem_range_of_degree_eq_one K r (IsAlgClosed.degree_eq_one_of_irreducible K (minpoly.irreducible hint)) have hcroot : Polynomial.eval₂ (algebraMap A K) c Q = 0 := by apply (algebraMap K w.ResidueField).injective rw [Polynomial.hom_eval₂, ← Polynomial.eval₂_map, hc, hrootκ, map_zero] obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp (⟨Q, hQ, hcroot⟩ : IsIntegral A c) refine ⟨y, (w.hasValueAt_iff_residue hfO _).mpr ?_⟩ rw [← hr, ← hc, ← hy] rfl private theorem exists_unique_valueHom [IsAlgClosed K] (g : F) (B₀ : Subring F) (hint : ∀ b : B₀, ∃ p : Polynomial (Subring.closure (algebraMap K F '' (A : Set K) ∪ {g})), p.Monic ∧ Polynomial.eval₂ (Subring.closure (algebraMap K F '' (A : Set K) ∪ {g})).subtype (b : F) p = 0) (hw : ∃ a : A, g - algebraMap K F (a : K) ∈ w.toValuationSubring.nonunits) : ∃! φ : B₀ →+* A, ∀ b : B₀, (b : F) - algebraMap K F ((φ b : A) : K) ∈ w.toValuationSubring.nonunits := by obtain ⟨a₀, ha₀⟩ := hw have hg : g ∈ w.compSubring A := w.mem_compSubring_of_hasValueAt a₀.2 ha₀ have hS : Subring.closure (algebraMap K F '' (A : Set K) ∪ {g}) ≤ w.compSubring A := by rw [Subring.closure_le] rintro y (⟨c, hc, rfl⟩ | rfl) · exact (w.algebraMap_mem_compSubring_iff A c).mpr hc · exact hg have hB₀ : B₀ ≤ w.compSubring A := fun b hb => w.mem_compSubring_of_isIntegral' A hS (hint ⟨b, hb⟩) refine ⟨(w.value A).comp (Subring.inclusion hB₀), fun b => w.hasValueAt_value A ⟨b, hB₀ b.2⟩, ?_⟩ intro ψ hψ refine RingHom.ext fun b => ?_ have h1 : w.HasValueAt (b : F) ((ψ b : A) : K) := hψ b have h2 : ψ b = w.value A ⟨b, hB₀ b.2⟩ := Subtype.ext (h1.unique (w.hasValueAt_value A ⟨b, hB₀ b.2⟩)) exact h2 variable {A} in private theorem residue_comp_value_surjective {B : Subring F} (hB : B ≤ w.compSubring A) (hconst : ∀ a : A, algebraMap K F a ∈ B) : Function.Surjective (((IsLocalRing.residue A).comp (w.value A)).comp (Subring.inclusion hB)) := by intro x obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective x refine ⟨⟨algebraMap K F a, hconst a⟩, ?_⟩ change IsLocalRing.residue A (w.value A ⟨algebraMap K F a, hB (hconst a)⟩) = _ rw [w.value_eq_of_hasValueAt (w.hasValueAt_algebraMap (a : K))] variable {A} in private theorem ker_residue_comp_value {B : Subring F} (hB : B ≤ w.compSubring A) : RingHom.ker (((IsLocalRing.residue A).comp (w.value A)).comp (Subring.inclusion hB)) = (w.centre A).comap (Subring.inclusion hB) := by ext b rw [RingHom.mem_ker, Ideal.mem_comap, mem_centre_iff, RingHom.comp_apply, RingHom.comp_apply, IsLocalRing.residue_eq_zero_iff] variable {A} in private theorem centre_comap_isMaximal {B : Subring F} (hB : B ≤ w.compSubring A) (hconst : ∀ a : A, algebraMap K F a ∈ B) : ((w.centre A).comap (Subring.inclusion hB)).IsMaximal := by rw [← w.ker_residue_comp_value hB] exact RingHom.ker_isMaximal_of_surjective _ (w.residue_comp_value_surjective hB hconst) variable {A} in private theorem sub_value_mem_centre_comap {B : Subring F} (hB : B ≤ w.compSubring A) (hconst : ∀ a : A, algebraMap K F a ∈ B) (b : B) : b - ⟨algebraMap K F (w.value A ⟨b, hB b.2⟩ : K), hconst _⟩ ∈ (w.centre A).comap (Subring.inclusion hB) := by rw [Ideal.mem_comap, mem_centre_iff] simp only [map_sub] have h1 : w.value A (Subring.inclusion hB ⟨algebraMap K F (w.value A ⟨b, hB b.2⟩ : K), hconst _⟩) = w.value A ⟨b, hB b.2⟩ := w.value_eq_of_hasValueAt (w.hasValueAt_algebraMap _) have h2 : w.value A (Subring.inclusion hB b) = w.value A ⟨b, hB b.2⟩ := rfl rw [h1, h2, sub_self] exact Ideal.zero_mem _ variable {A} in private theorem algebraMap_mem_centre_comap_iff {B : Subring F} (hB : B ≤ w.compSubring A) (hconst : ∀ a : A, algebraMap K F a ∈ B) (a : A) : (⟨algebraMap K F a, hconst a⟩ : B) ∈ (w.centre A).comap (Subring.inclusion hB) ↔ a ∈ maximalIdeal A := by rw [Ideal.mem_comap] exact w.algebraMap_mem_centre_iff A a end Place end AlgebraicCurve set_option autoImplicit false namespace ValuationSubring variable {K : Type*} [Field K] (A : ValuationSubring K) private theorem algebraMap_bijective_of_isIntegral_of_isAlgClosed [IsAlgClosed K] (R : Type*) [CommRing R] [IsDomain R] [Algebra A R] [FaithfulSMul A R] [Algebra.IsIntegral A R] : Function.Bijective (algebraMap A R) := by have hinj : Function.Injective (algebraMap A R) := FaithfulSMul.algebraMap_injective A R refine ⟨hinj, fun r => ?_⟩ haveI : Algebra.IsAlgebraic A R := Algebra.IsIntegral.isAlgebraic let φ : R →ₐ[A] K := IsAlgClosed.lift have hφ : Function.Injective φ := by rw [injective_iff_map_eq_zero] intro x hx have hker : RingHom.ker φ.toRingHom = ⊥ := by refine Ideal.eq_bot_of_comap_eq_bot (R := A) ?_ rw [eq_bot_iff] intro a ha rw [Ideal.mem_comap, RingHom.mem_ker] at ha change φ (algebraMap A R a) = 0 at ha rw [AlgHom.commutes] at ha have h0 : (a : K) = 0 := ha have ha0 : a = 0 := by exact_mod_cast h0 rw [ha0] exact Ideal.zero_mem _ have hmem : x ∈ RingHom.ker φ.toRingHom := hx rw [hker] at hmem exact Ideal.mem_bot.mp hmem have hint : IsIntegral A (φ r) := (Algebra.IsIntegral.isIntegral (R := A) r).map φ obtain ⟨a, ha⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint refine ⟨a, hφ ?_⟩ rw [AlgHom.commutes, ha] section Quotient open Polynomial variable {F : Type*} [Field F] [Algebra K F] private abbrev constants : A →+* F := (algebraMap K F).comp A.subtype variable {A} private theorem exists_sub_constants_mem [IsAlgClosed K] {x : F} {B : Subring F} (hconst : ∀ a : A, A.constants a ∈ B) (hxB : x ∈ B) (hint : ∀ b : B, IsIntegral (Subring.closure (Set.range (A.constants (F := F)) ∪ {x})) (b : F)) (𝔭 : Ideal B) [𝔭.IsPrime] (hbot : ∀ a : A, (⟨A.constants a, hconst a⟩ : B) ∈ 𝔭 → a = 0) (a₀ : A) (hx : (⟨x, hxB⟩ : B) - ⟨A.constants a₀, hconst a₀⟩ ∈ 𝔭) (b : B) : ∃ a : A, b - ⟨A.constants a, hconst a⟩ ∈ 𝔭 := by classical set S : Subring F := Subring.closure (Set.range (A.constants (F := F)) ∪ {x}) with hS have hSB : S ≤ B := by rw [hS, Subring.closure_le] rintro y (⟨a, rfl⟩ | rfl) exacts [hconst a, hxB] let cB : A →+* B := (A.constants (F := F)).codRestrict B hconst letI alg : Algebra A (B ⧸ 𝔭) := ((Ideal.Quotient.mk 𝔭).comp cB).toAlgebra have halg : ∀ a : A, algebraMap A (B ⧸ 𝔭) a = Ideal.Quotient.mk 𝔭 (cB a) := fun _ => rfl let ψ : S →+* B ⧸ 𝔭 := (Ideal.Quotient.mk 𝔭).comp (Subring.inclusion hSB) have step1 : ∀ (y : F) (hy : y ∈ S), ψ ⟨y, hy⟩ ∈ (algebraMap A (B ⧸ 𝔭)).range := by intro y hy induction hy using Subring.closure_induction with | mem y hy => rcases hy with ⟨a, rfl⟩ | h · exact ⟨a, rfl⟩ · have h' : x = y := (Set.mem_singleton_iff.mp h).symm subst h' refine ⟨a₀, ?_⟩ rw [halg] change Ideal.Quotient.mk 𝔭 (cB a₀) = Ideal.Quotient.mk 𝔭 ⟨x, hxB⟩ rw [Ideal.Quotient.eq] have := 𝔭.neg_mem hx rwa [neg_sub] at this | zero => change ψ 0 ∈ _ rw [map_zero] exact Subring.zero_mem _ | one => change ψ 1 ∈ _ rw [map_one] exact Subring.one_mem _ | add y z hy hz ihy ihz => change ψ (⟨y, hy⟩ + ⟨z, hz⟩) ∈ _ rw [map_add] exact Subring.add_mem _ ihy ihz | neg y hy ihy => change ψ (-⟨y, hy⟩) ∈ _ rw [map_neg] exact Subring.neg_mem _ ihy | mul y z hy hz ihy ihz => change ψ (⟨y, hy⟩ * ⟨z, hz⟩) ∈ _ rw [map_mul] exact Subring.mul_mem _ ihy ihz have step1' : ∀ s : S, ψ s ∈ (algebraMap A (B ⧸ 𝔭)).range := fun s => step1 s s.2 haveI hintq : Algebra.IsIntegral A (B ⧸ 𝔭) := by refine ⟨fun y => ?_⟩ obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective y obtain ⟨f, hf, hfb⟩ := hint b set g : Polynomial B := f.map (Subring.inclusion hSB) with hg have hgm : g.Monic := hf.map _ have hgb : g.eval b = 0 := by apply Subtype.val_injective change B.subtype (eval b (f.map (Subring.inclusion hSB))) = ((0 : B) : F) rw [eval_map, hom_eval₂] exact hfb set gq : Polynomial (B ⧸ 𝔭) := g.map (Ideal.Quotient.mk 𝔭) with hgq have hgqm : gq.Monic := hgm.map _ have hgqb : gq.eval (Ideal.Quotient.mk 𝔭 b) = 0 := by rw [hgq, eval_map, eval₂_hom, hgb, map_zero] have hlifts : gq ∈ Polynomial.lifts (algebraMap A (B ⧸ 𝔭)) := by rw [lifts_iff_coeff_lifts] intro n rw [hgq, coeff_map, hg, coeff_map] exact step1' (f.coeff n) obtain ⟨q, hqmap, -, hqm⟩ := lifts_and_degree_eq_and_monic hlifts hgqm refine ⟨q, hqm, ?_⟩ rw [← eval_map, hqmap, hgqb] haveI : FaithfulSMul A (B ⧸ 𝔭) := by rw [faithfulSMul_iff_algebraMap_injective, injective_iff_map_eq_zero] intro a ha rw [halg, Ideal.Quotient.eq_zero_iff_mem] at ha exact hbot a ha obtain ⟨a, ha⟩ := (A.algebraMap_bijective_of_isIntegral_of_isAlgClosed (B ⧸ 𝔭)).2 (Ideal.Quotient.mk 𝔭 b) refine ⟨a, ?_⟩ rw [halg, Ideal.Quotient.eq] at ha have := 𝔭.neg_mem ha rwa [neg_sub] at this private theorem constants_unique_mod {B : Subring F} (hconst : ∀ a : A, A.constants a ∈ B) (𝔭 : Ideal B) (hbot : ∀ a : A, (⟨A.constants a, hconst a⟩ : B) ∈ 𝔭 → a = 0) {a c : A} (h : (⟨A.constants a, hconst a⟩ : B) - ⟨A.constants c, hconst c⟩ ∈ 𝔭) : a = c := by have : (⟨A.constants (a - c), hconst (a - c)⟩ : B) ∈ 𝔭 := by convert h using 1 apply Subtype.ext push_cast rw [map_sub] exact sub_eq_zero.mp (hbot _ this) end Quotient end ValuationSubring set_option autoImplicit false noncomputable section open IsLocalRing IsDedekindDomain namespace Subring variable {F : Type*} [Field F] {B : Subring F} private theorem exists_valuationSubring_dominating (𝔭 : Ideal B) [𝔭.IsPrime] : ∃ O : ValuationSubring F, B ≤ O.toSubring ∧ ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭 := by let L := Localization.AtPrime 𝔭 have hunit : ∀ y : 𝔭.primeCompl, IsUnit (B.subtype y) := by intro y refine isUnit_iff_ne_zero.mpr fun h => y.2 ?_ have : (y : B) = 0 := Subtype.ext h rw [this] exact 𝔭.zero_mem let f : L →+* F := IsLocalization.lift hunit have hf : ∀ b : B, f (algebraMap B L b) = b := fun b => IsLocalization.lift_eq hunit b obtain ⟨O, hO, hloc⟩ := IsLocalRing.exists_factor_valuationRing f refine ⟨O, fun b hb => ?_, fun b => ?_⟩ · have := hO (algebraMap B L ⟨b, hb⟩) rwa [hf] at this · let z : O := ⟨f (algebraMap B L b), hO _⟩ have hz : f.codRestrict O.toSubring hO (algebraMap B L b) = z := rfl have key : IsUnit z ↔ b ∉ 𝔭 := by rw [← hz, isUnit_map_iff (f.codRestrict O.toSubring hO), IsLocalization.AtPrime.isUnit_to_map_iff L 𝔭 b] rfl have hzF : (z : F) = b := hf b rw [← hzF, ValuationSubring.coe_mem_nonunits_iff, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, key, not_not] private theorem ne_top_of_dominating {𝔭 : Ideal B} {O : ValuationSubring F} (hdom : ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭) (h𝔭 : 𝔭 ≠ ⊥) : O ≠ ⊤ := by intro htop apply h𝔭 rw [eq_bot_iff] intro b hb have hn : (b : F) ∈ O.nonunits := (hdom b).mpr hb rcases (ValuationSubring.mem_nonunits_iff_or _).mp hn with h0 | hinv · exact (Ideal.mem_bot).mpr (Subtype.ext h0) · exact absurd (htop ▸ ValuationSubring.mem_top _) hinv private theorem algebraMap_mem_of_dominating {K : Type*} [Field K] [Algebra K F] (A : ValuationSubring K) (hconst : ∀ a : A, algebraMap K F a ∈ B) {𝔭 : Ideal B} {O : ValuationSubring F} (hle : B ≤ O.toSubring) (hdom : ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭) (hbot : ∀ a : A, (⟨algebraMap K F a, hconst a⟩ : B) ∈ 𝔭 → a = 0) (c : K) : algebraMap K F c ∈ O := by by_cases hc : c ∈ A · exact hle (hconst ⟨c, hc⟩) · have hcinv : c⁻¹ ∈ A := (A.mem_or_inv_mem c).resolve_left hc have hc0 : c ≠ 0 := fun h => hc (h ▸ A.zero_mem) have hnot : (⟨algebraMap K F (c⁻¹ : K), hconst ⟨c⁻¹, hcinv⟩⟩ : B) ∉ 𝔭 := fun h => inv_ne_zero hc0 (by simpa using congrArg Subtype.val (hbot ⟨c⁻¹, hcinv⟩ h)) have hnu : algebraMap K F c⁻¹ ∉ O.nonunits := fun h => hnot ((hdom _).mp h) rw [map_inv₀, ValuationSubring.inv_mem_nonunits_iff, not_or] at hnu exact not_not.mp hnu.2 end Subring namespace ValuationSubring variable {F : Type*} [Field F] variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F] variable (O : ValuationSubring F) private def centreOver (hO : ∀ r : R, algebraMap R F r ∈ O) : Ideal R := (IsLocalRing.maximalIdeal O).comap ((algebraMap R F).codRestrict O.toSubring hO) private instance centreOver_isPrime (hO : ∀ r : R, algebraMap R F r ∈ O) : (O.centreOver hO).IsPrime := Ideal.comap_isPrime _ _ omit [IsDedekindDomain R] [IsFractionRing R F] in private theorem mem_centreOver_iff (hO : ∀ r : R, algebraMap R F r ∈ O) {r : R} : r ∈ O.centreOver hO ↔ algebraMap R F r ∈ O.nonunits := by rw [centreOver, Ideal.mem_comap, ← ValuationSubring.coe_mem_nonunits_iff] rfl omit [IsDedekindDomain R] [IsFractionRing R F] in private theorem inv_algebraMap_mem (hO : ∀ r : R, algebraMap R F r ∈ O) {s : R} (hs : s ∉ O.centreOver hO) : (algebraMap R F s)⁻¹ ∈ O := by rw [mem_centreOver_iff, ValuationSubring.mem_nonunits_iff, not_lt] at hs have hy : O.valuation (algebraMap R F s) ≤ 1 := (O.valuation_le_one_iff _).mpr (hO s) have h1 : O.valuation (algebraMap R F s) = 1 := le_antisymm hy hs apply (O.valuation_le_one_iff _).mp rw [map_inv₀, h1, inv_one] private theorem centreOver_ne_bot (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) : O.centreOver hO ≠ ⊥ := by intro hbot apply hne refine SetLike.ext fun x => ⟨fun _ => ValuationSubring.mem_top x, fun _ => ?_⟩ obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective (A := R) x rw [div_eq_mul_inv] refine O.mul_mem _ _ (hO a) (O.inv_algebraMap_mem hO fun hmem => ?_) rw [hbot, Ideal.mem_bot] at hmem exact nonZeroDivisors.ne_zero hb hmem private def centreHeightOneSpectrum (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) : HeightOneSpectrum R := ⟨O.centreOver hO, inferInstance, O.centreOver_ne_bot hO hne⟩ private theorem valuationSubringAtPrime_centre_le (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) : HeightOneSpectrum.valuationSubringAtPrime F (O.centreHeightOneSpectrum hO hne) ≤ O := by rintro x ⟨a, s, hs, rfl⟩ exact O.mul_mem _ _ (hO a) (O.inv_algebraMap_mem hO hs) private theorem eq_valuationSubringAtPrime_centre (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) : O = HeightOneSpectrum.valuationSubringAtPrime F (O.centreHeightOneSpectrum hO hne) := (ValuationSubring.eq_of_le_of_ne_top _ (O.valuationSubringAtPrime_centre_le hO hne) hne).symm private theorem isPrincipalIdealRing_of_dedekind_le (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) : IsPrincipalIdealRing O := by rw [O.eq_valuationSubringAtPrime_centre hO hne] infer_instance end ValuationSubring namespace AlgebraicCurve namespace Place variable {K F : Type*} [Field K] [Field F] [Algebra K F] variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F] private def ofValuationSubringOver (O : ValuationSubring F) (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) (hK : ∀ c : K, algebraMap K F c ∈ O) : Place K F where toValuationSubring := O algebraMap_mem' := hK ne_top' := hne isPrincipalIdealRing' := O.isPrincipalIdealRing_of_dedekind_le hO hne @[simp] private theorem ofValuationSubringOver_toValuationSubring (O : ValuationSubring F) (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) (hK : ∀ c : K, algebraMap K F c ∈ O) : (ofValuationSubringOver O hO hne hK).toValuationSubring = O := rfl private theorem mem_nonunits_ofValuationSubringOver_iff (O : ValuationSubring F) (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) (hK : ∀ c : K, algebraMap K F c ∈ O) {B : Subring F} {𝔭 : Ideal B} (hdom : ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭) (b : B) : (b : F) ∈ (ofValuationSubringOver O hO hne hK).toValuationSubring.nonunits ↔ b ∈ 𝔭 := hdom b end Place end AlgebraicCurve set_option autoImplicit false open IsLocalRing Polynomial namespace Valuation variable {R Γ₀ : Type*} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] private theorem exists_ne_map_eq_of_sum_eq_zero {ι : Type*} [DecidableEq ι] (v : Valuation R Γ₀) {s : Finset ι} {f : ι → R} (hs : ∑ i ∈ s, f i = 0) {j : ι} (hj : j ∈ s) (hj0 : v (f j) ≠ 0) (hmax : ∀ i ∈ s, v (f i) ≤ v (f j)) : ∃ i ∈ s, i ≠ j ∧ v (f i) = v (f j) := by by_contra h push Not at h have hlt : ∀ i ∈ s \ {j}, v (f i) < v (f j) := by intro i hi rw [Finset.mem_sdiff, Finset.mem_singleton] at hi exact lt_of_le_of_ne (hmax i hi.1) (h i hi.1 hi.2) have := v.map_sum_eq_of_lt hj hlt rw [hs, map_zero] at this exact hj0 this.symm end Valuation namespace ValuationSubring variable {K : Type*} [Field K] (A : ValuationSubring K) variable {k : Type*} [Field k] private theorem natCast_mem_ker (ℓ : ℕ) [CharP k ℓ] (red : A →+* k) : ((ℓ : ℕ) : A) ∈ RingHom.ker red := by rw [RingHom.mem_ker, map_natCast, CharP.cast_eq_zero] private theorem natCast_mem_maximalIdeal (ℓ : ℕ) [CharP k ℓ] (red : A →+* k) : ((ℓ : ℕ) : A) ∈ maximalIdeal A := IsLocalRing.le_maximalIdeal (RingHom.ker_ne_top red) (A.natCast_mem_ker ℓ red) private theorem isUnit_intCast_of_not_dvd (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) {m : ℤ} (hm : ¬ (ℓ : ℤ) ∣ m) : IsUnit ((m : ℤ) : A) := by have hprime : Prime (ℓ : ℤ) := Nat.prime_iff_prime_int.mp Fact.out obtain ⟨a, b, hab⟩ := (Irreducible.coprime_iff_not_dvd hprime.irreducible).mpr hm have hA : (a : A) * ((ℓ : ℕ) : A) + (b : A) * (m : A) = 1 := by have := congrArg (Int.cast : ℤ → A) hab push_cast at this exact this have hℓm : (a : A) * ((ℓ : ℕ) : A) ∈ maximalIdeal A := Ideal.mul_mem_left _ _ (A.natCast_mem_maximalIdeal ℓ red) have hu : IsUnit ((b : A) * (m : A)) := by by_contra hnu have hmem : (b : A) * (m : A) ∈ maximalIdeal A := (IsLocalRing.mem_maximalIdeal _).mpr hnu have h1 : (1 : A) ∈ maximalIdeal A := hA ▸ Ideal.add_mem _ hℓm hmem exact (IsLocalRing.maximalIdeal.isMaximal A).ne_top (Ideal.eq_top_of_isUnit_mem _ h1 isUnit_one) exact isUnit_of_mul_isUnit_right hu private theorem map_intCast_eq_zero_of_not_isUnit (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) {m : ℤ} (hm : ¬ IsUnit ((m : ℤ) : A)) : red (m : A) = 0 := by have hdvd : (ℓ : ℤ) ∣ m := by by_contra h exact hm (A.isUnit_intCast_of_not_dvd ℓ red h) obtain ⟨c, rfl⟩ := hdvd rw [map_intCast] push_cast rw [CharP.cast_eq_zero k ℓ, zero_mul] private theorem map_eq_zero_of_rat_mem_maximalIdeal (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) (φ : ℚ →+* K) (r : ℚ) (hrA : φ r ∈ A) (hr : (⟨φ r, hrA⟩ : A) ∈ maximalIdeal A) : red ⟨φ r, hrA⟩ = 0 := by have hnum : (⟨φ r, hrA⟩ : A) * ((r.den : ℕ) : A) = ((r.num : ℤ) : A) := by apply Subtype.ext change φ r * (((r.den : ℕ) : A) : K) = (((r.num : ℤ) : A) : K) push_cast rw [← map_natCast φ, ← map_intCast φ, ← map_mul, Rat.mul_den_eq_num] have hnum_mem : ((r.num : ℤ) : A) ∈ maximalIdeal A := hnum ▸ Ideal.mul_mem_right _ _ hr have hnum0 : red ((r.num : ℤ) : A) = 0 := A.map_intCast_eq_zero_of_not_isUnit ℓ red ((IsLocalRing.mem_maximalIdeal _).mp hnum_mem) have hden : ¬ (ℓ : ℤ) ∣ (r.den : ℤ) := by intro h have hℓnum : (ℓ : ℤ) ∣ r.num := by by_contra h' have hu : IsUnit ((r.num : ℤ) : A) := A.isUnit_intCast_of_not_dvd ℓ red h' exact (IsLocalRing.mem_maximalIdeal _).mp hnum_mem hu have h1 : (ℓ : ℤ) ∣ (Int.gcd r.num (r.den : ℤ) : ℤ) := Int.dvd_coe_gcd hℓnum h have hg : Int.gcd r.num (r.den : ℤ) = 1 := by simpa [Int.gcd, Int.natAbs_natCast] using r.reduced rw [hg] at h1 have := Int.eq_one_of_dvd_one (by positivity) h1 have hℓ1 : ℓ = 1 := by exact_mod_cast this exact (Fact.out : ℓ.Prime).one_lt.ne' hℓ1 have hden0 : red ((r.den : ℕ) : A) ≠ 0 := by rw [map_natCast] intro h0 rw [CharP.cast_eq_zero_iff k ℓ] at h0 exact hden (by exact_mod_cast h0) have := congrArg red hnum rw [map_mul, hnum0] at this exact (mul_eq_zero.mp this).resolve_right hden0 private theorem exists_pow_valuation_eq_of_isRoot (φ : ℚ →+* K) {x : K} (hx0 : x ≠ 0) {p : ℚ[X]} (hp0 : p ≠ 0) (hpx : p.eval₂ φ x = 0) : ∃ n : ℕ, 0 < n ∧ ∃ r : ℚ, r ≠ 0 ∧ A.valuation (x ^ n) = A.valuation (φ r) := by classical set v := A.valuation with hv let f : ℕ → K := fun i => φ (p.coeff i) * x ^ i have hsum : ∑ i ∈ p.support, f i = 0 := by rw [eval₂_eq_sum, Polynomial.sum_def] at hpx exact hpx have hvx : v x ≠ 0 := (v.ne_zero_iff).mpr hx0 have hf0 : ∀ i ∈ p.support, v (f i) ≠ 0 := by intro i hi refine (v.ne_zero_iff).mpr (mul_ne_zero ?_ (pow_ne_zero _ hx0)) exact (map_ne_zero φ).mpr (mem_support_iff.mp hi) obtain ⟨j, hj, hjmax⟩ := Finset.exists_max_image p.support (fun i => v (f i)) (support_nonempty.mpr hp0) obtain ⟨i, hi, hij, heq⟩ := v.exists_ne_map_eq_of_sum_eq_zero hsum hj (hf0 j hj) hjmax obtain ⟨a, b, hab, ha, hb, heq'⟩ : ∃ a b : ℕ, a < b ∧ a ∈ p.support ∧ b ∈ p.support ∧ v (f a) = v (f b) := by rcases lt_or_gt_of_ne hij with h | h · exact ⟨i, j, h, hi, hj, heq⟩ · exact ⟨j, i, h, hj, hi, heq.symm⟩ have hca0 : v (φ (p.coeff a)) ≠ 0 := (v.ne_zero_iff).mpr ((map_ne_zero φ).mpr (mem_support_iff.mp ha)) have hcb0 : v (φ (p.coeff b)) ≠ 0 := (v.ne_zero_iff).mpr ((map_ne_zero φ).mpr (mem_support_iff.mp hb)) have h1 : v (φ (p.coeff a)) * v x ^ a = (v (φ (p.coeff b)) * v x ^ (b - a)) * v x ^ a := by have e : v x ^ b = v x ^ (b - a) * v x ^ a := by rw [← pow_add, Nat.sub_add_cancel hab.le] have := heq' simp only [f, map_mul, map_pow] at this rw [this, e, ← mul_assoc] have h2 : v (φ (p.coeff a)) = v (φ (p.coeff b)) * v x ^ (b - a) := mul_right_cancel₀ (pow_ne_zero _ hvx) h1 refine ⟨b - a, Nat.sub_pos_of_lt hab, p.coeff a / p.coeff b, div_ne_zero (mem_support_iff.mp ha) (mem_support_iff.mp hb), ?_⟩ rw [map_div₀, map_div₀, map_pow, h2, mul_div_cancel_left₀ _ hcb0] private theorem ker_eq_maximalIdeal_of_isAlgebraic [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K] (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) : RingHom.ker red = maximalIdeal A := by refine le_antisymm (IsLocalRing.le_maximalIdeal (RingHom.ker_ne_top red)) ?_ intro x hx rw [RingHom.mem_ker] rcases eq_or_ne x 0 with rfl | hx0 · exact map_zero red have hxK : (x : K) ≠ 0 := by simpa [ne_eq, ZeroMemClass.coe_eq_zero] using hx0 obtain ⟨p, hp0, hpx⟩ := Algebra.IsAlgebraic.isAlgebraic (R := ℚ) (x : K) obtain ⟨n, hn, r, hr0, hval⟩ := A.exists_pow_valuation_eq_of_isRoot (algebraMap ℚ K) hxK hp0 (by rwa [← aeval_def]) obtain ⟨u, hu⟩ := (A.valuation_eq_iff _ _).mp hval have hcoe : ((((u⁻¹ : Aˣ) : A) * x ^ n : A) : K) = algebraMap ℚ K r := by push_cast rw [← hu, ← mul_assoc, ← MulMemClass.coe_mul, Units.inv_mul, OneMemClass.coe_one, one_mul] have hrA : algebraMap ℚ K r ∈ A := hcoe ▸ SetLike.coe_mem _ have hxn : x ^ n = (u : A) * ⟨algebraMap ℚ K r, hrA⟩ := by apply Subtype.ext push_cast exact hu.symm have hrm : (⟨algebraMap ℚ K r, hrA⟩ : A) ∈ maximalIdeal A := by have hxnm : x ^ n ∈ maximalIdeal A := Ideal.pow_mem_of_mem _ hx n hn rw [hxn] at hxnm exact ((IsLocalRing.maximalIdeal.isMaximal A).isPrime.mem_or_mem hxnm).resolve_left (fun h => (IsLocalRing.mem_maximalIdeal _).mp h u.isUnit) have hr0' : red ⟨algebraMap ℚ K r, hrA⟩ = 0 := A.map_eq_zero_of_rat_mem_maximalIdeal ℓ red (algebraMap ℚ K) r hrA hrm have : red (x ^ n) = 0 := by rw [hxn, map_mul, hr0', mul_zero] rw [map_pow] at this exact pow_eq_zero_iff hn.ne' |>.mp this private theorem exists_mul_eq_one_of_map_ne_zero [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K] (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) {a : A} (ha : red a ≠ 0) : ∃ b : A, red a * red b = 1 := by have hunit : IsUnit a := by by_contra h have : a ∈ RingHom.ker red := by rw [A.ker_eq_maximalIdeal_of_isAlgebraic ℓ red] exact (IsLocalRing.mem_maximalIdeal _).mpr h exact ha this obtain ⟨u, rfl⟩ := hunit exact ⟨((u⁻¹ : Aˣ) : A), by rw [← map_mul, Units.mul_inv, map_one]⟩ private theorem ker_eq_maximalIdeal_apply [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K] (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) (a : A) : red a = 0 ↔ a ∈ maximalIdeal A := by rw [← RingHom.mem_ker, A.ker_eq_maximalIdeal_of_isAlgebraic ℓ red] end ValuationSubring set_option autoImplicit false noncomputable section open scoped IntermediateField.algebraAdjoinAdjoin open IntermediateField Polynomial namespace AlgebraicCurve variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F} private theorem isPrincipalIdealRing_adjoin_singleton (hj : Transcendental K j) : IsPrincipalIdealRing (Algebra.adjoin K ({j} : Set F)) := IsPrincipalIdealRing.of_surjective (Polynomial.algEquivOfTranscendental K j hj).toRingHom (Polynomial.algEquivOfTranscendental K j hj).surjective private theorem isDedekindDomain_adjoin_singleton (hj : Transcendental K j) : IsDedekindDomain (Algebra.adjoin K ({j} : Set F)) := haveI := isPrincipalIdealRing_adjoin_singleton hj inferInstance private theorem isDedekindDomain_integralClosure_adjoin (hj : Transcendental K j) [FiniteDimensional K⟮j⟯ F] [Algebra.IsSeparable K⟮j⟯ F] : IsDedekindDomain (integralClosure (Algebra.adjoin K ({j} : Set F)) F) := haveI := isDedekindDomain_adjoin_singleton hj integralClosure.isDedekindDomain (Algebra.adjoin K ({j} : Set F)) K⟮j⟯ F private theorem isFractionRing_integralClosure_adjoin (hj : Transcendental K j) [FiniteDimensional K⟮j⟯ F] : IsFractionRing (integralClosure (Algebra.adjoin K ({j} : Set F)) F) F := haveI := isDedekindDomain_adjoin_singleton hj integralClosure.isFractionRing_of_finite_extension (A := Algebra.adjoin K ({j} : Set F)) K⟮j⟯ F private theorem integralClosure_adjoin_le_valuationSubring (O : ValuationSubring F) (hK : ∀ c : K, algebraMap K F c ∈ O) (hjO : j ∈ O) (r : integralClosure (Algebra.adjoin K ({j} : Set F)) F) : (r : F) ∈ O := by let O' : Subalgebra K F := { O.toSubring with algebraMap_mem' := hK } have hle : Algebra.adjoin K ({j} : Set F) ≤ O' := Algebra.adjoin_le (Set.singleton_subset_iff.mpr hjO) let φ : Algebra.adjoin K ({j} : Set F) →+* O := (Subalgebra.val _).toRingHom.codRestrict O.toSubring (fun y => hle y.2) obtain ⟨p, hp, hpr⟩ : IsIntegral (Algebra.adjoin K ({j} : Set F)) (r : F) := r.2 have hint : IsIntegral O (r : F) := by refine ⟨p.map φ, hp.map φ, ?_⟩ rw [eval₂_map] exact hpr obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint rw [← hy] exact y.2 private theorem algebraMap_mem_integralClosure_adjoin (c : K) : algebraMap K F c ∈ integralClosure (Algebra.adjoin K ({j} : Set F)) F := by rw [mem_integralClosure_iff, IsScalarTower.algebraMap_apply K (Algebra.adjoin K ({j} : Set F)) F] exact isIntegral_algebraMap private theorem self_mem_integralClosure_adjoin : j ∈ integralClosure (Algebra.adjoin K ({j} : Set F)) F := by rw [mem_integralClosure_iff] have : j = algebraMap (Algebra.adjoin K ({j} : Set F)) F ⟨j, Algebra.self_mem_adjoin_singleton K j⟩ := rfl rw [this] exact isIntegral_algebraMap private theorem le_integralClosure_adjoin_of_isIntegral {S B : Subring F} (hS : S ≤ (Algebra.adjoin K ({j} : Set F)).toSubring) (hint : ∀ b : B, IsIntegral S (b : F)) (b : B) : (b : F) ∈ integralClosure (Algebra.adjoin K ({j} : Set F)) F := by rw [mem_integralClosure_iff] obtain ⟨p, hp, hpb⟩ := hint b let φ : S →+* Algebra.adjoin K ({j} : Set F) := S.subtype.codRestrict (Algebra.adjoin K ({j} : Set F)).toSubring (fun y => hS y.2) refine ⟨p.map φ, hp.map φ, ?_⟩ rw [eval₂_map] exact hpb end AlgebraicCurve set_option autoImplicit false open Polynomial namespace ValuationSubring variable {K : Type*} [Field K] (A : ValuationSubring K) {k : Type*} [Field k] private theorem isAlgClosed_of_surjective [IsAlgClosed K] (red : A →+* k) (hred : Function.Surjective red) : IsAlgClosed k := by refine IsAlgClosed.of_exists_root k fun p hp hirr => ?_ have hlifts : p ∈ Polynomial.lifts red := (lifts_iff_coeff_lifts p).mpr fun n => hred _ obtain ⟨P, hPp, hPdeg, hP⟩ := lifts_and_degree_eq_and_monic hlifts hp have hdegK : (P.map (algebraMap A K)).degree ≠ 0 := by rw [hP.degree_map, hPdeg] exact (degree_pos_of_irreducible hirr).ne' obtain ⟨x, hx⟩ := IsAlgClosed.exists_root (P.map (algebraMap A K)) hdegK have hint : IsIntegral A x := ⟨P, hP, by rwa [IsRoot.def, eval_map] at hx⟩ obtain ⟨y, rfl⟩ := IsIntegrallyClosed.isIntegral_iff.mp hint have hy : P.eval y = 0 := by apply IsFractionRing.injective A K rw [map_zero, ← Polynomial.eval₂_at_apply, ← eval_map] exact hx refine ⟨red y, ?_⟩ rw [← hPp, eval_map, Polynomial.eval₂_at_apply, hy, map_zero] end ValuationSubring set_option autoImplicit false namespace RingHom variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C) private def imagePrime (𝔮 : Ideal B) : Ideal π.range := 𝔮.map π.rangeRestrict variable {π} in private theorem rangeRestrict_mem_imagePrime_iff {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (b : B) : π.rangeRestrict b ∈ π.imagePrime 𝔮 ↔ b ∈ 𝔮 := by rw [imagePrime, ← Ideal.mem_comap, Ideal.comap_map_of_surjective _ π.rangeRestrict_surjective, ← RingHom.ker, ker_rangeRestrict, sup_eq_left.mpr hker] variable {π} in private theorem mk_mem_imagePrime_iff {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (b : B) (hb : π b ∈ π.range := π.mem_range_self b) : (⟨π b, hb⟩ : π.range) ∈ π.imagePrime 𝔮 ↔ b ∈ 𝔮 := rangeRestrict_mem_imagePrime_iff hker b variable {π} in private theorem mem_imagePrime_iff {𝔮 : Ideal B} (y : π.range) : y ∈ π.imagePrime 𝔮 ↔ ∃ b ∈ 𝔮, π.rangeRestrict b = y := by rw [imagePrime, Ideal.mem_map_iff_of_surjective _ π.rangeRestrict_surjective] variable {π} in private theorem imagePrime_ne_top {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (h𝔮 : 𝔮 ≠ ⊤) : π.imagePrime 𝔮 ≠ ⊤ := by intro htop apply h𝔮 rw [Ideal.eq_top_iff_one, ← rangeRestrict_mem_imagePrime_iff hker, map_one, htop] exact Submodule.mem_top variable {π} in private theorem imagePrime_isPrime {𝔮 : Ideal B} [𝔮.IsPrime] (hker : ker π ≤ 𝔮) : (π.imagePrime 𝔮).IsPrime := Ideal.map_isPrime_of_surjective π.rangeRestrict_surjective (by rwa [ker_rangeRestrict]) variable {π} in private theorem imagePrime_isMaximal {𝔮 : Ideal B} [h : 𝔮.IsMaximal] (hker : ker π ≤ 𝔮) : (π.imagePrime 𝔮).IsMaximal := (Ideal.map_eq_top_or_isMaximal_of_surjective _ π.rangeRestrict_surjective h).resolve_left (imagePrime_ne_top hker h.ne_top) variable {π} in private theorem eq_zero_of_const_mem_imagePrime {A k : Type*} [CommRing A] [CommRing k] (σ : A →+* B) (red : A →+* k) (ι : k →+* C) (hcompat : ∀ a : A, π (σ a) = ι (red a)) (hred : Function.Surjective red) {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (h𝔮 : ∀ a : A, σ a ∈ 𝔮 → red a = 0) (c : k) (hc : ι c ∈ π.range) (hmem : (⟨ι c, hc⟩ : π.range) ∈ π.imagePrime 𝔮) : c = 0 := by obtain ⟨a, rfl⟩ := hred c refine h𝔮 a ((rangeRestrict_mem_imagePrime_iff hker (σ a)).mp ?_) convert hmem using 1 exact Subtype.ext (hcompat a) variable {π} in private theorem const_mem_range {A k : Type*} [CommRing A] [CommRing k] (σ : A →+* B) (red : A →+* k) (ι : k →+* C) (hcompat : ∀ a : A, π (σ a) = ι (red a)) (hred : Function.Surjective red) (c : k) : ι c ∈ π.range := by obtain ⟨a, rfl⟩ := hred c exact ⟨σ a, hcompat a⟩ end RingHom namespace AlgebraicCurve namespace Place variable {K F : Type*} [Field K] [Field F] [Algebra K F] private theorem eq_zero_of_X_sub_C_dvd_C {R : Type*} [CommRing R] {a₀ a : R} (h : (Polynomial.X - Polynomial.C a₀) ∣ Polynomial.C a) : a = 0 := by obtain ⟨g, hg⟩ := h have := congrArg (Polynomial.eval a₀) hg simpa using this private theorem exists_place_centre_comap_eq [IsAlgClosed K] (A : ValuationSubring K) {j : F} (hj : Transcendental K j) [FiniteDimensional K⟮j⟯ F] [Algebra.IsSeparable K⟮j⟯ F] {B : Subring F} (hconst : ∀ a : A, algebraMap K F a ∈ B) (hjB : j ∈ B) (hint : ∀ b : B, IsIntegral (Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {j})) (b : F)) (𝔮 : Ideal B) [𝔮.IsPrime] (h𝔮A : ∀ a : A, (⟨algebraMap K F a, hconst a⟩ : B) ∈ 𝔮 ↔ a ∈ IsLocalRing.maximalIdeal A) (a₀ : A) (hja : (⟨j, hjB⟩ : B) - ⟨algebraMap K F a₀, hconst a₀⟩ ∈ 𝔮) : ∃ (w : Place K F) (hB : B ≤ w.compSubring A), (w.centre A).comap (Subring.inclusion hB) = 𝔮 ∧ w.HasValueAt j a₀ := by classical set S : Subring F := Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {j}) with hSdef have hSB : S ≤ B := by rw [hSdef, Subring.closure_le] rintro y (⟨a, rfl⟩ | rfl) exacts [hconst a, hjB] haveI : IsIntegrallyClosed S := A.isIntegrallyClosed_closure hj have hjS : j ∈ S := Subring.subset_closure (Or.inr rfl) have hcS : ∀ a : A, algebraMap K F a ∈ S := fun a => Subring.subset_closure (Or.inl ⟨a, rfl⟩) let e := A.polynomialEquivClosure hj have heX : (e Polynomial.X : F) = j := by rw [ValuationSubring.polynomialEquivClosure_apply, Polynomial.aeval_X] have heC : ∀ a : A, (e (Polynomial.C a) : F) = algebraMap K F a := fun a => by rw [ValuationSubring.polynomialEquivClosure_apply, Polynomial.aeval_C] rfl have hegen : e (Polynomial.X - Polynomial.C a₀) = ⟨j, hjS⟩ - ⟨algebraMap K F a₀, hcS a₀⟩ := by apply Subtype.ext rw [map_sub] push_cast rw [heX, heC] let p₀ : Ideal (Polynomial A) := Ideal.span {Polynomial.X - Polynomial.C a₀} haveI hp₀ : p₀.IsPrime := by rw [← Ideal.Quotient.isDomain_iff_prime] exact (Polynomial.quotientSpanXSubCAlgEquiv a₀).toMulEquiv.isDomain_iff.mpr inferInstance let p : Ideal S := p₀.map e.toRingHom haveI hp : p.IsPrime := Ideal.map_isPrime_of_equiv e have hp_span : p = Ideal.span {(⟨j, hjS⟩ : S) - ⟨algebraMap K F a₀, hcS a₀⟩} := by change Ideal.map e.toRingHom (Ideal.span _) = _ rw [Ideal.map_span, Set.image_singleton] exact congrArg (fun y => Ideal.span {y}) hegen let q : Ideal S := 𝔮.comap (Subring.inclusion hSB) have hpq : p ≤ q := by rw [hp_span, Ideal.span_le, Set.singleton_subset_iff] change Subring.inclusion hSB (⟨j, hjS⟩ - ⟨algebraMap K F a₀, hcS a₀⟩) ∈ 𝔮 rw [map_sub] exact hja obtain ⟨𝔭, h𝔭𝔮, h𝔭, h𝔭p⟩ := Subring.exists_ideal_le_comap_eq_of_isIntegral hSB hint hpq 𝔮 rfl haveI := h𝔭 have hj𝔭 : (⟨j, hjB⟩ : B) - ⟨algebraMap K F a₀, hconst a₀⟩ ∈ 𝔭 := by have : (⟨j, hjS⟩ : S) - ⟨algebraMap K F a₀, hcS a₀⟩ ∈ 𝔭.comap (Subring.inclusion hSB) := by rw [h𝔭p, hp_span] exact Ideal.subset_span rfl rw [Ideal.mem_comap, map_sub] at this exact this have hbot : ∀ a : A, (⟨algebraMap K F a, hconst a⟩ : B) ∈ 𝔭 → a = 0 := by intro a ha have h1 : (⟨algebraMap K F a, hcS a⟩ : S) ∈ 𝔭.comap (Subring.inclusion hSB) := by rw [Ideal.mem_comap] exact ha rw [h𝔭p, hp_span, Ideal.mem_span_singleton'] at h1 obtain ⟨g, hg⟩ := h1 have h3 : e (Polynomial.C a) = ⟨algebraMap K F a, hcS a⟩ := Subtype.ext (heC a) have h4 : e.symm g * (Polynomial.X - Polynomial.C a₀) = Polynomial.C a := by apply e.injective rw [map_mul, e.apply_symm_apply, hegen, h3, hg] exact eq_zero_of_X_sub_C_dvd_C ⟨e.symm g, by rw [mul_comm]; exact h4.symm⟩ have hj_ne : j - algebraMap K F a₀ ≠ 0 := by intro h apply hj rw [sub_eq_zero] at h rw [h] exact isAlgebraic_algebraMap (a₀ : K) have h𝔭ne : 𝔭 ≠ ⊥ := by intro h rw [h, Ideal.mem_bot] at hj𝔭 exact hj_ne (by simpa using congrArg Subtype.val hj𝔭) obtain ⟨O, hle, hdom⟩ := Subring.exists_valuationSubring_dominating 𝔭 have hne : O ≠ ⊤ := Subring.ne_top_of_dominating hdom h𝔭ne have hK : ∀ c : K, algebraMap K F c ∈ O := Subring.algebraMap_mem_of_dominating A hconst hle hdom hbot let R := integralClosure (Algebra.adjoin K ({j} : Set F)) F haveI : IsDedekindDomain R := isDedekindDomain_integralClosure_adjoin hj haveI : IsFractionRing R F := isFractionRing_integralClosure_adjoin hj have hO : ∀ r : R, algebraMap R F r ∈ O := fun r => integralClosure_adjoin_le_valuationSubring O hK (hle hjB) r let w : Place K F := Place.ofValuationSubringOver O hO hne hK have hval : w.HasValueAt j a₀ := by have := (hdom (⟨j, hjB⟩ - ⟨algebraMap K F a₀, hconst a₀⟩)).mpr hj𝔭 simp at this exact this have hS_le : S ≤ w.compSubring A := by rw [hSdef, Subring.closure_le] rintro y (⟨a, rfl⟩ | rfl) · exact (w.algebraMap_mem_compSubring_iff A _).mpr a.2 · exact w.mem_compSubring_of_hasValueAt a₀.2 hval have hB : B ≤ w.compSubring A := fun b hb => w.mem_compSubring_of_isIntegral' A hS_le (hint ⟨b, hb⟩) refine ⟨w, hB, ?_, hval⟩ have h𝔭𝔓 : 𝔭 ≤ (w.centre A).comap (Subring.inclusion hB) := fun x hx => w.mem_centre_of_mem_nonunits ((hdom x).mpr hx) ext b obtain ⟨a, hab⟩ := ValuationSubring.exists_sub_constants_mem hconst hjB hint 𝔭 hbot a₀ hj𝔭 b have hab' : b - ⟨algebraMap K F a, hconst a⟩ ∈ 𝔭 := hab have key : ∀ (I : Ideal B), 𝔭 ≤ I → (b ∈ I ↔ (⟨algebraMap K F a, hconst a⟩ : B) ∈ I) := by intro I hI constructor · intro hb have := I.sub_mem hb (hI hab') rwa [sub_sub_cancel] at this · intro ha have := I.add_mem (hI hab') ha rwa [sub_add_cancel] at this rw [key _ h𝔭𝔓, key _ h𝔭𝔮, w.algebraMap_mem_centre_comap_iff hB hconst, h𝔮A] end Place end AlgebraicCurve namespace AlgebraicCurve namespace Place variable {K E : Type*} [Field K] [Field E] [Algebra K E] private theorem finite_residueField_of_adjoin_simple_eq_top_of_mem {x : E} (hx : Transcendental K x) (htop : IntermediateField.adjoin K ({x} : Set E) = ⊤) (v : Place K E) (hxv : x ∈ v.toValuationSubring) : Module.Finite K v.ResidueField := by classical haveI : IsDedekindDomain (Algebra.adjoin K ({x} : Set E)) := isDedekindDomain_adjoin_singleton hx haveI : FaithfulSMul (Algebra.adjoin K ({x} : Set E)) E := (faithfulSMul_iff_algebraMap_injective _ E).mpr Subtype.val_injective haveI : IsFractionRing (Algebra.adjoin K ({x} : Set E)) E := by refine IsFractionRing.of_field (Algebra.adjoin K ({x} : Set E)) E (fun z => ?_) have hz : z ∈ IntermediateField.adjoin K ({x} : Set E) := by rw [htop] exact IntermediateField.mem_top obtain ⟨r, hr, s, hs, rfl⟩ := IntermediateField.mem_adjoin_iff_div.mp hz exact ⟨⟨r, hr⟩, ⟨s, hs⟩, rfl⟩ set O := v.toValuationSubring with hOdef have hO : ∀ r : Algebra.adjoin K ({x} : Set E), algebraMap _ E r ∈ O := by intro r have hle : Algebra.adjoin K ({x} : Set E) ≤ { O.toSubring with algebraMap_mem' := v.algebraMap_mem' } := Algebra.adjoin_le (Set.singleton_subset_iff.mpr hxv) exact hle r.2 have hne : O ≠ ⊤ := v.ne_top' let xO : O := ⟨x, hxv⟩ let xbar : v.ResidueField := IsLocalRing.residue O xO have hcomp : (IsLocalRing.residue O).comp (algebraMap K O) = algebraMap K v.ResidueField := RingHom.ext fun _ => rfl have hres_aeval : ∀ p : K[X], IsLocalRing.residue O (Polynomial.aeval xO p) = Polynomial.aeval xbar p := fun p => by rw [Polynomial.aeval_def, Polynomial.aeval_def, Polynomial.hom_eval₂, hcomp] have hcoe_aeval : ∀ p : K[X], ((Polynomial.aeval xO p : O) : E) = Polynomial.aeval x p := fun p => by have := Polynomial.aeval_algHom_apply (IsScalarTower.toAlgHom K O E) xO p exact this.symm let e := Polynomial.algEquivOfTranscendental K x hx have hcoe_e : ∀ p : K[X], ((e p : Algebra.adjoin K ({x} : Set E)) : E) = Polynomial.aeval x p := fun p => by rw [Polynomial.algEquivOfTranscendental_apply, Polynomial.aeval_subalgebra_coe] have hOe : ∀ p : K[X], (⟨((e p : Algebra.adjoin K ({x} : Set E)) : E), hO (e p)⟩ : O) = Polynomial.aeval xO p := fun p => Subtype.ext (by rw [hcoe_aeval, hcoe_e]) obtain ⟨f, hf𝔭, hf0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot (O.centreOver_ne_bot hO hne) obtain ⟨g, rfl⟩ := e.surjective f have hg0 : g ≠ 0 := fun h => hf0 (by rw [h, map_zero]) have hgbar : Polynomial.aeval xbar g = 0 := by rw [← hres_aeval, IsLocalRing.residue_eq_zero_iff, ← hOe, ← ValuationSubring.coe_mem_nonunits_iff] exact (O.mem_centreOver_iff hO).mp hf𝔭 have halg : IsAlgebraic K xbar := ⟨g, hg0, hgbar⟩ have hint : IsIntegral K xbar := halg.isIntegral haveI : FiniteDimensional K K⟮xbar⟯ := IntermediateField.adjoin.finiteDimensional hint have htop' : K⟮xbar⟯ = ⊤ := by rw [eq_top_iff] intro y _ obtain ⟨z, rfl⟩ := IsLocalRing.residue_surjective y have hz : (z : E) ∈ IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime E (O.centreHeightOneSpectrum hO hne) := by rw [← O.eq_valuationSubringAtPrime_centre hO hne] exact z.2 obtain ⟨a, s, hs, hz'⟩ := hz obtain ⟨ga, rfl⟩ := e.surjective a obtain ⟨gs, rfl⟩ := e.surjective s have hsn : ((e gs : Algebra.adjoin K ({x} : Set E)) : E) ∉ O.nonunits := fun h => hs ((O.mem_centreOver_iff hO).mpr h) have hres_s : IsLocalRing.residue O (Polynomial.aeval xO gs) ≠ 0 := by rw [Ne, IsLocalRing.residue_eq_zero_iff, ← hOe, ← ValuationSubring.coe_mem_nonunits_iff] exact hsn have hs0 : ((e gs : Algebra.adjoin K ({x} : Set E)) : E) ≠ 0 := fun h => hsn (h ▸ (zero_mem O.nonunits)) have hmul : z * Polynomial.aeval xO gs = Polynomial.aeval xO ga := by rw [← hOe, ← hOe] apply Subtype.ext change (z : E) * _ = _ push_cast rw [hz'] exact inv_mul_cancel_right₀ hs0 _ have hzq : IsLocalRing.residue O z = Polynomial.aeval xbar ga / Polynomial.aeval xbar gs := by rw [eq_div_iff (by rwa [← hres_aeval]), ← hres_aeval, ← hres_aeval, ← map_mul, hmul] rw [hzq] refine div_mem ?_ ?_ <;> exact IntermediateField.algebra_adjoin_le_adjoin K _ (Polynomial.aeval_mem_adjoin_singleton K _) have : FiniteDimensional K (⊤ : IntermediateField K v.ResidueField) := by rw [← htop'] infer_instance exact IntermediateField.topEquiv.toLinearEquiv.finiteDimensional private theorem _root_.IntermediateField.adjoin_simple_inv_eq (x : E) : IntermediateField.adjoin K ({x⁻¹} : Set E) = IntermediateField.adjoin K ({x} : Set E) := by apply le_antisymm · rw [IntermediateField.adjoin_simple_le_iff] exact inv_mem (IntermediateField.mem_adjoin_simple_self K x) · rw [IntermediateField.adjoin_simple_le_iff] have h := inv_mem (IntermediateField.mem_adjoin_simple_self K x⁻¹) rwa [inv_inv] at h private theorem finite_residueField_of_adjoin_simple_eq_top {x : E} (hx : Transcendental K x) (htop : IntermediateField.adjoin K ({x} : Set E) = ⊤) (v : Place K E) : Module.Finite K v.ResidueField := by by_cases hxv : x ∈ v.toValuationSubring · exact finite_residueField_of_adjoin_simple_eq_top_of_mem hx htop v hxv · have hxinv : x⁻¹ ∈ v.toValuationSubring := (v.toValuationSubring.mem_or_inv_mem x).resolve_left hxv have hx' : Transcendental K x⁻¹ := fun h => hx (by simpa using h.inv) have htop' : IntermediateField.adjoin K ({x⁻¹} : Set E) = ⊤ := by rw [IntermediateField.adjoin_simple_inv_eq x, htop] exact finite_residueField_of_adjoin_simple_eq_top_of_mem hx' htop' v hxinv private theorem finiteResidue_of_adjoin_simple_eq_top {x : E} (hx : Transcendental K x) (htop : IntermediateField.adjoin K ({x} : Set E) = ⊤) (v : Place K E) : v.FiniteResidue := ⟨finite_residueField_of_adjoin_simple_eq_top hx htop v⟩ end Place end AlgebraicCurve namespace ValuationSubring variable {F : Type*} [Field F] variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F] private theorem eq_of_forall_mem_nonunits_iff {O₁ O₂ : ValuationSubring F} (h₁ : ∀ r : R, algebraMap R F r ∈ O₁) (hne₁ : O₁ ≠ ⊤) (h₂ : ∀ r : R, algebraMap R F r ∈ O₂) (hne₂ : O₂ ≠ ⊤) (h : ∀ r : R, algebraMap R F r ∈ O₁.nonunits ↔ algebraMap R F r ∈ O₂.nonunits) : O₁ = O₂ := by have hc : O₁.centreHeightOneSpectrum h₁ hne₁ = O₂.centreHeightOneSpectrum h₂ hne₂ := by ext r change r ∈ O₁.centreOver h₁ ↔ r ∈ O₂.centreOver h₂ rw [mem_centreOver_iff, mem_centreOver_iff] exact h r rw [O₁.eq_valuationSubringAtPrime_centre h₁ hne₁, O₂.eq_valuationSubringAtPrime_centre h₂ hne₂, hc] end ValuationSubring namespace AlgebraicCurve namespace Place variable {K F : Type*} [Field K] [Field F] [Algebra K F] private theorem eq_of_forall_mem_nonunits_iff (R : Type*) [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F] {v₁ v₂ : Place K F} (h₁ : ∀ r : R, algebraMap R F r ∈ v₁.toValuationSubring) (h₂ : ∀ r : R, algebraMap R F r ∈ v₂.toValuationSubring) (h : ∀ r : R, algebraMap R F r ∈ v₁.toValuationSubring.nonunits ↔ algebraMap R F r ∈ v₂.toValuationSubring.nonunits) : v₁ = v₂ := Place.ext (ValuationSubring.eq_of_forall_mem_nonunits_iff h₁ v₁.ne_top' h₂ v₂.ne_top' h) private theorem eq_of_forall_mem_nonunits_iff_of_surjective (R : Type*) [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F] {v₁ v₂ : Place K F} (h₁ : ∀ r : R, algebraMap R F r ∈ v₁.toValuationSubring) (h₂ : ∀ r : R, algebraMap R F r ∈ v₂.toValuationSubring) {ι : Type*} (f : ι → F) (hsurj : ∀ r : R, ∃ i, f i = algebraMap R F r) (h : ∀ i, f i ∈ v₁.toValuationSubring.nonunits ↔ f i ∈ v₂.toValuationSubring.nonunits) : v₁ = v₂ := eq_of_forall_mem_nonunits_iff R h₁ h₂ fun r => by obtain ⟨i, hi⟩ := hsurj r rw [← hi] exact h i variable (K) in private theorem integralClosure_adjoin_le_of_forall_isIntegral_mem {j : F} {S : Subring F} (hK : ∀ c : K, algebraMap K F c ∈ S) (hj : j ∈ S) (hS : ∀ x : F, (∃ p : Polynomial S, p.Monic ∧ Polynomial.eval₂ S.subtype x p = 0) → x ∈ S) (r : integralClosure (Algebra.adjoin K ({j} : Set F)) F) : (r : F) ∈ S := by let S' : Subalgebra K F := { S with algebraMap_mem' := hK } have hle : Algebra.adjoin K ({j} : Set F) ≤ S' := Algebra.adjoin_le (Set.singleton_subset_iff.mpr hj) let φ : Algebra.adjoin K ({j} : Set F) →+* S := (Subalgebra.val _).toRingHom.codRestrict S (fun y => hle y.2) obtain ⟨p, hp, hpr⟩ : IsIntegral (Algebra.adjoin K ({j} : Set F)) (r : F) := r.2 refine hS r ⟨p.map φ, hp.map φ, ?_⟩ rw [Polynomial.eval₂_map] exact hpr private theorem exists_eq_of_integralClosure_adjoin {j : F} {B : Type*} (π : B → F) {S : Subring F} (hrange : ∀ x, x ∈ S ↔ ∃ b, π b = x) (hK : ∀ c : K, algebraMap K F c ∈ S) (hj : j ∈ S) (hS : ∀ x : F, (∃ p : Polynomial S, p.Monic ∧ Polynomial.eval₂ S.subtype x p = 0) → x ∈ S) (r : integralClosure (Algebra.adjoin K ({j} : Set F)) F) : ∃ b, π b = algebraMap (integralClosure (Algebra.adjoin K ({j} : Set F)) F) F r := (hrange r).mp (integralClosure_adjoin_le_of_forall_isIntegral_mem K hK hj hS r) end Place end AlgebraicCurve namespace ModularCurve namespace CharPModel open AlgebraicCurve AlgebraicCurve.Place section SpecializationConstruction variable {A : ValuationSubring (AlgebraicClosure ℚ)} {N : ℕ} [NeZero N] {ℓ : ℕ} [Fact ℓ.Prime] {k : Type*} [Field k] [CharP k ℓ] {red : A →+* k} set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.bfin_le_compSubring (fm : FibreModel N A ℓ k red) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : fm.BFin ≤ (w.compSubring A : Subring (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) := by have hS : affineBaseFin N A ≤ w.compSubring A := by refine Subring.closure_le.mpr ?_ rintro x (⟨a, rfl⟩ | rfl) · exact (w.algebraMap_mem_compSubring_iff A _).mpr a.2 · exact hwFin exact fun x hx => w.mem_compSubring_of_isIntegral' A hS (fm.integralFin ⟨x, hx⟩) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.constFin_mem' (fm : FibreModel N A ℓ k red) : ∀ a : A, algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) a ∈ fm.BFin := fm.constFin_mem private noncomputable def FibreModel.centreFin (fm : FibreModel N A ℓ k red) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : Ideal fm.BFin := (w.centre A).comap (Subring.inclusion (fm.bfin_le_compSubring w hwFin)) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.centreFin_isMaximal (fm : FibreModel N A ℓ k red) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : (fm.centreFin w hwFin).IsMaximal := w.centre_comap_isMaximal (fm.bfin_le_compSubring w hwFin) fm.constFin_mem' set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.ker_piFin_le_centreFin (fm : FibreModel N A ℓ k red) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : RingHom.ker fm.piFin ≤ fm.centreFin w hwFin := by rw [fm.ker_piFin, Ideal.span_le] rintro x ⟨a, ha, rfl⟩ show _ ∈ (w.centre A).comap (Subring.inclusion (fm.bfin_le_compSubring w hwFin)) rw [Ideal.mem_comap] exact (w.algebraMap_mem_centre_iff A a).mpr ha include ℓ in set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem red_eq_zero_of_mem_maximalIdeal {a : A} (ha : a ∈ IsLocalRing.maximalIdeal A) : red a = 0 := by have hker := @ValuationSubring.ker_eq_maximalIdeal_of_isAlgebraic _ _ A _ _ (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ) ℓ _ _ red exact RingHom.mem_ker.mp (hker ▸ ha) private noncomputable def lineClosure (k : Type*) [Field k] (N : ℕ) [NeZero N] : Subalgebra (Algebra.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (modularFunctionFieldC k N) := integralClosure (Algebra.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (modularFunctionFieldC k N) set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.exists_spFin (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (data : ModularPolynomialData N) (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : ∃ v' : Place k (modularFunctionFieldC k N), ∀ b : fm.BFin, (fm.piFin b : modularFunctionFieldC k N) ∈ v'.toValuationSubring.nonunits ↔ b ∈ fm.centreFin w hwFin := by haveI hmax : (fm.centreFin w hwFin).IsMaximal := fm.centreFin_isMaximal w hwFin have hker := fm.ker_piFin_le_centreFin w hwFin haveI hPmax : (fm.piFin.imagePrime (fm.centreFin w hwFin)).IsMaximal := fm.piFin.imagePrime_isMaximal hker haveI hPprime : (fm.piFin.imagePrime (fm.centreFin w hwFin)).IsPrime := hPmax.isPrime obtain ⟨O, hle, hdom⟩ := Subring.exists_valuationSubring_dominating (B := fm.piFin.range) (fm.piFin.imagePrime (fm.centreFin w hwFin)) have hPne : fm.piFin.imagePrime (fm.centreFin w hwFin) ≠ ⊥ := by have hmem : (⟨jBar N, fm.jBar_mem⟩ : fm.BFin) - ⟨constantsHom N A (w.value A ⟨jBar N, hwFin⟩), fm.constFin_mem _⟩ ∈ fm.centreFin w hwFin := w.sub_value_mem_centre_comap (fm.bfin_le_compSubring w hwFin) fm.constFin_mem' _ have hy : fm.piFin.rangeRestrict ((⟨jBar N, fm.jBar_mem⟩ : fm.BFin) - ⟨constantsHom N A (w.value A ⟨jBar N, hwFin⟩), fm.constFin_mem _⟩) ∈ fm.piFin.imagePrime (fm.centreFin w hwFin) := (fm.piFin.rangeRestrict_mem_imagePrime_iff hker _).mpr hmem intro hbot rw [hbot, Ideal.mem_bot] at hy have hval : fm.piFin ((⟨jBar N, fm.jBar_mem⟩ : fm.BFin) - ⟨constantsHom N A (w.value A ⟨jBar N, hwFin⟩), fm.constFin_mem _⟩) = 0 := by have := congrArg Subtype.val hy simpa using this rw [map_sub] at hval have hj : fm.piFin ⟨jBar N, fm.jBar_mem⟩ = jLine k N := fm.piFin_j have hc : fm.piFin ⟨constantsHom N A (w.value A ⟨jBar N, hwFin⟩), fm.constFin_mem _⟩ = algebraMap k (modularFunctionFieldC k N) (red (w.value A ⟨jBar N, hwFin⟩)) := fm.piFin_const _ rw [hj, hc, sub_eq_zero] at hval exact (transcendental_jLine k N) (hval ▸ isAlgebraic_algebraMap _) have hne : O ≠ ⊤ := Subring.ne_top_of_dominating hdom hPne have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piFin.range := by intro c obtain ⟨a, rfl⟩ := hred c exact ⟨⟨constantsHom N A a, fm.constFin_mem a⟩, (fm.piFin_const a).symm ▸ rfl⟩ have hK : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ O := by intro c obtain ⟨a, rfl⟩ := hred c exact hle (hconstR (red a)) haveI hFD : FiniteDimensional (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (modularFunctionFieldC k N) := finiteDimensional_adjoin_jC k N data haveI hSep : Algebra.IsSeparable (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (modularFunctionFieldC k N) := isSeparable_line_fibre k N data hsep haveI hDed : IsDedekindDomain (lineClosure k N) := isDedekindDomain_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLine k N) haveI hFrac : IsFractionRing (lineClosure k N) (modularFunctionFieldC k N) := isFractionRing_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLine k N) have hjO : (jLine k N : modularFunctionFieldC k N) ∈ O := by have h := hle (fm.piFin.mem_range_self ⟨jBar N, fm.jBar_mem⟩) have hj : fm.piFin ⟨jBar N, fm.jBar_mem⟩ = jLine k N := fm.piFin_j rwa [hj] at h refine ⟨Place.ofValuationSubringOver (R := lineClosure k N) O (fun r => integralClosure_adjoin_le_valuationSubring O hK hjO r) hne hK, ?_⟩ intro b exact (hdom (fm.piFin.rangeRestrict b)).trans (fm.piFin.rangeRestrict_mem_imagePrime_iff hker b) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem transcendental_jLineInv (k : Type*) [Field k] (N : ℕ) [NeZero N] : Transcendental k (((jLine k N)⁻¹ : modularFunctionFieldC k N)) := by intro h exact transcendental_jLine k N (by simpa using h.inv) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.binf_le_compSubring (fm : FibreModel N A ℓ k red) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : fm.BInf ≤ (w.compSubring A : Subring (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) := by have hS : affineBaseInf N A ≤ w.compSubring A := by refine Subring.closure_le.mpr ?_ rintro x (⟨a, rfl⟩ | rfl) · exact (w.algebraMap_mem_compSubring_iff A _).mpr a.2 · exact hwInf exact fun x hx => w.mem_compSubring_of_isIntegral' A hS (fm.integralInf ⟨x, hx⟩) private noncomputable def FibreModel.centreInf (fm : FibreModel N A ℓ k red) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : Ideal fm.BInf := (w.centre A).comap (Subring.inclusion (fm.binf_le_compSubring w hwInf)) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.centreInf_isMaximal (fm : FibreModel N A ℓ k red) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : (fm.centreInf w hwInf).IsMaximal := w.centre_comap_isMaximal (fm.binf_le_compSubring w hwInf) fm.constInf_mem set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.ker_piInf_le_centreInf (fm : FibreModel N A ℓ k red) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : RingHom.ker fm.piInf ≤ fm.centreInf w hwInf := by rw [fm.ker_piInf, Ideal.span_le] rintro x ⟨a, ha, rfl⟩ show _ ∈ (w.centre A).comap (Subring.inclusion (fm.binf_le_compSubring w hwInf)) rw [Ideal.mem_comap] exact (w.algebraMap_mem_centre_iff A a).mpr ha private noncomputable def lineClosureInf (k : Type*) [Field k] (N : ℕ) [NeZero N] : Subalgebra (Algebra.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N)))) (modularFunctionFieldC k N) := integralClosure (Algebra.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N)))) (modularFunctionFieldC k N) set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.exists_spInf (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (data : ModularPolynomialData N) (hsep : ((data.Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hwInf : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : ∃ v' : Place k (modularFunctionFieldC k N), ∀ b : fm.BInf, (fm.piInf b : modularFunctionFieldC k N) ∈ v'.toValuationSubring.nonunits ↔ b ∈ fm.centreInf w hwInf := by haveI hmax : (fm.centreInf w hwInf).IsMaximal := fm.centreInf_isMaximal w hwInf have hker := fm.ker_piInf_le_centreInf w hwInf haveI hPmax : (fm.piInf.imagePrime (fm.centreInf w hwInf)).IsMaximal := fm.piInf.imagePrime_isMaximal hker haveI hPprime : (fm.piInf.imagePrime (fm.centreInf w hwInf)).IsPrime := hPmax.isPrime obtain ⟨O, hle, hdom⟩ := Subring.exists_valuationSubring_dominating (B := fm.piInf.range) (fm.piInf.imagePrime (fm.centreInf w hwInf)) have hPne : fm.piInf.imagePrime (fm.centreInf w hwInf) ≠ ⊥ := by have hmem : (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) - ⟨constantsHom N A (w.value A ⟨(jBar N)⁻¹, hwInf⟩), fm.constInf_mem _⟩ ∈ fm.centreInf w hwInf := w.sub_value_mem_centre_comap (fm.binf_le_compSubring w hwInf) fm.constInf_mem _ have hy : fm.piInf.rangeRestrict ((⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) - ⟨constantsHom N A (w.value A ⟨(jBar N)⁻¹, hwInf⟩), fm.constInf_mem _⟩) ∈ fm.piInf.imagePrime (fm.centreInf w hwInf) := (fm.piInf.rangeRestrict_mem_imagePrime_iff hker _).mpr hmem intro hbot rw [hbot, Ideal.mem_bot] at hy have hval : fm.piInf ((⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) - ⟨constantsHom N A (w.value A ⟨(jBar N)⁻¹, hwInf⟩), fm.constInf_mem _⟩) = 0 := by have := congrArg Subtype.val hy simpa using this rw [map_sub] at hval have hj : fm.piInf ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ = (jLine k N)⁻¹ := fm.piInf_jInv have hc : fm.piInf ⟨constantsHom N A (w.value A ⟨(jBar N)⁻¹, hwInf⟩), fm.constInf_mem _⟩ = algebraMap k (modularFunctionFieldC k N) (red (w.value A ⟨(jBar N)⁻¹, hwInf⟩)) := fm.piInf_const _ rw [hj, hc, sub_eq_zero] at hval exact (transcendental_jLineInv k N) (hval ▸ isAlgebraic_algebraMap _) have hne : O ≠ ⊤ := Subring.ne_top_of_dominating hdom hPne have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piInf.range := by intro c obtain ⟨a, rfl⟩ := hred c exact ⟨⟨constantsHom N A a, fm.constInf_mem a⟩, (fm.piInf_const a).symm ▸ rfl⟩ have hK : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ O := by intro c obtain ⟨a, rfl⟩ := hred c exact hle (hconstR (red a)) haveI hFD : FiniteDimensional (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N)))) (modularFunctionFieldC k N) := by rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)] exact finiteDimensional_adjoin_jC k N data haveI hSep : Algebra.IsSeparable (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N)))) (modularFunctionFieldC k N) := by rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)] exact isSeparable_line_fibre k N data hsep haveI hDed : IsDedekindDomain (lineClosureInf k N) := isDedekindDomain_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLineInv k N) haveI hFrac : IsFractionRing (lineClosureInf k N) (modularFunctionFieldC k N) := isFractionRing_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLineInv k N) have hjO : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ O := by have h := hle (fm.piInf.mem_range_self ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩) have hj : fm.piInf ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ = (jLine k N)⁻¹ := fm.piInf_jInv rwa [hj] at h refine ⟨Place.ofValuationSubringOver (R := lineClosureInf k N) O (fun r => integralClosure_adjoin_le_valuationSubring O hK hjO r) hne hK, ?_⟩ intro b exact (hdom (fm.piInf.rangeRestrict b)).trans (fm.piInf.rangeRestrict_mem_imagePrime_iff hker b) set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.chart_dichotomy (_fm : FibreModel N A ℓ k red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A ∨ ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A := by haveI hFD : FiniteDimensional (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := finiteDimensional_lineBar_of_dataAll N dataAll haveI h1 : Module.Finite ((w.restrict (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))))).ResidueField) w.ResidueField := rf_finite_residueField w haveI h2 : Module.Finite (AlgebraicClosure ℚ) ((w.restrict (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))))).ResidueField) := by have htop : IntermediateField.adjoin (AlgebraicClosure ℚ) ({⟨jBar N, IntermediateField.mem_adjoin_simple_self _ (jBar N)⟩} : Set (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))))) = ⊤ := by have h := adjoin_val_preimage_eq_top (K := AlgebraicClosure ℚ) (F := IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (S := {jBar N}) rfl have hset : (Subtype.val ⁻¹' {jBar N} : Set (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))))) = {⟨jBar N, IntermediateField.mem_adjoin_simple_self _ (jBar N)⟩} := by ext z simp only [Set.mem_preimage, Set.mem_singleton_iff] exact ⟨fun hz => Subtype.ext hz, fun hz => by rw [hz]⟩ rwa [hset] at h exact AlgebraicCurve.Place.finite_residueField_of_adjoin_simple_eq_top (transcendental_subtype _ (IntermediateField.mem_adjoin_simple_self _ (jBar N)) (transcendental_jBar N)) htop _ haveI h3 : Module.Finite (AlgebraicClosure ℚ) w.ResidueField := Module.Finite.trans ((w.restrict (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))))).ResidueField) w.ResidueField exact w.mem_compSubring_or_inv_mem A (w.surjective_algebraMap_residueField_of_isAlgClosed) (jBar N) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem fibreEvalSwap_subtype (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) = 0 := by have hcomp : ((modularFunctionFieldC k N).val.toRingHom).comp (Polynomial.aeval (R := ℤ) (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom = (Polynomial.aeval (R := ℤ) (jqNModC k N)).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X] rfl have h := Polynomial.hom_eval₂ data.Φ (Polynomial.aeval (R := ℤ) (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom ((modularFunctionFieldC k N).val.toRingHom) (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) apply Subtype.val_injective have h0 : (modularFunctionFieldC k N).val.toRingHom (data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)).toRingHom (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)) = 0 := by rw [h, hcomp] exact fibreEvalSwap_eq_zero N data hsym k simpa using h0 set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem barEvalSwap_laurent (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq))).toRingHom (coeffEmb (AlgebraicClosure ℚ) jq) = 0 := by have hswap0 : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (qExpand ℚ N jq)).toRingHom jq = 0 := by rw [show qExpand ℚ N jq = jqN N from rfl, hsym (jqN N) jq] have h0 := data.eval_eq_zero rw [show evalAtJ = (Polynomial.aeval (R := ℤ) jq).toRingHom from rfl] at h0 exact h0 have hcomp : ((coeffEmb (AlgebraicClosure ℚ)).comp (Polynomial.aeval (R := ℤ) (qExpand ℚ N jq)).toRingHom) = (Polynomial.aeval (R := ℤ) (coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq))).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X] have h := Polynomial.hom_eval₂ data.Φ (Polynomial.aeval (R := ℤ) (qExpand ℚ N jq)).toRingHom (coeffEmb (AlgebraicClosure ℚ)) jq rw [hswap0, map_zero, hcomp] at h exact h.symm set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem barEvalSwap_subtype (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) : data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom (jBar N) = 0 := by have hcomp : (((laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom).comp (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom) = (Polynomial.aeval (R := ℤ) (coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq))).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · simp only [RingHom.coe_comp, Function.comp_apply, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, Polynomial.aeval_X] rfl have h := Polynomial.hom_eval₂ data.Φ (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom ((laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom) (jBar N) apply Subtype.val_injective have h0 : (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)).val.toRingHom (data.Φ.eval₂ (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom (jBar N)) = 0 := by rw [h, hcomp] exact barEvalSwap_laurent N data hsym simpa using h0 set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem transcendental_jNC (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) : Transcendental k (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) := by intro halg haveI hFD : FiniteDimensional k (IntermediateField.adjoin k ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N))) := IntermediateField.adjoin.finiteDimensional halg.isIntegral have h2 : IsIntegral (IntermediateField.adjoin k ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N))) (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) := isIntegral_adjoin_of_bivar_monic data.monic (fibreEvalSwap_subtype k N data hsym) have h3 : IsIntegral k (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) := by haveI : Algebra.IsIntegral k (IntermediateField.adjoin k ({⟨jqNModC k N, jqNModC_mem k N⟩} : Set (modularFunctionFieldC k N))) := Algebra.IsIntegral.of_finite _ _ exact isIntegral_trans _ h2 exact (transcendental_jC k N) h3.isAlgebraic set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem transcendental_jNBar (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) : Transcendental (AlgebraicClosure ℚ) (jNBar N) := by intro halg haveI hFD : FiniteDimensional (AlgebraicClosure ℚ) (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jNBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) := IntermediateField.adjoin.finiteDimensional halg.isIntegral have h2 : IsIntegral (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jNBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (jBar N) := isIntegral_adjoin_of_bivar_monic data.monic (barEvalSwap_subtype N data hsym) have h3 : IsIntegral (AlgebraicClosure ℚ) (jBar N) := by haveI : Algebra.IsIntegral (AlgebraicClosure ℚ) (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jNBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) := Algebra.IsIntegral.of_finite _ _ exact isIntegral_trans _ h2 exact (transcendental_jBar N) h3.isAlgebraic private theorem jBar_ne_const (N : ℕ) [NeZero N] (c : AlgebraicClosure ℚ) : jBar N ≠ algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) c := fun h => transcendental_jBar N (h ▸ isAlgebraic_algebraMap c) private theorem jLine_ne_const (k : Type*) [Field k] (N : ℕ) [NeZero N] (c : k) : jLine k N ≠ algebraMap k (modularFunctionFieldC k N) c := fun h => transcendental_jLine k N (h ▸ isAlgebraic_algebraMap c) private theorem jLine_ne_zero (k : Type*) [Field k] (N : ℕ) [NeZero N] : (jLine k N : modularFunctionFieldC k N) ≠ 0 := fun h => transcendental_jLine k N (h ▸ isAlgebraic_zero) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem mem_of_ord_nonneg {k' F' : Type*} [Field k'] [Field F'] [Algebra k' F'] (v : Place k' F') {x : F'} (hx : x ≠ 0) (h : 0 ≤ v.ord x) : x ∈ v.toValuationSubring := by by_contra hmem rcases v.toValuationSubring.mem_or_inv_mem x with hx' | hinv · exact hmem hx' have hinv_nu : x⁻¹ ∈ v.toValuationSubring.nonunits := by refine (ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inr ?_) rwa [inv_inv] have hpos : 0 < v.ord x⁻¹ := (v.mem_nonunits_iff_ord_pos (inv_ne_zero hx)).mp hinv_nu rw [v.ord_inv] at hpos exact absurd h (not_le.mpr (neg_pos.mp hpos)) open Classical in private noncomputable def FibreModel.sp (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) → Place k (modularFunctionFieldC k N) := fun w => if h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A then (fm.exists_spFin hred (dataAll N (dvd_refl N)) hsep w h).choose else (fm.exists_spInf hred (dataAll N (dvd_refl N)) hsep w ((fm.chart_dichotomy dataAll w).resolve_left h)).choose set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_spec_fin (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : ∀ b : fm.BFin, (fm.piFin b : modularFunctionFieldC k N) ∈ (fm.sp hred dataAll hsep w).toValuationSubring.nonunits ↔ b ∈ fm.centreFin w h := by have hsp : fm.sp hred dataAll hsep w = (fm.exists_spFin hred (dataAll N (dvd_refl N)) hsep w h).choose := by unfold FibreModel.sp rw [dif_pos h] rw [hsp] exact (fm.exists_spFin hred (dataAll N (dvd_refl N)) hsep w h).choose_spec set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_spec_inf (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : ∀ b : fm.BInf, (fm.piInf b : modularFunctionFieldC k N) ∈ (fm.sp hred dataAll hsep w).toValuationSubring.nonunits ↔ b ∈ fm.centreInf w ((fm.chart_dichotomy dataAll w).resolve_left h) := by have hsp : fm.sp hred dataAll hsep w = (fm.exists_spInf hred (dataAll N (dvd_refl N)) hsep w ((fm.chart_dichotomy dataAll w).resolve_left h)).choose := by unfold FibreModel.sp rw [dif_neg h] rw [hsp] exact (fm.exists_spInf hred (dataAll N (dvd_refl N)) hsep w ((fm.chart_dichotomy dataAll w).resolve_left h)).choose_spec set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.value_jInv_mem_maximalIdeal (fm : FibreModel N A ℓ k red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : w.value A ⟨(jBar N)⁻¹, (fm.chart_dichotomy dataAll w).resolve_left h⟩ ∈ IsLocalRing.maximalIdeal A := by have hinv := (fm.chart_dichotomy dataAll w).resolve_left h by_contra hcu have hcu' : IsUnit (w.value A ⟨(jBar N)⁻¹, hinv⟩) := by by_contra hn exact hcu ((IsLocalRing.mem_maximalIdeal _).mpr hn) obtain ⟨u, hu⟩ := hcu' have hc0 : ((w.value A ⟨(jBar N)⁻¹, hinv⟩ : A) : AlgebraicClosure ℚ) ≠ 0 := by intro h0 apply hcu have hz : w.value A ⟨(jBar N)⁻¹, hinv⟩ = 0 := Subtype.ext h0 rw [hz] exact zero_mem _ have hmul : ((u : A) : AlgebraicClosure ℚ) * (((u⁻¹ : Aˣ) : A) : AlgebraicClosure ℚ) = 1 := by exact_mod_cast congrArg (Subtype.val) (Units.mul_inv u) have hd : (((u⁻¹ : Aˣ) : A) : AlgebraicClosure ℚ) = ((w.value A ⟨(jBar N)⁻¹, hinv⟩ : A) : AlgebraicClosure ℚ)⁻¹ := by rw [← hu] at hc0 ⊢ exact eq_inv_of_mul_eq_one_right (by rw [mul_comm] at hmul ⊢; exact hmul) have hv := (w.hasValueAt_value A ⟨(jBar N)⁻¹, hinv⟩).inv hc0 rw [inv_inv, ← hd] at hv exact h (w.mem_compSubring_of_hasValueAt ((u⁻¹ : Aˣ) : A).2 hv) set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_ord_jLine_neg (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : (fm.sp hred dataAll hsep w).ord (jLine k N) < 0 := by have hinv := (fm.chart_dichotomy dataAll w).resolve_left h have hcent : (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) ∈ fm.centreInf w hinv := by show _ ∈ (w.centre A).comap (Subring.inclusion (fm.binf_le_compSubring w hinv)) rw [Ideal.mem_comap] exact (w.mem_centre_iff _).mpr (fm.value_jInv_mem_maximalIdeal dataAll w h) have hnu := (fm.sp_spec_inf hred dataAll hsep w h ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩).mpr hcent rw [show fm.piInf ⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ = (jLine k N)⁻¹ from fm.piInf_jInv] at hnu have hpos : 0 < (fm.sp hred dataAll hsep w).ord ((jLine k N : modularFunctionFieldC k N))⁻¹ := ((fm.sp hred dataAll hsep w).mem_nonunits_iff_ord_pos (inv_ne_zero (jLine_ne_zero k N))).mp hnu rw [(fm.sp hred dataAll hsep w).ord_inv] at hpos exact neg_pos.mp hpos set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_d0_j (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (a : A) (hord : 0 < w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ))) : 0 < (fm.sp hred dataAll hsep w).ord (jLine k N - algebraMap k (modularFunctionFieldC k N) (red a)) := by by_cases h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A · have hmem : (⟨jBar N, fm.jBar_mem⟩ - ⟨constantsHom N A a, fm.constFin_mem a⟩ : fm.BFin) ∈ fm.centreFin w h := by show _ ∈ (w.centre A).comap (Subring.inclusion (fm.bfin_le_compSubring w h)) rw [Ideal.mem_comap] exact w.mem_centre_of_ord_pos hord have hnu := (fm.sp_spec_fin hred dataAll hsep w h _).mpr hmem rw [map_sub, fm.piFin_j, fm.piFin_const a] at hnu exact ((fm.sp hred dataAll hsep w).mem_nonunits_iff_ord_pos (sub_ne_zero.mpr (jLine_ne_const k N (red a)))).mp hnu · exfalso apply h have hval : w.HasValueAt (jBar N) (a : AlgebraicClosure ℚ) := by rw [hasValueAt_iff] exact (w.mem_nonunits_iff_ord_pos (sub_ne_zero.mpr (jBar_ne_const N (a : AlgebraicClosure ℚ)))).mpr hord exact w.mem_compSubring_of_hasValueAt a.2 hval set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_d0_j_pole (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hpole : ∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) : (fm.sp hred dataAll hsep w).ord (jLine k N) < 0 := by by_cases h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A · exfalso have ha₀ := w.ord_sub_value_pos (f := ⟨jBar N, h⟩) (jBar_ne_const N (w.value A ⟨jBar N, h⟩ : AlgebraicClosure ℚ)) exact absurd ha₀ (not_lt.mpr (hpole (w.value A ⟨jBar N, h⟩))) · exact fm.sp_ord_jLine_neg hred dataAll hsep w h private theorem jNBar_ne_const (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) (c : AlgebraicClosure ℚ) : jNBar N ≠ algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) c := fun h => transcendental_jNBar N data hsym (h ▸ isAlgebraic_algebraMap c) private theorem jNLine_ne_const (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) (c : k) : jNLine k N ≠ algebraMap k (modularFunctionFieldC k N) c := by intro h have htr : Transcendental k (jNLine k N) := transcendental_jNC k N data hsym exact htr (h ▸ isAlgebraic_algebraMap c) private theorem jNLine_ne_zero (k : Type*) [Field k] (N : ℕ) [NeZero N] (data : ModularPolynomialData N) (hsym : EvalSymm data.Φ) : (jNLine k N : modularFunctionFieldC k N) ≠ 0 := by intro h have htr : Transcendental k (jNLine k N) := transcendental_jNC k N data hsym exact htr (h ▸ isAlgebraic_zero) set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem aeval_mem_subring {F' : Type*} [Field F'] (S : Subring F') {x : F'} (hx : x ∈ S) (p : Polynomial ℤ) : Polynomial.aeval (R := ℤ) x p ∈ S := by have hcomp : (S.subtype).comp (Polynomial.aeval (R := ℤ) (⟨x, hx⟩ : S)).toRingHom = (Polynomial.aeval (R := ℤ) x).toRingHom := by apply Polynomial.ringHom_ext · intro a simp only [eq_intCast, map_intCast] · rw [RingHom.comp_apply] rw [show (Polynomial.aeval (R := ℤ) (⟨x, hx⟩ : S)).toRingHom Polynomial.X = (⟨x, hx⟩ : S) from Polynomial.aeval_X _] rw [show (Polynomial.aeval (R := ℤ) x).toRingHom Polynomial.X = x from Polynomial.aeval_X _] rfl have h := congrArg (fun φ : Polynomial ℤ →+* F' => φ p) hcomp simp only [RingHom.coe_comp, Function.comp_apply] at h rw [show Polynomial.aeval (R := ℤ) x p = (Polynomial.aeval (R := ℤ) x).toRingHom p from rfl, ← h] exact SetLike.coe_mem _ set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem ord_nonneg_of_mem' {k' F' : Type*} [Field k'] [Field F'] [Algebra k' F'] (v : Place k' F') {x : F'} (hx : x ≠ 0) (h : x ∈ v.toValuationSubring) : 0 ≤ v.ord x := by by_contra hneg have hpos : 0 < v.ord x⁻¹ := by rw [v.ord_inv] exact neg_pos.mpr (not_le.mp hneg) have hnu : x⁻¹ ∈ v.toValuationSubring.nonunits := (v.mem_nonunits_iff_ord_pos (inv_ne_zero hx)).mpr hpos rcases (ValuationSubring.mem_nonunits_iff_or _).mp hnu with h0 | hninv · exact inv_ne_zero hx h0 · rw [inv_inv] at hninv exact hninv h set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_d0_jN (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsym : EvalSymm (dataAll N (dvd_refl N)).Φ) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (a : A) (hord : 0 < w.ord (jNBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ))) : 0 < (fm.sp hred dataAll hsep w).ord (jNLine k N - algebraMap k (modularFunctionFieldC k N) (red a)) := by by_cases h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A · have hmem : (⟨jNBar N, fm.jNBar_mem⟩ - ⟨constantsHom N A a, fm.constFin_mem a⟩ : fm.BFin) ∈ fm.centreFin w h := by show _ ∈ (w.centre A).comap (Subring.inclusion (fm.bfin_le_compSubring w h)) rw [Ideal.mem_comap] exact w.mem_centre_of_ord_pos hord have hnu := (fm.sp_spec_fin hred dataAll hsep w h _).mpr hmem rw [map_sub, fm.piFin_jN, fm.piFin_const a] at hnu exact ((fm.sp hred dataAll hsep w).mem_nonunits_iff_ord_pos (sub_ne_zero.mpr (jNLine_ne_const k N (dataAll N (dvd_refl N)) hsym (red a)))).mp hnu · exfalso apply h have hvN : (jNBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A := by refine w.mem_compSubring_of_hasValueAt a.2 ?_ rw [hasValueAt_iff] exact (w.mem_nonunits_iff_ord_pos (sub_ne_zero.mpr (jNBar_ne_const N (dataAll N (dvd_refl N)) hsym (a : AlgebraicClosure ℚ)))).mpr hord have hS : Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N}) ≤ w.compSubring A := by refine Subring.closure_le.mpr ?_ rintro x (⟨a', rfl⟩ | rfl) · exact (w.algebraMap_mem_compSubring_iff A _).mpr a'.2 · exact hvN refine w.mem_compSubring_of_isIntegral' A hS ?_ refine ⟨(dataAll N (dvd_refl N)).Φ.map ((Polynomial.aeval (R := ℤ) (⟨jNBar N, Subring.subset_closure (Set.mem_union_right _ rfl)⟩ : Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N}))).toRingHom), (dataAll N (dvd_refl N)).monic.map _, ?_⟩ rw [Polynomial.eval₂_map] have hcomp : ((algebraMap (Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N})) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))).comp ((Polynomial.aeval (R := ℤ) (⟨jNBar N, Subring.subset_closure (Set.mem_union_right _ rfl)⟩ : Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N}))).toRingHom)) = (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom := by apply Polynomial.ringHom_ext · intro b simp only [eq_intCast, map_intCast] · rw [RingHom.comp_apply] rw [show (Polynomial.aeval (R := ℤ) (⟨jNBar N, Subring.subset_closure (Set.mem_union_right _ rfl)⟩ : Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N}))).toRingHom Polynomial.X = (⟨jNBar N, Subring.subset_closure (Set.mem_union_right _ rfl)⟩ : Subring.closure (Set.range ((algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))).comp A.subtype) ∪ {jNBar N})) from Polynomial.aeval_X _] rw [show (Polynomial.aeval (R := ℤ) (jNBar N)).toRingHom Polynomial.X = jNBar N from Polynomial.aeval_X _] rfl rw [hcomp] exact barEvalSwap_subtype N (dataAll N (dvd_refl N)) hsym set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_d0_jN_pole (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsym : EvalSymm (dataAll N (dvd_refl N)).Φ) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hpole : ∀ a : A, w.ord (jNBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) : (fm.sp hred dataAll hsep w).ord (jNLine k N) < 0 := by by_cases h : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A · exfalso have hvN : (jNBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A := fm.bfin_le_compSubring w h fm.jNBar_mem have ha₀ := w.ord_sub_value_pos (f := ⟨jNBar N, hvN⟩) (jNBar_ne_const N (dataAll N (dvd_refl N)) hsym (w.value A ⟨jNBar N, hvN⟩ : AlgebraicClosure ℚ)) exact absurd ha₀ (not_lt.mpr (hpole (w.value A ⟨jNBar N, hvN⟩))) · have hjneg := fm.sp_ord_jLine_neg hred dataAll hsep w h by_contra hge have hmemN : (jNLine k N : modularFunctionFieldC k N) ∈ (fm.sp hred dataAll hsep w).toValuationSubring := mem_of_ord_nonneg _ (jNLine_ne_zero k N (dataAll N (dvd_refl N)) hsym) (not_lt.mp hge) have hmemJ : (jLine k N : modularFunctionFieldC k N) ∈ (fm.sp hred dataAll hsep w).toValuationSubring := by refine (fm.sp hred dataAll hsep w).mem_of_eval_monic_eq_zero (P := (dataAll N (dvd_refl N)).Φ.map ((Polynomial.aeval (R := ℤ) (jNLine k N)).toRingHom)) ((dataAll N (dvd_refl N)).monic.map _) (fun i => ?_) ?_ · rw [Polynomial.coeff_map] exact aeval_mem_subring (fm.sp hred dataAll hsep w).toValuationSubring.toSubring hmemN _ · rw [Polynomial.eval_map] exact fibreEvalSwap_subtype k N (dataAll N (dvd_refl N)) hsym exact absurd (ord_nonneg_of_mem' _ (jLine_ne_zero k N) hmemJ) (not_le.mpr hjneg) set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.piFin_mem_valuationSubring (fm : FibreModel N A ℓ k red) (v' : Place k (modularFunctionFieldC k N)) (hjO : (jLine k N : modularFunctionFieldC k N) ∈ v'.toValuationSubring) (b : fm.BFin) : (fm.piFin b : modularFunctionFieldC k N) ∈ v'.toValuationSubring := by obtain ⟨p, hp, hpe⟩ := fm.integralFin b have hABle : affineBaseFin N A ≤ fm.BFin := by refine Subring.closure_le.mpr ?_ rintro x (⟨a, rfl⟩ | rfl) · exact fm.constFin_mem a · exact fm.jBar_mem have hψO : ∀ (x : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (hx : x ∈ affineBaseFin N A), fm.piFin ⟨x, hABle hx⟩ ∈ v'.toValuationSubring := by intro x hx induction hx using Subring.closure_induction with | mem y hy => rcases hy with ⟨a, rfl⟩ | rfl · rw [show ∀ h : constantsHom N A a ∈ fm.BFin, fm.piFin ⟨constantsHom N A a, h⟩ = algebraMap k (modularFunctionFieldC k N) (red a) from fun _ => fm.piFin_const a] exact v'.algebraMap_mem' (red a) · rw [show ∀ h : jBar N ∈ fm.BFin, fm.piFin ⟨jBar N, h⟩ = jLine k N from fun _ => fm.piFin_j] exact hjO | one => have h1 : fm.piFin ⟨1, hABle (one_mem _)⟩ = 1 := by rw [show (⟨1, hABle (one_mem _)⟩ : fm.BFin) = 1 from Subtype.ext rfl, map_one] exact h1 ▸ one_mem _ | zero => have h0 : fm.piFin ⟨0, hABle (zero_mem _)⟩ = 0 := by rw [show (⟨0, hABle (zero_mem _)⟩ : fm.BFin) = 0 from Subtype.ext rfl, map_zero] exact h0 ▸ zero_mem _ | add y z hy hz ihy ihz => have ha : fm.piFin ⟨y + z, hABle (add_mem hy hz)⟩ = fm.piFin ⟨y, hABle hy⟩ + fm.piFin ⟨z, hABle hz⟩ := by rw [show (⟨y + z, hABle (add_mem hy hz)⟩ : fm.BFin) = ⟨y, hABle hy⟩ + ⟨z, hABle hz⟩ from Subtype.ext rfl, map_add] exact ha ▸ add_mem ihy ihz | neg y hy ihy => have hn : fm.piFin ⟨-y, hABle (neg_mem hy)⟩ = -fm.piFin ⟨y, hABle hy⟩ := by rw [show (⟨-y, hABle (neg_mem hy)⟩ : fm.BFin) = -(⟨y, hABle hy⟩ : fm.BFin) from Subtype.ext rfl, map_neg] exact hn ▸ neg_mem ihy | mul y z hy hz ihy ihz => have hm : fm.piFin ⟨y * z, hABle (mul_mem hy hz)⟩ = fm.piFin ⟨y, hABle hy⟩ * fm.piFin ⟨z, hABle hz⟩ := by rw [show (⟨y * z, hABle (mul_mem hy hz)⟩ : fm.BFin) = ⟨y, hABle hy⟩ * ⟨z, hABle hz⟩ from Subtype.ext rfl, map_mul] exact hm ▸ mul_mem ihy ihz have hq : Polynomial.eval₂ (Subring.inclusion hABle) b p = 0 := by apply Subtype.val_injective have h := Polynomial.hom_eval₂ p (Subring.inclusion hABle) fm.BFin.subtype b have hcomp : (fm.BFin.subtype).comp (Subring.inclusion hABle) = (affineBaseFin N A).subtype := by apply RingHom.ext intro x rfl rw [hcomp] at h calc (↑(Polynomial.eval₂ (Subring.inclusion hABle) b p) : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) = fm.BFin.subtype (Polynomial.eval₂ (Subring.inclusion hABle) b p) := rfl _ = Polynomial.eval₂ ((affineBaseFin N A).subtype) (fm.BFin.subtype b) p := h _ = 0 := hpe refine v'.mem_of_eval_monic_eq_zero (P := p.map (fm.piFin.comp (Subring.inclusion hABle))) (hp.map _) (fun i => ?_) ?_ · rw [Polynomial.coeff_map] exact hψO _ (p.coeff i).2 · rw [Polynomial.eval_map] have h := Polynomial.hom_eval₂ p (Subring.inclusion hABle) fm.piFin b rw [← h, hq, map_zero] set_option maxHeartbeats 3200000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.exists_sp_eq_fin (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (v' : Place k (modularFunctionFieldC k N)) (hjO : (jLine k N : modularFunctionFieldC k N) ∈ v'.toValuationSubring) : ∃ w, fm.sp hred dataAll hsep w = v' := by haveI : IsAlgClosed k := A.isAlgClosed_of_surjective red hred haveI hFD : FiniteDimensional (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (modularFunctionFieldC k N) := finiteDimensional_adjoin_jC k N (dataAll N (dvd_refl N)) haveI h1 : Module.Finite ((v'.restrict (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))).ResidueField) v'.ResidueField := rf_finite_residueField v' haveI h2 : Module.Finite k ((v'.restrict (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))).ResidueField) := by have htop : IntermediateField.adjoin k ({⟨jLine k N, IntermediateField.mem_adjoin_simple_self _ (jLine k N)⟩} : Set (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))) = ⊤ := by have h := adjoin_val_preimage_eq_top (K := k) (F := IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (S := {jLine k N}) rfl have hset : (Subtype.val ⁻¹' {jLine k N} : Set (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))) = {⟨jLine k N, IntermediateField.mem_adjoin_simple_self _ (jLine k N)⟩} := by ext z simp only [Set.mem_preimage, Set.mem_singleton_iff] exact ⟨fun hz => Subtype.ext hz, fun hz => by rw [hz]⟩ rwa [hset] at h exact AlgebraicCurve.Place.finite_residueField_of_adjoin_simple_eq_top (transcendental_subtype _ (IntermediateField.mem_adjoin_simple_self _ (jLine k N)) (transcendental_jLine k N)) htop _ haveI h3 : Module.Finite k v'.ResidueField := Module.Finite.trans ((v'.restrict (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N)))).ResidueField) v'.ResidueField have hsurj : Function.Surjective (algebraMap k v'.ResidueField) := v'.surjective_algebraMap_residueField_of_isAlgClosed let φ : fm.BFin →+* v'.toValuationSubring := fm.piFin.codRestrict v'.toValuationSubring (fm.piFin_mem_valuationSubring v' hjO) let ρ := (IsLocalRing.residue (v'.toValuationSubring : Type _)).comp φ haveI : (RingHom.ker ρ).IsPrime := RingHom.ker_isPrime ρ have h𝔮A : ∀ a : A, (⟨constantsHom N A a, fm.constFin_mem a⟩ : fm.BFin) ∈ RingHom.ker ρ ↔ a ∈ IsLocalRing.maximalIdeal A := by intro a rw [RingHom.mem_ker] have hφc : φ ⟨constantsHom N A a, fm.constFin_mem a⟩ = ⟨algebraMap k (modularFunctionFieldC k N) (red a), v'.algebraMap_mem' (red a)⟩ := by apply Subtype.ext exact fm.piFin_const a rw [show ρ ⟨constantsHom N A a, fm.constFin_mem a⟩ = IsLocalRing.residue _ (φ ⟨constantsHom N A a, fm.constFin_mem a⟩) from rfl, hφc, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff] constructor · intro h have h0 : v'.HasValueAt (algebraMap k (modularFunctionFieldC k N) (red a)) 0 := by rw [hasValueAt_zero_iff] exact h have hza : red a = 0 := ((v'.hasValueAt_algebraMap (red a)).unique h0) exact (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _ (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ) ℓ _ _ red a).mp hza · intro ha have hza : red a = 0 := (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _ (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ) ℓ _ _ red a).mpr ha show algebraMap k (modularFunctionFieldC k N) (red a) ∈ v'.toValuationSubring.nonunits rw [hza, map_zero] exact (ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inl rfl) obtain ⟨c, hc⟩ := v'.exists_hasValueAt hsurj hjO obtain ⟨a₀, rfl⟩ := hred c have hja : (⟨jBar N, fm.jBar_mem⟩ : fm.BFin) - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩ ∈ RingHom.ker ρ := by rw [RingHom.mem_ker] rw [show ρ (⟨jBar N, fm.jBar_mem⟩ - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩) = IsLocalRing.residue _ (φ (⟨jBar N, fm.jBar_mem⟩ - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩)) from rfl, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff] have hval : ((φ (⟨jBar N, fm.jBar_mem⟩ - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩) : v'.toValuationSubring) : modularFunctionFieldC k N) = jLine k N - algebraMap k (modularFunctionFieldC k N) (red a₀) := by show (fm.piFin (⟨jBar N, fm.jBar_mem⟩ - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩) : modularFunctionFieldC k N) = _ rw [map_sub, fm.piFin_j, fm.piFin_const a₀] rfl rw [hval] exact hc haveI hFDbar : FiniteDimensional (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := finiteDimensional_lineBar_of_dataAll N dataAll haveI hCZ : CharZero (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) := charZero_of_injective_algebraMap (algebraMap (AlgebraicClosure ℚ) _).injective haveI hSepBar : Algebra.IsSeparable (IntermediateField.adjoin (AlgebraicClosure ℚ) ({jBar N} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := inferInstance obtain ⟨w, hB, hcent, hval⟩ := AlgebraicCurve.Place.exists_place_centre_comap_eq A (transcendental_jBar N) fm.constFin_mem fm.jBar_mem fm.integralFin (RingHom.ker ρ) h𝔮A a₀ hja refine ⟨w, ?_⟩ have hwFin : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A := w.mem_compSubring_of_hasValueAt a₀.2 hval have hspec := fm.sp_spec_fin hred dataAll hsep w hwFin have hcent' : fm.centreFin w hwFin = RingHom.ker ρ := hcent have hjOu : (jLine k N : modularFunctionFieldC k N) ∈ (fm.sp hred dataAll hsep w).toValuationSubring := by have h1 : (⟨jBar N, fm.jBar_mem⟩ : fm.BFin) - ⟨constantsHom N A a₀, fm.constFin_mem a₀⟩ ∈ fm.centreFin w hwFin := by rw [hcent'] exact hja have h2 := (hspec _).mpr h1 rw [map_sub, fm.piFin_j, fm.piFin_const a₀] at h2 have h3 := (fm.sp hred dataAll hsep w).toValuationSubring.nonunits_subset h2 have h4 := add_mem h3 ((fm.sp hred dataAll hsep w).algebraMap_mem' (red a₀)) simpa [jLine] using h4 have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piFin.range := by intro c obtain ⟨a, rfl⟩ := hred c exact ⟨⟨constantsHom N A a, fm.constFin_mem a⟩, (fm.piFin_const a).symm ▸ rfl⟩ haveI hSepLine : Algebra.IsSeparable (IntermediateField.adjoin k ({jLine k N} : Set (modularFunctionFieldC k N))) (modularFunctionFieldC k N) := isSeparable_line_fibre k N (dataAll N (dvd_refl N)) hsep haveI hDed : IsDedekindDomain (lineClosure k N) := isDedekindDomain_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLine k N) haveI hFrac : IsFractionRing (lineClosure k N) (modularFunctionFieldC k N) := isFractionRing_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLine k N) refine AlgebraicCurve.Place.eq_of_forall_mem_nonunits_iff_of_surjective (lineClosure k N) (fun r => integralClosure_adjoin_le_valuationSubring _ (fun c => (fm.sp hred dataAll hsep w).algebraMap_mem' c) hjOu r) (fun r => integralClosure_adjoin_le_valuationSubring _ (fun c => v'.algebraMap_mem' c) hjO r) (fun b : fm.BFin => (fm.piFin b : modularFunctionFieldC k N)) (AlgebraicCurve.Place.exists_eq_of_integralClosure_adjoin (fun b : fm.BFin => (fm.piFin b : modularFunctionFieldC k N)) (fun x => RingHom.mem_range) hconstR ⟨⟨jBar N, fm.jBar_mem⟩, fm.piFin_j⟩ fm.intClosed_piFin) (fun b => ?_) rw [hspec b, hcent', RingHom.mem_ker, show ρ b = IsLocalRing.residue _ (φ b) from rfl, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff] rfl set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.piInf_mem_valuationSubring (fm : FibreModel N A ℓ k red) (v' : Place k (modularFunctionFieldC k N)) (hjO : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ v'.toValuationSubring) (b : fm.BInf) : (fm.piInf b : modularFunctionFieldC k N) ∈ v'.toValuationSubring := by obtain ⟨p, hp, hpe⟩ := fm.integralInf b have hABle : affineBaseInf N A ≤ fm.BInf := by refine Subring.closure_le.mpr ?_ rintro x (⟨a, rfl⟩ | rfl) · exact fm.constInf_mem a · exact fm.jInvBar_mem have hψO : ∀ (x : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (hx : x ∈ affineBaseInf N A), fm.piInf ⟨x, hABle hx⟩ ∈ v'.toValuationSubring := by intro x hx induction hx using Subring.closure_induction with | mem y hy => rcases hy with ⟨a, rfl⟩ | rfl · rw [show ∀ h : constantsHom N A a ∈ fm.BInf, fm.piInf ⟨constantsHom N A a, h⟩ = algebraMap k (modularFunctionFieldC k N) (red a) from fun _ => fm.piInf_const a] exact v'.algebraMap_mem' (red a) · rw [show ∀ h : (jBar N)⁻¹ ∈ fm.BInf, fm.piInf ⟨(jBar N)⁻¹, h⟩ = (jLine k N)⁻¹ from fun _ => fm.piInf_jInv] exact hjO | one => have h1 : fm.piInf ⟨1, hABle (one_mem _)⟩ = 1 := by rw [show (⟨1, hABle (one_mem _)⟩ : fm.BInf) = 1 from Subtype.ext rfl, map_one] exact h1 ▸ one_mem _ | zero => have h0 : fm.piInf ⟨0, hABle (zero_mem _)⟩ = 0 := by rw [show (⟨0, hABle (zero_mem _)⟩ : fm.BInf) = 0 from Subtype.ext rfl, map_zero] exact h0 ▸ zero_mem _ | add y z hy hz ihy ihz => have ha : fm.piInf ⟨y + z, hABle (add_mem hy hz)⟩ = fm.piInf ⟨y, hABle hy⟩ + fm.piInf ⟨z, hABle hz⟩ := by rw [show (⟨y + z, hABle (add_mem hy hz)⟩ : fm.BInf) = ⟨y, hABle hy⟩ + ⟨z, hABle hz⟩ from Subtype.ext rfl, map_add] exact ha ▸ add_mem ihy ihz | neg y hy ihy => have hn : fm.piInf ⟨-y, hABle (neg_mem hy)⟩ = -fm.piInf ⟨y, hABle hy⟩ := by rw [show (⟨-y, hABle (neg_mem hy)⟩ : fm.BInf) = -(⟨y, hABle hy⟩ : fm.BInf) from Subtype.ext rfl, map_neg] exact hn ▸ neg_mem ihy | mul y z hy hz ihy ihz => have hm : fm.piInf ⟨y * z, hABle (mul_mem hy hz)⟩ = fm.piInf ⟨y, hABle hy⟩ * fm.piInf ⟨z, hABle hz⟩ := by rw [show (⟨y * z, hABle (mul_mem hy hz)⟩ : fm.BInf) = ⟨y, hABle hy⟩ * ⟨z, hABle hz⟩ from Subtype.ext rfl, map_mul] exact hm ▸ mul_mem ihy ihz have hq : Polynomial.eval₂ (Subring.inclusion hABle) b p = 0 := by apply Subtype.val_injective have h := Polynomial.hom_eval₂ p (Subring.inclusion hABle) fm.BInf.subtype b have hcomp : (fm.BInf.subtype).comp (Subring.inclusion hABle) = (affineBaseInf N A).subtype := by apply RingHom.ext intro x rfl rw [hcomp] at h calc (↑(Polynomial.eval₂ (Subring.inclusion hABle) b p) : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) = fm.BInf.subtype (Polynomial.eval₂ (Subring.inclusion hABle) b p) := rfl _ = Polynomial.eval₂ ((affineBaseInf N A).subtype) (fm.BInf.subtype b) p := h _ = 0 := hpe refine v'.mem_of_eval_monic_eq_zero (P := p.map (fm.piInf.comp (Subring.inclusion hABle))) (hp.map _) (fun i => ?_) ?_ · rw [Polynomial.coeff_map] exact hψO _ (p.coeff i).2 · rw [Polynomial.eval_map] have h := Polynomial.hom_eval₂ p (Subring.inclusion hABle) fm.piInf b rw [← h, hq, map_zero] set_option maxHeartbeats 3200000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.exists_sp_eq_inf (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (v' : Place k (modularFunctionFieldC k N)) (hjinvO : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ v'.toValuationSubring) (hjO : ¬ (jLine k N : modularFunctionFieldC k N) ∈ v'.toValuationSubring) : ∃ w, fm.sp hred dataAll hsep w = v' := by let φ : fm.BInf →+* v'.toValuationSubring := fm.piInf.codRestrict v'.toValuationSubring (fm.piInf_mem_valuationSubring v' hjinvO) let ρ := (IsLocalRing.residue (v'.toValuationSubring : Type _)).comp φ haveI : (RingHom.ker ρ).IsPrime := RingHom.ker_isPrime ρ have h𝔮A : ∀ a : A, (⟨constantsHom N A a, fm.constInf_mem a⟩ : fm.BInf) ∈ RingHom.ker ρ ↔ a ∈ IsLocalRing.maximalIdeal A := by intro a rw [RingHom.mem_ker] have hφc : φ ⟨constantsHom N A a, fm.constInf_mem a⟩ = ⟨algebraMap k (modularFunctionFieldC k N) (red a), v'.algebraMap_mem' (red a)⟩ := by apply Subtype.ext exact fm.piInf_const a rw [show ρ ⟨constantsHom N A a, fm.constInf_mem a⟩ = IsLocalRing.residue _ (φ ⟨constantsHom N A a, fm.constInf_mem a⟩) from rfl, hφc, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff] constructor · intro h have h0 : v'.HasValueAt (algebraMap k (modularFunctionFieldC k N) (red a)) 0 := by rw [hasValueAt_zero_iff] exact h have hza : red a = 0 := ((v'.hasValueAt_algebraMap (red a)).unique h0) exact (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _ (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ) ℓ _ _ red a).mp hza · intro ha have hza : red a = 0 := (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _ (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ) ℓ _ _ red a).mpr ha show algebraMap k (modularFunctionFieldC k N) (red a) ∈ v'.toValuationSubring.nonunits rw [hza, map_zero] exact (ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inl rfl) have hjnu : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ v'.toValuationSubring.nonunits := by refine (ValuationSubring.mem_nonunits_iff_or _).mpr (Or.inr ?_) rwa [inv_inv] have hja : (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) - ⟨constantsHom N A 0, fm.constInf_mem 0⟩ ∈ RingHom.ker ρ := by rw [RingHom.mem_ker] rw [show ρ (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ - ⟨constantsHom N A 0, fm.constInf_mem 0⟩) = IsLocalRing.residue _ (φ (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ - ⟨constantsHom N A 0, fm.constInf_mem 0⟩)) from rfl, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff] have hval : ((φ (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ - ⟨constantsHom N A 0, fm.constInf_mem 0⟩) : v'.toValuationSubring) : modularFunctionFieldC k N) = ((jLine k N)⁻¹ : modularFunctionFieldC k N) := by show (fm.piInf (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ - ⟨constantsHom N A 0, fm.constInf_mem 0⟩) : modularFunctionFieldC k N) = _ rw [map_sub, fm.piInf_jInv, fm.piInf_const 0, map_zero, map_zero, sub_zero] rfl rw [hval] exact hjnu have htrinv : Transcendental (AlgebraicClosure ℚ) ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := by intro halg exact transcendental_jBar N (inv_inv (jBar N) ▸ halg.inv) haveI hFDbar : FiniteDimensional (IntermediateField.adjoin (AlgebraicClosure ℚ) ({(jBar N)⁻¹} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := by rw [IntermediateField.adjoin_simple_inv_eq (jBar N)] exact finiteDimensional_lineBar_of_dataAll N dataAll haveI hCZ : CharZero (IntermediateField.adjoin (AlgebraicClosure ℚ) ({(jBar N)⁻¹} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) := charZero_of_injective_algebraMap (algebraMap (AlgebraicClosure ℚ) _).injective haveI hSepBar : Algebra.IsSeparable (IntermediateField.adjoin (AlgebraicClosure ℚ) ({(jBar N)⁻¹} : Set (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)))) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) := inferInstance obtain ⟨w, hB, hcent, hval⟩ := AlgebraicCurve.Place.exists_place_centre_comap_eq A htrinv fm.constInf_mem fm.jInvBar_mem fm.integralInf (RingHom.ker ρ) h𝔮A 0 (by simpa using hja) refine ⟨w, ?_⟩ have hval0 : ((jBar N)⁻¹ : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.toValuationSubring.nonunits := by have h := hval rw [HasValueAt] at h rwa [show ((0 : A) : AlgebraicClosure ℚ) = 0 from rfl, map_zero, sub_zero] at h have hwInf : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A := by intro hmem obtain ⟨c, hc⟩ := (w.mem_compSubring_iff (A := A)).mp hmem have hjne : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ≠ 0 := fun h => transcendental_jBar N (h ▸ isAlgebraic_zero) have hjmem : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.toValuationSubring := by have h1 := w.toValuationSubring.nonunits_subset hc have h2 := add_mem h1 (w.algebraMap_mem' (c : AlgebraicClosure ℚ)) simpa using h2 have h𝔪 : (⟨(jBar N)⁻¹, w.toValuationSubring.nonunits_subset hval0⟩ : w.toValuationSubring) ∈ IsLocalRing.maximalIdeal _ := by rw [← ValuationSubring.coe_mem_nonunits_iff] exact hval0 have hone : (⟨jBar N, hjmem⟩ : w.toValuationSubring) * ⟨(jBar N)⁻¹, w.toValuationSubring.nonunits_subset hval0⟩ = 1 := by apply Subtype.ext show (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) * (jBar N)⁻¹ = 1 exact mul_inv_cancel₀ hjne have htop : (1 : w.toValuationSubring) ∈ IsLocalRing.maximalIdeal _ := by rw [← hone] exact Ideal.mul_mem_left _ _ h𝔪 exact (IsLocalRing.maximalIdeal.isMaximal _).ne_top (Ideal.eq_top_of_isUnit_mem _ htop isUnit_one) have hspec := fm.sp_spec_inf hred dataAll hsep w hwInf have hcent' : fm.centreInf w ((fm.chart_dichotomy dataAll w).resolve_left hwInf) = RingHom.ker ρ := hcent have hjinvOu : (((jLine k N)⁻¹ : modularFunctionFieldC k N)) ∈ (fm.sp hred dataAll hsep w).toValuationSubring := by have h1 : (⟨(jBar N)⁻¹, fm.jInvBar_mem⟩ : fm.BInf) - ⟨constantsHom N A 0, fm.constInf_mem 0⟩ ∈ fm.centreInf w ((fm.chart_dichotomy dataAll w).resolve_left hwInf) := by rw [hcent'] exact hja have h2 := (hspec _).mpr h1 rw [map_sub, fm.piInf_jInv, fm.piInf_const 0, map_zero, map_zero, sub_zero] at h2 exact (fm.sp hred dataAll hsep w).toValuationSubring.nonunits_subset h2 have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piInf.range := by intro c obtain ⟨a, rfl⟩ := hred c exact ⟨⟨constantsHom N A a, fm.constInf_mem a⟩, (fm.piInf_const a).symm ▸ rfl⟩ haveI hSepLine : Algebra.IsSeparable (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N)))) (modularFunctionFieldC k N) := by rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)] exact isSeparable_line_fibre k N (dataAll N (dvd_refl N)) hsep haveI hFDLine : FiniteDimensional (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N)))) (modularFunctionFieldC k N) := by rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)] exact finiteDimensional_adjoin_jC k N (dataAll N (dvd_refl N)) haveI hDed : IsDedekindDomain (lineClosureInf k N) := isDedekindDomain_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLineInv k N) haveI hFrac : IsFractionRing (lineClosureInf k N) (modularFunctionFieldC k N) := isFractionRing_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLineInv k N) refine AlgebraicCurve.Place.eq_of_forall_mem_nonunits_iff_of_surjective (lineClosureInf k N) (fun r => integralClosure_adjoin_le_valuationSubring _ (fun c => (fm.sp hred dataAll hsep w).algebraMap_mem' c) hjinvOu r) (fun r => integralClosure_adjoin_le_valuationSubring _ (fun c => v'.algebraMap_mem' c) hjinvO r) (fun b : fm.BInf => (fm.piInf b : modularFunctionFieldC k N)) (AlgebraicCurve.Place.exists_eq_of_integralClosure_adjoin (fun b : fm.BInf => (fm.piInf b : modularFunctionFieldC k N)) (fun x => RingHom.mem_range) hconstR ⟨⟨(jBar N)⁻¹, fm.jInvBar_mem⟩, fm.piInf_jInv⟩ fm.intClosed_piInf) (fun b => ?_) rw [hspec b, hcent', RingHom.mem_ker, show ρ b = IsLocalRing.residue _ (φ b) from rfl, IsLocalRing.residue_eq_zero_iff, ← ValuationSubring.coe_mem_nonunits_iff] rfl set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_d4 (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) : Function.Surjective (fm.sp hred dataAll hsep) := by intro v' by_cases hjO : (jLine k N : modularFunctionFieldC k N) ∈ v'.toValuationSubring · exact fm.exists_sp_eq_fin hred dataAll hsep v' hjO · exact fm.exists_sp_eq_inf hred dataAll hsep v' ((v'.toValuationSubring.mem_or_inv_mem _).resolve_left hjO) hjO set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.exists_specializationMap_assembled (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsym : EvalSymm (dataAll N (dvd_refl N)).Φ) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (fm : FibreModel N A ℓ k red) : ∃ sp : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) → Place k (modularFunctionFieldC k N), (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), ∀ a : A, 0 < w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) → 0 < (sp w).ord ((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) - algebraMap k (modularFunctionFieldC k N) (red a))) ∧ (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), (∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) → (sp w).ord ((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)) < 0) ∧ (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), ∀ a : A, 0 < w.ord (jNBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) → 0 < (sp w).ord ((⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) - algebraMap k (modularFunctionFieldC k N) (red a))) ∧ (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), (∀ a : A, w.ord (jNBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) → (sp w).ord ((⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)) < 0) ∧ Function.Surjective sp := ⟨fm.sp hred dataAll hsep, fun w a h => fm.sp_d0_j hred dataAll hsep w a h, fun w h => fm.sp_d0_j_pole hred dataAll hsep w h, fun w a h => fm.sp_d0_jN hred dataAll hsym hsep w a h, fun w h => fm.sp_d0_jN_pole hred dataAll hsym hsep w h, fm.sp_d4 hred dataAll hsep⟩ set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_hasValueAt_inf (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) (b : fm.BInf) (a : A) (hb : w.HasValueAt (b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) : (fm.sp hred dataAll hsep w).HasValueAt (fm.piInf b : modularFunctionFieldC k N) (red a) := by have hinv := (fm.chart_dichotomy dataAll w).resolve_left h set b' : fm.BInf := b - ⟨constantsHom N A a, fm.constInf_mem a⟩ with hb' have hcentmem : b' ∈ fm.centreInf w hinv := by rw [FibreModel.centreInf, Ideal.mem_comap] refine (w.mem_centre_iff_of_hasValueAt (a := (0 : A)) ?_).mpr (zero_mem _) show w.HasValueAt ((b' : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) ((0 : A) : AlgebraicClosure ℚ) show (b' : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) - algebraMap _ _ ((0 : A) : AlgebraicClosure ℚ) ∈ w.toValuationSubring.nonunits rw [show (((0 : A) : AlgebraicClosure ℚ)) = 0 from rfl, map_zero, sub_zero] show ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) - constantsHom N A a) ∈ w.toValuationSubring.nonunits exact hb have h2 := (fm.sp_spec_inf hred dataAll hsep w h b').mpr hcentmem rw [hb', map_sub, fm.piInf_const a] at h2 exact h2 set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_piInf_nonunits_iff (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) (b : fm.BInf) : (fm.piInf b : modularFunctionFieldC k N) ∈ (fm.sp hred dataAll hsep w).toValuationSubring.nonunits ↔ w.value A (Subring.inclusion (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b) ∈ IsLocalRing.maximalIdeal A := by rw [fm.sp_spec_inf hred dataAll hsep w h b] rw [FibreModel.centreInf, Ideal.mem_comap] exact w.mem_centre_iff _ set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_jLineInv_mem (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) : (((jLine k N)⁻¹ : modularFunctionFieldC k N)) ∈ (fm.sp hred dataAll hsep w).toValuationSubring := by have hneg := fm.sp_ord_jLine_neg hred dataAll hsep w h refine mem_of_ord_nonneg _ (inv_ne_zero (jLine_ne_zero k N)) ?_ rw [(fm.sp hred dataAll hsep w).ord_inv] exact (neg_pos.mpr hneg).le set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.fibre_place_ext_inf_impl (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (v₁ v₂ : Place k (modularFunctionFieldC k N)) (h₁ : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ v₁.toValuationSubring) (h₂ : ((jLine k N)⁻¹ : modularFunctionFieldC k N) ∈ v₂.toValuationSubring) (hagree : ∀ b : fm.BInf, ((fm.piInf b : modularFunctionFieldC k N) ∈ v₁.toValuationSubring.nonunits ↔ (fm.piInf b : modularFunctionFieldC k N) ∈ v₂.toValuationSubring.nonunits)) : v₁ = v₂ := by have hconstR : ∀ c : k, algebraMap k (modularFunctionFieldC k N) c ∈ fm.piInf.range := by intro c obtain ⟨a, rfl⟩ := hred c exact ⟨⟨constantsHom N A a, fm.constInf_mem a⟩, (fm.piInf_const a).symm ▸ rfl⟩ haveI hSepLine : Algebra.IsSeparable (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N)))) (modularFunctionFieldC k N) := by rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)] exact isSeparable_line_fibre k N (dataAll N (dvd_refl N)) hsep haveI hFDLine : FiniteDimensional (IntermediateField.adjoin k (({(jLine k N)⁻¹} : Set (modularFunctionFieldC k N)))) (modularFunctionFieldC k N) := by rw [IntermediateField.adjoin_simple_inv_eq (jLine k N)] exact finiteDimensional_adjoin_jC k N (dataAll N (dvd_refl N)) haveI hDed : IsDedekindDomain (lineClosureInf k N) := isDedekindDomain_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLineInv k N) haveI hFrac : IsFractionRing (lineClosureInf k N) (modularFunctionFieldC k N) := isFractionRing_integralClosure_adjoin (K := k) (F := modularFunctionFieldC k N) (transcendental_jLineInv k N) exact AlgebraicCurve.Place.eq_of_forall_mem_nonunits_iff_of_surjective (lineClosureInf k N) (fun r => integralClosure_adjoin_le_valuationSubring _ (fun c => v₁.algebraMap_mem' c) h₁ r) (fun r => integralClosure_adjoin_le_valuationSubring _ (fun c => v₂.algebraMap_mem' c) h₂ r) (fun b : fm.BInf => (fm.piInf b : modularFunctionFieldC k N)) (AlgebraicCurve.Place.exists_eq_of_integralClosure_adjoin (fun b : fm.BInf => (fm.piInf b : modularFunctionFieldC k N)) (fun x => RingHom.mem_range) hconstR ⟨⟨(jBar N)⁻¹, fm.jInvBar_mem⟩, fm.piInf_jInv⟩ fm.intClosed_piInf) hagree set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem not_jBar_mem_compSubring_of_forall_ord_le (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hpole : ∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A := by intro hmem have ha₀ := w.ord_sub_value_pos (f := ⟨jBar N, hmem⟩) (jBar_ne_const N (w.value A ⟨jBar N, hmem⟩ : AlgebraicClosure ℚ)) exact absurd ha₀ (not_lt.mpr (hpole (w.value A ⟨jBar N, hmem⟩))) set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.exists_specializationMap_dict_impl (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsym : EvalSymm (dataAll N (dvd_refl N)).Φ) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (fm : FibreModel N A ℓ k red) : ∃ sp : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) → Place k (modularFunctionFieldC k N), (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), ∀ a : A, 0 < w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) → 0 < (sp w).ord ((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) - algebraMap k (modularFunctionFieldC k N) (red a))) ∧ (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), (∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) → (sp w).ord ((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N)) < 0) ∧ (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), ∀ a : A, 0 < w.ord (jNBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) → 0 < (sp w).ord ((⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) - algebraMap k (modularFunctionFieldC k N) (red a))) ∧ (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), (∀ a : A, w.ord (jNBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) → (sp w).ord ((⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N)) < 0) ∧ Function.Surjective sp ∧ (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), (∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) → ∀ b : fm.BInf, ∀ a : A, ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ∈ w.toValuationSubring.nonunits → ((fm.piInf b : modularFunctionFieldC k N) - algebraMap k (modularFunctionFieldC k N) (red a)) ∈ (sp w).toValuationSubring.nonunits) ∧ (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), (∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) → (((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N))⁻¹ ∈ (sp w).toValuationSubring)) ∧ (∀ w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)), (∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) → ∀ b : fm.BInf, ((fm.piInf b : modularFunctionFieldC k N) ∈ (sp w).toValuationSubring.nonunits ↔ ∃ a : A, a ∈ IsLocalRing.maximalIdeal A ∧ ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ∈ w.toValuationSubring.nonunits)) := ⟨fm.sp hred dataAll hsep, fun w a h => fm.sp_d0_j hred dataAll hsep w a h, fun w h => fm.sp_d0_j_pole hred dataAll hsep w h, fun w a h => fm.sp_d0_jN hred dataAll hsym hsep w a h, fun w h => fm.sp_d0_jN_pole hred dataAll hsym hsep w h, fm.sp_d4 hred dataAll hsep, fun w hpole b a hb => fm.sp_hasValueAt_inf hred dataAll hsep w (not_jBar_mem_compSubring_of_forall_ord_le w hpole) b a hb, fun w hpole => fm.sp_jLineInv_mem hred dataAll hsep w (not_jBar_mem_compSubring_of_forall_ord_le w hpole), fun w hpole b => by have h := not_jBar_mem_compSubring_of_forall_ord_le w hpole constructor · intro hnu have hval := (fm.sp_piInf_nonunits_iff hred dataAll hsep w h b).mp hnu exact ⟨w.value A (Subring.inclusion (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b), hval, w.hasValueAt_value A (Subring.inclusion (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b)⟩ · rintro ⟨a, ha𝔪, hval⟩ have ht : ((fm.piInf b : modularFunctionFieldC k N) - algebraMap k (modularFunctionFieldC k N) (red a)) ∈ (fm.sp hred dataAll hsep w).toValuationSubring.nonunits := fm.sp_hasValueAt_inf hred dataAll hsep w h b a hval have hred0 : red a = 0 := (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _ (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ) ℓ _ _ red a).mpr ha𝔪 rwa [hred0, map_zero, sub_zero] at ht⟩ set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in private theorem FibreModel.sp_piInf_nonunits_iff_of_hasValueAt (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (h : ¬ (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A) (b : fm.BInf) (a : A) (hb : w.HasValueAt (b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) : (fm.piInf b : modularFunctionFieldC k N) ∈ (fm.sp hred dataAll hsep w).toValuationSubring.nonunits ↔ a ∈ IsLocalRing.maximalIdeal A := by rw [fm.sp_piInf_nonunits_iff hred dataAll hsep w h b, w.value_eq_of_hasValueAt (f := Subring.inclusion (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b) hb] noncomputable def FibreModel.spPlace (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) → Place k (modularFunctionFieldC k N) := fm.sp hred dataAll hsep noncomputable def FibreModel.spDiv (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N) → Divisor k (modularFunctionFieldC k N) := Finsupp.mapDomain (fm.spPlace hred dataAll hsep) def FibreModel.SpDivPreservesPrincipal (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) : Prop := (∀ D ∈ Divisor.degZero (K := AlgebraicClosure ℚ) (F := modularFunctionFieldBar N), fm.spDiv hred dataAll hsep D ∈ Divisor.degZero (K := k) (F := modularFunctionFieldC k N)) ∧ (∀ D ∈ Divisor.degZero (K := AlgebraicClosure ℚ) (F := modularFunctionFieldBar N), D ∈ Divisor.principal (K := AlgebraicClosure ℚ) (F := modularFunctionFieldBar N) → fm.spDiv hred dataAll hsep D ∈ Divisor.principal (K := k) (F := modularFunctionFieldC k N)) open Classical in noncomputable def FibreModel.spPic0 (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) : JZero N →+ Pic0 k (modularFunctionFieldC k N) := if h : fm.SpDivPreservesPrincipal hred dataAll hsep then QuotientAddGroup.map _ _ (AddMonoidHom.mk' (fun D => ⟨fm.spDiv hred dataAll hsep ↑D, h.1 ↑D D.2⟩) (fun D E => Subtype.ext (by show fm.spDiv hred dataAll hsep ↑(D + E) = fm.spDiv hred dataAll hsep ↑D + fm.spDiv hred dataAll hsep ↑E rw [AddSubgroup.coe_add] exact Finsupp.mapDomain_add))) (fun D hD => AddSubgroup.mem_comap.mpr ((AddSubgroup.mem_addSubgroupOf).mpr (h.2 ↑D D.2 ((AddSubgroup.mem_addSubgroupOf).mp hD)))) else 0 set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in theorem FibreModel.piInf_mem_spPlace_nonunits_iff (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hpole : ∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) (b : fm.BInf) : ((fm.piInf b : modularFunctionFieldC k N) ∈ (fm.spPlace hred dataAll hsep w).toValuationSubring.nonunits ↔ ∃ a : A, a ∈ IsLocalRing.maximalIdeal A ∧ ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ∈ w.toValuationSubring.nonunits) := by have h := not_jBar_mem_compSubring_of_forall_ord_le w hpole constructor · intro hnu have hval := (fm.sp_piInf_nonunits_iff hred dataAll hsep w h b).mp hnu exact ⟨w.value A (Subring.inclusion (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b), hval, w.hasValueAt_value A (Subring.inclusion (fm.binf_le_compSubring w ((fm.chart_dichotomy dataAll w).resolve_left h)) b)⟩ · rintro ⟨a, ha, hval⟩ have ht : ((fm.piInf b : modularFunctionFieldC k N) - algebraMap k (modularFunctionFieldC k N) (red a)) ∈ (fm.spPlace hred dataAll hsep w).toValuationSubring.nonunits := fm.sp_hasValueAt_inf hred dataAll hsep w h b a hval have hred0 : red a = 0 := (@ValuationSubring.ker_eq_maximalIdeal_apply _ _ A _ _ (AlgebraicClosure.instAlgebra ℚ) (AlgebraicClosure.isAlgebraic ℚ) ℓ _ _ red a).mpr ha rwa [hred0, map_zero, sub_zero] at ht set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in theorem FibreModel.piFin_mem_spPlace_nonunits_iff (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (a₀ : A) (ha₀ : 0 < w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a₀ : AlgebraicClosure ℚ))) (b : fm.BFin) : ((fm.piFin b : modularFunctionFieldC k N) ∈ (fm.spPlace hred dataAll hsep w).toValuationSubring.nonunits ↔ ∃ a : A, a ∈ IsLocalRing.maximalIdeal A ∧ ((b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ∈ w.toValuationSubring.nonunits) := by have hmem : (jBar N : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ∈ w.compSubring A := w.mem_compSubring_of_hasValueAt a₀.2 (w.hasValueAt_of_ord_pos ha₀) have hspec := fm.sp_spec_fin hred dataAll hsep w hmem b constructor · intro hnu have hcent := hspec.mp hnu rw [FibreModel.centreFin, Ideal.mem_comap] at hcent exact ⟨w.value A (Subring.inclusion (fm.bfin_le_compSubring w hmem) b), (w.mem_centre_iff _).mp hcent, w.hasValueAt_value A (Subring.inclusion (fm.bfin_le_compSubring w hmem) b)⟩ · rintro ⟨a, ha, hval⟩ refine hspec.mpr ?_ rw [FibreModel.centreFin, Ideal.mem_comap] have hval' : w.HasValueAt (Subring.inclusion (fm.bfin_le_compSubring w hmem) b : laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) ↑a := hval exact (w.mem_centre_iff_of_hasValueAt hval').mpr ha set_option maxHeartbeats 800000 in set_option synthInstance.maxHeartbeats 400000 in theorem FibreModel.jLineInv_mem_spPlace (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (w : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N))) (hpole : ∀ a : A, w.ord (jBar N - algebraMap (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull N)) (a : AlgebraicClosure ℚ)) ≤ 0) : (((⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N))⁻¹ ∈ (fm.spPlace hred dataAll hsep w).toValuationSubring) := fm.sp_jLineInv_mem hred dataAll hsep w (not_jBar_mem_compSubring_of_forall_ord_le w hpole) set_option maxHeartbeats 1600000 in set_option synthInstance.maxHeartbeats 400000 in noncomputable def FibreModel.placeSpecializationOf (fm : FibreModel N A ℓ k red) (hred : Function.Surjective red) (dataAll : ∀ (d : ℕ) [NeZero d], d ∣ N → ModularPolynomialData d) (hsep : (((dataAll N (dvd_refl N)).Φ.map (Polynomial.mapRingHom (Int.castRingHom k))).map (algebraMap (Polynomial k) (RatFunc k))).Separable) (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data) (hα : HeckeAlphaBarIntegral (AlgebraicClosure ℚ) N ℓ) (hβ : HeckeBetaBarIntegral (AlgebraicClosure ℚ) N ℓ) (h_d0_j : ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N), ∀ a : A, 0 < w.ord (⟨coeffEmb (AlgebraicClosure ℚ) jq, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full N (jq_mem N))⟩ - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N) (a : AlgebraicClosure ℚ)) → 0 < ((fm.spPlace hred dataAll hsep) w).ord (⟨jqModC k, jqModC_mem k N⟩ - algebraMap k (modularFunctionFieldC k N) (red a))) (h_d0_j_pole : ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N), (∀ a : A, w.ord (⟨coeffEmb (AlgebraicClosure ℚ) jq, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full N (jq_mem N))⟩ - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N) (a : AlgebraicClosure ℚ)) ≤ 0) → ((fm.spPlace hred dataAll hsep) w).ord (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) < 0) (h_d0_jN : ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N), ∀ a : A, 0 < w.ord (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq), coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jqd_mem_full N (dvd_refl N))⟩ - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N) (a : AlgebraicClosure ℚ)) → 0 < ((fm.spPlace hred dataAll hsep) w).ord (⟨jqNModC k N, jqNModC_mem k N⟩ - algebraMap k (modularFunctionFieldC k N) (red a))) (h_d0_jN_pole : ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N), (∀ a : A, w.ord (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq), coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jqd_mem_full N (dvd_refl N))⟩ - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N) (a : AlgebraicClosure ℚ)) ≤ 0) → ((fm.spPlace hred dataAll hsep) w).ord (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) < 0) (h_d1 : ∀ W : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull (N * ℓ))), (fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ) hα) = frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ) hβ)) ∨ frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ) hα)) = (fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ) hβ)) (h_d2 : ∀ v : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N), frobOnPlacesGeomLevel k N data hKr (frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) v)) ≠ (fm.spPlace hred dataAll hsep) v → ∃ W₀ : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull (N * ℓ))), W₀.restrictAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ) hβ = v ∧ (fm.spPlace hred dataAll hsep) (W₀.restrictAlong (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ) hα) = frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) v) ∧ W₀.ramificationIndexAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ) = 1 ∧ ∀ W : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionFieldFull (N * ℓ))), W.restrictAlong (heckeBetaBar (AlgebraicClosure ℚ) N ℓ) hβ = v → (fm.spPlace hred dataAll hsep) (W.restrictAlong (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ) hα) = frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) v) → W = W₀) (h_d4 : Function.Surjective (fm.spPlace hred dataAll hsep)) (h_d5 : ∀ f : modularFunctionFieldBar N, f ≠ 0 → ∀ D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N), (∀ v, D v = v.ord f) → ∃ g : modularFunctionFieldC k N, g ≠ 0 ∧ ∀ v' : Place k (modularFunctionFieldC k N), Finsupp.mapDomain (fm.spPlace hred dataAll hsep) D v' = v'.ord g) (h_d6_inertia : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, σ ∈ A.inertiaSubgroupIn ℚ → ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N), (fm.spPlace hred dataAll hsep) (arithmeticGalois (modularFunctionFieldFull N) σ • w) = (fm.spPlace hred dataAll hsep) w) (h_d6_frobenius : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, A.IsFrobeniusAt σ ℓ → ∀ w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N), (fm.spPlace hred dataAll hsep) (arithmeticGalois (modularFunctionFieldFull N) σ • w) = frobOnPlacesGeomLevel k N data hKr ((fm.spPlace hred dataAll hsep) w)) (h_d7_dictInfty : ∀ (w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) (τ : A) (ht : (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq), coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jqd_mem_full N (dvd_refl N))⟩ : modularFunctionFieldBar N) / (⟨coeffEmb (AlgebraicClosure ℚ) jq, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full N (jq_mem N))⟩ : modularFunctionFieldBar N) ^ N ∈ w.toValuationSubring), (∀ a : A, w.ord (⟨coeffEmb (AlgebraicClosure ℚ) jq, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full N (jq_mem N))⟩ - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N) (a : AlgebraicClosure ℚ)) ≤ 0) → IsLocalRing.residue w.toValuationSubring ⟨_, ht⟩ = algebraMap (AlgebraicClosure ℚ) w.ResidueField (τ : AlgebraicClosure ℚ) → ⟨jqNModC k N, jqNModC_mem k N⟩ / (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) ^ N - algebraMap k (modularFunctionFieldC k N) (red τ) = 0 ∨ 0 < ((fm.spPlace hred dataAll hsep) w).ord (⟨jqNModC k N, jqNModC_mem k N⟩ / (⟨jqModC k, jqModC_mem k N⟩ : modularFunctionFieldC k N) ^ N - algebraMap k (modularFunctionFieldC k N) (red τ))) (h_d7_dictZero : ∀ (w : Place (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) (τ : A) (ht : (⟨coeffEmb (AlgebraicClosure ℚ) jq, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full N (jq_mem N))⟩ : modularFunctionFieldBar N) / (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq), coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jqd_mem_full N (dvd_refl N))⟩ : modularFunctionFieldBar N) ^ N ∈ w.toValuationSubring), (∀ a : A, w.ord (⟨coeffEmb (AlgebraicClosure ℚ) (qExpand ℚ N jq), coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (jqd_mem_full N (dvd_refl N))⟩ - algebraMap (AlgebraicClosure ℚ) (modularFunctionFieldBar N) (a : AlgebraicClosure ℚ)) ≤ 0) → IsLocalRing.residue w.toValuationSubring ⟨_, ht⟩ = algebraMap (AlgebraicClosure ℚ) w.ResidueField (τ : AlgebraicClosure ℚ) → ⟨jqModC k, jqModC_mem k N⟩ / (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) ^ N - algebraMap k (modularFunctionFieldC k N) (red τ) = 0 ∨ 0 < ((fm.spPlace hred dataAll hsep) w).ord (⟨jqModC k, jqModC_mem k N⟩ / (⟨jqNModC k N, jqNModC_mem k N⟩ : modularFunctionFieldC k N) ^ N - algebraMap k (modularFunctionFieldC k N) (red τ))) (h_spPic0_compat : ∀ D : Divisor.degZero (K := AlgebraicClosure ℚ) (F := ↥(modularFunctionFieldBar N)), ∃ D' : Divisor.degZero (K := k) (F := ↥(modularFunctionFieldC k N)), (D' : Divisor k (modularFunctionFieldC k N)) = Finsupp.mapDomain (fm.spPlace hred dataAll hsep) (D : Divisor (AlgebraicClosure ℚ) (modularFunctionFieldBar N)) ∧ (fm.spPic0 hred dataAll hsep) (Pic0.mk D) = Pic0.mk D') : PlaceSpecialization A ℓ N data hKr k red hα hβ := ⟨fm.spPlace hred dataAll hsep, fm.spPic0 hred dataAll hsep, h_d0_j, h_d0_j_pole, h_d0_jN, h_d0_jN_pole, h_d1, h_d2, h_d4, h_d5, h_d6_inertia, h_d6_frobenius, h_d7_dictInfty, h_d7_dictZero, h_spPic0_compat⟩ end SpecializationConstruction end CharPModel end ModularCurve