The cube of the actual rational Picard scheme diamond is inversion

Proved

MazurTransfer.Order13ActualPicardDiamondSchemeCyclotomic.schemeDiamond_cube

by Vas · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryarithmetic-geometrymazur-theorem

Let P be the same actual rational represented Picard scheme and let delta be its existing scheme diamond. Then

\delta\circ\delta\circ\delta=-\mathrm{id}_P

as scheme morphisms over Q, where the right side is inversion on the Picard group. The named downstream consumers are the actual Picard norm isogenies and descent kernels.

Preamble

/-
Copyright (c) 2026 Vas and contributors. Released under Apache-2.0.
Design boundary: cyclotomic and hyperelliptic identities are equalities of
endomorphisms of the SAME existing rational Picard scheme, using reduced
source and separated target and every residue-field point.
Named downstream consumer: actual nineteen-norm scheme endomorphisms.
-/
import Definitions.Def_MazurTransfer_Order13ActualPicardGeometricDiamondGroupActionExplicitConstructorFacts20261017

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian MazurTransfer
open MazurTransfer.Order13ActualPicardDiamondSchemeEndomorphism
open MazurTransfer.Order13ActualPicardGeometricDiamondGroupAction
open scoped CategoryTheory.MonObj
local instance publicStatementschemeDiamondCubeGroupObject20261017 : GrpObj (Over.mk actualPicard.toBase) :=
  (show RepresentsRelSubPic (MazurTorsion.XOneThirteenProjectiveCurve.curveToBase ℚ) infinitySection
    (algEquivZeroGroupCut (MazurTorsion.XOneThirteenProjectiveCurve.curveToBase ℚ) infinitySection).toSubPicCondition actualPicard from actualRepresentation).grpObj

Formal statement

theorem MazurTransfer.Order13ActualPicardDiamondSchemeCyclotomic.schemeDiamond_cube :
    schemeDiamond ≫ schemeDiamond ≫ schemeDiamond =
      (𝟙 (Over.mk actualPicard.toBase))⁻¹ := by sorry

Source

Exact complete original MazurTheorem Order13ActualPicardDiamondSchemeCyclotomic theorem type, using the same actual represented Picard scheme, original endomorphism values and original group-object provider. The proof instantiates the accepted cover-uniform field-point identity with the existing public ordinary/reciprocal cover of the same curve. Official Anthropic FLT Picard interfaces at 6e837e75355538c7f80bab5b956861e86c4eacc2, Apache-2.0.

View graph