import Definitions.Def_FLTPrelim_FreyPackage import Definitions.Def_FLTPrelim_GaloisRep import Definitions.Def_FLTPrelim_Modularity import Definitions.Def_FLTPrelim_ModularRep import Definitions.Def_FLTPrelim_Ramification import Definitions.Def_FreyPackage_LevelRaising import Definitions.Def_RibetLevelLowering_CharacterGroupApparatusV2 import Definitions.Def_GaloisRep_GlobalUnramifiedAt import Definitions.Def_FreyPackage_GaloisRep import Definitions.Def_FreyPackage_ExchangeCase import Definitions.Def_FreyPackage_LoweringAt import Definitions.Def_FreyPackage_AtPNewLowering import Definitions.Def_WeierstrassCurve_PeuRamifiee import Definitions.Def_WeierstrassCurve_Semistability set_option autoImplicit false noncomputable section open WeierstrassCurve WeierstrassCurve.Affine.Point FreyCurve open scoped CongruenceSubgroup namespace FreyPackage noncomputable local instance instDecEqQbarUniformPin : DecidableEq (AlgebraicClosure ā„š) := Classical.decEq _ def ModularRepOfLevelNewAtPinned (P : FreyPackage) (M q : ā„•) : Prop := āˆƒ (g : CuspForm (CongruenceSubgroup.Gamma0 M) 2) (š”Ŗ : Ideal (integralClosure ā„¤ ā„‚)), g.IsNormalizedEigenform āˆ§ š”Ŗ.IsMaximal āˆ§ (P.p : integralClosure ā„¤ ā„‚) āˆˆ š”Ŗ āˆ§ (āˆ€ ā„“ : ā„•, ā„“.Prime ā†’ (freyCurveInt P).IsGoodPrimeFor ā„“ ā†’ Ā¬ ā„“ āˆ£ M ā†’ ā„“ ā‰  P.p ā†’ āˆƒ a : integralClosure ā„¤ ā„‚, (a : ā„‚) = ModularFormClass.qCoeff g ā„“ āˆ§ a - (((freyCurveInt P).apOfModel ā„“ : ā„¤) : integralClosure ā„¤ ā„‚) āˆˆ š”Ŗ) āˆ§ g.IsNewAt q def MazurPrincipleNewLoweringAtUniform (P : FreyPackage) (q : ā„•) : Prop := āˆ€ N : ā„•, 0 < N ā†’ q.Prime ā†’ q ā‰  2 ā†’ q ā‰  P.p ā†’ Ā¬ q āˆ£ N ā†’ Ā¬ P.ExchangeCongruence q ā†’ GaloisRepIsIrreducible (K := AlgebraicClosure ā„š) ā„š P.freyCurve P.p ā†’ GlobalGaloisRep.IsUnramifiedAt P.freyGaloisRep q ā†’ P.ModularRepOfLevelNewAtPinned (N * q) q ā†’ P.ModularRepOfLevelAt N def ExchangeCaseLoweringAtUniform (P : FreyPackage) (q : ā„•) : Prop := āˆ€ N : ā„•, 0 < N ā†’ q.Prime ā†’ q ā‰  2 ā†’ q ā‰  P.p ā†’ Ā¬ q āˆ£ N ā†’ P.ExchangeCongruence q ā†’ GaloisRepIsIrreducible (K := AlgebraicClosure ā„š) ā„š P.freyCurve P.p ā†’ GlobalGaloisRep.IsUnramifiedAt P.freyGaloisRep q ā†’ P.ModularRepOfLevelNewAtPinned (N * q) q ā†’ P.ModularRepOfLevelAt N def AtPNewLoweringAtUniform (P : FreyPackage) : Prop := āˆ€ Nā‚€ : ā„•, 0 < Nā‚€ ā†’ Ā¬ P.p āˆ£ Nā‚€ ā†’ GaloisRepIsIrreducible (K := AlgebraicClosure ā„š) ā„š P.freyCurve P.p ā†’ P.freyCurve.IsPeuRamifieeAt P.p P.p ā†’ P.ModularRepOfLevelNewAtPinned (Nā‚€ * P.p) P.p ā†’ P.ModularRepOfLevelAt Nā‚€ end FreyPackage end