Modular curves, following Katz–Mazur

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

Definition`Y₁(N)` is a fine moduli scheme for `N ≥ 4`#

For N ≥ 4, the naive moduli problem [Γ₁(N)] over Ell/B is represented by the universal elliptic curve over Y₁(N) (EllObj.yOne B N): the naive [Γ₁(N)]-structures on an object X of Ell/B correspond to the arrows X ⟶ EllObj.yOne B N, by pulling back the point (0, 0) (naiveLevelEquiv_gammaOneNaiveRepresentableBy_homEquiv).

TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneNaiveRepresentableBy.{u}
  {B : AlgebraicGeometry.Scheme} {N : ℕ} [NeZero N] (h4 : 4 ≤ N) :
  CategoryTheory.Functor.RepresentableBy (TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneNaive B N)
    (TauCeti.AlgebraicGeometry.EllObj.yOne B N)

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneNaiveRepresentableBy.

Sources

LeanTauCeti.AlgebraicGeometry.ModuliProblem.gammaOneNaiveRepresentableBy

Used by 2

Used byTauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy · Y₁(N) is smooth over B

Theorem`Y₁(N)` is smooth over `B`#

For N ≥ 4 invertible on B, the structure morphism of the fine moduli scheme Y₁(N) to B is smooth; for example Y₁(N) is smooth over ℤ[1/N].

TauCeti.AlgebraicGeometry.EllObj.smooth_yOne_structureMap.{u} (B : AlgebraicGeometry.Scheme) (N : ℕ)
  [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) (h4 : 4 ≤ N) :
  AlgebraicGeometry.Smooth (TauCeti.AlgebraicGeometry.EllObj.yOne B N).structureMap

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.EllObj.smooth_yOne_structureMap.

Sources

LeanTauCeti.AlgebraicGeometry.EllObj.smooth_yOne_structureMap

Uses 2

Proof usesThe n-torsion of an elliptic curve is étale where n is invertible (Katz–Mazur 2.3.1) · Y₁(N) is a fine moduli scheme for N ≥ 4

DefinitionTauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy #

For N ≥ 4 invertible on B, the existing fine curve Y₁(N) also represents the integral Drinfeld [Γ₁(N)] problem restricted to B.

TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy.{u} {B : AlgebraicGeometry.Scheme}
  {N : ℕ} [NeZero N] {hN : ∀ (b : ↥B), ↑N ≠ 0} (h4 : 4 ≤ N) :
  CategoryTheory.Functor.RepresentableBy (TauCeti.AlgebraicGeometry.ModuliProblem.gammaOne B N)
    (TauCeti.AlgebraicGeometry.EllObj.yOne B N)

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy.

Sources

LeanTauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy

Uses 3

Statement usesY₁(N) is a fine moduli scheme for N ≥ 4

Proof usesThe n-torsion of an elliptic curve is étale where n is invertible (Katz–Mazur 2.3.1) · Deligne's theorem (TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.pow_eq_one_of_finrank)

DefinitionDrinfeld and naive `[Γ(N)]`-structures coincide where `N` is invertible (Katz–Mazur, §3.7)#

over a base B on which N is invertible, gammaToGammaNaive and gammaNaiveToGamma are mutually inverse isomorphisms between [Γ(N)] and [Γ(N)]_naive.

TauCeti.AlgebraicGeometry.ModuliProblem.gammaIsoGammaNaive.{u} (B : AlgebraicGeometry.Scheme)
  (N : ℕ) [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) :
  TauCeti.AlgebraicGeometry.ModuliProblem.gamma B N ≅
    TauCeti.AlgebraicGeometry.ModuliProblem.gammaNaive B N

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.ModuliProblem.gammaIsoGammaNaive.

Sources

LeanTauCeti.AlgebraicGeometry.ModuliProblem.gammaIsoGammaNaive

Uses 2 · Used by 1

Proof usesThe Jacobian criterion for étaleness · Vieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient

Used byThe moduli problem [Γ(N)] is étale over Ell/B when N is invertible on B (Katz–Mazur, 3.7.1)

TheoremThe moduli problem `[Γ(N)]` is étale over `Ell/B` when `N` is invertible on `B` (Katz–Mazur, 3.7.1)#

where N is invertible on B, [Γ(N)] is isomorphic to [Γ(N)]_naive, whose representing schemes are étale over their bases. Together with ModuliProblem.hasProperty_isFinite_gammaRelRepData, this makes [Γ(N)] finite étale over Ell/B.

TauCeti.AlgebraicGeometry.ModuliProblem.hasProperty_etale_gammaRelRepData.{u}
  (B : AlgebraicGeometry.Scheme) (N : ℕ) [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) :
  (TauCeti.AlgebraicGeometry.ModuliProblem.gammaRelRepData B N).HasProperty @AlgebraicGeometry.Etale

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.ModuliProblem.hasProperty_etale_gammaRelRepData.

Sources

LeanTauCeti.AlgebraicGeometry.ModuliProblem.hasProperty_etale_gammaRelRepData

Uses 3

Statement usesThe integral moduli problem [Γ(N)] is relatively representable (Katz–Mazur, 3.6.0)

Proof usesThe n-torsion of an elliptic curve is étale where n is invertible (Katz–Mazur 2.3.1) · Drinfeld and naive [Γ(N)]-structures coincide where N is invertible (Katz–Mazur, §3.7)

Theorem`[Γ(N)]` is rigid for `N ≥ 3` where `N` is invertible (Katz–Mazur, 2.7.2)#

Over a base B on which N is invertible, [Γ(N)] is isomorphic to the rigid naive problem [Γ(N)]_naive (ModuliProblem.isRigid_gammaNaive).

TauCeti.AlgebraicGeometry.ModuliProblem.isRigid_gamma.{u} (B : AlgebraicGeometry.Scheme) (N : ℕ)
  [NeZero N] (hN : ∀ (b : ↥B), ↑N ≠ 0) (hN3 : 3 ≤ N) :
  (TauCeti.AlgebraicGeometry.ModuliProblem.gamma B N).IsRigid

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.ModuliProblem.isRigid_gamma.

Sources

LeanTauCeti.AlgebraicGeometry.ModuliProblem.isRigid_gamma

Uses 1

Proof usesVieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient

DefinitionThe integral moduli problem `[Γ(N)]` is relatively representable (Katz–Mazur, 3.6.0)#

For an elliptic curve E/S, it is represented by the closed Drinfeld-basis locus in E[N] ×_S E[N].

TauCeti.AlgebraicGeometry.ModuliProblem.gammaRelRepData.{u} (B : AlgebraicGeometry.Scheme) (N : ℕ)
  [NeZero N] : (TauCeti.AlgebraicGeometry.ModuliProblem.gamma B N).RelRepData

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.ModuliProblem.gammaRelRepData.

Sources

LeanTauCeti.AlgebraicGeometry.ModuliProblem.gammaRelRepData

Uses 1 · Used by 1

Proof usesThe Jacobian criterion for étaleness

Used byThe moduli problem [Γ(N)] is étale over Ell/B when N is invertible on B (Katz–Mazur, 3.7.1)

DefinitionThe moduli problem `[Γ₁(N)]` is relatively representable (Katz–Mazur, 3.6.0)#

For an object X = (E/S) of Ell/B, the functor T ↦ [Γ₁(N)](E_T/T) on schemes over S is represented by the exact-order scheme E.exactOrderScheme N, the closed subscheme of E of points of exact order N, through gammaOneBaseChangeEquiv. No hypothesis is placed on B, and N need not be invertible on it.

TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRelRepData.{u} (B : AlgebraicGeometry.Scheme)
  (N : ℕ) : (TauCeti.AlgebraicGeometry.ModuliProblem.gammaOne B N).RelRepData

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRelRepData.

Sources

LeanTauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRelRepData

TheoremMultiplication by a nonzero integer `n` is an isogeny of degree `n²`#

TauCeti.AlgebraicGeometry.EllipticCurveGeom.isogenyOfDegree_intCast.{u}
  {S : AlgebraicGeometry.Scheme} (E : TauCeti.AlgebraicGeometry.EllipticCurveGeom S) {n : ℤ}
  (hn : n ≠ 0) : TauCeti.GroupScheme.IsogenyOfDegree (↑n).asHom.hom (n.natAbs ^ 2)

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.EllipticCurveGeom.isogenyOfDegree_intCast.

Sources

LeanTauCeti.AlgebraicGeometry.EllipticCurveGeom.isogenyOfDegree_intCast

Uses 1

Proof usesThe Jacobian criterion for étaleness

TheoremThe `n`-torsion of an elliptic curve is étale where `n` is invertible (Katz–Mazur 2.3.1)#

For an elliptic curve E over a scheme S and an integer n invertible in every residue field of S, the n-torsion E[n] is étale over S. It is also finite over S (EllipticCurveGeom.isFinite_torsion_hom), so E[n] is finite étale over S.

TauCeti.AlgebraicGeometry.EllipticCurveGeom.etale_torsion_hom_of_forall_intCast_ne_zero.{u}
  {S : AlgebraicGeometry.Scheme} (E : TauCeti.AlgebraicGeometry.EllipticCurveGeom S) {n : ℤ}
  (hn : ∀ (s : ↥S), ↑n ≠ 0) : AlgebraicGeometry.Etale (E.torsion n).X.hom

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.EllipticCurveGeom.etale_torsion_hom_of_forall_intCast_ne_zero.

Sources

LeanTauCeti.AlgebraicGeometry.EllipticCurveGeom.etale_torsion_hom_of_forall_intCast_ne_zero

Uses 2 · Used by 3

Proof usesThe Jacobian criterion for étaleness · Vieta's formula at a pair of parameters, cleared of the inverse of the cubic's leading coefficient

Used byTauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy · The moduli problem [Γ(N)] is étale over Ell/B when N is invertible on B (Katz–Mazur, 3.7.1) · Y₁(N) is smooth over B

DefinitionGalois theory for finite étale schemes over a field #

For a separable closure Ω of K, finite étale K-schemes are equivalent to finite sets with a continuous action of Gal(Ω/K). A finite étale scheme Spec A goes to the set of Ω-valued points of A (specCompGaloisEquivalenceFunctorIso).

TauCeti.FiniteEtaleScheme.galoisEquivalence.{u} (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω]
  [IsSepClosed Ω] [IsGalois K Ω] :
  TauCeti.FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K) ≌ ContAction FintypeCat Gal(Ω/K)

Lean

Formalized in Tau Ceti as TauCeti.FiniteEtaleScheme.galoisEquivalence.

Sources

LeanTauCeti.FiniteEtaleScheme.galoisEquivalence

Used by 1

Used byFinite étale commutative group schemes over a field are finite Galois modules

DefinitionFinite étale commutative group schemes over a field are finite Galois modules #

Commutative group objects in finite étale K-schemes are equivalent to commutative group objects in finite continuous Gal(Ω/K)-sets, that is, to finite abelian groups with a continuous action of Gal(Ω/K) by group automorphisms.

TauCeti.FiniteEtaleScheme.galoisEquivalenceCommGrp.{u} (K Ω : Type u) [Field K] [Field Ω]
  [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] :
  CategoryTheory.CommGrp (TauCeti.FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K)) ≌
    CategoryTheory.CommGrp (ContAction FintypeCat Gal(Ω/K))

Lean

Formalized in Tau Ceti as TauCeti.FiniteEtaleScheme.galoisEquivalenceCommGrp.

Sources

LeanTauCeti.FiniteEtaleScheme.galoisEquivalenceCommGrp

Uses 1

Statement usesGalois theory for finite étale schemes over a field

Theorem`GL₂(ℤ/Nℤ)` acts freely on `𝕄(𝒫, [Γ(N)])` for every rigid `𝒫`#

Let V represent the simultaneous problem (𝒫, [Γ(N)]) with the naive full level-N problem, on which GL₂(ℤ/Nℤ) acts by change of basis. If a point of V.base with values in a nonempty scheme is fixed by a matrix g, then g = 1. For N = 3 this is the freeness of the action of GL₂(𝔽₃) on the moduli scheme of 𝒫 rigidified by naive level-three structures.

TauCeti.AlgebraicGeometry.ModuliProblem.IsRigid.eq_one_of_comp_simultaneousAction_gammaNaiveAction_base_eq.{u}
  {B : AlgebraicGeometry.Scheme} {P : TauCeti.AlgebraicGeometry.ModuliProblem B}
  {V : TauCeti.AlgebraicGeometry.EllObj B} {N : ℕ} (hP : P.IsRigid)
  (R :
    CategoryTheory.Functor.RepresentableBy
      (CategoryTheory.MonoidalCategoryStruct.tensorObj P
        (TauCeti.AlgebraicGeometry.ModuliProblem.gammaNaive B N))
      V)
  {T : AlgebraicGeometry.Scheme} [Nonempty ↥T] {x : T ⟶ V.base} {g : (GL (Fin 2) (ZMod N))ᵐᵒᵖ}
  (hx :
    CategoryTheory.CategoryStruct.comp x
        ((TauCeti.AlgebraicGeometry.ModuliProblem.simultaneousAction R
                  (TauCeti.AlgebraicGeometry.ModuliProblem.gammaNaiveAction B N))
                g).asIso.hom.base =
      x) :
  g = 1

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.ModuliProblem.IsRigid.eq_one_of_comp_simultaneousAction_gammaNaiveAction_base_eq.

Sources

LeanTauCeti.AlgebraicGeometry.ModuliProblem.IsRigid.eq_one_of_comp_simultaneousAction_gammaNaiveAction_base_eq

DefinitionCategoryTheory.CommMon.invariantSubalgebraPresheaf #

The presheaf of subalgebras of invariant sections of A.

CategoryTheory.CommMon.invariantSubalgebraPresheaf.{u, v} {X : AlgebraicGeometry.Scheme}
  {A : CategoryTheory.CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* CategoryTheory.Aut A) :
  A.SubalgebraPresheaf

Lean

Formalized in Tau Ceti as CategoryTheory.CommMon.invariantSubalgebraPresheaf.

Sources

LeanCategoryTheory.CommMon.invariantSubalgebraPresheaf

DefinitionTauCeti.DescentDatum.descended #

The scheme descended from a descent datum D on an affine morphism X ⟶ S': the relative spectrum over S of the functions on X whose pullbacks along the action and along the second projection S' ×_S X ⟶ X agree.

TauCeti.DescentDatum.descended.{u} {S S' : AlgebraicGeometry.Scheme} {p : S' ⟶ S}
  [AlgebraicGeometry.IsAffineHom p] {X : CategoryTheory.Over S'}
  [AlgebraicGeometry.IsAffineHom X.hom] (D : TauCeti.DescentDatum p X) : CategoryTheory.Over S

Lean

Formalized in Tau Ceti as TauCeti.DescentDatum.descended.

Sources

LeanTauCeti.DescentDatum.descended

DefinitionTauCeti.StrictHenselization.algebra #

The colimit of pointed étale algebras. For a local base ring and a separable closure of its residue field as target, this is the strict henselization.

TauCeti.StrictHenselization.algebra.{u} (R Ω : Type u) [CommRing R] [CommRing Ω] [Algebra R Ω] :
  CommAlgCat R

Lean

Formalized in Tau Ceti as TauCeti.StrictHenselization.algebra.

Sources

LeanTauCeti.StrictHenselization.algebra

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Modular curves, following Katz–Mazur

DefinitionY₁(N) is a fine moduli scheme for N ≥ 4#

Lean

Sources

TheoremY₁(N) is smooth over B#

Lean

Sources

DefinitionTauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy#

Lean

Sources

DefinitionDrinfeld and naive [Γ(N)]-structures coincide where N is invertible (Katz–Mazur, §3.7)#

Lean

Sources

TheoremThe moduli problem [Γ(N)] is étale over Ell/B when N is invertible on B (Katz–Mazur, 3.7.1)#

Lean

Sources

Theorem[Γ(N)] is rigid for N ≥ 3 where N is invertible (Katz–Mazur, 2.7.2)#

Lean

Sources

DefinitionThe integral moduli problem [Γ(N)] is relatively representable (Katz–Mazur, 3.6.0)#

Lean

Sources

DefinitionThe moduli problem [Γ₁(N)] is relatively representable (Katz–Mazur, 3.6.0)#

Lean

Sources

TheoremMultiplication by a nonzero integer n is an isogeny of degree n²#

Lean

Sources

TheoremThe n-torsion of an elliptic curve is étale where n is invertible (Katz–Mazur 2.3.1)#

Lean

Sources

DefinitionGalois theory for finite étale schemes over a field#

Lean

Sources

DefinitionFinite étale commutative group schemes over a field are finite Galois modules#

Lean

Sources

TheoremGL₂(ℤ/Nℤ) acts freely on 𝕄(𝒫, [Γ(N)]) for every rigid 𝒫#

Lean

Sources

DefinitionCategoryTheory.CommMon.invariantSubalgebraPresheaf#

Lean

Sources

DefinitionTauCeti.DescentDatum.descended#

Lean

Sources

DefinitionTauCeti.StrictHenselization.algebra#

Lean

Sources

Definition`Y₁(N)` is a fine moduli scheme for `N ≥ 4`#

Theorem`Y₁(N)` is smooth over `B`#

DefinitionTauCeti.AlgebraicGeometry.ModuliProblem.gammaOneRepresentableBy #

DefinitionDrinfeld and naive `[Γ(N)]`-structures coincide where `N` is invertible (Katz–Mazur, §3.7)#

TheoremThe moduli problem `[Γ(N)]` is étale over `Ell/B` when `N` is invertible on `B` (Katz–Mazur, 3.7.1)#

Theorem`[Γ(N)]` is rigid for `N ≥ 3` where `N` is invertible (Katz–Mazur, 2.7.2)#

DefinitionThe integral moduli problem `[Γ(N)]` is relatively representable (Katz–Mazur, 3.6.0)#

DefinitionThe moduli problem `[Γ₁(N)]` is relatively representable (Katz–Mazur, 3.6.0)#

TheoremMultiplication by a nonzero integer `n` is an isogeny of degree `n²`#

TheoremThe `n`-torsion of an elliptic curve is étale where `n` is invertible (Katz–Mazur 2.3.1)#

DefinitionGalois theory for finite étale schemes over a field #

DefinitionFinite étale commutative group schemes over a field are finite Galois modules #

Theorem`GL₂(ℤ/Nℤ)` acts freely on `𝕄(𝒫, [Γ(N)])` for every rigid `𝒫`#

DefinitionCategoryTheory.CommMon.invariantSubalgebraPresheaf #

DefinitionTauCeti.DescentDatum.descended #

DefinitionTauCeti.StrictHenselization.algebra #