The original inverse finite-model comparison has its specified two-chart image

Proved

MazurTransfer.Order13InverseParameterFiniteAlgebra.finiteModelToCurve_range

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

algebraic-geometrymazur-theoremscheme-morphisms

Let $R$ be a noetherian commutative integral domain with $104$ invertible. Let $v:\operatorname{Spec}B\to C$ be the original glued comparison from the actual inverse finite coordinate algebra to the order-thirteen curve. Its image is exactly the union of the specified ordinary-parameter and positive-reciprocal chart images:

\operatorname{im}(v)=\operatorname{im}(v_{\mathrm{ord}})\cup\operatorname{im}(v_{\mathrm{rec}}).

This identifies the underlying subset used by the actual inverse affine-chart presentation.

Preamble

import Mathlib
import Definitions.Def_MazurTransfer_Order13InverseFiniteModelToCurve
open CategoryTheory AlgebraicGeometry
open MazurTorsion.XOneThirteenProjectiveCurve
open MazurTransfer.Order13InverseParameterFiniteAlgebra
universe u

Formal statement

theorem MazurTransfer.Order13InverseParameterFiniteAlgebra.finiteModelToCurve_range (R : Type u) [CommRing R] [IsDomain R] [IsNoetherianRing R] (h104 : IsUnit (104 : R)) :
    Set.range (finiteModelToCurve R h104) =
      Set.range (ordinaryParameterCurveMap R) ∪ Set.range (positiveReciprocalCurveMap R)  := by sorry

Source

MazurTheorem, Apache-2.0, Vas and contributors. The seventeen-line original finiteModelToCurve_range proof from Order13InverseParameterGlobalComparison.lean is unchanged. Its project import is the public glued-morphism definition and original chart restriction identities. Native, strict and full frontend checks pass with standard axioms only. Named downstream consumer: original inverse affine-chart isomorphism and actual integral FiniteMapData.

View graph