31.16 Effective Cartier… to 31.24 Meromorphic functions and…

Section31.16 Effective Cartier divisors on Noetherian schemes#

Section 31.16 of the Stacks Project, Tag 0B3Q. 13 tags here are carried by 21 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AYL, a lemma

Tag 0AYL in the Stacks Project.

Stacks.Divisors.isRegularSection_iff_forall_associatedPoint_notMem_maximalSmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularSectionAssociatedPoints.lean, line 255.

Stacks Project, Tag 0AYL. Let X be a locally Noetherian scheme, L an invertible 𝒪_X-module and s ∈ Γ(X, L). Then s is a regular section if and only if s does not vanish at any associated point of X, i.e. its germ at every associated point avoids 𝔪_x L_x.

theorem isRegularSection_iff_forall_associatedPoint_notMem_maximalSmul
    [AlgebraicGeometry.IsLocallyNoetherian X] (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : L.sections) :
    AlgebraicGeometry.IsRegularSection X.presheaf
        (structureSheafRing X.toRingedSpace).property s ↔
      ∀ x ∈ schemeAssociatedPoints X,
        (L.presheaf.Γgerm x).hom (s.eval (op ⊤)) ∉ Stacks.ModuleStalk.maximalSmul L x

Tag 0AG8, a lemma

Tag 0AG8 in the Stacks Project.

Stacks.Divisors.isLocallyPrincipal_of_stalk_isPrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierStalk/Stalkwise.lean, line 255.

Stacks Project, Tag 0AG8. A closed subscheme of a locally Noetherian scheme is locally principal if its ideal is principal in the local ring at each point of the subscheme.

Outside the support the ideal of the local ring is the unit ideal, so the hypothesis is only about points of the subscheme; at each point principality then spreads to an affine neighbourhood by Stacks.Divisors.exists_affineOpens_isPrincipal_of_stalk_isPrincipal.

The companion Stacks.Divisors.isEffectiveCartierDivisor_of_stalk_isPrincipal_nonZeroDivisor upgrades the conclusion to an effective Cartier divisor when the stalk generators are nonzerodivisors.

theorem isLocallyPrincipal_of_stalk_isPrincipal {X : Scheme.{u}} [IsLocallyNoetherian X]
    (I : X.IdealSheafData)
    (hI : ∀ x : X, x ∈ I.support → (IdealSheafData.stalk I x).IsPrincipal) :
    IsLocallyPrincipal I

Stacks.Divisors.isEffectiveCartierDivisor_of_stalk_isPrincipal_nonZeroDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierStalk/StalkwiseRegular.lean, line 161. References: EGA IV (21.2.12), “special case”.

Stacks Project, Tag 0AG8. A closed subscheme of a locally Noetherian scheme is an effective Cartier divisor if its ideal is generated by a single nonzerodivisor in the local ring at each point of the subscheme.

theorem isEffectiveCartierDivisor_of_stalk_isPrincipal_nonZeroDivisor {X : Scheme.{u}}
    [IsLocallyNoetherian X] (I : X.IdealSheafData)
    (hI : ∀ x : X, x ∈ I.support → ∃ g ∈ nonZeroDivisors (X.presheaf.stalk x),
      IdealSheafData.stalk I x = Ideal.span {g}) :
    IsEffectiveCartierDivisor I

Stacks.Divisors.isLocallyPrincipal_of_forall_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/StalkLocallyPrincipal.lean, line 281. The attribute's comment: “(1)”.

If the stalk of the ideal sheaf at every point of the closed subscheme can be generated by one element, the subscheme is locally principal.

theorem isLocallyPrincipal_of_forall_stalk [IsLocallyNoetherian X]
    (hst : ∀ x ∈ I.supportSet, ∃ (U : X.affineOpens) (hxU : x ∈ (U : Set X)),
      (Ideal.map (X.presheaf.germ U.1 x hxU).hom (I.ideal U)).IsPrincipal) :
    IsLocallyPrincipal I

Stacks.Divisors.isEffectiveCartierDivisor_of_forall_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/StalkLocallyPrincipal.lean, line 298. The attribute's comment: “(2)”.

If the stalk of the ideal sheaf at every point of the closed subscheme can be generated by a single nonzerodivisor, the subscheme is an effective Cartier divisor.

theorem isEffectiveCartierDivisor_of_forall_stalk [IsLocallyNoetherian X]
    (hst : ∀ x ∈ I.supportSet, ∃ (U : X.affineOpens) (hxU : x ∈ (U : Set X)),
      ∃ ξ ∈ nonZeroDivisors (X.presheaf.stalk x),
        Ideal.map (X.presheaf.germ U.1 x hxU).hom (I.ideal U) = Ideal.span {ξ}) :
    IsEffectiveCartierDivisor I

Tag 0BCN, a lemma

Tag 0BCN in the Stacks Project.

AlgebraicGeometry.ringKrullDim_stalk_le_one_of_isLocallyPrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/Codimension.lean, line 185. The attribute's comment: “part (1)”.

A component of a locally principal closed subscheme has codimension at most one.

theorem ringKrullDim_stalk_le_one_of_isLocallyPrincipal
    {X : Scheme.{u}} [IsLocallyNoetherian X] (I : X.IdealSheafData)
    (hI : IsLocallyPrincipal I)
    (ξ : I.subscheme)
    (hξ : ∃ Z : irreducibleComponents I.subscheme, IsGenericPoint ξ (Z : Set I.subscheme)) :
    ringKrullDim (X.presheaf.stalk (I.subschemeι ξ)) ≤ 1

AlgebraicGeometry.ringKrullDim_stalk_eq_one_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/Codimension.lean, line 204. The attribute's comment: “part (2)”.

A component of an effective Cartier divisor has codimension exactly one.

theorem ringKrullDim_stalk_eq_one_of_isEffectiveCartierDivisor
    {X : Scheme.{u}} [IsLocallyNoetherian X] (I : X.IdealSheafData)
    (hI : IsEffectiveCartierDivisor I)
    (ξ : I.subscheme)
    (hξ : ∃ Z : irreducibleComponents I.subscheme, IsGenericPoint ξ (Z : Set I.subscheme)) :
    ringKrullDim (X.presheaf.stalk (I.subschemeι ξ)) = 1

Tag 0AG9, a lemma

Tag 0AG9 in the Stacks Project.

AlgebraicGeometry.isDiscreteValuationRing_stalk_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/DiscreteValuation.lean, line 39. References: EGA IV (3.4.6), “partial”.

Let X be a locally Noetherian scheme and D ⊆ X an integral closed subscheme which is an effective Cartier divisor. The local ring of X at the generic point of D is a discrete valuation ring; in particular it is a domain.

theorem isDiscreteValuationRing_stalk_genericPoint {X : Scheme.{u}} [IsLocallyNoetherian X]
    (I : X.IdealSheafData) [IsIntegral I.subscheme] (hI : IsEffectiveCartierDivisor I) :
    ∃ _ : IsDomain (X.presheaf.stalk (I.subschemeι (_root_.genericPoint I.subscheme))),
      IsDiscreteValuationRing
        (X.presheaf.stalk (I.subschemeι (_root_.genericPoint I.subscheme)))

Tag 0B3R, a lemma

Tag 0B3R in the Stacks Project.

AlgebraicGeometry.isEffectiveCartierDivisor_hasPropertySk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/SerreCondition.lean, line 174.

An effective Cartier divisor of an (Sₖ) locally Noetherian scheme is (Sₖ₋₁) for k ≥ 1.

theorem isEffectiveCartierDivisor_hasPropertySk
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (I : X.IdealSheafData) (hI : IsEffectiveCartierDivisor I)
    (k : ℕ) (hk : 1 ≤ k) (hX : HasPropertySk X k) :
    @HasPropertySk I.subscheme
      (LocallyOfFiniteType.isLocallyNoetherian I.subschemeι) (k - 1)

Tag 0B3S, a lemma

Tag 0B3S in the Stacks Project.

AlgebraicGeometry.isNormal_effectiveCartierDivisor_hasPropertySk_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/SerreCondition.lean, line 283. References: EGA IV (21.7.3), “normal ⇒ (S_1)”.

Stacks Project, Tag 0B3S. An effective Cartier divisor on a locally Noetherian normal scheme satisfies Serre's condition (S₁): the scheme satisfies (S₂) by Serre's criterion, and Tag 0B3R drops the index by one.

theorem isNormal_effectiveCartierDivisor_hasPropertySk_one (X : Scheme.{u})
    [IsLocallyNoetherian X] [IsNormal X] (I : X.IdealSheafData)
    (hI : IsEffectiveCartierDivisor I) :
    letI : IsLocallyNoetherian I.subscheme :=
      LocallyOfFiniteType.isLocallyNoetherian I.subschemeι
    HasPropertySk I.subscheme 1

Tag 0AGA, a lemma

Tag 0AGA in the Stacks Project.

AlgebraicGeometry.isEffectiveCartierDivisor_of_codimension_one_of_uniqueFactorizationMonoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/CodimensionOne.lean, line 175. References: EGA IV (21.7.4), “c) => a'')”; EGA IV (21.6.9), “(ii) c) ⇒ b)”.

A codimension-one integral closed subscheme is an effective Cartier divisor when the ambient local rings along it are UFDs.

theorem isEffectiveCartierDivisor_of_codimension_one_of_uniqueFactorizationMonoid
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (I : X.IdealSheafData) [IsIntegral I.subscheme]
    (hcodim : codimension (IrreducibleCloseds.closureSingleton
      (I.subschemeι (_root_.genericPoint I.subscheme))) = 1)
    (hUFD : ∀ x : X, x ∈ I.support →
      UniqueFactorizationMonoid (X.presheaf.stalk x)) :
    IsEffectiveCartierDivisor I

Tag 0AGB, a lemma

Tag 0AGB in the Stacks Project.

AlgebraicGeometry.exists_effectiveCartierDivisor_agree_off_codimension_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/CartierPart.lean, line 1086. The attribute's comment: “cartier_part”.

The Cartier part of a closed subscheme supported, up to codimension two, on integral effective Cartier divisors.

theorem exists_effectiveCartierDivisor_agree_off_codimension_two
    (X : Scheme.{u}) [IsNoetherian X] (Z : X.IdealSheafData)
    {ι : Type v} (D : ι → X.IdealSheafData) (Z' : Closeds X)
    (hD : ∀ i, IsIntegral (D i).subscheme ∧
      IsEffectiveCartierDivisor (D i))
    (hZ' : ∀ x : X, x ∈ (Z' : Set X) →
      (2 : ℕ∞) ≤ codimension (IrreducibleCloseds.closureSingleton x))
    (hcover : (Z.support : Set X) ⊆
      (Z' : Set X) ∪ ⋃ i, ((D i).support : Set X)) :
    ∃ a : ι →₀ ℕ,
      let E : X.IdealSheafData := a.prod fun i n => (D i) ^ n
      IsEffectiveCartierDivisor E ∧
        Z ≤ E ∧
        ∃ U : X.Opens,
          E.comap U.ι = Z.comap U.ι ∧
          ∀ x : X, x ∈ (Z.support : Set X) → x ∉ (U : Set X) →
            (2 : ℕ∞) ≤ codimension (IrreducibleCloseds.closureSingleton x)

AlgebraicGeometry.exists_integral_effectiveCartierDivisors_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/DivisorCover.lean, line 87. The attribute's comment: “supply_divisors”.

A nowhere dense closed subscheme of a Noetherian scheme with factorial local rings along it, or of a regular scheme, is covered by integral effective Cartier divisors up to a closed subset of codimension at least two.

theorem exists_integral_effectiveCartierDivisors_cover
    (X : Scheme.{u}) [IsNoetherian X] (Z : X.IdealSheafData)
    (hZ : IsNowhereDense (Z.support : Set X))
    (h : (∀ x : X, x ∈ Z.support →
        UniqueFactorizationMonoid (X.presheaf.stalk x)) ∨ IsRegular X) :
    ∃ (D : Set X.IdealSheafData) (Z' : Closeds X),
      (∀ I ∈ D, IsIntegral I.subscheme ∧
        IsEffectiveCartierDivisor I) ∧
      (∀ x : X, x ∈ (Z' : Set X) →
        (2 : ℕ∞) ≤ codimension (IrreducibleCloseds.closureSingleton x)) ∧
      (Z.support : Set X) ⊆ (Z' : Set X) ∪ ⋃ I ∈ D, (I.support : Set X)

Tag 0BXH, a lemma

Tag 0BXH in the Stacks Project.

AlgebraicGeometry.isEffectiveCartierDivisor_of_codimension_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/NoEmbeddedPoints.lean, line 317. References: EGA IV (21.6.9), “(ii) c) ⇒ b)”.

A codimension-one closed subscheme with no embedded points is an effective Cartier divisor when the ambient local rings along it are UFDs, or the ambient scheme is regular.

theorem isEffectiveCartierDivisor_of_codimension_one
    {X : Scheme.{u}} [IsNoetherian X] (I : X.IdealSheafData)
    (hno : HasNoEmbeddedPoints I.subscheme)
    (hcodim : ∀ Z ∈ irreducibleComponents I.subscheme,
      ∀ x : I.subscheme, IsGenericPoint x Z →
        codimension (IrreducibleCloseds.closureSingleton (I.subschemeι x)) = 1)
    (hlocal : (∀ x : X, x ∈ I.support →
      UniqueFactorizationMonoid (X.presheaf.stalk x)) ∨ IsRegular X) :
    IsEffectiveCartierDivisor I

Tag 0BXI, a lemma

Tag 0BXI in the Stacks Project.

Ideal.isPrincipal_of_noEmbeddedAssociatedPrimes_of_minimalPrimes_height_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PrincipalIdeals.lean, line 138. References: EGA IV (21.12.9), “special case”.

An ideal of pure height one with no embedded primes in a Noetherian UFD is principal.

theorem isPrincipal_of_noEmbeddedAssociatedPrimes_of_minimalPrimes_height_eq_one
    {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R]
    [UniqueFactorizationMonoid R] (I : Ideal R)
    (hI : HasNoEmbeddedAssociatedPrimes (R ⧸ I) (R ⧸ I))
    (hheight : ∀ p ∈ I.minimalPrimes, p.height = 1) :
    I.IsPrincipal

Tag 0BCP, a lemma

Tag 0BCP in the Stacks Project.

AlgebraicGeometry.exists_finsupp_eq_prod_of_support_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/Decomposition.lean, line 221. The attribute's comment: “decomposition”.

Let X be a Noetherian scheme and D an effective Cartier divisor on X whose points are covered by a family Dᵢ of integral effective Cartier divisors. Then D is a finite nonnegative combination of the Dᵢ: there is a finitely supported a : ι →₀ ℕ with ℐ_D = Π ℐ_{Dᵢ}^{aᵢ}.

theorem exists_finsupp_eq_prod_of_support_cover
    {X : Scheme.{u}} [IsNoetherian X] (I : X.IdealSheafData)
    (hI : IsEffectiveCartierDivisor I)
    {ι : Type v} (D : ι → X.IdealSheafData)
    (hD : ∀ i, IsIntegral (D i).subscheme ∧ IsEffectiveCartierDivisor (D i))
    (hcover : ∀ x ∈ I.supportSet, ∃ i, x ∈ (D i).supportSet) :
    ∃ a : ι →₀ ℕ, I = a.prod fun i n => D i ^ n

AlgebraicGeometry.exists_integral_effectiveCartierDivisors_cover_supportSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/Decomposition.lean, line 260. The attribute's comment: “existence of the covering divisors”.

Let X be a Noetherian scheme and D an effective Cartier divisor on X. If the local rings of X at the points of D are unique factorization domains — in particular if X is regular — then there is a family of integral effective Cartier divisors covering the points of D.

theorem exists_integral_effectiveCartierDivisors_cover_supportSet
    {X : Scheme.{u}} [IsNoetherian X] (I : X.IdealSheafData)
    (hI : IsEffectiveCartierDivisor I)
    (h : (∀ x : X, x ∈ I.supportSet → UniqueFactorizationMonoid (X.presheaf.stalk x)) ∨
      IsRegular X) :
    ∃ S : Set X.IdealSheafData,
      (∀ J ∈ S, IsIntegral J.subscheme ∧ IsEffectiveCartierDivisor J) ∧
      (∀ x ∈ I.supportSet, ∃ J ∈ S, x ∈ J.supportSet)

Tag 0AYM, a lemma

Tag 0AYM in the Stacks Project.

AlgebraicGeometry.InvertibleSheafGeneral.exists_effectiveCartierDivisors_tensor_invertibleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheafGeneral.lean, line 211.

Stacks Project, Tag 0AYM, the general clause. On a Noetherian scheme X carrying an ample invertible module ℒ, every invertible 𝒪_X-module 𝒩 is the sheaf 𝒪_X(D - D') of a difference of two effective Cartier divisors, and D and D' may both be chosen disjoint from any prescribed finite subset E of X.

𝒩 ≅ 𝒪_X(D - D') = 𝒪_X(D) ⊗ 𝒪_X(D')^{⊗ -1} is stated here in the equivalent multiplicative form 𝒩 ⊗ 𝒪_X(D') ≅ 𝒪_X(D); see the module documentation. The case D' = ∅ for X quasi-affine is AlgebraicGeometry.exists_effectiveCartierDivisor_invertibleSheaf_of_isQuasiAffine.

theorem exists_effectiveCartierDivisors_tensor_invertibleSheaf [IsNoetherian X] (L : X.Modules)
    [IsInvertibleModule X L] (hL : IsAmple X L) (N : X.Modules) [IsInvertibleModule X N]
    {E : Set X} (hE : E.Finite) :
    ∃ D D' : X.IdealSheafData,
      Stacks.Divisors.IsEffectiveCartierDivisor D ∧
      Stacks.Divisors.IsEffectiveCartierDivisor D' ∧
      Disjoint E D.supportSet ∧ Disjoint E D'.supportSet ∧
      Nonempty ((N ⊗ Stacks.Divisors.invertibleSheaf' D' : X.Modules) ≅
        Stacks.Divisors.invertibleSheaf' D)

AlgebraicGeometry.exists_effectiveCartierDivisor_invertibleSheaf_of_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/QuasiAffineInvertibleSheaf.lean, line 151. The attribute's comment: “quasi-affine case with empty negative divisor”.

Stacks Project, Tag 0AYM, the quasi-affine clause. On a Noetherian quasi-affine scheme every invertible 𝒪_X-module 𝒩 is isomorphic to the invertible sheaf 𝒪_X(D) of an effective Cartier divisor D, and D may be chosen disjoint from any prescribed finite subset E of X. This is the case D' = ∅ of the general statement 𝒩 ≅ 𝒪_X(D - D').

theorem exists_effectiveCartierDivisor_invertibleSheaf_of_isQuasiAffine
    [IsNoetherian X] [X.IsQuasiAffine] (N : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property N]
    {E : Set X} (hE : E.Finite) :
    ∃ D : X.IdealSheafData,
      Stacks.Divisors.IsEffectiveCartierDivisor D ∧
      Disjoint E D.supportSet ∧
      Nonempty (N ≅ Stacks.Divisors.invertibleSheaf' D)

Tag 0B3T, a lemma

Tag 0B3T in the Stacks Project.

AlgebraicGeometry.exists_reflexiveHull_exteriorPower_iso_tensor_cartier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DeterminantTwistBoundDivisorQuotient.lean, line 63. The attribute's comment: “bounded Cartier twist”.

Stacks Project, Tag 0B3T. In a right-exact sequence of coherent modules of generic rank r on an integral regular scheme of dimension at most two, whose quotient is the direct image of a module of rank s finite locally free on an integral effective Cartier divisor D, the determinant line bundles of the first two terms differ by at most min s r copies of D.

The cokernel of the stalk map at the generic point of D is κ ^ s by AlgebraicGeometry.linearEquiv_quotient_range_stalkHom_fin, which is the one hypothesis of AlgebraicGeometry.exists_pow_le_min_tensorIso_detMap_of_isEffectiveCartierDivisor still open. Local Noetherianness, all the proof needs, comes from regularity.

theorem exists_reflexiveHull_exteriorPower_iso_tensor_cartier (X : Scheme.{u})
    [IsIntegral X] (hX : AlgebraicGeometry.IsRegular X)
    (hXdim : topologicalKrullDim X ≤ 2)
    (D : X.IdealSheafData) (hD : Stacks.Divisors.IsEffectiveCartierDivisor D)
    [IsIntegral D.subscheme]
    (G : D.subscheme.Modules) (s : ℕ)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} G s]
    (S : ShortComplex X.Modules) [S.X₁.IsCoherent] [S.X₂.IsCoherent]
    (hS : S.Exact) [Epi S.g]
    (hquot : S.X₃ ≅ (Scheme.Modules.pushforward D.subschemeι).obj G)
    (r : ℕ) (U : X.Opens) (hU : ∃ x : X, x ∈ U)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (S.X₁.over U) r]
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (S.X₂.over U) r] :
    ∃ k : ℕ, k ≤ min s r ∧ Nonempty ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨X.sheaf.obj, Presheaf.isSheaf_of_isSheaf_comp _ (X.sheaf.obj) (forget₂ CommRingCat RingCat)
        (X.ringCatSheaf.property)⟩).obj ((Stacks.Divisors.invertibleSheaf' (D ^ k)))).obj
          ((reflexiveHull (exteriorPower S.X₁ (r : ℤ))))) ≅
      reflexiveHull (exteriorPower S.X₂ (r : ℤ)))

AlgebraicGeometry.isInvertible_reflexiveHull_exteriorPower_of_genericRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/DeterminantInvertible.lean, line 323. The attribute's comment: “invertibility of the determinant line bundles”.

Stacks Project, Tag 0B3T. The reflexive hull (⋀^r F)^∨∨ of the top exterior power of a coherent module of generic rank r on an integral regular scheme of dimension at most two is a line bundle.

Generic rank r is finite local freeness of rank r of F on the slice site over a nonempty open U. The hull is coherent and reflexive, hence finite locally free by Tag 0B3N, and on the irreducible space of an integral scheme its fibre rank is constant; over U the exterior power ⋀^r F is finite locally free of rank binom(r, r) = 1 with free stalks, and the hull preserves the fibre rank there, so that constant is one.

theorem isInvertible_reflexiveHull_exteriorPower_of_genericRank
    (X : Scheme.{u}) [IsIntegral X] (hX : AlgebraicGeometry.IsRegular X)
    (hXdim : topologicalKrullDim X ≤ 2)
    (F : X.Modules) [F.IsCoherent] (r : ℕ) (U : X.Opens) (hU : ∃ x : X, x ∈ U)
    [SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u} (F.over U) r] :
    Stacks.SheafOfModules.IsInvertible X.sheaf.obj (structureSheaf X.sheaf).property
      (Stacks.AlgebraicGeometry.ReflexiveModules.reflexiveHull
        (Scheme.Modules.exteriorPower F r))

Sources

• Section 31.16, Tag 0B3Q
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Divisors.isRegularSection_iff_forall_associatedPoint_notMem_maximalSmul · Stacks.Divisors.isLocallyPrincipal_of_stalk_isPrincipal · Stacks.Divisors.isEffectiveCartierDivisor_of_stalk_isPrincipal_nonZeroDivisor · Stacks.Divisors.isLocallyPrincipal_of_forall_stalk · Stacks.Divisors.isEffectiveCartierDivisor_of_forall_stalk · AlgebraicGeometry.ringKrullDim_stalk_le_one_of_isLocallyPrincipal · AlgebraicGeometry.ringKrullDim_stalk_eq_one_of_isEffectiveCartierDivisor · AlgebraicGeometry.isDiscreteValuationRing_stalk_genericPoint

Section31.17 Complements of affine opens#

Section 31.17 of the Stacks Project, Tag 0BCQ. 6 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BCR, a lemma

Tag 0BCR in the Stacks Project.

Stacks.Divisors.isAffineOpen_puncturedSpectrum_iff_krullDimLE_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/PuncturedSpectrumAffineCriterion.lean, line 358. References: EGA IV (21.12.9), “special case”.

The punctured spectrum of a Noetherian local ring is affine if and only if the ring has Krull dimension at most one.

theorem isAffineOpen_puncturedSpectrum_iff_krullDimLE_one :
    IsAffineOpen (puncturedSpectrum A) ↔ Ring.KrullDimLE 1 A

Tag 0BCU, a lemma

Tag 0BCU in the Stacks Project.

Stacks.Divisors.krullDimLE_one_stalk_at_genericPoint_compl_affineOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/PuncturedSpectrumAffineCriterion.lean, line 435. The attribute's comment: “dimension bound”. References: EGA IV (21.12.7), “codimension ≤ 1”; SGA 6 II (2.2.6), “dim ≤ 1 at maximal pts”; SGA 2 V (3.4).

Let U be an open subscheme of a locally Noetherian scheme X whose inclusion is affine. At the generic point ξ of an irreducible component of X ∖ U the local ring has Krull dimension at most one.

Pulling U back along Spec 𝒪_{X,ξ} → X gives the punctured spectrum of 𝒪_{X,ξ}, which is affine because the inclusion of U is; so Tag 0BCR applies.

theorem krullDimLE_one_stalk_at_genericPoint_compl_affineOpenImmersion
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (U : X.Opens) [IsAffineHom U.ι]
    {Z : Set ↑((U : Set X)ᶜ)} (hZ : Z ∈ irreducibleComponents ↑((U : Set X)ᶜ))
    {ξ : ↑((U : Set X)ᶜ)} (hξ : IsGenericPoint ξ Z) :
    Ring.KrullDimLE 1 (X.presheaf.stalk (ξ : X))

Stacks.Divisors.ringKrullDim_stalk_at_genericPoint_compl_affineOpenImmersion_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/PuncturedSpectrumAffineCriterion.lean, line 503. The attribute's comment: “equality in the closure”. References: EGA IV (21.12.7), “codimension = 1 if dense”; SGA 6 II (2.2.6), “dim = 1 case”.

With the hypotheses of Stacks.Divisors.krullDimLE_one_stalk_at_genericPoint_compl_affineOpenImmersion, if U is dense or ξ lies in the closure of U, then the local ring at ξ has dimension exactly one.

Some point of U specializes to ξ, so it is a point of Spec 𝒪_{X,ξ} other than the closed point; hence the dimension is positive.

theorem ringKrullDim_stalk_at_genericPoint_compl_affineOpenImmersion_eq_one
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (U : X.Opens) [IsAffineHom U.ι]
    {Z : Set ↑((U : Set X)ᶜ)} (hZ : Z ∈ irreducibleComponents ↑((U : Set X)ᶜ))
    {ξ : ↑((U : Set X)ᶜ)} (hξ : IsGenericPoint ξ Z)
    (hξU : Dense (U : Set X) ∨ (ξ : X) ∈ closure (U : Set X)) :
    ringKrullDim (X.presheaf.stalk (ξ : X)) = 1

Tag 0BCV, a lemma

Tag 0BCV in the Stacks Project.

Stacks.PuncturedSpectrum.krullDimLE_one_stalk_at_genericPoint_compl_affineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PuncturedSpectrum/SeparatedComplement.lean, line 71. The attribute's comment: “dimension bound”. References: EGA IV (21.12.7), “dim ≤ 1, U affine open”; SGA 2 V (3.4); SGA 6 II (2.2.6), “X sep, U affine; dim≤1”.

Stacks Project, Tag 0BCV. The local ring at the generic point of an irreducible component of the complement of an affine open in a separated locally Noetherian scheme has Krull dimension at most one.

theorem krullDimLE_one_stalk_at_genericPoint_compl_affineOpen
    (X : Scheme.{u}) [Scheme.IsSeparated X] [IsLocallyNoetherian X]
    (U : X.Opens) (hU : IsAffineOpen U)
    {Z : Set ↑((U : Set X)ᶜ)} (hZ : Z ∈ irreducibleComponents ↑((U : Set X)ᶜ))
    {ξ : ↑((U : Set X)ᶜ)} (hξ : IsGenericPoint ξ Z) :
    Ring.KrullDimLE 1 (X.presheaf.stalk (ξ : X))

Stacks.PuncturedSpectrum.ringKrullDim_stalk_at_genericPoint_compl_affineOpen_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/PuncturedSpectrum/SeparatedComplement.lean, line 85. The attribute's comment: “equality in the closure”. References: EGA IV (21.12.7), “dim = 1, U affine open”; SGA 6 II (2.2.6), “X sep, U affine; dim=1”.

Stacks Project, Tag 0BCV. Under the hypotheses of the dimension bound, the local ring has dimension one when the affine open is dense or the generic point is in its closure.

theorem ringKrullDim_stalk_at_genericPoint_compl_affineOpen_eq_one
    (X : Scheme.{u}) [Scheme.IsSeparated X] [IsLocallyNoetherian X]
    (U : X.Opens) (hU : IsAffineOpen U)
    {Z : Set ↑((U : Set X)ᶜ)} (hZ : Z ∈ irreducibleComponents ↑((U : Set X)ᶜ))
    {ξ : ↑((U : Set X)ᶜ)} (hξ : IsGenericPoint ξ Z)
    (hξU : Dense (U : Set X) ∨ (ξ : X) ∈ closure (U : Set X)) :
    ringKrullDim (X.presheaf.stalk (ξ : X)) = 1

Tag 0BCW, a lemma

Tag 0BCW in the Stacks Project.

AlgebraicGeometry.exists_effectiveCartierDivisor_compl_affineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/AffineComplement.lean, line 107. The attribute's comment: “the separated case, where the diagonal is affine”.

Stacks Project, Tag 0EGJ. The complement of a dense affine open in a Noetherian scheme with affine diagonal is the support of an effective Cartier divisor if its local rings along the complement are UFDs.

theorem exists_effectiveCartierDivisor_compl_affineOpen
    (X : Scheme.{u}) [IsNoetherian X]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    (U : X.Opens) (hU : IsAffineOpen U) (hDense : Dense (U : Set X))
    (hUFD : ∀ x : X, x ∉ U → UniqueFactorizationMonoid (X.presheaf.stalk x)) :
    ∃ I : X.IdealSheafData,
      IsEffectiveCartierDivisor I ∧
        (I.support : Set X) = (U : Set X)ᶜ

AlgebraicGeometry.exists_effectiveCartierDivisor_compl_affineOpen_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/SeparatedAffineComplement.lean, line 54.

Stacks Project, Tag 0BCW. Let X be a Noetherian separated scheme and U ⊆ X a dense affine open whose complement meets only points with factorial local rings. Then there is an effective Cartier divisor D ⊆ X with U = X ∖ D.

theorem exists_effectiveCartierDivisor_compl_affineOpen_of_isSeparated
    (X : Scheme.{u}) [IsNoetherian X] [Scheme.IsSeparated X]
    (U : X.Opens) (hU : IsAffineOpen U) (hdense : Dense (U : Set X))
    (hUFD : ∀ x : X, x ∉ U → UniqueFactorizationMonoid (X.presheaf.stalk x)) :
    ∃ I : X.IdealSheafData,
      IsEffectiveCartierDivisor I ∧ (U : Set X) = (I.support : Set X)ᶜ

Tag 0EGJ, a lemma

Tag 0EGJ in the Stacks Project.

AlgebraicGeometry.exists_effectiveCartierDivisor_compl_affineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/AffineComplement.lean, line 107.

Stacks Project, Tag 0EGJ. The complement of a dense affine open in a Noetherian scheme with affine diagonal is the support of an effective Cartier divisor if its local rings along the complement are UFDs.

theorem exists_effectiveCartierDivisor_compl_affineOpen
    (X : Scheme.{u}) [IsNoetherian X]
    [IsAffineHom (pullback.diagonal (terminal.from X))]
    (U : X.Opens) (hU : IsAffineOpen U) (hDense : Dense (U : Set X))
    (hUFD : ∀ x : X, x ∉ U → UniqueFactorizationMonoid (X.presheaf.stalk x)) :
    ∃ I : X.IdealSheafData,
      IsEffectiveCartierDivisor I ∧
        (I.support : Set X) = (U : Set X)ᶜ

Tag 0GML, a lemma

Tag 0GML in the Stacks Project.

AlgebraicGeometry.exists_isAmpleFamily_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AmpleFamilyRegular.lean, line 187. References: SGA 6 II (2.2.7.1), “more general”.

Stacks Project, Tag 0GML. A quasi-compact regular scheme whose diagonal is affine has an ample family of invertible modules.

The family is {𝒪_X(D x)} indexed by the points of X, where D x is the effective Cartier divisor whose support is the complement of a dense affine open around x, supplied by Tag 0EGJ; the required section of 𝒪_X(D x) is the canonical section 1_{D x}, whose nonvanishing locus is exactly that affine open.

theorem exists_isAmpleFamily_of_isRegular (X : Scheme.{u}) [CompactSpace X]
    [IsAffineHom (pullback.diagonal (terminal.from X))] (hX : IsRegular X) :
    ∃ (I : Type u) (L : I → X.Modules), X.IsAmpleFamily L

Sources

• Section 31.17, Tag 0BCQ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Divisors.isAffineOpen_puncturedSpectrum_iff_krullDimLE_one · Stacks.Divisors.krullDimLE_one_stalk_at_genericPoint_compl_affineOpenImmersion · Stacks.Divisors.ringKrullDim_stalk_at_genericPoint_compl_affineOpenImmersion_eq_one · Stacks.PuncturedSpectrum.krullDimLE_one_stalk_at_genericPoint_compl_affineOpen · Stacks.PuncturedSpectrum.ringKrullDim_stalk_at_genericPoint_compl_affineOpen_eq_one · AlgebraicGeometry.exists_effectiveCartierDivisor_compl_affineOpen · AlgebraicGeometry.exists_effectiveCartierDivisor_compl_affineOpen_of_isSeparated · AlgebraicGeometry.exists_isAmpleFamily_of_isRegular

Section31.18 Norms#

Section 31.18 of the Stacks Project, Tag 0BCX. 11 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0BCX, the section

Tag 0BCX in the Stacks Project.

Stacks.Norm.MorphismNorm, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/FiniteLocallyFree/Norm.lean, line 125. The attribute's comment: “norm of degree d”.

Stacks Project, Section 0BCX. A norm of degree d for a morphism of schemes: a multiplicative map of sheaves preserving pointwise vanishing whose value on a function pulled back from the target is its d-th power.

structure MorphismNorm {X Y : Scheme.{u}} (f : X ⟶ Y) (d : ℕ) extends MorphismNormMap f

Tag 0BUT, a lemma

Tag 0BUT in the Stacks Project.

Stacks.Divisors.exists_isTrivial_restrict_preimage_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteTrivialize/TargetCover.lean, line 188.

Stacks Project, Tag 0BUT, written with Stacks.SheafOfModules.IsTrivial: for a finite morphism f : X ⟶ Y, an invertible 𝒪_X-module L and a point y of Y, there is an open neighbourhood V of y over which L becomes trivial on the inverse image.

theorem exists_isTrivial_restrict_preimage_of_isFinite {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsFinite f] (L : X.Modules)
    [IsInvertible X.presheaf (structureSheafRing X.toRingedSpace).property L] (y : Y) :
    ∃ V : Y.Opens, y ∈ V ∧
      IsTrivial (f ⁻¹ᵁ V).toScheme.presheaf
        (structureSheafRing (f ⁻¹ᵁ V).toScheme.toRingedSpace).property
        (L.restrict (f ⁻¹ᵁ V).ι)

Tag 0BCY, a lemma

Tag 0BCY in the Stacks Project.

Stacks.Divisors.hasNormPullbackPower_normPicardData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormInvertible/PullbackPower.lean, line 270. The attribute's comment: “the pullback-power formula”.

Stacks Project, Tag 0BCY, the pullback--power clause: the homomorphism of Picard groups induced by a norm of degree d carries the class of f^*𝒩 to the class of 𝒩^{⊗ d}, for every invertible 𝒪_Y-module 𝒩.

Together with Stacks.Divisors.exists_normPicardAddMonoidHom, which is the tag's other clause, this completes Tag 0BCY.

theorem hasNormPullbackPower_normPicardData (g : X ⟶ Y) [IsFinite g] (e : ℕ)
    (M : MorphismNorm g e) :
    HasNormPullbackPower g e (normPicardData g e M).picardMap

Stacks.Divisors.exists_normPicardAddMonoidHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormInvertible/TensorAdditive.lean, line 335. The attribute's comment: “the homomorphism of abelian groups”.

The norm descends to a homomorphism of Picard groups.

theorem exists_normPicardAddMonoidHom (f : X ⟶ Y) [IsFinite f] {d : ℕ}
    (N : MorphismNorm f d) :
    ∃ F : X.picardGroup →+ Y.picardGroup,
      ∀ (L : X.Modules) (hL : IsInvertible X.presheaf (structureSheaf X.sheaf).property L),
        F (picardClass X.presheaf (structureSheaf X.sheaf).property L hL) =
          picardClass Y.presheaf (structureSheaf Y.sheaf).property
            (normInvertible f N.toMorphismNormMap L)
            (isInvertible_normInvertible f N.toMorphismNormMap L
              (hasTrivializingTargetCover_of_isFinite_of_isInvertible f L hL))

Tag 0BCZ, a lemma

Tag 0BCZ in the Stacks Project.

Stacks.Divisors.normMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormInvertible/Map.lean, line 571. The attribute's comment: “the norm map”.

The norm of a map of invertible modules. A norm N of degree d on functions along a finite morphism f : X ⟶ Y carries a map φ : L ⟶ L' of invertible 𝒪_X-modules to a map of the norms of L and L'.

noncomputable def normMap :
    normInvertible f N.toMorphismNormMap L ⟶ normInvertible f N.toMorphismNormMap L'

Stacks.Divisors.normMap_generator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormInvertible/Map.lean, line 582. The attribute's comment: “local generator formula”.

In local frames the norm map is multiplication by the norm of the coefficient. If φ carries a frame s of L over f ⁻¹ᵁ U to a times a frame t of L' there, then the norm of φ carries the normed frame of s to N(a) times the normed frame of t. This pins the norm map down rather than merely asserting that some map with the right vanishing locus exists.

theorem normMap_generator (U : Y.Opens)
    (s : GeneratorSections X.toRingedSpace L (f ⁻¹ᵁ U))
    (t : GeneratorSections X.toRingedSpace L' (f ⁻¹ᵁ U)) (a : Γ(X, f ⁻¹ᵁ U))
    (ha : φ.val.app (op (f ⁻¹ᵁ U)) s.val =
      @SMul.smul ((structureSheaf X.sheaf).obj.obj (op (f ⁻¹ᵁ U)))
        (L'.val.obj (op (f ⁻¹ᵁ U))) _ a t.val) :
    (normMap f N L L' φ).val.app (op U)
        (normGenerator f N.toMorphismNormMap L
          (hasTrivializingTargetCover_of_isInvertible f L) U s).val =
      @SMul.smul ((structureSheaf Y.sheaf).obj.obj (op U))
        ((normInvertible f N.toMorphismNormMap L').val.obj (op U)) _ (N.app U a)
        (normGenerator f N.toMorphismNormMap L'
          (hasTrivializingTargetCover_of_isInvertible f L') U t).val

Stacks.Divisors.normMap_zeroAt_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormInvertible/Map.lean, line 603. The attribute's comment: “vanishing locus”.

The norm map vanishes at y exactly when the original map vanishes at some point of the fibre over y: the vanishing locus of the norm of φ is the image of the vanishing locus of φ.

theorem normMap_zeroAt_iff (y : Y) :
    zeroAt (normInvertible f N.toMorphismNormMap L) (normInvertible f N.toMorphismNormMap L')
        (normMap f N L L' φ) y ↔
      ∃ x : X, f x = y ∧ zeroAt L L' φ x

Tag 0BD0, a lemma

Tag 0BD0 in the Stacks Project.

Stacks.Divisors.exists_isAmple_of_morphismNorm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormAmple/Basic.lean, line 95.

Let f : X ⟶ Y be a finite morphism of schemes admitting a norm of degree d ≥ 1. If X has an ample invertible sheaf, then so has Y.

theorem exists_isAmple_of_morphismNorm (f : X ⟶ Y) [IsFinite f] {d : ℕ} (hd : 1 ≤ d)
    (N : MorphismNorm f d) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    (hL : AlgebraicGeometry.Scheme.Modules.IsAmple X L) :
    ∃ (M : Y.Modules) (hM : AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf
        (structureSheafRing Y.toRingedSpace).property M),
      @AlgebraicGeometry.Scheme.Modules.IsAmple Y M hM

Stacks.Divisors.exists_isAmple_of_hasNormOfDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormInvertible/Ample.lean, line 467.

Stacks Project, Tag 0BD0. Let f : X ⟶ Y be a finite morphism of schemes carrying a norm of positive degree. If X has an ample invertible 𝒪_X-module then so does Y: the norm of a sufficiently high tensor power of the given one.

Positivity of the degree is used exactly once, to see that f is surjective; the rest is Stacks.Divisors.exists_isAmple_of_morphismNormMap.

theorem exists_isAmple_of_hasNormOfDegree (f : X ⟶ Y) [IsFinite f] (L : X.Modules)
    [IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L) {d : ℕ} (hd : 0 < d)
    (hN : HasNormOfDegree f d) :
    ∃ (M : Y.Modules) (hM : IsInvertibleModule Y M), @Stacks.Ample.IsAmple Y M hM

Tag 0BD1, a lemma

Tag 0BD1 in the Stacks Project.

Stacks.Divisors.isQuasiAffine_of_isFinite_of_hasNormOfDegree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Norm/QuasiAffine.lean, line 144.

Stacks Project, Tag 0BD1. The target of a finite morphism carrying a norm of positive degree is quasi-affine as soon as its source is.

theorem isQuasiAffine_of_isFinite_of_hasNormOfDegree (f : X ⟶ Y) [IsFinite f]
    [Scheme.IsQuasiAffine X] {d : ℕ} (hd : 0 < d) (hN : HasNormOfDegree f d) :
    Scheme.IsQuasiAffine Y

Stacks.Divisors.isQuasiAffine_of_morphismNorm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormQuasiAffine/Basic.lean, line 46.

Let f : X ⟶ Y be a finite morphism of schemes admitting a norm of degree d ≥ 1. If X is quasi-affine, then so is Y.

public theorem isQuasiAffine_of_morphismNorm (f : X ⟶ Y) [IsFinite f] {d : ℕ} (hd : 1 ≤ d)
    (N : MorphismNorm f d) [X.IsQuasiAffine] : Y.IsQuasiAffine

Tag 0BD2, a lemma

Tag 0BD2 in the Stacks Project.

Stacks.Divisors.finiteLocallyFreeNorm, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Norm/Basic.lean, line 409. The attribute's comment: “the canonical norm”. References: EGA II (6.5.1), “special case”; SGA 3 V (4.1.1), “more general”.

Stacks Project, Tag 0BD2. The canonical determinant norm constructed in the proof, for an arbitrary finite locally free morphism, including varying and zero rank.

Its defining property is finiteLocallyFreeNorm_app_affine_eq_projectiveNorm: on an affine open of the target it is the determinant of multiplication. Taken with the two fields of DeterminantNorm — the determinant formula on affine opens where the algebra is free, and the power law at constant rank — this pins the norm down.

noncomputable def finiteLocallyFreeNorm {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Morphisms.IsFiniteLocallyFree f] : DeterminantNorm f

Stacks.Divisors.finiteLocallyFreeNormOfRank, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Norm/Basic.lean, line 454. The attribute's comment: “the norm of positive constant degree”. References: EGA II (6.5.1), “special case”.

Stacks Project, Tag 0BD2. At positive constant rank d, the canonical determinant norm is a norm of degree d in the sense of the Norms section.

noncomputable def finiteLocallyFreeNormOfRank {X Y : Scheme.{u}} (f : X ⟶ Y) (d : ℕ)
    [Morphisms.IsFiniteLocallyFreeOfRank f d] (_hd : 0 < d) :
    {N : MorphismNorm f d // IsDeterminantNorm N.toMorphismNormMap}

Stacks.Divisors.finiteLocallyFreeNorm_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormBaseChange/Basic.lean, line 64. The attribute's comment: “compatibility with arbitrary base change”.

Stacks Project, Tag 0BD2. Formation of the canonical determinant norm commutes with arbitrary base change, even when the rank is not constant: around a cartesian square the base change f' of a finite locally free morphism f is again finite locally free, and the norm of a section of the structure sheaf pulled back around the square is the pullback of its norm.

theorem finiteLocallyFreeNorm_baseChange
    {X Y X' Y' : Scheme.{u}} (f : X ⟶ Y) (f' : X' ⟶ Y')
    (g' : X' ⟶ X) (g : Y' ⟶ Y)
    [Morphisms.IsFiniteLocallyFree f]
    (sq : IsPullback g' f' f g) :
    ∃ h' : Morphisms.IsFiniteLocallyFree f',
      letI := h'
      ∀ (U : Y.Opens) (s : Γ(X, f ⁻¹ᵁ U)),
        (finiteLocallyFreeNorm f').app (g ⁻¹ᵁ U)
            (g'.appLE (f ⁻¹ᵁ U) (f' ⁻¹ᵁ (g ⁻¹ᵁ U)) (by
              intro x hx
              change f (g' x) ∈ U
              rw [← Scheme.Hom.comp_apply, sq.w, Scheme.Hom.comp_apply]
              exact hx) s) =
          g.app U ((finiteLocallyFreeNorm f).app U s)

Stacks.Divisors.finiteLocallyFreeNormOfRank_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormBaseChange/Rank.lean, line 58. The attribute's comment: “compatibility of the degree-d norm with arbitrary base change”.

Stacks Project, Tag 0BD2. At positive constant rank, arbitrary base change preserves the specified degree and the norm on sections: around a cartesian square the base change f' of a morphism f that is finite locally free of rank d is again finite locally free of rank d, and the degree-d norm of a section of the structure sheaf pulled back around the square is the pullback of its degree-d norm.

theorem finiteLocallyFreeNormOfRank_baseChange
    {X Y X' Y' : Scheme.{u}} (f : X ⟶ Y) (f' : X' ⟶ Y')
    (g' : X' ⟶ X) (g : Y' ⟶ Y) (d : ℕ)
    [Morphisms.IsFiniteLocallyFreeOfRank f d] (hd : 0 < d)
    (sq : IsPullback g' f' f g) :
    ∃ h' : Morphisms.IsFiniteLocallyFreeOfRank f' d,
      letI := h'
      ∀ (U : Y.Opens) (s : Γ(X, f ⁻¹ᵁ U)),
        (finiteLocallyFreeNormOfRank f' d hd).1.app (g ⁻¹ᵁ U)
            (g'.appLE (f ⁻¹ᵁ U) (f' ⁻¹ᵁ (g ⁻¹ᵁ U)) (by
              intro x hx
              change f (g' x) ∈ U
              rw [← Scheme.Hom.comp_apply, sq.w, Scheme.Hom.comp_apply]
              exact hx) s) =
          g.app U ((finiteLocallyFreeNormOfRank f d hd).1.app U s)

Tag 0BD3, a lemma

Tag 0BD3 in the Stacks Project.

Stacks.Divisors.exists_norm_of_finite_surjective_of_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Norm/FunctionFieldDegree.lean, line 551.

Stacks Project, Tag 0BD3. A finite surjective morphism of integral schemes with normal target carries a norm of the function-field extension degree.

theorem exists_norm_of_finite_surjective_of_normal
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f] [Surjective f]
    [IsIntegral X] [IsIntegral Y] [IsNormal Y] :
    ∃ φ : Y.functionField →+* X.functionField,
      (∀ (U : Y.Opens) [Nonempty U] [Nonempty (f ⁻¹ᵁ U)]
        (s : Γ(Y, U)),
        φ (Y.germToFunctionField U s) =
          X.germToFunctionField (f ⁻¹ᵁ U) (f.app U s)) ∧
      (letI : Algebra Y.functionField X.functionField := φ.toAlgebra
       HasNormOfDegree f (Module.finrank Y.functionField X.functionField))

Tag 0BDZ, a lemma

Tag 0BDZ in the Stacks Project.

Stacks.Divisors.exists_normOfDegree_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Norm/Reduction.lean, line 201.

Stacks Project, Tag 0BDZ. On a Noetherian scheme in prime characteristic p a sufficiently high Frobenius power supplies a norm of degree a positive power of p for the canonical morphism from the reduction.

theorem exists_normOfDegree_reduction (X : Scheme.{u}) [IsNoetherian X]
    (p : ℕ) (hp : p.Prime) (hchar : (p : Γ(X, ⊤)) = 0) :
    ∃ e : ℕ, 0 < e ∧
      HasNormOfDegree (Scheme.IdealSheafData.vanishingIdeal (⊤ : Closeds X)).subschemeι
        (p ^ e)

Tag 0BD4, a proposition

Tag 0BD4 in the Stacks Project.

Stacks.Divisors.exists_isAmple_of_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormInvertible/Ample.lean, line 482. The attribute's comment: “finite_locally_free_case”. References: EGA II (6.6.1), “absolute, loc free case”; EGA II (6.6.2), “locally free case”.

Stacks Project, Tag 0BD4, case (1). A finite locally free, finite surjective morphism descends the existence of an ample invertible module. The canonical determinant norm of [Stacks, Tag 0BD2] is available at varying rank, and no constant degree is needed: the degree is what Tag 0BD0 uses to get surjectivity, and here surjectivity is a hypothesis.

theorem exists_isAmple_of_isFiniteLocallyFree (f : X ⟶ Y) [IsFinite f] [Surjective f]
    [Morphisms.IsFiniteLocallyFree f] (L : X.Modules) [IsInvertibleModule X L]
    (hL : Stacks.Ample.IsAmple X L) :
    ∃ (M : Y.Modules) (hM : IsInvertibleModule Y M), @Stacks.Ample.IsAmple Y M hM

Stacks.Divisors.exists_isAmple_of_isAmple_reduction_char_p, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormInvertible/Ample.lean, line 494. The attribute's comment: “reduction_characteristic_p_case”.

Stacks Project, Tag 0BD4, case (3). On a Noetherian scheme of prime characteristic p, an ample invertible module on the reduction descends to an ample invertible module on the scheme: a Frobenius power supplies a norm of degree a positive power of p for the canonical morphism from the reduction ([Stacks, Tag 0BDZ]).

theorem exists_isAmple_of_isAmple_reduction_char_p (Y : Scheme.{u}) [IsNoetherian Y] (p : ℕ)
    (hp : p.Prime) (hchar : (p : Γ(Y, ⊤)) = 0)
    (L : (Scheme.IdealSheafData.vanishingIdeal (⊤ : Closeds Y)).subscheme.Modules)
    [IsInvertibleModule (Scheme.IdealSheafData.vanishingIdeal (⊤ : Closeds Y)).subscheme L]
    (hL : Stacks.Ample.IsAmple
      (Scheme.IdealSheafData.vanishingIdeal (⊤ : Closeds Y)).subscheme L) :
    ∃ (M : Y.Modules) (hM : IsInvertibleModule Y M), @Stacks.Ample.IsAmple Y M hM

Stacks.Divisors.exists_isAmple_of_isIntegral_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NormInvertible/Ample.lean, line 511. The attribute's comment: “integral_normal_case”. References: EGA II (6.6.1), “absolute, Y normal”; EGA II (6.6.2), “Y integral normal”.

Stacks Project, Tag 0BD4, case (2). A finite surjective morphism onto an integral normal scheme descends the existence of an ample invertible module. The source is replaced by an irreducible component dominating the target, viewed as a reduced closed subscheme; that component is integral, so [Stacks, Tag 0BD3] supplies a norm of the function-field degree.

theorem exists_isAmple_of_isIntegral_isNormal {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f]
    [Surjective f] [IsIntegral Y] [IsNormal Y] (L : X.Modules) [IsInvertibleModule X L]
    (hL : Stacks.Ample.IsAmple X L) :
    ∃ (M : Y.Modules) (hM : IsInvertibleModule Y M), @Stacks.Ample.IsAmple Y M hM

Tag 0BD5, a lemma

Tag 0BD5 in the Stacks Project.

Stacks.Divisors.isQuasiAffine_of_isFinite_surjective_of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Norm/QuasiAffineFiniteSurjective.lean, line 132. The attribute's comment: “integral normal target case”.

Stacks Project, Tag 0BD5, case (2). Quasi-affineness descends along a finite surjective morphism onto an integral normal scheme.

theorem isQuasiAffine_of_isFinite_surjective_of_isNormal {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsFinite f] [Surjective f] [IsIntegral Y] [IsNormal Y] [Scheme.IsQuasiAffine X] :
    Scheme.IsQuasiAffine Y

Stacks.Divisors.isQuasiAffine_of_isFiniteLocallyFree_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Norm/QuasiAffineFiniteSurjective.lean, line 176. The attribute's comment: “finite locally free case”.

Stacks Project, Tag 0BD5, case (1). Quasi-affineness descends along a finite locally free surjective morphism.

theorem isQuasiAffine_of_isFiniteLocallyFree_surjective {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsFinite f] [Surjective f] [Morphisms.IsFiniteLocallyFree f] [Scheme.IsQuasiAffine X] :
    Scheme.IsQuasiAffine Y

Sources

• Section 31.18, Tag 0BCX
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Norm.MorphismNorm · Stacks.Divisors.exists_isTrivial_restrict_preimage_of_isFinite · Stacks.Divisors.hasNormPullbackPower_normPicardData · Stacks.Divisors.exists_normPicardAddMonoidHom · Stacks.Divisors.normMap · Stacks.Divisors.normMap_generator · Stacks.Divisors.normMap_zeroAt_iff · Stacks.Divisors.exists_isAmple_of_morphismNorm

Section31.19 Relative effective Cartier divisors#

Section 31.19 of the Stacks Project, Tag 056P. 9 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 056Q, a lemma

Tag 056Q in the Stacks Project.

AlgebraicGeometry.isEffectiveCartierDivisor_comap_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/BaseChangeDivisor.lean, line 123. References: EGA IV (21.15.9), “partial”.

A relative effective Cartier divisor stays effective Cartier under arbitrary base change.

theorem isEffectiveCartierDivisor_comap_pullback {X S S' : Scheme.{u}}
    (f : X ⟶ S) (g : S' ⟶ S) (I : X.IdealSheafData)
    (hI : IsEffectiveCartierDivisor I)
    [Flat (I.subschemeι ≫ f)] :
    IsEffectiveCartierDivisor
      (I.comap (pullback.snd g f))

Tag 062T, a definition

Tag 062T in the Stacks Project.

Stacks.Divisors.IsRelativeEffectiveCartierDivisor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/RelativeEffectiveCartier.lean, line 46.

Stacks Project, Tag 062T. A closed subscheme of X is a relative effective Cartier divisor over S when it is an effective Cartier divisor on X and its structure morphism to S is flat.

abbrev IsRelativeEffectiveCartierDivisor {X S : Scheme.{u}}
    (f : X ⟶ S) (I : X.IdealSheafData) : Prop

Tag 0B8U, a lemma

Tag 0B8U in the Stacks Project.

AlgebraicGeometry.isRelativeEffectiveCartierDivisor_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/RelativeSum.lean, line 204.

Stacks Project, Tag 0B8U. The sum of two relative effective Cartier divisors on X over S is a relative effective Cartier divisor over S.

theorem isRelativeEffectiveCartierDivisor_mul {X S : Scheme.{u}} (f : X ⟶ S)
    (I J : X.IdealSheafData)
    (hI : IsRelativeEffectiveCartierDivisor f I)
    (hJ : IsRelativeEffectiveCartierDivisor f J) :
    IsRelativeEffectiveCartierDivisor f (I * J)

Tag 0B8V, a lemma

Tag 0B8V in the Stacks Project.

Stacks.Divisors.isRelativeEffectiveCartierDivisor_of_mul_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/RelativeDifference.lean, line 288.

Stacks Project, Tag 0B8V. An effective Cartier divisor which is the difference of two relative effective Cartier divisors is itself relative.

theorem isRelativeEffectiveCartierDivisor_of_mul_eq
    {X S : Scheme.{u}} (f : X ⟶ S) (D₁ D₂ E : X.IdealSheafData)
    (hD₁ : IsRelativeEffectiveCartierDivisor f D₁)
    (hD₂ : IsRelativeEffectiveCartierDivisor f D₂)
    (hE : IsEffectiveCartierDivisor E)
    (h : D₂ = D₁ * E) :
    IsRelativeEffectiveCartierDivisor f E

Tag 062U, a lemma

Tag 062U in the Stacks Project.

AlgebraicGeometry.isFlatAt_of_relativeEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/FlatAtDivisor.lean, line 185.

Stacks Project, Tag 062U. The ambient morphism is flat at a point of a relative effective Cartier divisor whose ambient local ring is Noetherian.

theorem isFlatAt_of_relativeEffectiveCartierDivisor
    {X S : Scheme.{u}} (f : X ⟶ S) (I : X.IdealSheafData)
    (hI : IsRelativeEffectiveCartierDivisor f I)
    (x : X) (hx : x ∈ I.supportSet)
    (hNoetherian : IsNoetherianRing (X.presheaf.stalk x)) :
    IsFlatAt f.toLRSHom.toShHom x

Tag 062V, a lemma

Tag 062V in the Stacks Project.

Stacks.AlgebraicGeometry.exists_open_flat_of_isRelativeEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/FlatNeighbourhood.lean, line 538.

A relative effective Cartier divisor lies in an open subscheme on which the ambient morphism is flat, provided that morphism is locally of finite presentation.

theorem exists_open_flat_of_isRelativeEffectiveCartierDivisor
    {X S : Scheme.{u}} (f : X ⟶ S) (I : X.IdealSheafData)
    (hI : Stacks.Divisors.IsRelativeEffectiveCartierDivisor f I)
    [LocallyOfFinitePresentation f] :
    ∃ U : X.Opens, I.supportSet ⊆ (U : Set X) ∧ Flat (U.ι ≫ f)

Tag 062W, a lemma

Tag 062W in the Stacks Project.

AlgebraicGeometry.flat_of_flat_off_relativeEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/FlatOffDivisor.lean, line 214.

A morphism flat away from a relative effective Cartier divisor is flat.

theorem flat_of_flat_off_relativeEffectiveCartierDivisor
    {X S : Scheme.{u}} (f : X ⟶ S) (I : X.IdealSheafData)
    (hI : IsRelativeEffectiveCartierDivisor f I)
    (hf : ∀ x : X, x ∉ I.supportSet →
      IsFlatAt f.toLRSHom.toShHom x) :
    Flat f

Tag 062X, an example

Tag 062X in the Stacks Project.

AlgebraicGeometry.NonflatAmbient.not_flat_ambientRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/NonflatAmbientExample.lean, line 149. The attribute's comment: “ambient ring not flat”.

The ring B is not flat over k[t].

theorem not_flat_ambientRing : ¬ RingHom.Flat (baseMap k)

AlgebraicGeometry.NonflatAmbient.quotientByX_equiv_polynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/NonflatAmbientExample.lean, line 436. The attribute's comment: “quotient by x”.

The quotient B / xB is isomorphic to k[t] by a ring isomorphism carrying the class of t to the coordinate and constants to constants.

theorem quotientByX_equiv_polynomial :
    ∃ e : (ambientRing k ⧸ Ideal.span {x k}) ≃+* Polynomial k,
      e (Ideal.Quotient.mk (Ideal.span {x k}) (t k)) = Polynomial.X ∧
        ∀ a : k,
          e (Ideal.Quotient.mk (Ideal.span {x k})
            (algebraMap k (ambientRing k) a)) = Polynomial.C a

AlgebraicGeometry.NonflatAmbient.quotientByX_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/NonflatAmbientExample.lean, line 508. The attribute's comment: “quotient by x flat”.

The quotient B / xB is flat over k[t].

theorem quotientByX_flat :
    RingHom.Flat
      ((Ideal.Quotient.mk (Ideal.span {x k})).comp (baseMap k))

AlgebraicGeometry.NonflatAmbient.x_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/NonflatAmbientExample.lean, line 531. The attribute's comment: “x nonzerodivisor”.

The element x is a nonzerodivisor of B.

theorem x_isRegular : IsRegular (x k)

AlgebraicGeometry.NonflatAmbient.divisor_isRelativeEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/NonflatAmbientExample.lean, line 593. The attribute's comment: “relative effective Cartier divisor”.

The closed subscheme of Spec B cut out by x is a relative effective Cartier divisor over Spec k[t].

theorem divisor_isRelativeEffectiveCartierDivisor :
    Stacks.Divisors.IsRelativeEffectiveCartierDivisor
      (Spec.map (CommRingCat.ofHom (baseMap k))) (divisor k)

AlgebraicGeometry.NonflatAmbient.no_flat_neighbourhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/NonflatAmbientExample.lean, line 717. The attribute's comment: “no flat neighbourhood”.

No open subscheme of Spec B containing the divisor is flat over Spec k[t].

theorem no_flat_neighbourhood
    (U : (Spec (.of (ambientRing k))).Opens)
    (hU : (divisor k).supportSet ⊆ (U : Set (Spec (.of (ambientRing k))))) :
    ¬ Flat (U.ι ≫ Spec.map (CommRingCat.ofHom (baseMap k)))

Tag 062Y, a lemma

Tag 062Y in the Stacks Project.

Stacks.Divisors.exists_isRelativeEffectiveCartierDivisor_containing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/ContainingDivisorFibre.lean, line 313. The attribute's comment: “local_containing_divisor”.

Let f : X ⟶ S be flat and locally of finite presentation, let Z be a closed subscheme of X and let x be a point of Z whose fibre over f x is an effective Cartier divisor in a neighbourhood of x. Then there is an open neighbourhood U of x carrying a relative effective Cartier divisor D over S with Z ∩ U ⊆ D and Z_{f x} ∩ U = D_{f x}.

theorem exists_isRelativeEffectiveCartierDivisor_containing (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (Z : X.IdealSheafData) (x : X) (hx : x ∈ Z.support)
    (hfib : ∃ N : (f.fiber (f x)).Opens, f.asFiber x ∈ N ∧
      IsEffectiveCartierDivisor ((Z.comap (f.fiberι (f x))).comap N.ι)) :
    ∃ (U : X.Opens) (_ : x ∈ U) (D : U.toScheme.IdealSheafData),
      IsRelativeEffectiveCartierDivisor (U.ι ≫ f) D ∧ D ≤ Z.comap U.ι ∧
        (Z.comap U.ι).comap ((U.ι ≫ f).fiberι (f x)) =
          D.comap ((U.ι ≫ f).fiberι (f x))

Stacks.Divisors.exists_isRelativeEffectiveCartierDivisor_of_flat_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/FlatCartierFibre.lean, line 296. The attribute's comment: “flat_finitely_presented_case”.

Let f : X ⟶ S be flat and locally of finite presentation, let Z be a closed subscheme of X of finite presentation over X and let x be a point of Z at which Z is flat over S and whose fibre over f x is an effective Cartier divisor in a neighbourhood of x. Then Z restricts to a relative effective Cartier divisor over S on an affine open neighbourhood of x.

theorem exists_isRelativeEffectiveCartierDivisor_of_flat_of_finitePresentation (f : X ⟶ S)
    [Flat f] [LocallyOfFinitePresentation f] (Z : X.IdealSheafData)
    [LocallyOfFinitePresentation Z.subschemeι] (x : X) (hx : x ∈ Z.support)
    (hfib : ∃ V : (f.fiber (f x)).Opens, f.asFiber x ∈ V ∧
      IsEffectiveCartierDivisor ((Z.comap (f.fiberι (f x))).comap V.ι))
    (hflat : ((Z.subschemeι ≫ f).stalkMap (⟨x, hx⟩ : Z.subscheme)).hom.Flat) :
    ∃ V : X.Opens, x ∈ V ∧ IsAffineOpen V ∧
      IsRelativeEffectiveCartierDivisor (V.ι ≫ f) (Z.comap V.ι)

Stacks.Divisors.isRelativeEffectiveCartierDivisor_of_flat_of_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/FlatCartierFibre.lean, line 313. The attribute's comment: “flat_fibres_global_case”. References: EGA IV (21.15.3.3), “converse”.

A closed subscheme of a scheme flat and locally of finite presentation over S, itself flat and locally of finite presentation over S, all of whose fibres are effective Cartier divisors, is a relative effective Cartier divisor over S.

theorem isRelativeEffectiveCartierDivisor_of_flat_of_fibres (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (Z : X.IdealSheafData) [Flat (Z.subschemeι ≫ f)]
    [LocallyOfFinitePresentation (Z.subschemeι ≫ f)]
    (hfib : ∀ s : S, IsEffectiveCartierDivisor (Z.comap (f.fiberι s))) :
    IsRelativeEffectiveCartierDivisor f Z

Stacks.Divisors.exists_isRelativeEffectiveCartierDivisor_of_ideal_isPrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/LocallyPrincipalFibre.lean, line 393. The attribute's comment: “locally_principal_case”.

Let f : X ⟶ S be flat and locally of finite presentation, let Z be a closed subscheme of X and let x be a point of Z whose fibre over f x is an effective Cartier divisor in a neighbourhood of x. If the ideal of Z is principal on some affine open neighbourhood of x, then Z restricts to a relative effective Cartier divisor over S on an affine open neighbourhood of x.

theorem exists_isRelativeEffectiveCartierDivisor_of_ideal_isPrincipal (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (Z : X.IdealSheafData) (x : X) (hx : x ∈ Z.support)
    (hprin : ∃ U : X.affineOpens, x ∈ (U : X.Opens) ∧ (Z.ideal U).IsPrincipal)
    (hfib : ∃ V : (f.fiber (f x)).Opens, f.asFiber x ∈ V ∧
      IsEffectiveCartierDivisor ((Z.comap (f.fiberι (f x))).comap V.ι)) :
    ∃ V : X.Opens, x ∈ V ∧ IsAffineOpen V ∧
      IsRelativeEffectiveCartierDivisor (V.ι ≫ f) (Z.comap V.ι)

Stacks.Divisors.isRelativeEffectiveCartierDivisor_of_isLocallyPrincipal_of_fibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/LocallyPrincipalFibre.lean, line 411. The attribute's comment: “locally_principal_global_case”. References: EGA IV (21.15.3.3), “forward direction”.

A locally principal closed subscheme of a scheme flat and locally of finite presentation over S, all of whose fibres are effective Cartier divisors, is a relative effective Cartier divisor over S.

theorem isRelativeEffectiveCartierDivisor_of_isLocallyPrincipal_of_fibres (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (Z : X.IdealSheafData) (hZ : IsLocallyPrincipal Z)
    (hfib : ∀ s : S, IsEffectiveCartierDivisor (Z.comap (f.fiberι s))) :
    IsRelativeEffectiveCartierDivisor f Z

Sources

• Section 31.19, Tag 056P
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isEffectiveCartierDivisor_comap_pullback · Stacks.Divisors.IsRelativeEffectiveCartierDivisor · AlgebraicGeometry.isRelativeEffectiveCartierDivisor_mul · Stacks.Divisors.isRelativeEffectiveCartierDivisor_of_mul_eq · AlgebraicGeometry.isFlatAt_of_relativeEffectiveCartierDivisor · Stacks.AlgebraicGeometry.exists_open_flat_of_isRelativeEffectiveCartierDivisor · AlgebraicGeometry.flat_of_flat_off_relativeEffectiveCartierDivisor · AlgebraicGeometry.NonflatAmbient.not_flat_ambientRing

Section31.20 The normal cone of an immersion#

Section 31.20 of the Stacks Project, Tag 062Z. 8 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0630, a definition

Tag 0630 in the Stacks Project.

Stacks.Conormal.conormalAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalAlgebra/Immersion.lean, line 543. The attribute's comment: “the conormal algebra”. References: EGA IV (16.1.2), “Gr_•(f), immersions”.

The conormal algebra of an immersion, together with its local associated-graded quotient presentations.

noncomputable def conormalAlgebra {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i] :
    ConormalAlgebraData i

Tag 0631, an equation

Tag 0631 in the Stacks Project.

Stacks.Conormal.conormalAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalAlgebra/Immersion.lean, line 543. The attribute's comment: “its degree-n piece: i_* C_{Z/X, n} = I^n/I^{n+1}”. References: EGA IV (16.1.2), “Gr_•(f), immersions”.

The conormal algebra of an immersion, together with its local associated-graded quotient presentations.

noncomputable def conormalAlgebra {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i] :
    ConormalAlgebraData i

Tag 0632, an equation

Tag 0632 in the Stacks Project.

Stacks.Conormal.conormalDegreeOneHom_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/DegreeOne.lean, line 464. The attribute's comment: “degree one: the conormal algebra in degree one is the conormal sheaf”.

[Stacks, Tag 0632]: the conormal algebra in degree one is the conormal sheaf. The canonical morphism 𝒞_{Z/X} ⟶ 𝒞_{Z/X,1} is an isomorphism.

This is the degree-one assertion of the canonical surjection Sym^*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*}: the identification of the degree-one piece of the conormal algebra with the conormal sheaf, which is what makes that surjection an isomorphism in degree one.

theorem conormalDegreeOneHom_isIso (i : Z ⟶ X) [IsImmersion i] :
    IsIso (conormalDegreeOneHom i)

Stacks.Conormal.conormalDegreeOneIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Conormal/DegreeOne.lean, line 478. The attribute's comment: “degree one: the identification as an isomorphism”.

[Stacks, Tag 0632]: the degree-one identification 𝒞_{Z/X} ≅ 𝒞_{Z/X,1}.

noncomputable def conormalDegreeOneIso (i : Z ⟶ X) [IsImmersion i] :
    conormalSheaf i ≅ (conormalAlgebra i).algebra.piece 1

Stacks.Conormal.conormalSymmetricHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/SymmetricQuotient.lean, line 241. The attribute's comment: “the canonical map Sym(C_{Z/X}) → C_{Z/X,} of graded algebras”. References: EGA 0 (19.5.2), “more general”; EGA 0 (22.1.1), “more general”; EGA IV (17.12.1).

Stacks Project, Tag 0632. The canonical map Sym*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*} of graded 𝒪_Z-algebras, the unital homomorphism which is the identity on degree-one generators.

def conormalSymmetricHom (i : Z ⟶ X) [IsImmersion i] :
    SheafOfModules.GradedAlgebra.UnitalHom (conormalSymmetricAlgebra i)
      (conormalAlgebra i).algebra

Stacks.Conormal.conormalSymmetricHom_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/SymmetricQuotient.lean, line 260. The attribute's comment: “uniqueness of the canonical map Sym(C_{Z/X}) → C_{Z/X,}”.

Stacks Project, Tag 0632. A unital homomorphism which is the identity on degree-one generators is the canonical map, so the canonical map is well defined.

theorem conormalSymmetricHom_unique (i : Z ⟶ X) [IsImmersion i]
    {g : SheafOfModules.GradedAlgebra.UnitalHom (conormalSymmetricAlgebra i)
      (conormalAlgebra i).algebra}
    (hg : Scheme.Modules.symmetricAlgebraGen Z ((conormalAlgebra i).algebra.piece 1) ≫
      g.app 1 = 𝟙 ((conormalAlgebra i).algebra.piece 1)) :
    g = conormalSymmetricHom i

Stacks.Conormal.isIso_conormalSymmetricHom_app_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/SymmetricQuotient.lean, line 276. The attribute's comment: “the canonical map Sym(C_{Z/X}) → C_{Z/X,} is an isomorphism in degree 1”.

Stacks Project, Tag 0632. The canonical map Sym*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*} is an isomorphism in degree one. The degree-one generator 𝒞_{Z/X} ⟶ Sym¹(𝒞_{Z/X}) is an isomorphism, and the canonical map is the identity on it.

theorem isIso_conormalSymmetricHom_app_one (i : Z ⟶ X) [IsImmersion i] :
    IsIso ((conormalSymmetricHom i).app 1)

Stacks.Conormal.isIso_conormalSymmetricHom_app_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/SymmetricQuotient.lean, line 408. The attribute's comment: “the canonical map Sym(C_{Z/X}) → C_{Z/X,} is an isomorphism in degree 0”.

Stacks Project, Tag 0632. The canonical map Sym*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*} is an isomorphism in degree zero. It is a monomorphism because both degree-zero pieces are generated by their graded units, freely on the source and without torsion on the target, and an epimorphism because on an affine closed-immersion chart every degree-zero section of the target is a multiple of the unit.

theorem isIso_conormalSymmetricHom_app_zero (i : Z ⟶ X) [IsImmersion i] :
    IsIso ((conormalSymmetricHom i).app 0)

Stacks.Conormal.epi_conormalSymmetricHom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/SymmetricQuotient.lean, line 521. The attribute's comment: “the canonical map Sym(C_{Z/X}) → C_{Z/X,} is surjective”.

Stacks Project, Tag 0632. The canonical map Sym*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*} is surjective: an epimorphism of sheaves of modules in every degree. In a negative degree the target vanishes, and in a nonnegative degree the map is locally surjective, because over an affine closed-immersion chart ℐⁿ/ℐⁿ⁺¹ is generated by products of n sections of ℐ.

theorem epi_conormalSymmetricHom_app (i : Z ⟶ X) [IsImmersion i] (n : ℤ) :
    Epi ((conormalSymmetricHom i).app n)

Tag 0633, a lemma

Tag 0633 in the Stacks Project.

Stacks.Conormal.conormalAlgebra_identifications, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/ConormalInverseImage.lean, line 311. The attribute's comment: “part (1)”.

Let i : Z ⟶ X be an immersion and U ⊆ X an open subscheme such that i(Z) ⊆ U is a closed subset of U; let ℐ ⊆ 𝒪_U be the quasi-coherent ideal sheaf of the closed subscheme i(Z) ⊂ U. Then 𝒞_{Z/X,*} = i^*(⨁_{n ≥ 0} ℐⁿ) = i^{-1}(⨁_{n ≥ 0} ℐⁿ/ℐⁿ⁺¹): * the conormal algebra is isomorphic to i^*(⨁ₙ ℐⁿ) as sheaves of graded 𝒪_Z-algebras, the isomorphism carrying the unit to the unit; * the topological inverse image i^{-1}(⨁ₙ ℐⁿ/ℐⁿ⁺¹), a sheaf of graded i^{-1}𝒪_U-algebras, is isomorphic to the conormal algebra read over i^{-1}𝒪_U along the structure map i^{-1}𝒪_U ⟶ 𝒪_Z, as sheaves of graded algebras, the isomorphism carrying the unit to the unit.

The isomorphisms are Stacks.Conormal.conormalIsoReesPullback and Stacks.Conormal.inverseImageGrIsoConormal.

theorem conormalAlgebra_identifications :
    (∃ e : (conormalAlgebra i).algebra ≅ openReesPullback i U hsub, ∀ W : Z.Opens,
      (e.hom.app 0).val.app (op W) ((conormalAlgebra i).algebra.one.eval (op W)) =
        (openReesPullback i U hsub).one.eval (op W)) ∧
    (∃ e : inverseImageGradedAlgebra (openLift i U hsub).base (U.toScheme).sheaf
          (grGradedAlgebra (openIdeal i U hsub)) ≅
        SheafOfModules.GradedAlgebra.scalarRestrict (openStructureMap i U hsub)
          (conormalAlgebra i).algebra, ∀ W : Z.Opens,
      (e.hom.app 0).val.app (op W)
          ((inverseImageGradedAlgebra (openLift i U hsub).base (U.toScheme).sheaf
            (grGradedAlgebra (openIdeal i U hsub))).one.eval (op W)) =
        (conormalAlgebra i).algebra.one.eval (op W))

AlgebraicGeometry.affineSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/ConormalSections.lean, line 183. The attribute's comment: “conormal_algebra_affine_sections”.

The homogeneous sections of the conormal algebra on an affine closed-immersion chart are canonically the quotients I^n/I^(n+1), compatibly with multiplication, unit, and scalars.

noncomputable def affineSectionsEquiv {Z X : Scheme.{u}} (i : Z ⟶ X)
    [IsImmersion i] (U : X.affineOpens)
    (hU : IsClosedImmersion (i.resLE U.1 (i ⁻¹ᵁ U.1) le_rfl)) :
    AffineSectionsEquiv i U hU

AlgebraicGeometry.conormalAlgebra_on_closed_open, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/ConormalSections.lean, line 543. The attribute's comment: “conormal_algebra_on_closed_open”.

Both canonical identifications of the conormal algebra on an open where the immersion is closed.

noncomputable def conormalAlgebra_on_closed_open
    {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
    (U : X.Opens)
    (hU : IsClosed (Set.range (i.resLE U (i ⁻¹ᵁ U) le_rfl))) :
    ClosedOpenIdentifications i U

Tag 0634, a lemma

Tag 0634 in the Stacks Project.

AlgebraicGeometry.conormalAlgebraHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/Functoriality/ConormalAlgebraHom.lean, line 603.

Stacks Project, Tag 0634. The unique morphism of conormal graded algebras over a commutative square of immersions is induced on every affine closed-immersion chart by the ring map on ideal-power quotients.

noncomputable def conormalAlgebraHom {Z X Z' X' : Scheme.{u}}
    (i : Z ⟶ X) (i' : Z' ⟶ X') (f : Z ⟶ Z') (g : X ⟶ X')
    [IsImmersion i] [IsImmersion i'] (comm : f ≫ i' = i ≫ g) :
    CanonicalConormalAlgebraHom i i' f g

Tag 0635, a lemma

Tag 0635 in the Stacks Project.

AlgebraicGeometry.conormalAlgebraMap_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/BaseChange.lean, line 834. The attribute's comment: “surjectivity”.

The canonical map on each homogeneous piece of the conormal algebra is locally surjective for a cartesian square of immersions.

theorem conormalAlgebraMap_epi {Z X Z' X' : Scheme.{u}}
    (i : Z ⟶ X) (i' : Z' ⟶ X') (f : Z ⟶ Z') (g : X ⟶ X')
    [IsImmersion i] [IsImmersion i'] (sq : IsPullback i f g i') (n : ℤ) :
    Epi ((canonicalPullbackHom i i' f g sq.w.symm).hom n)

AlgebraicGeometry.conormalAlgebraMap_isIso_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/BaseChange.lean, line 1152. The attribute's comment: “flat isomorphism”.

Under flat base change the canonical map on every homogeneous piece is an isomorphism.

theorem conormalAlgebraMap_isIso_of_flat {Z X Z' X' : Scheme.{u}}
    (i : Z ⟶ X) (i' : Z' ⟶ X') (f : Z ⟶ Z') (g : X ⟶ X')
    [IsImmersion i] [IsImmersion i'] [Flat g]
    (sq : IsPullback i f g i') (n : ℤ) :
    IsIso ((canonicalPullbackHom i i' f g sq.w.symm).hom n)

Tag 0636, a definition

Tag 0636 in the Stacks Project.

Stacks.Conormal.normalBundle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/NormalBundle.lean, line 112. The attribute's comment: “the normal bundle N_ZX = Spec_Z(Sym(C_{Z/X}))”.

Stacks Project, Tag 0636. The normal bundle N_ZX = Spec_Z(Sym(𝒞_{Z/X})) of an immersion i : Z ⟶ X: the relative spectrum over Z of the symmetric algebra on the conormal sheaf 𝒞_{Z/X} = 𝒞_{Z/X,1}, that is, the vector bundle of Tag 01M2 associated to 𝒞_{Z/X}.

def normalBundle : Scheme.{u}

Stacks.Conormal.normalBundleVectorBundle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/NormalBundle.lean, line 145. The attribute's comment: “N_ZX is a vector bundle over Z in the sense of 062M”.

Stacks Project, Tag 0636. N_ZX is a vector bundle over Z in the sense of Tag 062M: it is the vector bundle 𝐕(𝒞_{Z/X}) of Tag 01M2 attached to the conormal sheaf, the relative spectrum of Sym(𝒞_{Z/X}) graded by the symmetric powers Symⁿ(𝒞_{Z/X}).

def normalBundleVectorBundle : VectorBundle Z

Stacks.Conormal.normalConeCone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/NormalBundle.lean, line 216. The attribute's comment: “C_ZX is a cone over Z in the sense of 062R”.

Stacks Project, Tag 0636. C_ZX is a cone over Z in the sense of Tag 062R: it is affine over Z, and the homogeneous pieces 𝒞_{Z/X,n} of the conormal algebra decompose the direct image of its structure sheaf — uniquely over every open, locally surjectively, and multiplicatively — with the degree-zero piece the structure sheaf of Z.

def normalConeCone : AbstractCone Z

Declarations registered for the tag:

• Stacks.Conormal.normalCone, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/NormalBundle.lean, line 253 (StacksFrontier): “the normal cone C_ZX = Spec_Z(C_{Z/X,*})”.

Tag 0637, an equation

Tag 0637 in the Stacks Project.

Stacks.Conormal.normalConeToNormalBundle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/NormalConeInNormalBundle.lean, line 241. The attribute's comment: “the canonical surjection of graded algebras defines a morphism C_ZX → N_ZX”.

Stacks Project, Tag 0637. The canonical morphism C_ZX ⟶ N_ZX from the normal cone to the normal bundle of an immersion, defined by the canonical map Sym*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*} of graded algebras of Tag 0632: it is the morphism of relative spectra attached to that map of algebra sheaves, and Stacks.Conormal.ι_normalConeToNormalBundle is its characterising property.

def normalConeToNormalBundle :
    normalCone i ⟶ Scheme.Modules.vectorBundle Z (conormalSheafDegreeOne i)

Stacks.Conormal.normalConeToNormalBundle_toBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalCone/NormalConeInNormalBundle.lean, line 250. The attribute's comment: “the morphism C_ZX → N_ZX is a morphism over Z”.

Stacks Project, Tag 0637. The canonical morphism C_ZX ⟶ N_ZX is a morphism of schemes over Z: it carries the projection of the normal bundle to the projection of the normal cone.

theorem normalConeToNormalBundle_toBase :
    normalConeToNormalBundle i ≫
        Scheme.Modules.vectorBundleToBase Z (conormalSheafDegreeOne i) =
      normalConeToBase i

Sources

• Section 31.20, Tag 062Z
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Conormal.conormalAlgebra · Stacks.Conormal.conormalDegreeOneHom_isIso · Stacks.Conormal.conormalDegreeOneIso · Stacks.Conormal.conormalSymmetricHom · Stacks.Conormal.conormalSymmetricHom_unique · Stacks.Conormal.isIso_conormalSymmetricHom_app_one · Stacks.Conormal.isIso_conormalSymmetricHom_app_zero · Stacks.Conormal.epi_conormalSymmetricHom_app

Section31.21 Regular ideal sheaves#

Section 31.21 of the Stacks Project, Tag 067M. 11 tags here are carried by 31 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0639, an equation

Tag 0639 in the Stacks Project.

AlgebraicGeometry.regularSequenceMultiplication, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/RegularIdealSheaves.lean, line 330.

Stacks Project, Tag 0639. Multiplication by f i on O_X/(f₀, …, f_{i-1}), for an arbitrary ringed space.

public noncomputable def regularSequenceMultiplication
    (X : RingedSpace.{u, v}) {n : ℕ}
    (f : Fin n → X.presheaf.obj (op (⊤ : Opens X))) (i : Fin n) :
    RegularSequenceMultiplicationData X f i

Tag 063A, an equation

Tag 063A in the Stacks Project.

Declarations registered for the tag:

• Stacks.AlgebraicGeometry.SeqKoszul.sheafComplex, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/QuasiRegular/SectionKoszulComplex.lean, line 22 (StacksFrontier): “the notation K_•(O_X, f_•) of the section on regular ideal sheaves: the Koszul complex of Modules, Definition 17.24.2 (Tag 062L) for the structure sheaf of a ringed space and a finite family of its global sections.”.

Tag 063B, an equation

Tag 063B in the Stacks Project.

Stacks.AlgebraicGeometry.QuasiRegular.quasiRegularMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiRegular/Basic.lean, line 500.

The canonical morphism of sheaves (O_X / J)[T₁, ..., Tᵣ] ⟶ ⨁ d, J^d / J^(d+1) associated to global sections f₁, ..., fᵣ, sending Tᵢ to fᵢ mod J².

noncomputable def quasiRegularMap (X : RingedSpace.{u}) {r : ℕ}
    (f : Fin r → X.presheaf.obj (op (⊤ : Opens X))) : QuasiRegularMapData X f

Tag 063C, a lemma

Tag 063C in the Stacks Project.

Stacks.AlgebraicGeometry.SeqKoszul.isH1RegularSequence_of_isKoszulRegularSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Koszul/Sheaf/Regular.lean, line 77. The attribute's comment: “Koszul-regular implies H₁-regular”. References: EGA IV (19.5.1), “b) => b')”.

Stacks Project, Tag 063C. A Koszul-regular sequence is H₁-regular: degree 1 is one of the positive degrees in which the Koszul complex of a Koszul-regular sequence is acyclic.

theorem isH1RegularSequence_of_isKoszulRegularSequence
    (h : IsKoszulRegularSequence X f) : IsH1RegularSequence X f

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularSequence_of_regularSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/Implications.lean, line 205. The attribute's comment: “regular implies Koszul-regular”. References: EGA IV (19.5.1), “a) => b)”.

A regular sequence of global sections of the structure sheaf is a Koszul-regular sequence: if multiplication by f i on O_X/(f₁, …, f_{i-1}) is an injective map of sheaves for every i, then the Koszul complex K_•(O_X, f_•) is acyclic in positive degrees.

theorem isKoszulRegularSequence_of_regularSequence {r : ℕ}
    (f : Fin r → X.presheaf.obj (op (⊤ : Opens X)))
    (hf : ∀ i : Fin r, Mono (regularSequenceMultiplication X f i).multiplication) :
    SeqKoszul.IsKoszulRegularSequence X f

Stacks.AlgebraicGeometry.RegularIdealSheaf.isIso_quasiRegularMap_of_isH1RegularSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/Implications.lean, line 217. The attribute's comment: “H₁-regular implies quasi-regular”.

For an H₁-regular sequence of global sections the quasi-regularity morphism of Stacks tag 063B is an isomorphism, i.e. the sequence is quasi-regular.

theorem isIso_quasiRegularMap_of_isH1RegularSequence {r : ℕ}
    (f : Fin r → X.presheaf.obj (op (⊤ : Opens X)))
    (h : SeqKoszul.IsH1RegularSequence X f) : IsIso (quasiRegularMap X f).hom

Tag 063D, a definition

Tag 063D in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.IsQuasiRegularIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Basic.lean, line 132. The attribute's comment: “part (4): quasi-regular ideal sheaf”. References: EGA IV (16.9.1), “quasi-regular”.

The local quasi-regularity condition of Stacks tag 063D, part (4). The ideal sheaf J is quasi-regular when, near every point of the support of O_X / J, it is generated by a sequence whose sheaf quasi-regularity map of Stacks tag 063B is an isomorphism.

def IsQuasiRegularIdealSheaf (X : RingedSpace.{u})
    (J : (structureSheafModule X).Submodule) : Prop

Stacks.AlgebraicGeometry.RegularIdealSheaf.IsRegularIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Regular.lean, line 134. The attribute's comment: “part (1): regular ideal sheaf”.

Stacks tag 063D, part (1). The ideal sheaf J is regular when, near every point of the support of O_X/J, it is generated by a regular sequence of sections.

def IsRegularIdealSheaf (X : RingedSpace.{u}) (J : (structureSheafModule X).Submodule) : Prop

Stacks.AlgebraicGeometry.RegularIdealSheaf.IsKoszulRegularIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Regular.lean, line 143. The attribute's comment: “part (2): Koszul-regular ideal sheaf”. References: SGA 6 VII (1.4), “regular ideal J”.

Stacks tag 063D, part (2). The ideal sheaf J is Koszul-regular when, near every point of the support of O_X/J, it is generated by a sequence whose Koszul complex is acyclic in positive degrees.

def IsKoszulRegularIdealSheaf (X : RingedSpace.{u})
    (J : (structureSheafModule X).Submodule) : Prop

Stacks.AlgebraicGeometry.RegularIdealSheaf.IsH1RegularIdealSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Regular.lean, line 153. The attribute's comment: “part (3): H₁-regular ideal sheaf”.

Stacks tag 063D, part (3). The ideal sheaf J is H₁-regular when, near every point of the support of O_X/J, it is generated by a sequence whose Koszul complex is exact in degree 1.

def IsH1RegularIdealSheaf (X : RingedSpace.{u})
    (J : (structureSheafModule X).Submodule) : Prop

Tag 063E, a lemma

Tag 063E in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularIdealSheaf_of_isRegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/Implications.lean, line 238. The attribute's comment: “regular implies Koszul-regular”.

A regular ideal sheaf is Koszul-regular. One implication of Stacks tag 063E, between parts (1) and (2) of Stacks tag 063D.

theorem isKoszulRegularIdealSheaf_of_isRegularIdealSheaf (h : IsRegularIdealSheaf X J) :
    IsKoszulRegularIdealSheaf X J

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularIdealSheaf_of_isH1RegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/Implications.lean, line 247. The attribute's comment: “H₁-regular implies quasi-regular”.

An H₁-regular ideal sheaf is quasi-regular. One implication of Stacks tag 063E, between parts (3) and (4) of Stacks tag 063D.

theorem isQuasiRegularIdealSheaf_of_isH1RegularIdealSheaf (h : IsH1RegularIdealSheaf X J) :
    IsQuasiRegularIdealSheaf X J

Stacks.AlgebraicGeometry.RegularIdealSheaf.IsKoszulRegularIdealSheaf.isH1RegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Regular.lean, line 162. The attribute's comment: “Koszul-regular implies H₁-regular”.

Stacks Project, Tag 063E. A Koszul-regular ideal sheaf is H₁-regular: the local witnesses are the same sequences, and degree 1 is a positive degree.

theorem IsKoszulRegularIdealSheaf.isH1RegularIdealSheaf {X : RingedSpace.{u}}
    {J : (structureSheafModule X).Submodule} (h : IsKoszulRegularIdealSheaf X J) :
    IsH1RegularIdealSheaf X J

Tag 063H, a lemma

Tag 063H in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_isGeneratedByOn_of_isFiniteType_of_le_sup_sq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiRegular/StalkGenerators.lean, line 324. The attribute's comment: “the Nakayama and shrinking step of the proof only: sections of a finite-type J whose germs generate J_x/J_x² generate J near x. The characterization itself is Stacks.AlgebraicGeometry.RegularIdealSheaf.Conormal.isQuasiRegularIdealSheaf_iff.”.

The Nakayama and shrinking step in the proof of Stacks tag 063H. Let J ⊆ O_X be a sheaf of ideals of finite type on a locally ringed space and let x be a point of the support of O_X / J. Sections f₁, …, f_r of J over a neighbourhood U of x whose germs generate J_x modulo J_x² generate J on a neighbourhood of x.

theorem exists_isGeneratedByOn_of_isFiniteType_of_le_sup_sq
    (hJ : SheafOfModules.IsFiniteType.{u, u, u} J.toSheafOfModules) {x : X}
    (hne : stalkIdeal J x ≠ ⊤) {U : Opens X} (hxU : x ∈ U) {r : ℕ}
    (f : Fin r → X.presheaf.obj (op U)) (hf : ∀ i, f i ∈ J.obj (op U))
    (hle : stalkIdeal J x
      ≤ Jid (germFamily X.toRingedSpace U f x hxU) ⊔ stalkIdeal J x ^ 2) :
    ∃ (V : Opens X) (_ : x ∈ V) (hVU : V ≤ U),
      IsGeneratedByOn X.toRingedSpace J V
        (fun i => X.presheaf.map (homOfLE hVU).op (f i))

Stacks.AlgebraicGeometry.RegularIdealSheaf.Conormal.isQuasiRegularIdealSheaf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Characterization/IndependentGenerators.lean, line 747. The attribute's comment: “both directions of the characterization: quasi-regular iff of finite type, with finite locally free conormal sheaf and isomorphic symmetric-power-to-graded maps”. References: EGA IV (16.9.4); EGA IV (17.12.1), “more general”.

Stacks Project, Tag 063H. A sheaf of ideals is quasi-regular if and only if it is of finite type, has finite locally free conormal sheaf, and has isomorphic canonical symmetric-power-to-associated-graded maps in every degree.

public theorem isQuasiRegularIdealSheaf_iff (X : LocallyRingedSpace.{u})
    (J : (Stacks.RingedSpace.structureSheafModule X.toRingedSpace).Submodule) :
    IsQuasiRegularIdealSheaf X.toRingedSpace J ↔
      (J.toSheafOfModules.IsFiniteType ∧
        AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree (conormalSheaf X.toRingedSpace J) ∧
        ∀ n : ℕ, IsIso (conormalSymmetricToGradedMap X.toRingedSpace J n))

Tag 067N, a lemma

Tag 067N in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_quasiRegular_generators_of_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Generators.lean, line 421. The attribute's comment: “(1)”. References: EGA IV (16.9.5), “(b') => (a)”.

Stacks Project, Tag 067N, part (1). Let J be a quasi-regular ideal sheaf on a locally ringed space X, let x ∈ X and let f₁, …, f_r ∈ J_x be germs whose classes form a basis of the cotangent fibre J_x / 𝔪_x J_x. Then there is an open neighbourhood U of x on which the f_i are the germs of sections of J which form a quasi-regular sequence generating J over U.

theorem exists_quasiRegular_generators_of_basis (x : X) {r : ℕ}
    (f : Fin r → Stacks.RingedSpace.stalkIdeal J x)
    (b : Module.Basis (Fin r)
      (X.presheaf.stalk x ⧸ IsLocalRing.maximalIdeal (X.presheaf.stalk x))
      (Stacks.RingedSpace.idealCotangentFiber J x))
    (hf : ∀ i, b i = Submodule.Quotient.mk (f i))
    (hJ : IsQuasiRegularIdealSheaf X.toRingedSpace J) :
    ∃ (U : Opens X) (hxU : x ∈ U) (fU : Fin r → J.obj (op U)),
      (∀ i, X.presheaf.germ U x hxU (fU i).1 = (f i).1) ∧
      IsIso (quasiRegularMap (X.toRingedSpace.restrict U.isOpenEmbedding)
        (fun i => sectionOnRestriction X.toRingedSpace U (fU i).1)).hom ∧
      IsGeneratedByOn X.toRingedSpace J U (fun i => (fU i).1)

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_h1Regular_generators_of_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Generators.lean, line 449. The attribute's comment: “(2)”.

Stacks Project, Tag 067N, part (2). The H₁-regular case: for an H₁-regular ideal sheaf the sections produced over U have a Koszul complex which is germwise exact in degree 1.

theorem exists_h1Regular_generators_of_basis (x : X) {r : ℕ}
    (f : Fin r → Stacks.RingedSpace.stalkIdeal J x)
    (b : Module.Basis (Fin r)
      (X.presheaf.stalk x ⧸ IsLocalRing.maximalIdeal (X.presheaf.stalk x))
      (Stacks.RingedSpace.idealCotangentFiber J x))
    (hf : ∀ i, b i = Submodule.Quotient.mk (f i))
    (hJ : IsH1RegularIdealSheaf X.toRingedSpace J) :
    ∃ (U : Opens X) (hxU : x ∈ U) (fU : Fin r → J.obj (op U)),
      (∀ i, X.presheaf.germ U x hxU (fU i).1 = (f i).1) ∧
      IsKoszulSequenceExactOn X.toRingedSpace U (fun i => (fU i).1) (fun j => j = 1) ∧
      IsGeneratedByOn X.toRingedSpace J U (fun i => (fU i).1)

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_koszulRegular_generators_of_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Generators.lean, line 475. The attribute's comment: “(3)”.

Stacks Project, Tag 067N, part (3). The Koszul-regular case: for a Koszul-regular ideal sheaf the sections produced over U have a Koszul complex which is germwise exact in every positive degree.

theorem exists_koszulRegular_generators_of_basis (x : X) {r : ℕ}
    (f : Fin r → Stacks.RingedSpace.stalkIdeal J x)
    (b : Module.Basis (Fin r)
      (X.presheaf.stalk x ⧸ IsLocalRing.maximalIdeal (X.presheaf.stalk x))
      (Stacks.RingedSpace.idealCotangentFiber J x))
    (hf : ∀ i, b i = Submodule.Quotient.mk (f i))
    (hJ : IsKoszulRegularIdealSheaf X.toRingedSpace J) :
    ∃ (U : Opens X) (hxU : x ∈ U) (fU : Fin r → J.obj (op U)),
      (∀ i, X.presheaf.germ U x hxU (fU i).1 = (f i).1) ∧
      IsKoszulSequenceExactOn X.toRingedSpace U (fun i => (fU i).1) (fun j => 0 < j) ∧
      IsGeneratedByOn X.toRingedSpace J U (fun i => (fU i).1)

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_koszulRegular_sections_of_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/ConormalPermanence.lean, line 166. The attribute's comment: “part (3), with the local witness at x in place of Koszul-regularity of J, and assuming J_x is not the whole local ring”. References: SGA 6 VII (1.4), “1.4.2”.

[Stacks Project, Tag 067N] part (3). Let J be an ideal subsheaf of the structure sheaf of a locally ringed space, generated on a neighbourhood of x by a sequence that is Koszul-regular at every point. Then any lift of a basis of the cotangent fibre J_x/𝔪_x J_x is realised on a neighbourhood of x by sections that generate J and are Koszul-regular at every point.

Koszul-regularity of a family on an open is taken germwise, which isKoszulSequenceExactOn_iff_forall_germ_isKoszulRegular identifies with exactness of its sheaf Koszul complex.

Two departures from the source. The hypothesis is the local witness at x that Koszul-regularity of J supplies there, rather than Koszul-regularity of J itself; that is weaker, so a caller with the source's hypothesis can supply it. And J_x ≠ 𝒪_{X,x} is assumed, which the source does not assume: in the excluded case the cotangent fibre is the residue field, so r = 1 and f 0 is a unit, and the source's conclusion holds there too.

theorem exists_koszulRegular_sections_of_basis {X : LocallyRingedSpace.{u}}
    (J : (structureSheafModule X.toRingedSpace).Submodule) (x : X) {r : ℕ}
    (f : Fin r → stalkIdeal J x)
    (b : Module.Basis (Fin r)
      (X.presheaf.stalk x ⧸ IsLocalRing.maximalIdeal (X.presheaf.stalk x))
      (idealCotangentFiber J x))
    (hf : ∀ i, b i = Submodule.Quotient.mk (f i))
    (hsupp : stalkIdeal J x ≠ ⊤)
    (V : Opens X) (hxV : x ∈ V) {s : ℕ} (g : Fin s → X.presheaf.obj (op V))
    (hgen : IsGeneratedByOn X.toRingedSpace J V g)
    (hK : ∀ (y : X) (hy : y ∈ V), Koszul.IsKoszulRegular (germFamily X.toRingedSpace V g y hy)) :
    ∃ (U : Opens X) (hxU : x ∈ U) (fU : Fin r → X.presheaf.obj (op U)),
      (∀ i, X.presheaf.germ U x hxU (fU i) = (f i : X.presheaf.stalk x)) ∧
      IsGeneratedByOn X.toRingedSpace J U fU ∧
      ∀ (y : X) (hy : y ∈ U), Koszul.IsKoszulRegular (germFamily X.toRingedSpace U fU y hy)

Tag 063F, a lemma

Tag 063F in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isFiniteType_of_isRegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Relative/RegularIdealSheafFiniteType.lean, line 373. The attribute's comment: “finite type for regular ideal sheaves”.

Stacks Project, Tag 063F. A regular ideal sheaf on a scheme is of finite type.

theorem isFiniteType_of_isRegularIdealSheaf (hJ : IsRegularIdealSheaf X.toRingedSpace J) :
    J.toSheafOfModules.IsFiniteType

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasicoherent_of_isRegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Relative/RegularIdealSheafFiniteType.lean, line 381. The attribute's comment: “quasi-coherence for regular ideal sheaves”.

Stacks Project, Tag 063F. A regular ideal sheaf on a scheme is quasi-coherent.

theorem isQuasicoherent_of_isRegularIdealSheaf (hJ : IsRegularIdealSheaf X.toRingedSpace J) :
    J.toSheafOfModules.IsQuasicoherent

Stacks.AlgebraicGeometry.RegularIdealSheaf.isFiniteType_of_isKoszulRegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Relative/RegularIdealSheafFiniteType.lean, line 387. The attribute's comment: “finite type for Koszul-regular ideal sheaves”.

Stacks Project, Tag 063F. A Koszul-regular ideal sheaf on a scheme is of finite type.

theorem isFiniteType_of_isKoszulRegularIdealSheaf
    (hJ : IsKoszulRegularIdealSheaf X.toRingedSpace J) :
    J.toSheafOfModules.IsFiniteType

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasicoherent_of_isKoszulRegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Relative/RegularIdealSheafFiniteType.lean, line 396. The attribute's comment: “quasi-coherence for Koszul-regular ideal sheaves”.

Stacks Project, Tag 063F. A Koszul-regular ideal sheaf on a scheme is quasi-coherent.

theorem isQuasicoherent_of_isKoszulRegularIdealSheaf
    (hJ : IsKoszulRegularIdealSheaf X.toRingedSpace J) :
    J.toSheafOfModules.IsQuasicoherent

Stacks.AlgebraicGeometry.RegularIdealSheaf.isFiniteType_of_isH1RegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Relative/RegularIdealSheafFiniteType.lean, line 403. The attribute's comment: “finite type for H₁-regular ideal sheaves”.

Stacks Project, Tag 063F. An H₁-regular ideal sheaf on a scheme is of finite type.

theorem isFiniteType_of_isH1RegularIdealSheaf (hJ : IsH1RegularIdealSheaf X.toRingedSpace J) :
    J.toSheafOfModules.IsFiniteType

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasicoherent_of_isH1RegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Relative/RegularIdealSheafFiniteType.lean, line 411. The attribute's comment: “quasi-coherence for H₁-regular ideal sheaves”.

Stacks Project, Tag 063F. An H₁-regular ideal sheaf on a scheme is quasi-coherent.

theorem isQuasicoherent_of_isH1RegularIdealSheaf (hJ : IsH1RegularIdealSheaf X.toRingedSpace J) :
    J.toSheafOfModules.IsQuasicoherent

Stacks.AlgebraicGeometry.RegularIdealSheaf.isFiniteType_of_isQuasiRegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Relative/RegularIdealSheafFiniteType.lean, line 417. The attribute's comment: “finite type for quasi-regular ideal sheaves”.

Stacks Project, Tag 063F. A quasi-regular ideal sheaf on a scheme is of finite type.

theorem isFiniteType_of_isQuasiRegularIdealSheaf
    (hJ : IsQuasiRegularIdealSheaf X.toRingedSpace J) :
    J.toSheafOfModules.IsFiniteType

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasicoherent_of_isQuasiRegularIdealSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Relative/RegularIdealSheafFiniteType.lean, line 426. The attribute's comment: “quasi-coherence for quasi-regular ideal sheaves”.

Stacks Project, Tag 063F. A quasi-regular ideal sheaf on a scheme is quasi-coherent.

theorem isQuasicoherent_of_isQuasiRegularIdealSheaf
    (hJ : IsQuasiRegularIdealSheaf X.toRingedSpace J) :
    J.toSheafOfModules.IsQuasicoherent

Tag 063G, a lemma

Tag 063G in the Stacks Project.

Stacks.AlgebraicGeometry.H1RegularIdealSheaf.isH1RegularIdealSheaf_iff_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/H1RegularIdealSheaf/Affine.lean, line 120. The attribute's comment: “h1_regular”.

Stacks Project, Tag 063G (h1_regular). A sheaf of ideals on a scheme is H₁-regular if and only if, around each point of the support of its quotient, it is generated on an affine open by a sequence which is H₁-regular in the ring of sections of that open.

theorem isH1RegularIdealSheaf_iff_affine (X : Scheme.{u})
    (J : (structureSheafModule X.toRingedSpace).Submodule) :
    IsH1RegularIdealSheaf X.toRingedSpace J ↔
      ∀ x : X, x ∈ idealQuotientSupport X.toRingedSpace J →
        ∃ (U : X.affineOpens) (_hx : x ∈ (U : Set X)) (r : ℕ) (f : Fin r → Γ(X, U.1)),
          IsGeneratedByOn X.toRingedSpace J U.1 f ∧ Koszul.IsH1Regular f

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularIdealSheaf_iff_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/KoszulRegularIdealSheaf/Stalkwise.lean, line 104. The attribute's comment: “koszul_regular”.

Stacks Project, Tag 063G (koszul_regular). A sheaf of ideals on a scheme is Koszul-regular if and only if, around each point of the support of its quotient, it is generated on an affine open by a sequence which is Koszul-regular in the ring of sections of that open.

theorem isKoszulRegularIdealSheaf_iff_affine (X : Scheme.{u})
    (J : (structureSheafModule X.toRingedSpace).Submodule) :
    IsKoszulRegularIdealSheaf X.toRingedSpace J ↔
      ∀ x : X, x ∈ idealQuotientSupport X.toRingedSpace J →
        ∃ (U : X.affineOpens) (_hx : x ∈ (U : Set X)) (r : ℕ) (f : Fin r → Γ(X, U.1)),
          IsGeneratedByOn X.toRingedSpace J U.1 f ∧ Koszul.IsKoszulRegular f

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularIdealSheaf_iff_exists_affine_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/QuasiRegular.lean, line 148. The attribute's comment: “quasi_regular”.

A sheaf of ideals on a scheme is quasi-regular if and only if, around each point of the support of its quotient, it is generated on an affine open by a quasi-regular sequence in the ring of sections of that open.

theorem isQuasiRegularIdealSheaf_iff_exists_affine_generators (X : Scheme.{u})
    (J : (structureSheafModule X.toRingedSpace).Submodule) :
    IsQuasiRegularIdealSheaf X.toRingedSpace J ↔
      ∀ x : X, x ∈ idealQuotientSupport X.toRingedSpace J →
        ∃ (U : X.affineOpens) (_hx : x ∈ (U : Set X)) (r : ℕ)
          (f : Fin r → X.toRingedSpace.presheaf.obj (op U.1)),
          IsGeneratedByOn X.toRingedSpace J U.1 f ∧
            RingTheory.Sequence.IsQuasiRegular
              (X.toRingedSpace.presheaf.obj (op U.1)) (List.ofFn f)

Stacks.AlgebraicGeometry.RegularIdealSheafAffine.isRegularIdealSheaf_iff_exists_affine_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheafAffine/Regular.lean, line 100. The attribute's comment: “regular”.

Stacks Project, Tag 063G (regular). A sheaf of ideals on a scheme is regular if and only if, around each point of the support of its quotient, it is generated on an affine open by a regular sequence in the ring of sections of that open.

theorem isRegularIdealSheaf_iff_exists_affine_generators (X : Scheme.{u})
    (J : (structureSheafModule X.toRingedSpace).Submodule) :
    IsRegularIdealSheaf X.toRingedSpace J ↔
      ∀ x : X, x ∈ idealQuotientSupport X.toRingedSpace J →
        ∃ (U : Opens X) (_hx : x ∈ U) (_hU : IsAffineOpen U) (r : ℕ)
          (f : Fin r → X.presheaf.obj (op U)),
          RingTheory.Sequence.IsRegular (X.presheaf.obj (op U)) (List.ofFn f) ∧
            IsGeneratedByOn X.toRingedSpace J U f

Tag 063I, a lemma

Tag 063I in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.regular_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularIdealSheaf/NoetherianEquivalence.lean, line 66. References: EGA IV (16.9.10); EGA IV (16.9.11); SGA 6 VII (1.4), “special case”.

Let X be a locally Noetherian scheme, let J be a quasi-coherent sheaf of ideals and let x be a point of the support of O_X / J. The following are equivalent:

1. J_x is generated by a regular sequence in O_{X, x};
2. J_x is generated by a Koszul-regular sequence in O_{X, x};
3. J_x is generated by an H₁-regular sequence in O_{X, x};
4. J_x is generated by a quasi-regular sequence in O_{X, x};
5. there is an affine neighbourhood U of x with J(U) generated by a regular sequence;
6. there is an affine neighbourhood U of x with J(U) generated by a Koszul-regular sequence;
7. there is an affine neighbourhood U of x with J(U) generated by an H₁-regular sequence;
8. there is an affine neighbourhood U of x with J(U) generated by a quasi-regular sequence;
9. there is a neighbourhood U of x on which J is a regular ideal sheaf;
10. there is a neighbourhood U of x on which J is a Koszul-regular ideal sheaf;
11. there is a neighbourhood U of x on which J is an H₁-regular ideal sheaf;
12. there is a neighbourhood U of x on which J is a quasi-regular ideal sheaf.

theorem regular_tfae [IsLocallyNoetherian X] (J : X.IdealSheafData) (x : X)
    (hx : x ∈ J.support) :
    List.TFAE
      [∃ (s : ℕ) (g : Fin s → X.presheaf.stalk x),
          stalkIdeal J x hx = Ideal.span (Set.range g) ∧
            IsRegular (X.presheaf.stalk x) (List.ofFn g),
        ∃ (s : ℕ) (g : Fin s → X.presheaf.stalk x),
          stalkIdeal J x hx = Ideal.span (Set.range g) ∧ Koszul.IsKoszulRegular g,
        ∃ (s : ℕ) (g : Fin s → X.presheaf.stalk x),
          stalkIdeal J x hx = Ideal.span (Set.range g) ∧ Koszul.IsH1Regular g,
        ∃ (s : ℕ) (g : Fin s → X.presheaf.stalk x),
          stalkIdeal J x hx = Ideal.span (Set.range g) ∧
            IsQuasiRegular (X.presheaf.stalk x) (List.ofFn g),
        ∃ (U : X.affineOpens) (_ : x ∈ U.1) (s : ℕ) (f : Fin s → Γ(X, U.1)),
          J.ideal U = Ideal.span (Set.range f) ∧ IsRegular Γ(X, U.1) (List.ofFn f),
        ∃ (U : X.affineOpens) (_ : x ∈ U.1) (s : ℕ) (f : Fin s → Γ(X, U.1)),
          J.ideal U = Ideal.span (Set.range f) ∧ Koszul.IsKoszulRegular f,
        ∃ (U : X.affineOpens) (_ : x ∈ U.1) (s : ℕ) (f : Fin s → Γ(X, U.1)),
          J.ideal U = Ideal.span (Set.range f) ∧ Koszul.IsH1Regular f,
        ∃ (U : X.affineOpens) (_ : x ∈ U.1) (s : ℕ) (f : Fin s → Γ(X, U.1)),
          J.ideal U = Ideal.span (Set.range f) ∧ IsQuasiRegular Γ(X, U.1) (List.ofFn f),
        ∃ U : X.Opens, x ∈ U ∧ IsRegularImmersion (J.comap U.ι).subschemeι,
        ∃ U : X.Opens, x ∈ U ∧ IsKoszulRegularImmersion (J.comap U.ι).subschemeι,
        ∃ U : X.Opens, x ∈ U ∧ IsH1RegularImmersion (J.comap U.ι).subschemeι,
        ∃ U : X.Opens, x ∈ U ∧ IsQuasiRegularImmersion (J.comap U.ι).subschemeι]

Sources

• Section 31.21, Tag 067M
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.regularSequenceMultiplication · Stacks.AlgebraicGeometry.SeqKoszul.sheafComplex · Stacks.AlgebraicGeometry.QuasiRegular.quasiRegularMap · Stacks.AlgebraicGeometry.SeqKoszul.isH1RegularSequence_of_isKoszulRegularSequence · Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularSequence_of_regularSequence · Stacks.AlgebraicGeometry.RegularIdealSheaf.isIso_quasiRegularMap_of_isH1RegularSequence · Stacks.AlgebraicGeometry.RegularIdealSheaf.IsQuasiRegularIdealSheaf · Stacks.AlgebraicGeometry.RegularIdealSheaf.IsRegularIdealSheaf

Section31.22 Regular immersions#

Section 31.22 of the Stacks Project, Tag 0638. 12 tags here are carried by 55 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 063J, a definition

Tag 063J in the Stacks Project.

Stacks.AlgebraicGeometry.isRegularImmersion_iff_of_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/RegularOpenIndependence.lean, line 126. The attribute's comment: “part (1): independence of the chosen open”.

An immersion i : Z ⟶ X is regular if and only if, for one — equivalently any — open subscheme U of X through which i factors as a closed immersion j : Z ⟶ U, the defining ideal of j is a regular ideal sheaf on U.

theorem isRegularImmersion_iff_of_open {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
    (U : X.Opens) (j : Z ⟶ U.toScheme) [IsClosedImmersion j] (hij : j ≫ U.ι = i) :
    IsRegularImmersion i ↔
      IsRegularIdealSheaf U.toScheme.toLocallyRingedSpace.toRingedSpace
        (definingIdealOfHom j)

Stacks.AlgebraicGeometry.RegularIdealSheaf.IsRegularImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Immersion.lean, line 225. The attribute's comment: “part (1): regular immersion”.

Stacks tag 063J, part (1). The immersion i is regular when the defining ideal sheaf of its canonical closed factor is a regular ideal sheaf.

def IsRegularImmersion (i : Z ⟶ X) [IsImmersion i] : Prop

Stacks.AlgebraicGeometry.RegularIdealSheaf.IsKoszulRegularImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Immersion.lean, line 232. The attribute's comment: “part (2): Koszul-regular immersion”. References: SGA 6 VII (1.4), “regular immersion”.

Stacks tag 063J, part (2). The immersion i is Koszul-regular when the defining ideal sheaf of its canonical closed factor is a Koszul-regular ideal sheaf.

def IsKoszulRegularImmersion (i : Z ⟶ X) [IsImmersion i] : Prop

Stacks.AlgebraicGeometry.RegularIdealSheaf.IsH1RegularImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Immersion.lean, line 239. The attribute's comment: “part (3): H₁-regular immersion”.

Stacks tag 063J, part (3). The immersion i is H₁-regular when the defining ideal sheaf of its canonical closed factor is an H₁-regular ideal sheaf.

def IsH1RegularImmersion (i : Z ⟶ X) [IsImmersion i] : Prop

Stacks.AlgebraicGeometry.RegularIdealSheaf.IsQuasiRegularImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Immersion.lean, line 246. The attribute's comment: “part (4): quasi-regular immersion”. References: EGA IV (16.9.2), “quasi-regular”.

Stacks tag 063J, part (4). The immersion i is quasi-regular when the defining ideal sheaf of its canonical closed factor is a quasi-regular ideal sheaf.

def IsQuasiRegularImmersion (i : Z ⟶ X) [IsImmersion i] : Prop

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularIdealSheaf_definingIdealOfHom_congr, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Independence.lean, line 925. The attribute's comment: “part (2): independence of the chosen open, for the restricted defining ideal”.

Stacks tag 063J, part (2): independence of the chosen open. For an immersion i : Z ⟶ X and two opens of X in which i is closed, the Koszul-regularity condition of Stacks tag 063D on the restriction of the defining ideal sheaf of i is the same on both.

theorem isKoszulRegularIdealSheaf_definingIdealOfHom_congr (i : Z ⟶ X) [IsImmersion i]
    (V V' : X.Opens) (j : Z ⟶ V.toScheme) [IsClosedImmersion j] (hij : j ≫ V.ι = i)
    (j' : Z ⟶ V'.toScheme) [IsClosedImmersion j'] (hij' : j' ≫ V'.ι = i) :
    IsKoszulRegularIdealSheaf V.toScheme.toLocallyRingedSpace.toRingedSpace
        (restrictSubmodule V (definingIdealOfHom i)) ↔
      IsKoszulRegularIdealSheaf V'.toScheme.toLocallyRingedSpace.toRingedSpace
        (restrictSubmodule V' (definingIdealOfHom i))

Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularIdealSheaf_definingIdealOfHom_congr, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Independence.lean, line 937. The attribute's comment: “part (3): independence of the chosen open, for the restricted defining ideal”.

Stacks tag 063J, part (3): independence of the chosen open.

theorem isH1RegularIdealSheaf_definingIdealOfHom_congr (i : Z ⟶ X) [IsImmersion i]
    (V V' : X.Opens) (j : Z ⟶ V.toScheme) [IsClosedImmersion j] (hij : j ≫ V.ι = i)
    (j' : Z ⟶ V'.toScheme) [IsClosedImmersion j'] (hij' : j' ≫ V'.ι = i) :
    IsH1RegularIdealSheaf V.toScheme.toLocallyRingedSpace.toRingedSpace
        (restrictSubmodule V (definingIdealOfHom i)) ↔
      IsH1RegularIdealSheaf V'.toScheme.toLocallyRingedSpace.toRingedSpace
        (restrictSubmodule V' (definingIdealOfHom i))

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularIdealSheaf_definingIdealOfHom_congr, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Independence.lean, line 949. The attribute's comment: “part (4): independence of the chosen open, for the restricted defining ideal”.

Stacks tag 063J, part (4): independence of the chosen open.

theorem isQuasiRegularIdealSheaf_definingIdealOfHom_congr (i : Z ⟶ X) [IsImmersion i]
    (V V' : X.Opens) (j : Z ⟶ V.toScheme) [IsClosedImmersion j] (hij : j ≫ V.ι = i)
    (j' : Z ⟶ V'.toScheme) [IsClosedImmersion j'] (hij' : j' ≫ V'.ι = i) :
    IsQuasiRegularIdealSheaf V.toScheme.toLocallyRingedSpace.toRingedSpace
        (restrictSubmodule V (definingIdealOfHom i)) ↔
      IsQuasiRegularIdealSheaf V'.toScheme.toLocallyRingedSpace.toRingedSpace
        (restrictSubmodule V' (definingIdealOfHom i))

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularImmersion_iff_of_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Independence.lean, line 1005. The attribute's comment: “part (2): independence of the chosen open”.

Stacks tag 063J, part (2): independence of the chosen open. An immersion is Koszul-regular exactly when the defining ideal sheaf of its closed factor through any open in which it is closed is a Koszul-regular ideal sheaf — not only the canonical one.

theorem isKoszulRegularImmersion_iff_of_open (i : Z ⟶ X) [IsImmersion i]
    (V : X.Opens) (j : Z ⟶ V.toScheme) [IsClosedImmersion j] (hij : j ≫ V.ι = i) :
    IsKoszulRegularImmersion i ↔
      IsKoszulRegularIdealSheaf V.toScheme.toLocallyRingedSpace.toRingedSpace
        (definingIdealOfHom j)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularImmersion_iff_of_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Independence.lean, line 1019. The attribute's comment: “part (3): independence of the chosen open”.

Stacks tag 063J, part (3): independence of the chosen open.

theorem isH1RegularImmersion_iff_of_open (i : Z ⟶ X) [IsImmersion i]
    (V : X.Opens) (j : Z ⟶ V.toScheme) [IsClosedImmersion j] (hij : j ≫ V.ι = i) :
    IsH1RegularImmersion i ↔
      IsH1RegularIdealSheaf V.toScheme.toLocallyRingedSpace.toRingedSpace
        (definingIdealOfHom j)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularImmersion_iff_of_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Independence.lean, line 1033. The attribute's comment: “part (4): independence of the chosen open”.

Stacks tag 063J, part (4): independence of the chosen open.

theorem isQuasiRegularImmersion_iff_of_open (i : Z ⟶ X) [IsImmersion i]
    (V : X.Opens) (j : Z ⟶ V.toScheme) [IsClosedImmersion j] (hij : j ≫ V.ι = i) :
    IsQuasiRegularImmersion i ↔
      IsQuasiRegularIdealSheaf V.toScheme.toLocallyRingedSpace.toRingedSpace
        (definingIdealOfHom j)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularImmersion_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Independence.lean, line 1137. The attribute's comment: “part (2): stability under restricting the target to an open”.

Stacks tag 063J, part (2): Koszul-regularity survives restricting the target to an open. If i : Z ⟶ X is a Koszul-regular immersion then so is its restriction i.resLE V (i ⁻¹ᵁ V) le_rfl : i ⁻¹ᵁ V ⟶ V to any open V ⊆ X.

theorem isKoszulRegularImmersion_resLE (i : Z ⟶ X) [IsImmersion i]
    (h : IsKoszulRegularImmersion i) (V : X.Opens) :
    IsKoszulRegularImmersion (i.resLE V (i ⁻¹ᵁ V) le_rfl)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularImmersion_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Independence.lean, line 1154. The attribute's comment: “part (3): stability under restricting the target to an open”.

Stacks tag 063J, part (3): H₁-regularity survives restricting the target to an open.

theorem isH1RegularImmersion_resLE (i : Z ⟶ X) [IsImmersion i]
    (h : IsH1RegularImmersion i) (V : X.Opens) :
    IsH1RegularImmersion (i.resLE V (i ⁻¹ᵁ V) le_rfl)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularImmersion_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/Independence.lean, line 1171. The attribute's comment: “part (4): stability under restricting the target to an open”.

Stacks tag 063J, part (4): quasi-regularity survives restricting the target to an open.

theorem isQuasiRegularImmersion_resLE (i : Z ⟶ X) [IsImmersion i]
    (h : IsQuasiRegularImmersion i) (V : X.Opens) :
    IsQuasiRegularImmersion (i.resLE V (i ⁻¹ᵁ V) le_rfl)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularImmersion_of_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/ZariskiLocal.lean, line 97. The attribute's comment: “part (2): gluing along an open cover of the target”.

Stacks tag 063J, part (2): Koszul-regularity glues along an open cover of the target. If every restriction i.resLE (V k) (i ⁻¹ᵁ V k) le_rfl of the immersion i over a member of an open cover V of X is a Koszul-regular immersion, then so is i.

theorem isKoszulRegularImmersion_of_resLE
    (h : ∀ k, IsKoszulRegularImmersion (i.resLE (V k) (i ⁻¹ᵁ V k) le_rfl)) :
    IsKoszulRegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularImmersion_of_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/ZariskiLocal.lean, line 121. The attribute's comment: “part (3): gluing along an open cover of the target”.

Stacks tag 063J, part (3): H₁-regularity glues along an open cover of the target.

theorem isH1RegularImmersion_of_resLE
    (h : ∀ k, IsH1RegularImmersion (i.resLE (V k) (i ⁻¹ᵁ V k) le_rfl)) :
    IsH1RegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularImmersion_of_resLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/ZariskiLocal.lean, line 145. The attribute's comment: “part (4): gluing along an open cover of the target”.

Stacks tag 063J, part (4): quasi-regularity glues along an open cover of the target.

theorem isQuasiRegularImmersion_of_resLE
    (h : ∀ k, IsQuasiRegularImmersion (i.resLE (V k) (i ⁻¹ᵁ V k) le_rfl)) :
    IsQuasiRegularImmersion i

Stacks.AlgebraicGeometry.isQuasiRegularImmersion_iff_of_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/OpenIndependence.lean, line 582. The attribute's comment: “part (4): independence of the chosen open”.

An immersion i : Z ⟶ X is quasi-regular if and only if, for one — equivalently any — open subscheme U of X through which i factors as a closed immersion j : Z ⟶ U, the defining ideal of j is a quasi-regular ideal sheaf on U.

theorem isQuasiRegularImmersion_iff_of_open {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
    (U : X.Opens) (j : Z ⟶ U.toScheme) [IsClosedImmersion j] (hij : j ≫ U.ι = i) :
    IsQuasiRegularImmersion i ↔
      IsQuasiRegularIdealSheaf U.toScheme.toLocallyRingedSpace.toRingedSpace
        (definingIdealOfHom j)

Tag 063K, a lemma

Tag 063K in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularImmersion_of_isRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/Implications.lean, line 262.

A regular immersion is Koszul-regular. The first implication of Stacks tag 063K, between parts (1) and (2) of Stacks tag 063J.

theorem isKoszulRegularImmersion_of_isRegularImmersion (h : IsRegularImmersion i) :
    IsKoszulRegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularImmersion_of_isKoszulRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/Implications.lean, line 270.

A Koszul-regular immersion is H₁-regular. The second implication of Stacks tag 063K, between parts (2) and (3) of Stacks tag 063J.

theorem isH1RegularImmersion_of_isKoszulRegularImmersion (h : IsKoszulRegularImmersion i) :
    IsH1RegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularImmersion_of_isH1RegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/Implications.lean, line 277.

An H₁-regular immersion is quasi-regular. The third implication of Stacks tag 063K, between parts (3) and (4) of Stacks tag 063J.

theorem isQuasiRegularImmersion_of_isH1RegularImmersion (h : IsH1RegularImmersion i) :
    IsQuasiRegularImmersion i

Tag 063L, a lemma

Tag 063L in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isRegularImmersion_iff_isKoszulRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/NoetherianRegularKoszul.lean, line 104. The attribute's comment: “regular iff Koszul-regular”.

Stacks tag 063L, parts (1) and (2). An immersion into a locally Noetherian scheme is regular if and only if it is Koszul-regular.

theorem isRegularImmersion_iff_isKoszulRegularImmersion (i : Z ⟶ X) [IsImmersion i]
    [IsLocallyNoetherian X] :
    IsRegularImmersion i ↔ IsKoszulRegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularImmersion_iff_isH1RegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/NoetherianRegularKoszul.lean, line 131. The attribute's comment: “Koszul-regular iff H₁-regular”.

Stacks tag 063L, parts (2) and (3). An immersion into a locally Noetherian scheme is Koszul-regular if and only if it is H₁-regular.

theorem isKoszulRegularImmersion_iff_isH1RegularImmersion (i : Z ⟶ X) [IsImmersion i]
    [IsLocallyNoetherian X] :
    IsKoszulRegularImmersion i ↔ IsH1RegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularImmersion_iff_isQuasiRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/NoetherianRegularKoszul.lean, line 141. The attribute's comment: “H₁-regular iff quasi-regular”.

Stacks tag 063L, parts (3) and (4). An immersion into a locally Noetherian scheme is H₁-regular if and only if it is quasi-regular.

theorem isH1RegularImmersion_iff_isQuasiRegularImmersion (i : Z ⟶ X) [IsImmersion i]
    [IsLocallyNoetherian X] :
    IsH1RegularImmersion i ↔ IsQuasiRegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.regularImmersion_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/NoetherianRegularKoszul.lean, line 153. The attribute's comment: “the four notions agree over a locally Noetherian base”. References: EGA IV (16.9.10); EGA IV (16.9.11), “more general”.

Stacks tag 063L. For an immersion into a locally Noetherian scheme the four notions of regularity — regular, Koszul-regular, H₁-regular and quasi-regular — are equivalent.

theorem regularImmersion_tfae (i : Z ⟶ X) [IsImmersion i] [IsLocallyNoetherian X] :
    List.TFAE [IsRegularImmersion i, IsKoszulRegularImmersion i, IsH1RegularImmersion i,
      IsQuasiRegularImmersion i]

Tag 067P, a lemma

Tag 067P in the Stacks Project.

Stacks.AlgebraicGeometry.isRegularImmersion_pullback_snd_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularIdealSheaf/FlatBaseChange.lean, line 163. The attribute's comment: “regular”.

A regular immersion remains a regular immersion after base change along a flat morphism.

theorem isRegularImmersion_pullback_snd_of_flat {Z X X' : Scheme.{u}} (i : Z ⟶ X) (g : X' ⟶ X)
    [IsImmersion i] [Flat g] (hi : IsRegularImmersion i) :
    IsRegularImmersion (pullback.snd i g)

Stacks.AlgebraicGeometry.isKoszulRegularImmersion_pullback_snd_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularIdealSheaf/FlatBaseChange.lean, line 221. The attribute's comment: “koszul”.

A Koszul-regular immersion remains a Koszul-regular immersion after base change along a flat morphism.

theorem isKoszulRegularImmersion_pullback_snd_of_flat {Z X X' : Scheme.{u}} (i : Z ⟶ X)
    (g : X' ⟶ X) [IsImmersion i] [Flat g] (hi : IsKoszulRegularImmersion i) :
    IsKoszulRegularImmersion (pullback.snd i g)

Stacks.AlgebraicGeometry.isH1RegularImmersion_pullback_snd_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularIdealSheaf/FlatBaseChange.lean, line 275. The attribute's comment: “h1”.

A H₁-regular immersion remains a H₁-regular immersion after base change along a flat morphism.

theorem isH1RegularImmersion_pullback_snd_of_flat {Z X X' : Scheme.{u}} (i : Z ⟶ X)
    (g : X' ⟶ X) [IsImmersion i] [Flat g] (hi : IsH1RegularImmersion i) :
    IsH1RegularImmersion (pullback.snd i g)

Stacks.AlgebraicGeometry.isQuasiRegularImmersion_pullback_snd_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularIdealSheaf/FlatBaseChange.lean, line 333. The attribute's comment: “quasi”. References: EGA IV (19.1.5), “(ii)”.

A quasi-regular immersion remains a quasi-regular immersion after base change along a flat morphism.

theorem isQuasiRegularImmersion_pullback_snd_of_flat {Z X X' : Scheme.{u}} (i : Z ⟶ X)
    (g : X' ⟶ X) [IsImmersion i] [Flat g] (hi : IsQuasiRegularImmersion i) :
    IsQuasiRegularImmersion (pullback.snd i g)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularIdealSheaf_pullbackIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/FlatBaseChange.lean, line 375. The attribute's comment: “part (2), ideal-sheaf level: the inverse image ideal sheaf h⁻¹J·O_{X'} of a Koszul-regular ideal sheaf along a morphism of locally ringed spaces with flat stalk maps is Koszul-regular”. References: SGA 6 VII (1.5), “flat base change, Koszul”.

Stacks tag 067P, part (2), at the level of ideal sheaves. The inverse image ideal sheaf of a Koszul-regular ideal sheaf along a morphism with flat stalk maps is Koszul-regular.

theorem isKoszulRegularIdealSheaf_pullbackIdeal (hflat : HasFlatStalks h)
    (J : (structureSheafModule X.toRingedSpace).Submodule)
    (hJ : IsKoszulRegularIdealSheaf X.toRingedSpace J) :
    IsKoszulRegularIdealSheaf X'.toRingedSpace (pullbackIdeal h J)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularIdealSheaf_pullbackIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/FlatBaseChange.lean, line 386. The attribute's comment: “part (3), ideal-sheaf level: the inverse image ideal sheaf h⁻¹J·O_{X'} of an H₁-regular ideal sheaf along a morphism of locally ringed spaces with flat stalk maps is H₁-regular”. References: SGA 6 VII (1.5), “flat base change, H1”.

Stacks tag 067P, part (3), at the level of ideal sheaves. The inverse image ideal sheaf of an H₁-regular ideal sheaf along a morphism with flat stalk maps is H₁-regular.

theorem isH1RegularIdealSheaf_pullbackIdeal (hflat : HasFlatStalks h)
    (J : (structureSheafModule X.toRingedSpace).Submodule)
    (hJ : IsH1RegularIdealSheaf X.toRingedSpace J) :
    IsH1RegularIdealSheaf X'.toRingedSpace (pullbackIdeal h J)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularIdealSheaf_pullbackIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularIdealSheaf/FlatBaseChange.lean, line 397. The attribute's comment: “part (4), ideal-sheaf level: the inverse image ideal sheaf h⁻¹J·O_{X'} of a quasi-regular ideal sheaf along a morphism of locally ringed spaces with flat stalk maps is quasi-regular”. References: SGA 6 VII (1.5), “flat base change, quasi”.

Stacks tag 067P, part (4), at the level of ideal sheaves. The inverse image ideal sheaf of a quasi-regular ideal sheaf along a morphism with flat stalk maps is quasi-regular.

theorem isQuasiRegularIdealSheaf_pullbackIdeal (hflat : HasFlatStalks h)
    (J : (structureSheafModule X.toRingedSpace).Submodule)
    (hJ : IsQuasiRegularIdealSheaf X.toRingedSpace J) :
    IsQuasiRegularIdealSheaf X'.toRingedSpace (pullbackIdeal h J)

Tag 063M, a lemma

Tag 063M in the Stacks Project.

AlgebraicGeometry.isFiniteLocallyFree_universalConormalSheaf_of_isKoszulRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/LocalCompleteIntersection/UnramifiedConormal.lean, line 97. The attribute's comment: “condition (2) for a Koszul-regular immersion, for the conormal sheaf of Tag 04F4. Condition (1) is at RegularImmersion/FinitePresentation.lean; condition (2) does not need Tag 063H, and is proved at RegularImmersion/ConormalLocallyFree.lean by a route through Tags 063G, 08RK, 01R3, 00NX and 05JM that never uses 063H”.

The conormal sheaf of a Koszul-regular immersion of schemes, in the sense of Stacks 04F4, is finite locally free.

theorem isFiniteLocallyFree_universalConormalSheaf_of_isKoszulRegularImmersion
    {Z P : Scheme.{u}} (i : Z ⟶ P) [IsImmersion i] (hi : IsKoszulRegularImmersion i) :
    SheafOfModules.IsFiniteLocallyFree.{u, u, u} (universalConormalSheaf i)

Stacks.Conormal.isQuasiRegularImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/ConormalQuasiRegularCriterion.lean, line 381. The attribute's comment: “the whole statement: an immersion is quasi-regular iff it is locally of finite presentation, its conormal sheaf is finite locally free, and the map of 0632 is an isomorphism”. References: EGA IV (16.9.8), “(i)”; EGA IV (17.12.1); EGA IV (19.1.3).

An immersion i : Z ⟶ X of schemes is quasi-regular if and only if (1) it is locally of finite presentation, (2) its conormal sheaf 𝒞_{Z/X} is finite locally free, and (3) the canonical map Sym*(𝒞_{Z/X}) ⟶ 𝒞_{Z/X,*} of [Stacks, Tag 0632] is an isomorphism in every degree.

theorem isQuasiRegularImmersion_iff (i : Z ⟶ X) [IsImmersion i] :
    Stacks.AlgebraicGeometry.RegularIdealSheaf.IsQuasiRegularImmersion i ↔
      LocallyOfFinitePresentation i ∧
        AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} (conormalSheaf i) ∧
          ∀ n : ℤ, IsIso ((conormalSymmetricHom i).app n)

Stacks.AlgebraicGeometry.RegularIdealSheaf.locallyOfFinitePresentation_of_isQuasiRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/FinitePresentation.lean, line 103. The attribute's comment: “condition (1) of the statement, in the direction out of quasi-regularity: a quasi-regular immersion is locally of finite presentation. The whole iff is proved at Stacks.Conormal.isQuasiRegularImmersion_iff”. References: EGA IV (16.9.8), “(i), one direction”; EGA IV (16.9.9), “l.f.p. is necessary”; SGA 3 III (4.6.2), “more general”.

[Stacks, Tag 063M], condition (1) in the direction out of quasi-regularity. A quasi-regular immersion of schemes is locally of finite presentation.

The canonical closed factor i.liftCoborder is locally of finite presentation by [Stacks, Tag 01TV], since the quasi-regular defining ideal sheaf is finitely generated over every affine open, and the remaining factor i.coborderRange.ι is an open immersion.

theorem locallyOfFinitePresentation_of_isQuasiRegularImmersion (i : Z ⟶ X) [IsImmersion i]
    (h : IsQuasiRegularImmersion i) : LocallyOfFinitePresentation i

Tag 063N, a lemma

Tag 063N in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.mono_conormalLeftMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/ConormalSequence.lean, line 400. The attribute's comment: “exactness at the left term: for an H₁-regular immersion i the canonical map i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} is a monomorphism”.

[Stacks Project, Tag 063N]: the conormal sequence of an H1-regular immersion is exact at its left-hand term. For immersions Z --i--→ Y --j--→ X with i an H1-regular immersion, the canonical map i^* C_{Y/X} ⟶ C_{Z/X} of [Stacks Project, Tag 01R4] is a monomorphism.

theorem mono_conormalLeftMap (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j]
    (hi : IsH1RegularImmersion i) : Mono (conormalLeftMap i j)

Stacks.AlgebraicGeometry.RegularIdealSheaf.conormalSequence_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/ConormalSequence.lean, line 554. The attribute's comment: “exactness: the canonical sequence 0 ⟶ i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0 of an H₁-regular immersion is short exact”.

[Stacks Project, Tag 063N]: the conormal sequence of an H1-regular immersion is short exact. For immersions Z --i--→ Y --j--→ X with i an H1-regular immersion, the canonical sequence 0 ⟶ i^* C_{Y/X} ⟶ C_{Z/X} ⟶ C_{Z/Y} ⟶ 0 of [Stacks Project, Tag 062S] is a short exact sequence of O_Z-modules.

Exactness in the middle and surjectivity on the right are [Stacks Project, Tag 062S]; what H1-regularity of i adds is injectivity on the left, Stacks.AlgebraicGeometry.RegularIdealSheaf.mono_conormalLeftMap.

theorem conormalSequence_shortExact (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j]
    (hi : IsH1RegularImmersion i) : (conormalSequenceShortComplex i j).ShortExact

Stacks.AlgebraicGeometry.RegularIdealSheaf.conormalSequence_locallySplit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/ConormalSequence.lean, line 566. The attribute's comment: “local splitness: on a neighbourhood of every point of Z the canonical sequence of an H₁-regular immersion splits”. References: EGA IV (16.9.13), “more general”; EGA IV (19.1.5), “more general”.

[Stacks Project, Tag 063N]: the conormal sequence of an H1-regular immersion is locally split. Every point of Z has an open neighbourhood over which the short exact sequence 0 ⟶ i^* C_{Y/X} ⟶ C_{Z/X} ⟶ C_{Z/Y} ⟶ 0 splits, the restriction to an open being the slice restriction SheafOfModules.over.

theorem conormalSequence_locallySplit (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j]
    (hi : IsH1RegularImmersion i) (z : Z) :
    ∃ V : Z.Opens, z ∈ V ∧ Nonempty (((conormalSequenceShortComplex i j).map
      (_root_.SheafOfModules.overFunctor
        (structureSheafRing Z.toLocallyRingedSpace.toRingedSpace) V)).Splitting)

Tag 067Q, a lemma

Tag 067Q in the Stacks Project.

Stacks.AlgebraicGeometry.isRegularImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/Composition.lean, line 155. The attribute's comment: “composition_regular”. References: EGA IV (19.1.5); SGA 6 VIII (1.1), “special case”.

The composite of two regular immersions of schemes is a regular immersion.

theorem isRegularImmersion_comp {Z Y X : Scheme.{u}} (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i]
    [IsImmersion j] (hi : IsRegularImmersion i) (hj : IsRegularImmersion j) :
    IsRegularImmersion (i ≫ j)

Stacks.AlgebraicGeometry.isKoszulRegularImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionComposition.lean, line 263. The attribute's comment: “composition_koszul_regular”. References: SGA 6 VII (1.7); SGA 6 VIII (1.1); SGA 6 VIII (1.3).

Stacks tag 067Q, the Koszul-regular case. The composite of two Koszul-regular immersions of schemes is a Koszul-regular immersion.

theorem isKoszulRegularImmersion_comp {Z Y X : Scheme.{u}} (i : Z ⟶ Y) (j : Y ⟶ X)
    [IsImmersion i] [IsImmersion j] (hi : IsKoszulRegularImmersion i)
    (hj : IsKoszulRegularImmersion j) :
    IsKoszulRegularImmersion (i ≫ j)

Stacks.AlgebraicGeometry.isH1RegularImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionComposition.lean, line 282. The attribute's comment: “composition_h1_regular”.

Stacks tag 067Q, the H₁-regular case. The composite of two H₁-regular immersions of schemes is an H₁-regular immersion.

theorem isH1RegularImmersion_comp {Z Y X : Scheme.{u}} (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i]
    [IsImmersion j] (hi : IsH1RegularImmersion i) (hj : IsH1RegularImmersion j) :
    IsH1RegularImmersion (i ≫ j)

Stacks.AlgebraicGeometry.isQuasiRegularImmersion_comp_of_isH1RegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RegularImmersionComposition.lean, line 300. The attribute's comment: “composition_h1_quasi_regular”.

Stacks tag 067Q, the mixed case. The composite of an H₁-regular immersion of schemes and a quasi-regular immersion of schemes is a quasi-regular immersion.

theorem isQuasiRegularImmersion_comp_of_isH1RegularImmersion {Z Y X : Scheme.{u}} (i : Z ⟶ Y)
    (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] (hi : IsH1RegularImmersion i)
    (hj : IsQuasiRegularImmersion j) :
    IsQuasiRegularImmersion (i ≫ j)

Tag 068Z, a lemma

Tag 068Z in the Stacks Project.

Stacks.AlgebraicGeometry.isH1RegularImmersion_of_comp_of_isSplitExactConormalSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SplitConormalH1Regular.lean, line 427. The attribute's comment: “(2) H₁-regularity descends to the first immersion”.

[Stacks Project, Tag 068Z], part (2). For immersions i : Z ⟶ Y and j : Y ⟶ X with j locally of finite presentation whose conormal sequence is exact and locally split, H₁-regularity of i ≫ j descends to i.

theorem isH1RegularImmersion_of_comp_of_isSplitExactConormalSequence
    (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] [LocallyOfFinitePresentation j]
    (hS : IsSplitExactConormalSequence i j) (hij : IsH1RegularImmersion (i ≫ j)) :
    IsH1RegularImmersion i

Stacks.AlgebraicGeometry.isKoszulRegularImmersion_of_comp_of_isSplitExactConormalSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SplitConormalKoszulRegular.lean, line 473. The attribute's comment: “(3) Koszul-regularity of the first immersion”.

[Stacks Project, Tag 068Z], part (3). For immersions i : Z ⟶ Y and j : Y ⟶ X with j locally of finite presentation whose conormal sequence is exact and locally split, i is Koszul-regular as soon as both j and i ≫ j are.

theorem isKoszulRegularImmersion_of_comp_of_isSplitExactConormalSequence
    (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] [LocallyOfFinitePresentation j]
    (hS : IsSplitExactConormalSequence i j) (hj : IsKoszulRegularImmersion j)
    (hij : IsKoszulRegularImmersion (i ≫ j)) :
    IsKoszulRegularImmersion i

Stacks.AlgebraicGeometry.isQuasiRegularImmersion_of_comp_of_isSplitExactConormalSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SplitConormalQuasiRegular.lean, line 454. The attribute's comment: “(1) quasi-regularity descends to the first immersion”.

[Stacks Project, Tag 068Z], part (1). For immersions i : Z ⟶ Y and j : Y ⟶ X with j locally of finite presentation whose conormal sequence is exact and locally split, quasi-regularity of i ≫ j descends to i.

theorem isQuasiRegularImmersion_of_comp_of_isSplitExactConormalSequence
    (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j] [LocallyOfFinitePresentation j]
    (hS : IsSplitExactConormalSequence i j) (hij : IsQuasiRegularImmersion (i ≫ j)) :
    IsQuasiRegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularIdealSheaf_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/ConormalPermanence.lean, line 412. The attribute's comment: “part (3) for closed immersions: Koszul-regularity of j and of i ≫ j together with injectivity of the cotangent-fibre map I_x/𝔪_x I_x ⟶ J_x/𝔪_x J_x gives Koszul-regularity of i. That injectivity is a hypothesis here, not derived from exactness and local splitness of the conormal sequence”.

[Stacks Project, Tag 068Z] part (3) for closed immersions, from injectivity on cotangent fibres. Let Z --i--→ Y --j--→ X be closed immersions with Koszul-regular defining ideal sheaves for j and for i ≫ j. If at every point of Z the induced map of cotangent fibres I_x/𝔪_x I_x → J_x/𝔪_x J_x of the two defining ideals is injective, then the defining ideal sheaf of i is Koszul-regular.

Over an affine open U of X around the image of the point, local generators f of the ideal of Y extend to local generators f, g of the ideal of Z, both Koszul-regular, and the images of the g under j on sections generate the ideal of Z in Y and are Koszul-regular by [Stacks Project, Tag 068M].

theorem isKoszulRegularIdealSheaf_of_comp (i : Z ⟶ Y) (j : Y ⟶ X)
    [IsClosedImmersion i] [IsClosedImmersion j]
    (hinj : ∀ z : Z, Function.Injective (conormalFibreMap i j z))
    (hj : IsKoszulRegularIdealSheaf X.toRingedSpace (definingIdealOfHom j))
    (hij : IsKoszulRegularIdealSheaf X.toRingedSpace (definingIdealOfHom (i ≫ j))) :
    IsKoszulRegularIdealSheaf Y.toRingedSpace (definingIdealOfHom i)

Tag 0690, a lemma

Tag 0690 in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_opens_isSplitExactConormalSequence_of_split, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/H1RegularSplitConormal.lean, line 146. The attribute's comment: “(2) => (3)”. References: EGA IV (19.1.5), “(iv)”; SGA 6 VII (4.2), “partial”.

Stacks tag 0690, (2) ⇒ (3). Let i : Z ⟶ Y and j : Y ⟶ X be immersions of schemes and let z : Z. If i and i ≫ j are regular immersions in a neighbourhood of z, then i ≫ j is a regular immersion in a neighbourhood of z and the conormal sequence 0 ⟶ i^* 𝒞_{Y/X} ⟶ 𝒞_{Z/X} ⟶ 𝒞_{Z/Y} ⟶ 0 is exact and locally split in a neighbourhood of z.

theorem exists_opens_isSplitExactConormalSequence_of_split (i : Z ⟶ Y) (j : Y ⟶ X)
    [IsImmersion i] [IsImmersion j] (z : Z)
    (hi : ∃ W : Z.Opens, z ∈ W ∧ IsRegularImmersion (W.ι ≫ i))
    (hji : ∃ U : Z.Opens, z ∈ U ∧ IsRegularImmersion (U.ι ≫ (i ≫ j))) :
    (∃ U : Z.Opens, z ∈ U ∧ IsRegularImmersion (U.ι ≫ (i ≫ j))) ∧
      ∃ W : Z.Opens, z ∈ W ∧ IsSplitExactConormalSequence (W.ι ≫ i) j

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_opens_isRegularImmersion_of_factors_of_split, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/H1RegularSplitConormal.lean, line 172. The attribute's comment: “(2) => (1)”.

Stacks tag 0690, (2) ⇒ (1). Let i : Z ⟶ Y and j : Y ⟶ X be immersions of schemes with X locally Noetherian and let z : Z. If i and i ≫ j are regular immersions in a neighbourhood of z, then i is a regular immersion in a neighbourhood of z and j is one in a neighbourhood of i z.

theorem exists_opens_isRegularImmersion_of_factors_of_split (i : Z ⟶ Y) (j : Y ⟶ X)
    [IsImmersion i] [IsImmersion j] [IsLocallyNoetherian X] (z : Z)
    (hi : ∃ W : Z.Opens, z ∈ W ∧ IsRegularImmersion (W.ι ≫ i))
    (hji : ∃ U : Z.Opens, z ∈ U ∧ IsRegularImmersion (U.ι ≫ (i ≫ j))) :
    (∃ W : Z.Opens, z ∈ W ∧ IsRegularImmersion (W.ι ≫ i)) ∧
      ∃ V : Y.Opens, i.base z ∈ V ∧ IsRegularImmersion (V.ι ≫ j)

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_opens_isSplitExactConormalSequence_of_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/H1RegularSplitConormal.lean, line 201. The attribute's comment: “(1) => (3)”. References: EGA IV (19.1.5), “partial”; SGA 6 VII (4.2), “partial”; SGA 6 VIII (1.3), “clause (i), special case”.

Stacks tag 0690, (1) ⇒ (3). Let i : Z ⟶ Y and j : Y ⟶ X be immersions of schemes with X locally Noetherian and let z : Z. If i is a regular immersion in a neighbourhood of z and j is one in a neighbourhood of i z, then i ≫ j is a regular immersion in a neighbourhood of z and the conormal sequence of the pair is exact and locally split in a neighbourhood of z.

theorem exists_opens_isSplitExactConormalSequence_of_factors (i : Z ⟶ Y) (j : Y ⟶ X)
    [IsImmersion i] [IsImmersion j] [IsLocallyNoetherian X] (z : Z)
    (hi : ∃ W : Z.Opens, z ∈ W ∧ IsRegularImmersion (W.ι ≫ i))
    (hj : ∃ V : Y.Opens, i.base z ∈ V ∧ IsRegularImmersion (V.ι ≫ j)) :
    (∃ U : Z.Opens, z ∈ U ∧ IsRegularImmersion (U.ι ≫ (i ≫ j))) ∧
      ∃ W : Z.Opens, z ∈ W ∧ IsSplitExactConormalSequence (W.ι ≫ i) j

Stacks.AlgebraicGeometry.RegularIdealSheaf.tfae_isRegularImmersion_near, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/H1RegularSplitConormal.lean, line 215.

Stacks tag 0690. For immersions i : Z ⟶ Y and j : Y ⟶ X with X locally Noetherian and z : Z, the following are equivalent: (1) i is a regular immersion near z and j is one near i z; (2) i and i ≫ j are regular immersions near z; (3) i ≫ j is a regular immersion near z and the conormal sequence of the pair is exact and locally split near z.

theorem tfae_isRegularImmersion_near (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i] [IsImmersion j]
    [IsLocallyNoetherian X] (z : Z) :
    List.TFAE
      [(∃ W : Z.Opens, z ∈ W ∧ IsRegularImmersion (W.ι ≫ i)) ∧
          ∃ V : Y.Opens, i.base z ∈ V ∧ IsRegularImmersion (V.ι ≫ j),
        (∃ W : Z.Opens, z ∈ W ∧ IsRegularImmersion (W.ι ≫ i)) ∧
          ∃ U : Z.Opens, z ∈ U ∧ IsRegularImmersion (U.ι ≫ (i ≫ j)),
        (∃ U : Z.Opens, z ∈ U ∧ IsRegularImmersion (U.ι ≫ (i ≫ j))) ∧
          ∃ W : Z.Opens, z ∈ W ∧ IsSplitExactConormalSequence (W.ι ≫ i) j]

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_opens_isRegularImmersion_of_split_near, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/NoetherianSplitConormal.lean, line 199. The attribute's comment: “(3) => (1)”.

Stacks tag 0690, (3) ⇒ (1). Let i : Z ⟶ Y and j : Y ⟶ X be immersions of schemes with X locally Noetherian, let z : Z and let y = i z. If i ≫ j is a regular immersion in a neighbourhood of z and the conormal sequence of the pair is exact and locally split in a neighbourhood of z, then i is a regular immersion in a neighbourhood of z and j is one in a neighbourhood of y.

theorem exists_opens_isRegularImmersion_of_split_near (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i]
    [IsImmersion j] [IsLocallyNoetherian X] (z : Z)
    (hji : ∃ U : Z.Opens, z ∈ U ∧ IsRegularImmersion (U.ι ≫ (i ≫ j)))
    (hS : ∃ W : Z.Opens, z ∈ W ∧ IsSplitExactConormalSequence (W.ι ≫ i) j) :
    (∃ W : Z.Opens, z ∈ W ∧ IsRegularImmersion (W.ι ≫ i)) ∧
      ∃ V : Y.Opens, i.base z ∈ V ∧ IsRegularImmersion (V.ι ≫ j)

Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_opens_isRegularImmersion_comp_of_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/NoetherianSplitConormal.lean, line 263. The attribute's comment: “(1) => (2)”.

Stacks tag 0690, (1) ⇒ (2). Let i : Z ⟶ Y and j : Y ⟶ X be immersions of schemes with X locally Noetherian and let z : Z. If i is a regular immersion in a neighbourhood of z and j is one in a neighbourhood of i z, then i ≫ j is a regular immersion in a neighbourhood of z.

theorem exists_opens_isRegularImmersion_comp_of_factors (i : Z ⟶ Y) (j : Y ⟶ X) [IsImmersion i]
    [IsImmersion j] [IsLocallyNoetherian X] (z : Z)
    (hi : ∃ W : Z.Opens, z ∈ W ∧ IsRegularImmersion (W.ι ≫ i))
    (hj : ∃ V : Y.Opens, i.base z ∈ V ∧ IsRegularImmersion (V.ι ≫ j)) :
    ∃ U : Z.Opens, z ∈ U ∧ IsRegularImmersion (U.ι ≫ (i ≫ j))

Tag 0691, a remark

Tag 0691 in the Stacks Project.

Stacks.Examples.regular_immersion_not_permanent_in_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Scheme/RegularImmersionNotPermanentInMiddle.lean, line 710. The attribute's comment: “The counterexample of the remark for X = 𝐀¹_k, Y = Spec(k[x]/(x²)) and Z = Spec(k[x]/(x)) over an arbitrary field k, at the level of schemes throughout. The three immersions are the Spec of the quotient maps k[x] → k[x]/(x²) (that is j), k[x] → k[x]/(x) (that is j ∘ i, identified with the composite by Stacks.Examples.simpleOriginImmersion_comp_doubleOriginLineImmersion) and k[x]/(x²) → k[x]/(x) (that is i). The predicate is Stacks.AlgebraicGeometry.RegularIdealSheaf.IsRegularImmersion, part (1) of Stacks tag 063J and the one whose variants the statements carrying Stacks tag 0690 compare; the in a neighbourhood of a point form in which Stacks tag 0690 states its three parts is Stacks.Examples.IsRegularImmersionAt, and the splitting condition of its part (3) is Stacks.AlgebraicGeometry.IsSplitExactConormalSequence on a neighbourhood, the form in which the proved implications of Stacks tag 0690 state it. Both forms are delivered: regularity of j at every point of Y, of i ≫ j at every point of Z and of both globally, against the refutation of regularity of i at every point of Z and globally. All three parts of Stacks tag 0690 are refuted, each as a whole and at every point of Z: parts (1) and (2) through their common first half, part (3) through its second half, the splitting, since its first half holds here. That last refutation runs through the implication (3) ⇒ (1) of Stacks tag 0690, Stacks.AlgebraicGeometry.RegularIdealSheaf.exists_opens_isRegularImmersion_of_split_near, which is proved; nothing here rests on an unproved result. The three ideal-level statements are retained as the affine half to which that predicate reduces by Stacks tag 063G. No hypothesis is carried beyond k being a field.”.

Stacks tag 0691. Regularity of an immersion is not inherited by the middle term of a factorization. For Z = Spec(k[x]/(x)) --i--→ Y = Spec(k[x]/(x²)) --j--→ X = 𝐀¹_k = Spec(k[x]) the two outer immersions j and j ∘ i are regular immersions — at every point of their sources and globally — while the middle one, i, is a regular immersion in no neighbourhood of any point of Z and in particular not globally, and the conormal sequence of the pair is exact and split in no neighbourhood of any point of Z; at the level of ideals, the ideals of Y in X and of Z in X are each generated by a weakly regular sequence and the ideal of Z in Y is generated by none. So each of the three parts of Stacks tag 0690 fails at every point of Z — parts (1) and (2) through their common first half, regularity of i near the point, and part (3) through its second half, the splitting, its first half being true — while "j ∘ i and j are regular immersions at z and y" holds, which is the content of the remark.

theorem regular_immersion_not_permanent_in_middle (k : Type*) [Field k] :
    -- `j` is a regular immersion at every point of `Y`, and `j ∘ i` at every point of `Z`
    (∀ y, IsRegularImmersionAt (doubleOriginLineImmersion k) y) ∧
      (∀ z, IsRegularImmersionAt
        (simpleOriginImmersion k ≫ doubleOriginLineImmersion k) z) ∧
      -- while `i` is a regular immersion in no neighbourhood of any point of `Z`
      (∀ z, ¬ IsRegularImmersionAt (simpleOriginImmersion k) z) ∧
      -- and the conormal sequence is exact and split in no neighbourhood of any point of `Z`
      (∀ z, ¬ ∃ W : (Spec (CommRingCat.of (SimpleOriginRing k))).Opens, z ∈ W ∧
        IsSplitExactConormalSequence (W.ι ≫ simpleOriginImmersion k)
          (doubleOriginLineImmersion k)) ∧
      -- so that each of the three parts of Stacks tag 0690 fails at every point of `Z`
      (∀ z, ¬ (IsRegularImmersionAt (simpleOriginImmersion k) z ∧
        IsRegularImmersionAt (doubleOriginLineImmersion k) ((simpleOriginImmersion k).base z))) ∧
      (∀ z, ¬ (IsRegularImmersionAt (simpleOriginImmersion k) z ∧
        IsRegularImmersionAt (simpleOriginImmersion k ≫ doubleOriginLineImmersion k) z)) ∧
      (∀ z, ¬ (IsRegularImmersionAt (simpleOriginImmersion k ≫ doubleOriginLineImmersion k) z ∧
        ∃ W : (Spec (CommRingCat.of (SimpleOriginRing k))).Opens, z ∈ W ∧
          IsSplitExactConormalSequence (W.ι ≫ simpleOriginImmersion k)
            (doubleOriginLineImmersion k))) ∧
      -- the same three facts globally
      RegularIdealSheaf.IsRegularImmersion (doubleOriginLineImmersion k) ∧
      RegularIdealSheaf.IsRegularImmersion
        (simpleOriginImmersion k ≫ doubleOriginLineImmersion k) ∧
      ¬ RegularIdealSheaf.IsRegularImmersion (simpleOriginImmersion k) ∧
      -- and at the level of ideals, to which Stacks tag 063G reduces them
      (∃ rs : List (Polynomial k),
        Ideal.ofList rs = doubleOriginIdeal k ∧ IsWeaklyRegular (Polynomial k) rs) ∧
      (∃ rs : List (Polynomial k),
        Ideal.ofList rs = simpleOriginIdeal k ∧ IsWeaklyRegular (Polynomial k) rs) ∧
      (¬ ∃ rs : List (DoubleOriginRing k),
        Ideal.ofList rs = doubleOriginPointIdeal k ∧
          IsWeaklyRegular (DoubleOriginRing k) rs)

Tag 0692, a lemma

Tag 0692 in the Stacks Project.

Stacks.AlgebraicGeometry.exists_smooth_surjective_regular_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/KoszulRegularSmoothCover.lean, line 493.

Stacks Project, Tag 0692. A Koszul-regular closed immersion becomes a regular immersion after a surjective smooth base change of its target.

Both conditions are stated with the classes of Stacks tag 063J, parts (2) and (1): RegularIdealSheaf.IsKoszulRegularImmersion and RegularIdealSheaf.IsRegularImmersion.

theorem exists_smooth_surjective_regular_baseChange {Z X : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] (hi : RegularIdealSheaf.IsKoszulRegularImmersion i) :
    ∃ (X' : Scheme.{u}) (g : X' ⟶ X),
      Surjective g ∧ Smooth g ∧
        RegularIdealSheaf.IsRegularImmersion (pullback.snd i g)

Tag 0E9J, a lemma

Tag 0E9J in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isRegularImmersion_of_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/ImmersionOfRegularSchemes.lean, line 65. References: EGA IV (19.7.5), “more general”.

Stacks tag 0E9J. An immersion between regular schemes is a regular immersion.

theorem isRegularImmersion_of_isRegular {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
    (hZ : AlgebraicGeometry.IsRegular Z) (hX : AlgebraicGeometry.IsRegular X) :
    IsRegularImmersion i

Sources

• Section 31.22, Tag 0638
• AxiomMath/Stacks at 5ed82d14

LeanStacks.AlgebraicGeometry.isRegularImmersion_iff_of_open · Stacks.AlgebraicGeometry.RegularIdealSheaf.IsRegularImmersion · Stacks.AlgebraicGeometry.RegularIdealSheaf.IsKoszulRegularImmersion · Stacks.AlgebraicGeometry.RegularIdealSheaf.IsH1RegularImmersion · Stacks.AlgebraicGeometry.RegularIdealSheaf.IsQuasiRegularImmersion · Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularIdealSheaf_definingIdealOfHom_congr · Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularIdealSheaf_definingIdealOfHom_congr · Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularIdealSheaf_definingIdealOfHom_congr

Section31.23 Relative regular immersions#

Section 31.23 of the Stacks Project, Tag 063P. 12 tags here are carried by 25 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 063R, a lemma

Tag 063R in the Stacks Project.

Stacks.AlgebraicGeometry.isQuasiRegularImmersion_baseChange_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/BaseChange.lean, line 369. The attribute's comment: “quasi_base_change”.

Stacks Project, Tag 063R, the quasi-regular half. A quasi-regular immersion whose source is flat over the base remains quasi-regular after any base change of the base scheme.

The H₁-regular half of the tag is Stacks.AlgebraicGeometry.isH1RegularImmersion_baseChange_of_flat, in StacksFrontier.AlgebraicGeometry.RegularImmersion.H1BaseChange.

theorem isQuasiRegularImmersion_baseChange_of_flat {S X Z S' : Scheme.{u}} (f : X ⟶ S)
    (i : Z ⟶ X) [IsImmersion i] [Flat (i ≫ f)] (hi : IsQuasiRegularImmersion i) (g : S' ⟶ S) :
    IsQuasiRegularImmersion (pullback.fst (pullback.snd g f) i)

Stacks.AlgebraicGeometry.isH1RegularImmersion_baseChange_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/H1BaseChange.lean, line 185. The attribute's comment: “h1_base_change”.

Stacks Project, Tag 063R, the H₁-regular half. An H₁-regular immersion whose source is flat over the base remains H₁-regular after any base change of the base scheme.

theorem isH1RegularImmersion_baseChange_of_flat {S X Z S' : Scheme.{u}} (f : X ⟶ S)
    (i : Z ⟶ X) [IsImmersion i] [Flat (i ≫ f)] (hi : IsH1RegularImmersion i) (g : S' ⟶ S) :
    IsH1RegularImmersion (pullback.fst (pullback.snd g f) i)

Tag 063S, a definition

Tag 063S in the Stacks Project.

AlgebraicGeometry.IsRelativeH1RegularImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/RelativeDefs.lean, line 49. The attribute's comment: “part (2): relative H₁-regular immersion”.

Part (2) of Stacks tag 063S. An immersion into a scheme over a base is a relative H₁-regular immersion when the immersed scheme is flat over the base and the immersion is H₁-regular.

abbrev IsRelativeH1RegularImmersion {Z X S : Scheme.{u}}
    (f : X ⟶ S) (i : Z ⟶ X) [IsImmersion i] : Prop

Stacks.AlgebraicGeometry.IsRelativeQuasiRegularImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/Basic.lean, line 84. The attribute's comment: “part (1): relative quasi-regular immersion”.

Part (1) of Stacks tag 063S. An immersion into a scheme over a base is a relative quasi-regular immersion when the immersed scheme is flat over the base and the immersion is quasi-regular.

abbrev IsRelativeQuasiRegularImmersion {Z X S : Scheme.{u}} (f : X ⟶ S) (i : Z ⟶ X)
    [IsImmersion i] : Prop

Tag 063T, a lemma

Tag 063T in the Stacks Project.

AlgebraicGeometry.isFlatAt_of_isRelativeQuasiRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/RelativeFlatness.lean, line 377.

Let f : X ⟶ S be a morphism of schemes and i : Z ⟶ X a relative quasi-regular immersion over S. Then f is flat at every point of the image of i whose local ring on X is Noetherian.

theorem isFlatAt_of_isRelativeQuasiRegularImmersion
    {X S Z : Scheme.{u}} (f : X ⟶ S) (i : Z ⟶ X) [IsImmersion i]
    (hi : IsRelativeQuasiRegularImmersion f i)
    (x : X) (hx : x ∈ Set.range i.base)
    (hNoetherian : IsNoetherianRing (X.presheaf.stalk x)) :
    IsFlatAt f.toLRSHom.toShHom x

Tag 063U, a lemma

Tag 063U in the Stacks Project.

Stacks.AlgebraicGeometry.isRegularImmersion_baseChange_of_isRelativeQuasiRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/BaseChange.lean, line 385. The attribute's comment: “regularity after arbitrary base change”. References: EGA IV (19.2.4), “c') => b')”.

Stacks Project, Tag 063U, regularity after an arbitrary base change. A relative quasi-regular immersion into a scheme flat and locally of finite presentation over the base remains a regular immersion after any change of the base.

The base change is again a relative quasi-regular immersion over S': its quasi-regularity is the quasi-regular half of Stacks tag 063R and the flatness of its source over S' is flat_comp_of_isPullback. Flatness and local finite presentation of S' ×_S X ⟶ S' are base changes of those of X ⟶ S. So the already-proved isRegularImmersion_of_isRelativeQuasiRegularImmersion applies over S'.

theorem isRegularImmersion_baseChange_of_isRelativeQuasiRegularImmersion {S X Z S' : Scheme.{u}}
    (f : X ⟶ S) (i : Z ⟶ X) [IsImmersion i] [Flat f] [LocallyOfFinitePresentation f]
    (hi : IsRelativeQuasiRegularImmersion f i) (g : S' ⟶ S) :
    IsRegularImmersion (pullback.fst (pullback.snd g f) i)

Stacks.AlgebraicGeometry.isRegularImmersion_of_isRelativeQuasiRegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RegularImmersion/Relative.lean, line 216. The attribute's comment: “regularity of the immersion”. References: EGA IV (19.2.4), “c') => c)”.

A relative quasi-regular immersion into a scheme flat and locally of finite presentation over the base is a regular immersion.

theorem isRegularImmersion_of_isRelativeQuasiRegularImmersion {S X Z : Scheme.{u}} (f : X ⟶ S)
    (i : Z ⟶ X) [IsImmersion i] [Flat f] [LocallyOfFinitePresentation f]
    (hi : IsRelativeQuasiRegularImmersion f i) : IsRegularImmersion i

Tag 0FUD, a remark

Tag 0FUD in the Stacks Project.

AlgebraicGeometry.isRegular_atPrime_baseChange_of_isQuasiRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/QuasiRegularBaseChange.lean, line 91. The attribute's comment: “regularity at primes after base change”.

Let A → B be flat and of finite presentation and let f₁, …, f_r ∈ B be a quasi-regular sequence whose quotient is flat over A. For any A-algebra A' and any prime q of B' = B ⊗_A A' containing the base-changed sequence, that sequence is regular in the local ring B'_q.

theorem isRegular_atPrime_baseChange_of_isQuasiRegular
    {A B A' : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [CommRing A'] [Algebra A A'] [Module.Flat A B]
    [Algebra.FinitePresentation A B] {r : ℕ} (f : Fin r → B)
    (hflat : Module.Flat A (B ⧸ Ideal.span (Set.range f)))
    (hf : IsQuasiRegular B (List.ofFn f))
    (q : Ideal (B ⊗[A] A')) [q.IsPrime]
    (hq : Ideal.span (Set.range (KoszulH1.fp (A := A) (A' := A') f)) ≤ q) :
    IsRegular (Localization.AtPrime q)
      ((List.ofFn (KoszulH1.fp (A := A) (A' := A') f)).map
        (algebraMap (B ⊗[A] A') (Localization.AtPrime q)))

Declarations registered for the tag:

• Koszul.quasiRegular_and_h1Regular_baseChange_of_quotient_flat, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/QuasiRegularBaseChange.lean, line 38 (StacksFrontier): “quasi-regularity and constant length after base change”.

Tag 063V, a lemma

Tag 063V in the Stacks Project.

Stacks.AlgebraicGeometry.exists_open_flat_of_isRelativeH1RegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/FlatNeighbourhood.lean, line 506. The attribute's comment: “part (1): flat open neighbourhood of a relative H₁-regular immersion”.

Let f : X ⟶ S be locally of finite presentation and let i : Z ⟶ X be a relative H₁-regular immersion over S. Then there is an open subscheme of X containing the image of Z on which f is flat.

theorem exists_open_flat_of_isRelativeH1RegularImmersion
    {S X Z : Scheme.{u}} (f : X ⟶ S) (i : Z ⟶ X) [IsImmersion i]
    [LocallyOfFinitePresentation f]
    (hi : AlgebraicGeometry.IsRelativeH1RegularImmersion f i) :
    ∃ U : X.Opens, Set.range i.base ⊆ (U : Set X) ∧ Flat (U.ι ≫ f)

Stacks.AlgebraicGeometry.isRegularImmersion_of_isRelativeH1RegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/FlatNeighbourhoodRegularity.lean, line 115. The attribute's comment: “part (2): the immersion is regular”.

Stacks Project, Tag 063V, part (2): the immersion is regular. A relative H₁-regular immersion into a scheme locally of finite presentation over the base is a regular immersion.

theorem isRegularImmersion_of_isRelativeH1RegularImmersion {S X Z : Scheme.{u}} (f : X ⟶ S)
    (i : Z ⟶ X) [IsImmersion i] [LocallyOfFinitePresentation f]
    (hi : AlgebraicGeometry.IsRelativeH1RegularImmersion f i) : IsRegularImmersion i

Stacks.AlgebraicGeometry.isRegularImmersion_baseChange_of_isRelativeH1RegularImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularImmersion/FlatNeighbourhoodRegularity.lean, line 126. The attribute's comment: “part (2): the immersion stays regular after any base change”.

Stacks Project, Tag 063V, part (2): regularity after an arbitrary base change. A relative H₁-regular immersion into a scheme locally of finite presentation over the base remains a regular immersion after any change of the base scheme.

theorem isRegularImmersion_baseChange_of_isRelativeH1RegularImmersion {S X Z S' : Scheme.{u}}
    (f : X ⟶ S) (i : Z ⟶ X) [IsImmersion i] [LocallyOfFinitePresentation f]
    (hi : AlgebraicGeometry.IsRelativeH1RegularImmersion f i) (g : S' ⟶ S) :
    IsRegularImmersion (pullback.fst (pullback.snd g f) i)

Tag 063W, a lemma

Tag 063W in the Stacks Project.

Stacks.AlgebraicGeometry.exists_mem_isRelativeQuasiRegularImmersion_le_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeRegularImmersion/Containing.lean, line 638. The attribute's comment: “item (1): containing”.

Stacks tag 063W, item (1). Let f : X ⟶ S be flat and locally of finite presentation, let T be a closed subscheme of X and let x be a point of T whose fibre over f x is a quasi-regular immersion near x. Then there is an open U ∋ x and a relative quasi-regular immersion Z ⊆ U over S with T ∩ U ⊆ Z and Z_s = T_s ∩ U_s.

theorem exists_mem_isRelativeQuasiRegularImmersion_le_comap (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (T : X.IdealSheafData) (x : X) (hx : x ∈ T.support)
    (hfib : ∃ V : (f.fiber (f x)).Opens, f.asFiber x ∈ V ∧ IsQuasiRegularImmersion
      (((T.comap (f.fiberι (f x))).comap V.ι).subschemeι)) :
    ∃ (U : X.Opens) (_ : x ∈ U) (Z : U.toScheme.IdealSheafData),
      IsRelativeQuasiRegularImmersion (U.ι ≫ f) Z.subschemeι ∧ Z ≤ T.comap U.ι ∧
        Z.comap ((f.fiberι (f x)).resLE U (f.fiberι (f x) ⁻¹ᵁ U) le_rfl)
          = (T.comap (f.fiberι (f x))).comap (f.fiberι (f x) ⁻¹ᵁ U).ι

Stacks.AlgebraicGeometry.exists_mem_isRelativeQuasiRegularImmersion_of_dim_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeRegularImmersion/EqualityEquationCount.lean, line 159. The attribute's comment: “item (3): equation count”.

Stacks tag 063W, item (3). Let f : X ⟶ S be flat and locally of finite presentation, let T be a closed subscheme of X and let x be a point of T such that the fibre of T over f x is a quasi-regular immersion on a neighbourhood of x. Assume that T is cut out on an affine open neighbourhood of x by n equations, and that n is the drop in local dimension from the fibre X_s to the fibre T_s at x. Then there is an open U ∋ x on which T itself is a relative quasi-regular immersion over S, and a regular immersion.

theorem exists_mem_isRelativeQuasiRegularImmersion_of_dim_eq (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (T : X.IdealSheafData) (x : X) (hx : x ∈ T.support)
    (hfib : ∃ V : (f.fiber (f x)).Opens, f.asFiber x ∈ V ∧ IsQuasiRegularImmersion
      (((T.comap (f.fiberι (f x))).comap V.ι).subschemeι))
    {n : ℕ} {U₀ : X.Opens} (hU₀ : IsAffineOpen U₀) (hxU₀ : x ∈ U₀) (g : Fin n → Γ(X, U₀))
    (hg : T.ideal ⟨U₀, hU₀⟩ = Ideal.span (Set.range g))
    (hdim : topologicalKrullDimAt (T.comap (f.fiberι (f x))).subscheme
          ⟨f.asFiber x, asFiber_mem_support_comap f T x hx⟩ + (n : WithBot ℕ∞)
        = topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x)) :
    ∃ U : X.Opens, x ∈ U ∧
      IsRelativeQuasiRegularImmersion (U.ι ≫ f) (T.comap U.ι).subschemeι ∧
        IsRegularImmersion (T.comap U.ι).subschemeι

Stacks.AlgebraicGeometry.exists_mem_isRelativeQuasiRegularImmersion_of_flatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeRegularImmersion/EqualityFlat.lean, line 71. The attribute's comment: “equality_flat”. References: EGA IV (19.2.4), “b) => c)”.

Stacks tag 063W, item (2). Let f : X ⟶ S be flat and locally of finite presentation, let T be a closed subscheme of X whose closed immersion into X is locally of finite presentation, and let x be a point of T such that the fibre of T over f x is a quasi-regular immersion on a neighbourhood of x and T is flat over S at x. Then there is an open U ∋ x on which T itself is a relative quasi-regular immersion over S, and a regular immersion.

theorem exists_mem_isRelativeQuasiRegularImmersion_of_flatAt {X S : Scheme.{u}} (f : X ⟶ S)
    [Flat f] [LocallyOfFinitePresentation f] (T : X.IdealSheafData)
    [LocallyOfFinitePresentation T.subschemeι] (x : X) (hx : x ∈ T.support)
    (hfib : ∃ V : (f.fiber (f x)).Opens, f.asFiber x ∈ V ∧
      IsQuasiRegularImmersion (((T.comap (f.fiberι (f x))).comap V.ι).subschemeι))
    (hflat : ((T.subschemeι ≫ f).stalkMap (⟨x, hx⟩ : T.subscheme)).hom.Flat) :
    ∃ U : X.Opens, x ∈ U ∧
      IsRelativeQuasiRegularImmersion (U.ι ≫ f) (T.comap U.ι).subschemeι ∧
        IsRegularImmersion (T.comap U.ι).subschemeι

Stacks.AlgebraicGeometry.isRelativeQuasiRegularImmersion_subschemeι_of_forall_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeRegularImmersion/Fibrewise.lean, line 82. The attribute's comment: “fibrewise criterion”.

The fibrewise criterion of Stacks tag 063W. Let f : X ⟶ S be flat and locally of finite presentation and let T be a closed subscheme of X which is flat and locally of finite presentation over S. If every fibre of T is a quasi-regular closed subscheme of the corresponding fibre of X, then T is a relative quasi-regular immersion over S.

theorem isRelativeQuasiRegularImmersion_subschemeι_of_forall_fiber (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (T : X.IdealSheafData) [Flat (T.subschemeι ≫ f)]
    [LocallyOfFinitePresentation (T.subschemeι ≫ f)]
    (hfib : ∀ s : S, IsQuasiRegularImmersion (T.comap (f.fiberι s)).subschemeι) :
    IsRelativeQuasiRegularImmersion f T.subschemeι

Tag 067R, a lemma

Tag 067R in the Stacks Project.

Stacks.AlgebraicGeometry.isRegularImmersion_of_smooth_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Relative/SmoothSection.lean, line 65. References: EGA IV (17.12.3), “necessity”; SGA 6 VII (1.10), “section case”; SGA 6 VII (4.2), “more general”; SGA 6 VIII (1.3), “more general”; SGA 6 VIII (2.4), “special case”.

Stacks Project, Tag 067R. A section σ of a smooth morphism f : X ⟶ S of schemes is a regular immersion.

theorem isRegularImmersion_of_smooth_section (f : X ⟶ S) [Smooth f] (σ : S ⟶ X)
    (hσ : σ ≫ f = 𝟙 S) :
    letI : IsImmersion σ := isImmersion_of_comp_eq_id σ f hσ
    IsRegularImmersion σ

Tag 067S, a lemma

Tag 067S in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isRegularImmersion_of_comp_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SmoothPermanence.lean, line 81. The attribute's comment: “regular”.

Stacks 067S for regular immersions. If the composite of an immersion with a smooth morphism is regular, the immersion is regular.

theorem isRegularImmersion_of_comp_of_smooth
    (i : Y ⟶ X) (f : X ⟶ S) [IsImmersion i] [IsImmersion (i ≫ f)] [Smooth f]
    (hj : IsRegularImmersion (i ≫ f)) : IsRegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularImmersion_of_comp_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SmoothPermanence.lean, line 103. The attribute's comment: “koszul_regular”.

Stacks 067S for Koszul-regular immersions. If the composite of an immersion with a smooth morphism is Koszul-regular, the immersion is Koszul-regular.

theorem isKoszulRegularImmersion_of_comp_of_smooth
    (i : Y ⟶ X) (f : X ⟶ S) [IsImmersion i] [IsImmersion (i ≫ f)] [Smooth f]
    (hj : IsKoszulRegularImmersion (i ≫ f)) : IsKoszulRegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularImmersion_of_comp_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SmoothPermanence.lean, line 130. The attribute's comment: “h1_regular”.

Stacks 067S for H₁-regular immersions. If the composite of an immersion with a smooth morphism is H₁-regular, the immersion is H₁-regular.

theorem isH1RegularImmersion_of_comp_of_smooth
    (i : Y ⟶ X) (f : X ⟶ S) [IsImmersion i] [IsImmersion (i ≫ f)] [Smooth f]
    (hj : IsH1RegularImmersion (i ≫ f)) : IsH1RegularImmersion i

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularImmersion_of_comp_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SmoothPermanence.lean, line 147. The attribute's comment: “quasi_regular”.

Stacks 067S for quasi-regular immersions. If the composite of an immersion with a smooth morphism is quasi-regular, the immersion is quasi-regular.

theorem isQuasiRegularImmersion_of_comp_of_smooth
    (i : Y ⟶ X) (f : X ⟶ S) [IsImmersion i] [IsImmersion (i ≫ f)] [Smooth f]
    (hj : IsQuasiRegularImmersion (i ≫ f)) : IsQuasiRegularImmersion i

Tag 067T, a lemma

Tag 067T in the Stacks Project.

Stacks.AlgebraicGeometry.isRegularImmersion_of_syntomic_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeRegularImmersion/SyntomicIntoSmooth.lean, line 82. References: SGA 6 VII (1.10), “more general”.

Stacks Project, Tag 067T. Let i : Y ⟶ X be an immersion and f : X ⟶ S a smooth morphism such that the structure morphism i ≫ f of Y over S is syntomic. Then i is a regular immersion.

theorem isRegularImmersion_of_syntomic_of_smooth [IsImmersion i] [Smooth f]
    (h : Syntomic (i ≫ f)) : IsRegularImmersion i

Tag 067U, a lemma

Tag 067U in the Stacks Project.

Stacks.AlgebraicGeometry.isRegularImmersion_of_smooth_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RelativeRegularImmersion/SyntomicIntoSmooth.lean, line 135. References: SGA 6 VII (1.10); SGA 1 II (4.16), “X smooth ⇒ i regular”; SGA 6 VIII (1.1), “more general”; SGA 6 VIII (1.3), “more general”; SGA 6 VIII (1.8), “partial, special case”; SGA 6 VIII (2.4), “special case”.

Stacks Project, Tag 067U. An immersion i : Y ⟶ X between two schemes smooth over S is a regular immersion. This is the case of Stacks tag 067T in which the structure morphism of Y is smooth, a smooth morphism being syntomic (Stacks tag 01VD).

theorem isRegularImmersion_of_smooth_of_smooth [IsImmersion i] [Smooth f] [Smooth (i ≫ f)] :
    IsRegularImmersion i

Tag 0693, a lemma

Tag 0693 in the Stacks Project.

Stacks.AlgebraicGeometry.RegularIdealSheaf.isKoszulRegularImmersion_comp_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SmoothTargetPermanence.lean, line 481. The attribute's comment: “koszul_regular”.

Stacks tag 0693 for Koszul-regular immersions. In a commutative triangle Y ⟶ X ⟶ S with X ⟶ S smooth and both Y ⟶ X and Y ⟶ S immersions, the composite Y ⟶ S of a Koszul-regular immersion Y ⟶ X is a Koszul-regular immersion.

Koszul-regularity is local on the source, and near a point of Y the immersion into X is pushed into a relative affine space 𝔸ⁿ_V over an affine open V ⊆ S. Shrinking V to an affine open T over which Y is closed, the lifted coordinates of that chart define a section σ of 𝔸ⁿ_V ⟶ V over T through which the chart factors, and Stacks tag 068Z for the retracted immersion σ descends Koszul-regularity to Y ⟶ T.

theorem isKoszulRegularImmersion_comp_of_smooth (i : Y ⟶ X) (f : X ⟶ S) [IsImmersion i]
    [IsImmersion (i ≫ f)] [Smooth f] (hi : IsKoszulRegularImmersion i) :
    IsKoszulRegularImmersion (i ≫ f)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isH1RegularImmersion_comp_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SmoothTargetPermanence.lean, line 549. The attribute's comment: “h1_regular”.

Stacks tag 0693 for H₁-regular immersions. In a commutative triangle Y ⟶ X ⟶ S with X ⟶ S smooth and both Y ⟶ X and Y ⟶ S immersions, the composite Y ⟶ S of an H₁-regular immersion Y ⟶ X is an H₁-regular immersion.

H₁-regularity is local on the source, and near a point of Y the immersion into X is pushed into a relative affine space 𝔸ⁿ_V over an affine open V ⊆ S. Shrinking V to an affine open T over which Y is closed, the lifted coordinates of that chart define a section σ of 𝔸ⁿ_V ⟶ V over T through which the chart factors, and Stacks tag 068Z for the retracted immersion σ descends H₁-regularity to Y ⟶ T.

theorem isH1RegularImmersion_comp_of_smooth (i : Y ⟶ X) (f : X ⟶ S) [IsImmersion i]
    [IsImmersion (i ≫ f)] [Smooth f] (hi : IsH1RegularImmersion i) :
    IsH1RegularImmersion (i ≫ f)

Stacks.AlgebraicGeometry.RegularIdealSheaf.isQuasiRegularImmersion_comp_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/RegularImmersion/SmoothTargetQuasiRegular.lean, line 260. The attribute's comment: “quasi_regular”.

Smooth postcomposition. In a commutative triangle Y ⟶ X ⟶ S with X ⟶ S smooth and both Y ⟶ X and Y ⟶ S immersions, the composite Y ⟶ S of a quasi-regular immersion Y ⟶ X is a quasi-regular immersion.

theorem isQuasiRegularImmersion_comp_of_smooth {Y X S : Scheme.{u}} (i : Y ⟶ X) (f : X ⟶ S)
    [IsImmersion i] [IsImmersion (i ≫ f)] [Smooth f] (hi : IsQuasiRegularImmersion i) :
    IsQuasiRegularImmersion (i ≫ f)

Sources

• Section 31.23, Tag 063P
• AxiomMath/Stacks at 5ed82d14

LeanStacks.AlgebraicGeometry.isQuasiRegularImmersion_baseChange_of_flat · Stacks.AlgebraicGeometry.isH1RegularImmersion_baseChange_of_flat · AlgebraicGeometry.IsRelativeH1RegularImmersion · Stacks.AlgebraicGeometry.IsRelativeQuasiRegularImmersion · AlgebraicGeometry.isFlatAt_of_isRelativeQuasiRegularImmersion · Stacks.AlgebraicGeometry.isRegularImmersion_baseChange_of_isRelativeQuasiRegularImmersion · Stacks.AlgebraicGeometry.isRegularImmersion_of_isRelativeQuasiRegularImmersion · AlgebraicGeometry.isRegular_atPrime_baseChange_of_isQuasiRegular

Section31.24 Meromorphic functions and sections#

Section 31.24 of the Stacks Project, Tag 01X1. 10 tags here are carried by 47 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01X2, a definition

Tag 01X2 in the Stacks Project.

AlgebraicGeometry.MeromorphicFunction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TotalQuotient.lean, line 70. The attribute's comment: “a meromorphic function”. References: EGA IV (20.1.3), “M(X)”.

A meromorphic function on a locally ringed space is a global section of its sheaf of meromorphic functions, the sheaf of total quotient rings of its structure sheaf.

abbrev MeromorphicFunction (O : TopCat.Sheaf CommRingCat.{u} X) : Type u

Declarations registered for the tag:

• totalQuotientSheaf registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TotalQuotient.lean, line 138 (StacksFrontier): “the sheaf of meromorphic functions”.

Tag 01X3, an example

Tag 01X3 in the Stacks Project.

AlgebraicGeometry.NoChange.noChangeRing, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/NoChange.lean, line 71. The attribute's comment: “the ring”.

The ring ℂ[x, {y_α}]/((x-α)y_α, y_α y_β).

abbrev noChangeRing

AlgebraicGeometry.NoChange.normalForm_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/NoChange.lean, line 479. The attribute's comment: “unique normal form”.

Every element of the example ring has a unique displayed normal form.

theorem normalForm_bijective : Function.Bijective normalForm

AlgebraicGeometry.NoChange.isUnit_of_isRegular_localizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/NoChange.lean, line 487. The attribute's comment: “nonzerodivisors on principal opens”.

On every principal open of Spec A, a nonzerodivisor is a unit.

theorem isUnit_of_isRegular_localizationAway (f : noChangeRing)
    (a : Localization.Away f) (ha : IsRegular a) : IsUnit a

AlgebraicGeometry.NoChange.isIso_toTotalQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/NoChange.lean, line 676. The attribute's comment: “equality of sheaves”.

The canonical map from the structure sheaf of Spec A to its sheaf of meromorphic functions is an isomorphism.

theorem isIso_toTotalQuotientSheaf :
    IsIso (Scheme.toTotalQuotientSheaf
      (Spec (.of noChangeRing)))

Tag 01X4, a definition

Tag 01X4 in the Stacks Project.

AlgebraicGeometry.meromorphicSectionSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/MeromorphicSections.lean, line 61. The attribute's comment: “part (1)”. References: EGA IV (20.1.3), “M_X(F)”.

The sheaf K_X(F) of meromorphic sections of F, obtained by extension of scalars from O to its sheaf of total quotient rings.

noncomputable abbrev meromorphicSectionSheaf (O : TopCat.Sheaf CommRingCat.{u} X)
    (F : SheafOfModules.{max u z} (Stacks.Sheaves.Differentials.ringSheaf (C := Opens X)
      (J := Opens.grothendieckTopology X) O)) :
    SheafOfModules.{max u z} (Stacks.Sheaves.Differentials.ringSheaf (C := Opens X)
      (J := Opens.grothendieckTopology X) (totalQuotientSheaf (X := X) O))

AlgebraicGeometry.MeromorphicSection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/MeromorphicSections.lean, line 75. The attribute's comment: “part (2)”. References: EGA IV (20.1.3), “M(X,F)”.

A meromorphic section of F is a global section of K_X(F).

abbrev MeromorphicSection (O : TopCat.Sheaf CommRingCat.{u} X)
    (F : SheafOfModules.{max u z} (Stacks.Sheaves.Differentials.ringSheaf (C := Opens X)
      (J := Opens.grothendieckTopology X) O))

Tag 02OT, a definition

Tag 02OT in the Stacks Project.

AlgebraicGeometry.PullbacksMeromorphicSections, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/Pullback.lean, line 105. References: EGA IV (20.1.11), “M_f = M_X condition”.

Pullbacks of meromorphic functions are defined for f when the pullback to every compatible pair of opens sends regular sections of the target structure sheaf to regular sections of the source structure sheaf.

noncomputable abbrev PullbacksMeromorphicSections
    {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) : Prop

Tag 02OU, a lemma

Tag 02OU in the Stacks Project.

AlgebraicGeometry.pullbacksMeromorphicSections_of_mapsTo_genericPoints, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PullbackCriteria.lean, line 86. The attribute's comment: “weakly_associated”.

If a morphism of schemes maps every weakly associated point of its source to the generic point of an irreducible component of its target, then pullbacks of meromorphic functions are defined for the morphism.

lemma pullbacksMeromorphicSections_of_mapsTo_genericPoints
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    (hf : Set.MapsTo f (Stacks.Divisors.schemeWeaklyAssociatedPoints X) (genericPoints Y)) :
    PullbacksMeromorphicSections f.1

AlgebraicGeometry.pullbacksMeromorphicSections_of_reduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PullbackCriteria.lean, line 127. The attribute's comment: “reduced_source”.

Stacks Project, Tag 02OU (reduced source). If a morphism from a reduced scheme sends every generic point of an irreducible component to a generic point of an irreducible component, then pullbacks of meromorphic functions along it are defined.

theorem pullbacksMeromorphicSections_of_reduced {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsReduced X] (hf : Set.MapsTo f (genericPoints X) (genericPoints Y)) :
    PullbacksMeromorphicSections f.toLRSHom

AlgebraicGeometry.pullbacksMeromorphicSections_of_isIntegral, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PullbackCriteria.lean, line 137. The attribute's comment: “integral_source”.

Stacks Project, Tag 02OU (integral source). If the source of a morphism of schemes is integral and its generic point maps to a generic point of an irreducible component of the target, then pullbacks of meromorphic functions are defined.

lemma pullbacksMeromorphicSections_of_isIntegral
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegral X]
    (h : f (genericPoint X) ∈ genericPoints Y) :
    PullbacksMeromorphicSections f.toLRSHom

AlgebraicGeometry.pullbacksMeromorphicSections_of_isDominant, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PullbackCriteria.lean, line 146. The attribute's comment: “dominant_integral”. References: EGA IV (21.4.5), “(iii), X,X' integral”.

Stacks Project, Tag 02OU. Pullbacks of meromorphic functions are defined along a dominant morphism between integral schemes.

lemma pullbacksMeromorphicSections_of_isDominant
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegral X] [IsIntegral Y] [IsDominant f] :
    PullbacksMeromorphicSections f.toLRSHom

AlgebraicGeometry.pullbacksMeromorphicSections_of_associatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PullbackCriteria.lean, line 158. The attribute's comment: “associated_points”. References: EGA IV (21.4.5), “(ii), to generic points”.

Stacks Project, Tag 02OU (associated points). If every associated point of a locally Noetherian source scheme maps to the generic point of an irreducible component of the target, then pullbacks of meromorphic functions are defined.

theorem pullbacksMeromorphicSections_of_associatedPoints
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian X]
    (h : ∀ x ∈ Stacks.Divisors.schemeAssociatedPoints X,
      ∃ Z ∈ irreducibleComponents Y, IsGenericPoint (f x) Z) :
    PullbacksMeromorphicSections f.toLRSHom

AlgebraicGeometry.pullbacksMeromorphicSections_of_noEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PullbackCriteria.lean, line 175. The attribute's comment: “no_embedded_points”.

Stacks Project, Tag 02OU (no embedded points). If a morphism from a locally Noetherian scheme without embedded points sends every generic point of an irreducible component to a generic point of an irreducible component, then pullbacks of meromorphic functions along it are defined.

theorem pullbacksMeromorphicSections_of_noEmbeddedPoints
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsLocallyNoetherian X]
    (hX : AlgebraicGeometry.HasNoEmbeddedPoints X)
    (hf : Set.MapsTo f (genericPoints X) (genericPoints Y)) :
    PullbacksMeromorphicSections f.toLRSHom

AlgebraicGeometry.pullbacksMeromorphicSections_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/PullbackCriteria.lean, line 197. The attribute's comment: “flat”. References: EGA IV (21.4.5), “(i)”.

Pullbacks of meromorphic functions are defined along a flat morphism of schemes.

theorem pullbacksMeromorphicSections_of_flat
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] :
    PullbacksMeromorphicSections f.toLRSHom

Tag 0EMF, a lemma

Tag 0EMF in the Stacks Project.

AlgebraicGeometry.regularSectionGerms_eq_nonZeroDivisors_of_weaklyAssociatedPoints_subset_genericPoints, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/StalksWeaklyAssociated.lean, line 139. The attribute's comment: “regular_elements_in_stalks”.

If weakly associated points are generic points of irreducible components and quasi-compact opens have finitely many irreducible components, then the germs of regular sections at every point are exactly the nonzerodivisors in its local ring.

lemma regularSectionGerms_eq_nonZeroDivisors_of_weaklyAssociatedPoints_subset_genericPoints
    (X : Scheme.{u})
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ (U : X.Opens), IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) :
    (⨆ (U : Opens X) (hx : x ∈ U),
      ((X.presheaf.submonoidPresheafOfStalk
        (fun y ↦ nonZeroDivisors (X.presheaf.stalk y))).obj (Opposite.op U)).map
          (X.presheaf.germ U x hx).hom) =
      nonZeroDivisors (X.presheaf.stalk x)

AlgebraicGeometry.stalk_totalQuotientPresheaf_isFractionRing_of_weaklyAssociatedPoints_subset_genericPoints, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/StalksWeaklyAssociated.lean, line 183. The attribute's comment: “stalk_total_quotient_ring”.

If every weakly associated point of a scheme is a generic point of an irreducible component and every quasi-compact open has finitely many irreducible components, then the stalk of the presheaf of meromorphic functions at any point is the total quotient ring of the local ring.

lemma stalk_totalQuotientPresheaf_isFractionRing_of_weaklyAssociatedPoints_subset_genericPoints
    (X : Scheme.{u})
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ (U : X.Opens), IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) :
    letI : Algebra (X.presheaf.stalk x) (X.presheaf.totalQuotientPresheaf.stalk x) :=
      ((TopCat.Presheaf.stalkFunctor CommRingCat x).map
        X.presheaf.toTotalQuotientPresheaf).hom.toAlgebra
    IsFractionRing (X.presheaf.stalk x) (X.presheaf.totalQuotientPresheaf.stalk x)

AlgebraicGeometry.stalk_totalQuotientSheaf_isFractionRing_of_weaklyAssociated, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/TotalQuotientSheafStalks.lean, line 85. The attribute's comment: “stalk_total_quotient_ring”.

If every weakly associated point of a scheme is a generic point of an irreducible component and every quasi-compact open has finitely many irreducible components, then the stalk K_{X, x} of the sheaf of meromorphic functions at any point is the total quotient ring of the local ring 𝒪_{X, x}.

lemma stalk_totalQuotientSheaf_isFractionRing_of_weaklyAssociated
    (X : Scheme.{u})
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ (U : X.Opens), IsCompact (U : Set X) → (irreducibleComponents U).Finite)
    (x : X) :
    letI : Algebra (X.presheaf.stalk x) (X.totalQuotientSheaf.presheaf.stalk x) :=
      ((TopCat.Presheaf.stalkFunctor CommRingCat x).map
        X.toTotalQuotientSheaf.hom).hom.toAlgebra
    IsFractionRing (X.presheaf.stalk x) (X.totalQuotientSheaf.presheaf.stalk x)

AlgebraicGeometry.isIso_toGenericPointStalkProduct, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Basic.lean, line 268. The attribute's comment: “generic_point_decomposition”.

The comparison map of sheaves of rings is an isomorphism: it is so on stalks, because the presheaf-level comparison is bijective on the affine opens and the sheafification unit is an isomorphism on stalks.

lemma isIso_toGenericPointStalkProduct
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite) :
    IsIso (toGenericPointStalkProduct X)

AlgebraicGeometry.meromorphicFunctions_iso_product_genericPointStalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Basic.lean, line 363. The attribute's comment: “generic_point_decomposition”.

Stacks 0EMF. The 𝒪_X-module of meromorphic functions is the product of the pushed-forward structure sheaves of the local schemes at the generic points of the irreducible components, for a scheme whose weakly associated points are generic points of irreducible components and whose quasi-compact opens have finitely many irreducible components.

theorem meromorphicFunctions_iso_product_genericPointStalks
    (X : Scheme.{u})
    (hassoc : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ U : X.Opens, IsCompact (U : Set X) →
      (irreducibleComponents U).Finite) :
    Nonempty (meromorphicFunctions X ≅
      ∏ᶜ fun η : genericPoints X ↦ genericPointStalkModule X η)

AlgebraicGeometry.meromorphicFunctions_iso_coproduct_genericPointStalks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Coproduct.lean, line 247. The attribute's comment: “generic_point_decomposition”.

Stacks 0EMF, displayed direct-sum decomposition. For a scheme whose weakly associated points are generic points of irreducible components and whose quasi-compact opens have finitely many irreducible components, the 𝒪_X-module of meromorphic functions is the direct sum over the generic points of the irreducible components of the pushed-forward structure sheaves of the spectra of the local rings there.

theorem meromorphicFunctions_iso_coproduct_genericPointStalks (X : Scheme.{u})
    (hassoc : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite) :
    Nonempty (meromorphicFunctions X ≅
      ∐ fun η : genericPoints X ↦ genericPointStalkModule X η)

AlgebraicGeometry.isLocalization_totalQuotientSheaf_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 185. The attribute's comment: “part (5)”.

Part (5) of [Stacks, Tag 0EMF]. On an affine open U of a scheme whose weakly associated points are generic points of irreducible components and whose quasi-compact opens have finitely many irreducible components, the sections K_X(U) of the sheaf of meromorphic functions — not only those of the presheaf — are the total quotient ring of Γ(X, U), that is, its localization at its nonzerodivisors.

theorem isLocalization_totalQuotientSheaf_obj
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite)
    {U : X.Opens} (hU : IsAffineOpen U) :
    letI : Algebra Γ(X, U) (X.totalQuotientSheaf.obj.obj (op U)) :=
      (X.toTotalQuotientSheaf.hom.app (op U)).hom.toAlgebra
    IsLocalization (nonZeroDivisors Γ(X, U)) (X.totalQuotientSheaf.obj.obj (op U))

AlgebraicGeometry.nonempty_meromorphicSections_iso_pi_genericPointStalkModuleOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 624. The attribute's comment: “part (2), product”.

Part (2) of [Stacks, Tag 0EMF], the product decomposition. For a quasi-coherent module F on a scheme whose weakly associated points are generic points of irreducible components and whose quasi-compact opens have finitely many irreducible components, the sheaf K_X(F) of meromorphic sections of F is the product over the generic points of the irreducible components of the generic-point contributions.

theorem nonempty_meromorphicSections_iso_pi_genericPointStalkModuleOf
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite)
    (F : X.Modules) [F.IsQuasicoherent] :
    Nonempty (meromorphicSections X F ≅
      ∏ᶜ fun η : genericPoints X ↦ genericPointStalkModuleOf X F η)

AlgebraicGeometry.nonempty_meromorphicSections_iso_sigma_genericPointStalkModuleOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 636. The attribute's comment: “part (2), direct sum”.

Part (2) of [Stacks, Tag 0EMF], the direct-sum decomposition. The family of generic-point contributions is locally finite, so the product of the previous theorem is also their direct sum.

theorem nonempty_meromorphicSections_iso_sigma_genericPointStalkModuleOf
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite)
    (F : X.Modules) [F.IsQuasicoherent] :
    Nonempty (meromorphicSections X F ≅
      ∐ fun η : genericPoints X ↦ genericPointStalkModuleOf X F η)

AlgebraicGeometry.meromorphicSections_isQuasicoherent_of_genericHypotheses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicGenericPointDecomposition/Globalization.lean, line 649. The attribute's comment: “part (2), quasi-coherence”.

Part (2) of [Stacks, Tag 0EMF], quasi-coherence. The sheaf K_X(F) of meromorphic sections of a quasi-coherent module F is quasi-coherent, being the product of the generic-point contributions.

theorem meromorphicSections_isQuasicoherent_of_genericHypotheses
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite)
    (F : X.Modules) [F.IsQuasicoherent] :
    (meromorphicSections X F).IsQuasicoherent

Stacks.AlgebraicGeometry.MeromorphicQuasicoherent.meromorphicFunctions_isQuasicoherent_of_genericHypotheses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MeromorphicQuasicoherent/Criteria.lean, line 60. The attribute's comment: “part (1)”.

Part (1) of [Stacks, Tag 0EMF]. On a scheme whose weakly associated points are generic points of irreducible components and whose quasi-compact opens have finitely many irreducible components, the sheaf of meromorphic functions is quasi-coherent: it is then the product of the generic-point contributions, and that product is quasi-coherent.

theorem meromorphicFunctions_isQuasicoherent_of_genericHypotheses {X : Scheme.{u}}
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfin : ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents (U : Set X)).Finite) :
    (meromorphicFunctions X).IsQuasicoherent

AlgebraicGeometry.exists_commRing_rationalFunctions_ringEquiv_totalQuotientSheaf_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RationalFunctions/Meromorphic.lean, line 608. The attribute's comment: “part (6)”. References: EGA I (7.1.3), “special case”.

Part (6) of [Stacks, Tag 0EMF], with the commutative ring structure on the rational functions constructed rather than assumed: it is transported from the global sections of the sheaf of total quotient rings along the bijection, and every section on a dense open set is a ring homomorphism to it, which is the characterization of [Stacks, Tag 01RU].

theorem exists_commRing_rationalFunctions_ringEquiv_totalQuotientSheaf_top (X : Scheme.{u})
    (hass : Stacks.Divisors.schemeWeaklyAssociatedPoints X ⊆ genericPoints X)
    (hfinite : ∀ V : X.Opens, IsCompact (V : Set X) → (irreducibleComponents V).Finite) :
    ∃ _ : CommRing X.rationalFunctions,
      (∀ (U : X.Opens) (hU : Dense (U : Set X)),
          ∃ ψ : Γ(X, U) →+* X.rationalFunctions,
            ∀ s, ψ s = X.rationalFunctionOfSection U hU s) ∧
        Nonempty (X.rationalFunctions ≃+* X.totalQuotientSheaf.presheaf.obj (op ⊤))

Tag 02OX, a definition

Tag 02OX in the Stacks Project.

AlgebraicGeometry.IsRegularMeromorphicSection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/MeromorphicSections.lean, line 83. References: EGA IV (20.1.8), “regular section defn”.

A meromorphic section is regular if its induced map from the total quotient sheaf to the meromorphic section sheaf is injective.

noncomputable abbrev IsRegularMeromorphicSection (O : TopCat.Sheaf CommRingCat.{u} X)
    (L : SheafOfModules.{u} (Stacks.Sheaves.Differentials.ringSheaf (C := Opens X)
      (J := Opens.grothendieckTopology X) O))
    (s : MeromorphicSection O L) : Prop

Tag 02OY, a lemma

Tag 02OY in the Stacks Project.

AlgebraicGeometry.pullbackMeromorphicSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/SectionPullback.lean, line 216. The attribute's comment: “part (1)”. References: EGA IV (20.1.11), “mero section pullback”.

The canonical pullback map on meromorphic sections. When pullbacks of meromorphic functions are defined for f, a meromorphic section of a sheaf of 𝒪_Y-modules F pulls back to a meromorphic section of f^* F: apply the morphism 𝒦_Y(F) ⟶ f_* 𝒦_X(f^* F) and read the resulting global section over the whole of X.

noncomputable def pullbackMeromorphicSection (s : MeromorphicSection Y.sheaf F) :
    MeromorphicSection X.sheaf
      ((RingedSpaceModuleAdjunction.modulePullback f.toShHom).obj F)

AlgebraicGeometry.isRegularMeromorphicSection_pullbackMeromorphicSection_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/SectionPullbackRegularGeneral.lean, line 49. The attribute's comment: “part (2)”.

Stacks 02OY part (2). Let f : X ⟶ Y be a morphism of locally ringed spaces for which pullbacks of meromorphic functions are defined and let L be an invertible 𝒪_Y-module. The pullback of a regular meromorphic section of L is a regular meromorphic section of f^* L.

theorem isRegularMeromorphicSection_pullbackMeromorphicSection_of_isInvertible
    {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) (hf : PullbacksMeromorphicSections f)
    (L : SheafOfModules.{u} Y.ringCatSheaf)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.property L)
    (s : MeromorphicSection Y.sheaf L) (hs : IsRegularMeromorphicSection Y.sheaf L s) :
    IsRegularMeromorphicSection X.sheaf
      ((RingedSpaceModuleAdjunction.modulePullback f.toShHom).obj L)
      (pullbackMeromorphicSection f hf L s)

Tag 02P0, a lemma

Tag 02P0 in the Stacks Project.

Stacks.DenominatorIdeal.denominatorIdeal_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DenominatorIdeal/Basic.lean, line 117. The attribute's comment: “the denominator rule”.

A section of the structure sheaf is a denominator of the meromorphic section s exactly when its product with s is a section of L.

theorem denominatorIdeal_sections (U : Opens X)
    (f : (SheafOfModules.unit (O X)).val.obj (op U)) :
    (∃ d : (denominatorIdeal X L s).val.obj (op U),
      (denominatorIdealι X L s).val.app (op U) d = f) ↔
    (∃ t : L.val.obj (op U),
      (sectionMap X L s).val.app (op U) f =
        (toK X L).val.app (op U) t)

Stacks.DenominatorIdeal.denominatorIdeal_section_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DenominatorIdeal/Basic.lean, line 167. The attribute's comment: “multiplication is injective”.

Multiplication by a regular meromorphic section embeds its denominator ideal in L.

theorem denominatorIdeal_section_mono (hs : IsRegularMeromorphicSection X.sheaf L s) :
    Mono (denominatorIdealMul X L s)

Stacks.DenominatorIdealInvertible.denominatorIdeal_inclusion_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DenominatorIdealInvertible/Basic.lean, line 140. The attribute's comment: “inclusion is injective”.

The denominator ideal of a meromorphic section of an invertible sheaf embeds in the structure sheaf. Stacks Tag 02P0, "inclusion is injective".

theorem denominatorIdeal_inclusion_mono (s : MeromorphicSection.{u, u} X.sheaf L)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf (O X).property L) :
    Mono (denominatorIdealι X L s)

Stacks.DenominatorIdealQcoh.denominatorIdeal_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DenominatorIdealQcoh/Basic.lean, line 276. The attribute's comment: “quasi-coherence”. References: EGA IV (20.2.14), “special case”.

The denominator ideal of a meromorphic section of an invertible sheaf is quasi-coherent.

Around every point there is an affine open V on which the denominator ideal is the colon ideal (b Γ(X, V) : a) for a nonzerodivisor b and a numerator a, and the colon ideal commutes with localization, so the sections over each basic open of V are the localization of the sections over V. Those affine opens cover X, and quasi-coherence is detected by that condition on the members of a cover.

theorem denominatorIdeal_isQuasicoherent
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf (O X).property L) :
    (denominatorIdeal X L s).IsQuasicoherent

Stacks.DenominatorIdealQcoh.denominatorIdealData_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DenominatorIdealQcoh/IdealData.lean, line 189. The attribute's comment: “affine denominator ideal”.

On each affine open the ideal-sheaf data are exactly the denominators.

Scheme.IdealSheafData.ofIdeals is a supremum and in general shrinks the family of ideals it is applied to; it does not here, because quasi-coherence of the denominator ideal makes that family compatible with passage to a basic open, so it is already an ideal sheaf.

theorem denominatorIdealData_ideal
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf (O X).property L)
    (U : X.affineOpens) :
    (denominatorIdealData X L s).ideal U =
      ((denominatorIdealι X L s).val.app (op U.1)).hom.range

Stacks.DenominatorIdealQcoh.denominatorIdealData_support_isNowhereDense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DenominatorIdealQcoh/IdealData.lean, line 204. The attribute's comment: “support of the denominator ideal”.

The closed support of the denominator ideal is nowhere dense.

Around every point of every open set there is an affine open carrying a nonzerodivisor b which is a denominator of s, so (b) ⊆ I there and the support is contained in V(b), which has empty interior. Shrinking freely is legitimate because the nowhere-density argument runs on an affine open of its own choosing inside the interior of the support.

theorem denominatorIdealData_support_isNowhereDense
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf (O X).property L) :
    IsNowhereDense ((denominatorIdealData X L s).support : Set X)

Stacks.DenominatorCokernel.denominatorIdeal_inclusion_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DenominatorLocalRatio/Cokernels.lean, line 189. The attribute's comment: “support of the first cokernel”.

The cokernel of the inclusion of the denominator ideal in the structure sheaf is supported on a closed nowhere dense subset.

theorem denominatorIdeal_inclusion_support
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf (O X).property L) :
    ∃ T : Set X, IsClosed T ∧ IsNowhereDense T ∧
      (asModuleSheaf X (cokernel (denominatorIdealι X L s))).supp ⊆ T

Stacks.DenominatorCokernel.denominatorIdeal_section_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DenominatorLocalRatio/MulCokernel.lean, line 112. The attribute's comment: “support of the second cokernel”.

The cokernel of multiplication by a regular meromorphic section of an invertible sheaf is supported on a closed nowhere dense subset. Stacks Tag 02P0, "support of the second cokernel".

theorem denominatorIdeal_section_support
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf (O X).property L)
    (hs : IsRegularMeromorphicSection X.sheaf L s) :
    ∃ T : Set X, IsClosed T ∧ IsNowhereDense T ∧
      (asModuleSheaf X (cokernel (denominatorIdealMul X L s))).supp ⊆ T

AlgebraicGeometry.exists_denominatorIdeal_inclusion_app_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorRule.lean, line 93. The attribute's comment: “the denominator rule”.

Stacks Project, Tag 02P0, the denominator rule. A section f of 𝒪_X over V lies in the ideal of denominators of a meromorphic section s of L exactly when f s is a section of L over V; here "lies in the ideal" means that f is the image of a section of the fibre product under the ideal inclusion, and "f s is a section of L" means that f s is the image of a section of L under the canonical map L ⟶ K_X(L).

theorem exists_denominatorIdeal_inclusion_app_eq_iff
    (L : SheafOfModules.{u}
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf))
    (s : MeromorphicSection X.sheaf L) (V : Opens X)
    (f : (SheafOfModules.unit
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf)).val.obj
        (op V)) :
    (∃ d : (denominatorIdeal X L s).val.obj (op V),
      (denominatorIdealι X L s).val.app (op V) d = f) ↔
    (∃ t : L.val.obj (op V),
      (meromorphicSectionMul X L s).val.app (op V) f =
        (toMeromorphicSectionSheafAsModule X L).val.app (op V) t)

AlgebraicGeometry.denominatorIdeal_section_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/Denominators.lean, line 241. The attribute's comment: “multiplication is injective”.

Stacks Project, Tag 02P0, injectivity of multiplication by the section. For a regular meromorphic section s of L, multiplication by s embeds the ideal of denominators of s in L.

theorem denominatorIdeal_section_mono
    (L : SheafOfModules.{u}
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf))
    (s : MeromorphicSection X.sheaf L)
    (_hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf).property
        L)
    (hs : IsRegularMeromorphicSection X.sheaf L s) :
    Mono (denominatorIdealMul X L s)

AlgebraicGeometry.denominatorIdeal_inclusion_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/DenominatorsInclusion.lean, line 473. The attribute's comment: “inclusion is injective”.

Stacks Project, Tag 02P0, injectivity of the ideal inclusion. For an invertible sheaf of modules L and a meromorphic section s of L, the ideal of denominators of s embeds in the structure sheaf.

theorem denominatorIdeal_inclusion_mono
    (L : SheafOfModules.{u}
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf))
    (s : MeromorphicSection X.sheaf L)
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf).property
        L) :
    Mono (denominatorIdealι X L s)

AlgebraicGeometry.denominatorIdealData_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/DenominatorIdealData.lean, line 228. The attribute's comment: “affine denominator ideal”.

Stacks Project, Tag 02P0, the affine denominator ideal. For an invertible sheaf of modules L and a meromorphic section s of L, the component of AlgebraicGeometry.denominatorIdealData at an affine open U is exactly the range of the inclusion of the ideal of denominators on sections over U: assembling the ideal sheaf from those ranges by AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals does not shrink any of them.

theorem denominatorIdealData_ideal
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf).property
        L)
    (U : X.affineOpens) :
    (denominatorIdealData X L s).ideal U =
      ((denominatorIdealι X L s).val.app (op U.1)).hom.range

AlgebraicGeometry.denominatorIdealData_support_isNowhereDense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/DenominatorIdealData.lean, line 256. The attribute's comment: “support of the denominator ideal”.

Stacks Project, Tag 02P0, the support of the ideal of denominators. For an invertible sheaf of modules L and a meromorphic section s of L, the support of AlgebraicGeometry.denominatorIdealData is a nowhere dense subset of X.

It is contained in the complement of the union, over the points of X, of the part of the affine neighbourhood produced by AlgebraicGeometry.exists_isAffineOpen_nhds_isNowhereDense_denominator on which the denominator b found there is invertible: on an affine open inside such a set the ideal inclusion is surjective on sections, so by AlgebraicGeometry.denominatorIdealData_ideal the component of the ideal sheaf there is the unit ideal and its zero locus contains no point of that open. The union is dense because the vanishing locus of a nonzerodivisor on an affine open is nowhere dense, so its complement is nowhere dense.

theorem denominatorIdealData_support_isNowhereDense
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf).property
        L) :
    IsNowhereDense ((denominatorIdealData X L s).support : Set X)

AlgebraicGeometry.denominatorIdeal_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/DenominatorQuasicoherent.lean, line 411. The attribute's comment: “quasi-coherence”. References: EGA IV (20.2.14), “special case”.

Stacks Project, Tag 02P0, quasi-coherence of the ideal of denominators. For an invertible sheaf of modules L and a meromorphic section s of L, the ideal of denominators of s is a quasi-coherent sheaf of ideals.

Quasi-coherence is checked by the localization criterion on the affine opens contained in the neighbourhoods of AlgebraicGeometry.exists_isAffineOpen_nhds_denominator_numerator_isUnit, which cover X. There the sections of the ideal are cut out by the colon condition f · a ∈ (b) of AlgebraicGeometry.exists_denominatorIdeal_inclusion_app_eq_iff_mul_eq_of_le, and a colon condition localizes by AlgebraicGeometry.isLocalizedModule_restrictₗ_of_colon. Regularity of s is not used: the source assumes it throughout Tag 02P0, but of its conclusions only injectivity of multiplication by s and the support of that map's cokernel need it.

theorem denominatorIdeal_isQuasicoherent
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf).property
        L) :
    (denominatorIdeal X L s).IsQuasicoherent

AlgebraicGeometry.denominatorIdeal_inclusion_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/DenominatorSupport.lean, line 350. The attribute's comment: “support of the first cokernel”.

Stacks Project, Tag 02P0, the support of the first cokernel. For an invertible sheaf of modules L and a meromorphic section s of L, the cokernel of the inclusion of the ideal of denominators of s in the structure sheaf is supported on a closed nowhere dense subset.

The set is the complement of the union, over the points of X, of the part of the affine neighbourhood produced by AlgebraicGeometry.exists_isAffineOpen_nhds_isNowhereDense_denominator on which the denominator b found there is invertible. On each such open set the whole structure sheaf consists of denominators, because b lies in the ideal and is a unit, so the cokernel has no sections there; and the union is dense because the vanishing locus of a nonzerodivisor on an affine open is nowhere dense.

theorem denominatorIdeal_inclusion_support
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf).property
        L) :
    ∃ T : Set X, IsClosed T ∧ IsNowhereDense T ∧
      (⟨(cokernel (denominatorIdealι X L s)).val,
        (cokernel (denominatorIdealι X L s)).isSheaf⟩ :
          RingedSpace.ModuleSheaf.{u} X.toRingedSpace).supp ⊆ T

AlgebraicGeometry.denominatorIdeal_section_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Meromorphic/DenominatorSupport.lean, line 580. The attribute's comment: “support of the second cokernel”.

Stacks Project, Tag 02P0, the support of the second cokernel. For an invertible sheaf of modules L and a regular meromorphic section s of L, the cokernel of multiplication by s on the ideal of denominators of s is supported on a closed nowhere dense subset.

The set is the complement of the union, over the points of X, of the part of the affine neighbourhood produced by AlgebraicGeometry.exists_isAffineOpen_nhds_denominator_numerator on which the numerator a found there is invertible. On each such open set every section of L is d · s for a denominator d, because L is generated by g and b · s = a · g with a a unit; and the union is dense because a is a nonzerodivisor (AlgebraicGeometry.numerator_mem_nonZeroDivisors, which is where regularity of s enters) and the vanishing locus of a nonzerodivisor on an affine open is nowhere dense.

theorem denominatorIdeal_section_support
    (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf).property
        L)
    (hs : IsRegularMeromorphicSection X.sheaf L s) :
    ∃ T : Set X, IsClosed T ∧ IsNowhereDense T ∧
      (⟨(cokernel (denominatorIdealMul X L s)).val,
        (cokernel (denominatorIdealMul X L s)).isSheaf⟩ :
          RingedSpace.ModuleSheaf.{u} X.toRingedSpace).supp ⊆ T

Tag 02P1, a definition

Tag 02P1 in the Stacks Project.

AlgebraicGeometry.denominatorIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/Denominators.lean, line 190. The attribute's comment: “the ideal sheaf of denominators of s”. References: EGA IV (20.2.14), “definition”.

The sheaf of denominators of a meromorphic section, as the fibre product of the structure sheaf and L over K_X(L). Its sections over V are the pairs (f, t) with f s = t in K_X(L)(V), so the image of its first projection is {f ∈ 𝒪_X(V) | f s ∈ L(V)}.

def denominatorIdeal
    (L : SheafOfModules.{u}
      (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X) X.sheaf))
    (s : MeromorphicSection X.sheaf L) :
    SheafOfModules.{u} (Stacks.Sheaves.Differentials.ringSheaf (J := Opens.grothendieckTopology X)
      X.sheaf)

Sources

• Section 31.24, Tag 01X1
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.MeromorphicFunction · totalQuotientSheaf · AlgebraicGeometry.NoChange.noChangeRing · AlgebraicGeometry.NoChange.normalForm_bijective · AlgebraicGeometry.NoChange.isUnit_of_isRegular_localizationAway · AlgebraicGeometry.NoChange.isIso_toTotalQuotientSheaf · AlgebraicGeometry.meromorphicSectionSheaf · AlgebraicGeometry.MeromorphicSection

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.