37.46 Application to morphisms… to 37.52 Closed points in fibres

Section37.46 Application to morphisms with connected fibres #

Section 37.46 of the Stacks Project, Tag 057H. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 057I, a lemma

Tag 057I in the Stacks Project.

AlgebraicGeometry.exists_compactOpen_geometricallyConnected_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 123.

Stacks Project, Tag 057I. A geometrically connected fibre in a flat, finitely presented family with geometrically reduced fibres and a nonempty finite locally free multisection has a quasi-compact open neighbourhood in the source whose nonempty fibres are geometrically connected.

theorem exists_compactOpen_geometricallyConnected_fibers : Statement057I.{u}

Tag 055W, a lemma

Tag 055W in the Stacks Project.

AlgebraicGeometry.exists_etaleNeighborhood_geometricallyConnected, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 131.

Stacks Project, Tag 055W. A geometrically connected open in a fibre of a flat, finitely presented morphism with geometrically reduced fibres spreads, after an affine elementary étale base change, to a quasi-compact open with geometrically connected fibres.

theorem exists_etaleNeighborhood_geometricallyConnected : Statement055W.{u}

Tag 0EY5, a lemma

Tag 0EY5 in the Stacks Project.

AlgebraicGeometry.exists_etaleCover_factors_geometricallyConnected, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ConnectedFibreCover.lean, line 625.

Stacks Project, Tag 0EY5. A flat morphism locally of finite presentation with geometrically reduced fibres admits an étale covering of its source each member of which factors through an étale morphism to the base, the first factor being flat of finite presentation with geometrically connected and geometrically reduced fibres.

theorem exists_etaleCover_factors_geometricallyConnected
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFinitePresentation f] [Flat f]
    [GeometricallyReduced f] :
    ∃ 𝒰 : X.Cover.{u} Scheme.etalePrecoverage, ∀ i : 𝒰.I₀,
      ∃ (Sᵢ : Scheme.{u}) (h : Sᵢ ⟶ S) (g : 𝒰.X i ⟶ Sᵢ),
        Etale h ∧ Flat g ∧ FinitePresentation g ∧
          GeometricallyConnected g ∧ GeometricallyReduced g ∧
            g ≫ h = 𝒰.f i ≫ f

Tag 057J, a lemma

Tag 057J in the Stacks Project.

AlgebraicGeometry.exists_etaleNeighborhood_geometricallyIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 139.

Stacks Project, Tag 057J. A geometrically irreducible open in a fibre of a normal, finitely presented morphism spreads, after an affine elementary étale base change, to a quasi-compact open with geometrically integral fibres.

theorem exists_etaleNeighborhood_geometricallyIntegral : Statement057J.{u}

Sources

LeanAlgebraicGeometry.exists_compactOpen_geometricallyConnected_fibers · AlgebraicGeometry.exists_etaleNeighborhood_geometricallyConnected · AlgebraicGeometry.exists_etaleCover_factors_geometricallyConnected · AlgebraicGeometry.exists_etaleNeighborhood_geometricallyIntegral

Section37.47 Application to the structure of finite type morphisms #

Section 37.47 of the Stacks Project, Tag 052D. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 052E, a lemma

Tag 052E in the Stacks Project.

AlgebraicGeometry.exists_finite_over_smooth_of_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FiniteOverSmooth/Main.lean, line 59.

Stacks 052E. Let f : X ⟶ S be locally of finite type, let x ∈ X and set s = f x. If the fibre X_s has local dimension n at x, then there is a commutative square g ≫ f = π ≫ h in which h : Y ⟶ S is smooth of relative dimension n, g : (X', x') ⟶ (X, x) is an elementary étale neighbourhood, π : X' ⟶ Y is finite, and the fibre of π over y = π x' is the single point x'; moreover κ(y) is a purely transcendental extension of κ(s), and if f is locally of finite presentation then π is of finite presentation.

theorem exists_finite_over_smooth_of_locallyOfFiniteType
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f] (x : X) (n : ℕ)
    (hdim : topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = n) :
    ∃ (Y : Scheme.{u}) (h : Y ⟶ S) (N : EtaleNeighborhood X x) (π : N.scheme ⟶ Y),
      SmoothOfRelativeDimension n h ∧ N.IsElementary ∧ IsFinite π ∧
      {z : N.scheme | π z = π N.point} = {N.point} ∧
      N.toBase ≫ f = π ≫ h ∧
      (∃ hy : h (π N.point) = f x,
        letI : Algebra (S.residueField (f x)) (Y.residueField (π N.point)) :=
          (((S.residueFieldCongr hy).inv ≫ h.residueFieldMap (π N.point)).hom).toAlgebra
        PurelyTranscendental (S.residueField (f x)) (Y.residueField (π N.point))) ∧
      (LocallyOfFinitePresentation f → FinitePresentation π)

Tag 057K, a lemma

Tag 057K in the Stacks Project.

AlgebraicGeometry.exists_finite_over_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/GenericFibre/ShrinkingConsequences.lean, line 149.

Stacks Project, Tag 057K. A morphism locally of finite type is, in elementary étale neighbourhoods of a point and of its image, finite over a smooth morphism of relative dimension the dimension of the fibre at that point, with geometrically integral fibres and purely transcendental residue field extension; and the finite morphism is of finite presentation as soon as the original one is.

theorem exists_finite_over_smooth : Statement057K.{u}

Tag 057L, a lemma

Tag 057L in the Stacks Project.

AlgebraicGeometry.exists_finite_over_smooth_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FiniteOverSmoothAffine.lean, line 186.

Stacks Project, Tag 057L. The finite-over-smooth local structure of a locally finite-type morphism can be obtained with all three new schemes affine.

theorem exists_finite_over_smooth_affine {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (x : X) :
    ∃ (n : ℕ) (_ : topologicalKrullDimAt (f.fiber (f x)) (f.asFiber x) = n)
      (U : EtaleNeighborhood X x) (V : EtaleNeighborhood S (f x))
      (Y : Scheme.{u}) (h : Y ⟶ V.scheme) (π : U.scheme ⟶ Y),
      U.IsElementary ∧ V.IsElementary ∧ (U.toBase ≫ f = π ≫ h ≫ V.toBase) ∧
        SmoothOfRelativeDimension n h ∧
        (∀ s' : V.scheme, GeometricallyIntegral (h.fiberToSpecResidueField s')) ∧
        IsFinite π ∧ (∀ z : U.scheme, π z = π U.point ↔ z = U.point) ∧
        (∃ heq : h (π U.point) = V.point,
          letI : Algebra (V.scheme.residueField V.point) (Y.residueField (π U.point)) :=
            ((V.scheme.residueFieldCongr heq).inv ≫ h.residueFieldMap (π U.point)).hom.toAlgebra
          PurelyTranscendental (V.scheme.residueField V.point)
            (Y.residueField (π U.point))) ∧
        (LocallyOfFinitePresentation f → FinitePresentation π) ∧
        IsAffine V.scheme ∧ IsAffine Y ∧ IsAffine U.scheme

Tag 05B8, a lemma

Tag 05B8 in the Stacks Project.

AlgebraicGeometry.exists_open_preimage_le, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/FiniteSingletonFibre.lean, line 60. The attribute's comment: “inverse_image_neighbourhoods”.

For a finite morphism whose fibre over y is the singleton x, the inverse image of some open neighbourhood of y is contained in any prescribed open neighbourhood of x.

lemma exists_open_preimage_le {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f]
    (x : X) (y : Y) (hxy : f x = y) (hfiber : f ⁻¹' {y} = {x})
    (U : X.Opens) (hxU : x ∈ U) :
    ∃ V : Y.Opens, y ∈ V ∧ f ⁻¹ᵁ V ≤ U

AlgebraicGeometry.finite_stalkMap_of_preimage_singleton, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/FiniteSingletonFibre.lean, line 200. The attribute's comment: “finite_local_ring_map”.

For a finite morphism with a singleton fibre at x, the induced map on the local rings at f x and x is finite.

lemma finite_stalkMap_of_preimage_singleton
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f]
    (x : X) (hx : f ⁻¹' {f x} = {x}) :
    (f.stalkMap x).hom.Finite

AlgebraicGeometry.finitePresentation_stalkMap_of_preimage_singleton, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/FiniteSingletonFibre.lean, line 256. The attribute's comment: “finitely_presented_local_ring_map”.

If a finite morphism of finite presentation has a singleton fibre over f x, its local-ring map at x is of finite presentation.

lemma finitePresentation_stalkMap_of_preimage_singleton
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f]
    (x : X) (hx : f ⁻¹' {f x} = {x}) (hfp : FinitePresentation f) :
    (f.stalkMap x).hom.FinitePresentation

AlgebraicGeometry.stalk_isomorphic_pushforward_of_finite_singleton_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/EtaleNeighbourhood/FiniteSingletonFibre.lean, line 418. The attribute's comment: “pushforward_stalk”.

Let f : X ⟶ Y be finite and suppose that the fibre over f x is the singleton {x}. For a quasi-coherent O_X-module F, its stalk at x, viewed as an O_{Y,f x}-module, is isomorphic to the stalk at f x of f_* F.

theorem stalk_isomorphic_pushforward_of_finite_singleton_fiber
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f]
    (x : X) (hfiber : f ⁻¹' ({f x} : Set Y) = {x})
    (F : X.Modules) [F.IsQuasicoherent] :
    letI : Module (X.presheaf.stalk x)
        ↑(TopCat.Presheaf.stalk F.val.presheaf x) :=
      PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
        (R := X.presheaf) F.val x
    letI : Module (Y.presheaf.stalk (f x))
        ↑(TopCat.Presheaf.stalk F.val.presheaf x) :=
      Module.compHom _ (f.stalkMap x).hom
    letI : Module (Y.presheaf.stalk (f x))
        ↑(TopCat.Presheaf.stalk
          ((Scheme.Modules.pushforward f).obj F).val.presheaf (f x)) :=
      PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
        (R := Y.presheaf) ((Scheme.Modules.pushforward f).obj F).val (f x)
    Nonempty
      (ModuleCat.of (Y.presheaf.stalk (f x))
          ↑(TopCat.Presheaf.stalk F.val.presheaf x) ≅
        ModuleCat.of (Y.presheaf.stalk (f x))
          ↑(TopCat.Presheaf.stalk
            ((Scheme.Modules.pushforward f).obj F).val.presheaf (f x)))

Sources

LeanAlgebraicGeometry.exists_finite_over_smooth_of_locallyOfFiniteType · AlgebraicGeometry.exists_finite_over_smooth · AlgebraicGeometry.exists_finite_over_smooth_affine · AlgebraicGeometry.exists_open_preimage_le · AlgebraicGeometry.finite_stalkMap_of_preimage_singleton · AlgebraicGeometry.finitePresentation_stalkMap_of_preimage_singleton · AlgebraicGeometry.stalk_isomorphic_pushforward_of_finite_singleton_fiber

Section37.48 Application to the fppf topology #

Section 37.48 of the Stacks Project, Tag 05WM. 8 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DET, a lemma

Tag 0DET in the Stacks Project.

Stacks.Topologies.Fppf.etaleFiniteLocallyFreeDominates, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/LocallyQuasiFiniteRefinement.lean, line 151.

Stacks Project, Tag 0DET. An fppf covering {S_i ⟶ S} is refined by an fppf covering {V_a ⟶ S} whose members factor as V_a ⟶ S'_a ⟶ S with {S'_a ⟶ S} an étale covering and V_a ⟶ S'_a surjective finite locally free.

theorem etaleFiniteLocallyFreeDominates {S : Scheme.{u}}
    (𝒰 : S.Cover.{v} Scheme.fppfPrecoverage) :
    EtaleFiniteLocallyFreeDominates 𝒰

Tag 05WN, a lemma

Tag 05WN in the Stacks Project.

Stacks.Topologies.Fppf.exists_openCover_finiteLocallyFree_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/LocallyQuasiFiniteRefinement.lean, line 193.

Stacks Project, Tag 05WN. Let 𝒮 = {S_i ⟶ S} be an fppf covering of a scheme. Then there are a Zariski open covering S = ⋃ U_j, surjective finite locally free morphisms W_j ⟶ U_j, Zariski open coverings W_j = ⋃_k W_{j,k}, and surjective finite locally free morphisms T_{j,k} ⟶ W_{j,k}, such that the composites {T_{j,k} ⟶ S} form an fppf covering refining 𝒮.

This is exists_openCover_finiteLocallyFree_refinement_of_hasQuasiFiniteSlices applied to AlgebraicGeometry.hasQuasiFiniteSlices, the form of [Stacks, Tag 0570] used here.

theorem exists_openCover_finiteLocallyFree_refinement (S : Scheme.{u})
    (𝒮 : S.Cover.{v} Scheme.fppfPrecoverage) :
    ∃ (𝒰 : S.OpenCover.{max u v})
      (W : 𝒰.I₀ → Scheme.{u})
      (g : ∀ j, W j ⟶ 𝒰.X j)
      (𝒲 : ∀ j, (W j).OpenCover.{max u v})
      (T : ∀ j, (𝒲 j).I₀ → Scheme.{u})
      (h : ∀ j k, T j k ⟶ (𝒲 j).X k),
      (∀ j, Surjective (g j) ∧ Stacks.Morphisms.IsFiniteLocallyFree (g j)) ∧
      (∀ j k, Surjective (h j k) ∧ Stacks.Morphisms.IsFiniteLocallyFree (h j k)) ∧
      Presieve.ofArrows
          (fun jk : Σ j, (𝒲 j).I₀ ↦ T jk.1 jk.2)
          (fun jk ↦ h jk.1 jk.2 ≫ (𝒲 jk.1).f jk.2 ≫ g jk.1 ≫ 𝒰.f jk.1) ∈
        Scheme.fppfPrecoverage S ∧
      ∀ j k, ∃ i, ∃ l : T j k ⟶ 𝒮.X i,
        l ≫ 𝒮.f i = h j k ≫ (𝒲 j).f k ≫ g j ≫ 𝒰.f j

Tag 0CNX, a lemma

Tag 0CNX in the Stacks Project.

AlgebraicGeometry.exists_integral_surjective_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FppfApplication/IntegralSurjectiveExtension.lean, line 81. The attribute's comment: “a surjective integral morphism over a retrocompact open of S extends to a surjective integral morphism over S with the same restriction to the open”.

Stacks Project, Tag 0CNX, in corrected form, with U retrocompact in S: a surjective integral morphism over a retrocompact open subscheme extends to a surjective integral morphism over the whole scheme, without changing its restriction to the open subscheme. The general statement of [Stacks, Tag 0CNX] is false; AlgebraicGeometry.exists_integral_surjective_extension_and_not_forall pairs this theorem with the failure of the statement for an arbitrary open subscheme.

theorem exists_integral_surjective_extension
    {S : Scheme.{u}} (U : S.Opens) [QuasiCompact U.ι]
    {V : Scheme.{u}} (f : V ⟶ U.toScheme) [IsIntegralHom f] [Surjective f] :
    ∃ (W : Scheme.{u}) (g : W ⟶ S),
      IsIntegralHom g ∧ Surjective g ∧
        Nonempty (Over.mk f ≅ (Over.pullback U.ι).obj (Over.mk g))

Tag 0CNY, a lemma

Tag 0CNY in the Stacks Project.

Stacks.FiniteFactorization.exists_finite_surjective_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteFactorization/ExtendFiniteSurjective.lean, line 47.

Let S be a quasi-compact quasi-separated scheme and let U ⊆ S be a quasi-compact open. A finite surjective morphism f : V ⟶ U extends to a finite surjective morphism g : V̄ ⟶ S: there is an isomorphism e : V̄ ×_S U ≅ V identifying the projection V̄ ×_S U ⟶ U with f, so that e is an isomorphism of schemes over U.

theorem exists_finite_surjective_extension {S V : Scheme.{u}}
    [CompactSpace S] [QuasiSeparatedSpace S]
    (U : S.Opens) (hU : IsCompact (U : Set S))
    (f : V ⟶ U.toScheme) [IsFinite f] [Surjective f] :
    ∃ (Vbar : Scheme.{u}) (g : Vbar ⟶ S),
      IsFinite g ∧ Surjective g ∧
        ∃ e : pullback g U.ι ≅ V,
          e.hom ≫ f = pullback.snd g U.ι

Tag 0CNZ, a lemma

Tag 0CNZ in the Stacks Project.

AlgebraicGeometry.exists_integral_surjective_openCover_factorization_of_mem_fppfPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FppfApplication/IntegralDomination.lean, line 125.

Stacks Project, Tag 0CNZ. For every fppf covering {X i ⟶ S} of a scheme S there are a surjective integral morphism g : S' ⟶ S and an open covering of S' such that each member U c of the covering maps to S through some member X i of the given covering.

No hypothesis is imposed on S, as none is imposed in the source.

theorem exists_integral_surjective_openCover_factorization_of_mem_fppfPrecoverage
    {I : Type v} {S : Scheme.{u}}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ S)
    (hf : Presieve.ofArrows X f ∈ Scheme.fppfPrecoverage S) :
    ∃ (S' : Scheme.{u}) (g : S' ⟶ S), IsIntegralHom g ∧ Surjective g ∧
      ∃ (J : Type u) (U : J → S'.Opens), (⨆ c, U c) = ⊤ ∧
        ∀ c, ∃ i, ∃ t : (U c).toScheme ⟶ X i, (U c).ι ≫ g = t ≫ f i

Tag 0CP0, a lemma

Tag 0CP0 in the Stacks Project.

AlgebraicGeometry.exists_finite_surjective_openCover_factorization_of_mem_fppfPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/FppfApplication/FiniteDomination.lean, line 165.

[Stacks, Tag 0CP0]. For every fppf covering {X i ⟶ S} of a quasi-compact and quasi-separated scheme S there are a surjective finite morphism g : S' ⟶ S of finite presentation and an open covering of S' such that each member U c of the covering maps to S through some member X i of the given covering.

The second input of the source proof, [Stacks, Tag 09YZ], is supplied by Stacks.AlgebraicGeometry.Tag0817PartTwo.nonempty_integralLimitPresentation, which proves it at exactly the quasi-compactness and quasi-separatedness assumed here.

theorem exists_finite_surjective_openCover_factorization_of_mem_fppfPrecoverage
    {I : Type v} {S : Scheme.{u}} [CompactSpace S] [QuasiSeparatedSpace S]
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ S)
    (hf : Presieve.ofArrows X f ∈ Scheme.fppfPrecoverage S) :
    ∃ (S' : Scheme.{u}) (g : S' ⟶ S), IsFinite g ∧ Surjective g ∧ FinitePresentation g ∧
      ∃ (J : Type u) (U : J → S'.Opens), (⨆ c, U c) = ⊤ ∧
        ∀ c, ∃ i, ∃ t : (U c).toScheme ⟶ X i, (U c).ι ≫ g = t ≫ f i

Tag 0DBT, a lemma

Tag 0DBT in the Stacks Project.

AlgebraicGeometry.isPHCoveringInCutoff_of_isEtaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToEtaleSquares.lean, line 81. The attribute's comment: “étale coverings in a cutoff category”.

An étale covering family in a size-bounded category of schemes is a ph covering family there, since both conditions are read off the image of the family in all schemes.

public theorem isPHCoveringInCutoff_of_isEtaleCovering {κ : Cardinal.{u}}
    (𝒰 : Covering.{u + 1, u, u + 1} (SchemeBelow κ)) (h𝒰 : IsEtaleCovering 𝒰) :
    IsPHCoveringInCutoff 𝒰

AlgebraicGeometry.bigEtaleOverTopology_le_bigPHOverTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToEtaleSquares.lean, line 176. The attribute's comment: “étale coverings on a slice”.

The big-site comparison from ph to étale is induced by the identity functor on the common slice category: every étale covering of the slice is a ph covering of the slice.

public theorem bigEtaleOverTopology_le_bigPHOverTopology (B : BigPHSite.{u}) (X : B.Schemes) :
    BigEtaleOver.topology (phAssociatedBigEtaleSite B) X.1 X.2 ≤ B.topology.over X

AlgebraicGeometry.isPHCovering_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopology/EtaleHComparison.lean, line 102. The attribute's comment: “étale coverings”.

A family of étale morphisms of schemes whose images cover the target is a ph covering.

public theorem isPHCovering_of_etale {T : Scheme.{u}} {I : Type v} (X : I → Scheme.{u})
    (f : ∀ i, X i ⟶ T) (hsurj : ∀ x : T, ∃ i, x ∈ Set.range (f i).base)
    (hetale : ∀ i, Etale (f i)) :
    IsPHCovering X f

AlgebraicGeometry.IsPHCovering.of_mem_fppfPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/V/FppfAffineDomination.lean, line 116.

An fppf covering of schemes is a ph covering.

theorem IsPHCovering.of_mem_fppfPrecoverage
    {T : Scheme.{u}} {I : Type v} (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : Presieve.ofArrows X f ∈ Scheme.fppfPrecoverage T) :
    IsPHCovering X f

Tag 0DBU, a remark

Tag 0DBU in the Stacks Project.

AlgebraicGeometry.phToFppf_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToFppfComparison.lean, line 407. The attribute's comment: “the comparison is the morphism of sites given by the identity functor on underlying categories”.

Stacks 0DBU: ε is the morphism of sites given by the identity functor on underlying categories. The two sites have the one underlying category, the slice over X of the common category of schemes, and the identity functor of it, read from the fppf site to the ph site, satisfies the two conditions of Stacks 00X1: it is continuous and the functor it induces on sheaves of sets is left exact. So it is a morphism of sites (Sch/S)_ph ⟶ (Sch/S)_fppf, and AlgebraicGeometry.phToBigFppfMorphism is the morphism of topoi Stacks 00XC attaches to it.

public theorem phToFppf_isMorphismOfSites (B : BigPHSite.{u}) (X : B.Schemes) :
    IsMorphismOfSites.{u + 1} (𝟭 (Over X))
      (BigFppfOver.topology (phAssociatedBigFppfSite B) X.1 X.2) (B.topology.over X)

AlgebraicGeometry.phToBigFppf_pushforward_comp_sheafToPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToFppfComparison.lean, line 419. The attribute's comment: “the direct image is the identity on underlying presheaves”.

Stacks 0DBU: ε_* is the identity on underlying presheaves. Forming the direct image of a ph sheaf and then forgetting the fppf sheaf condition gives back the presheaf one started from, because the direct image is restriction along the identity functor of the common slice category. The two sides are equal, not merely isomorphic.

public theorem phToBigFppf_pushforward_comp_sheafToPresheaf (B : BigPHSite.{u})
    (X : B.Schemes) :
    (phToBigFppfMorphism B X).pushforward ⋙
        sheafToPresheaf (BigFppfOver.topology (phAssociatedBigFppfSite B) X.1 X.2)
          (Type (u + 1)) =
      sheafToPresheaf (B.topology.over X) (Type (u + 1))

AlgebraicGeometry.phToBigFppf_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToFppfComparison.lean, line 439. The attribute's comment: “the inverse image is the ph sheafification of an fppf sheaf”.

Stacks 0DBU: ε⁻¹ associates to an fppf sheaf its ph sheafification. The inverse image is the functor on sheaves of sets induced by the identity functor of the common slice, and the left Kan extension along the identity is the identity, so the inverse image is the forgetful functor to presheaves followed by ph sheafification.

The isomorphism is the canonical one, not just some isomorphism of the right type: ε is by construction the change-of-topology morphism of the identity functor, and the comparison is CategoryTheory.changeOfTopologyMorphism_inverseImageIso, built from the construction of the induced functor as a left Kan extension followed by sheafification.

public def phToBigFppf_inverseImageIso (B : BigPHSite.{u}) (X : B.Schemes) :
    (phToBigFppfMorphism B X).inverseImage ≅
      sheafToPresheaf (BigFppfOver.topology (phAssociatedBigFppfSite B) X.1 X.2)
          (Type (u + 1)) ⋙
        presheafToSheaf (B.topology.over X) (Type (u + 1))

AlgebraicGeometry.phToZariski_pushforward_comp_sheafToPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToFppfComparison.lean, line 518. The attribute's comment: “by composition, the comparison of the ph topology with the Zariski topology”.

Stacks 0DBU: by composition the ph topology is compared with the Zariski topology. AlgebraicGeometry.phToZariskiMorphism, the composition of ε with the change-of-topology morphism from the fppf to the Zariski topology, is a comparison of the ph topology with the Zariski topology of Stacks 03FF: it is a morphism of topoi from ph sheaves to Zariski sheaves whose direct image is the identity on underlying presheaves, as ε's own is.

public theorem phToZariski_pushforward_comp_sheafToPresheaf (B : BigPHSite.{u})
    (X : B.Schemes) :
    (phToZariskiMorphism B X).pushforward ⋙
        sheafToPresheaf ((phAssociatedBigFppfSite B).zariskiTopology.over X) (Type (u + 1)) =
      sheafToPresheaf (B.topology.over X) (Type (u + 1))

AlgebraicGeometry.phToEtale_pushforward_comp_sheafToPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToFppfComparison.lean, line 544. The attribute's comment: “by composition, the comparison of the ph topology with the étale topology”.

Stacks 0DBU: by composition the ph topology is compared with the étale topology. AlgebraicGeometry.phToEtaleMorphism, the composition of ε with the change-of-topology morphism from the fppf to the étale topology, is a comparison of the ph topology with the étale topology of Stacks 03FF: it is a morphism of topoi from ph sheaves to étale sheaves whose direct image is the identity on underlying presheaves, as ε's own is.

public theorem phToEtale_pushforward_comp_sheafToPresheaf (B : BigPHSite.{u}) (X : B.Schemes) :
    (phToEtaleMorphism B X).pushforward ⋙
        sheafToPresheaf ((phAssociatedBigFppfSite B).etaleTopology.over X) (Type (u + 1)) =
      sheafToPresheaf (B.topology.over X) (Type (u + 1))

AlgebraicGeometry.phToSmooth_pushforward_comp_sheafToPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToFppfComparison.lean, line 569. The attribute's comment: “by composition, the comparison of the ph topology with the smooth topology”.

Stacks 0DBU: by composition the ph topology is compared with the smooth topology. AlgebraicGeometry.phToSmoothMorphism, the composition of ε with the change-of-topology morphism from the fppf to the smooth topology, is a comparison of the ph topology with the smooth topology of Stacks 03FF: it is a morphism of topoi from ph sheaves to smooth sheaves whose direct image is the identity on underlying presheaves, as ε's own is.

public theorem phToSmooth_pushforward_comp_sheafToPresheaf (B : BigPHSite.{u}) (X : B.Schemes) :
    (phToSmoothMorphism B X).pushforward ⋙
        sheafToPresheaf ((phAssociatedBigFppfSite B).smoothTopology.over X) (Type (u + 1)) =
      sheafToPresheaf (B.topology.over X) (Type (u + 1))

AlgebraicGeometry.phToSyntomic_pushforward_comp_sheafToPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToFppfComparison.lean, line 594. The attribute's comment: “by composition, the comparison of the ph topology with the syntomic topology”.

Stacks 0DBU: by composition the ph topology is compared with the syntomic topology. AlgebraicGeometry.phToSyntomicMorphism, the composition of ε with the change-of-topology morphism from the fppf to the syntomic topology, is a comparison of the ph topology with the syntomic topology of Stacks 03FF: it is a morphism of topoi from ph sheaves to syntomic sheaves whose direct image is the identity on underlying presheaves, as ε's own is.

public theorem phToSyntomic_pushforward_comp_sheafToPresheaf (B : BigPHSite.{u})
    (X : B.Schemes) :
    (phToSyntomicMorphism B X).pushforward ⋙
        sheafToPresheaf ((phAssociatedBigFppfSite B).syntomicTopology.over X) (Type (u + 1)) =
      sheafToPresheaf (B.topology.over X) (Type (u + 1))

Sources

LeanStacks.Topologies.Fppf.etaleFiniteLocallyFreeDominates · Stacks.Topologies.Fppf.exists_openCover_finiteLocallyFree_refinement · AlgebraicGeometry.exists_integral_surjective_extension · Stacks.FiniteFactorization.exists_finite_surjective_extension · AlgebraicGeometry.exists_integral_surjective_openCover_factorization_of_mem_fppfPrecoverage · AlgebraicGeometry.exists_finite_surjective_openCover_factorization_of_mem_fppfPrecoverage · AlgebraicGeometry.isPHCoveringInCutoff_of_isEtaleCovering · AlgebraicGeometry.bigEtaleOverTopology_le_bigPHOverTopology

Section37.49 Quasi-projective schemes #

Section 37.49 of the Stacks Project, Tag 0B41. 3 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B42, a lemma

Tag 0B42 in the Stacks Project.

AlgebraicGeometry.isQuasiProjective_tfae_of_exists_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveOverAmpleBase.lean, line 238. The attribute's comment: “all five conditions, with no hypothesis”.

Stacks Project, Tag 0B42. Let S be a scheme carrying an ample invertible module and let f : X ⟶ S be a morphism of schemes. The following are equivalent:

f is quasi-projective;

f is H-quasi-projective;

X is a quasi-compact open subscheme, over S, of a scheme projective over S;

f is of finite type and X carries an ample invertible module;

f is of finite type and carries an f-very ample invertible module.

The cycle is (1) ⟹ (4) ⟹ (2) ⟹ (1), with (2) ⟹ (3), (3) ⟹ (5) and (5) ⟹ (1) closing the remaining conditions. Nothing is assumed.

theorem isQuasiProjective_tfae_of_exists_isAmple (f : X ⟶ S)
    (hS : ∃ (M : S.Modules) (hM : Stacks.Ample.IsInvertibleModule S M),
      letI : Stacks.Ample.IsInvertibleModule S M := hM
      Stacks.Ample.IsAmple S M) :
    List.TFAE
      [IsQuasiProjective f,
        IsHQuasiProjective f,
        ∃ (X' : Scheme.{u}) (p : X' ⟶ S) (j : X ⟶ X'),
          IsOpenImmersion j ∧ QuasiCompact j ∧ j ≫ p = f ∧ IsProjective p,
        (LocallyOfFiniteType f ∧ QuasiCompact f) ∧
          ∃ (L : X.Modules) (hL : Stacks.Ample.IsInvertibleModule X L),
            letI : Stacks.Ample.IsInvertibleModule X L := hL
            Stacks.Ample.IsAmple X L,
        (LocallyOfFiniteType f ∧ QuasiCompact f) ∧
          ∃ (L : X.Modules) (hL : Stacks.Ample.IsInvertibleModule X L),
            letI : Stacks.Ample.IsInvertibleModule X L := hL
            Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f L]

Tag 0B43, a lemma

Tag 0B43 in the Stacks Project.

AlgebraicGeometry.QuasiProjectiveSchemesOver.baseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveCategoryClosure.lean, line 234. The attribute's comment: “part (1), base change; the source's hypothesis that S' has an ample invertible sheaf is not needed, Tag 0B3G needing no such hypothesis”. References: EGA II (5.3.4).

Stacks Project, Tag 0B43, clause (1). For a morphism of bases g : S' ⟶ S, base change along g is a functor QP_S ⥤ QP_{S'}: the fibre product X ×_S S' of a scheme X quasi-projective over S is quasi-projective over S'.

The object part is [Stacks, Tag 0B3G], AlgebraicGeometry.IsQuasiProjective.of_isPullback, applied to the fibre-product square. That result is unconditional, so the hypothesis of the source that S' carries an ample invertible sheaf is not needed and is not assumed.

def QuasiProjectiveSchemesOver.baseChange {S S' : Scheme.{u}} (g : S' ⟶ S) :
    QuasiProjectiveSchemesOver S ⥤ QuasiProjectiveSchemesOver S'

AlgebraicGeometry.isQuasiProjective_comp_of_exists_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveCategoryClosure.lean, line 250. The attribute's comment: “part (2), composition”.

Stacks Project, Tag 0B43, clause (2). Let S carry an ample invertible sheaf. If X ∈ QP_S and Y ∈ QP_X, then Y ∈ QP_S: for f : Y ⟶ X and g : X ⟶ S quasi-projective, f ≫ g is quasi-projective.

The source reads this off condition (4) of [Stacks, Tag 0B42]. It is taken here from [Stacks, Tag 0C4M], AlgebraicGeometry.IsQuasiProjective.comp, which is already proved over a quasi-compact base; the ample invertible sheaf on S supplies that quasi-compactness and nothing else is used.

theorem isQuasiProjective_comp_of_exists_isAmple {X Y S : Scheme.{u}} (f : Y ⟶ X) (g : X ⟶ S)
    (hS : ∃ (M : S.Modules) (hM : Stacks.Ample.IsInvertibleModule S M),
      letI : Stacks.Ample.IsInvertibleModule S M := hM
      Stacks.Ample.IsAmple S M)
    (hf : IsQuasiProjective f) (hg : IsQuasiProjective g) : IsQuasiProjective (f ≫ g)

AlgebraicGeometry.isQuasiProjective_pullback_snd_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveCategoryClosure.lean, line 267. The attribute's comment: “part (3), fibre products”.

Stacks Project, Tag 0B43, clause (3). QP_S is closed under fibre products over S. For f : X ⟶ S and g : Y ⟶ S quasi-projective and S carrying an ample invertible sheaf, the structure morphism X ×_S Y ⟶ S is quasi-projective.

This is the source's proof: the projection X ×_S Y ⟶ Y is a base change of f, hence quasi-projective by clause (1), and clause (2) composes it with g.

theorem isQuasiProjective_pullback_snd_comp {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
    (hS : ∃ (M : S.Modules) (hM : Stacks.Ample.IsInvertibleModule S M),
      letI : Stacks.Ample.IsInvertibleModule S M := hM
      Stacks.Ample.IsAmple S M)
    (hf : IsQuasiProjective f) (hg : IsQuasiProjective g) :
    IsQuasiProjective (pullback.snd f g ≫ g)

AlgebraicGeometry.quasiProjectiveOver_isClosedUnderBinaryProducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveCategoryClosure.lean, line 306. The attribute's comment: “part (3), fibre products, as closure of the category under binary products”. References: EGA II (5.3.4), “(iv)”.

Stacks Project, Tag 0B43, clause (3), as a closure property of the category QP_S. For S carrying an ample invertible sheaf, the full subcategory of schemes quasi-projective over S is closed under binary products in the category of schemes over S — that is, under fibre products over S.

A binary product in Over S is a fibre product of the sources over S, by AlgebraicGeometry.isLimitOverBinaryFan, so this is AlgebraicGeometry.isQuasiProjective_pullback_snd_comp transported along the comparison isomorphism.

theorem quasiProjectiveOver_isClosedUnderBinaryProducts (S : Scheme.{u})
    (hS : ∃ (M : S.Modules) (hM : Stacks.Ample.IsInvertibleModule S M),
      letI : Stacks.Ample.IsInvertibleModule S M := hM
      Stacks.Ample.IsAmple S M) :
    (quasiProjectiveOver S).IsClosedUnderBinaryProducts

AlgebraicGeometry.isQuasiProjective_of_isQuasiAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveCategoryClosure.lean, line 335. The attribute's comment: “part (6), quasi-affine of finite type; no hypothesis on the base is used”.

Stacks Project, Tag 0B43, clause (6). If f : X ⟶ S is quasi-affine of finite type then X ∈ QP_S.

This is Morphisms [Stacks, Tag 0B3H], Stacks.HProjective.isQuasiProjective_of_isQuasiAffineHom: the structure sheaf 𝒪_X is ample relative to a quasi-affine morphism. It needs no hypothesis on the base. Finite type is the conjunction of local finite type and quasi-compactness as in [Stacks, Tag 01T1], and quasi-compactness already follows from quasi-affineness, so only the local finite type half appears.

theorem isQuasiProjective_of_isQuasiAffineHom {X S : Scheme.{u}} (f : X ⟶ S)
    [IsQuasiAffineHom f] (hf : LocallyOfFiniteType f) : IsQuasiProjective f

AlgebraicGeometry.isQuasiProjective_of_locallyQuasiFinite_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveCategoryClosure.lean, line 351. The attribute's comment: “part (7), quasi-finite and separated; no hypothesis on the base is used”. References: EGA III (4.4.12), “more general”.

Stacks Project, Tag 0B43, clause (7). If f : X ⟶ S is quasi-finite and separated then X ∈ QP_S.

This is the source's proof: a quasi-finite separated morphism is quasi-affine by [Stacks, Tag 02LR], AlgebraicGeometry.isQuasiAffineHom_of_locallyQuasiFinite, and clause (6) applies. Quasi-finiteness is local quasi-finiteness together with finite type, as in [Stacks, Tag 02NG]. No hypothesis on the base is used.

theorem isQuasiProjective_of_locallyQuasiFinite_of_isSeparated {X S : Scheme.{u}} (f : X ⟶ S)
    [IsSeparated f] [LocallyQuasiFinite f] [LocallyOfFiniteType f] [QuasiCompact f] :
    IsQuasiProjective f

AlgebraicGeometry.isQuasiProjective_of_isImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveCategoryClosure.lean, line 367. The attribute's comment: “part (8), quasi-compact immersion; no hypothesis on the base is used”.

Stacks Project, Tag 0B43, clause (8). If f : X ⟶ S is a quasi-compact immersion then X ∈ QP_S.

The source goes through clause (7) and Morphisms [Stacks, Tag 01TN], an immersion being locally quasi-finite; here that tag is Mathlib's LocallyQuasiFinite instance for an immersion, and an immersion is locally of finite type as well, so clause (7) applies directly. No hypothesis on the base is used.

theorem isQuasiProjective_of_isImmersion {X S : Scheme.{u}} (f : X ⟶ S) [IsImmersion f]
    [QuasiCompact f] : IsQuasiProjective f

AlgebraicGeometry.isQuasiProjective_sigmaDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveDisjointUnion.lean, line 230. The attribute's comment: “part (4), finite disjoint unions; proved through clause (6) and clause (2) over the base ∐ S rather than through the ampleness of a glued module on a disjoint union, which the source asserts with details omitted”.

Let S carry an ample invertible sheaf. If f i : Z i ⟶ S is quasi-projective for every member of a finite family, then the structure morphism ∐ Z ⟶ S of the disjoint union is quasi-projective.

theorem isQuasiProjective_sigmaDesc (f : ∀ i, Z i ⟶ S)
    (hS : ∃ (M : S.Modules) (hM : Stacks.Ample.IsInvertibleModule S M),
      letI : Stacks.Ample.IsInvertibleModule S M := hM
      Stacks.Ample.IsAmple S M)
    (hf : ∀ i, IsQuasiProjective (f i)) : IsQuasiProjective (Sigma.desc f)

AlgebraicGeometry.quasiProjectiveOver_prop_of_isColimit_cofan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/QuasiProjectiveDisjointUnion.lean, line 268. The attribute's comment: “part (4), finite disjoint unions, as closure of the category under finite coproducts”. References: EGA II (5.3.6), “special case”.

For S carrying an ample invertible sheaf, the full subcategory of schemes quasi-projective over S is closed under finite coproducts in the category of schemes over S.

theorem quasiProjectiveOver_prop_of_isColimit_cofan (S : Scheme.{u})
    (hS : ∃ (M : S.Modules) (hM : Stacks.Ample.IsInvertibleModule S M),
      letI : Stacks.Ample.IsInvertibleModule S M := hM
      Stacks.Ample.IsAmple S M)
    {ι : Type u} [Finite ι] {X : ι → Over S} (hX : ∀ i, quasiProjectiveOver S (X i))
    (c : Cofan X) (hc : IsColimit c) : quasiProjectiveOver S c.pt

AlgebraicGeometry.IsProjective.isQuasiProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProjectiveBundleProperFiniteType/Basic.lean, line 219. The attribute's comment: “part (5), a projective morphism is in QP_S; the source's hypothesis that S has an ample invertible sheaf is not needed, Tag 07RL needing no such hypothesis”.

Stacks Project, Tag 07RL. A projective morphism is quasi-projective. Properness supplies the finite-type half, and the f-very ample module of AlgebraicGeometry.IsProjective.exists_isRelativelyVeryAmple is f-ample by [Stacks, Tag 01VN], f being quasi-compact. No hypothesis on the base is used, which is how the source states the tag.

It is also clause (5) of [Stacks, Tag 0B43], which the source proves by citing Tag 07RL: membership of X in the category QP_S of that tag is AlgebraicGeometry.IsQuasiProjective X.hom, so "if X ⟶ S is projective then X ∈ QP_S" is this statement. Tag 0B43's hypothesis that S carries an ample invertible sheaf is not needed for it and is not assumed.

theorem IsProjective.isQuasiProjective {f : X ⟶ S} (hf : IsProjective f) :
    IsQuasiProjective f

Tag 0EJY, a lemma

Tag 0EJY in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Scheme.IsQuasiAffine.of_isAffineHom registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 54 (StacksFrontier): “U is quasi-affine (stated for affine f; integral morphisms are affine)”. References: EGA II (5.1.10), “(ii), special case”.
AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch37.lean, line 56 (StacksFrontier): “the square U → Spec Γ(U), X → Spec Γ(X) is cartesian (stated for affine f)”.

Sources

LeanAlgebraicGeometry.isQuasiProjective_tfae_of_exists_isAmple · AlgebraicGeometry.QuasiProjectiveSchemesOver.baseChange · AlgebraicGeometry.isQuasiProjective_comp_of_exists_isAmple · AlgebraicGeometry.isQuasiProjective_pullback_snd_comp · AlgebraicGeometry.quasiProjectiveOver_isClosedUnderBinaryProducts · AlgebraicGeometry.isQuasiProjective_of_isQuasiAffineHom · AlgebraicGeometry.isQuasiProjective_of_locallyQuasiFinite_of_isSeparated · AlgebraicGeometry.isQuasiProjective_of_isImmersion

Section37.50 Projective schemes #

Section 37.50 of the Stacks Project, Tag 0B44. 4 tags here are carried by 8 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B44, the section

Tag 0B44 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.isProjective_tfae_of_exists_isAmple, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemesSection.lean, line 23 (StacksFrontier): “the characterizations of projectivity over a base with an ample invertible sheaf”.
AlgebraicGeometry.ProjectiveSchemesOver.baseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemesSection.lean, line 25 (StacksFrontier): “base change”.
AlgebraicGeometry.isProjective_comp_of_hasAmpleInvertibleSheaf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemesSection.lean, line 26 (StacksFrontier): “composition”.
AlgebraicGeometry.isProjective_pullback_snd_comp, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemesSection.lean, line 27 (StacksFrontier): “fibre products”.
AlgebraicGeometry.isProjective_of_isFinite_of_hasAmpleInvertibleSheaf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemesSection.lean, line 28 (StacksFrontier): “finite morphisms”.
AlgebraicGeometry.projectiveOver_isClosedUnderFiniteCoproducts, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemesSection.lean, line 30 (StacksFrontier): “finite disjoint unions”.
Stacks.AmpleFibreLimit.exists_mem_isRelativelyAmple_of_isAmple_fibre, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemesSection.lean, line 32 (StacksFrontier): “projectivity spreads out from a fibre”.

Tag 0B45, a lemma

Tag 0B45 in the Stacks Project.

AlgebraicGeometry.exists_sheafGradedAlgebra_of_isProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveOverAmpleBase.lean, line 245. The attribute's comment: “clause (8), reached from clause (1)”.

Stacks Tag 0B45, clause (1) implies clause (8). A projective morphism exhibits its source as the relative homogeneous spectrum of a quasi-coherent graded 𝒪_S-algebra generated in degree one whose degree-one piece is of finite type.

AlgebraicGeometry.IsProjective is a closed immersion j : X ⟶ 𝐏(ℰ) over S for a quasi-coherent ℰ of finite type, and 𝐏(ℰ) is Proj_S(Sym(ℰ)) by definition (Stacks.SymGraded.schemeProjectiveBundle), so no presentation of projective space as a relative Proj is needed: exists_sheafGradedAlgebra_of_isClosedImmersion applies to j at once. Its three hypotheses on Sym(ℰ) are proved — Stacks.SymGraded.isGeneratedInDegreeOneAt_schemeSheafGradedAlgebra, Stacks.SymGraded.quasiCompact_schemeProjectiveBundleToBase, and, for the degree-one piece, AlgebraicGeometry.Scheme.Modules.symmetricAlgebraGenIso, which identifies Sym¹(ℰ) with ℰ.

theorem exists_sheafGradedAlgebra_of_isProjective {X S : Scheme.{u}} {f : X ⟶ S}
    (hf : IsProjective f) :
    ∃ A : SheafGradedAlgebra.{u} S,
      Stacks.AlgebraicGeometry.ProjRepresentsF1.IsGeneratedInDegreeOne A ∧
        (A.piece 1).IsFiniteType ∧
        ∃ e : X ≅ (relativeProj A).scheme, e.hom ≫ (relativeProj A).toBase = f

AlgebraicGeometry.isProjective_tfae_of_exists_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveOverAmpleBase.lean, line 376.

Stacks Project, Tag 0B45. Let S be a scheme carrying an ample invertible module and let f : X ⟶ S be a morphism of schemes. The following are equivalent:

f is projective;

f is H-projective;

f is quasi-projective and proper;

f is H-quasi-projective and proper;

f is proper and X carries an ample invertible module;

f is proper and carries an f-ample invertible module;

f is proper and carries an f-very ample invertible module;

X is, over S, the relative homogeneous spectrum of a quasi-coherent graded 𝒪_S-algebra generated in degree one over its degree-zero part whose degree-one piece is of finite type.

Nothing is assumed beyond the source's own hypothesis on the base. Conditions (1) to (7) are AlgebraicGeometry.isProjective_tfae_seven_of_exists_isAmple; (8) ⟹ (1) is the source's citation Tag 0B3U, AlgebraicGeometry.isProjective_relativeProj_toBase; and (1) ⟹ (8) is the source's other citation, Tag 0801, applied to the closed immersion X ⟶ 𝐏(ℰ) that clause (1) is, which is AlgebraicGeometry.exists_sheafGradedAlgebra_of_isProjective above.

theorem isProjective_tfae_of_exists_isAmple
    {X S : Scheme.{u}} (f : X ⟶ S)
    (hS : ∃ (M : S.Modules) (hM : Stacks.Ample.IsInvertibleModule S M),
      letI : Stacks.Ample.IsInvertibleModule S M := hM
      Stacks.Ample.IsAmple S M) :
    List.TFAE
      [IsProjective f,
        IsProjectiveMorphism f,
        IsQuasiProjective f ∧ IsProper f,
        IsHQuasiProjective f ∧ IsProper f,
        IsProper f ∧
          ∃ (L : X.Modules) (hL : Stacks.Ample.IsInvertibleModule X L),
            letI : Stacks.Ample.IsInvertibleModule X L := hL
            Stacks.Ample.IsAmple X L,
        IsProper f ∧
          ∃ (L : X.Modules) (hL : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
              X.ringCatSheaf.2 L),
            letI : AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
              X.ringCatSheaf.2 L := hL
            Stacks.RelativeAmple.IsRelativelyAmple f L,
        IsProper f ∧
          ∃ (L : X.Modules) (hL : Stacks.Ample.IsInvertibleModule X L),
            letI : Stacks.Ample.IsInvertibleModule X L := hL
            Stacks.Tag01VMVeryAmple.IsRelativelyVeryAmple f L,
        ∃ A : SheafGradedAlgebra.{u} S,
          Stacks.AlgebraicGeometry.ProjRepresentsF1.IsGeneratedInDegreeOne A ∧
            (A.piece 1).IsFiniteType ∧
            ∃ e : X ≅ (relativeProj A).scheme,
              e.hom ≫ (relativeProj A).toBase = f]

Tag 0B46, a lemma

Tag 0B46 in the Stacks Project.

AlgebraicGeometry.ProjectiveSchemesOver.baseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemes.lean, line 243. The attribute's comment: “base change”.

Stacks Project, Tag 0B46, clause (1). For a morphism of bases g : S' ⟶ S, base change along g is a functor P_S ⥤ P_{S'}: the fibre product S' ×_S X of a scheme X projective over S is projective over S'.

The object part is the first assertion of Tag 02V6, AlgebraicGeometry.IsProjective.of_isPullback, applied to the fibre-product square. Its Tag 01O3 input is AlgebraicGeometry.projectiveBundleBaseChangeComparison, a theorem, so nothing is assumed.

def ProjectiveSchemesOver.baseChange
    {S S' : Scheme.{u}} (g : S' ⟶ S) : ProjectiveSchemesOver S ⥤ ProjectiveSchemesOver S'

AlgebraicGeometry.isProjective_comp_of_hasAmpleInvertibleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemes.lean, line 259. The attribute's comment: “composition”.

Stacks Project, Tag 0B46, clause (2). Let S carry an ample invertible sheaf. If f : X ⟶ S is projective and g : Y ⟶ X is projective, then g ≫ f : Y ⟶ S is projective.

This is the source's proof. Condition (5) of Tag 0B45 at the base S makes f proper with X carrying an ample invertible sheaf; the same condition at the base X makes g proper with Y carrying an ample invertible sheaf; a composition of proper morphisms is proper (Tag 01W3); and condition (5) read backwards at the base S returns projectivity of g ≫ f. Condition (5) is part of the unconditional cycle of Tag 0B45, so nothing is assumed.

theorem isProjective_comp_of_hasAmpleInvertibleSheaf
    {X Y S : Scheme.{u}} (g : Y ⟶ X) (f : X ⟶ S)
    (hS : HasAmpleInvertibleSheaf S) (hf : IsProjective f) (hg : IsProjective g) :
    IsProjective (g ≫ f)

AlgebraicGeometry.isProjective_pullback_snd_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemes.lean, line 277. The attribute's comment: “fibre products”.

Stacks Project, Tag 0B46, clause (3). P_S is closed under fibre products over S. For f : X ⟶ S and g : Y ⟶ S projective and S carrying an ample invertible sheaf, the structure morphism X ×_S Y ⟶ S is projective.

The source's proof: the projection X ×_S Y ⟶ Y is a base change of f, hence projective by clause (1), and clause (2) composes it with g.

theorem isProjective_pullback_snd_comp
    {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
    (hS : HasAmpleInvertibleSheaf S) (hf : IsProjective f) (hg : IsProjective g) :
    IsProjective (pullback.snd f g ≫ g)

AlgebraicGeometry.isProjective_of_isFinite_of_hasAmpleInvertibleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemes.lean, line 348. The attribute's comment: “finite morphisms”.

Stacks Project, Tag 0B46, clause (5). A finite morphism f : X ⟶ S over a base carrying an ample invertible sheaf is projective, so X is an object of P_S.

The source cites Tag 0B3I, which is about an arbitrary base and whose proof in this repository is conditional. Over the base of Tag 0B46 none of that is needed: a finite morphism is proper and quasi-affine, so 𝒪_X is f-ample by Tag 0891 in the form Stacks.AmplePullback.isRelativelyAmple_of_isQuasiAffineHom_of_iso_unitModule, which is condition (6) of Tag 0B45, and condition (6) ⟹ condition (1) belongs to the unconditional cycle of that tag.

theorem isProjective_of_isFinite_of_hasAmpleInvertibleSheaf {X S : Scheme.{u}} (f : X ⟶ S)
    [IsFinite f] (hS : HasAmpleInvertibleSheaf.{u} S) : IsProjective f

AlgebraicGeometry.projectiveOver_isClosedUnderFiniteCoproducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Projective/ProjectiveSchemes.lean, line 444. The attribute's comment: “finite disjoint unions”. References: EGA II (5.5.6), “special case”.

Stacks Project, Tag 0B46, clause (4). P_S is closed under finite disjoint unions, for S carrying an ample invertible sheaf. This includes the empty disjoint union.

The empty and the binary cases are AlgebraicGeometry.isProjective_of_isEmpty and AlgebraicGeometry.isProjective_coprod_desc, and CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts.mk' assembles them into every finite disjoint union.

theorem projectiveOver_isClosedUnderFiniteCoproducts (S : Scheme.{u})
    (hS : HasAmpleInvertibleSheaf S) :
    (projectiveOver S).IsClosedUnderFiniteCoproducts

Tag 0D2S, a lemma

Tag 0D2S in the Stacks Project.

Stacks.AmpleFibreLimit.exists_mem_isRelativelyAmple_of_isAmple_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleFibreLimit/Basic.lean, line 473. References: EGA IV (9.6.4).

[Stacks, Tag 0D2S]. Let f : X ⟶ S be a proper morphism of schemes, let ℒ be an invertible 𝒪_X-module and let y be a point of S such that ℒ_y is ample on the fibre X_y. Then y has an open neighbourhood V ⊆ S such that ℒ|_{f⁻¹V} is ample relative to f⁻¹V / V.

No hypothesis on S: this is [Stacks, Tag 0D2N], Stacks.AmpleFibreNeighbourhood.exists_mem_isRelativelyAmple_of_isAmple_fibre, with its Noetherian hypothesis removed by the limit argument described in the module documentation. The statement is otherwise the same, down to the spelling of the hypothesis and of the conclusion, and invertibility of ℒ_y is an instance rather than a hypothesis for the same reason as there.

The base is replaced by an affine — hence quasi-compact and quasi-separated — open neighbourhood A of y, which is legitimate in both directions: the hypothesis transfers by Stacks.AmpleFibreLimit.isAmple_fibre_morphismRestrict, and the conclusion transfers back along the isomorphism of arrows AlgebraicGeometry.morphismRestrictRestrict by Stacks.AmpleFibreLimit.isRelativelyAmple_pullbackModule_of_commSq, whose two horizontal morphisms are in this instance isomorphisms.

theorem exists_mem_isRelativelyAmple_of_isAmple_fibre {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] (L : X.Modules) [IsInvertibleModule X L] (y : S)
    (hL : IsAmple (f.fiber y) (pullbackModule (f.fiberι y) L)) :
    ∃ V : S.Opens, y ∈ V ∧
      Stacks.RelativeAmple.IsRelativelyAmple (f ∣_ V) (pullbackModule (f ⁻¹ᵁ V).ι L)

Sources

LeanAlgebraicGeometry.isProjective_tfae_of_exists_isAmple · AlgebraicGeometry.ProjectiveSchemesOver.baseChange · AlgebraicGeometry.isProjective_comp_of_hasAmpleInvertibleSheaf · AlgebraicGeometry.isProjective_pullback_snd_comp · AlgebraicGeometry.isProjective_of_isFinite_of_hasAmpleInvertibleSheaf · AlgebraicGeometry.projectiveOver_isClosedUnderFiniteCoproducts · Stacks.AmpleFibreLimit.exists_mem_isRelativelyAmple_of_isAmple_fibre · AlgebraicGeometry.exists_sheafGradedAlgebra_of_isProjective

Section37.51 Proj and Spec #

Section 37.51 of the Stacks Project, Tag 0EKF. 4 tags here are carried by 183 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0EKF, the section

Tag 0EKF in the Stacks Project.

Stacks.Truncation.span_degreeOne_pow_eq_truncationIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Truncation.lean, line 727. The attribute's comment: “the clause that makes the section's cone a blowup: if A is generated over A₀ by elements of degree one then (A₊)^m = A_{≥ m} for every m ≥ 0, so that B = ⨁_{d ≥ 0} A_{≥ d} is the Rees algebra of A₊ and L = Proj(B) ⟶ X = Spec(A) is the blowing up of Z = V(A₊). Nothing else of Section 37.51 is claimed here: the graded ring B with its maps σ, ψ, τ is Tag 0EKG, already in this file; the five localization facts about σ(f), σ(A_d) and ker(τ) on D₊(ψ(f)), the identification B_{σ(f)} ≅ A_f[T] that makes L ⟶ X an isomorphism over U = X ∖ Z, and the description of L over the largest open of P on which 𝒪_P(1) is invertible, are not proved”. References: EGA II (8.2.10), “(iii), special case”.

If A is generated over A_0 by its degree-one part, in the form A_{d+1} ⊆ A_1 · A_d for every d, then (A_+)^m = A_{≥ m} for every m ≥ 0.

theorem span_degreeOne_pow_eq_truncationIdeal
    (hgen : ∀ d : ℕ, ∀ a ∈ 𝒜 (d + 1),
      a ∈ Ideal.span (𝒜 1 : Set A) * Ideal.span (𝒜 d : Set A))
    (m : ℕ) : Ideal.span (𝒜 1 : Set A) ^ m = truncationIdeal 𝒜 m

Tag 0EKG, an equation

Tag 0EKG in the Stacks Project.

Stacks.AlgebraicGeometry.ProjAndSpec.zToX, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 137. The attribute's comment: “the morphism Z → X”.

The closed immersion Z = Spec A₀ ⟶ X = Spec A induced by the projection A → A₀.

def zToX : Spec (CommRingCat.of (𝒜 0)) ⟶ Spec (CommRingCat.of A)

Stacks.AlgebraicGeometry.ProjAndSpec.xToZ, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 142. The attribute's comment: “the morphism X → Z”.

The morphism X = Spec A ⟶ Z = Spec A₀ induced by the inclusion A₀ → A.

def xToZ : Spec (CommRingCat.of A) ⟶ Spec (CommRingCat.of (𝒜 0))

Stacks.AlgebraicGeometry.ProjAndSpec.openU, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 154. The attribute's comment: “the open U ⊆ X”.

The open U = X ∖ V(A₊) of X = Spec A: the union of the standard opens D(f) of the homogeneous elements f of positive degree.

def openU : (Spec (CommRingCat.of A)).Opens

Stacks.AlgebraicGeometry.ProjAndSpec.projMapDomain_tau_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 288. The attribute's comment: “τ defines a morphism on all of Proj(A)”.

τ induces a morphism on all of P = Proj 𝒜.

theorem projMapDomain_tau_eq_top : mapDomain ℬ 𝒜 c.tau = ⊤

Stacks.AlgebraicGeometry.ProjAndSpec.projMapDomain_psi_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 294. The attribute's comment: “ψ defines a morphism on all of Proj(B)”.

ψ induces a morphism on all of L = Proj ℬ: the power condition is exactly the radical inclusion of irrelevant ideals that makes the standard opens D₊(ψ f) cover Proj ℬ.

theorem projMapDomain_psi_eq_top : mapDomain 𝒜 ℬ c.psi = ⊤

Stacks.AlgebraicGeometry.ProjAndSpec.pi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 311. The attribute's comment: “the cone projection π : L → P”.

The cone projection π : L = Proj ℬ ⟶ P = Proj 𝒜, induced by ψ.

def pi : AlgebraicGeometry.Proj ℬ ⟶ AlgebraicGeometry.Proj 𝒜

Stacks.AlgebraicGeometry.ProjAndSpec.zeroSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 316. The attribute's comment: “the zero section 0 : P → L”.

The zero section 0 : P = Proj 𝒜 ⟶ L = Proj ℬ, induced by τ.

def zeroSection : AlgebraicGeometry.Proj 𝒜 ⟶ AlgebraicGeometry.Proj ℬ

Stacks.AlgebraicGeometry.ProjAndSpec.toSpecA, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 327. The attribute's comment: “the structure morphism L → X”.

The structure morphism L = Proj ℬ ⟶ X = Spec A, using the identification σ of A with the degree-zero part of B.

def toSpecA : AlgebraicGeometry.Proj ℬ ⟶ Spec (CommRingCat.of A)

Stacks.AlgebraicGeometry.ProjAndSpec.openUInL, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 332. The attribute's comment: “the open U ⊆ L”.

The inverse image in L of the open U = X ∖ V(A₊).

def openUInL : (AlgebraicGeometry.Proj ℬ).Opens

Stacks.AlgebraicGeometry.ProjAndSpec.pi_preimage_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 362. The attribute's comment: “π⁻¹ of a standard open”.

The inverse image under π of a standard open of P is the standard open of the image element: π⁻¹(D₊(f)) = D₊(ψ f).

theorem pi_preimage_basicOpen (f : A) (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    pi c ⁻¹ᵁ Proj.basicOpen 𝒜 f = Proj.basicOpen ℬ (c.psi f)

Stacks.AlgebraicGeometry.ProjAndSpec.isAffineHom_pi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 384. The attribute's comment: “π is affine”.

The cone projection is affine. The standard opens of positive-degree homogeneous elements cover P and are affine, and their inverse images are again standard opens of positive-degree homogeneous elements.

theorem isAffineHom_pi : IsAffineHom (pi c)

Stacks.AlgebraicGeometry.ProjAndSpec.zeroSection_comp_pi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 393. The attribute's comment: “π ∘ 0 = id_P”.

π ∘ 0 = id_P: the zero section is a section of the cone projection.

theorem zeroSection_comp_pi : zeroSection c ≫ pi c = 𝟙 (AlgebraicGeometry.Proj 𝒜)

Stacks.AlgebraicGeometry.ProjAndSpec.isClosedImmersion_zeroSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 403. The attribute's comment: “0 : P → L is a closed immersion”.

The zero section is a closed immersion, τ being surjective in every degree.

theorem isClosedImmersion_zeroSection : IsClosedImmersion (zeroSection c)

Stacks.AlgebraicGeometry.ProjAndSpec.range_zeroSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 470. The attribute's comment: “the image of the zero section is the inverse image of Z”.

The zero section maps onto the inverse image of Z. Set theoretically the image of 0 : P → L is the complement of the part of L lying over U = X ∖ V(A₊). A point of the image contains σ (A₊) because τ ∘ σ kills the positive degrees; conversely a homogeneous prime of B containing σ (A₊) is the image of its own contraction along ψ, which is relevant because ψ is everywhere defined.

theorem range_zeroSection :
    Set.range (zeroSection c) = ((openUInL c : Set (AlgebraicGeometry.Proj ℬ)))ᶜ

Stacks.AlgebraicGeometry.ProjAndSpec.isAffineHom_pi_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 519. The attribute's comment: “U → P is affine”.

The punctured cone is affine over P. Over the standard open D₊(f) the part of L lying over U is the standard open D₊(σ f · ψ f) of a positive-degree homogeneous element, hence affine.

theorem isAffineHom_pi_restrict : IsAffineHom ((openUInL c).ι ≫ pi c)

Stacks.AlgebraicGeometry.ProjAndSpec.pi_comp_toSpecZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 546. The attribute's comment: “the square L → P, X → Z commutes”.

The right square commutes: L → P → Z equals L → X → Z.

theorem pi_comp_toSpecZero :
    pi c ≫ Proj.toSpecZero 𝒜 = toSpecA c ≫ xToZ 𝒜

Stacks.AlgebraicGeometry.ProjAndSpec.zeroSection_comp_toSpecA, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpec.lean, line 553. The attribute's comment: “the square P → L, Z → X commutes”.

The left square commutes: P → L → X equals P → Z → X.

theorem zeroSection_comp_toSpecA :
    zeroSection c ≫ toSpecA c = Proj.toSpecZero 𝒜 ≫ zToX 𝒜

Stacks.AlgebraicGeometry.ProjConeTwist.truncationCone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecDiagram.lean, line 320. The attribute's comment: “π : L → P is a cone over P, whose direct-image algebra is graded by the twists O_P(m), m ≥ 0”.

π : L ⟶ P is a cone over P in the sense of [Stacks, Tag 062R], graded by the algebra ⨁_{m ≥ 0} 𝒪_P(m) of nonnegative twists: π is affine, the homogeneous pieces include in π_* 𝒪_L by the degreewise inclusions 𝒪_P(m) ⟶ π_* 𝒪_L, every function on the cone is locally a unique finite sum of homogeneous ones, the inclusions are multiplicative, the negative pieces vanish and the degree-zero piece is 𝒪_P, included by the structure map.

def truncationCone : AbstractCone (AlgebraicGeometry.Proj 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.range_zeroSection_eq_preimage_range_zToX, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecDiagram.lean, line 343. The attribute's comment: “the zero section maps set theoretically onto the inverse image of Z in L”.

The zero section 0 : P ⟶ L maps set theoretically onto the inverse image of Z in L: its image is the inverse image under σ : L ⟶ X of the image of Z = Spec A₀ ⟶ X.

theorem range_zeroSection_eq_preimage_range_zToX :
    Set.range (zeroSection 𝒜) = toSpecA 𝒜 ⁻¹' Set.range (ProjAndSpec.zToX 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.zeroSection_appLE_coneIota_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecDiagram.lean, line 442. The attribute's comment: “the zero section 0 : P → L is the vertex of the cone π”.

The zero section 0 : P ⟶ L is the vertex of the cone π : L ⟶ P: it is a section of π, and pulling functions back along it kills every homogeneous piece 𝒪_P(m), m > 0, of π_* 𝒪_L = ⨁_{m ≥ 0} 𝒪_P(m), over every open of P. So 0 is the closed immersion cut out by the positive part of the grading, Spec_P(𝒪_P) ⟶ Spec_P(⨁_{m ≥ 0} 𝒪_P(m)).

theorem zeroSection_appLE_coneIota_eq_zero (m : ℤ) (hm : 0 < m)
    (U : Opens (ProjectiveSpectrum.top 𝒜)) (s : (nonnegTwistingSheaf 𝒜 m).val.obj (op U)) :
    (zeroSection 𝒜).appLE (pi 𝒜 ⁻¹ᵁ U) U (le_zeroSection_preimage_pi_preimage 𝒜 U)
      ((coneIota 𝒜 m).val.app (op U) s) = 0

Stacks.AlgebraicGeometry.ProjConeTwist.projAndSpec_diagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecDiagram.lean, line 493. The attribute's comment: “the commutative diagram Spec_P(⨁_{m ∈ ℤ} O_P(m)) → L = Spec_P(⨁_{m ≥ 0} O_P(m)) → P over U → X → Z, with π a cone whose zero section maps set theoretically onto the inverse image of Z in L”. References: EGA II (8.6.3), “special case”.

The diagram of [Stacks, Tag 0EKG]. Let A be a graded ring, X = Spec A, Z = V(A₊) = Spec A₀, U = X ∖ Z, P = Proj A, and let L = Proj B for B = ⨁_{d ≥ 0} A_{≥ d}, with cone projection π : L ⟶ P, structure morphism σ : L ⟶ X and zero section 0 : P ⟶ L. Then, writing j : Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ⟶ L for the top-left arrow and e : Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ≅ U for the left identification:

π is a cone over P (truncationCone, graded by ⨁_{m ≥ 0} 𝒪_P(m), whose pieces are the twisting sheaves 𝒪_P(m), m ≥ 0), and L = Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) over P;

j lies over P, it is an open immersion, and its image is the part of L over U;

e is an identification over P;

the left square j ≫ σ = e ≫ (U ⟶ X) and the right square π ≫ (P ⟶ Z) = σ ≫ (X ⟶ Z) commute;

the zero section is a section of π, it is the vertex of the cone (pulling back along it kills the pieces 𝒪_P(m), m > 0, of π_* 𝒪_L), and it maps set theoretically onto the inverse image of Z in L.

theorem projAndSpec_diagram :
    -- `π` is a cone over `P`, graded by the nonnegative twists
    (truncationCone 𝒜).π = pi 𝒜 ∧
    (truncationCone 𝒜).grading = nonnegTwistAlgebra 𝒜 ∧
    (truncationCone 𝒜).ι = coneIota 𝒜 ∧
    (∀ m : ℕ, (truncationCone 𝒜).grading.piece m = twistingSheaf 𝒜 m) ∧
    (∀ m : ℤ, (integerTwistAlgebra 𝒜).piece m = twistingSheaf 𝒜 m) ∧
    -- `L = Spec_P(⨁_{m ≥ 0} 𝒪_P(m))` over `P`
    (coneProjIsoRelativeSpecTwistAlgebra 𝒜).hom ≫
        relativeSpecToBase (nonnegTwistAlgebraSheaf 𝒜) = pi 𝒜 ∧
    -- the top-left arrow lies over `P`, is an open immersion, with image the part of `L` over `U`
    puncturedToConeProj 𝒜 ≫ pi 𝒜 = relativeSpecToBase (integerTwistAlgebraSheaf 𝒜) ∧
    IsOpenImmersion (puncturedToConeProj 𝒜) ∧
    (puncturedToConeProj 𝒜).opensRange = openUInL 𝒜 ∧
    -- the left identification `Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) = U` lies over `P`
    (puncturedConeRelativeSpecTwistAlgebraIsoOpenU 𝒜).hom ≫ openUToProj 𝒜 =
      relativeSpecToBase (integerTwistAlgebraSheaf 𝒜) ∧
    -- the left square
    puncturedToConeProj 𝒜 ≫ toSpecA 𝒜 =
      (puncturedConeRelativeSpecTwistAlgebraIsoOpenU 𝒜).hom ≫ (ProjAndSpec.openU 𝒜).ι ∧
    -- the right square
    pi 𝒜 ≫ Proj.toSpecZero 𝒜 = toSpecA 𝒜 ≫ ProjAndSpec.xToZ 𝒜 ∧
    -- the zero section
    zeroSection 𝒜 ≫ pi 𝒜 = 𝟙 (AlgebraicGeometry.Proj 𝒜) ∧
    (∀ (m : ℤ), 0 < m → ∀ (U : Opens (ProjectiveSpectrum.top 𝒜))
        (s : (nonnegTwistingSheaf 𝒜 m).val.obj (op U)),
      (zeroSection 𝒜).appLE (pi 𝒜 ⁻¹ᵁ U) U (le_zeroSection_preimage_pi_preimage 𝒜 U)
        ((coneIota 𝒜 m).val.app (op U) s) = 0) ∧
    Set.range (zeroSection 𝒜) = toSpecA 𝒜 ⁻¹' Set.range (ProjAndSpec.zToX 𝒜)

Stacks.AlgebraicGeometry.ProjAndSpecTruncation.isIso_toSpecA_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecIsoOverU.lean, line 235. The attribute's comment: “L → X is an isomorphism over U”.

The structure morphism L ⟶ X is an isomorphism over U = X ∖ V(A₊). This is the equality on the left of the diagram of [Stacks, Tag 0EKG]: being an isomorphism over an open is local on that open, and over each standard open of a positive-degree homogeneous element the morphism is an isomorphism.

theorem isIso_toSpecA_restrict : IsIso (toSpecA 𝒜 ∣_ ProjAndSpec.openU 𝒜)

Stacks.AlgebraicGeometry.ProjAndSpecTruncation.openUInL_ι_comp_toSpecA, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecIsoOverU.lean, line 264. The attribute's comment: “the part of L over U is U, over X”.

The punctured cone is the open U, over X: the part of L lying over U maps to X through the isomorphism of Stacks.AlgebraicGeometry.ProjAndSpecTruncation.isIso_toSpecA_restrict followed by the inclusion of U.

theorem openUInL_ι_comp_toSpecA :
    (openUInL 𝒜).ι ≫ toSpecA 𝒜 =
      (toSpecA 𝒜 ∣_ ProjAndSpec.openU 𝒜) ≫ (ProjAndSpec.openU 𝒜).ι

Stacks.AlgebraicGeometry.ProjAndSpecTruncation.truncationConeData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecTruncation.lean, line 364. The attribute's comment: “the truncation algebra B = ⨁_{d ≥ 0} A_{≥ d} is cone data over A”.

The truncation algebra B = ⨁_{d ≥ 0} A_{≥ d} is cone data over A: the maps ψ, τ and σ satisfy τ ∘ ψ = id, the two formulas tying σ to ψ and τ, and the three divisibility conditions.

def truncationConeData : ProjAndSpec.ConeData 𝒜 (grading 𝒜)

Stacks.AlgebraicGeometry.ProjAndSpecTruncation.openUInL_eq_iSup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecTruncation.lean, line 424. The attribute's comment: “U ⊆ L is a union of standard opens, for the truncation algebra”.

The part of L lying over U is the union of the standard opens of the σ-images of the positive-degree homogeneous elements of A.

theorem openUInL_eq_iSup :
    openUInL 𝒜 = ⨆ (d : ℕ) (_ : 0 < d) (f : 𝒜 d),
      Proj.basicOpen (grading 𝒜) ((sigma 𝒜 (f : A) : grading 𝒜 0) : TruncationRing 𝒜)

Stacks.AlgebraicGeometry.ProjAndSpecTruncation.openUInL_inf_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecTruncation.lean, line 439. The attribute's comment: “U ⊆ L over a standard open, for the truncation algebra”.

Over a standard open D₊(f) of P the part of L lying over U is the standard open of σ f · ψ f.

theorem openUInL_inf_basicOpen (f : A) (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    openUInL 𝒜 ⊓ Proj.basicOpen (grading 𝒜) (psi 𝒜 f) =
      Proj.basicOpen (grading 𝒜)
        (((sigma 𝒜 f : grading 𝒜 0) : TruncationRing 𝒜) * psi 𝒜 f)

Stacks.AlgebraicGeometry.ProjAndSpecTruncation.toSpecA_preimage_specBasicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecTruncation.lean, line 501. The attribute's comment: “the inverse image in L of a standard open of X”.

The inverse image in L of a standard open of X is the standard open of σ f · ψ f, a homogeneous element of positive degree, for f homogeneous of positive degree.

theorem toSpecA_preimage_specBasicOpen (f : A) (d : ℕ) (hf : f ∈ 𝒜 d) :
    toSpecA 𝒜 ⁻¹ᵁ ProjAndSpec.specBasicOpen f =
      Proj.basicOpen (grading 𝒜)
        (((sigma 𝒜 f : grading 𝒜 0) : TruncationRing 𝒜) * psi 𝒜 f)

Stacks.AlgebraicGeometry.ProjAndSpecTruncation.isAffineOpen_toSpecA_preimage_specBasicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecTruncation.lean, line 512. The attribute's comment: “the part of L over a standard open of X is affine”.

The part of L lying over a standard open of X is affine, for f homogeneous of positive degree.

theorem isAffineOpen_toSpecA_preimage_specBasicOpen (f : A) (d : ℕ) (hf : f ∈ 𝒜 d)
    (hd : 0 < d) : IsAffineOpen (toSpecA 𝒜 ⁻¹ᵁ ProjAndSpec.specBasicOpen f)

Stacks.AlgebraicGeometry.ProjAndSpec.awayι_comp_pi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeChart.lean, line 68. The attribute's comment: “the cone projection on an affine chart is Spec of the map of degree-zero localizations”.

On the affine chart Spec B_{(ψ f)} of L the cone projection is Spec of the map A_{(f)} ⟶ B_{(ψ f)} of degree-zero localizations. The chart of L is carried by the inclusion of D₊(ψ f), on which the cone projection is the local morphism attached to f, and that local morphism is by construction the one of the degree-zero localizations.

theorem awayι_comp_pi :
    Proj.awayι ℬ (c.psi f) (c.psi.map_mem hf) hd ≫ pi c =
      Spec.map (CommRingCat.ofHom (Away.map c.psi f)) ≫ Proj.awayι 𝒜 f hf hd

Stacks.AlgebraicGeometry.ProjAndSpec.awayToSection_comp_pi_appLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeChart.lean, line 159. The attribute's comment: “the cone projection on functions over a standard open is the map of degree-zero localizations”.

The cone projection acts on functions over a standard open by the map of degree-zero localizations. Through the identifications A_{(f)} = Γ(P, D₊(f)) and B_{(ψ f)} = Γ(L, D₊(ψ f)) of [Stacks, Tag 01M6], the pullback of functions along π is HomogeneousLocalization.Away.map ψ f. This is the module-theoretic content of the chart description Stacks.AlgebraicGeometry.ProjAndSpec.awayι_comp_pi: it says which A_{(f)}-algebra the functions on the part of L over D₊(f) form.

theorem awayToSection_comp_pi_appLE :
    Proj.awayToSection 𝒜 f ≫ (pi c).appLE (Proj.basicOpen 𝒜 f)
        (Proj.basicOpen ℬ (c.psi f)) (pi_preimage_basicOpen c f d hf hd).ge =
      CommRingCat.ofHom (Away.map c.psi f) ≫ Proj.awayToSection ℬ (c.psi f)

Stacks.AlgebraicGeometry.ProjAndSpec.awayToSection_comp_pi_appLE_sigmaMulPsi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeChartPunctured.lean, line 105. The attribute's comment: “the punctured cone projection on functions over a standard open is the map of degree-zero localizations A_(f) to B_(sigma f * psi f)”.

On the chart D₊(σ f · ψ f) of the punctured cone the projection acts on functions by the map A_{(f)} ⟶ B_{(σ f · ψ f)} of degree-zero localizations. Through the identifications A_{(f)} = Γ(P, D₊(f)) and B_{(σ f · ψ f)} = Γ(L, D₊(σ f · ψ f)) of [Stacks, Tag 01M6], the pullback of functions along π to the part of U over D₊(f) is puncturedAwayMap.

theorem awayToSection_comp_pi_appLE_sigmaMulPsi (hd : 0 < d) (hf : f ∈ 𝒜 d) :
    Proj.awayToSection 𝒜 f ≫ (pi c).appLE (Proj.basicOpen 𝒜 f)
        (Proj.basicOpen ℬ ((c.sigma f : B) * c.psi f))
        (basicOpen_sigmaMulPsi_le_pi_preimage c hd hf) =
      CommRingCat.ofHom (puncturedAwayMap c hd hf) ≫
        Proj.awayToSection ℬ ((c.sigma f : B) * c.psi f)

Stacks.AlgebraicGeometry.ProjAndSpec.awayToSection_comp_puncturedPi_appLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeChartPunctured.lean, line 137. The attribute's comment: “the restricted projection pi|_U on functions over a standard open, on the chart given by the inverse image of D+(sigma f * psi f)”.

The same statement for the restricted projection π|_U : U ⟶ P, whose chart over D₊(f) is the inverse image of D₊(σ f · ψ f) under the open immersion of U: there too the pullback of functions is puncturedAwayMap, followed by restriction along that open immersion.

theorem awayToSection_comp_puncturedPi_appLE (hd : 0 < d) (hf : f ∈ 𝒜 d) :
    Proj.awayToSection 𝒜 f ≫ ((openUInL c).ι ≫ pi c).appLE (Proj.basicOpen 𝒜 f)
        ((openUInL c).ι ⁻¹ᵁ Proj.basicOpen ℬ ((c.sigma f : B) * c.psi f))
        (((TopologicalSpace.Opens.map (openUInL c).ι.base).map
          (homOfLE (basicOpen_sigmaMulPsi_le_pi_preimage c hd hf))).le) =
      CommRingCat.ofHom (puncturedAwayMap c hd hf) ≫
        Proj.awayToSection ℬ ((c.sigma f : B) * c.psi f) ≫
          (openUInL c).ι.appLE (Proj.basicOpen ℬ ((c.sigma f : B) * c.psi f))
            ((openUInL c).ι ⁻¹ᵁ Proj.basicOpen ℬ ((c.sigma f : B) * c.psi f)) le_rfl

Stacks.AlgebraicGeometry.ProjConeTwist.coneRelativeSpecIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeRelativeSpec.lean, line 115. The attribute's comment: “L is, over P, the relative spectrum of the direct-image algebra of the cone”.

L = Spec_P(π_* 𝒪_L): the cone is, over P = Proj A, the relative spectrum of its direct-image algebra, the cone projection being affine.

def coneRelativeSpecIso :
    Over.mk (ProjAndSpec.pi c) ≅
      Over.mk (relativeSpecToBase (pushforwardAlgebra (ProjAndSpec.pi c)))

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeRelativeSpecIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeRelativeSpec.lean, line 123. The attribute's comment: “the punctured cone is, over P, the relative spectrum of its direct-image algebra”.

U = Spec_P((π|_U)_* 𝒪_U): the punctured cone is, over P = Proj A, the relative spectrum of its direct-image algebra, the restricted cone projection being affine.

def puncturedConeRelativeSpecIso :
    Over.mk ((ProjAndSpec.openUInL c).ι ≫ ProjAndSpec.pi c) ≅
      Over.mk (relativeSpecToBase
        (pushforwardAlgebra ((ProjAndSpec.openUInL c).ι ≫ ProjAndSpec.pi c)))

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeRelativeSpecIsoOpenU, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeRelativeSpec.lean, line 201. The attribute's comment: “the relative spectrum of the punctured cone's direct-image algebra is U”. References: EGA II (8.12.5), “special case”; EGA II (8.6.2), “special case”.

The relative spectrum over P of the direct-image algebra of the punctured cone is the open U = X ∖ V(A₊) of X, for the truncation algebra. This is the equality on the left of the diagram of [Stacks, Tag 0EKG]: the punctured cone is that relative spectrum, and L ⟶ X carries it isomorphically onto U.

def puncturedConeRelativeSpecIsoOpenU :
    Stacks.AffineAlgebraEquivalence.relativeSpec
        (pushforwardAlgebra ((openUInL 𝒜).ι ≫ pi 𝒜)) ≅
      (ProjAndSpec.openU 𝒜).toScheme

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeRelativeSpecTwistAlgebraIsoOpenU, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeRelativeSpec.lean, line 248. The attribute's comment: “the left equality: U is Spec_P of the integer twist algebra”. References: EGA II (8.12.5), “special case”; EGA II (8.6.2), “special case”.

Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) = U: the relative spectrum over P = Proj A of the algebra of all integral twists is the open U = X ∖ V(A₊) of X = Spec A. This is the equality on the left of the diagram of [Stacks, Tag 0EKG], with the algebra named as the twist algebra ⨁_{m ∈ ℤ} 𝒪_P(m) itself rather than as the direct image (π|_U)_* 𝒪_U it was computed from: the punctured cone is that relative spectrum by Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeRelativeSpecTwistAlgebraIso, and L ⟶ X carries the punctured cone isomorphically onto U by Stacks.AlgebraicGeometry.ProjAndSpecTruncation.isIso_toSpecA_restrict.

def puncturedConeRelativeSpecTwistAlgebraIsoOpenU :
    Stacks.AffineAlgebraEquivalence.relativeSpec (integerTwistAlgebraSheaf 𝒜) ≅
      (ProjAndSpec.openU 𝒜).toScheme

Stacks.AlgebraicGeometry.ProjConeTwist.degreeZeroRingMap_coneTwistAwayHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraInclusion.lean, line 97. The attribute's comment: “the degreewise inclusion of the sections of O_P(m) into the degree-zero localization of the truncation algebra at psi f, followed by restriction to the chart of the punctured cone, is the punctured degreewise inclusion, for a nonnegative degree m”.

The degreewise inclusion of Γ(D₊(f), 𝒪_P(m)) into the functions on the cone chart, followed by restriction to the chart of the punctured cone, is the degreewise inclusion into the functions on that chart, for m ≥ 0. Both sides are elements of (B[1/σ f · ψ f])₀, and the comparison map to A[1/f] is injective and sends both to the standard-open description of the section one starts from.

theorem degreeZeroRingMap_coneTwistAwayHom (m : ℕ) {d : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (s : (twistingSheaf 𝒜 (m : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    ProjectiveSpectrum.degreeZeroRingMap (grading 𝒜) (psi 𝒜 f) (sigmaMulPsi 𝒜 f)
        ⟨d, hd, GradedRingHom.map_mem (psi 𝒜) hf⟩ ⟨d, hd, sigmaMulPsi_mem_grading 𝒜 d hf⟩
        (basicOpen_sigmaMulPsi_le_psi 𝒜) (coneTwistAwayHom 𝒜 m d hf hd s) =
      puncturedConeTwistAwayHom 𝒜 (m : ℤ) d hf hd s

Stacks.AlgebraicGeometry.ProjConeTwist.appLE_coneTwistApp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraInclusion.lean, line 117. The attribute's comment: “the local degreewise inclusion O_P(m) to pi_* O_L over a standard open, followed by restriction to the punctured cone, is the punctured local degreewise inclusion, for a nonnegative degree m”.

The local degreewise inclusion into π_* 𝒪_L over a standard open, followed by restriction along the open immersion of the punctured cone, is the punctured local degreewise inclusion, for m ≥ 0. Both are read on the chart D₊(σ f · ψ f) of the punctured cone inside the chart D₊(ψ f) of the cone, where restriction of functions is the degree-zero restriction map of B and Stacks.AlgebraicGeometry.ProjConeTwist.degreeZeroRingMap_coneTwistAwayHom applies.

theorem appLE_coneTwistApp (m : ℕ) {d : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (hle : ((openUInL 𝒜).ι ≫ pi 𝒜) ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f ≤
      (openUInL 𝒜).ι ⁻¹ᵁ (pi 𝒜 ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f))
    (s : (twistingSheaf 𝒜 (m : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    ((openUInL 𝒜).ι.appLE (pi 𝒜 ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f)
          (((openUInL 𝒜).ι ≫ pi 𝒜) ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f) hle).hom
        ((coneTwistApp 𝒜 m d hf hd).hom s) =
      (puncturedConeTwistApp 𝒜 (m : ℤ) d hf hd).hom s

Stacks.AlgebraicGeometry.ProjConeTwist.appLE_coneTwistHom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraInclusion.lean, line 161. The attribute's comment: “the degreewise inclusion O_P(m) to pi_ O_L followed by restriction to the punctured cone is the degreewise inclusion O_P(m) to (pi|_U)_ O_U, for a nonnegative degree m”.

The degreewise inclusion 𝒪_P(m) ⟶ π_* 𝒪_L followed by restriction of functions from the cone to the punctured cone is the degreewise inclusion 𝒪_P(m) ⟶ (π|_U)_* 𝒪_U, for m ≥ 0, read on the sections over an arbitrary open of P. Both sides are morphisms out of the sheaf the punctured inclusion is glued from, so it is enough to compare them over the positive-degree standard opens, where the comparison is Stacks.AlgebraicGeometry.ProjConeTwist.appLE_coneTwistApp.

theorem appLE_coneTwistHom_app (m : ℕ) (V : Opens (ProjectiveSpectrum.top 𝒜))
    (hleV : ((openUInL 𝒜).ι ≫ pi 𝒜) ⁻¹ᵁ V ≤ (openUInL 𝒜).ι ⁻¹ᵁ (pi 𝒜 ⁻¹ᵁ V))
    (x : (twistingSheaf 𝒜 (m : ℤ)).val.obj (op V)) :
    ((openUInL 𝒜).ι.appLE (pi 𝒜 ⁻¹ᵁ V) (((openUInL 𝒜).ι ≫ pi 𝒜) ⁻¹ᵁ V) hleV).hom
        ((coneTwistHom 𝒜 m).val.app (op V) x) =
      (puncturedTwistHom 𝒜 (m : ℤ)).val.app (op V) x

Stacks.AlgebraicGeometry.ProjConeTwist.nonnegToIntegerTwistUnitalHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraInclusion.lean, line 207. The attribute's comment: “the inclusion of the nonnegative twist algebra in the integral one, as a unital homomorphism of sheaves of graded algebras”.

The inclusion ⨁_{m ≥ 0} 𝒪_P(m) ⟶ ⨁_{m ∈ ℤ} 𝒪_P(m) as a unital homomorphism of sheaves of graded algebras. It is Stacks.AlgebraicGeometry.ProjConeTwist.nonnegToIntegerTwistAlgebra with the preservation of the degree-zero unit recorded: both unit sections are the unit section Stacks.AlgebraicGeometry.ProjConeTwist.twistOne of the untwisted sheaf, and in degree zero the inclusion is the identity.

def nonnegToIntegerTwistUnitalHom :
    SheafOfModules.GradedAlgebra.UnitalHom (nonnegTwistAlgebra 𝒜) (integerTwistAlgebra 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.nonnegToIntegerTwistAlgebraSheafHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraInclusion.lean, line 219. The attribute's comment: “the inclusion of the nonnegative twist algebra in the integral one, as a morphism of sheaves of commutative algebras over the structure sheaf of P”.

The inclusion of the two twist algebras as a morphism of sheaves of commutative 𝒪_P-algebras, which is the shape the relative spectrum of [Stacks, Tag 01LM] consumes. Its underlying morphism of sheaves of rings is the one the degreewise inclusions induce on the ungraded realizations.

def nonnegToIntegerTwistAlgebraSheafHom :
    nonnegTwistAlgebraSheaf 𝒜 ⟶ integerTwistAlgebraSheaf 𝒜

Stacks.AlgebraicGeometry.ProjConeTwist.appLE_coneIota_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraInclusion.lean, line 235. The attribute's comment: “the inclusion of each homogeneous piece of the nonnegative twist algebra in pi_ O_L, followed by restriction to the punctured cone, is the degreewise inclusion in (pi|_U)_ O_U after the inclusion of the two twist algebras”.

The degreewise inclusion of each homogeneous piece of ⨁_{m ≥ 0} 𝒪_P(m) into π_* 𝒪_L, followed by restriction to the punctured cone, is the degreewise inclusion into (π|_U)_* 𝒪_U composed with the degreewise inclusion of the two twist algebras: the nonnegative-degree case is Stacks.AlgebraicGeometry.ProjConeTwist.appLE_coneTwistHom_app, and in a negative degree the source sheaf is zero, so both sides vanish.

theorem appLE_coneIota_app (i : ℤ) (W : Opens (ProjectiveSpectrum.top 𝒜))
    (hleW : ((openUInL 𝒜).ι ≫ pi 𝒜) ⁻¹ᵁ W ≤ (openUInL 𝒜).ι ⁻¹ᵁ (pi 𝒜 ⁻¹ᵁ W))
    (y : (nonnegTwistingSheaf 𝒜 i).val.obj (op W)) :
    ((openUInL 𝒜).ι.appLE (pi 𝒜 ⁻¹ᵁ W) (((openUInL 𝒜).ι ≫ pi 𝒜) ⁻¹ᵁ W) hleW).hom
        ((coneIota 𝒜 i).val.app (op W) y) =
      (puncturedTwistHom 𝒜 i).val.app (op W) ((nonnegToIntegerApp 𝒜 i).val.app (op W) y)

Stacks.AlgebraicGeometry.ProjConeTwist.ungradedSheafMap_comp_puncturedConeUngradedSheafIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraInclusion.lean, line 292. The attribute's comment: “the inclusion of the two twist algebras is restriction of functions from the cone to the punctured cone, as morphisms of sheaves of rings”.

The inclusion of the two twist algebras is restriction of functions from the cone to the punctured cone, as morphisms of sheaves of rings: the morphism the degreewise inclusions induce on the ungraded realizations, followed by the identification of ⨁_{m ∈ ℤ} 𝒪_P(m) with (π|_U)_* 𝒪_U, is the identification of ⨁_{m ≥ 0} 𝒪_P(m) with π_* 𝒪_L followed by the restriction map of the two direct images.

theorem ungradedSheafMap_comp_puncturedConeUngradedSheafIso :
    SheafOfModules.GradedAlgebra.ungradedSheafMap (nonnegToIntegerTwistUnitalHom 𝒜) ≫
        (puncturedConeUngradedSheafIso 𝒜).hom =
      (coneUngradedSheafIso 𝒜).hom ≫
        Stacks.RelativeSpec.AlgebraSheaf.ringSheafMap
          (coneToPuncturedConeAlgebra (truncationConeData 𝒜))

Stacks.AlgebraicGeometry.ProjConeTwist.nonnegToIntegerTwistAlgebraSheafHom_comp_puncturedConeAlgebraSheafIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraInclusion.lean, line 345. The attribute's comment: “the inclusion of the two twist algebras is restriction of functions from the cone to the punctured cone, as morphisms of sheaves of commutative algebras over the structure sheaf of P”.

The inclusion of the two twist algebras is restriction of functions from the cone to the punctured cone, as morphisms of sheaves of commutative 𝒪_P-algebras. This is the square that makes the morphism of relative spectra induced by the inclusion the open immersion of the punctured cone, and hence the left square of the diagram of [Stacks, Tag 0EKG] commute.

theorem nonnegToIntegerTwistAlgebraSheafHom_comp_puncturedConeAlgebraSheafIso :
    nonnegToIntegerTwistAlgebraSheafHom 𝒜 ≫ (puncturedConeAlgebraSheafIso 𝒜).hom =
      (coneAlgebraSheafIso 𝒜).hom ≫ coneToPuncturedConeAlgebra (truncationConeData 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.heq_nonnegTwistMul_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraSheaf.lean, line 107. The attribute's comment: “the multiplication of the nonnegative twist algebra is commutative on homogeneous local sections”.

The multiplication of the algebra of nonnegative twists is commutative on homogeneous local sections. In a negative degree both products vanish; in nonnegative degrees both are the pointwise product of the values in the module fibres.

theorem heq_nonnegTwistMul_comm (i j : ℤ) (U : (Opens (ProjectiveSpectrum.top 𝒜))ᵒᵖ)
    (a : (nonnegTwistingSheaf 𝒜 i).val.obj U) (b : (nonnegTwistingSheaf 𝒜 j).val.obj U) :
    HEq ((nonnegTwistMul 𝒜 i j).app U a b) ((nonnegTwistMul 𝒜 j i).app U b a)

Stacks.AlgebraicGeometry.ProjConeTwist.nonnegTwistAlgebraSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraSheaf.lean, line 132. The attribute's comment: “the nonnegative twist algebra as a sheaf of commutative algebras over the structure sheaf of P”.

The algebra of nonnegative twists ⨁_{m ≥ 0} 𝒪_P(m) as a sheaf of commutative 𝒪_P-algebras, which is the shape the relative spectrum of [Stacks, Tag 01LM] takes as input. Its sheaf of rings is the ungraded realization of [Stacks, Tag 01CF] and its structure morphism is r ↦ r · 1.

def nonnegTwistAlgebraSheaf : Stacks.RelativeSpec.AlgebraSheaf (AlgebraicGeometry.Proj 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.coneTotalMap_structureMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraSheaf.lean, line 145. The attribute's comment: “the degreewise inclusions carry the structure map of the ungraded realization of the nonnegative twist algebra to the pullback of functions along the cone projection”.

The degreewise inclusions carry the structure map r ↦ r · 1 of the ungraded realization to the pullback of functions along π. This is what makes the identification of π_* 𝒪_L with the twist algebra one of algebras over 𝒪_P, and not merely of sheaves of rings: the inclusions are 𝒪_P-linear and unital, and the action of a section of 𝒪_P on a function on the cone is multiplication by its pullback.

theorem coneTotalMap_structureMap (U : Opens (ProjectiveSpectrum.top 𝒜))
    (r : (AlgebraicGeometry.Proj 𝒜).ringCatSheaf.obj.obj (op U)) :
    coneTotalMap 𝒜 U ((nonnegTwistPresheafAlgebra 𝒜).structureMap (op U) r) =
      ((pi 𝒜).c.app (op U)).hom r

Stacks.AlgebraicGeometry.ProjConeTwist.coneAlgebraSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraSheaf.lean, line 174. The attribute's comment: “the identification pi_* O_L = the nonnegative twist algebra, as sheaves of commutative algebras over the structure sheaf of P, for the cone of the truncation algebra”.

π_* 𝒪_L is the algebra of nonnegative twists, as sheaves of commutative 𝒪_P-algebras.

def coneAlgebraSheafIso :
    nonnegTwistAlgebraSheaf 𝒜 ≅ pushforwardAlgebra (pi 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.isQuasicoherent_nonnegTwistAlgebraSheaf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraSheaf.lean, line 191. The attribute's comment: “the nonnegative twist algebra is a quasi-coherent sheaf of algebras over the structure sheaf of P”.

The algebra of nonnegative twists is a quasi-coherent sheaf of 𝒪_P-algebras: it is the direct image of the structure sheaf of the cone along the affine morphism π.

instance isQuasicoherent_nonnegTwistAlgebraSheaf :
    Stacks.RelativeSpec.AlgebraSheaf.IsQuasicoherent (nonnegTwistAlgebraSheaf 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.coneRelativeSpecTwistAlgebraIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistAlgebraSheaf.lean, line 202. The attribute's comment: “L is, over P, the relative spectrum of the nonnegative twist algebra, for the cone of the truncation algebra”. References: EGA II (8.7.3), “partial”.

L = Spec_P(⨁_{m ≥ 0} 𝒪_P(m)): the cone is, over P = Proj A, the relative spectrum of the algebra of nonnegative twists. This is the presentation on the right of the diagram of [Stacks, Tag 0EKG], with the algebra named as the twist algebra rather than as the direct image π_* 𝒪_L it was computed from.

def coneRelativeSpecTwistAlgebraIso :
    Over.mk (pi 𝒜) ≅ Over.mk (relativeSpecToBase (nonnegTwistAlgebraSheaf 𝒜))

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistNatDirectSumHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistConeCoproduct.lean, line 82. The attribute's comment: “the family of degreewise inclusions O_P(m) -> pi_* O_L as one morphism out of the objectwise direct sum over the natural numbers, for the truncation cone”.

The degreewise inclusions 𝒪_P(m) ⟶ π_* 𝒪_L as a single morphism out of the objectwise direct sum over the natural numbers.

def coneTwistNatDirectSumHom :
    Stacks.directSum (fun n : ℕ => (twistingSheaf 𝒜 (n : ℤ)).val) ⟶
      (Stacks.Morphisms.pushforwardStructureSheaf (pi 𝒜)).val

Stacks.AlgebraicGeometry.ProjConeTwist.bijective_coneTwistNatDirectSumHom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistConeCoproduct.lean, line 117. The attribute's comment: “the morphism out of the objectwise direct sum over the natural numbers of the twisting sheaves is bijective on the sections over a standard open of a positive-degree homogeneous element, for the cone of the truncation algebra”.

Over a standard open of a positive-degree homogeneous element the comparison out of the direct sum over the natural numbers is bijective.

theorem bijective_coneTwistNatDirectSumHom_app (p : PositiveElem 𝒜) :
    Function.Bijective
      ((coneTwistNatDirectSumHom 𝒜).app (op (positiveBasicOpen 𝒜 p))).hom

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistDirectSumHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistConeCoproduct.lean, line 141. The attribute's comment: “the inclusions of the homogeneous pieces of the nonnegative twist algebra as one morphism out of the objectwise direct sum over all integers, for the truncation cone”.

The homogeneous pieces of the algebra of nonnegative twists, included in π_* 𝒪_L out of the objectwise direct sum over all integers.

def coneTwistDirectSumHom :
    Stacks.directSum (fun m : ℤ => (nonnegTwistingSheaf 𝒜 m).val) ⟶
      (Stacks.Morphisms.pushforwardStructureSheaf (pi 𝒜)).val

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistDirectSumHom_app_directSumNatToIntApp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistConeCoproduct.lean, line 163. The attribute's comment: “the inclusion of the nonnegative part of the objectwise direct sum carries the integer-indexed comparison to the one indexed by the natural numbers, on the sections over a standard open of a positive-degree homogeneous element”.

The reindexing ℕ → ℤ identifies the two comparisons on the sections over a standard open of the basis.

theorem coneTwistDirectSumHom_app_directSumNatToIntApp (p : PositiveElem 𝒜)
    (z : Stacks.DirectSumType (fun k : ℕ => (nonnegTwistingSheaf 𝒜 (k : ℤ)).val)
      (op (positiveBasicOpen 𝒜 p))) :
    (coneTwistDirectSumHom 𝒜).app (op (positiveBasicOpen 𝒜 p))
        (Stacks.directSumNatToIntApp (fun m : ℤ => (nonnegTwistingSheaf 𝒜 m).val)
          (op (positiveBasicOpen 𝒜 p)) z) =
      (coneTwistNatDirectSumHom 𝒜).app (op (positiveBasicOpen 𝒜 p)) z

Stacks.AlgebraicGeometry.ProjConeTwist.bijective_coneTwistDirectSumHom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistConeCoproduct.lean, line 190. The attribute's comment: “the morphism out of the objectwise direct sum over all integers of the homogeneous pieces of the nonnegative twist algebra is bijective on the sections over a standard open of a positive-degree homogeneous element, for the cone of the truncation algebra”.

Over a standard open of a positive-degree homogeneous element the comparison out of the direct sum over all integers is bijective.

theorem bijective_coneTwistDirectSumHom_app (p : PositiveElem 𝒜) :
    Function.Bijective
      ((coneTwistDirectSumHom 𝒜).app (op (positiveBasicOpen 𝒜 p))).hom

Stacks.AlgebraicGeometry.ProjConeTwist.coneStructureSheafifyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistConeCoproduct.lean, line 207. The attribute's comment: “the direct image of the structure sheaf of the cone is the sheafification of the objectwise direct sum of the homogeneous pieces of the nonnegative twist algebra, for the truncation cone”.

π_* 𝒪_L is the sheafification of the objectwise direct sum of the homogeneous pieces of the algebra of nonnegative twists.

def coneStructureSheafifyIso :
    (PresheafOfModules.sheafification (𝟙 _)).obj
        (Stacks.directSum fun m : ℤ => (nonnegTwistingSheaf 𝒜 m).val) ≅
      Stacks.Morphisms.pushforwardStructureSheaf (pi 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.coneStructureCoproductIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistConeCoproduct.lean, line 224. The attribute's comment: “the identification pi_* O_L = the coproduct of the homogeneous pieces of the nonnegative twist algebra, as sheaves of O_P-modules, for the cone of the truncation algebra”.

π_* 𝒪_L ≅ ∐_{m ∈ ℤ} (nonnegTwistAlgebra 𝒜).piece m: the identification of the direct image of the structure sheaf of the cone with the coproduct of the homogeneous pieces of the algebra of nonnegative twists.

def coneStructureCoproductIso :
    Stacks.Morphisms.pushforwardStructureSheaf (pi 𝒜) ≅
      ∐ fun m : ℤ => nonnegTwistingSheaf 𝒜 m

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistAwayHom_degreeZeroRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistGlobalMap.lean, line 140. The attribute's comment: “the degreewise inclusion of the sections of O_P(m) into the degree-zero localization of the truncation algebra commutes with restriction between two standard opens”.

The degreewise inclusion commutes with restriction between two standard opens, read in the degree-zero localizations of the truncation algebra.

theorem coneTwistAwayHom_degreeZeroRingMap (m : ℕ) {d e : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (hg : g ∈ 𝒜 e) (he : 0 < e)
    (hfg : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f)
    (s : (ProjectiveSpectrum.Proj.twistingSheaf 𝒜 (m : ℤ)).val.obj
      (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    coneTwistAwayHom 𝒜 m e hg he
        (((ProjectiveSpectrum.Proj.twistingSheaf 𝒜 (m : ℤ)).val.map (homOfLE hfg).op).hom s) =
      ProjectiveSpectrum.degreeZeroRingMap (grading 𝒜) (psi 𝒜 f) (psi 𝒜 g)
        (exists_psi_mem 𝒜 hf hd) (exists_psi_mem 𝒜 hg he)
        (basicOpen_psi_le 𝒜 hf hd hg he hfg) (coneTwistAwayHom 𝒜 m d hf hd s)

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistApp_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistGlobalMap.lean, line 194. The attribute's comment: “the degreewise inclusion O_P(m) to pi_* O_L over standard opens is compatible with restriction between two standard opens”.

The local degreewise inclusion commutes with restriction to a smaller standard open.

theorem coneTwistApp_restrict (m : ℕ) {d e : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d) (hg : g ∈ 𝒜 e)
    (he : 0 < e)
    (hfg : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f)
    (s : (ProjectiveSpectrum.Proj.twistingSheaf 𝒜 (m : ℤ)).val.obj
      (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (coneTwistApp 𝒜 m e hg he).hom
        (((ProjectiveSpectrum.Proj.twistingSheaf 𝒜 (m : ℤ)).val.map (homOfLE hfg).op).hom s) =
      ((Stacks.Morphisms.pushforwardStructureSheaf (pi 𝒜)).val.map (homOfLE hfg).op).hom
        ((coneTwistApp 𝒜 m d hf hd).hom s)

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistApp_degree_indep, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistGlobalMap.lean, line 244. The attribute's comment: “the degreewise inclusion O_P(m) to pi_* O_L over one standard open depends only on that open, not on the degree of the element cutting it out”.

The local degreewise inclusion depends only on the standard open, not on the degree in which the element cutting it out is homogeneous.

theorem coneTwistApp_degree_indep (m : ℕ) {d d' : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (hf' : f ∈ 𝒜 d') (hd' : 0 < d') :
    coneTwistApp 𝒜 m d hf hd = coneTwistApp 𝒜 m d' hf' hd'

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistGlobalMap.lean, line 286. The attribute's comment: “the degreewise inclusion O_P(m) to pi_* O_L as a morphism of sheaves of O_P-modules, for the truncation cone and a nonnegative degree m”.

The degreewise inclusion 𝒪_P(m) ⟶ π_* 𝒪_L, for m ≥ 0: the morphism of sheaves of 𝒪_P-modules glued from the local maps over the standard opens of positive-degree homogeneous elements.

def coneTwistHom (m : ℕ) :
    ProjectiveSpectrum.Proj.twistingSheaf 𝒜 (m : ℤ) ⟶
      Stacks.Morphisms.pushforwardStructureSheaf (pi 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistHom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistGlobalMap.lean, line 294. The attribute's comment: “the global degreewise inclusion restricts on each standard open to the local one”.

The glued morphism restricts on a standard open to the local degreewise inclusion.

theorem coneTwistHom_app (m : ℕ) {d : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (coneTwistHom 𝒜 m).val.app (op (ProjectiveSpectrum.basicOpen 𝒜 f)) =
      coneTwistApp 𝒜 m d hf hd

Stacks.AlgebraicGeometry.ProjConeTwist.coneIota, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistGlobalMap.lean, line 307. The attribute's comment: “the inclusion of each homogeneous piece of the nonnegative twist algebra in pi_* O_L, for the truncation cone”.

The inclusion of each homogeneous piece of ⨁_{m ≥ 0} 𝒪_P(m) in π_* 𝒪_L: the glued degreewise inclusion in a nonnegative degree, and the morphism out of the zero sheaf in a negative one.

def coneIota : ∀ n : ℤ, nonnegTwistingSheaf 𝒜 n ⟶
    Stacks.Morphisms.pushforwardStructureSheaf (pi 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistHom_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistGlobalMul.lean, line 97. The attribute's comment: “the glued degreewise inclusion O_P(m) to pi_* O_L is multiplicative over a standard open of a positive-degree homogeneous element”.

The glued degreewise inclusion is multiplicative over a standard open of a positive-degree homogeneous element.

theorem coneTwistHom_mul {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d) (i j : ℕ)
    (x : (twistingSheaf 𝒜 (i : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)))
    (y : (twistingSheaf 𝒜 (j : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (show coneSections 𝒜 (ProjectiveSpectrum.basicOpen 𝒜 f) from
        (coneTwistHom 𝒜 (i + j)).val.app (op (ProjectiveSpectrum.basicOpen 𝒜 f))
          (natTwistMulSection 𝒜 i j (op (ProjectiveSpectrum.basicOpen 𝒜 f)) x y)) =
      (show coneSections 𝒜 (ProjectiveSpectrum.basicOpen 𝒜 f) from
          (coneTwistHom 𝒜 i).val.app (op (ProjectiveSpectrum.basicOpen 𝒜 f)) x) *
        (show coneSections 𝒜 (ProjectiveSpectrum.basicOpen 𝒜 f) from
          (coneTwistHom 𝒜 j).val.app (op (ProjectiveSpectrum.basicOpen 𝒜 f)) y)

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistHom_mul_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistGlobalMul.lean, line 119. The attribute's comment: “the glued degreewise inclusion O_P(m) to pi_* O_L is multiplicative over every open of P, in nonnegative degrees”.

The glued degreewise inclusion 𝒪_P(i) ⟶ π_* 𝒪_L is multiplicative over every open of P. The standard opens of positive-degree homogeneous elements are a basis, and both sides restrict to them as the standard-open statement says.

theorem coneTwistHom_mul_app (i j : ℕ) (U : Opens (ProjectiveSpectrum.top 𝒜))
    (a : (twistingSheaf 𝒜 (i : ℤ)).val.obj (op U))
    (b : (twistingSheaf 𝒜 (j : ℤ)).val.obj (op U)) :
    (show coneSections 𝒜 U from
        (coneTwistHom 𝒜 (i + j)).val.app (op U) (natTwistMulSection 𝒜 i j (op U) a b)) =
      (show coneSections 𝒜 U from (coneTwistHom 𝒜 i).val.app (op U) a) *
        (show coneSections 𝒜 U from (coneTwistHom 𝒜 j).val.app (op U) b)

Stacks.AlgebraicGeometry.ProjConeTwist.coneIota_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistGlobalMul.lean, line 160. The attribute's comment: “the inclusions of the homogeneous pieces of the nonnegative twist algebra in pi_* O_L are multiplicative, over every open of P and in every integer degree, for the truncation cone”.

The inclusions of the homogeneous pieces of the algebra of nonnegative twists in π_* 𝒪_L multiply as the grading prescribes, over every open of P and in all integer degrees. This is the ι_mul condition of AlgebraicGeometry.AbstractCone for the cone of the truncation algebra, graded by Stacks.AlgebraicGeometry.ProjConeTwist.nonnegTwistAlgebra. In a negative degree the piece is the zero sheaf, so both sides vanish.

theorem coneIota_mul (i j : ℤ) (U : Opens (ProjectiveSpectrum.top 𝒜))
    (a : (nonnegTwistingSheaf 𝒜 i).val.obj (op U))
    (b : (nonnegTwistingSheaf 𝒜 j).val.obj (op U)) :
    (show coneSections 𝒜 U from
        (coneIota 𝒜 (i + j)).val.app (op U) ((nonnegTwistMul 𝒜 i j).app (op U) a b)) =
      (show coneSections 𝒜 U from (coneIota 𝒜 i).val.app (op U) a) *
        (show coneSections 𝒜 U from (coneIota 𝒜 j).val.app (op U) b)

Stacks.Truncation.awayToLocalization_map_psi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistLocalMap.lean, line 67. The attribute's comment: “the comparison map (B[1/psi f])_0 to A[1/f] undoes the map of degree-zero localizations attached to psi”.

The comparison map (B[1/ψ f])₀ → A[1/f] undoes HomogeneousLocalization.Away.map ψ f: the fraction ψ a / (ψ f)ᵏ of the truncation algebra is sent to the fraction a / fᵏ.

theorem awayToLocalization_map_psi (d : ℕ) (hf : f ∈ 𝒜 d)
    (r : HomogeneousLocalization.Away 𝒜 f) :
    awayToLocalization 𝒜 (HomogeneousLocalization.Away.map (psi 𝒜) f r) = r.val

Stacks.Truncation.awayGradingEquivSectionsTwist_symm_degree_indep, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistLocalMap.lean, line 106. The attribute's comment: “the degreewise inclusion of the sections of O_P(m) over D+(f) into the functions on the cone depends only on the standard open, not on the degree of f”.

The degreewise inclusion depends only on the standard open, not on the degree in which f is homogeneous.

theorem awayGradingEquivSectionsTwist_symm_degree_indep {d d' : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (hf' : f ∈ 𝒜 d') (hd' : 0 < d') (m : ℕ)
    (s : (twistingSheaf 𝒜 (m : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (((awayGradingEquivSectionsTwist 𝒜 d hf hd m).symm s :
        HomogeneousLocalization.Away (grading 𝒜) (psi 𝒜 f))) =
      (((awayGradingEquivSectionsTwist 𝒜 d' hf' hd' m).symm s :
        HomogeneousLocalization.Away (grading 𝒜) (psi 𝒜 f)))

Stacks.Truncation.awayGradingEquivSectionsTwist_symm_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistLocalMap.lean, line 126. The attribute's comment: “the degreewise inclusion is semilinear for the map of degree-zero localizations attached to psi, over one standard open D+(f)”.

The degreewise inclusion Γ(D₊(f), 𝒪_P(m)) → (B[1/ψ f])₀ is semilinear for the map HomogeneousLocalization.Away.map ψ f of degree-zero localizations: scaling a section of 𝒪_P(m) by the degree-zero fraction r multiplies its image by the image of r.

theorem awayGradingEquivSectionsTwist_symm_smul (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) (m : ℕ)
    (r : HomogeneousLocalization.Away 𝒜 f)
    (s : (twistingSheaf 𝒜 (m : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (((awayGradingEquivSectionsTwist 𝒜 d hf hd m).symm
          ((ProjectiveSpectrum.Proj.awayToSection 𝒜 f).hom r • s) :
        HomogeneousLocalization.Away (grading 𝒜) (psi 𝒜 f))) =
      HomogeneousLocalization.Away.map (psi 𝒜) f r *
        (((awayGradingEquivSectionsTwist 𝒜 d hf hd m).symm s :
          HomogeneousLocalization.Away (grading 𝒜) (psi 𝒜 f)))

Stacks.AlgebraicGeometry.ProjConeTwist.awayToSection_pi_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistLocalMap.lean, line 205. The attribute's comment: “the cone projection on functions over a standard open, with the sections over D+(psi f) transported along the identity of opens pi^{-1}(D+(f)) = D+(psi f)”.

The cone projection on functions over a standard open: the image of a degree-zero fraction of A under ψ, read as a function on D₊(ψ f) and transported along π⁻¹(D₊(f)) = D₊(ψ f), is the pullback of that fraction along π.

theorem awayToSection_pi_app (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (r : HomogeneousLocalization.Away 𝒜 f) :
    (AlgebraicGeometry.Proj (grading 𝒜)).presheaf.map
        (eqToHom (pi_preimage_basicOpen 𝒜 f d hf hd)).op
        ((AlgebraicGeometry.Proj.awayToSection (grading 𝒜) (psi 𝒜 f)).hom
          (HomogeneousLocalization.Away.map (psi 𝒜) f r)) =
      ((pi 𝒜).app (AlgebraicGeometry.Proj.basicOpen 𝒜 f)).hom
        ((AlgebraicGeometry.Proj.awayToSection 𝒜 f).hom r)

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistAwayHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistLocalMap.lean, line 231. The attribute's comment: “the degreewise inclusion of the sections of O_P(m) over D+(f) into the degree-zero localization of the truncation algebra, as an additive map”.

The degreewise inclusion Γ(D₊(f), 𝒪_P(m)) → (B[1/ψ f])₀, as an additive map: the inverse of Stacks.Truncation.awayGradingEquivSectionsTwist followed by the inclusion of the degree-m summand.

def coneTwistAwayHom (m d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    ((twistingSheaf 𝒜 (m : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) →+
      HomogeneousLocalization.Away (grading 𝒜) (psi 𝒜 f)

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistApp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistLocalMap.lean, line 250. The attribute's comment: “the degreewise inclusion O_P(m) to pi_* O_L over one standard open D+(f), as a map of modules over the sections of O_P there”.

The local degreewise inclusion Γ(D₊(f), 𝒪_P(m)) ⟶ Γ(D₊(f), π_* 𝒪_L), as a morphism of modules over the sections of 𝒪_P on D₊(f).

def coneTwistApp (m d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (twistingSheaf 𝒜 (m : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)) ⟶
      (Stacks.Morphisms.pushforwardStructureSheaf (pi 𝒜)).val.obj
        (op (AlgebraicGeometry.Proj.basicOpen 𝒜 f))

Stacks.Truncation.awayToLocalization_degreeZeroRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistLocalRestriction.lean, line 99. The attribute's comment: “the comparison maps (B[1/psi f])_0 to A[1/f] commute with the restriction maps of degree-zero localizations, for a general inclusion D+(g) <= D+(f) of standard opens”.

The comparison maps (B[1/ψ f])₀ → A[1/f] commute with the restriction maps of degree-zero localizations: the one of B attached to D₊(ψ g) ⊆ D₊(ψ f) on the source, the one of A attached to D₊(g) ⊆ D₊(f) on the target.

theorem awayToLocalization_degreeZeroRingMap
    (hf : ∃ d : ℕ, 0 < d ∧ f ∈ 𝒜 d) (hg : ∃ e : ℕ, 0 < e ∧ g ∈ 𝒜 e)
    (hψf : ∃ d : ℕ, 0 < d ∧ psi 𝒜 f ∈ grading 𝒜 d)
    (hψg : ∃ e : ℕ, 0 < e ∧ psi 𝒜 g ∈ grading 𝒜 e)
    (hfg : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f)
    (hψfg : ProjectiveSpectrum.basicOpen (grading 𝒜) (psi 𝒜 g) ≤
      ProjectiveSpectrum.basicOpen (grading 𝒜) (psi 𝒜 f))
    (z : HomogeneousLocalization.Away (grading 𝒜) (psi 𝒜 f)) :
    awayToLocalization 𝒜
        (ProjectiveSpectrum.degreeZeroRingMap (grading 𝒜) (psi 𝒜 f) (psi 𝒜 g)
          hψf hψg hψfg z) =
      ProjectiveSpectrum.localizedRingMap 𝒜 f g hf hg hfg (awayToLocalization 𝒜 z)

Stacks.AlgebraicGeometry.ProjConeTwist.integerTwistAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 248. The attribute's comment: “the graded algebra of all integral twists”.

The graded algebra ⨁_{m ∈ ℤ} 𝒪_P(m) of all integral twists on P = Proj A.

def integerTwistAlgebra :
    SheafOfModules.GradedAlgebra (AlgebraicGeometry.Proj 𝒜).ringCatSheaf

Stacks.AlgebraicGeometry.ProjConeTwist.isZero_nonnegTwistingSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 286. The attribute's comment: “the homogeneous pieces in negative degrees”.

In negative degrees the pieces of the algebra of nonnegative twists vanish.

theorem isZero_nonnegTwistingSheaf {n : ℤ} (hn : n < 0) :
    IsZero (nonnegTwistingSheaf 𝒜 n)

Stacks.AlgebraicGeometry.ProjConeTwist.nonnegTwistAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 337. The attribute's comment: “the graded algebra of nonnegative twists”.

The graded algebra ⨁_{m ≥ 0} 𝒪_P(m) of nonnegative twists on P = Proj A.

def nonnegTwistAlgebra :
    SheafOfModules.GradedAlgebra (AlgebraicGeometry.Proj 𝒜).ringCatSheaf

Stacks.AlgebraicGeometry.ProjConeTwist.nonnegPieceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 409. The attribute's comment: “the homogeneous pieces in nonnegative degrees”.

In nonnegative degrees the piece of the algebra of nonnegative twists is the twisting sheaf.

def nonnegPieceIso {n : ℤ} (hn : 0 ≤ n) :
    (nonnegTwistAlgebra 𝒜).piece n ≅ twistingSheaf 𝒜 n

Stacks.AlgebraicGeometry.ProjConeTwist.nonnegToIntegerTwistAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 474. The attribute's comment: “the inclusion of the nonnegative twist algebra in the integral one”.

The inclusion ⨁_{m ≥ 0} 𝒪_P(m) ⟶ ⨁_{m ∈ ℤ} 𝒪_P(m) of graded algebras.

def nonnegToIntegerTwistAlgebra :
    SheafOfModules.GradedAlgebra.Hom (nonnegTwistAlgebra 𝒜) (integerTwistAlgebra 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.nonnegToIntegerTwistAlgebra_app_natCast, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 481. The attribute's comment: “the inclusion is the identity on each nonnegative twist”.

In nonnegative degrees the inclusion of the two twist algebras is the identity.

theorem nonnegToIntegerTwistAlgebra_app_natCast (m : ℕ) :
    (nonnegToIntegerTwistAlgebra 𝒜).app (m : ℤ) = CategoryStruct.id _

Stacks.AlgebraicGeometry.ProjConeTwist.coneAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 509. The attribute's comment: “the direct-image algebra of the cone”.

The direct-image algebra π_* 𝒪_L of the cone.

def coneAlgebra : Stacks.RelativeSpec.AlgebraSheaf (AlgebraicGeometry.Proj 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 515. The attribute's comment: “the direct-image algebra of the punctured cone”.

The direct-image algebra (π|_U)_* 𝒪_U of the punctured cone, the part of L lying over U = X ∖ V(A₊).

def puncturedConeAlgebra : Stacks.RelativeSpec.AlgebraSheaf (AlgebraicGeometry.Proj 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.coneToPuncturedConeAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 522. The attribute's comment: “the inclusion of the two direct-image algebras”.

Restriction of functions from the cone to the punctured cone, as a morphism of 𝒪_P-algebras.

def coneToPuncturedConeAlgebra : coneAlgebra c ⟶ puncturedConeAlgebra c

Stacks.AlgebraicGeometry.ProjConeTwist.coneToPuncturedConeAlgebra_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 529. The attribute's comment: “the restriction formula for the inclusion of the two algebras”.

Over an open of P the restriction map of the two direct-image algebras is the canonical map on functions induced by the open immersion of the punctured cone.

theorem coneToPuncturedConeAlgebra_app (U : (AlgebraicGeometry.Proj 𝒜).Opens)
    (hle : ((ProjAndSpec.openUInL c).ι ≫ ProjAndSpec.pi c) ⁻¹ᵁ U ≤
      (ProjAndSpec.openUInL c).ι ⁻¹ᵁ (ProjAndSpec.pi c ⁻¹ᵁ U)) :
    (coneToPuncturedConeAlgebra c).right.hom.app (op U) =
      (ProjAndSpec.openUInL c).ι.appLE (ProjAndSpec.pi c ⁻¹ᵁ U)
        (((ProjAndSpec.openUInL c).ι ≫ ProjAndSpec.pi c) ⁻¹ᵁ U) hle

Stacks.AlgebraicGeometry.ProjConeTwist.structureSheafToTwistZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 572. The attribute's comment: “the comparison of the degree-zero piece with the structure sheaf”.

A section of the structure sheaf, read in the localizations of A, as a section of the untwisted sheaf.

def structureSheafToTwistZero (U : Opens (ProjectiveSpectrum.top 𝒜))
    (r : (ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (op U)) :
    (twistingSheaf 𝒜 0).val.obj (op U)

Stacks.AlgebraicGeometry.ProjConeTwist.structureSheafToTwistZero_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 586. The attribute's comment: “the degree-zero comparison preserves the unit”.

The comparison carries the unit section of the structure sheaf to the unit section of the untwisted sheaf.

theorem structureSheafToTwistZero_one (U : Opens (ProjectiveSpectrum.top 𝒜)) :
    structureSheafToTwistZero 𝒜 U 1 = (twistOne 𝒜).eval (op U)

Stacks.AlgebraicGeometry.ProjConeTwist.structureSheafToTwistZero_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 593. The attribute's comment: “the degree-zero comparison is multiplicative”.

The comparison is multiplicative, the product on the right being the degree-zero part of the multiplication of twists.

theorem structureSheafToTwistZero_mul (U : Opens (ProjectiveSpectrum.top 𝒜))
    (r r' : (ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (op U)) :
    structureSheafToTwistZero 𝒜 U (r * r') =
      twistMulSection 𝒜 0 0 (op U) (structureSheafToTwistZero 𝒜 U r)
        (structureSheafToTwistZero 𝒜 U r')

Stacks.AlgebraicGeometry.ProjConeTwist.structureSheafToTwistZero_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 609. The attribute's comment: “injectivity of the degree-zero comparison”.

The comparison of the structure sheaf with 𝒪_P(0) is injective over every open.

theorem structureSheafToTwistZero_injective (U : Opens (ProjectiveSpectrum.top 𝒜)) :
    Function.Injective (structureSheafToTwistZero 𝒜 U)

Stacks.AlgebraicGeometry.ProjConeTwist.structureSheafToTwistZero_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 617. The attribute's comment: “surjectivity of the degree-zero comparison”.

The comparison of the structure sheaf with 𝒪_P(0) is surjective over every open.

theorem structureSheafToTwistZero_surjective (U : Opens (ProjectiveSpectrum.top 𝒜)) :
    Function.Surjective (structureSheafToTwistZero 𝒜 U)

Stacks.AlgebraicGeometry.ProjConeTwist.structureSheafToTwistZero_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPresentation.lean, line 642. The attribute's comment: “the degree-zero piece is the structure sheaf”.

The degree-zero piece of the twist algebra is the structure sheaf: over every open the comparison is a bijection.

theorem structureSheafToTwistZero_bijective (U : Opens (ProjectiveSpectrum.top 𝒜)) :
    Function.Bijective (structureSheafToTwistZero 𝒜 U)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedTotalPresheafHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedAlgebraSheaf.lean, line 97. The attribute's comment: “the degreewise inclusions as a morphism of presheaves of rings from the ungraded realization of the integral twist algebra to (pi|_U)_* O_U, for the truncation cone”.

The degreewise inclusions as a morphism of presheaves of rings from the ungraded realization of the algebra of all integral twists into (π|_U)_* 𝒪_U.

def puncturedTotalPresheafHom :
    (integerTwistPresheafAlgebra 𝒜).totalPresheaf ⟶ (puncturedConePushforwardRingSheaf 𝒜).obj

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeUngradedSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedAlgebraSheaf.lean, line 131. The attribute's comment: “the identification (pi|_U)_* O_U = the ungraded realization of the integral twist algebra, as sheaves of rings, for the punctured cone of the truncation algebra”.

(π|_U)_* 𝒪_U is the ungraded realization of the algebra of all integral twists, as sheaves of rings.

def puncturedConeUngradedSheafIso :
    (integerTwistAlgebra 𝒜).ungradedSheaf ≅ puncturedConePushforwardRingSheaf 𝒜

Stacks.AlgebraicGeometry.ProjConeTwist.heq_twistMul_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedAlgebraSheaf.lean, line 151. The attribute's comment: “the multiplication of the integral twist algebra is commutative on homogeneous local sections”.

The multiplication of the algebra of all integral twists is commutative on homogeneous local sections: it is the pointwise product of the values in the module fibres.

theorem heq_twistMul_comm (i j : ℤ) (V : (Opens (ProjectiveSpectrum.top 𝒜))ᵒᵖ)
    (a : (twistingSheaf 𝒜 i).val.obj V) (b : (twistingSheaf 𝒜 j).val.obj V) :
    HEq ((twistMul 𝒜 i j).app V a b) ((twistMul 𝒜 j i).app V b a)

Stacks.AlgebraicGeometry.ProjConeTwist.integerTwistAlgebraSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedAlgebraSheaf.lean, line 164. The attribute's comment: “the integral twist algebra as a sheaf of commutative algebras over the structure sheaf of P”.

The algebra of all integral twists ⨁_{m ∈ ℤ} 𝒪_P(m) as a sheaf of commutative 𝒪_P-algebras.

def integerTwistAlgebraSheaf : Stacks.RelativeSpec.AlgebraSheaf (AlgebraicGeometry.Proj 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedTotalMap_structureMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedAlgebraSheaf.lean, line 174. The attribute's comment: “the degreewise inclusions carry the structure map of the ungraded realization of the integral twist algebra to the pullback of functions along the punctured cone projection”.

The degreewise inclusions carry the structure map r ↦ r · 1 of the ungraded realization to the pullback of functions along π|_U.

theorem puncturedTotalMap_structureMap (V : Opens (ProjectiveSpectrum.top 𝒜))
    (r : ((ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj ⋙
      forget₂ CommRingCat.{u} RingCat.{u}).obj (op V)) :
    puncturedTotalMap 𝒜 V ((integerTwistPresheafAlgebra 𝒜).structureMap (op V) r) =
      (((openUInL 𝒜).ι ≫ pi 𝒜).c.app (op V)).hom r

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeAlgebraSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedAlgebraSheaf.lean, line 205. The attribute's comment: “the identification (pi|_U)_* O_U = the integral twist algebra, as sheaves of commutative algebras over the structure sheaf of P, for the punctured cone of the truncation algebra”.

(π|_U)_* 𝒪_U is the algebra of all integral twists, as sheaves of commutative 𝒪_P-algebras.

def puncturedConeAlgebraSheafIso :
    integerTwistAlgebraSheaf 𝒜 ≅ pushforwardAlgebra ((openUInL 𝒜).ι ≫ pi 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.isQuasicoherent_integerTwistAlgebraSheaf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedAlgebraSheaf.lean, line 222. The attribute's comment: “the integral twist algebra is a quasi-coherent sheaf of algebras over the structure sheaf of P”.

The algebra of all integral twists is a quasi-coherent sheaf of 𝒪_P-algebras: it is the direct image of the structure sheaf of the punctured cone along the affine morphism π|_U.

instance isQuasicoherent_integerTwistAlgebraSheaf :
    Stacks.RelativeSpec.AlgebraSheaf.IsQuasicoherent (integerTwistAlgebraSheaf 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeRelativeSpecTwistAlgebraIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedAlgebraSheaf.lean, line 231. The attribute's comment: “U is, over P, the relative spectrum of the integral twist algebra, for the punctured cone of the truncation algebra”.

U = Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)): the punctured cone is, over P = Proj A, the relative spectrum of the algebra of all integral twists.

def puncturedConeRelativeSpecTwistAlgebraIso :
    Over.mk ((openUInL 𝒜).ι ≫ pi 𝒜) ≅
      Over.mk (relativeSpecToBase (integerTwistAlgebraSheaf 𝒜))

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedTwistDirectSumHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedCoproduct.lean, line 95. The attribute's comment: “the family of degreewise inclusions O_P(m) -> (pi|_U)_* O_U as one morphism out of the objectwise direct sum over all integers m, for the truncation cone”.

The family of punctured degreewise inclusions as a single morphism out of the objectwise direct sum ⨁_{m ∈ ℤ} 𝒪_P(m) ⟶ (π|_U)_* 𝒪_U.

def puncturedTwistDirectSumHom :
    Stacks.directSum (fun m : ℤ => (twistingSheaf 𝒜 m).val) ⟶
      (Stacks.Morphisms.pushforwardStructureSheaf ((openUInL 𝒜).ι ≫ pi 𝒜)).val

Stacks.AlgebraicGeometry.ProjConeTwist.bijective_puncturedTwistDirectSumHom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedCoproduct.lean, line 123. The attribute's comment: “the morphism out of the objectwise direct sum of the twisting sheaves is bijective on the sections over a standard open of a positive-degree homogeneous element, for the punctured cone of the truncation algebra”.

Over a standard open of a positive-degree homogeneous element the morphism out of the objectwise direct sum is bijective. It agrees there with the additive equivalence Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeAlgebraSectionsEquivTwistSections, read backwards.

theorem bijective_puncturedTwistDirectSumHom_app (p : PositiveElem 𝒜) :
    Function.Bijective
      ((puncturedTwistDirectSumHom 𝒜).app (op (positiveBasicOpen 𝒜 p))).hom

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeStructureSheafifyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedCoproduct.lean, line 151. The attribute's comment: “the direct image of the structure sheaf of the punctured cone is the sheafification of the objectwise direct sum of all the twisting sheaves, for the truncation cone”.

(π|_U)_* 𝒪_U is the sheafification of the objectwise direct sum ⨁_{m ∈ ℤ} 𝒪_P(m). The comparison morphism is bijective on the sections over every standard open of a positive-degree homogeneous element, and those form a basis of P.

def puncturedConeStructureSheafifyIso :
    (PresheafOfModules.sheafification (𝟙 _)).obj
        (Stacks.directSum fun m : ℤ => (twistingSheaf 𝒜 m).val) ≅
      Stacks.Morphisms.pushforwardStructureSheaf ((openUInL 𝒜).ι ≫ pi 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeStructureCoproductIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedCoproduct.lean, line 169. The attribute's comment: “the identification (pi|_U)_* O_U = the coproduct over all integers m of the twisting sheaves O_P(m), as sheaves of O_P-modules, for the punctured cone of the truncation algebra”.

(π|_U)_* 𝒪_U ≅ ∐_{m ∈ ℤ} 𝒪_P(m): the identification of [Stacks, Tag 0EKG] of the direct image of the structure sheaf of the punctured cone with the coproduct, over all integers, of the twisting sheaves of P = Proj A.

def puncturedConeStructureCoproductIso :
    Stacks.Morphisms.pushforwardStructureSheaf ((openUInL 𝒜).ι ≫ pi 𝒜) ≅
      ∐ fun m : ℤ => twistingSheaf 𝒜 m

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeStructurePushforwardCoproductIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedCoproduct.lean, line 182. The attribute's comment: “the identification (pi|_U)_* O_U = the coproduct over all integers m of the twisting sheaves O_P(m), with the source written as the direct image along the punctured cone projection of the truncation cone data”.

(π|_U)_* 𝒪_U ≅ ∐_{m ∈ ℤ} 𝒪_P(m), with the source written as the direct image along Stacks.AlgebraicGeometry.ProjAndSpec.puncturedConeProj of the structure sheaf of the punctured cone. This is the form in which the identification is consumed by the projection formula along π|_U.

def puncturedConeStructurePushforwardCoproductIso :
    (Scheme.Modules.pushforward
          (Stacks.AlgebraicGeometry.ProjAndSpec.puncturedConeProj (truncationConeData 𝒜))).obj
        (SheafOfModules.unit
          (Stacks.AlgebraicGeometry.ProjAndSpec.openUInL
            (truncationConeData 𝒜)).toScheme.ringCatSheaf) ≅
      ∐ fun m : ℤ => twistingSheaf 𝒜 m

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistApp_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedGlobalMap.lean, line 143. The attribute's comment: “the degreewise inclusion O_P(m) to (pi|_U)_* O_U over standard opens is compatible with restriction between two standard opens, for every integer m”.

The local punctured degreewise inclusion commutes with restriction to a smaller standard open. This is the compatibility the gluing principle of [Stacks, Tag 009U] asks for.

theorem puncturedConeTwistApp_restrict (m : ℤ) {d e : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (hg : g ∈ 𝒜 e) (he : 0 < e)
    (hfg : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f)
    (s : (twistingSheaf 𝒜 m).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (puncturedConeTwistApp 𝒜 m e hg he).hom
        (((twistingSheaf 𝒜 m).val.map (homOfLE hfg).op).hom s) =
      ((Stacks.Morphisms.pushforwardStructureSheaf ((openUInL 𝒜).ι ≫ pi 𝒜)).val.map
          (homOfLE hfg).op).hom ((puncturedConeTwistApp 𝒜 m d hf hd).hom s)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistApp_degree_indep, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedGlobalMap.lean, line 184. The attribute's comment: “the degreewise inclusion O_P(m) to (pi|_U)_* O_U over one standard open depends only on that open, not on the degree of the element cutting it out, for every integer m”.

The local punctured degreewise inclusion depends only on the standard open, not on the degree in which the element cutting it out is homogeneous.

theorem puncturedConeTwistApp_degree_indep (m : ℤ) {d d' : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (hf' : f ∈ 𝒜 d') (hd' : 0 < d') :
    puncturedConeTwistApp 𝒜 m d hf hd = puncturedConeTwistApp 𝒜 m d' hf' hd'

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedTwistHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedGlobalMap.lean, line 227. The attribute's comment: “the degreewise inclusion O_P(m) to (pi|_U)_* O_U as a morphism of sheaves of O_P-modules, for the punctured cone of the truncation algebra and every integer m”.

The degreewise inclusion 𝒪_P(m) ⟶ (π|_U)_* 𝒪_U, for every integer m: the morphism of sheaves of 𝒪_P-modules glued from the local maps over the standard opens of positive-degree homogeneous elements. This is the degreewise half of the presentation (π|_U)_* 𝒪_U = ⨁_{m ∈ ℤ} 𝒪_P(m) of [Stacks, Tag 0EKG].

def puncturedTwistHom (m : ℤ) :
    ProjectiveSpectrum.Proj.twistingSheaf 𝒜 m ⟶
      Stacks.Morphisms.pushforwardStructureSheaf ((openUInL 𝒜).ι ≫ pi 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedTwistHom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedGlobalMap.lean, line 238. The attribute's comment: “the global punctured degreewise inclusion restricts on each standard open to the local one, for every integer m”.

The glued punctured morphism restricts on a standard open to the local degreewise inclusion.

theorem puncturedTwistHom_app (m : ℤ) (p : PositiveElem 𝒜) :
    (puncturedTwistHom 𝒜 m).val.app (op (positiveBasicOpen 𝒜 p)) =
      puncturedConeTwistStandardOpenApp 𝒜 m p

Stacks.Truncation.puncturedToLocalization_degreeZeroRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalMap.lean, line 119. The attribute's comment: “the comparison maps (B[1/sigma f * psi f])_0 to A[1/f] and (B[1/psi f])_0 to A[1/f] agree across the degree-zero restriction map of B attached to D+(sigma f * psi f) <= D+(psi f)”.

The comparison maps (B[1/σ f · ψ f])₀ → A[1/f] and (B[1/ψ f])₀ → A[1/f] agree across the restriction map of B attached to D₊(σ f · ψ f) ⊆ D₊(ψ f).

theorem puncturedToLocalization_degreeZeroRingMap
    (hψf : ∃ e : ℕ, 0 < e ∧ psi 𝒜 f ∈ grading 𝒜 e)
    (hσψf : ∃ e : ℕ, 0 < e ∧ sigmaMulPsi 𝒜 f ∈ grading 𝒜 e)
    (hle : ProjectiveSpectrum.basicOpen (grading 𝒜) (sigmaMulPsi 𝒜 f) ≤
      ProjectiveSpectrum.basicOpen (grading 𝒜) (psi 𝒜 f))
    (z : HomogeneousLocalization.Away (grading 𝒜) (psi 𝒜 f)) :
    puncturedToLocalization 𝒜
        (ProjectiveSpectrum.degreeZeroRingMap (grading 𝒜) (psi 𝒜 f) (sigmaMulPsi 𝒜 f)
          hψf hσψf hle z) =
      awayToLocalization 𝒜 z

Stacks.Truncation.puncturedToLocalization_degreeZeroRingMap_map_psi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalMap.lean, line 153. The attribute's comment: “the comparison map (B[1/sigma f * psi f])_0 to A[1/f] undoes the chart description of the punctured cone projection on a standard open”.

The comparison map (B[1/σ f · ψ f])₀ → A[1/f] undoes the chart description of the punctured cone projection, the map A₍f₎ → B₍σ f · ψ f₎ of degree-zero localizations attached to ψ followed by restriction.

theorem puncturedToLocalization_degreeZeroRingMap_map_psi (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (r : HomogeneousLocalization.Away 𝒜 f) :
    puncturedToLocalization 𝒜
        (ProjectiveSpectrum.degreeZeroRingMap (grading 𝒜) (psi 𝒜 f) (sigmaMulPsi 𝒜 f)
          ⟨d, hd, GradedRingHom.map_mem (psi 𝒜) hf⟩ ⟨d, hd, sigmaMulPsi_mem_grading 𝒜 d hf⟩
          (basicOpen_sigmaMulPsi_le_psi 𝒜)
          (HomogeneousLocalization.Away.map (psi 𝒜) f r)) =
      r.val

Stacks.Truncation.puncturedGradingEquivSectionsTwist_symm_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalMap.lean, line 185. The attribute's comment: “the degreewise inclusion of the sections of O_P(m) over D+(f) into the degree-zero localization of the truncation algebra at sigma f * psi f is semilinear for the chart description of the punctured cone projection, for every integer m”.

The degreewise inclusion Γ(D₊(f), 𝒪_P(m)) → (B[1/σ f · ψ f])₀ is semilinear for the chart description of the punctured cone projection, the map A₍f₎ → B₍σ f · ψ f₎ of degree-zero localizations attached to ψ followed by restriction. Scaling a section of 𝒪_P(m) by a degree-zero fraction r multiplies its image by the image of r.

theorem puncturedGradingEquivSectionsTwist_symm_smul (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) (m : ℤ)
    (r : HomogeneousLocalization.Away 𝒜 f)
    (s : (twistingSheaf 𝒜 m).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (((puncturedGradingEquivSectionsTwist 𝒜 d hf hd m).symm
          ((ProjectiveSpectrum.Proj.awayToSection 𝒜 f).hom r • s) :
        HomogeneousLocalization.Away (grading 𝒜) (sigmaMulPsi 𝒜 f))) =
      ProjectiveSpectrum.degreeZeroRingMap (grading 𝒜) (psi 𝒜 f) (sigmaMulPsi 𝒜 f)
          ⟨d, hd, GradedRingHom.map_mem (psi 𝒜) hf⟩ ⟨d, hd, sigmaMulPsi_mem_grading 𝒜 d hf⟩
          (basicOpen_sigmaMulPsi_le_psi 𝒜) (HomogeneousLocalization.Away.map (psi 𝒜) f r) *
        (((puncturedGradingEquivSectionsTwist 𝒜 d hf hd m).symm s :
          HomogeneousLocalization.Away (grading 𝒜) (sigmaMulPsi 𝒜 f)))

Stacks.Truncation.puncturedGradingEquivSectionsTwist_symm_degree_indep, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalMap.lean, line 207. The attribute's comment: “the punctured degreewise inclusion over one standard open depends only on that open, not on the degree of the element cutting it out”.

The punctured degreewise inclusion depends only on the standard open, not on the degree in which f is homogeneous.

theorem puncturedGradingEquivSectionsTwist_symm_degree_indep {d d' : ℕ} (hf : f ∈ 𝒜 d)
    (hd : 0 < d) (hf' : f ∈ 𝒜 d') (hd' : 0 < d') (m : ℤ)
    (s : (twistingSheaf 𝒜 m).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (((puncturedGradingEquivSectionsTwist 𝒜 d hf hd m).symm s :
        HomogeneousLocalization.Away (grading 𝒜) (sigmaMulPsi 𝒜 f))) =
      (((puncturedGradingEquivSectionsTwist 𝒜 d' hf' hd' m).symm s :
        HomogeneousLocalization.Away (grading 𝒜) (sigmaMulPsi 𝒜 f)))

Stacks.AlgebraicGeometry.ProjConeTwist.openUInL_image_puncturedPi_preimage_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalMap.lean, line 262. The attribute's comment: “the image in L of the chart of U over a standard open D+(f) is the standard open D+(sigma f * psi f), for the truncation cone”.

The image in L of the chart of U over D₊(f) is the standard open D₊(σ f · ψ f).

theorem openUInL_image_puncturedPi_preimage_basicOpen (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (openUInL 𝒜).ι ''ᵁ (((openUInL 𝒜).ι ≫ pi 𝒜) ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f) =
      AlgebraicGeometry.Proj.basicOpen (grading 𝒜) (sigmaMulPsi 𝒜 f)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedPi_preimage_basicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalMap.lean, line 272. The attribute's comment: “the chart of U over a standard open D+(f) is the inverse image of D+(sigma f * psi f) under the open immersion of U, for the truncation cone”.

The chart of U over D₊(f) is the inverse image of D₊(σ f · ψ f).

theorem puncturedPi_preimage_basicOpen (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    ((openUInL 𝒜).ι ≫ pi 𝒜) ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f =
      (openUInL 𝒜).ι ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen (grading 𝒜) (sigmaMulPsi 𝒜 f)

Stacks.AlgebraicGeometry.ProjConeTwist.awayToSection_puncturedPi_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalMap.lean, line 330. The attribute's comment: “the punctured cone projection on functions over a standard open, with the sections over D+(sigma f * psi f) restricted to the chart of U over D+(f)”.

The punctured cone projection on functions over a standard open, in the form the direct image needs: the image of a degree-zero fraction of A under the chart description puncturedAwayMap, read as a function on D₊(σ f · ψ f) and restricted to the chart of U over D₊(f), is the pullback of that fraction along π|_U.

theorem awayToSection_puncturedPi_app (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (r : HomogeneousLocalization.Away 𝒜 f) :
    (puncturedChartRestrict 𝒜 d hf hd).hom
        ((AlgebraicGeometry.Proj.awayToSection (grading 𝒜) (sigmaMulPsi 𝒜 f)).hom
          (ProjectiveSpectrum.degreeZeroRingMap (grading 𝒜) (psi 𝒜 f) (sigmaMulPsi 𝒜 f)
            ⟨d, hd, GradedRingHom.map_mem (psi 𝒜) hf⟩
            ⟨d, hd, sigmaMulPsi_mem_grading 𝒜 d hf⟩ (basicOpen_sigmaMulPsi_le_psi 𝒜)
            (HomogeneousLocalization.Away.map (psi 𝒜) f r))) =
      (((openUInL 𝒜).ι ≫ pi 𝒜).app (AlgebraicGeometry.Proj.basicOpen 𝒜 f)).hom
        ((AlgebraicGeometry.Proj.awayToSection 𝒜 f).hom r)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistAwayHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalMap.lean, line 365. The attribute's comment: “the degreewise inclusion of the sections of O_P(m) over D+(f) into the degree-zero localization of the truncation algebra at sigma f * psi f, as an additive map, for every integer m”.

The degreewise inclusion Γ(D₊(f), 𝒪_P(m)) → (B[1/σ f · ψ f])₀, as an additive map, for every integer m. It is the inverse of Stacks.Truncation.puncturedGradingEquivSectionsTwist followed by the inclusion of the degree-m summand.

def puncturedConeTwistAwayHom (m : ℤ) (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    ((twistingSheaf 𝒜 m).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) →+
      HomogeneousLocalization.Away (grading 𝒜) (sigmaMulPsi 𝒜 f)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistApp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalMap.lean, line 384. The attribute's comment: “the degreewise inclusion O_P(m) to (pi|_U)_* O_U over one standard open D+(f), as a map of modules over the sections of O_P there, for every integer m”.

The local degreewise inclusion Γ(D₊(f), 𝒪_P(m)) ⟶ Γ(D₊(f), (π|_U)_* 𝒪_U), as a morphism of modules over the sections of 𝒪_P on D₊(f), for every integer m. This is the local datum from which the global morphism 𝒪_P(m) ⟶ (π|_U)_* 𝒪_U is glued.

def puncturedConeTwistApp (m : ℤ) (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (twistingSheaf 𝒜 m).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)) ⟶
      (Stacks.Morphisms.pushforwardStructureSheaf ((openUInL 𝒜).ι ≫ pi 𝒜)).val.obj
        (op (AlgebraicGeometry.Proj.basicOpen 𝒜 f))

Stacks.Truncation.puncturedToLocalization_degreeZeroRingMap_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalRestriction.lean, line 82. The attribute's comment: “the comparison maps (B[1/sigma f * psi f])_0 to A[1/f] commute with the restriction maps of degree-zero localizations, for a general inclusion D+(g) <= D+(f) of standard opens”.

The comparison maps (B[1/σ f · ψ f])₀ → A[1/f] commute with the restriction maps of degree-zero localizations: the one of B attached to D₊(σ g · ψ g) ⊆ D₊(σ f · ψ f) on the source, the one of A attached to D₊(g) ⊆ D₊(f) on the target. This is the restriction compatibility of the degreewise description of the functions on the punctured cone.

theorem puncturedToLocalization_degreeZeroRingMap_le
    (hf : ∃ d : ℕ, 0 < d ∧ f ∈ 𝒜 d) (hg : ∃ e : ℕ, 0 < e ∧ g ∈ 𝒜 e)
    (hσψf : ∃ d : ℕ, 0 < d ∧ sigmaMulPsi 𝒜 f ∈ grading 𝒜 d)
    (hσψg : ∃ e : ℕ, 0 < e ∧ sigmaMulPsi 𝒜 g ∈ grading 𝒜 e)
    (hfg : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f)
    (hσψfg : ProjectiveSpectrum.basicOpen (grading 𝒜) (sigmaMulPsi 𝒜 g) ≤
      ProjectiveSpectrum.basicOpen (grading 𝒜) (sigmaMulPsi 𝒜 f))
    (z : HomogeneousLocalization.Away (grading 𝒜) (sigmaMulPsi 𝒜 f)) :
    puncturedToLocalization 𝒜
        (ProjectiveSpectrum.degreeZeroRingMap (grading 𝒜) (sigmaMulPsi 𝒜 f) (sigmaMulPsi 𝒜 g)
          hσψf hσψg hσψfg z) =
      ProjectiveSpectrum.localizedRingMap 𝒜 f g hf hg hfg (puncturedToLocalization 𝒜 z)

Stacks.AlgebraicGeometry.ProjConeTwist.basicOpen_sigmaMulPsi_le_of_basicOpen_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalRestriction.lean, line 126. The attribute's comment: “the chart of U over D+(g) is contained in the chart over D+(f), for the truncation cone and an inclusion D+(g) <= D+(f) of standard opens of P”.

The chart of U over D₊(g) is contained in the chart over D₊(f) as soon as D₊(g) ⊆ D₊(f): each chart is the part U ⊓ D₊(ψ ·) of the punctured cone lying over the standard open, and ψ carries the inclusion to one of standard opens of L.

theorem basicOpen_sigmaMulPsi_le_of_basicOpen_le {d e : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (hg : g ∈ 𝒜 e) (he : 0 < e)
    (hfg : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f) :
    ProjectiveSpectrum.basicOpen (grading 𝒜) (sigmaMulPsi 𝒜 g) ≤
      ProjectiveSpectrum.basicOpen (grading 𝒜) (sigmaMulPsi 𝒜 f)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistAwayHom_degreeZeroRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedLocalRestriction.lean, line 146. The attribute's comment: “the punctured degreewise inclusion of the sections of O_P(m) into the degree-zero localization of the truncation algebra at sigma f * psi f commutes with restriction between two standard opens, for every integer m”.

The punctured degreewise inclusion commutes with restriction between two standard opens, read in the degree-zero localizations of the truncation algebra. On the source the restriction of a section of 𝒪_P(m) is the map of localizations of the shifted regular module, on the target it is the degree-zero restriction map of B, and the comparison maps to A[1/g] identify the two.

theorem puncturedConeTwistAwayHom_degreeZeroRingMap (m : ℤ) {d e : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (hg : g ∈ 𝒜 e) (he : 0 < e)
    (hfg : ProjectiveSpectrum.basicOpen 𝒜 g ≤ ProjectiveSpectrum.basicOpen 𝒜 f)
    (s : (ProjectiveSpectrum.Proj.twistingSheaf 𝒜 m).val.obj
      (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    puncturedConeTwistAwayHom 𝒜 m e hg he
        (((ProjectiveSpectrum.Proj.twistingSheaf 𝒜 m).val.map (homOfLE hfg).op).hom s) =
      ProjectiveSpectrum.degreeZeroRingMap (grading 𝒜) (sigmaMulPsi 𝒜 f) (sigmaMulPsi 𝒜 g)
        ⟨d, hd, sigmaMulPsi_mem_grading 𝒜 d hf⟩ ⟨e, he, sigmaMulPsi_mem_grading 𝒜 e hg⟩
        (basicOpen_sigmaMulPsi_le_of_basicOpen_le 𝒜 hf hd hg he hfg)
        (puncturedConeTwistAwayHom 𝒜 m d hf hd s)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistAwayHom_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedMul.lean, line 88. The attribute's comment: “the punctured degreewise inclusion of the sections of the twisting sheaves over D+(f) into the degree-zero localization of the truncation algebra at sigma f * psi f is multiplicative, in every pair of integer degrees”.

The punctured degreewise inclusion Γ(D₊(f), 𝒪_P(m)) → (B[1/σ f · ψ f])₀ is multiplicative, in every pair of integer degrees.

theorem puncturedConeTwistAwayHom_mul (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) (i j : ℤ)
    (x : (twistingSheaf 𝒜 i).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)))
    (y : (twistingSheaf 𝒜 j).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    puncturedConeTwistAwayHom 𝒜 (i + j) d hf hd
        (twistMulSection 𝒜 i j (op (ProjectiveSpectrum.basicOpen 𝒜 f)) x y) =
      puncturedConeTwistAwayHom 𝒜 i d hf hd x * puncturedConeTwistAwayHom 𝒜 j d hf hd y

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistAwayHom_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedMul.lean, line 111. The attribute's comment: “the punctured degreewise inclusion of the sections of the untwisted sheaf over D+(f) into the degree-zero localization of the truncation algebra at sigma f * psi f carries the unit section to 1”.

The punctured degreewise inclusion Γ(D₊(f), 𝒪_P(0)) → (B[1/σ f · ψ f])₀ is unital.

theorem puncturedConeTwistAwayHom_one (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    puncturedConeTwistAwayHom 𝒜 0 d hf hd
        ((twistOne 𝒜).eval (op (ProjectiveSpectrum.basicOpen 𝒜 f))) = 1

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistApp_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedMul.lean, line 126. The attribute's comment: “the local punctured degreewise inclusion of the sections of O_P(m) into the functions on the punctured cone over D+(f) is multiplicative, in every pair of integer degrees”.

The local punctured degreewise inclusion on sections is multiplicative, in every pair of integer degrees.

theorem puncturedConeTwistApp_mul (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) (i j : ℤ)
    (x : (twistingSheaf 𝒜 i).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)))
    (y : (twistingSheaf 𝒜 j).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (show puncturedConeSections 𝒜 (ProjectiveSpectrum.basicOpen 𝒜 f) from
        (puncturedConeTwistApp 𝒜 (i + j) d hf hd).hom
          (twistMulSection 𝒜 i j (op (ProjectiveSpectrum.basicOpen 𝒜 f)) x y)) =
      (show puncturedConeSections 𝒜 (ProjectiveSpectrum.basicOpen 𝒜 f) from
          (puncturedConeTwistApp 𝒜 i d hf hd).hom x) *
        (show puncturedConeSections 𝒜 (ProjectiveSpectrum.basicOpen 𝒜 f) from
          (puncturedConeTwistApp 𝒜 j d hf hd).hom y)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistApp_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedMul.lean, line 148. The attribute's comment: “the local punctured degreewise inclusion in degree zero carries the unit section of the untwisted sheaf to the function 1 on the punctured cone, over a standard open”.

The local punctured degreewise inclusion in degree zero carries the unit section to the function 1 on the part of the punctured cone over the standard open.

theorem puncturedConeTwistApp_one (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (show puncturedConeSections 𝒜 (ProjectiveSpectrum.basicOpen 𝒜 f) from
        (puncturedConeTwistApp 𝒜 0 d hf hd).hom
          ((twistOne 𝒜).eval (op (ProjectiveSpectrum.basicOpen 𝒜 f)))) = 1

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedTwistHom_mul_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedMul.lean, line 243. The attribute's comment: “the inclusions of the homogeneous pieces of the integral twist algebra in (pi|_U)_* O_U are multiplicative, over every open of P and in every pair of integer degrees, for the punctured cone of the truncation algebra”.

The inclusions of the homogeneous pieces of the algebra of all integral twists in (π|_U)_* 𝒪_U multiply as the grading prescribes, over every open of P and in every pair of integer degrees. This is the ι_mul condition of AlgebraicGeometry.AbstractCone for the punctured cone of the truncation algebra, graded by Stacks.AlgebraicGeometry.ProjConeTwist.integerTwistAlgebra.

theorem puncturedTwistHom_mul_app (i j : ℤ) (U : Opens (ProjectiveSpectrum.top 𝒜))
    (a : (twistingSheaf 𝒜 i).val.obj (op U)) (b : (twistingSheaf 𝒜 j).val.obj (op U)) :
    (show puncturedConeSections 𝒜 U from
        (puncturedTwistHom 𝒜 (i + j)).val.app (op U)
          ((twistMul 𝒜 i j).app (op U) a b)) =
      (show puncturedConeSections 𝒜 U from (puncturedTwistHom 𝒜 i).val.app (op U) a) *
        (show puncturedConeSections 𝒜 U from (puncturedTwistHom 𝒜 j).val.app (op U) b)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedTwistHom_one_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedMul.lean, line 267. The attribute's comment: “the inclusion of the degree-zero piece of the integral twist algebra carries the unit of the algebra to the function 1 on the punctured cone, over every open of P”.

The inclusion of the degree-zero piece of the algebra of all integral twists carries the unit of that algebra to the function 1 on the punctured cone, over every open of P.

theorem puncturedTwistHom_one_app (U : Opens (ProjectiveSpectrum.top 𝒜)) :
    (show puncturedConeSections 𝒜 U from
        (puncturedTwistHom 𝒜 0).val.app (op U) ((twistOne 𝒜).eval (op U))) = 1

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeAlgebraSectionsEquivAway, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedPushforward.lean, line 67. The attribute's comment: “the sections of the direct image of the structure sheaf of the punctured cone over a standard open D₊(f) of P are the localization A[1/f]”.

The sections of the direct image of the structure sheaf of the punctured cone over a standard open D₊(f) of P = Proj A are the localization of A at f: ((π|_U)_* 𝒪_U)(D₊(f)) ≃+* A[1/f].

def puncturedConeAlgebraSectionsEquivAway (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (puncturedConeAlgebra (truncationConeData 𝒜)).right.obj.obj
        (op (Proj.basicOpen 𝒜 f)) ≃+*
      Localization.Away f

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeAlgebraSectionsRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedPushforward.lean, line 82. The attribute's comment: “the footnote computation (π|_U)_* O_U = ⨁_{m ∈ ℤ} O_P(m), over one standard open D₊(f) of P and for the truncation algebra, with the summands written as the homogeneous parts of A[1/f]”.

The sections of the direct image of the structure sheaf of the punctured cone over a standard open D₊(f) of P = Proj A are the direct sum, over all integer degrees, of the homogeneous parts of the localization A[1/f]: ((π|_U)_* 𝒪_U)(D₊(f)) ≃+* ⨁_{m ∈ ℤ} (A[1/f])_m.

def puncturedConeAlgebraSectionsRingEquiv (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (puncturedConeAlgebra (truncationConeData 𝒜)).right.obj.obj
        (op (Proj.basicOpen 𝒜 f)) ≃+*
      (⨁ m : ℤ, ↥(puncturedGrading 𝒜 d hf m))

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeAlgebraSectionsEquivTwistSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedPushforward.lean, line 98. The attribute's comment: “the footnote computation (π|_U)_* O_U = ⨁_{m ∈ ℤ} O_P(m), over one standard open D₊(f) of P and for the truncation algebra, with the summands written as the sections of the twisting sheaves”.

The sections of the direct image of the structure sheaf of the punctured cone over a standard open D₊(f) of P = Proj A are the direct sum of the sections of the twisting sheaves over D₊(f): ((π|_U)_* 𝒪_U)(D₊(f)) ≃+ ⨁_{m ∈ ℤ} Γ(D₊(f), 𝒪_P(m)).

def puncturedConeAlgebraSectionsEquivTwistSections (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (puncturedConeAlgebra (truncationConeData 𝒜)).right.obj.obj
        (op (Proj.basicOpen 𝒜 f)) ≃+
      (⨁ m : ℤ, ↥((ProjectiveSpectrum.Proj.twistingSheaf 𝒜 m).val.obj
        (op (ProjectiveSpectrum.basicOpen 𝒜 f))))

Stacks.AlgebraicGeometry.ProjConeTwist.coneAlgebraSectionsEquivTwistSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedPushforward.lean, line 112. The attribute's comment: “the footnote computation π_* O_L = ⨁_{m ≥ 0} O_P(m), over one standard open D₊(f) of P and for the truncation algebra, with the summands written as the sections of the twisting sheaves”.

The sections of the direct image of the structure sheaf of the cone over a standard open D₊(f) of P = Proj A are the direct sum of the sections of the nonnegative twisting sheaves over D₊(f): (π_* 𝒪_L)(D₊(f)) ≃+ ⨁_{m ≥ 0} Γ(D₊(f), 𝒪_P(m)).

def coneAlgebraSectionsEquivTwistSections (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (coneAlgebra (truncationConeData 𝒜)).right.obj.obj
        (op (Proj.basicOpen 𝒜 f)) ≃+
      (⨁ m : ℕ, ↥((ProjectiveSpectrum.Proj.twistingSheaf 𝒜 (m : ℤ)).val.obj
        (op (ProjectiveSpectrum.basicOpen 𝒜 f))))

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeAlgebraSectionsRingEquiv_symm_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedStandardOpenSum.lean, line 75. The attribute's comment: “the inverse of the standard-open direct-sum decomposition of the functions on the punctured cone carries the m-th summand to the inclusion of a degree-m fraction, for every integer m”.

The m-th summand of the ring isomorphism Γ(D₊(f), (π|_U)_* 𝒪_U) ≃+* ⨁_{m ∈ ℤ} (A[1/f])_m. Read backwards, a degree-m element y of (B[1/σ f · ψ f])₀ placed in the m-th summand is y itself, read as a function on D₊(σ f · ψ f) through the identification of [Stacks, Tag 01M6] and restricted to the chart of U over D₊(f).

theorem puncturedConeAlgebraSectionsRingEquiv_symm_of (m : ℤ) (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (y : puncturedGrading 𝒜 d hf m) :
    (puncturedConeAlgebraSectionsRingEquiv 𝒜 d hf hd).symm
        (DirectSum.of (fun k : ℤ => ↥(puncturedGrading 𝒜 d hf k)) m y) =
      (eqToHom (puncturedConeAlgebra_sections_basicOpen 𝒜 d hf hd).symm).hom
        ((AlgebraicGeometry.Proj.awayToSection (grading 𝒜) (sigmaMulPsi 𝒜 f)).hom
          (y : HomogeneousLocalization.Away (grading 𝒜) (sigmaMulPsi 𝒜 f)))

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeAlgebraSectionsEquivTwistSections_symm_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedStandardOpenSum.lean, line 104. The attribute's comment: “the m-th summand of the standard-open direct-sum decomposition of the functions on the punctured cone is the local degreewise inclusion of the sections of O_P(m), for the truncation cone and every integer m”.

The m-th summand of the standard-open decomposition Γ(D₊(f), (π|_U)_* 𝒪_U) = ⨁_{m ∈ ℤ} Γ(D₊(f), 𝒪_P(m)) is the local degreewise inclusion Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeTwistApp. This identifies the footnote computation of [Stacks, Tag 0EKG] over one standard open with the local datum the morphism 𝒪_P(m) ⟶ (π|_U)_* 𝒪_U of sheaves of 𝒪_P-modules is glued from.

theorem puncturedConeAlgebraSectionsEquivTwistSections_symm_of (m : ℤ) (d : ℕ) (hf : f ∈ 𝒜 d)
    (hd : 0 < d)
    (s : (ProjectiveSpectrum.Proj.twistingSheaf 𝒜 m).val.obj
      (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (puncturedConeAlgebraSectionsEquivTwistSections 𝒜 d hf hd).symm (DirectSum.of _ m s) =
      (puncturedConeTwistApp 𝒜 m d hf hd).hom s

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedTotalMap_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedTotalRing.lean, line 158. The attribute's comment: “the comparison from the objectwise direct sum of the twisting sheaves to the functions on the punctured cone is multiplicative, over every open of P”.

The map is multiplicative.

theorem puncturedTotalMap_mul (V : Opens (ProjectiveSpectrum.top 𝒜))
    (z w : (integerTwistPresheafAlgebra 𝒜).Total (op V)) :
    puncturedTotalMap 𝒜 V (z * w) = puncturedTotalMap 𝒜 V z * puncturedTotalMap 𝒜 V w

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedTotalRingHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPuncturedTotalRing.lean, line 174. The attribute's comment: “the degreewise inclusions as a ring homomorphism from the sections of the ungraded realization of the integral twist algebra to the functions on the punctured cone, over every open of P, for the truncation cone”.

The degreewise inclusions as a ring homomorphism Γ(V, ⨁_{m ∈ ℤ} 𝒪_P(m)) →+* Γ(U, (π|_U)⁻¹V). The sections of the ungraded realization of the algebra of all integral twists over V map to the functions on the part of the punctured cone lying over V, degreewise by the inclusion of the twisting sheaf.

def puncturedTotalRingHom (V : Opens (ProjectiveSpectrum.top 𝒜)) :
    (integerTwistPresheafAlgebra 𝒜).Total (op V) →+* puncturedConeSections 𝒜 V

Stacks.AlgebraicGeometry.ProjConeTwist.coneAlgebraSectionsRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistPushforward.lean, line 55. The attribute's comment: “the footnote computation π_* O_L = ⨁_{m ≥ 0} O_P(m), over one standard open D₊(f) of P and for the truncation algebra, with the summands written as the homogeneous parts of A[1/f]”.

The sections of the direct image of the structure sheaf of the cone over a standard open D₊(f) of P = Proj A are the direct sum, over the nonnegative degrees, of the homogeneous parts of the localization A[1/f]: (π_* 𝒪_L)(D₊(f)) ≃+* ⨁_{m ≥ 0} (A[1/f])_m.

def coneAlgebraSectionsRingEquiv (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (coneAlgebra (truncationConeData 𝒜)).right.obj.obj (op (Proj.basicOpen 𝒜 f)) ≃+*
      (⨁ m : ℕ, ↥(awayGrading 𝒜 d hf m))

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedToConeRelativeSpecTwistAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 94. The attribute's comment: “the top-left arrow of the diagram, the morphism of relative spectra over P induced by the inclusion of the nonnegative twist algebra in the integral one”.

The morphism Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ⟶ Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) over P = Proj A induced by the inclusion ⨁_{m ≥ 0} 𝒪_P(m) ↪ ⨁_{m ∈ ℤ} 𝒪_P(m) of Stacks.AlgebraicGeometry.ProjConeTwist.nonnegToIntegerTwistAlgebraSheafHom.

def puncturedToConeRelativeSpecTwistAlgebra :
    Over.mk (relativeSpecToBase (integerTwistAlgebraSheaf 𝒜)) ⟶
      Over.mk (relativeSpecToBase (nonnegTwistAlgebraSheaf 𝒜))

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedToConeRelativeSpecTwistAlgebra_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 105. The attribute's comment: “the top-left arrow of the diagram is the open immersion of the punctured cone in the cone, under the two presentations as relative spectra, as morphisms over P”.

The morphism Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ⟶ Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) is the open immersion of the punctured cone in the cone, under the two presentations L = Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) and U = Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)), as morphisms over P = Proj A.

theorem puncturedToConeRelativeSpecTwistAlgebra_comp :
    puncturedToConeRelativeSpecTwistAlgebra 𝒜 ≫ (coneRelativeSpecTwistAlgebraIso 𝒜).inv =
      (puncturedConeRelativeSpecTwistAlgebraIso 𝒜).inv ≫ openUInLOver 𝒜

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedToConeRelativeSpecTwistAlgebra_left_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 146. The attribute's comment: “the left square of the diagram commutes: the top-left arrow followed by L → X is the left identification with U followed by the inclusion of U in X”. References: EGA II (8.6.2), “special case”.

The morphism Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ⟶ Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) = L followed by the structure morphism σ : L ⟶ X is the identification Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ≅ U of Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeRelativeSpecTwistAlgebraIsoOpenU followed by the inclusion U ⟶ X.

theorem puncturedToConeRelativeSpecTwistAlgebra_left_comp :
    (puncturedToConeRelativeSpecTwistAlgebra 𝒜).left ≫
        (coneRelativeSpecTwistAlgebraIso 𝒜).inv.left ≫ toSpecA 𝒜 =
      (puncturedConeRelativeSpecTwistAlgebraIsoOpenU 𝒜).hom ≫ (ProjAndSpec.openU 𝒜).ι

Stacks.AlgebraicGeometry.ProjConeTwist.coneProjIsoRelativeSpecTwistAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 160. The attribute's comment: “L = Proj B is, as a scheme, the relative spectrum over P of the nonnegative twist algebra”.

The cone L = Proj B of the truncation algebra B = ⨁_{d ≥ 0} A_{≥ d} is, as a scheme, the relative spectrum over P = Proj A of the algebra of nonnegative twists.

def coneProjIsoRelativeSpecTwistAlgebra :
    AlgebraicGeometry.Proj (grading 𝒜) ≅
      Stacks.AffineAlgebraEquivalence.relativeSpec (nonnegTwistAlgebraSheaf 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.coneProjIsoRelativeSpecTwistAlgebra_hom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 169. The attribute's comment: “the identification of L = Proj B with the relative spectrum of the nonnegative twist algebra is one over P, as morphisms of schemes”.

The identification L = Proj B ≅ Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) is one over P: followed by the structure morphism of the relative spectrum it is the cone projection π : L ⟶ P.

theorem coneProjIsoRelativeSpecTwistAlgebra_hom_comp :
    (coneProjIsoRelativeSpecTwistAlgebra 𝒜).hom ≫
        relativeSpecToBase (nonnegTwistAlgebraSheaf 𝒜) =
      pi 𝒜

Stacks.AlgebraicGeometry.ProjConeTwist.coneRelativeSpecIsoTwistAlgebraViaDirectImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 190. The attribute's comment: “L is, over P, the relative spectrum of the nonnegative twist algebra by the route of the diagram: the presentation of L as the relative spectrum of pi_ O_L composed with the comparison of pi_ O_L with the direct sum of the twists O_P(m) over m at least 0”. References: EGA II (8.7.3), “partial”.

L ≅ Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) over P, as the presentation of the cone as the relative spectrum of its direct-image algebra π_* 𝒪_L (Stacks.AlgebraicGeometry.ProjConeTwist.coneRelativeSpecIso) followed by the comparison Stacks.AlgebraicGeometry.ProjConeTwist.coneAlgebraSheafIso of π_* 𝒪_L with the algebra of nonnegative twists.

def coneRelativeSpecIsoTwistAlgebraViaDirectImage :
    Over.mk (pi 𝒜) ≅ Over.mk (relativeSpecToBase (nonnegTwistAlgebraSheaf 𝒜))

Stacks.AlgebraicGeometry.ProjConeTwist.coneRelativeSpecIsoTwistAlgebraViaDirectImage_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 201. The attribute's comment: “the route through pi_* O_L is the one-step identification of L with the relative spectrum of the nonnegative twist algebra”.

The identification of L with Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) through π_* 𝒪_L is Stacks.AlgebraicGeometry.ProjConeTwist.coneRelativeSpecTwistAlgebraIso.

theorem coneRelativeSpecIsoTwistAlgebraViaDirectImage_eq :
    coneRelativeSpecIsoTwistAlgebraViaDirectImage 𝒜 = coneRelativeSpecTwistAlgebraIso 𝒜

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedToConeRelativeSpecTwistAlgebra_left_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 234. The attribute's comment: “the top-left arrow of the diagram, as a morphism of schemes, is the open immersion of the punctured cone in L conjugated by the two relative-spectrum identifications”.

As a morphism of schemes, Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ⟶ Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) is the identification Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ≅ U, then the open immersion U ⟶ L, then the identification L ≅ Spec_P(⨁_{m ≥ 0} 𝒪_P(m)).

theorem puncturedToConeRelativeSpecTwistAlgebra_left_eq :
    (puncturedToConeRelativeSpecTwistAlgebra 𝒜).left =
      ((Over.forget (AlgebraicGeometry.Proj 𝒜)).mapIso
            (puncturedConeRelativeSpecTwistAlgebraIso 𝒜)).inv ≫
        (openUInL 𝒜).ι ≫ (coneProjIsoRelativeSpecTwistAlgebra 𝒜).hom

Stacks.AlgebraicGeometry.ProjConeTwist.isOpenImmersion_puncturedToConeRelativeSpecTwistAlgebra_left, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 245. The attribute's comment: “the top-left arrow of the diagram is an open immersion of schemes”.

The morphism Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ⟶ Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) is an open immersion of schemes.

instance isOpenImmersion_puncturedToConeRelativeSpecTwistAlgebra_left :
    IsOpenImmersion (puncturedToConeRelativeSpecTwistAlgebra 𝒜).left

Stacks.AlgebraicGeometry.ProjConeTwist.opensRange_puncturedToConeRelativeSpecTwistAlgebra_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 259. The attribute's comment: “the image in L = Proj B of the top-left arrow of the diagram, read through the identification of L with the relative spectrum, is the open punctured cone”.

Read through the identification of L = Proj B with Spec_P(⨁_{m ≥ 0} 𝒪_P(m)), the morphism Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ⟶ L has image the punctured cone Stacks.AlgebraicGeometry.ProjAndSpecTruncation.openUInL.

theorem opensRange_puncturedToConeRelativeSpecTwistAlgebra_left :
    ((puncturedToConeRelativeSpecTwistAlgebra 𝒜).left ≫
        (coneProjIsoRelativeSpecTwistAlgebra 𝒜).inv).opensRange = openUInL 𝒜

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedToConeProj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 278. The attribute's comment: “the top-left arrow of the diagram as a morphism of schemes whose target is the cone L = Proj B”.

The morphism Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ⟶ L = Proj B of schemes: the morphism of relative spectra over P read on underlying schemes, followed by the identification Spec_P(⨁_{m ≥ 0} 𝒪_P(m)) ≅ Proj B of Stacks.AlgebraicGeometry.ProjConeTwist.coneProjIsoRelativeSpecTwistAlgebra.

def puncturedToConeProj :
    Stacks.AffineAlgebraEquivalence.relativeSpec (integerTwistAlgebraSheaf 𝒜) ⟶
      AlgebraicGeometry.Proj (grading 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedConeRelativeSpecTwistAlgebraIsoOpenUOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 308. The attribute's comment: “the left square as an isomorphism over X: the left identification of Spec_P of the integer twist algebra with U is an isomorphism of schemes over X, its source lying over X by the top-left arrow followed by L → X”. References: EGA II (8.12.5), “special case”; EGA II (8.6.2), “special case”.

The identification Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ≅ U as an isomorphism of schemes over X = Spec A, the source lying over X by the morphism to L followed by σ : L ⟶ X and the target by the inclusion U ⟶ X.

def puncturedConeRelativeSpecTwistAlgebraIsoOpenUOver :
    Over.mk (puncturedToConeProj 𝒜 ≫ toSpecA 𝒜) ≅ Over.mk (ProjAndSpec.openU 𝒜).ι

Stacks.AlgebraicGeometry.ProjConeTwist.puncturedToConeProjOverSpecA, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistRelativeSpecInclusion.lean, line 319. The attribute's comment: “the left square as a morphism over X: the top-left arrow of the diagram is a morphism of schemes over X, its source lying over X by the left identification with U followed by the inclusion of U in X”.

The morphism Spec_P(⨁_{m ∈ ℤ} 𝒪_P(m)) ⟶ L = Proj B as a morphism of schemes over X = Spec A, the source lying over X by the identification with U followed by the inclusion U ⟶ X and the cone by σ : L ⟶ X.

def puncturedToConeProjOverSpecA :
    Over.mk ((puncturedConeRelativeSpecTwistAlgebraIsoOpenU 𝒜).hom ≫
        (ProjAndSpec.openU 𝒜).ι) ⟶
      Over.mk (toSpecA 𝒜)

Stacks.AlgebraicGeometry.ProjConeTwist.coe_associatedModuleSheafStandardOpenEquiv_twistMul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistStandardOpenMul.lean, line 152. The attribute's comment: “the standard-open identification of the sections of a twisting sheaf with the degree-zero fractions carries the product of two twists to the product of the fractions”.

The standard-open identification Γ(D₊(f), 𝒪_P(i)) = (A[1/f])_i carries the product of two twists to the product of their fractions.

theorem coe_associatedModuleSheafStandardOpenEquiv_twistMul {d : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (i j : ℤ)
    (x : (twistingSheaf 𝒜 i).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)))
    (y : (twistingSheaf 𝒜 j).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    ((associatedModuleSheafStandardOpenEquiv 𝒜 (twistGrading (S := A) 𝒜 (i + j)) hf hd
          (twistMulSection 𝒜 i j (op (ProjectiveSpectrum.basicOpen 𝒜 f)) x y) :
        LocalizedModule.Away f A)) =
      (associatedModuleSheafStandardOpenEquiv 𝒜 (twistGrading (S := A) 𝒜 i) hf hd x :
          LocalizedModule.Away f A) *
        (associatedModuleSheafStandardOpenEquiv 𝒜 (twistGrading (S := A) 𝒜 j) hf hd y :
          LocalizedModule.Away f A)

Stacks.AlgebraicGeometry.ProjConeTwist.coe_sectionsTwistEquivAwayGrading_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistStandardOpenMul.lean, line 195. The attribute's comment: “the identification of the sections of a twisting sheaf over a standard open with a homogeneous part of the localization is multiplicative”.

The identification of the sections of 𝒪_P(i) over D₊(f) with the degree-i part of A[1/f] is multiplicative.

theorem coe_sectionsTwistEquivAwayGrading_mul {d : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d) (i j : ℤ)
    (x : (twistingSheaf 𝒜 i).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)))
    (y : (twistingSheaf 𝒜 j).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    ((Stacks.ProjectiveCohomology.sectionsTwistEquivAwayGrading 𝒜 hf hd (i + j)
          (twistMulSection 𝒜 i j (op (ProjectiveSpectrum.basicOpen 𝒜 f)) x y) :
        LocalizedModule.Away f A)) =
      (Stacks.ProjectiveCohomology.sectionsTwistEquivAwayGrading 𝒜 hf hd i x :
          LocalizedModule.Away f A) *
        (Stacks.ProjectiveCohomology.sectionsTwistEquivAwayGrading 𝒜 hf hd j y :
          LocalizedModule.Away f A)

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistAwayHom_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistStandardOpenMul.lean, line 252. The attribute's comment: “the degreewise inclusion of the sections of the twisting sheaves over D+(f) into the degree-zero localization of the truncation algebra is multiplicative”.

The degreewise inclusion Γ(D₊(f), 𝒪_P(m)) → (B[1/ψ f])₀ is multiplicative: the product of a section of 𝒪_P(i) and one of 𝒪_P(j) goes to the product of their images.

theorem coneTwistAwayHom_mul (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) (i j : ℕ)
    (x : (twistingSheaf 𝒜 (i : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)))
    (y : (twistingSheaf 𝒜 (j : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    coneTwistAwayHom 𝒜 (i + j) d hf hd
        (natTwistMulSection 𝒜 i j (op (ProjectiveSpectrum.basicOpen 𝒜 f)) x y) =
      coneTwistAwayHom 𝒜 i d hf hd x * coneTwistAwayHom 𝒜 j d hf hd y

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistApp_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistStandardOpenMul.lean, line 270. The attribute's comment: “the local degreewise inclusion of the sections of O_P(m) into the functions on the cone over D+(f) is multiplicative, for the truncation cone”.

The local degreewise inclusion Γ(D₊(f), 𝒪_P(m)) ⟶ Γ(D₊(f), π_* 𝒪_L) is multiplicative.

theorem coneTwistApp_mul (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) (i j : ℕ)
    (x : (twistingSheaf 𝒜 (i : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)))
    (y : (twistingSheaf 𝒜 (j : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (show (AlgebraicGeometry.Proj (grading 𝒜)).presheaf.obj
          (op (pi 𝒜 ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f)) from
        (coneTwistApp 𝒜 (i + j) d hf hd).hom
          (natTwistMulSection 𝒜 i j (op (ProjectiveSpectrum.basicOpen 𝒜 f)) x y)) =
      (show (AlgebraicGeometry.Proj (grading 𝒜)).presheaf.obj
            (op (pi 𝒜 ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f)) from
          (coneTwistApp 𝒜 i d hf hd).hom x) *
        (show (AlgebraicGeometry.Proj (grading 𝒜)).presheaf.obj
            (op (pi 𝒜 ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen 𝒜 f)) from
          (coneTwistApp 𝒜 j d hf hd).hom y)

Stacks.AlgebraicGeometry.ProjConeTwist.coneAlgebraSectionsRingEquiv_symm_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistStandardOpenSum.lean, line 53. The attribute's comment: “the inverse of the standard-open direct-sum decomposition of the functions on the cone carries the m-th summand to the inclusion of a degree-m fraction”.

The inverse of the ring isomorphism (π_* 𝒪_L)(D₊(f)) ≃+* ⨁_{m ≥ 0} (A[1/f])_m sends a degree-m element y of (B[1/ψ f])₀, placed in the m-th summand, to y read as a function on D₊(ψ f) by AlgebraicGeometry.Proj.awayToSection and transported along π⁻¹(D₊(f)) = D₊(ψ f).

theorem coneAlgebraSectionsRingEquiv_symm_of (m d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (y : awayGrading 𝒜 d hf m) :
    (coneAlgebraSectionsRingEquiv 𝒜 d hf hd).symm
        (DirectSum.of (fun k : ℕ => ↥(awayGrading 𝒜 d hf k)) m y) =
      (eqToHom (coneAlgebra_sections_basicOpen 𝒜 d hf hd).symm).hom
        ((AlgebraicGeometry.Proj.awayToSection (grading 𝒜) (psi 𝒜 f)).hom
          (y : HomogeneousLocalization.Away (grading 𝒜) (psi 𝒜 f)))

Stacks.AlgebraicGeometry.ProjConeTwist.coneAlgebraSectionsEquivTwistSections_symm_of, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistStandardOpenSum.lean, line 78. The attribute's comment: “the m-th summand of the standard-open direct-sum decomposition of the functions on the cone is the local degreewise inclusion of the sections of O_P(m), for the truncation cone”.

The inclusion of the m-th summand of the standard-open decomposition Γ(D₊(f), π_* 𝒪_L) = ⨁_{m ≥ 0} Γ(D₊(f), 𝒪_P(m)) is the degreewise inclusion Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistApp.

theorem coneAlgebraSectionsEquivTwistSections_symm_of (m d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d)
    (s : (ProjectiveSpectrum.Proj.twistingSheaf 𝒜 (m : ℤ)).val.obj
      (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    (coneAlgebraSectionsEquivTwistSections 𝒜 d hf hd).symm (DirectSum.of _ m s) =
      (coneTwistApp 𝒜 m d hf hd).hom s

Stacks.AlgebraicGeometry.ProjConeTwist.coneTotalMap_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistTotalRing.lean, line 134. The attribute's comment: “the comparison from the objectwise direct sum of the homogeneous pieces of the nonnegative twist algebra to the functions on the cone is multiplicative, over every open of P”.

The map is multiplicative.

theorem coneTotalMap_mul (U : Opens (ProjectiveSpectrum.top 𝒜))
    (z w : (nonnegTwistPresheafAlgebra 𝒜).Total (op U)) :
    coneTotalMap 𝒜 U (z * w) = coneTotalMap 𝒜 U z * coneTotalMap 𝒜 U w

Stacks.AlgebraicGeometry.ProjConeTwist.coneTotalRingHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistTotalRing.lean, line 156. The attribute's comment: “the degreewise inclusions as a ring homomorphism from the sections of the ungraded realization of the nonnegative twist algebra to the functions on the cone, over every open of P, for the truncation cone”.

The degreewise inclusions as a ring homomorphism Γ(U, ⨁_{m ≥ 0} 𝒪_P(m)) →+* Γ(L, π⁻¹U). The sections of the ungraded realization of the algebra of nonnegative twists over U map to the functions on the part of the cone lying over U, degreewise by the inclusion of the homogeneous piece.

def coneTotalRingHom (U : Opens (ProjectiveSpectrum.top 𝒜)) :
    (nonnegTwistPresheafAlgebra 𝒜).Total (op U) →+* coneSections 𝒜 U

Stacks.AlgebraicGeometry.ProjConeTwist.coneTotalPresheafHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistUngradedSheaf.lean, line 97. The attribute's comment: “the degreewise inclusions as a morphism of presheaves of rings from the ungraded realization of the nonnegative twist algebra to pi_* O_L, for the truncation cone”.

The degreewise inclusions as a morphism of presheaves of rings from the ungraded realization of the algebra of nonnegative twists into π_* 𝒪_L. Over an open of P it is the ring homomorphism Stacks.AlgebraicGeometry.ProjConeTwist.coneTotalRingHom; naturality is the naturality of Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistDirectSumHom.

def coneTotalPresheafHom :
    (nonnegTwistPresheafAlgebra 𝒜).totalPresheaf ⟶ (conePushforwardRingSheaf 𝒜).obj

Stacks.AlgebraicGeometry.ProjConeTwist.coneUngradedSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistUngradedSheaf.lean, line 133. The attribute's comment: “the identification pi_* O_L = the ungraded realization of the nonnegative twist algebra, as sheaves of rings, for the cone of the truncation algebra”.

π_* 𝒪_L is the ungraded realization of the algebra of nonnegative twists, as sheaves of rings. This is the identification of [Stacks, Tag 0EKG] at the level of sheaves of rings, as opposed to the identification coneStructureCoproductIso of the underlying sheaves of 𝒪_P-modules.

def coneUngradedSheafIso :
    (nonnegTwistAlgebra 𝒜).ungradedSheaf ≅ conePushforwardRingSheaf 𝒜

Stacks.AlgebraicGeometry.ProjConeTwist.coe_sectionsTwistEquivAwayGrading_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistUnit.lean, line 107. The attribute's comment: “the standard-open identification of the sections of the untwisted sheaf with the degree-zero fractions carries the unit section to 1”.

The standard-open identification carries the unit section of 𝒪_P(0) to 1.

theorem coe_sectionsTwistEquivAwayGrading_one {d : ℕ} (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    ((Stacks.ProjectiveCohomology.sectionsTwistEquivAwayGrading 𝒜 hf hd 0
          ((twistOne 𝒜).eval (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
        LocalizedModule.Away f A)) = 1

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistAwayHom_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistUnit.lean, line 129. The attribute's comment: “the degreewise inclusion of the sections of the untwisted sheaf over D+(f) into the degree-zero localization of the truncation algebra carries the unit section to 1”.

The degreewise inclusion Γ(D₊(f), 𝒪_P(0)) → (B[1/ψ f])₀ is unital.

theorem coneTwistAwayHom_one (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    coneTwistAwayHom 𝒜 0 d hf hd ((twistOne 𝒜).eval
        (op (ProjectiveSpectrum.basicOpen 𝒜 f))) = 1

Stacks.AlgebraicGeometry.ProjConeTwist.coneTwistApp_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistUnit.lean, line 144. The attribute's comment: “the local degreewise inclusion in degree zero carries the unit section of the untwisted sheaf to the function 1 on the cone, over a standard open”.

The local degreewise inclusion in degree zero carries the unit section to the function 1 on the part of the cone over the standard open.

theorem coneTwistApp_one (d : ℕ) (hf : f ∈ 𝒜 d) (hd : 0 < d) :
    (show coneSections 𝒜 (ProjectiveSpectrum.basicOpen 𝒜 f) from
        (coneTwistApp 𝒜 0 d hf hd).hom
          ((twistOne 𝒜).eval (op (ProjectiveSpectrum.basicOpen 𝒜 f)))) = 1

Stacks.AlgebraicGeometry.ProjConeTwist.coneIota_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjConeTwistUnit.lean, line 178. The attribute's comment: “the inclusion of the degree-zero piece of the nonnegative twist algebra carries the unit of the algebra to the function 1, over every open of P, for the truncation cone”.

The inclusion of the degree-zero piece of the algebra of nonnegative twists carries the unit of that algebra to the function 1, over every open of P. With Stacks.AlgebraicGeometry.ProjConeTwist.coneIota_mul this exhibits the inclusions as a unital ring homomorphism out of the ungraded realization of the twist algebra.

theorem coneIota_one (U : Opens (ProjectiveSpectrum.top 𝒜)) :
    (show coneSections 𝒜 U from
        (coneIota 𝒜 0).val.app (op U) ((twistOne 𝒜).eval (op U))) = 1

Stacks.AlgebraicGeometry.ProjTwistAwayPiece.coe_sectionsTwistEquivGradedPiece_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjTwistAwayPieceScalars.lean, line 78. The attribute's comment: “the description of the sections of a twisting sheaf over a standard open as a homogeneous piece of the graded localization is multiplicative”.

The identification Γ(D₊(f), 𝒪_X(n)) ≅ (A_f)_n is multiplicative: the product of a section of 𝒪_X(i) and a section of 𝒪_X(j) over D₊(f), read in (A_f)_{i + j}, is the product in A_f of the two underlying elements.

theorem coe_sectionsTwistEquivGradedPiece_mul (hf : f ∈ 𝒜 k) (hk : 0 < k) (i j : ℤ)
    (x : (twistingSheaf 𝒜 i).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f)))
    (y : (twistingSheaf 𝒜 j).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))) :
    ((sectionsTwistEquivGradedPiece 𝒜 hf hk (i + j)
          (Stacks.AlgebraicGeometry.ProjConeTwist.twistMulSection 𝒜 i j
            (op (ProjectiveSpectrum.basicOpen 𝒜 f)) x y) :
        LocalizedModule.Away f A))
      = (sectionsTwistEquivGradedPiece 𝒜 hf hk i x : LocalizedModule.Away f A) *
        (sectionsTwistEquivGradedPiece 𝒜 hf hk j y : LocalizedModule.Away f A)

Stacks.Truncation.instGradedRingGrading, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Truncation.lean, line 318. The attribute's comment: “the graded ring B = ⨁_{d ≥ 0} A_{≥ d}”.

B = ⨁_{d ≥ 0} A_{≥ d} is a graded ring with degree-d part B_d ≃ A_{≥ d}.

instance instGradedRingGrading : GradedRing (grading 𝒜)

Stacks.Truncation.sigma, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Truncation.lean, line 346. The attribute's comment: “the isomorphism σ : A ≃ B₀”.

The ring isomorphism σ : A ≃+* B_0, a ↦ a⁽⁰⁾.

def sigma : A ≃+* grading 𝒜 0

Stacks.Truncation.psi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Truncation.lean, line 399. The attribute's comment: “the graded ring map ψ : A → B”.

The graded ring map ψ : A → B with ψ(a) = a⁽ᵈ⁾ for a ∈ A_d.

def psi : 𝒜 →+*ᵍ grading 𝒜

Stacks.Truncation.tau, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Truncation.lean, line 434. The attribute's comment: “the graded ring map τ : B → A”.

The surjective graded ring map τ : B → A with τ(a⁽ᵈ⁾) = a_d.

def tau : grading 𝒜 →+*ᵍ 𝒜

Stacks.Truncation.truncationAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Truncation.lean, line 492. The attribute's comment: “the graded ring B and the maps σ, ψ, τ”.

The graded ring B = ⨁_{d ≥ 0} A_{≥ d} with its canonical maps σ, ψ and τ.

def truncationAlgebra : TruncationAlgebra 𝒜

Stacks.Truncation.tau_comp_psi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Truncation.lean, line 508. The attribute's comment: “τ ∘ ψ = id”.

τ ∘ ψ = id_A.

theorem tau_comp_psi : s.tau.comp s.psi = GradedRingHom.id 𝒜

Stacks.Truncation.tau_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Truncation.lean, line 522. The attribute's comment: “τ is surjective”.

τ is surjective.

theorem tau_surjective : Function.Surjective s.tau

Stacks.Truncation.truncationAlgebra_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/Truncation.lean, line 630. The attribute's comment: “uniqueness of the graded ring B”.

Two truncation algebras are isomorphic by a unique ring isomorphism compatible with the identifications A_{≥ d} ≃+ B_d.

theorem truncationAlgebra_unique :
    ∃! e : s.B ≃+* t.B, ∀ (d : ℕ) (a : truncation 𝒜 d),
      e ((s.degreeEquiv d a : s.B)) = ((t.degreeEquiv d a : t.B))

Stacks.Truncation.isInternal_awayGrading, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/TruncationLocalizationGraded.lean, line 149. The attribute's comment: “the equality of homogeneous parts (B[1/ψ f])_0 = ⨁_{m ≥ 0} (A[1/f])_m, the ring-theoretic form of the identification of π_* O_L with the sum of the nonnegative twists”.

(B_{ψ f})₀ = ⨁_{m ≥ 0} (A_f)_m: the degree-zero part of the localization of the truncation algebra at ψ f is the internal direct sum of its homogeneous pieces, which the comparison map identifies with the homogeneous parts of A_f in nonnegative degrees.

theorem isInternal_awayGrading (hf : f ∈ 𝒜 d) :
    DirectSum.IsInternal (awayGrading 𝒜 d hf)

Stacks.Truncation.awayGradingEquivAwayPiece, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/TruncationLocalizationGraded.lean, line 183. The attribute's comment: “the degree-m piece of (B[1/ψ f])_0 is (A[1/f])_m”.

The degree-m piece of (B_{ψ f})₀ is the degree-m part (A_f)_m of A_f.

def awayGradingEquivAwayPiece (hf : f ∈ 𝒜 d) (m : ℕ) :
    awayGrading 𝒜 d hf m ≃+ awayPiece 𝒜 d hf m

Stacks.Truncation.puncturedRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/TruncationLocalizationPunctured.lean, line 211. The attribute's comment: “the equality of rings (B[1/σ f · ψ f])_0 = A[1/f], the functions on the punctured cone over a standard open D₊(f) of P”.

(B[1/σ f · ψ f])₀ = A[1/f]: the degree-zero part of the localization of the truncation algebra at σ f · ψ f is the whole localization of A at f, the comparison map a⁽ᵏᵈ⁾ / (σ f · ψ f)ᵏ ↦ a / f ²ᵏ being a ring isomorphism.

def puncturedRingEquiv (hf : f ∈ 𝒜 d) :
    HomogeneousLocalization.Away (grading 𝒜) (sigmaMulPsi 𝒜 f) ≃+* Localization.Away f

Stacks.Truncation.isInternal_puncturedGrading, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/TruncationLocalizationPunctured.lean, line 298. The attribute's comment: “the equality of homogeneous parts (B[1/σ f · ψ f])_0 = ⨁_{m ∈ ℤ} (A[1/f])_m, the ring-theoretic form of the identification of the direct image of the structure sheaf of the punctured cone with the sum of all the integral twists”.

(B[1/σ f · ψ f])₀ = ⨁_{m ∈ ℤ} (A[1/f])_m: the degree-zero part of the localization of the truncation algebra at σ f · ψ f is the internal direct sum of its homogeneous pieces, which the comparison map identifies with the homogeneous parts of A[1/f] in all integer degrees.

theorem isInternal_puncturedGrading (hf : f ∈ 𝒜 d) :
    DirectSum.IsInternal (puncturedGrading 𝒜 d hf)

Stacks.Truncation.puncturedGradingEquivAwayGrading, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/TruncationLocalizationPunctured.lean, line 342. The attribute's comment: “the degree-m piece of (B[1/σ f · ψ f])_0 is (A[1/f])_m, for every integer m”.

The degree-m piece of (B[1/σ f · ψ f])₀ is the degree-m part of A[1/f], for every integer m.

def puncturedGradingEquivAwayGrading (hf : f ∈ 𝒜 d) (m : ℤ) :
    puncturedGrading 𝒜 d hf m ≃+ Stacks.ProjectiveCohomology.awayGrading 𝒜 hf m

Stacks.Truncation.awayGradingEquivSectionsTwist, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/TruncationLocalizationPunctured.lean, line 387. The attribute's comment: “the degree-m summand of the functions on the cone over D₊(f) is the module of sections of O_P(m) over D₊(f), for m ≥ 0”.

The degree-m summand of (B[1/ψ f])₀ is the module of sections of the twisting sheaf 𝒪_P(m) over D₊(f), for m ≥ 0.

def awayGradingEquivSectionsTwist (hf : f ∈ 𝒜 d) (hd : 0 < d) (m : ℕ) :
    awayGrading 𝒜 d hf m ≃+
      (twistingSheaf 𝒜 (m : ℤ)).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))

Stacks.Truncation.puncturedGradingEquivSectionsTwist, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/GradedAlgebra/TruncationLocalizationPunctured.lean, line 397. The attribute's comment: “the degree-m summand of the functions on the punctured cone over D₊(f) is the module of sections of O_P(m) over D₊(f), for every integer m”.

The degree-m summand of (B[1/σ f · ψ f])₀ is the module of sections of the twisting sheaf 𝒪_P(m) over D₊(f), for every integer m.

def puncturedGradingEquivSectionsTwist (hf : f ∈ 𝒜 d) (hd : 0 < d) (m : ℤ) :
    puncturedGrading 𝒜 d hf m ≃+
      (twistingSheaf 𝒜 m).val.obj (op (ProjectiveSpectrum.basicOpen 𝒜 f))

Tag 0EKH, an equation

Tag 0EKH in the Stacks Project.

Stacks.AlgebraicGeometry.ProjAndSpec.derivedPushforwardPuncturedConeIsoTruncation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Constructions/ProjAndSpecPuncturedConeProjectionFormula.lean, line 266. The attribute's comment: “the direct-sum decomposition, with RΓ read as derived direct image to Spec A₀”.

RΓ(U, 𝓕_U) = ⨁_{m ∈ Z} RΓ(P, 𝓕 ⊗_{𝒪_P} 𝒪_P(m)). Let A be a nonnegatively graded ring, P = Proj A quasi-compact, π : L ⟶ P the cone of the truncation algebra B = ⨁_{d ≥ 0} A_{≥ d} and U ⊆ L the punctured cone. For a quasi-coherent 𝒪_P-module 𝓕 with pullback 𝓕_U = (π|_U)^*𝓕, the derived global sections of 𝓕_U decompose as the direct sum, over all integers m, of the derived global sections of the m-th twist of 𝓕; both sides are read as derived direct images to Z = Spec A₀.

def derivedPushforwardPuncturedConeIsoTruncation
    [CompactSpace (AlgebraicGeometry.Proj 𝒜)] (F : (AlgebraicGeometry.Proj 𝒜).Modules)
    [F.IsQuasicoherent] :
    (Stacks.Duality.derivedPushforward
          (puncturedConeProj (truncationConeData 𝒜) ≫
            AlgebraicGeometry.Proj.toSpecZero 𝒜)).obj
        ((DerivedCategory.singleFunctor _ 0).obj
          (puncturedConePullback (truncationConeData 𝒜) F)) ≅
      ∐ fun m : ℤ => (Stacks.Duality.derivedPushforward
        (AlgebraicGeometry.Proj.toSpecZero 𝒜)).obj
        ((DerivedCategory.singleFunctor _ 0).obj (twistSheafOfModules 𝒜 F m))

Tag 0EKI, a lemma

Tag 0EKI in the Stacks Project.

Stacks.SectionRingProjIso.projAndSpecDiagram_eq_laurentDiagram_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjIso/DiagramArrows.lean, line 364. The attribute's comment: “the whole statement: P = Proj A and diagram 0EKG becomes, arrow by arrow, the diagram of the relative spectra over P of the Laurent algebras of the ample module: the open immersion U → L is the morphism induced by the inclusion of algebras, the projections to P are the structure morphisms, and the left and right squares commute”. References: EGA II (8.7.4), “(ii), special case”; EGA II (8.8.3), “special case”.

Stacks Project, Tag 0EKI: for P proper over R and 𝓛 ample, diagram 0EKG is the diagram of Spec_P(⨁_{m ∈ ℤ} 𝓛^{⊗ m}) ⟶ Spec_P(⨁_{m ≥ 0} 𝓛^{⊗ m}) ⟶ P, arrow by arrow.

Let A = Γ_*(P, 𝓛), r : P ⟶ Proj A the canonical morphism, π : L ⟶ Proj A the cone of [Stacks, Tag 0EKG] with its punctured cone U ⊆ L, σ : L ⟶ X = Spec A, and ρ, Φ_L, Φ_U the identifications P ≅ Proj A, L ≅ Spec_P(⨁_{m ≥ 0} 𝓛^{⊗ m}), U ≅ Spec_P(⨁_{m ∈ ℤ} 𝓛^{⊗ m}) (the last two over P). Then:

r is an isomorphism (P = Proj A);

the top arrow: under Φ_U and Φ_L the open immersion U ⟶ L is the morphism Spec_P(⨁_{m ∈ ℤ} 𝓛^{⊗ m}) ⟶ Spec_P(⨁_{m ≥ 0} 𝓛^{⊗ m}) induced by the inclusion of algebras ⨁_{m ≥ 0} 𝓛^{⊗ m} ⊆ ⨁_{m ∈ ℤ} 𝓛^{⊗ m}, as morphisms over P;

the projections: under Φ_L and ρ the cone projection π is the structure morphism of Spec_P(⨁_{m ≥ 0} 𝓛^{⊗ m}), and under Φ_U and ρ its restriction π|_U is that of Spec_P(⨁_{m ∈ ℤ} 𝓛^{⊗ m});

the top arrow is a morphism over P and an open immersion;

the left vertical identification Spec_P(⨁_{m ∈ ℤ} 𝓛^{⊗ m}) ≅ U ⊆ X (the = of the diagram) is Φ_U⁻¹ followed by σ|_U, an isomorphism;

the left square of the new diagram commutes: the top arrow followed by σ (read through Φ_L) is the identification with U followed by U ⊆ X;

the right square of the new diagram commutes: the projection to P followed by P = Proj A ⟶ Z = Spec A₀ is σ (read through Φ_L) followed by X ⟶ Z.

theorem projAndSpecDiagram_eq_laurentDiagram_of_isProper :
    IsIso (projHomOfIsAmple L hL) ∧
    (puncturedConeIsoLaurentOfIsProper L hL f).inv ≫ openUInLOverOfIsProper L hL f =
      laurentToNonnegLaurentRelativeSpec L hL ≫ (coneIsoNonnegLaurentOfIsProper L hL f).inv ∧
    (coneIsoNonnegLaurentOfIsProper L hL f).hom.left ≫ (nonnegLaurentRelativeSpecOver L hL).hom =
      pi (grading L) ≫ (projIsoOfIsProper L hL f).inv ∧
    (puncturedConeIsoLaurentOfIsProper L hL f).hom.left ≫ (laurentRelativeSpecOver L hL).hom =
      (openUInL (grading L)).ι ≫ pi (grading L) ≫ (projIsoOfIsProper L hL f).inv ∧
    (laurentToNonnegLaurentRelativeSpec L hL).left ≫ (nonnegLaurentRelativeSpecOver L hL).hom =
      (laurentRelativeSpecOver L hL).hom ∧
    IsOpenImmersion (laurentToNonnegLaurentRelativeSpec L hL).left ∧
    IsIso ((puncturedConeIsoLaurentOfIsProper L hL f).inv.left ≫
      (toSpecA (grading L) ∣_ Stacks.AlgebraicGeometry.ProjAndSpec.openU (grading L))) ∧
    (laurentToNonnegLaurentRelativeSpec L hL).left ≫
        (coneIsoNonnegLaurentOfIsProper L hL f).inv.left ≫ toSpecA (grading L) =
      ((puncturedConeIsoLaurentOfIsProper L hL f).inv.left ≫
        (toSpecA (grading L) ∣_ Stacks.AlgebraicGeometry.ProjAndSpec.openU (grading L))) ≫
        (Stacks.AlgebraicGeometry.ProjAndSpec.openU (grading L)).ι ∧
    (nonnegLaurentRelativeSpecOver L hL).hom ≫ (projIsoOfIsProper L hL f).hom ≫
        Proj.toSpecZero (grading L) =
      (coneIsoNonnegLaurentOfIsProper L hL f).inv.left ≫ toSpecA (grading L) ≫
        Stacks.AlgebraicGeometry.ProjAndSpec.xToZ (grading L)

Stacks.SectionRingProjIso.coneIsoNonnegLaurentOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjIso/DiagramClause.lean, line 241. The attribute's comment: “the diagram clause: the nonnegatively graded left-hand entry L of diagram 0EKG becomes Spec_P of the direct sum of the nonnegative tensor powers of the ample module”.

The diagram clause of [Stacks, Tag 0EKI], nonnegatively graded entry. For P proper over a ring R and 𝓛 an ample invertible 𝒪_P-module with section ring A = Γ_*(P, 𝓛), the nonnegatively graded left-hand entry L of [Stacks, Tag 0EKG]'s diagram, read over P through the identification P = Proj A, is Spec_P(⨁_{m ≥ 0} 𝓛^{⊗ m}).

The structure morphism on the left is the cone projection π followed by the inverse of the canonical morphism r : P ⟶ Proj A of [Stacks, Tag 01PZ], which is an isomorphism by Stacks.SectionRingProjIso.isIso_projHomOfIsAmple_of_isProper; that is what makes the base change in coneBaseChangeIsoNonnegLaurent the identity, by Stacks.AlgebraicGeometry.OverBaseChange.overPullbackIsoOfIsIso.

def coneIsoNonnegLaurentOfIsProper :
    Over.mk (pi (grading L) ≫ (projIsoOfIsProper L hL f).inv) ≅
      nonnegLaurentRelativeSpecOver L hL

Stacks.SectionRingProjIso.puncturedConeIsoLaurentOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjIso/DiagramClause.lean, line 255. The attribute's comment: “the diagram clause: the integer-graded left-hand entry U of diagram 0EKG becomes Spec_P of the direct sum of all integral tensor powers of the ample module”.

The diagram clause of [Stacks, Tag 0EKI], integer-graded entry. For P proper over a ring R and 𝓛 an ample invertible 𝒪_P-module with section ring A = Γ_*(P, 𝓛), the integer-graded left-hand entry U of [Stacks, Tag 0EKG]'s diagram, read over P through the identification P = Proj A, is Spec_P(⨁_{m ∈ ℤ} 𝓛^{⊗ m}).

def puncturedConeIsoLaurentOfIsProper :
    Over.mk ((openUInL (grading L)).ι ≫ pi (grading L) ≫ (projIsoOfIsProper L hL f).inv) ≅
      laurentRelativeSpecOver L hL

Stacks.SectionRingProjIso.isIso_projHomOfIsAmple_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjIso/Proper.lean, line 112. The attribute's comment: “the identification P = Proj(A), for P proper over R”.

Let P be a proper scheme over a ring R and 𝓛 an ample invertible 𝒪_P-module with graded section ring A = Γ_*(P, 𝓛). Then the canonical morphism r : P ⟶ Proj A of [Stacks, Tag 01PZ] is an isomorphism.

theorem isIso_projHomOfIsAmple_of_isProper (hL : IsAmple X L) {R : CommRingCat.{u}}
    (f : X ⟶ Spec R) [IsProper f] :
    IsIso (projHomOfIsAmple L hL)

Stacks.SectionRingProjIso.projIsoOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjIso/Proper.lean, line 125. The attribute's comment: “the identification P = Proj(A) as an isomorphism P ≅ Proj Γ_*(P, 𝓛), for P proper over R”.

The isomorphism P ≅ Proj Γ_*(P, 𝓛) whose underlying morphism is the canonical one of [Stacks, Tag 01PZ], for P proper over R and 𝓛 ample.

noncomputable def projIsoOfIsProper (hL : IsAmple X L) {R : CommRingCat.{u}}
    (f : X ⟶ Spec R) [IsProper f] :
    X ≅ AlgebraicGeometry.Proj (grading L)

Sources

LeanStacks.Truncation.span_degreeOne_pow_eq_truncationIdeal · Stacks.AlgebraicGeometry.ProjAndSpec.zToX · Stacks.AlgebraicGeometry.ProjAndSpec.xToZ · Stacks.AlgebraicGeometry.ProjAndSpec.openU · Stacks.AlgebraicGeometry.ProjAndSpec.projMapDomain_tau_eq_top · Stacks.AlgebraicGeometry.ProjAndSpec.projMapDomain_psi_eq_top · Stacks.AlgebraicGeometry.ProjAndSpec.pi · Stacks.AlgebraicGeometry.ProjAndSpec.zeroSection

Section37.52 Closed points in fibres #

Section 37.52 of the Stacks Project, Tag 053Q. 9 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 053R, a lemma

Tag 053R in the Stacks Project.

Stacks.Divisors.fiber_support_eq_union_irreducibleComponents_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FibreDimension/GeneralCase.lean, line 355.

Stacks 053R. Let f : X ⟶ S be a dominant morphism locally of finite type between irreducible schemes, let I be a locally principal ideal sheaf on X whose closed subscheme misses the generic fibre of f, and let s be a point of S whose fibre has dimension at most that of the generic fibre. Then the support of the closed subscheme inside the fibre X_s is set-theoretically the union of the irreducible components of X_s that it contains.

No Noetherian hypothesis: the Noetherian case Stacks.Divisors.fiber_support_eq_union_irreducibleComponents is applied not to f but to a finitely generated ℤ-algebra that the affine situation descends to, in Stacks.Divisors.fiber_preimage_zeroLocus_eq_sUnion_irreducibleComponents. The two reductions in front of that are Stacks.Divisors.fiber_support_eq_union_irreducibleComponents_of_isIntegral, which passes to the reductions of X and S and so makes both integral, and Stacks.Divisors.fiber_support_eq_union_irreducibleComponents_integral, which localises to an affine chart on which I is principal.

public theorem fiber_support_eq_union_irreducibleComponents_general {X S : Scheme.{u}}
    (f : X ⟶ S) [IrreducibleSpace S] [IrreducibleSpace X] [IsDominant f] [LocallyOfFiniteType f]
    (I : X.IdealSheafData) (hI : IsLocallyPrincipal I)
    (hgeneric : IsEmpty ((I.subschemeι ≫ f).fiber (genericPoint S))) (s : S)
    (hdim : topologicalKrullDim (f.fiber s) ≤ topologicalKrullDim (f.fiber (genericPoint S))) :
    (f.fiberι s) ⁻¹' (I.support : Set X) =
      ⋃₀ {C : Set (f.fiber s) | C ∈ irreducibleComponents (f.fiber s) ∧
        C ⊆ (f.fiberι s) ⁻¹' (I.support : Set X)}

Stacks.Divisors.fiber_support_eq_union_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/LocallyPrincipalSupport.lean, line 180. The attribute's comment: “the locally Noetherian case, the form in which Krull's principal ideal theorem applies to f directly. The statement without [IsLocallyNoetherian X], which is the source's own, is Stacks.Divisors.fiber_support_eq_union_irreducibleComponents_general in StacksFrontier/AlgebraicGeometry/FibreDimension/GeneralCase.lean:352; it applies this one to a finitely generated ℤ-algebra that the affine situation descends to, by StacksFrontier.AlgebraicGeometry.FibreDimension.AffineGeneralCase.”.

Stacks 053R, the Noetherian case. Let f : X ⟶ S be a dominant morphism locally of finite type between irreducible schemes with X locally Noetherian, let I be a locally principal ideal sheaf on X whose closed subscheme misses the generic fibre, and let s ∈ S be a point whose fibre has dimension at most that of the generic fibre. Then the support of the closed subscheme inside f.fiber s is set-theoretically the union of the irreducible components of f.fiber s that it contains.

public theorem fiber_support_eq_union_irreducibleComponents {X S : Scheme.{u}} (f : X ⟶ S)
    [IrreducibleSpace S] [IrreducibleSpace X] [IsDominant f] [LocallyOfFiniteType f]
    [IsLocallyNoetherian X] (I : X.IdealSheafData) (hI : IsLocallyPrincipal I)
    (hgeneric : IsEmpty ((I.subschemeι ≫ f).fiber (genericPoint S))) (s : S)
    (hdim : topologicalKrullDim (f.fiber s) ≤
      topologicalKrullDim (f.fiber (genericPoint S))) :
    (f.fiberι s) ⁻¹' (I.support : Set X) =
      ⋃₀ {C : Set (f.fiber s) | C ∈ irreducibleComponents (f.fiber s) ∧
        C ⊆ (f.fiberι s) ⁻¹' (I.support : Set X)}

Tag 053S, a lemma

Tag 053S in the Stacks Project.

IsLocalRing.injective_quotient_of_dimension_add_trdeg_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/HorizontalDivisor.lean, line 471.

Stacks 053S. Let A ⊆ B be an injective local homomorphism of local domains with B essentially of finite type over A, and let g ∈ 𝔪_B lie in no minimal prime over 𝔪_A B. If dim (B/𝔪_A B) + trdeg_{κ(𝔪_A)} κ(𝔪_B) = trdeg_A B, then A → B/gB is injective, i.e. the generic point of Spec A is in the image of Spec (B/gB) → Spec A.

public theorem injective_quotient_of_dimension_add_trdeg_eq
    {A B : Type u} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
    [IsLocalRing A] [IsLocalRing B] [Algebra A B]
    [IsLocalHom (algebraMap A B)]
    (hinj : Function.Injective (algebraMap A B))
    (hB : IsEssentiallyOfFiniteType A B (algebraMap A B))
    (g : B) (hg : g ∈ maximalIdeal B)
    (hnot : ∀ q ∈ (Ideal.map (algebraMap A B) (maximalIdeal A)).minimalPrimes, g ∉ q)
    (hdim : letI := (ResidueField.map (algebraMap A B)).toAlgebra;
      ringKrullDim (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A)) +
        (Cardinal.toENat (Algebra.trdeg (ResidueField A) (ResidueField B)) :
          WithBot ℕ∞) =
      (Cardinal.toENat (Algebra.trdeg A B) : WithBot ℕ∞)) :
    Function.Injective ((Ideal.Quotient.mk (Ideal.span {g})).comp (algebraMap A B))

Tag 053T, a lemma

Tag 053T in the Stacks Project.

IsLocalRing.ringKrullDim_closedFiber_add_trdeg_eq_trdeg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/RelativeDimension/FlatLocalExtension.lean, line 399. References: EGA IV (5.5.7), “field base”.

The dimension of the closed fibre of an injective flat essentially finite type local extension of domains, plus the residue-field transcendence degree, is the transcendence degree of the extension.

public theorem ringKrullDim_closedFiber_add_trdeg_eq_trdeg
    {A B : Type u} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B]
    [IsLocalRing A] [IsLocalRing B] [Algebra A B]
    [IsLocalHom (algebraMap A B)]
    (hinj : Function.Injective (algebraMap A B))
    (hfinite : IsEssentiallyOfFiniteType A B (algebraMap A B))
    [Module.Flat A B] :
    letI := (IsLocalRing.ResidueField.map (algebraMap A B)).toAlgebra
    ringKrullDim (B ⧸ (IsLocalRing.maximalIdeal A).map (algebraMap A B)) +
      (Cardinal.toENat (Algebra.trdeg (IsLocalRing.ResidueField A)
        (IsLocalRing.ResidueField B)) : WithBot ℕ∞) =
      (Cardinal.toENat (Algebra.trdeg A B) : WithBot ℕ∞)

Tag 053U, a lemma

Tag 053U in the Stacks Project.

AlgebraicGeometry.closure_closedPoints_between_fiber_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/ClosedPointsBetweenInFibres.lean, line 1753. The attribute's comment: “the density conclusion of the tag, under the tag's own hypotheses — f locally of finite type, x ⤳ x', x' closed in X_{f x'} — together with its exact range of validity: the points of X_s closed in X_s and lying between x and x' are dense in the closure of x in X_s if and only if x = x' or f x ≠ f x'. The reverse implication is the tag itself, proved by the argument of the source in closure_closedPoints_between_fiber_eq; the forward implication disposes of the only remaining situation, a nontrivial specialization inside one fibre, where the tag's set is the single closed point x' and the density is false — a gap in the source's statement, computed in closure_closedPoints_between_fiber_subset_singleton_of_eq_base and respected by the source's own proof.”.

Stacks 053U, under the hypotheses of the tag and no others. Let f : X ⟶ S be locally of finite type, let x ⤳ x' be a specialization in X with x' closed in its fibre X_{f x'}, and set s = f x. Then the points of X_s which are closed in X_s and lie between x and x' are dense in the closure of x in X_s if and only if x = x' or f x ≠ f x'.

The reverse implication is the assertion of the tag and carries its mathematical content: it is AlgebraicGeometry.closure_closedPoints_between_fiber_eq, proved by the argument of the source.

The forward implication settles the one remaining situation, a nontrivial specialization inside one fibre, where the density fails: a point of X_s closed in X_s which specializes to x' is x', so the set of the tag is {x'}, whose closure is {x'}, while the closure of x in X_s is larger whenever x ≠ x' — for X = 𝔸¹ over a field with x its generic point and x' a closed point it is all of 𝔸¹. The implication is exactly that computation, through AlgebraicGeometry.closure_closedPoints_between_fiber_subset_singleton_of_eq_base. Since the source relates f x and f x' by no hypothesis, its statement overreaches there; its proof does not, drawing the same line at the prime-avoidance step (see the module docstring).

public theorem closure_closedPoints_between_fiber_eq_iff
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (x x' : X) (hxx' : x ⤳ x')
    (hx' : IsClosed ({f.asFiber x'} : Set (f.fiber (f x')))) :
    closure {y : f.fiber (f x) |
          IsClosed ({y} : Set (f.fiber (f x))) ∧
            x ⤳ ((f.fiberι (f x)) y) ∧
              ((f.fiberι (f x)) y) ⤳ x'} =
        closure ({f.asFiber x} : Set (f.fiber (f x))) ↔
      x = x' ∨ f x ≠ f x'

Tag 053V, a remark

Tag 053V in the Stacks Project.

AlgebraicGeometry.exists_chain_isImmediateSpecialization_isClosed_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/SpecializationChainInFibre.lean, line 118. The attribute's comment: “the chain of immediate specializations inside the fibre, of length d, ending in a closed point of the fibre, together with the avoidance clause, and with nothing assumed about a prescribed x'. The final link x_d ⤳ x' to a prescribed x' with x ⤳ x' closed in its own fibre is not in this file, which never mentions x'; it is AlgebraicGeometry.exists_chain_isImmediateSpecialization_specializes_fiber_of_isClosed in StacksFrontier.AlgebraicGeometry.Morphisms.Fibres.SpecializationChainToClosedSpecialization, where AlgebraicGeometry.exists_chain_isImmediateSpecialization_specializes_fiber_iff states every assertion of the remark at once, at the hypotheses of the tag, together with the exact range of validity of the remark.”.

Stacks 053V, the chain of immediate specializations inside the fibre, together with the avoidance clause. For f locally of finite type and W a closed subset of the fibre X_{f x} not containing x, there is a chain

x = c 0 ⤳ c 1 ⤳ ⋯ ⤳ c d

of d = natTrdegFiber f x immediate specializations inside X_{f x}, avoiding W, whose last term is a closed point of X_{f x}.

theorem exists_chain_isImmediateSpecialization_isClosed_fiber
    (f : X ⟶ S) [LocallyOfFiniteType f] (x : X)
    {W : Set (f.fiber (f x))} (hW : IsClosed W) (hxW : f.asFiber x ∉ W) :
    ∃ c : Fin (natTrdegFiber f x + 1) → f.fiber (f x),
      c 0 = f.asFiber x ∧
      (∀ i : Fin (natTrdegFiber f x),
        IsImmediateSpecialization (c i.castSucc) (c i.succ)) ∧
      IsClosed ({c (Fin.last (natTrdegFiber f x))} : Set (f.fiber (f x))) ∧
      ∀ i, c i ∉ W

AlgebraicGeometry.natTrdegFiber_eq_topologicalKrullDim_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/SpecializationChainInFibre.lean, line 156. The attribute's comment: “the equality of d with the dimension of the closure of x in the fibre”.

Stacks 053V, the identity d = dim(closure of {x}), the closure being taken in the fibre X_{f x}.

theorem natTrdegFiber_eq_topologicalKrullDim_closure (f : X ⟶ S) [LocallyOfFiniteType f]
    (x : X) :
    ((natTrdegFiber f x : ℕ∞) : WithBot ℕ∞) =
      topologicalKrullDim (closure ({f.asFiber x} : Set (f.fiber (f x))))

AlgebraicGeometry.natTrdegFiber_eq_toNat_trdeg_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/SpecializationChainInFibre.lean, line 239. The attribute's comment: “the equality of the length d of the chain with the transcendence degree trdeg_{κ(s)}(κ(x))”.

Stacks 053V, the identity d = trdeg_{κ(s)}(κ(x)): the integer produced by AlgebraicGeometry.natTrdegFiber is the transcendence degree of the residue field of X at x over the residue field of S at s = f x.

theorem natTrdegFiber_eq_toNat_trdeg_residueField (f : X ⟶ S) (x : X) :
    letI := (f.residueFieldMap x).hom.toAlgebra
    natTrdegFiber f x =
      Cardinal.toNat (Algebra.trdeg (S.residueField (f x)) (X.residueField x))

AlgebraicGeometry.exists_chain_isImmediateSpecialization_specializes_fiber_of_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/SpecializationChainToClosedSpecialization.lean, line 273. The attribute's comment: “the chain of immediate specializations inside the fibre, of length d, ending in a closed point of the fibre which specializes to the prescribed x' — unconditionally, the avoidance clause aside. The remark as a whole, avoidance clause included, is AlgebraicGeometry.exists_chain_isImmediateSpecialization_specializes_fiber_iff above, which states it at the hypotheses of the tag together with its exact range of validity”.

Stacks 053V without its avoidance clause, and with no hypothesis added to the tag. For f locally of finite type and x ⤳ x' with x' closed in its own fibre there is a chain

x = c 0 ⤳ c 1 ⤳ ⋯ ⤳ c d

of d = natTrdegFiber f x immediate specializations inside X_{f x} whose last term is a closed point of X_{f x} specializing to x'.

This needs no non-degeneracy hypothesis because the point to walk down to can be produced without Stacks 053U when x' already lies in the fibre of x: it is then x' itself. It is the avoidance clause that fails in that case, which is why the remark as a whole is registered on the equivalence AlgebraicGeometry.exists_chain_isImmediateSpecialization_specializes_fiber_iff above.

public theorem exists_chain_isImmediateSpecialization_specializes_fiber_of_isClosed
    (f : X ⟶ S) [LocallyOfFiniteType f] (x x' : X) (hxx' : x ⤳ x')
    (hx' : IsClosed ({f.asFiber x'} : Set (f.fiber (f x')))) :
    ∃ c : Fin (natTrdegFiber f x + 1) → f.fiber (f x),
      c 0 = f.asFiber x ∧
      (∀ i : Fin (natTrdegFiber f x),
        IsImmediateSpecialization (c i.castSucc) (c i.succ)) ∧
      IsClosed ({c (Fin.last (natTrdegFiber f x))} : Set (f.fiber (f x))) ∧
      f.fiberι (f x) (c (Fin.last (natTrdegFiber f x))) ⤳ x'

AlgebraicGeometry.exists_chain_isImmediateSpecialization_specializes_fiber_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Fibres/SpecializationChainToClosedSpecialization.lean, line 338. The attribute's comment: “EVERY assertion of the remark at once — the chain of d immediate specializations inside the fibre, its last term closed in the fibre, the final link x_d ⤳ x', the avoidance of any closed subset of the fibre which misses x, and d = natTrdegFiber f x — under the tag's own hypotheses, namely f locally of finite type, x ⤳ x' and x' closed in X_{f x'}, together with its exact range of validity: all of that holds if and only if x = x' or f x ≠ f x'. The reverse implication is the remark itself, by the argument of the source in exists_chain_isImmediateSpecialization_specializes_fiber; the forward implication disposes of the one remaining situation, a nontrivial specialization inside a single fibre, where {x'} is a closed subset of the fibre missing x which the last term of the chain cannot avoid, since a closed point specializing to x' is x'. That is the gap inherited from Stacks 053U, recorded there in closure_closedPoints_between_fiber_eq_iff, and respected by the source's own proof.”.

Stacks 053V, under the hypotheses of the tag and no others. Let f : X ⟶ S be locally of finite type, let x ⤳ x' be a specialization in X with x' closed in its own fibre X_{f x'}, and write d = natTrdegFiber f x. Then the remark holds — for every closed subset W of the fibre X_{f x} not containing x there is a chain

x = c 0 ⤳ c 1 ⤳ ⋯ ⤳ c d ⤳ x'

whose first d steps are immediate specializations inside X_{f x}, which avoids W, and whose last term c d is a closed point of X_{f x} — if and only if x = x' or f x ≠ f x'.

The reverse implication is the assertion of the remark and carries its mathematical content: it is AlgebraicGeometry.exists_chain_isImmediateSpecialization_specializes_fiber, which runs the argument of the source.

The forward implication settles the one remaining situation, a nontrivial specialization inside one fibre, where the remark fails. If f x = f x' then x' is a point z of X_{f x}, closed there, so {z} is a closed subset of X_{f x}; were x ≠ x' it would not contain x, hence would be a legitimate set to avoid, and the chain avoiding it would end in a point of X_{f x}, closed there, specializing to x' and different from z. But a point of a fibre closed in that fibre is the only point of the fibre it specializes to (AlgebraicGeometry.eq_of_fiberι_specializes_of_isClosed), so that last term is z after all. For X = 𝔸¹ over a field, x its generic point and x' a closed point, every hypothesis of the remark holds and its conclusion is therefore false. This is the gap inherited from Stacks 053U, whose density conclusion supplies the point to walk down to and which is stated with the same range of validity in AlgebraicGeometry.closure_closedPoints_between_fiber_eq_iff; the source's own proof draws the same line, at the prime-avoidance step (see the module docstring).

The closed set to be avoided is quantified inside the existence statement because that is where the source puts it: the points x_i can be chosen to avoid any closed subset of X_s not containing x. Fixing a single W instead would make the equivalence false, W = ∅ being avoided by a chain in every configuration.

public theorem exists_chain_isImmediateSpecialization_specializes_fiber_iff
    (f : X ⟶ S) [LocallyOfFiniteType f] (x x' : X) (hxx' : x ⤳ x')
    (hx' : IsClosed ({f.asFiber x'} : Set (f.fiber (f x')))) :
    (∀ W : Set (f.fiber (f x)), IsClosed W → f.asFiber x ∉ W →
        ∃ c : Fin (natTrdegFiber f x + 1) → f.fiber (f x),
          c 0 = f.asFiber x ∧
          (∀ i : Fin (natTrdegFiber f x),
            IsImmediateSpecialization (c i.castSucc) (c i.succ)) ∧
          IsClosed ({c (Fin.last (natTrdegFiber f x))} : Set (f.fiber (f x))) ∧
          f.fiberι (f x) (c (Fin.last (natTrdegFiber f x))) ⤳ x' ∧
          ∀ i, c i ∉ W) ↔
      x = x' ∨ f x ≠ f x'

Tag 05GT, a lemma

Tag 05GT in the Stacks Project.

Stacks.ClosedPointsFibre.exists_quotient_isLocalization_quasiFinite_of_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedPointsFibre/LocalRing.lean, line 55.

An open of the spectrum of an essentially finite type local algebra which meets the complement of the closed fibre contains a prime whose quotient is a localization of a quasi-finite algebra.

theorem exists_quotient_isLocalization_quasiFinite_of_isOpen
    {A B : Type u} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B]
    [IsNoetherianRing A]
    (f : A →+* B) (hf : IsLocalHom f)
    (heft : IsEssentiallyOfFiniteType A B f)
    (hres : letI : IsLocalHom f := hf;
      letI := (IsLocalRing.ResidueField.map f).toAlgebra;
      Module.Finite (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B))
    (V : Set (PrimeSpectrum B)) (hV : IsOpen V)
    (hne : ∃ q : PrimeSpectrum B,
      q ∈ V ∧ q.asIdeal.comap f ≠ IsLocalRing.maximalIdeal A) :
    ∃ q : PrimeSpectrum B, q ∈ V ∧
      q.asIdeal.comap f ≠ IsLocalRing.maximalIdeal A ∧
      letI := f.toAlgebra;
      ∃ (C : Type u) (_ : CommRing C) (_ : Algebra A C)
        (_ : Algebra.FiniteType A C) (_ : Algebra.QuasiFinite A C)
        (M : Submonoid C) (_ : Algebra C (B ⧸ q.asIdeal)),
        IsScalarTower A C (B ⧸ q.asIdeal) ∧ IsLocalization M (B ⧸ q.asIdeal)

Tag 05GU, a lemma

Tag 05GU in the Stacks Project.

Stacks.ClosedPointsFibre.exists_closedSubscheme_quasiFiniteAt_meeting_open, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedPointsFibre/ClosedSubscheme.lean, line 70.

Let f : X ⟶ S be locally of finite type with S locally Noetherian, and let x be closed in its fibre. If some point of the open U specializes to x and lies over a point other than f x, then there are a closed immersion i : Z ⟶ X and a point xZ of Z over x at which i ≫ f is quasi-finite, together with a generalization zZ of xZ mapping into U and lying over a point other than f x.

theorem exists_closedSubscheme_quasiFiniteAt_meeting_open
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (x : X) (U : X.Opens)
    (hx : IsClosed ({f.asFiber x} : Set (f.fiber (f x))))
    (hU : ∃ x' : X, x' ∈ U.1 ∧ x' ⤳ x ∧ f x' ≠ f x) :
    ∃ (Z : Scheme.{u}) (i : Z ⟶ X), IsClosedImmersion i ∧
      ∃ xZ : Z, i xZ = x ∧ quasiFiniteAt (i ≫ f) xZ ∧
        ∃ zZ : Z, i zZ ∈ U.1 ∧ zZ ⤳ xZ ∧ f (i zZ) ≠ f x

Tag 05GV, a remark

Tag 05GV in the Stacks Project.

AlgebraicGeometry.closure_closedPoints_between_fiber_eq_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedPointsFibre/DenseClosedPoints.lean, line 231. The attribute's comment: “the theorem the remark asserts, by the route it sketches; the hypothesis f x ≠ f x' (or x = x') is added, Stacks 053U being false without it”.

Stacks 053U for a locally Noetherian base. For f : X ⟶ S locally of finite type with S locally Noetherian, x ⤳ x' with x' closed in its fibre and f x ≠ f x' (or x = x'), the points of X_{f x} closed in X_{f x} and lying between x and x' are dense in the closure of x in X_{f x}.

public theorem closure_closedPoints_between_fiber_eq_of_isLocallyNoetherian {X S : Scheme.{u}}
    (f : X ⟶ S) [LocallyOfFiniteType f] [IsLocallyNoetherian S] (x x' : X) (hxx' : x ⤳ x')
    (hx' : IsClosed ({f.asFiber x'} : Set (f.fiber (f x'))))
    (hs : f x ≠ f x' ∨ x = x') :
    closure {y : f.fiber (f x) | IsClosed ({y} : Set (f.fiber (f x))) ∧
        x ⤳ f.fiberι (f x) y ∧ f.fiberι (f x) y ⤳ x'} =
      closure ({f.asFiber x} : Set (f.fiber (f x)))

Tag 05GW, a lemma

Tag 05GW in the Stacks Project.

Stacks.ClosedPointsFibre.exists_closedSubscheme_quasiFiniteAt_meeting_open_of_mem_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ClosedPointsFibre/ClosedSubscheme.lean, line 259.

Let f : X ⟶ S be locally of finite type with S locally Noetherian, and let x be closed in its fibre. If x lies in the closure of an open U no point of which lies over f x, then there are a closed immersion i : Z ⟶ X and a point xZ of Z over x at which i ≫ f is quasi-finite, together with a generalization zZ of xZ mapping into U and lying over a point other than f x.

theorem exists_closedSubscheme_quasiFiniteAt_meeting_open_of_mem_closure
    {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    [IsLocallyNoetherian S] (x : X) (U : X.Opens)
    (hx : IsClosed ({f.asFiber x} : Set (f.fiber (f x))))
    (hU : ∀ y : X, y ∈ U.1 → f y ≠ f x)
    (hclosure : x ∈ closure (U.1 : Set X)) :
    ∃ (Z : Scheme.{u}) (i : Z ⟶ X), IsClosedImmersion i ∧
      ∃ xZ : Z, i xZ = x ∧ quasiFiniteAt (i ≫ f) xZ ∧
        ∃ zZ : Z, i zZ ∈ U.1 ∧ zZ ⤳ xZ ∧ f (i zZ) ≠ f x

Sources

LeanStacks.Divisors.fiber_support_eq_union_irreducibleComponents_general · Stacks.Divisors.fiber_support_eq_union_irreducibleComponents · IsLocalRing.injective_quotient_of_dimension_add_trdeg_eq · IsLocalRing.ringKrullDim_closedFiber_add_trdeg_eq_trdeg · AlgebraicGeometry.closure_closedPoints_between_fiber_eq_iff · AlgebraicGeometry.exists_chain_isImmediateSpecialization_isClosed_fiber · AlgebraicGeometry.natTrdegFiber_eq_topologicalKrullDim_closure · AlgebraicGeometry.natTrdegFiber_eq_toNat_trdeg_residueField

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

37.46 Application to morphisms… to 37.52 Closed points in fibres

Section37.46 Application to morphisms with connected fibres#

Tag 057I, a lemma

Tag 055W, a lemma

Tag 0EY5, a lemma

Tag 057J, a lemma

Sources

Section37.47 Application to the structure of finite type morphisms#

Tag 052E, a lemma

Tag 057K, a lemma

Tag 057L, a lemma

Tag 05B8, a lemma

Sources

Section37.48 Application to the fppf topology#

Tag 0DET, a lemma

Tag 05WN, a lemma

Tag 0CNX, a lemma

Tag 0CNY, a lemma

Tag 0CNZ, a lemma

Tag 0CP0, a lemma

Tag 0DBT, a lemma

Tag 0DBU, a remark

Sources

Section37.49 Quasi-projective schemes#

Tag 0B42, a lemma

Tag 0B43, a lemma

Tag 0EJY, a lemma

Sources

Section37.50 Projective schemes#

Tag 0B44, the section

Tag 0B45, a lemma

Tag 0B46, a lemma

Tag 0D2S, a lemma

Sources

Section37.51 Proj and Spec#

Tag 0EKF, the section

Tag 0EKG, an equation

Tag 0EKH, an equation

Tag 0EKI, a lemma

Sources

Section37.52 Closed points in fibres#

Tag 053R, a lemma

Tag 053S, a lemma

Tag 053T, a lemma

Tag 053U, a lemma

Tag 053V, a remark

Tag 05GT, a lemma

Tag 05GU, a lemma

Tag 05GV, a remark

Tag 05GW, a lemma

Sources

Section37.46 Application to morphisms with connected fibres #

Section37.47 Application to the structure of finite type morphisms #

Section37.48 Application to the fppf topology #

Section37.49 Quasi-projective schemes #

Section37.50 Projective schemes #

Section37.51 Proj and Spec #

Section37.52 Closed points in fibres #