Definitions/Def_ModularCurve_RigidDescentNodesConclusion.lean
Conclusion predicate for rigid descent at supersingular nodes
RigidDescentNodesConclusion packages, as a single Prop-valued definition, the conclusion of the rigid-descent assertion about the q+1 nodes lying over a supersingular place. Its parameters form the frame shared with the statements that consume it: a prime q and a level M'; a valuation subring A of \overline{\mathbb Q}, a finite set W of places of the level-M' function field over the residue field of A with a chosen s \in W, and a constant reduction R_0 of the geometric level-M' function field; a subfield k_0 of \overline{\mathbb Q} with elements \pi_0 (lying in A), \varpi_t and \xi; an auxiliary prime \ell', an intermediate field K_\ell of the Laurent series over k_0 containing the q\ell'-th j-expansion and a nonzero j_\ell \in K_\ell; a constant a_0, a subfield K_0 \subseteq K_\ell, a subalgebra B_0 and a valuation subring W_0' of K_0; together with further auxiliary data (fields, valuation rings, uniformisers, an ideal, automorphisms, indices, a finite set of subrings and a subgroup), summarised here.
The conjunction asserts: the j-expansion is R_0-integral, its residue is s-integral, and \mathrm{res}_A(a_0)^q is the value of that residue at s (a Hasse-type q-th root of the supersingular j-invariant); and there is a finite set nodes of subrings of K_0 of cardinality q+1 such that (i) every node is a localisation of one subring generated over the constants of A by finitely many elements; (ii) the automorphisms of K_\ell realising \Gamma_0(M') through IsLevelAutAt permute the nodes, transitively; (iii) distinct nodes are separated by an element that is a unit in one and not in the other; (iv) a valuation subring of K_0 whose constants are exactly A and which specialises R_0-integral modular functions as prescribed by s either contains B_0 or dominates a node; and (v) for each node O: O \subseteq W_0', O is local and noetherian with constants and residues coming from A, and its \mathfrak m-adic completion is isomorphic, compatibly with constants, to the crossing model \hat A[[U,V]]/(UV-\pi_0^{E_0}), where \pi_0^{E_0} equals \varpi_t^{2w} times a unit of A, w being placeWidthChar of s; branch coordinates c_x, c_y with c_xc_y = \pi_0^{E_0}u correspond to unit multiples of U and V, with c_y in the maximal ideal of W_0' and c_x a unit there, while j_{q\ell'} - a_0 corresponds to a unit times V^e with e \ge 1; finally a node-adapted discrete valuation subring W_x with uniformiser \pi_0 selecting the opposite branch, subject to a Gauss-type coefficient clause, to clauses relating R_0-residues to membership in its maximal ideal and in O, and separating O from the other nodes; and a subring B_x of B_0 \cap O whose elements have no poles outside the poles of j_\ell, of which O is a localisation, which generates K_0 as a field of fractions, and which contains an element detecting the valuation subrings that fail to contain O.
Relation to Mathlib
Everything is expressed through local subrings of function fields rather than schemes: nodes are subrings of K_0 and the nodal shape is recorded by an isomorphism of the \mathfrak m-adic completion onto the project's UVCrossingModel, the quotient W[[U,V]]/(UV-\pi) of a two-variable power series ring. ConstantReduction, placeWidthChar and IsLevelAutAt are likewise project notions; Mathlib supplies the ambient ValuationSubring, AdicCompletion, MvPowerSeries and IsDiscreteValuationRing.
Where it is used
The predicate is the shared conclusion of the statements describing the q+1 nodes above a supersingular place on a descended integral model of the modular curve of level q^2M', and the crossing and branch data it records feed the analysis of the special fibre and component group at q used in the level-lowering part of the proof.
References
- P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, in: Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316
- K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476
- H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
References are suggested automatically and have not been individually verified.
English text generated automatically from the Lean source; the Lean statement is authoritative.
- 192 lines
- 1 declarations
- used in the statements of 1 theorems and imported by 2 proofs
- imports 16 definition modules
Source file: Definitions/Def_ModularCurve_RigidDescentNodesConclusion.lean
Imports
Def_ModularCurve_FullLevelSemistableCoveringDef_ModularCurve_SupersingularNodePlacesDef_AlgebraicCurve_ConstantReductionDef_FLTPrelim_RamificationDef_AlgebraicCurve_RegularProlongationDef_AlgebraicCurve_ResidueDiscsDef_ModularCurve_PlaceWidthCharDef_ModularCurve_FullLevelSemistableCoveringW2Def_ModularCurve_UVCrossingModelDef_AlgebraicCurve_TwoChartIntegralModelDef_ModularCurve_X1Def_ModularCurve_SupersingularModuliDef_ModularCurve_FullLevelJacobianDef_DrinfeldCurve_CoordRingDef_ModularCurve_FullLevelLevelAutAtDef_ModularCurve_JqCoeff
Imported by
- no other definition module
Declarations
Source
import Definitions.Def_ModularCurve_FullLevelSemistableCovering import Definitions.Def_ModularCurve_SupersingularNodePlaces import Definitions.Def_AlgebraicCurve_ConstantReduction import Definitions.Def_FLTPrelim_Ramification import Definitions.Def_AlgebraicCurve_RegularProlongation import Definitions.Def_AlgebraicCurve_ResidueDiscs import Definitions.Def_ModularCurve_PlaceWidthChar import Definitions.Def_ModularCurve_FullLevelSemistableCoveringW2 import Definitions.Def_ModularCurve_UVCrossingModel import Definitions.Def_AlgebraicCurve_TwoChartIntegralModel import Definitions.Def_ModularCurve_X1 import Definitions.Def_ModularCurve_SupersingularModuli import Definitions.Def_ModularCurve_FullLevelJacobian import Definitions.Def_DrinfeldCurve_CoordRing import Definitions.Def_ModularCurve_FullLevelLevelAutAt import Definitions.Def_ModularCurve_JqCoeff set_option autoImplicit false set_option synthInstance.maxHeartbeats 800000 set_option maxHeartbeats 12800000 open AlgebraicCurve ModularCurve ModularCurve.FullLevel IsLocalRing CongruenceSubgroup AlgebraicCurve.TwoChartIntegralModel open scoped MatrixGroups attribute [local instance] ModularCurve.instDecidableEqResidueFieldSemistable ModularCurve.instAlgebraResidueFieldModularFunctionFieldCSemistable def ModularCurve.FullLevel.RigidDescentNodesConclusion (q : ℕ) [Fact q.Prime] (M' : ℕ) [NeZero M'] (A : ValuationSubring (AlgebraicClosure ℚ)) (W : Finset (Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M'))) (R₀ : ConstantReduction A ↥(modularFunctionFieldBar M') (modularFunctionFieldC (ResidueField A) M')) (s : ↥W) (k₀ : IntermediateField ℚ (AlgebraicClosure ℚ)) (π₀ : ↥k₀) (hπ : (π₀ : (AlgebraicClosure ℚ)) ∈ A) (ℓ : ℕ) (ζ₀ : ↥k₀) (ϖt : ↥k₀) (Kb : IntermediateField ↥k₀ (AlgebraicClosure ℚ)) (Ab : ValuationSubring ↥Kb) (ϖb : ↥Ab) (ℓ' : ℕ) [Fact ℓ'.Prime] (ξ : ↥k₀) (Kℓ : IntermediateField ↥k₀ (LaurentSeries ↥k₀)) [Algebra ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) ↥Kℓ] [IsScalarTower ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) ↥k₀ ↥Kℓ] (jℓ : ↥Kℓ) [Fact (jℓ ≠ 0)] (ϖt' : ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) (y : Ideal ↥(chartAlgFin ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (↥Kℓ) jℓ)) (Bt : Subalgebra ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) ↥Kℓ) (Wt : ValuationSubring ↥Kℓ) (n : ℕ) (γ₀ : SL(2, ℤ)) (τ₀ : ↥Kℓ ≃ₐ[↥k₀] ↥Kℓ) (m : ℕ) (ζc : (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))))) (hjK : ModularCurve.jqNModC ↥k₀ (q * ℓ') ∈ Kℓ) (a₀ : ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) (ends : Finset (Subring ↥Kℓ)) (G : Subgroup (↥Kℓ ≃ₐ[↥k₀] ↥Kℓ)) (K₀ : IntermediateField ↥k₀ ↥Kℓ) (B₀ : Subalgebra ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) ↥Kℓ) (W₀' : ValuationSubring ↥K₀) : Prop := (∃ (hjR : (⟨coeffEmb (AlgebraicClosure ℚ) jq, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full M' (jq_mem M'))⟩ : ↥(modularFunctionFieldBar M')) ∈ R₀.integers) (_ : (R₀.residue ⟨_, hjR⟩ : modularFunctionFieldC (ResidueField A) M') ∈ (s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M')).toValuationSubring) (_ : ∀ ha₀ : ((a₀ : ↥k₀) : (AlgebraicClosure ℚ)) ∈ A, (residue A ⟨((a₀ : ↥k₀) : (AlgebraicClosure ℚ)), ha₀⟩) ^ q = (s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M')).evalAt (R₀.residue ⟨_, hjR⟩)) (nodes : Finset (Subring ↥K₀)), nodes.card = q + 1 ∧ (∃ Bc : Subring ↥K₀, (∃ T : Finset ↥K₀, Bc = Subring.closure ({f : ↥K₀ | ∃ x : ↥k₀, (x : (AlgebraicClosure ℚ)) ∈ A ∧ f = algebraMap ↥k₀ ↥K₀ x} ∪ (↑T : Set ↥K₀))) ∧ ∀ O ∈ nodes, (∀ f : ↥K₀, f ∈ Bc → f ∈ O) ∧ (∀ f : ↥K₀, f ∈ O ↔ ∃ g h : ↥K₀, g ∈ Bc ∧ h ∈ Bc ∧ (∀ hh : h ∈ O, IsUnit (⟨h, hh⟩ : ↥O)) ∧ f * h = g)) ∧ (∀ (γ : SL(2, ℤ)), γ ∈ Gamma0 M' → ∀ (τ : ↥Kℓ ≃ₐ[↥k₀] ↥Kℓ), ModularCurve.FullLevel.IsLevelAutAt ↥k₀ (q * ℓ') ξ (q * ℓ') ((q * ℓ') ^ 2 * M') (ModularCurve.FullLevel.levelH (q * ℓ') M') γ⁻¹ Kℓ τ → ∀ O ∈ nodes, ∃ O' ∈ nodes, ∀ (f : ↥Kℓ) (hf : f ∈ K₀) (hf' : τ f ∈ K₀), (⟨f, hf⟩ : ↥K₀) ∈ O ↔ (⟨_, hf'⟩ : ↥K₀) ∈ O') ∧ (∀ O ∈ nodes, ∀ O' ∈ nodes, ∃ (γ : SL(2, ℤ)) (_ : γ ∈ Gamma0 M') (τ : ↥Kℓ ≃ₐ[↥k₀] ↥Kℓ) (_ : ModularCurve.FullLevel.IsLevelAutAt ↥k₀ (q * ℓ') ξ (q * ℓ') ((q * ℓ') ^ 2 * M') (ModularCurve.FullLevel.levelH (q * ℓ') M') γ⁻¹ Kℓ τ), ∀ (f : ↥Kℓ) (hf : f ∈ K₀) (hf' : τ f ∈ K₀), (⟨f, hf⟩ : ↥K₀) ∈ O ↔ (⟨_, hf'⟩ : ↥K₀) ∈ O') ∧ (∀ O ∈ nodes, ∀ O' ∈ nodes, O ≠ O' → ∃ (f : ↥K₀) (hf : f ∈ O) (hf' : f ∈ O'), ¬ IsUnit (⟨f, hf⟩ : ↥O) ∧ IsUnit (⟨f, hf'⟩ : ↥O')) ∧ (∀ V : ValuationSubring ↥K₀, (∀ x : ↥k₀, (x : (AlgebraicClosure ℚ)) ∈ A ↔ algebraMap ↥k₀ ↥K₀ x ∈ V) → (∀ (g : LaurentSeries ℚ) (hg : g ∈ modularFunctionFieldFull M') (hgi : (⟨coeffEmb (AlgebraicClosure ℚ) g, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) hg⟩ : ↥(modularFunctionFieldBar M')) ∈ R₀.integers), (∀ P : Place (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar M'), 0 ≤ P.ord ((⟨coeffEmb (AlgebraicClosure ℚ) jq, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full M' (jq_mem M'))⟩ : ↥(modularFunctionFieldBar M')) : ↥(modularFunctionFieldBar M')) → 0 ≤ P.ord ((⟨coeffEmb (AlgebraicClosure ℚ) g, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) hg⟩ : ↥(modularFunctionFieldBar M')) : ↥(modularFunctionFieldBar M'))) → (R₀.residue ⟨_, hgi⟩ : modularFunctionFieldC (ResidueField A) M') ∈ (s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M')).toValuationSubring → ∀ (hgK : ModularCurve.qExpand ↥k₀ ℓ' (coeffEmb ↥k₀ g) ∈ Kℓ), ∃ hF : (⟨ModularCurve.qExpand ↥k₀ ℓ' (coeffEmb ↥k₀ g), hgK⟩ : ↥Kℓ) ∈ K₀, (⟨_, hF⟩ : ↥K₀) ∈ V ∧ ∀ (c : ↥k₀) (hc : (c : (AlgebraicClosure ℚ)) ∈ A), residue A ⟨(c : (AlgebraicClosure ℚ)), hc⟩ = (s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M')).evalAt (R₀.residue ⟨_, hgi⟩) → ∃ hm : (⟨_, hF⟩ : ↥K₀) - algebraMap ↥k₀ ↥K₀ c ∈ V, (⟨_, hm⟩ : ↥V) ∈ maximalIdeal ↥V) → (∀ f : ↥Kℓ, f ∈ B₀ → ∃ hf : f ∈ K₀, (⟨f, hf⟩ : ↥K₀) ∈ V) ∨ (∃ O ∈ nodes, ∀ (f : ↥K₀) (hfO : f ∈ O), f ∈ V ∧ (¬ IsUnit (⟨f, hfO⟩ : ↥O) → ∀ hfV : f ∈ V, (⟨f, hfV⟩ : ↥V) ∈ maximalIdeal ↥V))) ∧ (∀ O ∈ nodes, (∀ f : ↥K₀, f ∈ O → f ∈ W₀') ∧ ∃ (_ : IsLocalRing ↥O) (_ : IsNoetherianRing ↥O), (∀ x : ↥k₀, (x : (AlgebraicClosure ℚ)) ∈ A ↔ algebraMap ↥k₀ ↥K₀ x ∈ O) ∧ (∀ (f : ↥K₀) (hf : f ∈ O), ∃ (x : ↥k₀) (hx : algebraMap ↥k₀ ↥K₀ x ∈ O), (x : (AlgebraicClosure ℚ)) ∈ A ∧ ¬ IsUnit ((⟨f, hf⟩ : ↥O) - ⟨_, hx⟩)) ∧ (∃ (E₀ : ℕ) (_ : 1 ≤ E₀) (_ : ∃ v : ↥k₀, (v : (AlgebraicClosure ℚ)) ∈ A ∧ ((v⁻¹ : ↥k₀) : (AlgebraicClosure ℚ)) ∈ A ∧ π₀ ^ E₀ = ϖt ^ (2 * placeWidthChar q M' (s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M'))) * v) (hπO : algebraMap ↥k₀ ↥K₀ π₀ ∈ O) (cx cy : ↥O) (u : (↥O)ˣ) (ι : (AdicCompletion (maximalIdeal ↥O) ↥O) ≃+* UVCrossingModel (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀)) (γU γV : (UVCrossingModel (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀))ˣ), cx * cy = (⟨_, hπO⟩ : ↥O) ^ E₀ * (u : ↥O) ∧ (∀ (x : ↥k₀) (hx : (x : (AlgebraicClosure ℚ)) ∈ A) (hxO : algebraMap ↥k₀ ↥K₀ x ∈ O), ι (algebraMap ↥O (AdicCompletion (maximalIdeal ↥O) ↥O) ⟨_, hxO⟩) = UVCrossingModel.const ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀) (algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨x, hx⟩)) ∧ ι (algebraMap ↥O (AdicCompletion (maximalIdeal ↥O) ↥O) cx) = (γU : UVCrossingModel (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀)) * UVCrossingModel.U ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀) ∧ ι (algebraMap ↥O (AdicCompletion (maximalIdeal ↥O) ↥O) cy) = (γV : UVCrossingModel (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀)) * UVCrossingModel.V ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀) ∧ ((cy : ↥K₀) ∈ W₀') ∧ (∀ hcy : (cy : ↥K₀) ∈ W₀', (⟨(cy : ↥K₀), hcy⟩ : ↥W₀') ∈ maximalIdeal ↥W₀') ∧ (∀ hcx : (cx : ↥K₀) ∈ W₀', (⟨(cx : ↥K₀), hcx⟩ : ↥W₀') ∉ maximalIdeal ↥W₀') ∧ (∃ (hjF : (⟨ModularCurve.jqNModC ↥k₀ (q * ℓ'), hjK⟩ : ↥Kℓ) - algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) ↥Kℓ a₀ ∈ K₀) (hjO : (⟨_, hjF⟩ : ↥K₀) ∈ O) (e : ℕ) (wV : (UVCrossingModel (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀))ˣ), 1 ≤ e ∧ ι (algebraMap ↥O (AdicCompletion (maximalIdeal ↥O) ↥O) ⟨_, hjO⟩) = (wV : UVCrossingModel (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀)) * (UVCrossingModel.V ((algebraMap ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ))) (AdicCompletion (maximalIdeal ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ↥(A.comap (algebraMap ↥k₀ (AlgebraicClosure ℚ)))) ⟨π₀, hπ⟩) ^ E₀)) ^ e) ∧ (∃ Wx : ValuationSubring ↥K₀, (∀ f : ↥K₀, f ∈ O → f ∈ Wx) ∧ (∀ x : ↥k₀, (x : (AlgebraicClosure ℚ)) ∈ A ↔ algebraMap ↥k₀ ↥K₀ x ∈ Wx) ∧ IsDiscreteValuationRing ↥Wx ∧ (∃ hπW : algebraMap ↥k₀ ↥K₀ π₀ ∈ Wx, maximalIdeal ↥Wx = Ideal.span {(⟨_, hπW⟩ : ↥Wx)}) ∧ (∃ t : ↥Wx, ∀ p : Polynomial ↥k₀, (∀ n, ((p.coeff n : ↥k₀) : (AlgebraicClosure ℚ)) ∈ A) → (∃ hm : Polynomial.aeval (t : ↥K₀) p ∈ Wx, (⟨_, hm⟩ : ↥Wx) ∈ maximalIdeal ↥Wx) → ∀ n, ∃ hc : algebraMap ↥k₀ ↥K₀ (p.coeff n) ∈ Wx, (⟨_, hc⟩ : ↥Wx) ∈ maximalIdeal ↥Wx) ∧ (∀ hcx : (cx : ↥K₀) ∈ Wx, (⟨(cx : ↥K₀), hcx⟩ : ↥Wx) ∈ maximalIdeal ↥Wx) ∧ (∀ hcy : (cy : ↥K₀) ∈ Wx, (⟨(cy : ↥K₀), hcy⟩ : ↥Wx) ∉ maximalIdeal ↥Wx) ∧ (∀ (g : LaurentSeries ℚ) (hg : g ∈ modularFunctionFieldFull M') (hgi : (⟨coeffEmb (AlgebraicClosure ℚ) g, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) hg⟩ : ↥(modularFunctionFieldBar M')) ∈ R₀.integers), (∀ P : Place (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar M'), 0 ≤ P.ord ((⟨coeffEmb (AlgebraicClosure ℚ) jq, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) (modularFunctionField_le_full M' (jq_mem M'))⟩ : ↥(modularFunctionFieldBar M')) : ↥(modularFunctionFieldBar M')) → 0 ≤ P.ord ((⟨coeffEmb (AlgebraicClosure ℚ) g, coeffEmb_mem_laurentBaseChange (AlgebraicClosure ℚ) hg⟩ : ↥(modularFunctionFieldBar M')) : ↥(modularFunctionFieldBar M'))) → ∀ (hgK : ModularCurve.qExpand ↥k₀ ℓ' (coeffEmb ↥k₀ g) ∈ Kℓ), ∃ hF : (⟨ModularCurve.qExpand ↥k₀ ℓ' (coeffEmb ↥k₀ g), hgK⟩ : ↥Kℓ) ∈ K₀, (⟨_, hF⟩ : ↥K₀) ∈ Wx ∧ (∀ hW : (⟨_, hF⟩ : ↥K₀) ∈ Wx, (⟨_, hW⟩ : ↥Wx) ∈ maximalIdeal ↥Wx ↔ (R₀.residue ⟨_, hgi⟩ : modularFunctionFieldC (ResidueField A) M') = 0) ∧ ((R₀.residue ⟨_, hgi⟩ : modularFunctionFieldC (ResidueField A) M') ∈ (s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M')).toValuationSubring → (⟨_, hF⟩ : ↥K₀) ∈ O ∧ ∀ (hO : (⟨_, hF⟩ : ↥K₀) ∈ O) (c : ↥k₀) (hc : (c : (AlgebraicClosure ℚ)) ∈ A) (hcO : algebraMap ↥k₀ ↥K₀ c ∈ O), residue A ⟨(c : (AlgebraicClosure ℚ)), hc⟩ = (s : Place (ResidueField A) (modularFunctionFieldC (ResidueField A) M')).evalAt (R₀.residue ⟨_, hgi⟩) → ¬ IsUnit ((⟨_, hO⟩ : ↥O) - ⟨_, hcO⟩))) ∧ (∀ O' ∈ nodes, O' ≠ O → ∃ f : ↥K₀, f ∈ O' ∧ f ∉ Wx)) ∧ (∃ Bx : Subring ↥K₀, (∀ f : ↥K₀, f ∈ Bx → (f : ↥Kℓ) ∈ B₀ ∧ f ∈ O) ∧ (∀ (f : ↥K₀), f ∈ Bx → ∀ P : Place ↥k₀ ↥Kℓ, 0 ≤ P.ord (jℓ : ↥Kℓ) → 0 ≤ P.ord (f : ↥Kℓ)) ∧ (∀ f : ↥K₀, f ∈ O ↔ ∃ g h : ↥K₀, g ∈ Bx ∧ h ∈ Bx ∧ (∀ hh : h ∈ O, IsUnit (⟨h, hh⟩ : ↥O)) ∧ f * h = g) ∧ (∀ f : ↥K₀, ∃ g h : ↥K₀, g ∈ Bx ∧ h ∈ Bx ∧ h ≠ 0 ∧ f * h = g) ∧ (∃ T : Finset ↥K₀, Bx = Subring.closure ({f : ↥K₀ | ∃ x : ↥k₀, (x : (AlgebraicClosure ℚ)) ∈ A ∧ f = algebraMap ↥k₀ ↥K₀ x} ∪ (↑T : Set ↥K₀))) ∧ (∃ b : ↥K₀, b ∈ Bx ∧ ∀ V : ValuationSubring ↥K₀, (∀ x : ↥k₀, (x : (AlgebraicClosure ℚ)) ∈ A ↔ algebraMap ↥k₀ ↥K₀ x ∈ V) → (∀ hπV : algebraMap ↥k₀ ↥K₀ π₀ ∈ V, (⟨_, hπV⟩ : ↥V) ∈ maximalIdeal ↥V) → ∀ (hjK' : ModularCurve.qExpand ↥k₀ ℓ' (coeffEmb ↥k₀ jq) ∈ Kℓ) (hjF : (⟨ModularCurve.qExpand ↥k₀ ℓ' (coeffEmb ↥k₀ jq), hjK'⟩ : ↥Kℓ) ∈ K₀) (hjV : (⟨_, hjF⟩ : ↥K₀) ∈ V), (∀ p : Polynomial ↥k₀, p.Monic → (∀ i : ℕ, ((p.coeff i : ↥k₀) : (AlgebraicClosure ℚ)) ∈ A) → ∀ hp : Polynomial.aeval (⟨_, hjF⟩ : ↥K₀) (p.map (algebraMap ↥k₀ ↥K₀)) ∈ V, (⟨_, hp⟩ : ↥V) ∉ maximalIdeal ↥V) → (∃ f : ↥K₀, f ∈ O ∧ f ∉ V) → b ∉ V)))))