Module

schemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced.lean

Nyll.JacobianVarieties.Picard.schemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced

7 declarations indexed from sourceView source ↗

Module documentation

Rigidity from algebraic-closure-valued points

Geometric points of the generic fibre are dense in a flat scheme of finite type. For a reduced separated scheme this density detects equality of endomorphisms, including over a localization of the rational integers.

Imports25

Mathlib.Util.WithWeakNamespace
Mathlib.Algebra.Algebra.Tower
Mathlib.AlgebraicGeometry.AlgClosed.Basic
Mathlib.AlgebraicGeometry.Geometrically.Connected
Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.Scheme
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.RingTheory.Ideal.Prime
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.Topology.JacobsonSpace
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.RationalLocalization
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.JacobianVarieties.Picard.Designation
Nyll.JacobianVarieties.Picard.Representation
Nyll.AlgebraicCurves.Geometry.Picard.AlgEquivZeroCut

Imported by2

theorem

range_specMap_eq

L65 ↗

JacobianVarieties.Picard.Proofs.GeometricRigidity.RigidityGeomPoints.range_specMap_eq

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.GeometricRigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
namespace RigidityGeomPoints
universe u
variable {R K : Type u} [CommRing R] [IsDomain R] [Field K] [IsAlgClosed K] [Algebra R K]
local notation "bK" => Spec.map (CommRingCat.ofHom (algebraMap R K))
omit [IsAlgClosed K] in

Lean source · statement

theorem range_specMap_eq (hinj : Function.Injective (algebraMap R K)) :
    Set.range (bK).base = {(⟨⊥, Ideal.isPrime_bot⟩ : PrimeSpectrum R)}

theorem

dense_preimage_genericPoint

L85 ↗

JacobianVarieties.Picard.Proofs.GeometricRigidity.RigidityGeomPoints.dense_preimage_genericPoint

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.GeometricRigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
namespace RigidityGeomPoints
universe u
variable {R K : Type u} [CommRing R] [IsDomain R] [Field K] [IsAlgClosed K] [Algebra R K]
local notation "bK" => Spec.map (CommRingCat.ofHom (algebraMap R K))

Lean source · statement

theorem dense_preimage_genericPoint {D : Scheme.{u}} (t : D ⟶ Spec (CommRingCat.of R)) [Flat t] :
    Dense (t.base ⁻¹' {(⟨⊥, Ideal.isPrime_bot⟩ : PrimeSpectrum R)})

theorem

dense_range_of_points

L98 ↗

JacobianVarieties.Picard.Proofs.GeometricRigidity.RigidityGeomPoints.dense_range_of_points

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.GeometricRigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
namespace RigidityGeomPoints
universe u
variable {R K : Type u} [CommRing R] [IsDomain R] [Field K] [IsAlgClosed K] [Algebra R K]
local notation "bK" => Spec.map (CommRingCat.ofHom (algebraMap R K))

Lean source · statement

theorem dense_range_of_points (hinj : Function.Injective (algebraMap R K))
    {D : Scheme.{u}} (t : D ⟶ Spec (CommRingCat.of R)) [Flat t] [LocallyOfFiniteType t] :
    Dense (⋃ x : {x : Spec (CommRingCat.of K) ⟶ D // x ≫ t = bK},
      Set.range x.1.base)

theorem

ext_of_forall_geometric_point

L145 ↗

JacobianVarieties.Picard.Proofs.GeometricRigidity.RigidityGeomPoints.ext_of_forall_geometric_point

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.GeometricRigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
namespace RigidityGeomPoints
universe u
variable {R K : Type u} [CommRing R] [IsDomain R] [Field K] [IsAlgClosed K] [Algebra R K]
local notation "bK" => Spec.map (CommRingCat.ofHom (algebraMap R K))

Lean source · statement

theorem ext_of_forall_geometric_point (hinj : Function.Injective (algebraMap R K))
    {D : Scheme.{u}} (t : D ⟶ Spec (CommRingCat.of R))
    [Flat t] [LocallyOfFiniteType t] [IsSeparated t] [IsReduced D]
    (φ ψ : D ⟶ D) (hφ : φ ≫ t = t) (hψ : ψ ≫ t = t)
    (h : ∀ x : Spec (CommRingCat.of K) ⟶ D, x ≫ t = bK → x ≫ φ = x ≫ ψ) : φ = ψ

theorem

algebraMap_ratLocalizedAt_injective

L174 ↗

JacobianVarieties.Picard.Proofs.GeometricRigidity.RigidityGeomPoints.algebraMap_ratLocalizedAt_injective

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.GeometricRigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
section RIGAssembly
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian

Lean source · statement

theorem RigidityGeomPoints.algebraMap_ratLocalizedAt_injective (ℓ : ℕ) :
    Function.Injective (algebraMap ↥(Rat.LocalizationAt ℓ) (AlgebraicClosure ℚ))

theorem

rig

L179 ↗

JacobianVarieties.Picard.Proofs.GeometricRigidity.RigidityGeomPoints.rig

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.GeometricRigidity
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Topology
section RIGAssembly
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfra GoodReductionJacobian

Lean source · statement

theorem RigidityGeomPoints.rig
    (ℓ : ℕ) [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) [IsReduced D.P]
    (φ ψ : SchemeHomOver D.toBase D.toBase)
    (h : ∀ x : SchemeHomOver (Spec.map (CommRingCat.ofHom
        (algebraMap ↥(Rat.LocalizationAt ℓ) (AlgebraicClosure ℚ)))) D.toBase,
      x.1 ≫ φ.1 = x.1 ≫ ψ.1) :
    φ = ψ

theorem