Module

Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk

4 declarations indexed from sourceView source ↗

Module documentation

Scheme bijective presheaf map inf of is Integrally Closed stalk

Imports4

Mathlib.AlgebraicGeometry.AffineSpace
Mathlib.RingTheory.KrullDimension.Basic
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Nyll.AlgebraicCurves.Geometry.Schemes.existsUnique_extension_to_affine_of_isIntegrallyClosed_stalk

Imported by2

abbrev

A1

L57 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.HartogsSections.A1

Documentation

The polynomial ring in one variable over lifted integers, viewed as a commutative ring object.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace HartogsSections
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · statement

abbrev A1 : CommRingCat.{u}

theorem

bijective_appTop

L60 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.HartogsSections.bijective_appTop

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace HartogsSections
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · statement

theorem bijective_appTop {T : Scheme.{u}} [IsLocallyNoetherian T]
    (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') :
    Function.Bijective (V'.ι.appTop).hom

theorem

bijective_transport

L91 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.HartogsSections.bijective_transport

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace HartogsSections
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · statement

theorem bijective_transport {X : Scheme.{u}} {A A' B B' : X.Opens} (hA : A = A') (hB : B = B')
    (k : B ⟶ A) (h : B' ≤ A') (hb : Function.Bijective (X.presheaf.map k.op)) :
    Function.Bijective (X.presheaf.map (homOfLE h).op)

theorem

bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk

L106 ↗

AlgebraicGeometry.Scheme.bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry.Scheme
open AlgebraicGeometry.Scheme

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk
    {X : Scheme.{u}} [IsLocallyNoetherian X] (V U : X.Opens)
    (hV : ∀ x : X, x ∈ V → IsDomain (X.presheaf.stalk x) ∧ IsIntegrallyClosed (X.presheaf.stalk x))
    (hU : ∀ x : X, x ∈ V → ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ U) :
    Function.Bijective (X.presheaf.map (homOfLE (inf_le_left : V ⊓ U ≤ V)).op)

Module documentation

Scheme bijective presheaf map inf of is Integrally Closed stalk

Declarations

A1

bijective_appTop

bijective_transport

bijective_presheaf_map_inf_of_isIntegrallyClosed_stalk