Module

SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat

5 declarations indexed from sourceView source ↗

Module documentation

Scheme Hom Over ext of forall algebraic Closure point of is Reduced of flat

Imports9

Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.AlgClosed.Basic
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.RingTheory.Localization.FractionRing
Mathlib.Topology.JacobsonSpace
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver

Imported by10

theorem

range_specMap_eq

L46 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat.RigKerGeomPoints.range_specMap_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
open Topology CategoryTheory.Limits
namespace RigKerGeomPoints
variable {R L : Type u} [CommRing R] [IsDomain R] [Field L] [IsAlgClosed L] [Algebra R L]
local notation "bL" => Spec.map (CommRingCat.ofHom (algebraMap R L))
omit [IsAlgClosed L] in

Lean source · statement

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

theorem

dense_preimage_genericPoint

L66 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat.RigKerGeomPoints.dense_preimage_genericPoint

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
open Topology CategoryTheory.Limits
namespace RigKerGeomPoints
variable {R L : Type u} [CommRing R] [IsDomain R] [Field L] [IsAlgClosed L] [Algebra R L]
local notation "bL" => Spec.map (CommRingCat.ofHom (algebraMap R L))
omit [IsAlgClosed L] [Algebra R L] in

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

L77 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat.RigKerGeomPoints.dense_range_of_points

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
open Topology CategoryTheory.Limits
namespace RigKerGeomPoints
variable {R L : Type u} [CommRing R] [IsDomain R] [Field L] [IsAlgClosed L] [Algebra R L]
local notation "bL" => Spec.map (CommRingCat.ofHom (algebraMap R L))

Lean source · statement

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

theorem

ext_of_forall_geometric_point

L118 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat.RigKerGeomPoints.ext_of_forall_geometric_point

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
open Topology CategoryTheory.Limits
namespace RigKerGeomPoints
variable {R L : Type u} [CommRing R] [IsDomain R] [Field L] [IsAlgClosed L] [Algebra R L]
local notation "bL" => Spec.map (CommRingCat.ofHom (algebraMap R L))

Lean source · statement

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

theorem

ext_of_forall_algebraicClosure_point_of_isReduced_of_flat

L143 ↗

AlgebraicGeometry.SchemeHomOver.ext_of_forall_algebraicClosure_point_of_isReduced_of_flat

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace SchemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
open Topology CategoryTheory.Limits

Lean source · statement

theorem
  _root_.AlgebraicGeometry.SchemeHomOver.ext_of_forall_algebraicClosure_point_of_isReduced_of_flat
    {R : Type u} [CommRing R] [IsDomain R] (K : Type u) [Field K] [Algebra R K] [IsFractionRing R K]
    (Kbar : Type u) [Field Kbar] [Algebra K Kbar] [IsAlgClosure K Kbar] [Algebra R Kbar]
      [IsScalarTower R K Kbar]
    {Y X : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of R)} {gX : X ⟶ Spec (CommRingCat.of R)}
    [Flat gY] [LocallyOfFiniteType gY] [IsReduced Y] [IsSeparated gX]
    (φ ψ : SchemeHomOver gY gX)
    (h : ∀ x : SchemeHomOver (Spec.map (CommRingCat.ofHom (algebraMap R Kbar))) gY, x.1 ≫ φ.1 = x.1
      ≫ ψ.1) :
    φ = ψ

Module documentation

Scheme Hom Over ext of forall algebraic Closure point of is Reduced of flat

Declarations

range_specMap_eq

dense_preimage_genericPoint

dense_range_of_points

ext_of_forall_geometric_point

ext_of_forall_algebraicClosure_point_of_isReduced_of_flat