NYLL
Module

existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.lean

Nyll.AlgebraicCurves.Geometry.Schemes.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
17 declarations indexed from sourceView source ↗

Module documentation

exists Unique extension to affine of is Integrally Closed stalk

Imports13
Imported by3

Declarations

def

pointOfPrime

L54 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.pointOfPrime
Documentation

The point of an affine scheme corresponding to a prime of its global sections.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Affine
variable {X : Scheme.{u}} [IsAffine X]
Lean source · statement
def pointOfPrime (p : PrimeSpectrum Γ(X, ⊤)) : (⊤ : X.Opens)
theorem

primeIdealOf_pointOfPrime

L57 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.primeIdealOf_pointOfPrime
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Affine
variable {X : Scheme.{u}} [IsAffine X]
Lean source · statement
theorem primeIdealOf_pointOfPrime (p : PrimeSpectrum Γ(X, ⊤)) :
    (isAffineOpen_top X).primeIdealOf (pointOfPrime p) = p
instance

isLocalization_stalk_pointOfPrime

L63 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.isLocalization_stalk_pointOfPrime
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Affine
variable {X : Scheme.{u}} [IsAffine X]
Lean source · statement
instance isLocalization_stalk_pointOfPrime (p : PrimeSpectrum Γ(X, ⊤)) :
    IsLocalization.AtPrime (X.presheaf.stalk (pointOfPrime p).1) p.asIdeal
theorem

ringKrullDim_stalk_pointOfPrime

L68 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.ringKrullDim_stalk_pointOfPrime
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Affine
variable {X : Scheme.{u}} [IsAffine X]
Lean source · statement
theorem ringKrullDim_stalk_pointOfPrime (p : PrimeSpectrum Γ(X, ⊤)) :
    ringKrullDim (X.presheaf.stalk (pointOfPrime p).1) = p.asIdeal.height
theorem

isIntegrallyClosed_sections

L72 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.isIntegrallyClosed_sections
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Affine
variable {X : Scheme.{u}} [IsAffine X]
Lean source · statement
theorem isIntegrallyClosed_sections [IsDomain Γ(X, ⊤)]
    (h : ∀ x : X, IsIntegrallyClosed (X.presheaf.stalk x)) : IsIntegrallyClosed Γ(X, ⊤)
theorem

genericPoint_mem_of_ringKrullDim

L88 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.genericPoint_mem_of_ringKrullDim
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Sections
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem genericPoint_mem_of_ringKrullDim (V : X.Opens) (hV : ∀ x : X, ringKrullDim
  (X.presheaf.stalk x) ≤ 1 → x ∈ V) :
    genericPoint X ∈ V
theorem

restrict_injective

L97 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.restrict_injective
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Sections
variable {X : Scheme.{u}} [IsIntegral X]
Lean source · statement
theorem restrict_injective (V : X.Opens) (hV : ∀ x : X, ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈
  V) :
    Function.Injective (X.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op)
theorem

restrict_surjective

L111 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.restrict_surjective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Sections
variable {X : Scheme.{u}} [IsIntegral X]
variable [IsAffine X]
Lean source · statement
theorem restrict_surjective [IsLocallyNoetherian X] (hX : ∀ x : X, IsIntegrallyClosed
  (X.presheaf.stalk x))
    (V : X.Opens) (hV : ∀ x : X, ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ V) :
    Function.Surjective (X.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op)
theorem

appTop_bijective

L158 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.appTop_bijective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Sections
variable {X : Scheme.{u}} [IsIntegral X]
variable [IsAffine X]
Lean source · statement
theorem appTop_bijective [IsLocallyNoetherian X] (hX : ∀ x : X, IsIntegrallyClosed
  (X.presheaf.stalk x))
    (V : X.Opens) (hV : ∀ x : X, ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ V) :
    Function.Bijective V.ι.appTop
theorem

existsUnique_extension

L169 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.existsUnique_extension
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Sections
variable {X : Scheme.{u}} [IsIntegral X]
variable [IsAffine X]
Lean source · statement
theorem existsUnique_extension [IsLocallyNoetherian X] (hX : ∀ x : X, IsIntegrallyClosed
  (X.presheaf.stalk x))
    {Y : Scheme.{u}} [IsAffine Y] (V : X.Opens) (hV : ∀ x : X, ringKrullDim (X.presheaf.stalk x) ≤
      1 → x ∈ V)
    (v : (V : Scheme.{u}) ⟶ Y) : ∃! φ : X ⟶ Y, V.ι ≫ φ = v
theorem

exists_isDomain_away

L198 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.exists_isDomain_away
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section LocallyIntegral
open IsLocalization in
Lean source · statement
theorem exists_isDomain_away {B : Type*} [CommRing B] [IsNoetherianRing B] [_root_.IsReduced B]
    (p : Ideal B) [p.IsPrime] (Bp : Type*) [CommRing Bp] [Algebra B Bp] [IsLocalization.AtPrime Bp
      p] [IsDomain Bp] :
    ∃ f : B, f ∉ p ∧ ∀ (C : Type*) [CommRing C] [Algebra B C] [IsLocalization.Away f C], IsDomain C
theorem

exists_isIntegral_affineOpen

L278 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.exists_isIntegral_affineOpen
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Wrapper
variable {T : Scheme.{u}} [IsLocallyNoetherian T]
Lean source · statement
theorem exists_isIntegral_affineOpen (hT : ∀ x : T, IsDomain (T.presheaf.stalk x)) (x : T) :
    ∃ U : T.Opens, x ∈ U ∧ IsAffineOpen U ∧ IsIntegral (U : Scheme.{u})
theorem

hyp_restrict

L311 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.hyp_restrict
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Glue
variable {T : Scheme.{u}}
Lean source · statement
theorem hyp_restrict (hT : ∀ x : T, IsDomain (T.presheaf.stalk x) ∧ IsIntegrallyClosed
  (T.presheaf.stalk x))
    (V : T.Opens) (hV : ∀ x : T, ringKrullDim (T.presheaf.stalk x) ≤ 1 → x ∈ V) (U : T.Opens) :
    (∀ y : (U : Scheme.{u}), IsIntegrallyClosed ((U : Scheme.{u}).presheaf.stalk y)) ∧
    (∀ y : (U : Scheme.{u}), ringKrullDim ((U : Scheme.{u}).presheaf.stalk y) ≤ 1 → y ∈ U.ι ⁻¹ᵁ V)
theorem

exists_piece

L326 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.exists_piece
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Glue
variable {T : Scheme.{u}}
Lean source · statement
theorem exists_piece [IsLocallyNoetherian T]
    (hT : ∀ x : T, IsDomain (T.presheaf.stalk x) ∧ IsIntegrallyClosed (T.presheaf.stalk x))
    {Y : Scheme.{u}} [IsAffine Y] (V : T.Opens) (hV : ∀ x : T, ringKrullDim (T.presheaf.stalk x) ≤
      1 → x ∈ V)
    (v : (V : Scheme.{u}) ⟶ Y) (U : T.Opens) (hU : IsAffineOpen U) [IsIntegral (U : Scheme.{u})] :
    ∃! φ : (U : Scheme.{u}) ⟶ Y, (U.ι ⁻¹ᵁ V).ι ≫ φ = U.ι.resLE V (U.ι ⁻¹ᵁ V) le_rfl ≫ v
theorem

ext_of_agree

L336 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.ext_of_agree
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Glue
variable {T : Scheme.{u}}
Lean source · statement
theorem ext_of_agree {P Y : Scheme.{u}} [IsIntegral P] [IsAffine Y] (W : P.Opens) (hW : (W : Set
  P).Nonempty)
    (g₁ g₂ : P ⟶ Y) (h : W.ι ≫ g₁ = W.ι ≫ g₂) : g₁ = g₂
theorem

hartogs

L348 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk.AlgebraicGeometry.HartogsAffine.hartogs
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace HartogsAffine
open _root_.AlgebraicGeometry
section Main
Lean source · statement
theorem hartogs {T Y : Scheme.{u}} [IsLocallyNoetherian T]
    (hT : ∀ x : T, IsDomain (T.presheaf.stalk x) ∧ IsIntegrallyClosed (T.presheaf.stalk x))
    [IsAffine Y] (V : T.Opens) (hV : ∀ x : T, ringKrullDim (T.presheaf.stalk x) ≤ 1 → x ∈ V)
    (v : (V : Scheme.{u}) ⟶ Y) : ∃! φ : T ⟶ Y, V.ι ≫ φ = v
theorem

existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk

L456 ↗
AlgebraicGeometry.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk
    {T Y : Scheme.{u}} [IsLocallyNoetherian T]
    (hT : ∀ x : T, IsDomain (T.presheaf.stalk x) ∧ IsIntegrallyClosed (T.presheaf.stalk x))
    [IsAffine Y] (V : T.Opens) (hV : ∀ x : T, ringKrullDim (T.presheaf.stalk x) ≤ 1 → x ∈ V)
    (v : (V : Scheme.{u}) ⟶ Y) :
    ∃! φ : T ⟶ Y, V.ι ≫ φ = v

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