Documentation

MazurTorsion.ModularCurve.XZeroGeometricCyclicQuotient

Supplied geometric cyclic quotients for X₀(N) data #

This file specializes the ambient fppf quotient certificate to the actual finite-flat cyclic subgroup constructed from a rational Γ₀(N) datum. It does not construct the quotient elliptic curve. Every declaration below takes a geometric quotient presentation as an explicit argument, so the missing representability theorem remains visible.

The substantive comparison is with the repository's existing represented-point quotient. The pointwise subgroup used by the geometric presentation is exactly the rational-point image of the finite-flat subgroup already attached to the datum. Consequently the generic injection into quotient-scheme points and its H¹ boundary exactness apply to that same subgroup, without identifying quotient-scheme rational points with a point-group quotient.

source
@[reducible, inline]
abbrev MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.RationalDatumGeometricQuotientPresentation {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) :
Type (u + 1)

The type of a supplied geometric quotient presentation for the actual finite-flat subgroup attached to x. This abbreviation provides no constructor and asserts no existence theorem.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumGeometricPointKernelRange_toAddSubgroup {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (Q : RationalDatumGeometricQuotientPresentation x M) :
    Subgroup.toAddSubgroup (AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointKernelRange Q (AlgebraicGeometry.AffineCommGroupScheme.testObject K)) = finiteFlatSubgroupPointRange x M

    The subgroup of represented rational points used by a supplied geometric quotient is exactly the subgroup already used by the checked point-quotient construction.

    source
    noncomputable def MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumGeometricPointBoundaryHom {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (Q : RationalDatumGeometricQuotientPresentation x M) :
    Q.quotient.Point (AlgebraicGeometry.AffineCommGroupScheme.testObject K) →* (splitGammaZeroDatumOfRationalDatum x M).subgroup.carrier.obj.FppfHOne

    The fppf boundary homomorphism on the affine self-test object used by the represented rational-point quotient. It is the base-section boundary transported across the canonical isomorphism with the identity object of the slice.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumGeometricPointQuotientMap_injective {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (Q : RationalDatumGeometricQuotientPresentation x M) :
      Function.Injective ⇑(AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointQuotientMap Q (AlgebraicGeometry.AffineCommGroupScheme.testObject K))

      The quotient of represented rational points by the actual finite-flat cyclic subgroup embeds in the rational points of every supplied geometric quotient scheme.

      source
      theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumGeometricPointQuotient_boundary_exact {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (Q : RationalDatumGeometricQuotientPresentation x M) :
      Function.MulExact ⇑(AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.pointQuotientMap Q (AlgebraicGeometry.AffineCommGroupScheme.testObject K)) ⇑(rationalDatumGeometricPointBoundaryHom x M Q)

      For the actual cyclic subgroup attached to x, the image of the point quotient is precisely the zero fibre of the fppf connecting map. This is the retained H¹ obstruction to rational surjectivity.

      source
      theorem MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassGroupSchemeInterface.rationalDatumGeometricQuotient_baseChange_kernel_inclusion {K : Type u} [Field K] [DecidableEq K] {N : ℕ} [NeZero N] (x : XZeroModuli.RationalDatum K N) (M : WeierstrassGroupSchemeInterface x.curve) (Q : RationalDatumGeometricQuotientPresentation x M) (L : Type u) [Field L] [Algebra K L] :
      (AlgebraicGeometry.CommGroupScheme.FppfQuotientPresentation.baseChange Q (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap K L)))).kernelPresentation.inclusion = (splitGammaZeroDatumOfRationalDatum x M).subgroup.baseChange.inclusion

      Under extension of the base field, the geometric quotient presentation still has exactly the base-changed finite-flat cyclic subgroup as its chosen kernel inclusion.