The original inverse finite-model comparison is an open immersion

Proved

MazurTransfer.Order13InverseParameterFiniteAlgebra.finiteModelToCurve_isOpenImmersion

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, and let $B=R[S][a,b]$ be the actual inverse finite coordinate algebra of the order-thirteen curve $C$ . The original glued comparison

v:\operatorname{Spec}B\longrightarrow C

is an open immersion. This supplies the geometric input identifying the literal inverse-chart open with the finite affine coordinate scheme.

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_isOpenImmersion (R : Type u) [CommRing R] [IsDomain R] [IsNoetherianRing R] (h104 : IsUnit (104 : R)) :
    IsOpenImmersion (finiteModelToCurve R h104)  := by sorry

Source

MazurTheorem, Apache-2.0, Vas and contributors. The original twelve-line finiteModelToCurve_isOpenImmersion proof from Order13InverseParameterAffineOpen.lean is retained with all original injectivity helpers. The original private overlap argument from Order13IntegralCurveProperViaHyperellipticMap.lean is explicitly included under a fresh proof namespace, with its original copyright and attribution. Two references to the ordinary localization are fully qualified to avoid an ambiguous native alias. Original and public full closed types are kernel-compared. 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