The category Ell/B of elliptic curves over B-schemes

Let B be a scheme. The category Ell/B of Katz and Mazur has as objects the pairs (S, E) of a B-scheme S and an elliptic curve E over S (EllipticCurveGeom S), and as arrows (S', E') ⟶ (S, E) the pairs of a morphism of B-schemes f : S' ⟶ S and a morphism g : E' ⟶ E carrying the zero section of E' to that of E, such that the square formed by g, f and the two structure morphisms is cartesian. Thus every arrow exhibits its source as a base change of its target. For a ring R, the category Ell/R of Katz and Mazur is Ell/Spec R. A moduli problem is a contravariant functor on this category.

The forgetful functor EllObj.forget B : Ell/B ⥤ Sch/B, sending (S, E) to S, makes Ell/B a category fibred in groupoids over Sch/B:

• every arrow of Ell/B is strongly cartesian (EllObj.isStronglyCartesian): an arrow X ⟶ Z factors through an arrow Y ⟶ Z along any compatible morphism of bases, uniquely (EllObj.Hom.lift and EllObj.Hom.eq_lift), because the square of Y ⟶ Z is cartesian;
• every morphism T ⟶ S of B-schemes has a lift with target (S, E), namely the base change of E to T (EllObj.baseChangeHom), so EllObj.forget B is a fibered category;
• consequently an arrow of Ell/B is an isomorphism exactly when its morphism of bases is (EllObj.isIso_iff_isIso_base), and the fibre of Ell/B over a B-scheme S is the groupoid of elliptic curves over S.

Base change of a fixed object X = (S, E) is functorial in the scheme over S (EllObj.baseChangeFunctor), with the canonical morphisms EllipticCurveGeom.baseChangeMap between base changes as the morphisms of total spaces, and with the projections EllObj.baseChangeFunctorHom to X. Along an arrow f : X ⟶ Y of Ell/B, base change of X is base change of Y along the composite with f.base (EllObj.baseChangeFunctorIso); this is what makes the fibres of moduli problems over Ell/B compatible with base change.

The T-points of the base change E_T of X = (S, E) to a scheme T over S are the points of E with values in T (EllObj.baseChangePointsEquiv), naturally in T (EllObj.baseChangePointsEquiv_pointsPullback).

An arrow of Ell/B is determined by its morphism of total spaces (EllObj.hom_ext): the morphism of bases is recovered through the zero section (EllObj.Hom.base_eq). It is automatically compatible with the group laws (EllObj.Hom.addition_total and EllObj.Hom.neg_total).

Main definitions

• TauCeti.AlgebraicGeometry.EllObj B: the objects of Ell/B.
• TauCeti.AlgebraicGeometry.EllObj.Hom X Y: the arrows of Ell/B, cartesian pointed morphisms of elliptic curves over morphisms of B-schemes, with the category structure EllObj.category.
• TauCeti.AlgebraicGeometry.EllObj.forget B: the functor Ell/B ⥤ Over B to the base.
• TauCeti.AlgebraicGeometry.EllObj.baseChange and TauCeti.AlgebraicGeometry.EllObj.baseChangeHom: the base change of an object along a morphism of B-schemes, with its arrow to the object.
• TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctor X: base change of an object X = (S, E) of Ell/B as a functor from schemes over S to Ell/B.
• TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctorIso f: for an arrow f : X ⟶ Y, the natural isomorphism between base change of X and base change of Y along the composite with f.base.
• TauCeti.AlgebraicGeometry.EllObj.isoBaseChange g: for an arrow g : X ⟶ Y, the isomorphism of X with the base change of Y along g.base.
• TauCeti.AlgebraicGeometry.EllObj.baseChangePointsEquiv X T: the T-points of the base change of X = (S, E) to T are the points of E with values in T.
• TauCeti.AlgebraicGeometry.EllObj.prodCurve B C: an elliptic curve C over a scheme M, pulled back to B × M, as an object of Ell/B; prodCurvePoint B R is the pullback of a point R of C.
• TauCeti.AlgebraicGeometry.EllObj.homProdCurveEquiv X: arrows X ⟶ prodCurve B C are the cartesian morphisms from the curve of X to C preserving the zero sections.

Main results

• TauCeti.AlgebraicGeometry.EllObj.isStronglyCartesian: every arrow of Ell/B is strongly cartesian over Sch/B.
• TauCeti.AlgebraicGeometry.EllObj.isFibered_forget: Ell/B is a fibered category over Sch/B.
• TauCeti.AlgebraicGeometry.EllObj.isIso_iff_isIso_base: an arrow of Ell/B is an isomorphism if and only if its morphism of bases is.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Chapter 4.
• The Stacks Project, Categories, Section Fibred categories (Tag 02XJ) and Section Categories fibred in groupoids (Tag 003S).

structure TauCeti.AlgebraicGeometry.EllObj (B : AlgebraicGeometry.Scheme) : Type (u + 1)

An object of Ell/B: a scheme base over B, through structureMap, together with an elliptic curve curve over base. For a ring R, the objects of the category Ell/R of Katz and Mazur are the objects of EllObj (Spec R).

• base : AlgebraicGeometry.Scheme

  The base scheme S of the elliptic curve.

• structureMap : self.base ⟶ B

  The structure morphism S ⟶ B of the base.

• curve : EllipticCurveGeom self.base

  The elliptic curve over S.

structure TauCeti.AlgebraicGeometry.EllObj.Hom {B : AlgebraicGeometry.Scheme} (X Y : EllObj B) : Type u

An arrow of Ell/B from X = (S', E') to Y = (S, E): a morphism of B-schemes base : S' ⟶ S and a morphism total : E' ⟶ E of total spaces such that the square formed by total, base and the two structure morphisms is cartesian, and carrying the zero section of E' to that of E. It exhibits E' as the base change of E along base.

• base : X.base ⟶ Y.base

  The morphism of bases.

• base_structureMap : CategoryTheory.CategoryStruct.comp self.base Y.structureMap = X.structureMap

  The morphism of bases is a morphism of B-schemes.

• total : X.curve.carrier ⟶ Y.curve.carrier

  The morphism of total spaces.

• isPullback : CategoryTheory.IsPullback self.total X.curve.structureMap Y.curve.structureMap self.base

  The square formed by total, base and the structure morphisms is cartesian.

• zero_total : CategoryTheory.CategoryStruct.comp X.curve.zero self.total = CategoryTheory.CategoryStruct.comp self.base Y.curve.zero

  The morphism of total spaces carries the zero section to the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.zero_total_assoc {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (self : X.Hom Y) {Z : AlgebraicGeometry.Scheme} (h : Y.curve.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp X.curve.zero (CategoryTheory.CategoryStruct.comp self.total h) = CategoryTheory.CategoryStruct.comp self.base (CategoryTheory.CategoryStruct.comp Y.curve.zero h)

The morphism of total spaces carries the zero section to the zero section.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.base_structureMap_assoc {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (self : X.Hom Y) {Z : AlgebraicGeometry.Scheme} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp self.base (CategoryTheory.CategoryStruct.comp Y.structureMap h) = CategoryTheory.CategoryStruct.comp X.structureMap h

The morphism of bases is a morphism of B-schemes.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.total_structureMap {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X.Hom Y) : CategoryTheory.CategoryStruct.comp f.total Y.curve.structureMap = CategoryTheory.CategoryStruct.comp X.curve.structureMap f.base

The morphism of total spaces of an arrow of Ell/B lies over its morphism of bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.total_structureMap_assoc {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X.Hom Y) {Z : AlgebraicGeometry.Scheme} (h : Y.base ⟶ Z) : CategoryTheory.CategoryStruct.comp f.total (CategoryTheory.CategoryStruct.comp Y.curve.structureMap h) = CategoryTheory.CategoryStruct.comp X.curve.structureMap (CategoryTheory.CategoryStruct.comp f.base h)

The morphism of total spaces of an arrow of Ell/B lies over its morphism of bases.

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.addition_total {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X.Hom Y) : CategoryTheory.CategoryStruct.comp X.curve.addition f.total = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map X.curve.structureMap X.curve.structureMap Y.curve.structureMap Y.curve.structureMap f.total f.total f.base ⋯ ⋯) Y.curve.addition

The morphism of total spaces of an arrow of Ell/B carries the addition morphism of its source to that of its target.

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.addition_total_assoc {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X.Hom Y) {Z : AlgebraicGeometry.Scheme} (h : Y.curve.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp X.curve.addition (CategoryTheory.CategoryStruct.comp f.total h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map X.curve.structureMap X.curve.structureMap Y.curve.structureMap Y.curve.structureMap f.total f.total f.base ⋯ ⋯) (CategoryTheory.CategoryStruct.comp Y.curve.addition h)

The morphism of total spaces of an arrow of Ell/B carries the addition morphism of its source to that of its target.

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.neg_total {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X.Hom Y) : CategoryTheory.CategoryStruct.comp X.curve.neg f.total = CategoryTheory.CategoryStruct.comp f.total Y.curve.neg

The morphism of total spaces of an arrow of Ell/B carries the negation morphism of its source to that of its target.

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.neg_total_assoc {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X.Hom Y) {Z : AlgebraicGeometry.Scheme} (h : Y.curve.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp X.curve.neg (CategoryTheory.CategoryStruct.comp f.total h) = CategoryTheory.CategoryStruct.comp f.total (CategoryTheory.CategoryStruct.comp Y.curve.neg h)

The morphism of total spaces of an arrow of Ell/B carries the negation morphism of its source to that of its target.

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.base_eq {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X.Hom Y) : f.base = CategoryTheory.CategoryStruct.comp X.curve.zero (CategoryTheory.CategoryStruct.comp f.total Y.curve.structureMap)

The morphism of bases of an arrow of Ell/B is determined by its morphism of total spaces: it is the composite of the zero section, the morphism of total spaces and the structure morphism.

@[instance_reducible]

instance TauCeti.AlgebraicGeometry.EllObj.category {B : AlgebraicGeometry.Scheme} : CategoryTheory.Category.{u, u + 1} (EllObj B)

The category Ell/B, whose arrows are the cartesian pointed morphisms EllObj.Hom. The composite of two arrows pastes their cartesian squares.

theorem TauCeti.AlgebraicGeometry.EllObj.hom_ext {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} {f g : X ⟶ Y} (h : f.total = g.total) : f = g

Extensionality for arrows of Ell/B: two arrows with the same morphism of total spaces are equal.

theorem TauCeti.AlgebraicGeometry.EllObj.hom_ext_iff {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} {f g : X ⟶ Y} : f = g ↔ f.total = g.total

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.id_base {B : AlgebraicGeometry.Scheme} (X : EllObj B) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id X.base

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.id_total {B : AlgebraicGeometry.Scheme} (X : EllObj B) : (CategoryTheory.CategoryStruct.id X).total = CategoryTheory.CategoryStruct.id X.curve.carrier

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.comp_base {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.comp_total {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).total = CategoryTheory.CategoryStruct.comp f.total g.total

The cartesian factorisation

noncomputable def TauCeti.AlgebraicGeometry.EllObj.Hom.lift {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (g : Y ⟶ Z) (f : X ⟶ Z) (h : X.base ⟶ Y.base) (hh : CategoryTheory.CategoryStruct.comp h g.base = f.base) : X ⟶ Y

The cartesian factorisation in Ell/B. Given arrows g : Y ⟶ Z and f : X ⟶ Z and a morphism of bases h : X.base ⟶ Y.base with h ≫ g.base = f.base, this is the arrow X ⟶ Y over h whose composite with g is f (Hom.lift_comp). It is unique (Hom.eq_lift). Its morphism of total spaces is EllipticCurveGeom.baseChangeLift, induced by the cartesian square of g.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.lift_base {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (g : Y ⟶ Z) (f : X ⟶ Z) (h : X.base ⟶ Y.base) (hh : CategoryTheory.CategoryStruct.comp h g.base = f.base) : (lift g f h hh).base = h

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.lift_total_total {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (g : Y ⟶ Z) (f : X ⟶ Z) (h : X.base ⟶ Y.base) (hh : CategoryTheory.CategoryStruct.comp h g.base = f.base) : CategoryTheory.CategoryStruct.comp (lift g f h hh).total g.total = f.total

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.lift_total_total_assoc {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (g : Y ⟶ Z) (f : X ⟶ Z) (h : X.base ⟶ Y.base) (hh : CategoryTheory.CategoryStruct.comp h g.base = f.base) {Z✝ : AlgebraicGeometry.Scheme} (h✝ : Z.curve.carrier ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (lift g f h hh).total (CategoryTheory.CategoryStruct.comp g.total h✝) = CategoryTheory.CategoryStruct.comp f.total h✝

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.lift_comp {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (g : Y ⟶ Z) (f : X ⟶ Z) (h : X.base ⟶ Y.base) (hh : CategoryTheory.CategoryStruct.comp h g.base = f.base) : CategoryTheory.CategoryStruct.comp (lift g f h hh) g = f

The cartesian factorisation Hom.lift g f h hh composed with g is f.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.lift_comp_assoc {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (g : Y ⟶ Z) (f : X ⟶ Z) (h : X.base ⟶ Y.base) (hh : CategoryTheory.CategoryStruct.comp h g.base = f.base) {Z✝ : EllObj B} (h✝ : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (lift g f h hh) (CategoryTheory.CategoryStruct.comp g h✝) = CategoryTheory.CategoryStruct.comp f h✝

The cartesian factorisation Hom.lift g f h hh composed with g is f.

theorem TauCeti.AlgebraicGeometry.EllObj.Hom.eq_lift {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (g : Y ⟶ Z) (f : X ⟶ Z) (h : X.base ⟶ Y.base) (hh : CategoryTheory.CategoryStruct.comp h g.base = f.base) (k : X ⟶ Y) (hk : CategoryTheory.CategoryStruct.comp k g = f) (hkb : k.base = h) : k = lift g f h hh

Uniqueness of the cartesian factorisation. An arrow k : X ⟶ Y over h whose composite with g is f is the cartesian factorisation Hom.lift g f h hh.

The forgetful functor to the base

def TauCeti.AlgebraicGeometry.EllObj.forget (B : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (EllObj B) (CategoryTheory.Over B)

The forgetful functor Ell/B ⥤ Sch/B, sending an elliptic curve E over a B-scheme S to S, and an arrow of Ell/B to its morphism of bases.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.forget_obj (B : AlgebraicGeometry.Scheme) (X : EllObj B) : (forget B).obj X = CategoryTheory.Over.mk X.structureMap

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.forget_map (B : AlgebraicGeometry.Scheme) {X✝ Y✝ : EllObj B} (f : X✝ ⟶ Y✝) : (forget B).map f = CategoryTheory.Over.homMk f.base ⋯

theorem TauCeti.AlgebraicGeometry.EllObj.isHomLift_of_base_eq {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} {f : X ⟶ Y} {g : (forget B).obj X ⟶ (forget B).obj Y} (h : f.base = CategoryTheory.Over.Hom.left g) : (forget B).IsHomLift g f

An arrow of Ell/B lies over every morphism of B-schemes with the same underlying morphism of schemes as its morphism of bases.

instance TauCeti.AlgebraicGeometry.EllObj.isStronglyCartesian {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} {R S : CategoryTheory.Over B} (g : R ⟶ S) (f : X ⟶ Y) [(forget B).IsHomLift g f] : (forget B).IsStronglyCartesian g f

Every arrow of Ell/B is strongly cartesian over Sch/B: the cartesian factorisation Hom.lift is the unique lift of a morphism of bases.

theorem TauCeti.AlgebraicGeometry.EllObj.hom_ext_of_comp {B : AlgebraicGeometry.Scheme} {X Y Z : EllObj B} (g : Y ⟶ Z) {k k' : X ⟶ Y} (hk : CategoryTheory.CategoryStruct.comp k g = CategoryTheory.CategoryStruct.comp k' g) (hb : k.base = k'.base) : k = k'

Two arrows X ⟶ Y of Ell/B with the same morphism of bases and the same composite with an arrow g : Y ⟶ Z are equal, since g is strongly cartesian.

Base change

noncomputable def TauCeti.AlgebraicGeometry.EllObj.baseChange {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T : CategoryTheory.Over B} (g : T ⟶ (forget B).obj X) : EllObj B

The base change of an object X = (S, E) of Ell/B along a morphism g : T ⟶ S of B-schemes: the elliptic curve E.baseChange g.left over T.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChange_structureMap {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T : CategoryTheory.Over B} (g : T ⟶ (forget B).obj X) : (X.baseChange g).structureMap = T.hom

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChange_curve {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T : CategoryTheory.Over B} (g : T ⟶ (forget B).obj X) : (X.baseChange g).curve = X.curve.baseChange (CategoryTheory.Over.Hom.left g)

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChange_base {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T : CategoryTheory.Over B} (g : T ⟶ (forget B).obj X) : (X.baseChange g).base = T.left

noncomputable def TauCeti.AlgebraicGeometry.EllObj.baseChangeHom {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T : CategoryTheory.Over B} (g : T ⟶ (forget B).obj X) : X.baseChange g ⟶ X

The arrow of Ell/B from the base change of X along g to X, lying over g. Its morphism of total spaces is the first projection of the fibre product.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeHom_base {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T : CategoryTheory.Over B} (g : T ⟶ (forget B).obj X) : (X.baseChangeHom g).base = CategoryTheory.Over.Hom.left g

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeHom_total {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T : CategoryTheory.Over B} (g : T ⟶ (forget B).obj X) : (X.baseChangeHom g).total = CategoryTheory.CategoryStruct.comp (X.curve.baseChangeIso (CategoryTheory.Over.Hom.left g)).hom (CategoryTheory.Limits.pullback.fst X.curve.structureMap (CategoryTheory.Over.Hom.left g))

instance TauCeti.AlgebraicGeometry.EllObj.isHomLift_baseChangeHom {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T : CategoryTheory.Over B} (g : T ⟶ (forget B).obj X) : (forget B).IsHomLift g (X.baseChangeHom g)

The arrow baseChangeHom X g lies over g.

instance TauCeti.AlgebraicGeometry.EllObj.isFibered_forget {B : AlgebraicGeometry.Scheme} : (forget B).IsFibered

Ell/B is fibred over Sch/B: every morphism of B-schemes T ⟶ S lifts to an arrow of Ell/B with target any given elliptic curve over S, namely the base change. Since every arrow of Ell/B is cartesian, Ell/B is a category fibred in groupoids.

noncomputable def TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctor {B : AlgebraicGeometry.Scheme} (X : EllObj B) : CategoryTheory.Functor (CategoryTheory.Over X.base) (EllObj B)

The base-change functor of an object X = (S, E) of Ell/B: it sends a scheme T over S, through t : T ⟶ S, to the elliptic curve E.baseChange t over the B-scheme T, and a morphism k : T' ⟶ T of schemes over S to the arrow of Ell/B over k whose morphism of total spaces is the canonical morphism E.baseChangeMap k between the base changes.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctor_map_total {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) : (X.baseChangeFunctor.map k).total = X.curve.baseChangeMap (CategoryTheory.Over.Hom.left k) ⋯

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctor_obj_base {B : AlgebraicGeometry.Scheme} (X : EllObj B) (T : CategoryTheory.Over X.base) : (X.baseChangeFunctor.obj T).base = T.left

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctor_map_base {B : AlgebraicGeometry.Scheme} (X : EllObj B) {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) : (X.baseChangeFunctor.map k).base = CategoryTheory.Over.Hom.left k

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctor_obj_curve {B : AlgebraicGeometry.Scheme} (X : EllObj B) (T : CategoryTheory.Over X.base) : (X.baseChangeFunctor.obj T).curve = X.curve.baseChange T.hom

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctor_obj_structureMap {B : AlgebraicGeometry.Scheme} (X : EllObj B) (T : CategoryTheory.Over X.base) : (X.baseChangeFunctor.obj T).structureMap = CategoryTheory.CategoryStruct.comp T.hom X.structureMap

theorem TauCeti.AlgebraicGeometry.EllObj.isIso_iff_isIso_base {B : AlgebraicGeometry.Scheme} {Y : EllObj B} (X : EllObj B) (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.base

An arrow of Ell/B is an isomorphism if and only if its morphism of bases is. In particular, every arrow of Ell/B lying over the identity of its base is an isomorphism, so the fibres of Ell/B are groupoids.

instance TauCeti.AlgebraicGeometry.EllObj.isIso_base {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.base

The morphism of bases of an isomorphism of Ell/B is an isomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.inv_base {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (CategoryTheory.inv f).base = CategoryTheory.inv f.base

The morphism of bases of the inverse of an isomorphism of Ell/B is the inverse of its morphism of bases.

Base change along an arrow of Ell/B

noncomputable def TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctorHom {B : AlgebraicGeometry.Scheme} (X : EllObj B) (T : CategoryTheory.Over X.base) : X.baseChangeFunctor.obj T ⟶ X

The arrow of Ell/B from the base change X.baseChangeFunctor.obj T of X = (S, E) along T ⟶ S to X, lying over the structure morphism of T: the arrow baseChangeHom along T ⟶ S, whose source is X.baseChangeFunctor.obj T by definition. Its morphism of total spaces is the first projection of the fibre product.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctorHom_base {B : AlgebraicGeometry.Scheme} {X : EllObj B} (T : CategoryTheory.Over X.base) : (X.baseChangeFunctorHom T).base = T.hom

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctorHom_total {B : AlgebraicGeometry.Scheme} {X : EllObj B} (T : CategoryTheory.Over X.base) : (X.baseChangeFunctorHom T).total = CategoryTheory.CategoryStruct.comp (X.curve.baseChangeIso T.hom).hom (CategoryTheory.Limits.pullback.fst X.curve.structureMap T.hom)

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctor_map_baseChangeFunctorHom {B : AlgebraicGeometry.Scheme} {X : EllObj B} {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) : CategoryTheory.CategoryStruct.comp (X.baseChangeFunctor.map k) (X.baseChangeFunctorHom T) = X.baseChangeFunctorHom T'

The arrows baseChangeFunctorHom are natural in the scheme over the base of X.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctor_map_baseChangeFunctorHom_assoc {B : AlgebraicGeometry.Scheme} {X : EllObj B} {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) {Z : EllObj B} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.baseChangeFunctor.map k) (CategoryTheory.CategoryStruct.comp (X.baseChangeFunctorHom T) h) = CategoryTheory.CategoryStruct.comp (X.baseChangeFunctorHom T') h

The arrows baseChangeFunctorHom are natural in the scheme over the base of X.

noncomputable def TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctorIso {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X ⟶ Y) : X.baseChangeFunctor ≅ (CategoryTheory.Over.map f.base).comp Y.baseChangeFunctor

Base change along an arrow of Ell/B. For an arrow f : X ⟶ Y of Ell/B, the base change of X along a scheme T over X.base is identified with the base change of Y along the composite T ⟶ X.base ⟶ Y.base, naturally in T. The component at T lies over the identity of T (baseChangeFunctorIso_hom_app_base) and is the cartesian factorisation of X.baseChangeFunctorHom T ≫ f through Y.baseChangeFunctorHom (baseChangeFunctorIso_hom_app_comp).

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctorIso_hom_app_base {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X ⟶ Y) (T : CategoryTheory.Over X.base) : ((baseChangeFunctorIso f).hom.app T).base = CategoryTheory.CategoryStruct.id T.left

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctorIso_hom_app_comp {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X ⟶ Y) (T : CategoryTheory.Over X.base) : CategoryTheory.CategoryStruct.comp ((baseChangeFunctorIso f).hom.app T) (Y.baseChangeFunctorHom ((CategoryTheory.Over.map f.base).obj T)) = CategoryTheory.CategoryStruct.comp (X.baseChangeFunctorHom T) f

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangeFunctorIso_hom_app_comp_assoc {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (f : X ⟶ Y) (T : CategoryTheory.Over X.base) {Z : EllObj B} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((baseChangeFunctorIso f).hom.app T) (CategoryTheory.CategoryStruct.comp (Y.baseChangeFunctorHom ((CategoryTheory.Over.map f.base).obj T)) h) = CategoryTheory.CategoryStruct.comp (X.baseChangeFunctorHom T) (CategoryTheory.CategoryStruct.comp f h)

Arrows of Ell/B as base changes

noncomputable def TauCeti.AlgebraicGeometry.EllObj.isoBaseChange {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (g : X ⟶ Y) : X ≅ Y.baseChangeFunctor.obj (CategoryTheory.Over.mk g.base)

Every arrow of Ell/B exhibits its source as a base change of its target. For an arrow g : X ⟶ Y of Ell/B, this is the isomorphism of X with the base change of Y along g.base : X.base ⟶ Y.base. It lies over the identity of X.base (isoBaseChange_hom_base), and its composite with the projection of the base change to Y is g (isoBaseChange_hom_comp). It is the cartesian factorisation of g through Y.baseChangeFunctorHom.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.isoBaseChange_hom_base {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (g : X ⟶ Y) : (isoBaseChange g).hom.base = CategoryTheory.CategoryStruct.id X.base

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.isoBaseChange_inv_base {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (g : X ⟶ Y) : (isoBaseChange g).inv.base = CategoryTheory.CategoryStruct.id X.base

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.isoBaseChange_hom_comp {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (isoBaseChange g).hom (Y.baseChangeFunctorHom (CategoryTheory.Over.mk g.base)) = g

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.isoBaseChange_hom_comp_assoc {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (g : X ⟶ Y) {Z : EllObj B} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoBaseChange g).hom (CategoryTheory.CategoryStruct.comp (Y.baseChangeFunctorHom (CategoryTheory.Over.mk g.base)) h) = CategoryTheory.CategoryStruct.comp g h

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.isoBaseChange_inv_comp {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (isoBaseChange g).inv g = Y.baseChangeFunctorHom (CategoryTheory.Over.mk g.base)

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.isoBaseChange_inv_comp_assoc {B : AlgebraicGeometry.Scheme} {X Y : EllObj B} (g : X ⟶ Y) {Z : EllObj B} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoBaseChange g).inv (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (Y.baseChangeFunctorHom (CategoryTheory.Over.mk g.base)) h

Points of base changes

noncomputable def TauCeti.AlgebraicGeometry.EllObj.baseChangePointsEquiv {B : AlgebraicGeometry.Scheme} (X : EllObj B) (T : CategoryTheory.Over X.base) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (X.baseChangeFunctor.obj T).base) ⟶ CategoryTheory.Over.mk (X.baseChangeFunctor.obj T).curve.structureMap) ≃* (T ⟶ CategoryTheory.Over.mk X.curve.structureMap)

Points of a base change. For an object X = (S, E) of Ell/B and a scheme T over S, composing with the projection E_T ⟶ E identifies the group of T-points of the base change E_T of E to T with the group of points of E with values in T.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangePointsEquiv_apply_left {B : AlgebraicGeometry.Scheme} {X : EllObj B} {T : CategoryTheory.Over X.base} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (X.baseChangeFunctor.obj T).base) ⟶ CategoryTheory.Over.mk (X.baseChangeFunctor.obj T).curve.structureMap) : CategoryTheory.Over.Hom.left ((X.baseChangePointsEquiv T) P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left P) (X.baseChangeFunctorHom T).total

theorem TauCeti.AlgebraicGeometry.EllObj.baseChangePointsEquiv_pointsPullback {B : AlgebraicGeometry.Scheme} {X : EllObj B} {T' T : CategoryTheory.Over X.base} (k : T' ⟶ T) (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (X.baseChangeFunctor.obj T).base) ⟶ CategoryTheory.Over.mk (X.baseChangeFunctor.obj T).curve.structureMap) : (X.baseChangePointsEquiv T') ((EllipticCurveGeom.pointsPullback ⋯ ⋯) P) = CategoryTheory.CategoryStruct.comp k ((X.baseChangePointsEquiv T) P)

Points of base changes are natural. Along a morphism k : T' ⟶ T of schemes over the base of X, the base change to E_{T'} of a T-point of E_T corresponds to the point of E with values in T precomposed with k.

Elliptic curves over a product with B

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.EllObj.prodCurve (B : AlgebraicGeometry.Scheme) {M : AlgebraicGeometry.Scheme} (C : EllipticCurveGeom M) : EllObj B

An elliptic curve over a product with B. For an elliptic curve C over a scheme M, the object of Ell/B given by C pulled back to B × M along the second projection, over B through the first projection. Universal families, such as the universal elliptic curve with a basis of its 3-torsion over M = Spec ℤ[1/3, ζ₃][μ, 1/(μ³ - 1)], are objects of this form.

noncomputable def TauCeti.AlgebraicGeometry.EllObj.prodCurveProj (B : AlgebraicGeometry.Scheme) {M : AlgebraicGeometry.Scheme} (C : EllipticCurveGeom M) : (prodCurve B C).curve.carrier ⟶ C.carrier

The projection from the total space of prodCurve B C to that of C.

theorem TauCeti.AlgebraicGeometry.EllObj.isPullback_prodCurveProj (B : AlgebraicGeometry.Scheme) {M : AlgebraicGeometry.Scheme} (C : EllipticCurveGeom M) : CategoryTheory.IsPullback (prodCurveProj B C) (prodCurve B C).curve.structureMap C.structureMap CategoryTheory.Limits.prod.snd

The curve of prodCurve B C is the base change of C along the second projection.

theorem TauCeti.AlgebraicGeometry.EllObj.zero_prodCurveProj (B : AlgebraicGeometry.Scheme) {M : AlgebraicGeometry.Scheme} (C : EllipticCurveGeom M) : CategoryTheory.CategoryStruct.comp (prodCurve B C).curve.zero (prodCurveProj B C) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd C.zero

The projection prodCurveProj B C carries the zero section to the zero section.

theorem TauCeti.AlgebraicGeometry.EllObj.zero_prodCurveProj_assoc (B : AlgebraicGeometry.Scheme) {M : AlgebraicGeometry.Scheme} (C : EllipticCurveGeom M) {Z : AlgebraicGeometry.Scheme} (h : C.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (C.baseChange CategoryTheory.Limits.prod.snd).zero (CategoryTheory.CategoryStruct.comp (prodCurveProj B C) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp C.zero h)

The projection prodCurveProj B C carries the zero section to the zero section.

instance TauCeti.AlgebraicGeometry.EllObj.isAffineHom_prodCurve_structureMap (B : AlgebraicGeometry.Scheme) {M : AlgebraicGeometry.Scheme} (C : EllipticCurveGeom M) [AlgebraicGeometry.IsAffine M] : AlgebraicGeometry.IsAffineHom (prodCurve B C).structureMap

The structure morphism of prodCurve B C is affine when M is affine.

instance TauCeti.AlgebraicGeometry.EllObj.isAffine_prodCurve_base (B : AlgebraicGeometry.Scheme) {M : AlgebraicGeometry.Scheme} (C : EllipticCurveGeom M) [AlgebraicGeometry.IsAffine B] [AlgebraicGeometry.IsAffine M] : AlgebraicGeometry.IsAffine (prodCurve B C).base

The base of prodCurve B C is affine when B and M are.

noncomputable def TauCeti.AlgebraicGeometry.EllObj.homProdCurveEquiv {B M : AlgebraicGeometry.Scheme} {C : EllipticCurveGeom M} (X : EllObj B) : (X ⟶ prodCurve B C) ≃ { fg : (X.base ⟶ M) × (X.curve.carrier ⟶ C.carrier) // CategoryTheory.IsPullback fg.2 X.curve.structureMap C.structureMap fg.1 ∧ CategoryTheory.CategoryStruct.comp X.curve.zero fg.2 = CategoryTheory.CategoryStruct.comp fg.1 C.zero }

Arrows into prodCurve B C. Arrows X ⟶ prodCurve B C of Ell/B correspond to the pairs of a morphism f : S ⟶ M and a morphism g from E to C carrying the zero section to the zero section and exhibiting E as the base change of C along f, for X = (E/S), by composing with the second projection and with prodCurveProj B C.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.homProdCurveEquiv_apply_fst {B M : AlgebraicGeometry.Scheme} {C : EllipticCurveGeom M} {X : EllObj B} (k : X ⟶ prodCurve B C) : (↑(X.homProdCurveEquiv k)).1 = CategoryTheory.CategoryStruct.comp k.base CategoryTheory.Limits.prod.snd

The morphism of bases attached to an arrow k : X ⟶ prodCurve B C is k.base followed by the second projection.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.homProdCurveEquiv_apply_snd {B M : AlgebraicGeometry.Scheme} {C : EllipticCurveGeom M} {X : EllObj B} (k : X ⟶ prodCurve B C) : (↑(X.homProdCurveEquiv k)).2 = CategoryTheory.CategoryStruct.comp k.total (prodCurveProj B C)

The morphism of curves attached to an arrow k : X ⟶ prodCurve B C is k.total followed by the projection to C.

noncomputable def TauCeti.AlgebraicGeometry.EllObj.prodCurvePoint (B : AlgebraicGeometry.Scheme) {M : AlgebraicGeometry.Scheme} {C : EllipticCurveGeom M} (R : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over M) ⟶ CategoryTheory.Over.mk C.structureMap) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (prodCurve B C).base) ⟶ CategoryTheory.Over.mk (prodCurve B C).curve.structureMap

The point of prodCurve B C given by the base change of a point R of C.

theorem TauCeti.AlgebraicGeometry.EllObj.prodCurvePoint_def {B M : AlgebraicGeometry.Scheme} {C : EllipticCurveGeom M} (R : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over M) ⟶ CategoryTheory.Over.mk C.structureMap) : prodCurvePoint B R = (EllipticCurveGeom.pointsPullback ⋯ ⋯) R

prodCurvePoint B R is the base change of R along the second projection.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.prodCurvePoint_left_prodCurveProj {B M : AlgebraicGeometry.Scheme} {C : EllipticCurveGeom M} (R : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over M) ⟶ CategoryTheory.Over.mk C.structureMap) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (prodCurvePoint B R)) (prodCurveProj B C) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.Over.Hom.left R)

The projection prodCurveProj B C carries the point prodCurvePoint B R to R.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllObj.prodCurvePoint_left_prodCurveProj_assoc {B M : AlgebraicGeometry.Scheme} {C : EllipticCurveGeom M} (R : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over M) ⟶ CategoryTheory.Over.mk C.structureMap) {Z : AlgebraicGeometry.Scheme} (h : C.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (prodCurvePoint B R)) (CategoryTheory.CategoryStruct.comp (prodCurveProj B C) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left R) h)

The projection prodCurveProj B C carries the point prodCurvePoint B R to R.

theorem TauCeti.AlgebraicGeometry.EllObj.pointsPullback_prodCurvePoint_eq_iff {B M : AlgebraicGeometry.Scheme} {C : EllipticCurveGeom M} {X : EllObj B} (k : X ⟶ prodCurve B C) (R : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over M) ⟶ CategoryTheory.Over.mk C.structureMap) (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over X.base) ⟶ CategoryTheory.Over.mk X.curve.structureMap) : (EllipticCurveGeom.pointsPullback ⋯ ⋯) (prodCurvePoint B R) = P ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left P) (↑(X.homProdCurveEquiv k)).2 = CategoryTheory.CategoryStruct.comp (↑(X.homProdCurveEquiv k)).1 (CategoryTheory.Over.Hom.left R)

Points pulled back along an arrow into prodCurve B C. For an arrow k : X ⟶ prodCurve B C, with corresponding pair (f, g) (homProdCurveEquiv), a point P of X is the pullback along k of the point prodCurvePoint B R exactly when g carries P to the pullback of R along f.