105 Introducing Algebraic Stacks

Chapter 105 of the Stacks Project, Introducing Algebraic Stacks, Tag 072H: the 4 sections of its 7 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 7 tags are carried by 24 declarations of the repository (all in StacksFrontier).

Section105.2 Preliminary#

Section 105.2 of the Stacks Project, Tag 072J. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 072J, the section

Tag 072J in the Stacks Project.

AlgebraicGeometry.ModuliEllipticCurves.PointedFamily, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliEllipticCurves.lean, line 74. The attribute's comment: “the triple (E, f, 0)”.

A family of schemes over S together with a section of its structure morphism, that is, a triple (E, f, 0).

structure PointedFamily (S : Scheme.{u})

AlgebraicGeometry.ModuliEllipticCurves.PointedFamily.IsElliptic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliEllipticCurves.lean, line 90. The attribute's comment: “an elliptic curve over S”.

A pointed family is an elliptic curve when its structure morphism is proper and smooth of relative dimension one and each of its fibres is a connected curve of genus one, that is, has one-dimensional H⁰ and H¹.

def IsElliptic {S : Scheme.{u}} (E : PointedFamily S) : Prop

Sources

• Section 105.2, Tag 072J
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.ModuliEllipticCurves.PointedFamily · AlgebraicGeometry.ModuliEllipticCurves.PointedFamily.IsElliptic

Section105.4 Fibre products#

Section 105.4 of the Stacks Project, Tag 072L. 3 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 072L, the section

Tag 072L in the Stacks Project.

AlgebraicGeometry.ModuliEllipticCurves.Comparison, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliEllipticCurves.lean, line 173. The attribute's comment: “the triples (a, a', α)”.

A T-point of S ×_{𝓜₁,₁} S': morphisms a : T ⟶ S and a' : T ⟶ S' together with an isomorphism α : E ×_{S,a} T ⟶ E' ×_{S',a'} T of elliptic curves over T, that is, one compatible with the structure morphisms and the sections.

structure Comparison {S S' : Scheme.{u}} (E : PointedFamily S) (E' : PointedFamily S')
    (T : Scheme.{u})

AlgebraicGeometry.ModuliEllipticCurves.Comparison.IsBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliEllipticCurves.lean, line 192. The attribute's comment: “pullback of the triples”.

The triple y over U is the base change of the triple x over T along h : U ⟶ T when the two morphisms to the bases compose with h and the two isomorphisms agree after the canonical projections of the pulled-back families.

def IsBaseChange {S S' T : Scheme.{u}} {E : PointedFamily S} {E' : PointedFamily S'}
    (x : Comparison E E' T) {U : Scheme.{u}} (h : U ⟶ T) (y : Comparison E E' U) : Prop

AlgebraicGeometry.ModuliEllipticCurves.RepresentsComparisons, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliEllipticCurves.lean, line 237. The attribute's comment: “the scheme S ×_{M_{1,1}} S'”.

A scheme P is a fibre product S ×_{𝓜₁,₁} S' when its T-points are the triples (a, a', α), naturally in T.

structure RepresentsComparisons {S S' : Scheme.{u}} (E : PointedFamily S)
    (E' : PointedFamily S') (P : Scheme.{u})

Tag 072M, a lemma

Tag 072M in the Stacks Project.

AlgebraicGeometry.ModuliEllipticCurves.exists_representsComparisons, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliEllipticCurvesFibreProduct.lean, line 86.

Stacks Project, Tag 072M. Key fact. For elliptic curves E over S and E' over S', the functor sending a scheme T to the triples (a, a', α) is representable by a scheme, the fibre product S ×_{𝓜₁,₁} S'.

theorem exists_representsComparisons (E : PointedFamily S) (E' : PointedFamily S')
    (hE : E.IsElliptic) (hE' : E'.IsElliptic) :
    ∃ P : Scheme.{u}, Nonempty (RepresentsComparisons E E' P)

Tag 072P, a definition

Tag 072P in the Stacks Project.

AlgebraicGeometry.ModuliEllipticCurves.PointedFamily.IsSmooth, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliEllipticCurves.lean, line 275.

A morphism S ⟶ 𝓜₁,₁, that is, an elliptic curve over S, is smooth when for every morphism S' ⟶ 𝓜₁,₁ the projection S ×_{𝓜₁,₁} S' ⟶ S' is a smooth morphism of schemes.

def PointedFamily.IsSmooth {S : Scheme.{u}} (E : PointedFamily S) (_hE : E.IsElliptic) : Prop

Sources

• Section 105.4, Tag 072L
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.ModuliEllipticCurves.Comparison · AlgebraicGeometry.ModuliEllipticCurves.Comparison.IsBaseChange · AlgebraicGeometry.ModuliEllipticCurves.RepresentsComparisons · AlgebraicGeometry.ModuliEllipticCurves.exists_representsComparisons · AlgebraicGeometry.ModuliEllipticCurves.PointedFamily.IsSmooth

Section105.5 The definition#

Section 105.5 of the Stacks Project, Tag 072Q. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 072R, a definition

Tag 072R in the Stacks Project.

AlgebraicGeometry.ModuliEllipticCurves.ModuliStackIsAlgebraic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuliEllipticCurvesAlgebraic.lean, line 189.

Stacks Project, Tag 072R. The moduli stack 𝓜₁,₁ of elliptic curves is an algebraic stack if and only if descent for objects holds for the étale topology on the category of all schemes, the key fact holds, and there exists a surjective and smooth morphism S ⟶ 𝓜₁,₁ from a scheme.

def ModuliStackIsAlgebraic : Prop

Sources

• Section 105.5, Tag 072Q
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.ModuliEllipticCurves.ModuliStackIsAlgebraic

Section105.6 A smooth cover#

Section 105.6 of the Stacks Project, Tag 072S. 2 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 072S, the section

Tag 072S in the Stacks Project.

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.Δ_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamily.lean, line 88. The attribute's comment: “the discriminant Δ, written out”.

The discriminant of a Weierstrass equation, written out as a polynomial in the five coefficients.

theorem Δ_eq {R : Type*} [CommRing R] (W : WeierstrassCurve R) :
    W.Δ = -W.a₆ * W.a₁ ^ 6 + W.a₄ * W.a₃ * W.a₁ ^ 5
      + ((-W.a₃ ^ 2 - 12 * W.a₆) * W.a₂ + W.a₄ ^ 2) * W.a₁ ^ 4
      + (8 * W.a₄ * W.a₃ * W.a₂ + (W.a₃ ^ 3 + 36 * W.a₆ * W.a₃)) * W.a₁ ^ 3
      + ((-8 * W.a₃ ^ 2 - 48 * W.a₆) * W.a₂ ^ 2 + 8 * W.a₄ ^ 2 * W.a₂
        + (-30 * W.a₄ * W.a₃ ^ 2 + 72 * W.a₆ * W.a₄)) * W.a₁ ^ 2
      + (16 * W.a₄ * W.a₃ * W.a₂ ^ 2 + (36 * W.a₃ ^ 3 + 144 * W.a₆ * W.a₃) * W.a₂
        - 96 * W.a₄ ^ 2 * W.a₃) * W.a₁
      + (-16 * W.a₃ ^ 2 - 64 * W.a₆) * W.a₂ ^ 3 + 16 * W.a₄ ^ 2 * W.a₂ ^ 2
      + (72 * W.a₄ * W.a₃ ^ 2 + 288 * W.a₆ * W.a₄) * W.a₂
      + (-27 * W.a₃ ^ 4 - 216 * W.a₆ * W.a₃ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2)

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.Δ_smul_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamily.lean, line 106. The attribute's comment: “Δ is homogeneous of degree 12 for deg aᵢ = i”.

The discriminant is homogeneous of degree 12 in the coefficients, where aᵢ has degree i: scaling aᵢ by tⁱ scales Δ by t¹².

theorem Δ_smul_eq {R : Type*} [CommRing R] (t a₁ a₂ a₃ a₄ a₆ : R) :
    (⟨t * a₁, t ^ 2 * a₂, t ^ 3 * a₃, t ^ 4 * a₄, t ^ 6 * a₆⟩ : WeierstrassCurve R).Δ =
      t ^ 12 * (⟨a₁, a₂, a₃, a₄, a₆⟩ : WeierstrassCurve R).Δ

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.base, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamily.lean, line 130. The attribute's comment: “the Weierstrass scheme W”.

The Weierstrass scheme W = Spec(ℤ[a₁, a₂, a₃, a₄, a₆, 1/Δ]).

abbrev base : Scheme.{u}

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.total, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamily.lean, line 314. The attribute's comment: “the plane cubic E_W”.

The plane cubic E_W ⊂ P²_W cut out by the Weierstrass equation over W.

abbrev total : Scheme.{u}

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.embedding, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamily.lean, line 318. The attribute's comment: “E_W is a closed subscheme of P²_W”.

The closed immersion of E_W into P²_W.

abbrev embedding : total.{u} ⟶ projectivePlane.{u}

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.projection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamily.lean, line 324. The attribute's comment: “the projection f_W : E_W → W”.

The projection f_W : E_W ⟶ W.

abbrev projection : total.{u} ⟶ base.{u}

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.zero, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamily.lean, line 328. The attribute's comment: “the section 0_W = (0 : 1 : 0)”.

The section 0_W : W ⟶ E_W at infinity, the point (0 : 1 : 0).

abbrev zero : base.{u} ⟶ total.{u}

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.family, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamily.lean, line 338. The attribute's comment: “the triple (E_W, f_W, 0_W)”.

The Weierstrass family (E_W, f_W, 0_W): the plane cubic over W = Spec(ℤ[a₁, a₂, a₃, a₄, a₆, 1/Δ]) with the section (0 : 1 : 0) at infinity.

abbrev family : PointedFamily base.{u}

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.isElliptic_familyOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamilyElliptic.lean, line 113. The attribute's comment: “E_W over a ring with Δ invertible is an elliptic curve”.

Stacks Project, Tag 072S. The plane cubic of a Weierstrass equation with invertible discriminant, with its section at infinity, is an elliptic curve over Spec R.

theorem isElliptic_familyOf [C.IsElliptic] : (familyOf C).IsElliptic

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.isElliptic_family, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamilyElliptic.lean, line 124. The attribute's comment: “(E_W, f_W, 0_W) is an elliptic curve”.

Stacks Project, Tag 072S. The Weierstrass family (E_W, f_W, 0_W) over W = Spec(ℤ[a₁, a₂, a₃, a₄, a₆, 1/Δ]) is an elliptic curve.

theorem isElliptic_family : family.{u}.IsElliptic

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.finrank_structureSheafCohomology_projectionOf_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamilyFibres.lean, line 228. The attribute's comment: “H⁰ of a fibre is one-dimensional”.

Over a field, the global functions on the plane cubic are the constants: dim_k H⁰(E, 𝒪_E) = 1.

theorem finrank_structureSheafCohomology_projectionOf_zero :
    Module.finrank k (structureSheafCohomology (projectionOf C) 0) = 1

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.genus_projectionOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamilyFibres.lean, line 241. The attribute's comment: “a fibre has genus one”.

Over a field, the plane cubic has genus one: (3 - 1)(3 - 2)/2 = 1.

theorem genus_projectionOf : genus (projectionOf C) = 1

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.isProper_projectionOf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamilyProper.lean, line 60. The attribute's comment: “f_W is proper”.

The plane cubic of a Weierstrass equation is proper over the base.

instance isProper_projectionOf : IsProper (projectionOf C)

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.smoothOfRelativeDimension_projectionOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassFamilySmooth.lean, line 417. The attribute's comment: “f_W is smooth of relative dimension one”.

A Weierstrass cubic with invertible discriminant is smooth of relative dimension one over its base.

theorem smoothOfRelativeDimension_projectionOf (hΔ : IsUnit W.Δ) :
    SmoothOfRelativeDimension 1 (projectionOf W)

Tag 072T, a lemma

Tag 072T in the Stacks Project.

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.isSmooth_family, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassSmoothCover.lean, line 214. The attribute's comment: “the morphism W → M_{1,1} is smooth”.

Stacks Project, Tag 072T. The morphism W ⟶ 𝓜₁,₁ given by the Weierstrass family (E_W, f_W, 0_W) is smooth: for every elliptic curve E' over a scheme S' and every fibre product P = W ×_{𝓜₁,₁} S', the projection P ⟶ S' is smooth. Over an open of S' on which E' has a Weierstrass equation, P is the base change of the smooth projection H × W ⟶ W, because H × W is the fibre product W ×_{𝓜₁,₁} W.

theorem isSmooth_family : family.{u}.IsSmooth isElliptic_family.{u}

AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.isSurjective_family, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/WeierstrassSmoothCover.lean, line 225. The attribute's comment: “the morphism W → M_{1,1} is surjective”.

Stacks Project, Tag 072T. The morphism W ⟶ 𝓜₁,₁ given by the Weierstrass family (E_W, f_W, 0_W) is surjective: for every elliptic curve E' over a scheme S' and every fibre product P = W ×_{𝓜₁,₁} S', the projection P ⟶ S' is surjective, because the fibre of E' at each point has a Weierstrass equation.

theorem isSurjective_family : family.{u}.IsSurjective isElliptic_family.{u}

Sources

• Section 105.6, Tag 072S
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.ModuliEllipticCurves.Weierstrass.Δ_eq · AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.Δ_smul_eq · AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.base · AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.total · AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.embedding · AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.projection · AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.zero · AlgebraicGeometry.ModuliEllipticCurves.Weierstrass.family

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.