Torsion of commutative group schemes, transitions, and the coprime splitting

Let G be a commutative group scheme over a scheme S, that is, a commutative group object of Over S, and let n be an integer. The n-torsion G[n] is the scheme-theoretic kernel of multiplication by n, the integer n of the endomorphism ring End_S(G). Its points with values in any Z over S are the points of G killed by n.

Multiplication by m restricts to a homomorphism G[mn] ⟶ G[n], and G[m] includes into G[mn]. The transitions satisfy identity and composition laws, with transports between equal indices. These laws supply the coherence of towers of prime-power torsion. The transition is a base change of multiplication by m, and its scheme-theoretic kernel is the included G[m].

If G is killed by m * n, with m and n coprime, then addition G[m] ×_S G[n] ⟶ G is an isomorphism of group schemes over S. If a * m + b * n = 1, the projection of G to G[m] is multiplication by b * n, and the projection to G[n] is multiplication by a * m. By Deligne's theorem this applies to every finite locally free commutative group scheme over S of constant rank m * n. Katz and Mazur use this splitting to reduce statements about level structures, such as the generators of a finite locally free group scheme, to the prime-power case.

The argument is the splitting of an object of a preadditive category killed by a product of coprime integers (CategoryTheory.Limits.BinaryBicone.isBilimitOfCoprimeKernelForks), applied in the preadditive category CommGrp (Over S).

The definition of G[n] and its points API generalize the n-torsion of an elliptic curve in TauCeti/AlgebraicGeometry/EllipticCurve/Scheme/Geom/Torsion.lean (TauCeti.AlgebraicGeometry.EllipticCurveGeom.torsion, identified with a kernel by TauCeti.AlgebraicGeometry.EllipticCurveGeom.torsion_eq_kernel, together with its torsionι, torsionLift, torsionPointsMulEquiv, and torsionMap) from elliptic curves to arbitrary commutative group schemes.

Main definitions

• TauCeti.GroupScheme.torsion G n: the n-torsion G[n], a group object of Over S.
• TauCeti.GroupScheme.torsionι G n: its inclusion G[n] ⟶ G.
• TauCeti.GroupScheme.torsionLift: the point of G[n] given by a point of G killed by n.
• TauCeti.GroupScheme.torsionMap: the homomorphism G[n] ⟶ H[n] induced by a homomorphism G ⟶ H.
• TauCeti.GroupScheme.torsionPointsMulEquiv: the points of G[n] with values in Z, as a group, are the n-torsion of the points of G with values in Z.
• TauCeti.GroupScheme.torsionBaseChangeIso: formation of G[n] commutes with base change.
• TauCeti.GroupScheme.torsionMulBy: multiplication G[mn] ⟶ G[n] between torsion levels.
• TauCeti.GroupScheme.torsionInclusion: the inclusion G[m] ⟶ G[mn].
• TauCeti.GroupScheme.torsionTensorIso: for G killed by m * n with m and n coprime, the isomorphism G[m] ×_S G[n] ≅ G of group schemes given by addition.

Main results

• TauCeti.GroupScheme.exists_comp_torsionι_iff: the points of G[n] are the points of G killed by n.
• TauCeti.GroupScheme.torsion_zpow_eq_one: G[n] is killed by n.
• TauCeti.GroupScheme.isPullback_torsionι: G[n] is the fibre of multiplication by n over the unit section.
• TauCeti.GroupScheme.torsionBaseChangeIso_hom_hom_hom_comp_torsionMap: the base-change comparison for the n-torsion is natural in G.
• TauCeti.GroupScheme.isIso_tensorHom_torsionι_comp_mul: for G killed by m * n with m and n coprime, addition G[m] ×_S G[n] ⟶ G is an isomorphism.
• TauCeti.GroupScheme.torsionTensorIso_inv_hom_hom_fst_torsionι and TauCeti.GroupScheme.torsionTensorIso_inv_hom_hom_snd_torsionι: its inverse is given by multiplication by b * n and by a * m, for every Bézout identity a * m + b * n = 1.
• TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.isIso_tensorHom_torsionι_comp_mul: a finite locally free commutative group scheme of constant rank m * n, with m and n coprime, is the product of its m-torsion and its n-torsion.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, 1.10.14–1.10.15, 2.3.1 and Chapter 5.

The n-torsion of a commutative group scheme

noncomputable def TauCeti.GroupScheme.torsion {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : CategoryTheory.Grp (CategoryTheory.Over S)

The n-torsion G[n] of a commutative group scheme G over S: the scheme-theoretic kernel of multiplication by n, the integer n of the endomorphism ring of G, as a group object of Over S.

theorem TauCeti.GroupScheme.torsion_eq_kernel {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : torsion G n = CategoryTheory.Limits.kernel ((CategoryTheory.CommGrp.forget₂Grp (CategoryTheory.Over S)).map (↑n).asHom)

The torsion group scheme is the kernel of multiplication by its index.

noncomputable def TauCeti.GroupScheme.torsionι {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : (torsion G n).X ⟶ G.X

The inclusion G[n] ⟶ G of the n-torsion of G, a morphism of Over S.

instance TauCeti.GroupScheme.isMonHom_torsionι {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : CategoryTheory.IsMonHom (torsionι G n)

The inclusion of the n-torsion is a homomorphism of group schemes over S.

instance TauCeti.GroupScheme.mono_torsionι {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : CategoryTheory.Mono (torsionι G n)

The inclusion of the n-torsion is a monomorphism.

instance TauCeti.GroupScheme.isCommMonObj_torsion {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : CategoryTheory.IsCommMonObj (torsion G n).X

The n-torsion is commutative. Its group law is the restriction of that of G.

theorem TauCeti.GroupScheme.torsionι_comp_zpow {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : CategoryTheory.CategoryStruct.comp (torsionι G n) (CategoryTheory.CategoryStruct.id G.X ^ n) = 1

The inclusion of the n-torsion, followed by multiplication by n, is the unit point.

theorem TauCeti.GroupScheme.torsionι_comp_zpow_assoc {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) {Z : CategoryTheory.Over S} (h : G.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionι G n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id G.X ^ n) h) = CategoryTheory.CategoryStruct.comp 1 h

The inclusion of the n-torsion, followed by multiplication by n, is the unit point.

@[simp]

theorem TauCeti.GroupScheme.torsionι_zpow {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : torsionι G n ^ n = 1

The inclusion of the n-torsion, as a point of G with values in G[n], is killed by n.

theorem TauCeti.GroupScheme.isPullback_torsionι {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : CategoryTheory.IsPullback (torsionι G n) (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (torsion G n).X) (CategoryTheory.CategoryStruct.id G.X ^ n) CategoryTheory.MonObj.one

The n-torsion is the fibre of multiplication by n over the unit section.

theorem TauCeti.GroupScheme.torsion_hom_ext {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) {n : ℤ} {Z : CategoryTheory.Over S} {y y' : Z ⟶ (torsion G n).X} (h : CategoryTheory.CategoryStruct.comp y (torsionι G n) = CategoryTheory.CategoryStruct.comp y' (torsionι G n)) : y = y'

Two points of the n-torsion agree if their images in G do.

noncomputable def TauCeti.GroupScheme.torsionLift {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {n : ℤ} {Z : CategoryTheory.Over S} (x : Z ⟶ G.X) (hx : x ^ n = 1) : Z ⟶ (torsion G n).X

The point of the n-torsion of G given by a point x of G killed by n.

@[simp]

theorem TauCeti.GroupScheme.torsionLift_ι {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {n : ℤ} {Z : CategoryTheory.Over S} (x : Z ⟶ G.X) (hx : x ^ n = 1) : CategoryTheory.CategoryStruct.comp (torsionLift x hx) (torsionι G n) = x

The point torsionLift x hx of the n-torsion maps to x in G.

@[simp]

theorem TauCeti.GroupScheme.torsionLift_ι_assoc {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {n : ℤ} {Z : CategoryTheory.Over S} (x : Z ⟶ G.X) (hx : x ^ n = 1) {Z✝ : CategoryTheory.Over S} (h : G.X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (torsionLift x hx) (CategoryTheory.CategoryStruct.comp (torsionι G n) h) = CategoryTheory.CategoryStruct.comp x h

The point torsionLift x hx of the n-torsion maps to x in G.

theorem TauCeti.GroupScheme.exists_comp_torsionι_iff {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {n : ℤ} {Z : CategoryTheory.Over S} (x : Z ⟶ G.X) : (∃ (y : Z ⟶ (torsion G n).X), CategoryTheory.CategoryStruct.comp y (torsionι G n) = x) ↔ x ^ n = 1

The points of the n-torsion. A point of G factors through G[n] if and only if it is killed by n.

@[simp]

theorem TauCeti.GroupScheme.torsion_zpow_eq_one {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {n : ℤ} {Z : CategoryTheory.Over S} (y : Z ⟶ (torsion G n).X) : y ^ n = 1

The n-torsion is killed by n. Every point of G[n] is killed by n in the group of points of G[n].

instance TauCeti.GroupScheme.isMonHom_torsionLift {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {n : ℤ} {Z : CategoryTheory.Over S} [CategoryTheory.MonObj Z] (x : Z ⟶ G.X) [CategoryTheory.IsMonHom x] (hx : x ^ n = 1) : CategoryTheory.IsMonHom (torsionLift x hx)

A homomorphism into G killed by n factors through the n-torsion as a homomorphism.

Transitions between torsion levels

noncomputable def TauCeti.GroupScheme.torsionMulBy {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : (torsion G (m * n)).X ⟶ (torsion G n).X

Multiplication by m restricted to G[mn], with values in G[n].

@[simp]

theorem TauCeti.GroupScheme.torsionMulBy_torsionι {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : CategoryTheory.CategoryStruct.comp (torsionMulBy G m n) (torsionι G n) = torsionι G (m * n) ^ m

The transition G[mn] ⟶ G[n] sends a torsion point to its multiple by m.

@[simp]

theorem TauCeti.GroupScheme.torsionMulBy_torsionι_assoc {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) {Z : CategoryTheory.Over S} (h : G.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionMulBy G m n) (CategoryTheory.CategoryStruct.comp (torsionι G n) h) = CategoryTheory.CategoryStruct.comp (torsionι G (m * n) ^ m) h

The transition G[mn] ⟶ G[n] sends a torsion point to its multiple by m.

instance TauCeti.GroupScheme.isMonHom_torsionMulBy {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : CategoryTheory.IsMonHom (torsionMulBy G m n)

The torsion transition is a homomorphism of group schemes.

noncomputable def TauCeti.GroupScheme.torsionInclusion {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : (torsion G m).X ⟶ (torsion G (m * n)).X

The inclusion of G[m] in G[mn].

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_torsionι {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : CategoryTheory.CategoryStruct.comp (torsionInclusion G m n) (torsionι G (m * n)) = torsionι G m

The inclusion between torsion levels preserves the underlying point of G.

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_torsionι_assoc {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) {Z : CategoryTheory.Over S} (h : G.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionInclusion G m n) (CategoryTheory.CategoryStruct.comp (torsionι G (m * n)) h) = CategoryTheory.CategoryStruct.comp (torsionι G m) h

The inclusion between torsion levels preserves the underlying point of G.

instance TauCeti.GroupScheme.mono_torsionInclusion {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : CategoryTheory.Mono (torsionInclusion G m n)

The inclusion between torsion levels is a monomorphism.

instance TauCeti.GroupScheme.isMonHom_torsionInclusion {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : CategoryTheory.IsMonHom (torsionInclusion G m n)

The inclusion between torsion levels is a homomorphism of group schemes.

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_torsionMulBy {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : CategoryTheory.CategoryStruct.comp (torsionInclusion G m n) (torsionMulBy G m n) = 1

The transition kills the included m-torsion.

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_torsionMulBy_assoc {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) {Z : CategoryTheory.Over S} (h : (torsion G n).X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionInclusion G m n) (CategoryTheory.CategoryStruct.comp (torsionMulBy G m n) h) = CategoryTheory.CategoryStruct.comp 1 h

The transition kills the included m-torsion.

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_zpow {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : torsionInclusion G m n ^ m = 1

The inclusion G[m] ⟶ G[mn] is killed by m, as a point of G[mn].

theorem TauCeti.GroupScheme.isPullback_torsionMulBy {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : CategoryTheory.IsPullback (torsionι G (m * n)) (torsionMulBy G m n) (CategoryTheory.CategoryStruct.id G.X ^ m) (torsionι G n)

The torsion transition is the base change of multiplication by m on G.

theorem TauCeti.GroupScheme.isPullback_torsionInclusion {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n : ℤ) : CategoryTheory.IsPullback (torsionInclusion G m n) (CategoryTheory.SemiCartesianMonoidalCategory.toUnit (torsion G m).X) (torsionMulBy G m n) CategoryTheory.MonObj.one

The scheme-theoretic kernel of G[mn] ⟶ G[n] is the included G[m].

@[simp]

theorem TauCeti.GroupScheme.eqToHom_torsionι {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) {a b : ℤ} (h : a = b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (torsionι G b) = torsionι G a

Transport between equal torsion indices preserves the underlying point of G.

@[simp]

theorem TauCeti.GroupScheme.eqToHom_torsionι_assoc {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) {a b : ℤ} (h : a = b) {Z : CategoryTheory.Over S} (h✝ : G.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (torsionι G b) h✝) = CategoryTheory.CategoryStruct.comp (torsionι G a) h✝

Transport between equal torsion indices preserves the underlying point of G.

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_one {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m : ℤ) : torsionInclusion G m 1 = CategoryTheory.eqToHom ⋯

Inclusion into the same torsion level is the identity, after identifying m * 1 with m.

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_comp {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n l : ℤ) : CategoryTheory.CategoryStruct.comp (torsionInclusion G m n) (torsionInclusion G (m * n) l) = CategoryTheory.CategoryStruct.comp (torsionInclusion G m (n * l)) (CategoryTheory.eqToHom ⋯)

Successive torsion inclusions multiply their indices, with the associativity transport.

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_comp_assoc {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n l : ℤ) {Z : CategoryTheory.Over S} (h : (torsion G (m * n * l)).X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionInclusion G m n) (CategoryTheory.CategoryStruct.comp (torsionInclusion G (m * n) l) h) = CategoryTheory.CategoryStruct.comp (torsionInclusion G m (n * l)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

Successive torsion inclusions multiply their indices, with the associativity transport.

@[simp]

theorem TauCeti.GroupScheme.torsionMulBy_one {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : torsionMulBy G 1 n = CategoryTheory.eqToHom ⋯

Multiplication by one on torsion is the identity, after identifying 1 * n with n.

@[simp]

theorem TauCeti.GroupScheme.torsionMulBy_comp {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n l : ℤ) : CategoryTheory.CategoryStruct.comp (torsionMulBy G l (m * n)) (torsionMulBy G m n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (torsionMulBy G (l * m) n)

Successive torsion transitions multiply their indices, with the associativity transport.

@[simp]

theorem TauCeti.GroupScheme.torsionMulBy_comp_assoc {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (m n l : ℤ) {Z : CategoryTheory.Over S} (h : (torsion G n).X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionMulBy G l (m * n)) (CategoryTheory.CategoryStruct.comp (torsionMulBy G m n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (torsionMulBy G (l * m) n) h)

Successive torsion transitions multiply their indices, with the associativity transport.

noncomputable def TauCeti.GroupScheme.torsionPointsMulEquiv {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) (Z : CategoryTheory.Over S) : (Z ⟶ (torsion G n).X) ≃* ↥(zpowGroupHom n).ker

The points of the n-torsion. The points of G[n] with values in Z form the n-torsion subgroup of the commutative group of points of G with values in Z.

@[simp]

theorem TauCeti.GroupScheme.coe_torsionPointsMulEquiv_apply {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) (Z : CategoryTheory.Over S) (y : Z ⟶ (torsion G n).X) : ↑((torsionPointsMulEquiv G n Z) y) = CategoryTheory.CategoryStruct.comp y (torsionι G n)

A point of the n-torsion corresponds to its image in G.

@[simp]

theorem TauCeti.GroupScheme.torsionPointsMulEquiv_symm_apply_torsionι {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) (Z : CategoryTheory.Over S) (x : ↥(zpowGroupHom n).ker) : CategoryTheory.CategoryStruct.comp ((torsionPointsMulEquiv G n Z).symm x) (torsionι G n) = ↑x

The point of the n-torsion corresponding to a point x of G killed by n maps to x in G.

Functoriality of the n-torsion

noncomputable def TauCeti.GroupScheme.torsionMap {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) (n : ℤ) : (torsion G n).X ⟶ (torsion H n).X

The homomorphism G[n] ⟶ H[n] induced by a homomorphism f : G ⟶ H of commutative group schemes over S, the restriction of f to the n-torsion.

@[simp]

theorem TauCeti.GroupScheme.torsionMap_ι {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) (n : ℤ) : CategoryTheory.CategoryStruct.comp (torsionMap f n) (torsionι H n) = CategoryTheory.CategoryStruct.comp (torsionι G n) f.hom.hom.hom

The map induced on the n-torsion by f is the restriction of f.

@[simp]

theorem TauCeti.GroupScheme.torsionMap_ι_assoc {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) (n : ℤ) {Z : CategoryTheory.Over S} (h : H.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionMap f n) (CategoryTheory.CategoryStruct.comp (torsionι H n) h) = CategoryTheory.CategoryStruct.comp (torsionι G n) (CategoryTheory.CategoryStruct.comp f.hom.hom.hom h)

The map induced on the n-torsion by f is the restriction of f.

instance TauCeti.GroupScheme.isMonHom_torsionMap {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) (n : ℤ) : CategoryTheory.IsMonHom (torsionMap f n)

The map induced on the n-torsion is a homomorphism of group schemes over S.

@[simp]

theorem TauCeti.GroupScheme.torsionMulBy_comp_torsionMap {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) (m n : ℤ) : CategoryTheory.CategoryStruct.comp (torsionMulBy G m n) (torsionMap f n) = CategoryTheory.CategoryStruct.comp (torsionMap f (m * n)) (torsionMulBy H m n)

Torsion transitions commute with homomorphisms of commutative group schemes.

@[simp]

theorem TauCeti.GroupScheme.torsionMulBy_comp_torsionMap_assoc {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) (m n : ℤ) {Z : CategoryTheory.Over S} (h : (torsion H n).X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionMulBy G m n) (CategoryTheory.CategoryStruct.comp (torsionMap f n) h) = CategoryTheory.CategoryStruct.comp (torsionMap f (m * n)) (CategoryTheory.CategoryStruct.comp (torsionMulBy H m n) h)

Torsion transitions commute with homomorphisms of commutative group schemes.

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_comp_torsionMap {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) (m n : ℤ) : CategoryTheory.CategoryStruct.comp (torsionInclusion G m n) (torsionMap f (m * n)) = CategoryTheory.CategoryStruct.comp (torsionMap f m) (torsionInclusion H m n)

Inclusions between torsion levels commute with homomorphisms of commutative group schemes.

@[simp]

theorem TauCeti.GroupScheme.torsionInclusion_comp_torsionMap_assoc {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) (m n : ℤ) {Z : CategoryTheory.Over S} (h : (torsion H (m * n)).X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionInclusion G m n) (CategoryTheory.CategoryStruct.comp (torsionMap f (m * n)) h) = CategoryTheory.CategoryStruct.comp (torsionMap f m) (CategoryTheory.CategoryStruct.comp (torsionInclusion H m n) h)

Inclusions between torsion levels commute with homomorphisms of commutative group schemes.

@[simp]

theorem TauCeti.GroupScheme.torsionMap_id {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} (n : ℤ) : torsionMap (CategoryTheory.CategoryStruct.id G) n = CategoryTheory.CategoryStruct.id (torsion G n).X

The identity of G induces the identity of G[n].

@[simp]

theorem TauCeti.GroupScheme.torsionMap_comp {S : AlgebraicGeometry.Scheme} {G H K : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) (g : H ⟶ K) (n : ℤ) : torsionMap (CategoryTheory.CategoryStruct.comp f g) n = CategoryTheory.CategoryStruct.comp (torsionMap f n) (torsionMap g n)

The map induced on the n-torsion by a composite is the composite of the induced maps.

Base change of the n-torsion

noncomputable def TauCeti.GroupScheme.torsionBaseChangeIso {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) {T : AlgebraicGeometry.Scheme} (s : T ⟶ S) (n : ℤ) : (CategoryTheory.Over.pullback s).mapGrp.obj (torsion G n) ≅ torsion ((CategoryTheory.Over.pullback s).mapCommGrp.obj G) n

Formation of the n-torsion commutes with base change. The canonical isomorphism from the base change of G[n] along s : T ⟶ S to the n-torsion of the base change of G.

@[simp]

theorem TauCeti.GroupScheme.torsionBaseChangeIso_hom_hom_hom_torsionι {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) {T : AlgebraicGeometry.Scheme} (s : T ⟶ S) (n : ℤ) : CategoryTheory.CategoryStruct.comp (torsionBaseChangeIso G s n).hom.hom.hom (torsionι ((CategoryTheory.Over.pullback s).mapCommGrp.obj G) n) = (CategoryTheory.Over.pullback s).map (torsionι G n)

The base-change comparison for the n-torsion intertwines the two inclusions.

@[simp]

theorem TauCeti.GroupScheme.torsionBaseChangeIso_hom_hom_hom_torsionι_assoc {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) {T : AlgebraicGeometry.Scheme} (s : T ⟶ S) (n : ℤ) {Z : CategoryTheory.Over T} (h : ((CategoryTheory.Over.pullback s).mapCommGrp.obj G).X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionBaseChangeIso G s n).hom.hom.hom (CategoryTheory.CategoryStruct.comp (torsionι ((CategoryTheory.Over.pullback s).mapCommGrp.obj G) n) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback s).map (torsionι G n)) h

The base-change comparison for the n-torsion intertwines the two inclusions.

theorem TauCeti.GroupScheme.torsionBaseChangeIso_hom_hom_hom_comp_torsionMap {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) {T : AlgebraicGeometry.Scheme} (s : T ⟶ S) (n : ℤ) : CategoryTheory.CategoryStruct.comp (torsionBaseChangeIso G s n).hom.hom.hom (torsionMap ((CategoryTheory.Over.pullback s).mapCommGrp.map f) n) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback s).map (torsionMap f n)) (torsionBaseChangeIso H s n).hom.hom.hom

The base-change comparison for the n-torsion is natural: it intertwines the base change of the map induced on the n-torsion by f with the map induced by the base change of f.

theorem TauCeti.GroupScheme.torsionBaseChangeIso_hom_hom_hom_comp_torsionMap_assoc {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.CommGrp (CategoryTheory.Over S)} (f : G ⟶ H) {T : AlgebraicGeometry.Scheme} (s : T ⟶ S) (n : ℤ) {Z : CategoryTheory.Over T} (h : (torsion ((CategoryTheory.Over.pullback s).mapCommGrp.obj H) n).X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionBaseChangeIso G s n).hom.hom.hom (CategoryTheory.CategoryStruct.comp (torsionMap ((CategoryTheory.Over.pullback s).mapCommGrp.map f) n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback s).map (torsionMap f n)) (torsionBaseChangeIso H s n).hom.hom.hom) h

The base-change comparison for the n-torsion is natural: it intertwines the base change of the map induced on the n-torsion by f with the map induced by the base change of f.

The n-torsion as a kernel in CommGrp (Over S)

@[reducible, inline]

noncomputable abbrev TauCeti.GroupScheme.torsionCommGrp {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.CommGrp (CategoryTheory.Over S)) (n : ℤ) : CategoryTheory.CommGrp (CategoryTheory.Over S)

The n-torsion of G, as a commutative group object of Over S.

The coprime splitting

theorem TauCeti.GroupScheme.isIso_tensorHom_torsionι_comp_mul {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {m n : ℤ} (h : IsCoprime m n) (hG : CategoryTheory.CategoryStruct.id G.X ^ (m * n) = 1) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (torsionι G m) (torsionι G n)) CategoryTheory.MonObj.mul)

A commutative group scheme killed by m * n, with m and n coprime, is the product of its m-torsion and its n-torsion. Addition G[m] ×_S G[n] ⟶ G is an isomorphism.

noncomputable def TauCeti.GroupScheme.torsionTensorIso {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {m n : ℤ} (h : IsCoprime m n) (hG : CategoryTheory.CategoryStruct.id G.X ^ (m * n) = 1) : CategoryTheory.MonoidalCategoryStruct.tensorObj (torsion G m) (torsion G n) ≅ (CategoryTheory.CommGrp.forget₂Grp (CategoryTheory.Over S)).obj G

The coprime splitting of a commutative group scheme. If G is killed by m * n, with m and n coprime, then addition is an isomorphism G[m] ×_S G[n] ≅ G of group schemes over S.

@[simp]

theorem TauCeti.GroupScheme.torsionTensorIso_hom_hom_hom {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {m n : ℤ} (h : IsCoprime m n) (hG : CategoryTheory.CategoryStruct.id G.X ^ (m * n) = 1) : (torsionTensorIso h hG).hom.hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (torsionι G m) (torsionι G n)) CategoryTheory.MonObj.mul

The isomorphism G[m] ×_S G[n] ≅ G is addition.

theorem TauCeti.GroupScheme.torsionTensorIso_inv_hom_hom_fst_torsionι {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {a b m n : ℤ} (hab : a * m + b * n = 1) (hG : CategoryTheory.CategoryStruct.id G.X ^ (m * n) = 1) : CategoryTheory.CategoryStruct.comp (torsionTensorIso ⋯ hG).inv.hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst (torsion G m).X (torsion G n).X) (torsionι G m)) = CategoryTheory.CategoryStruct.id G.X ^ (b * n)

If a * m + b * n = 1, the projection of G to G[m] under G ≅ G[m] ×_S G[n] is multiplication by b * n.

theorem TauCeti.GroupScheme.torsionTensorIso_inv_hom_hom_fst_torsionι_assoc {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {a b m n : ℤ} (hab : a * m + b * n = 1) (hG : CategoryTheory.CategoryStruct.id G.X ^ (m * n) = 1) {Z : CategoryTheory.Over S} (h : G.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionTensorIso ⋯ hG).inv.hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst (torsion G m).X (torsion G n).X) (CategoryTheory.CategoryStruct.comp (torsionι G m) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id G.X ^ (b * n)) h

If a * m + b * n = 1, the projection of G to G[m] under G ≅ G[m] ×_S G[n] is multiplication by b * n.

theorem TauCeti.GroupScheme.torsionTensorIso_inv_hom_hom_snd_torsionι {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {a b m n : ℤ} (hab : a * m + b * n = 1) (hG : CategoryTheory.CategoryStruct.id G.X ^ (m * n) = 1) : CategoryTheory.CategoryStruct.comp (torsionTensorIso ⋯ hG).inv.hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (torsion G m).X (torsion G n).X) (torsionι G n)) = CategoryTheory.CategoryStruct.id G.X ^ (a * m)

If a * m + b * n = 1, the projection of G to G[n] under G ≅ G[m] ×_S G[n] is multiplication by a * m.

theorem TauCeti.GroupScheme.torsionTensorIso_inv_hom_hom_snd_torsionι_assoc {S : AlgebraicGeometry.Scheme} {G : CategoryTheory.CommGrp (CategoryTheory.Over S)} {a b m n : ℤ} (hab : a * m + b * n = 1) (hG : CategoryTheory.CategoryStruct.id G.X ^ (m * n) = 1) {Z : CategoryTheory.Over S} (h : G.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (torsionTensorIso ⋯ hG).inv.hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (torsion G m).X (torsion G n).X) (CategoryTheory.CategoryStruct.comp (torsionι G n) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id G.X ^ (a * m)) h

If a * m + b * n = 1, the projection of G to G[n] under G ≅ G[m] ×_S G[n] is multiplication by a * m.

theorem TauCeti.AlgebraicGeometry.FiniteFlatCommGroupScheme.isIso_tensorHom_torsionι_comp_mul {S : AlgebraicGeometry.Scheme} (G : FiniteFlatCommGroupScheme S) {m n : ℕ} (h : m.Coprime n) (hG : ∀ (s : ↥S), AlgebraicGeometry.Scheme.Hom.finrank G.structureMap s = m * n) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (GroupScheme.torsionι { X := G.toOver, grp := G.grpObj, comm := ⋯ } ↑m) (GroupScheme.torsionι { X := G.toOver, grp := G.grpObj, comm := ⋯ } ↑n)) CategoryTheory.MonObj.mul)

A finite locally free commutative group scheme of rank m * n, with m and n coprime, is the product of its m-torsion and its n-torsion. Let G be a finite locally free commutative group scheme over S whose rank is m * n at every point of S. Then addition G[m] ×_S G[n] ⟶ G is an isomorphism.