NYLL
Module

schemeHomOver_ext_of_forall_algebraicClosure_point.lean

Nyll.JacobianVarieties.Picard.schemeHomOver_ext_of_forall_algebraicClosure_point
1 declaration indexed from sourceView source ↗

Module documentation

Geometric-point extensionality over a localized integer ring

Smoothness makes the representing scheme reduced, so the reduced geometric-point extensionality theorem identifies morphisms agreeing on algebraic-closure-valued points.

Imports15
Imported by1

Declarations

theorem

schemeHomOver_ext_of_forall_algebraicClosure_point

L44 ↗
AlgebraicGeometry.RelPicard.schemeHomOver_ext_of_forall_algebraicClosure_point
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SmoothPointRigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.RelPicard NeronModelInfra GoodReductionJacobian
Lean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.schemeHomOver_ext_of_forall_algebraicClosure_point
    (ℓ : ℕ) [Fact ℓ.Prime]
    {X : Scheme.{0}} (c : X ⟶ Spec (CommRingCat.of ↥(Rat.LocalizationAt ℓ)))
    (D : RelativePic0Designation ↥(Rat.LocalizationAt ℓ) c)
    (hsm : Smooth D.toBase) (hpr : IsProper D.toBase)
    (φ ψ : SchemeHomOver D.toBase D.toBase)
    (h : ∀ x : SchemeHomOver (Spec.map (CommRingCat.ofHom
        (algebraMap ↥(Rat.LocalizationAt ℓ) (AlgebraicClosure ℚ)))) D.toBase,
      x.1 ≫ φ.1 = x.1 ≫ ψ.1) :
    φ = ψ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.