ModularCurves: Y₁(N) — the Γ₁(N) moduli problem is representable by a smooth affine curve (axiom-clean) - #5256
Merged
Conversation
… — pure-skeleton mapSkeleton_pullback_comp isolates the Quotient chase from the .some-unfolds; single-unfold shows + Pic.map_val rw; pullbackComp arg-order fixed. Pic is a contravariant group functor; STREAM FULLY SORRY-FREE (T-PIC0) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…r a filtered base are filtered colimits (presentedT/U + eval lemmas, poly stage-lift/stage-eq, span-representation eq_at_stage) + KL-2e equiv-transport (fable-FP)
…t (negModelHom_baseChange → A in parallel, whisker-BC stays c5β); NEW-CASCADE gate = T-G4 completion Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… scheme level (iota-cancellation + E.Point restrict-algebra: the unit component restricts to the zero point). Also leftUnitSection + its legs + groupSquareToSquare_snd (NEW-Y1)
…l commutative group-object law set; tensor_hom_ext tool; sharpened Over-monoidal-seam registry entry (NEW-Y1)
…osed (hand tensorObj/unitObj ≅ localized ⊗/𝟙 via μIso+counit), → direction assembled onto consumed Dual.lean IsInvertible.dual; leaves CMP-PAIR + CMP-← registered (T-PIC0) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…+bridges, leaves PAIR/← registered (fable-PIC0)
…the 8 class-typed defs, Sheaf.cond→property, Cocones.ext→Cocone.ext; Pic.lean warning-clean (T-PIC0) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…f presented algebras = concatenated presentation) with includeLeft/Right intertwining (fable-FP)
…leInr variable-doubling maps with transition/cocone naturality squares (fable-FP)
… contravariant group functor complete; GME 2.17 assembled; PAIR/← registered); seam-cut live both halves Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…om-free zero-section base change Of-form wrapper of projModelZero_baseChange, dissolving projModelBaseChangeOf's eqToHom via subst (mirrors mulModelHomBC_baseChange). Consumed by the unit-law transports. FINDING: the direct isPullback_projModelBaseChangeOf transport of the Over-level unit/inv/assoc laws whnf-times-out constructing pullback.map with a projModelBaseChangeOf leg (the eqToHom heaviness) — the fix is the of_map/of_eq layer (work at uWLU.map f where projModelBaseChange is eqToHom-free, via a mulModelHom_map_eq_BC classify-collapse, exactly the c6 of_map pattern). The whisker-BC-naturality logic itself is clean (pullback.map_comp + whiskerLeft_left full form + this helper — no projection spelling war). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… restructure teed up; A's neg-lemma landed Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…general-f upgrade); staged-sweep race boarded as fleet recipe (atomic pathspec commits); T-G4 final stretch Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…faithfullyFlat proven modulo {hkeyL/hkeyR square, KL-3 flat-at-stage, KL-4 ffl-at-stage}; endgame split into of_comp_aux (budget), Amitsur transport + section factoring + retract all green (fable-FP)
…l/r squares) — GATE NOW PROVEN MODULO {KL-3 flat-at-stage, KL-4 ffl-at-stage} only (fable-FP)
…e reduced to KL-3/KL-4 spreading-out leaves (fable-FP)
…aDesc_{of_isPullback,section} — unblock B3 bijection's curve-level torsor descent
De-privatize the three already-proven torsor base-change/trivialization helpers so the KM 4.7.0
representability bijection (coreData_surjective/injective) can run existsUnique_descent_of_torsor
and [B2b] at the CURVE level (the fibre direction needs the deck structure, not just
agreement-after-π). No proof changes; visibility widening only. TorsorMap green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…OLVED, hnat plumbing isolated The of_map/of_eq pattern (prove at uWLU.map f, subst) makes projModelBaseChangeOf's eqToHom = eqToHom rfl (cheap) — dissolves the whnf timeout that blocked the prior session. Full structure (raw/hbc/hw1/hw2/X/isPullback) compiles; sole remaining blocker isolated to hnat's pullback.map ≫ pullback.fst reduction (documented what resists). Preserved for continuation. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…umed on final 2 gaps (helpers unblocked, equivariance corrected)
…nge (base change of presented algebras, forward/backward + tautological-point evaluation); sorry inventory = {KL-3, KL-4} exactly (fable-FP)
…ge) executes now; top-up merge at gate-fire; steps 2-4 if T-G4 lands mid-session Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…merge; c5β of_map breakthrough; Y1 four-designed-sessions snapshot Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ockers cracked BREAKTHROUGH 1: of_map/of_eq dissolves the projModelBaseChangeOf eqToHom whnf-timeout (the prior-session blocker). BREAKTHROUGH 2: pullback.map ≫ pullback.fst reduces via rw [pullback.map, pullback.lift_fst] (crosses the (mo).hom/projModelπ spelling that simp cannot). The 4 projection sub-facts compile; sole remainder = a tiny assembly rw-match subtlety (documented, fix candidates listed). Reusable for all 4 transports. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…tible sets patch-clopen (induction over the boolean subalgebra), raw patch-compactness transfer, Spec patch-T2 via basicOpen clopen separation, comap patch-continuity via finite zeroLocus presentations (fable-FP)
…v→y1 merge) (NEW-CASCADE)
…fire step 1, v10.127(2)-approved) — C6 dictionary layer (AdditionSpecPoints/GroupLawAxioms/AdditionBaseChange/NegModelBaseChange) + ~900 commits of fleet drift onto the [T-B6'] home branch. Conflict resolutions boarded: tickets.md append-only verbatim-union (y1 suffix preserved under marker); sentinel ours; ModularCurves.lean = forced import-set union (registry file, outside board files — judgment call boarded in lieu of stop, resolution content-free: dev list + YOneAtlasClassify + YOneTatePoint) (NEW-CASCADE)
…rm intersection argument (span-representation descent through stages, ffl lift via comap-surjectivity, nu-square contraction) + Cantor patch-compactness stage extraction; K2 fibre-collapse remains (fable-FP)
… in-proof seam registry accepted; next-session queue confirmed); c5β 95% T-G4 watch hot Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…locus of two maps into an étale morphism is clopen (sorry-free, clean triple): agreementι + isOpenImmersion (unramified diagonal) + isClosedImmersion (separated diagonal) + isClopen_range_agreementι. The topological engine of the Y(N) clopen full-level locus (route γ): σ_cd=σ_c'd' loci are clopen ⟹ full-level = open complement; rooted (NEW-Y1)
…h — vanishing locus of an N-killed point is clopen (axiom-clean triple): consumes AgreementLocusClopen + torsionπ_etale' + isSeparated_torsionπ (torsionι closed-imm ≫ proper π). The per-combination clopen building block of the full-level open locus U; rooted (NEW-Y1)
…sor audit + 2 clean engine leaves (AgreementLocusClopen + isClopen_range_pointVanish, the openness foundation); ⊇ crux decomposed into [YF-U]/[YF-⊆]/[YF-⊇] with exact agent-audited API + the 2 sub-lemmas to build; next-session first act pinned (NEW-Y1)
…,d)≠0} vanish σ_cd)ᶜ, open via finite union of clopen vanishing loci (isClopen_range_pointVanish); axiom-clean; + tautCombo/tautCombo_killed (NEW-Y1)
… — fullLevelOpenSet/fullLevelOpens + fullLevelOpenSet_isOpen: complement of the union of the N²−1 clopen vanishing loci of the nonzero combinations combPoint c d = [c]·tautPt₁+[d]·tautPt₂ (killed via tautPt smul-zero); pointVanishSet exposed; taut killing made public. Half the clopen claim, proven; rooted (NEW-Y1)
…-clean, half the KM 3.7.1 clopen claim); remaining ⊆/⊇ with U:=fullLevelOpens + the 2 divisor sub-lemmas pinned (NEW-Y1)
… a surjection of finite free modules of equal rank is injective/bijective (axiom-clean): CommRing⟹OrzechProperty + LinearEquiv.ofFinrankEq. The module core of same-degree-subdivisor-equality (⊇); rooted (NEW-Y1)
…ed-immersion cancellation + ideal-equality via ker_comp_of_isIso); sole sorry = the equal-rank closed-immersion-iso core (ker j = ⊥ from equal fibrewise degree), a stalk-level module-descent sub-lemma (NEW-Y1)
…linear map of finite free modules of equal rank is bijective (Module.End.injective_of_surjective + basis transport); the module core for equal-rank closed-immersion iso (NEW-Y1)
…lk_eq — a surjection of finite FLAT modules of equal stalkwise rank is injective (axiom-clean, no Noetherian): subsingleton_of_localization_maximal + localize (free over R_p) + the free lemma + map_exact. The ring-level heart of same-degree-subdivisor-equality; rooted (NEW-Y1)
…ctive_ringHom_of_flat_rankAtStalk_eq: a surjective ring hom of finite-flat equal-stalkwise-rank algebras over a base is an iso (axiom-clean). The affine form of same-degree-divisor-equality — directly consumes the flat module lemma; rooted (NEW-Y1)
…SurjectiveFreeSameRank 4 lemmas, affine same-degree-iso); both clopen halves have cores proven; remaining = scheme plumbing [YF-SCHEME-ISO]/[YF-SUBDIV-EQ]/[YF-COMAX]/[YF-⊆⊇] (NEW-Y1)
…enLocus dup of FullLevelOpenLocus's fullLevelOpens; FiniteFreeSurjective + SubdivisorDegree subsumed by SurjectiveFreeSameRank's free/flat/ring cores) — reconcile self-collision from a stale view; reuse-not-duplicate (NEW-Y1)
…nkAtStalk_eq + bijective_quotient — a quotient of a finite-flat R₀-algebra whose quotient has equal stalkwise rank is trivial (I=⊥), Spec-maps to iso (axiom-clean). The affine same-degree-closed-immersion-iso, ready to consume affine-locally; rooted (NEW-Y1)
…ness [YF-U] + full ⊇ commutative-algebra chain through affine same-degree-iso); remaining = de-risked scheme assembly [YF-SUBDIV-EQ]/[YF-COMAX]/[YF-⊆⊇] (NEW-Y1)
…les removed, 07f3817) + YIELD to the live driver window; stale-view collision corrected (NEW-Y1)
…tive_of_flat_rankAtStalk_eq: any surjective ring hom of finite-flat equal-stalkwise-rank R₀-algebras Spec-maps to an iso (the divisor-comorphism form, ready to consume affine-locally); rooted (NEW-Y1)
…f_of_pairwise_sup_eq_top: a pairwise-comaximal finite family of ideal sheaves has product = intersection (axiom-clean; affine-local via Ideal.prod_eq_iInf_of_pairwise_isCoprime + idealAt monoid hom). The comaximality half of the ⊇ step (disjoint sections ⟹ ∏ker=⋂ker); rooted (NEW-Y1)
…rod_eq_biInf_of_pairwise_disjoint_support: ideal sheaves with pairwise disjoint supports have ∏=⨅ (via support_sup=⊓ + support_eq_bot_iff). The full disjoint-sections ⟹ ∏ker=⋂ker component of ⊇; axiom-clean, rooted (NEW-Y1)
…openness + ⊇ chain + [YF-COMAX]); remaining = D-stream assembly connecting cores to sectionsDivisor/taut construction (NEW-Y1)
…ly foundation), synced v10.167 (NEW-Y1)
…f_rankAtStalk_eq_isAffineBase — a closed immersion of finite-flat-lfp schemes of equal stalkwise rank over an AFFINE base is an iso (axiom-clean): transport via arrowIsoSpecΓ + the ring same-degree-iso form. The scheme form of same-degree-divisor-equality (affine base); rooted (NEW-Y1)
…; this window YIELDS; /loop over-firing config note for user (NEW-Y1)
…on to a target open (morphismRestrict is a base change; via isPullback_morphismRestrict + finrank_of_isPullback). Bridge for the general (non-affine-base) scheme wrapper; rooted (NEW-Y1)
…ank_eq_rankAtStalk_isAffineBase + finrank-hypothesis affine-base scheme wrapper (isIso_of_isClosedImmersion_of_finrank_eq_isAffineBase). Same-degree closed-imm-iso now takes scheme finrank over affine base; rooted (NEW-Y1)
…finrank_eq: a closed immersion of finite-flat-lfp schemes of equal scheme-rank over ANY base is an iso (axiom-clean). Reduces to affine base on g⁻¹(affine cover of S) via finrank_morphismRestrict. The full scheme form of same-degree-divisor-equality; rooted (NEW-Y1)
CBirkbeck
pushed a commit
that referenced
this pull request
Jul 12, 2026
… handoff notes Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This was referenced Jul 13, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The first modular curve, end-to-end: over any commutative ring
Rwith4 ≤ NandNinvertible inR, the naive Γ₁(N) moduli problem is representable, and every representing object is smooth and affine overSpec R. The representing scheme is constructed explicitly:yOne R N, an open subscheme of the N-torsion killed locus of the universal Tate curve over an explicit localized polynomial base.Main results (all
#print axioms={propext, Classical.choice, Quot.sound})ModularCurves.gammaOneNaive_representable(ModularCurve/YOneTatePoint.lean:1404) — the MASTER: representability + smooth + affine, universal over R.ModularCurves.yOne_representable_smooth_affine— the display form naming the witnessyOneEllObj R N/yOneStructMap R N.ModularCurves.gammaOneNaive_representable_zInv— the literal arithmetic form overℤ[1/N] = Localization.Away (N : ℤ)(Loeffler Thm 3.4.4).ModularCurves.exists_tatePoint— the marked universal Tate curve with its classifying universal property (Loeffler Cor 3.3.5).E[N]étaleness/finiteness/flatness for invertible N (KM 2.3.1, the quasi-finiteness leg via a cross-project HasseWeil bridge);AlgebraicGeometry.Scheme.PicwithPic.map(a contravariant group functor, GME 2.16); sheaf duals and pole sheaves; a glued Grassmannian scheme; Hopf–Galois descent for finite free Hopf algebras (Stacks 03BM).Validation
lean-toolchainand mathlib pin to currentmain(verified — the only lakefile delta is the ModularCurves[[lean_lib]]registration).main's default build surface is unchanged by this merge.WIP markers (per AINTLIB's explicit sorry-tolerance on main)
Non-headline files carry registered work-in-progress
sorrys belonging to in-flight producer lanes (Γ_H / Γ₀(N) / Y(N) streams, and boarded black-box reductions). None are on the axiom trail of the results above — the headline theorems print the clean triple.Debt register (for the cleanup lanes)
EllipticCurve/PoleSheaf.leancarries 9 registeredmaxHeartbeatsraises (boarded as fleet /buzz-decompose targets at the original merge); a small number of cosmetic lint warnings are boarded for main-merge cleanup.🤖 Generated with Claude Code