Relative group-law multiplication by n equals the underlying internal power of the identity
ProvedMazurTransfer.RelativeGroupSchemeNsmulInternalPowerCompatibility.schemeNsmul_eq_internal_poweralgebraic-geometryarithmetic-geometrymazur-theorem
Let a scheme over a commutative ring carry an internal group object structure in the over category. The relative group-law multiplication-by-n scheme morphism is the underlying scheme morphism of the nth pointwise power of its identity morphism. This retains the original complete universes and arbitrary commutative base ring. The named downstream consumer is converting the actual Picard norm composites into multiplication by nineteen.
Preamble
/-
Copyright (c) 2026 Vas and contributors. Released under Apache-2.0.
Design boundary: integer multiplication in the relative group-law API is
exactly the underlying morphism of the internal pointwise power of the
identity. Named downstream consumer: formal unramifiedness of the actual
Picard norm factors via their checked scalar-nineteen composites.
-/
import Definitions.Def_GoodReductionJacobian_RelativeGroupLawKernel
import Definitions.Def_AlgebraicGeometry_RelativeGroupLawGrpObj
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
variable {R : Type u} [CommRing R] {A : Scheme.{u}}
(f : A ⟶ Spec (CommRingCat.of R)) [GrpObj (Over.mk f)]
Formal statement
theorem MazurTransfer.RelativeGroupSchemeNsmulInternalPowerCompatibility.schemeNsmul_eq_internal_power (n : ℕ) :
(relativeGroupLawOfGrpObj R f).schemeNsmul n = ((𝟙 (Over.mk f)) ^ n).left := by sorrySource
Complete original MazurTheorem RelativeGroupSchemeNsmulInternalPowerCompatibility.schemeNsmul_eq_internal_power and its original pointwise power helper, using the official Anthropic FLT relative group-law interfaces at 6e837e75355538c7f80bab5b956861e86c4eacc2, Apache-2.0.