This file supplies scheme-theoretic boundary data using Scheme.IdealSheafData. The stalk ideal is constructed canonically as the supremum of the images of the ideal on affine neighbourhoods. Effective Cartier and normal-crossings conditions are then stated as local properties of this actual ideal-sheaf data.
The closed support and radical of an ideal sheaf are already provided by Scheme.IdealSheafData.support and Scheme.IdealSheafData.radical.
A scheme is regular at a point when its local ring there is regular.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Schemedef IsRegularAt (X : Scheme.{u}) (x : X) : PropA scheme is regular along a set when it is regular at every point of it.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Schemedef IsRegularAlong (X : Scheme.{u}) (Z : Set X) : PropA finite family in a local ring is a regular system of parameters when it is a regular sequence and generates the maximal ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Schemedef IsRegularSystemOfParameters
{R : Type u} [CommRing R] [IsLocalRing R] {d : ℕ}
(t : Fin d → R) : PropRing isomorphisms transport a regular system of parameters by mapping its concrete regular sequence and its maximal ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Schemetheorem IsRegularSystemOfParameters.map_ringEquiv
{R S : Type u} [CommRing R] [CommRing S]
[IsLocalRing R] [IsLocalRing S] {d : ℕ} {t : Fin d → R}
(h : IsRegularSystemOfParameters t) (e : R ≃+* S) :
IsRegularSystemOfParameters (e ∘ t)The product of the first r members of a parameter family.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Schemedef initialParameterProduct
{R : Type u} [CommMonoid R] {d : ℕ}
(t : Fin d → R) (r : ℕ) (hr : r ≤ d) : RThe ideal in the local ring obtained from an ideal sheaf.
It is the supremum of the images of the ideals on all affine neighbourhoods of the point. This avoids choosing a particular affine chart and is the direct ideal-theoretic analogue of forming the stalk of a subsheaf.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}def stalkIdeal (I : X.IdealSheafData) (x : X) :
Ideal (X.presheaf.stalk x)The contribution of any affine neighbourhood is contained in the stalk ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}lemma map_ideal_le_stalkIdeal (I : X.IdealSheafData) (x : X)
(U : X.affineOpens) (hx : x ∈ U.1) :
(I.ideal U).map (X.presheaf.germ U.1 x hx).hom ≤ I.stalkIdeal xTaking the stalk ideal is monotone in the ideal sheaf.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}lemma stalkIdeal_mono {I J : X.IdealSheafData} (h : I ≤ J) (x : X) :
I.stalkIdeal x ≤ J.stalkIdeal xThe stalk ideal of the unit ideal sheaf is the unit ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}lemma stalkIdeal_top (x : X) :
(⊤ : X.IdealSheafData).stalkIdeal x = ⊤An ideal sheaf is radical when it agrees with its sheafwise radical. Equivalently, it carries the reduced closed-subscheme structure on its support.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}def IsReduced (I : X.IdealSheafData) : PropAn ideal sheaf is an effective Cartier divisor at x if it is generated on an affine neighbourhood of x by a non-zero-divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}def IsEffectiveCartierAt (I : X.IdealSheafData) (x : X) : PropAn ideal sheaf defines an effective Cartier divisor if it does so at every point.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}def IsEffectiveCartier (I : X.IdealSheafData) : PropThe unit ideal sheaf is the empty effective Cartier divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}lemma isEffectiveCartier_top :
IsEffectiveCartier (⊤ : X.IdealSheafData)An ideal sheaf has strict normal crossings at x when the ambient local ring is regular and its stalk ideal is generated by a product of an initial segment of a regular system of parameters. This pointwise predicate is intended for points in the support.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}def IsStrictNormalCrossingsAt (I : X.IdealSheafData) (x : X) : PropAn ideal sheaf has strict normal crossings if it has strict normal crossings at every point of its support.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}def IsStrictNormalCrossings (I : X.IdealSheafData) : PropAn ideal sheaf has normal crossings at x when an étale neighbourhood whose image contains x makes its pullback a strict-normal-crossings ideal sheaf.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}def IsNormalCrossingsAt (I : X.IdealSheafData) (x : X) : PropAn ideal sheaf has normal crossings if it does so at every point of its support.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}def IsNormalCrossings (I : X.IdealSheafData) : PropThe ambient scheme is regular along the support of an ideal sheaf.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}def IsAmbientRegularAlongSupport (I : X.IdealSheafData) : PropStrict normal crossings force regularity of the ambient scheme along the support.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}lemma IsStrictNormalCrossings.isAmbientRegularAlongSupport
{I : X.IdealSheafData} (hI : I.IsStrictNormalCrossings) :
I.IsAmbientRegularAlongSupportStrict normal crossings are normal crossings, using the identity étale neighbourhood.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace IdealSheafData
variable {X : Scheme.{u}}lemma IsStrictNormalCrossings.isNormalCrossings
{I : X.IdealSheafData} (hI : I.IsStrictNormalCrossings) :
I.IsNormalCrossingsAn effective Cartier divisor on a scheme, represented by its ideal sheaf.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Schemedef EffectiveCartierDivisor (X : Scheme.{u})Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}instance : Coe (EffectiveCartierDivisor X) X.IdealSheafDataThe empty effective Cartier divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}def empty (X : Scheme.{u}) : EffectiveCartierDivisor XThe closed support of an effective Cartier divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}def support (D : EffectiveCartierDivisor X) : TopologicalSpace.Closeds XThe empty divisor has empty support.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}lemma support_empty (X : Scheme.{u}) :
(empty X).support = ⊥A reduced effective Cartier divisor has radical ideal sheaf.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}def IsReduced (D : EffectiveCartierDivisor X) : PropThe empty effective Cartier divisor is reduced.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}lemma isReduced_empty (X : Scheme.{u}) :
(empty X).IsReducedStrict normal crossings at a point of an effective Cartier divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}def IsStrictNormalCrossingsAt (D : EffectiveCartierDivisor X) (x : X) : PropStrict normal crossings for an effective Cartier divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}def IsStrictNormalCrossings (D : EffectiveCartierDivisor X) : PropNormal crossings at a point of an effective Cartier divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}def IsNormalCrossingsAt (D : EffectiveCartierDivisor X) (x : X) : PropNormal crossings for an effective Cartier divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}def IsNormalCrossings (D : EffectiveCartierDivisor X) : PropThe ambient scheme is regular along the support of an effective Cartier divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}def IsAmbientRegularAlongSupport (D : EffectiveCartierDivisor X) : PropA strict-normal-crossings effective Cartier divisor is a normal-crossings divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open scoped BigOperators
namespace AlgebraicGeometry
universe u
namespace Scheme
namespace EffectiveCartierDivisor
variable {X : Scheme.{u}}lemma IsStrictNormalCrossings.isNormalCrossings
{D : EffectiveCartierDivisor X} (hD : D.IsStrictNormalCrossings) :
D.IsNormalCrossings