Effective Cartier-divisor sequences twisted by a line bundle

The normalized Cartier sequence for D and E has line terms O_X(E-D) and O_X(E). This leaf tensors that sequence by arbitrary LineBundleData L, obtaining line terms L ⊗ O_X(E-D) and L ⊗ O_X(E). Exactness comes from the generic exact tensor functor; coherence of the quotient is then inherited from its cokernel presentation.

This is the reusable geometric root needed by divisor-chain applications. It keeps arbitrary base line bundles out of the Enriques paper adapter.

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.lineBundleTwistSequence {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : CategoryTheory.ShortComplex X.Modules

The normalized Cartier-divisor sequence, tensored on the left by an arbitrary line bundle.

Equations

• D.lineBundleTwistSequence L E = (D.twistSequence E).map L.line.tensorLeftFunctor

@[simp]

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.lineBundleTwistSequence_X₁ {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : (D.lineBundleTwistSequence L E).X₁ = (L.tensor (CartierDivisor.lineBundleData (E - D.divisor))).line

@[simp]

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.lineBundleTwistSequence_X₂ {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : (D.lineBundleTwistSequence L E).X₂ = (L.tensor (CartierDivisor.lineBundleData E)).line

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.lineBundleTwistSource_isCoherent {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : X.coherent (D.lineBundleTwistSequence L E).X₁

The source line of the tensor-twisted sequence is coherent.

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.lineBundleTwistMiddle_isCoherent {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : X.coherent (D.lineBundleTwistSequence L E).X₂

The middle line of the tensor-twisted sequence is coherent.

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.lineBundleTwistSequence_shortExact {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : (D.lineBundleTwistSequence L E).ShortExact

Tensoring by a line bundle preserves the short exact Cartier sequence.

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.lineBundleTwistCokernelIso {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : CategoryTheory.Limits.cokernel (D.lineBundleTwistSequence L E).f ≅ (D.lineBundleTwistSequence L E).X₃

The target of the line-bundle-twisted sequence is the cokernel of its first map.

Equations

• D.lineBundleTwistCokernelIso L E = (CategoryTheory.Limits.cokernelIsCokernel (D.lineBundleTwistSequence L E).f).coconePointUniqueUpToIso ⋯.gIsCokernel

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.lineBundleTwistTarget_isCoherent {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) [IsLocallyNoetherian X] (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : X.coherent (D.lineBundleTwistSequence L E).X₃

The quotient in the line-bundle-twisted sequence is coherent.

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohLineBundleTwistSequence {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) [IsLocallyNoetherian X] (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : CategoryTheory.ShortComplex (Coh X)

The coherent-sheaf form of the line-bundle-twisted Cartier sequence. Its first two objects are the canonical Coh X avatars of the two tensor-product line bundles.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohLineBundleTwistSequence_shortExact {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) [IsLocallyNoetherian X] (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) : (D.cohLineBundleTwistSequence L E).ShortExact

The coherent line-bundle-twisted Cartier sequence is short exact.