Finite subgroups generated by disjoint torsion sections

A finite group embedded fibrewise into an elliptic curve by torsion sections defines a finite étale subgroup scheme when the torsion level is invertible. Its divisor is the union of its disjoint sections. These results hold over arbitrary, possibly nonreduced bases and supply the subgroup-divisor condition for naive points of exact order.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §1.4 and §3.7.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsFiberwiseInjective.etale_pointsDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Group A] [Fintype A] {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)} (hφ : E.IsFiberwiseInjective φ) {N : ℕ} (hN : ∀ (s : ↥S), ↑N ≠ 0) (hkill : ∀ (a : A), φ a ^ N = 1) : AlgebraicGeometry.Etale (CategoryTheory.CategoryStruct.comp (E.pointsDivisor ⇑φ).subschemeι E.structureMap)

The divisor of a fibrewise injective finite family of sections killed by an invertible level is étale over the base.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsFiberwiseInjective.exists_grpObj_isMonHom_pointsDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {A : Type u_1} [Group A] [Fintype A] {φ : A →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)} (hφ : E.IsFiberwiseInjective φ) {N : ℕ} (hN : ∀ (s : ↥S), ↑N ≠ 0) (hkill : ∀ (a : A), φ a ^ N = 1) : ∃ (x : CategoryTheory.GrpObj (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp (E.pointsDivisor ⇑φ).subschemeι E.structureMap))), CategoryTheory.IsMonHom (CategoryTheory.Over.homMk (E.pointsDivisor ⇑φ).subschemeι ⋯)

A fibrewise injective finite family of torsion sections cuts out a subgroup scheme. The torsion level is required to be invertible on the base.