An integral affine chart recovers the actual generic-stalk morphism

Proved

MazurTransfer.AffineOpenChartGenericEmbeddingCompatibility.coordinateEmbedding_generic

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

algebraic-geometryarithmetic-geometrymazur-theorem

For an integral affine open chart j:Spec A -> C of an integral scheme, Spec of its original canonical coordinate embedding into C.functionField, followed by j, equals the actual morphism from the generic stalk of C. Every original universe, domain/integrality hypothesis and open-immersion hypothesis is retained.

Preamble

/-
Copyright (c) 2026 Vas and contributors. Released under Apache-2.0.
Design boundary: the explicit coordinate embedding of an integral affine
open chart recovers the scheme's literal generic-stalk morphism.
Named downstream consumer: compatibility of the order-13 generic embedding
with extension of the base field.
-/
import Definitions.Def_MazurTransfer_AffineOpenChartFunctionField

noncomputable section
universe u
open MazurTransfer
open AlgebraicGeometry CategoryTheory
open AffineOpenChartFunctionField
variable (A : CommRingCat.{u}) [IsDomain A] {C : Scheme.{u}} [IsIntegral C]
    (j : Spec A ⟶ C) [IsOpenImmersion j]

Formal statement

theorem MazurTransfer.AffineOpenChartGenericEmbeddingCompatibility.coordinateEmbedding_generic :
    Spec.map (CommRingCat.ofHom (coordinateEmbedding A j)) ≫ j =
      C.fromSpecStalk (genericPoint C) := by sorry

Source

Complete original MazurTheorem AffineOpenChartGenericEmbeddingCompatibility.coordinateEmbedding_generic proof and private fromSpecStalk_cast helper, Apache-2.0, Vas and contributors.

View graph