28.23 Extending quasi-coherent… to 28.30 Finding suitable affine…

Section28.23 Extending quasi-coherent sheaves#

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

Tag 01PE, a lemma

Tag 01PE in the Stacks Project.

AlgebraicGeometry.exists_quasicoherent_restrict_iso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/OpenExtension.lean, line 58. The attribute's comment: “extend_quasicoherent”. References: EGA I (1.4.2).

Stacks Project, Tag 01PE. A quasi-coherent module on a quasi-compact open subscheme extends to a quasi-coherent module on the ambient scheme: the pushforward along the open immersion is quasi-coherent, and its restriction is isomorphic to the given module.

public lemma exists_quasicoherent_restrict_iso {U X : Scheme.{u}} (j : U ⟶ X)
    [IsOpenImmersion j] [QuasiCompact j] (G : U.Modules) [G.IsQuasicoherent] :
    ∃ (F : X.Modules) (_ : F.IsQuasicoherent), Nonempty (F.restrict j ≅ G)

AlgebraicGeometry.exists_quasicoherent_extension, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionsAndBounds/QuasiCoherentExtension.lean, line 111. The attribute's comment: “extend_quasicoherent_morphism”.

Stacks Project, Tag 01PE. A morphism from a quasi-coherent module on a quasi-compact open subscheme to the restriction of a quasi-coherent module extends to a morphism of quasi-coherent modules on the whole scheme.

lemma exists_quasicoherent_extension
    {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j]
    (F : X.Modules) [F.IsQuasicoherent]
    (G : U.Modules) [G.IsQuasicoherent] (φ : G ⟶ F.restrict j) :
    ∃ (H : X.Modules) (_ : H.IsQuasicoherent)
      (ψ : H ⟶ F) (e : H.restrict j ≅ G),
      e.hom ≫ φ = (Scheme.Modules.restrictFunctor j).map ψ

AlgebraicGeometry.exists_quasicoherentSubobject_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionsAndBounds/QuasiCoherentExtension.lean, line 142. The attribute's comment: “extend_quasicoherent_subsheaf”.

Stacks Project, Tag 01PE. A quasi-coherent submodule of the restriction of a quasi-coherent module to a quasi-compact open subscheme extends to a quasi-coherent submodule of the ambient module.

theorem exists_quasicoherentSubobject_restrict {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j]
    (F : X.Modules) [F.IsQuasicoherent]
    (G : Subobject (F.restrict j)) (hG : (G : U.Modules).IsQuasicoherent) :
    ∃ H : Subobject F, (H : X.Modules).IsQuasicoherent ∧
      ∃ e : (H : X.Modules).restrict j ≅ (G : U.Modules),
        e.hom ≫ G.arrow = (restrictFunctor j).map H.arrow

Tag 01PF, a lemma

Tag 01PF in the Stacks Project.

Stacks.AlgebraicGeometry.Tag01PFAffineExtend.exists_isFiniteType_submodule_restrictTo_eq_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineExtend/Induction.lean, line 209. References: EGA I (9.4.6), “qcqs case”; EGA I (9.4.3), “qcqs scheme”; EGA I (9.4.7), “(b)”.

Stacks Project, Tag 01PF. Let X be a quasi-compact and quasi-separated scheme, let U ⊆ X be a quasi-compact open, let F be a quasi-coherent 𝒪_X-module and let G ⊆ F|_U be a quasi-coherent 𝒪_U-submodule which is of finite type. Then there exists a quasi-coherent submodule G' ⊆ F which is of finite type such that G'|_U = G.

theorem exists_isFiniteType_submodule_restrictTo_eq_of_qcqs
    [CompactSpace X] [QuasiSeparatedSpace X] [F.IsQuasicoherent]
    {U : X.Opens} (hU : IsCompact (U : Set X)) (G : (F.restrict U.ι).Submodule)
    (hqc : (G.toSheafOfModules : U.toScheme.Modules).IsQuasicoherent)
    (hft : (G.toSheafOfModules : U.toScheme.Modules).IsFiniteType) :
    ∃ N : F.Submodule, (N.toSheafOfModules : X.Modules).IsQuasicoherent ∧
      (N.toSheafOfModules : X.Modules).IsFiniteType ∧ restrictTo U.ι N = G

AlgebraicGeometry.exists_finiteTypeQuasicoherentSubobject_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionsAndBounds/FiniteTypeSubobjectExtension.lean, line 442. References: EGA I (9.4.6), “qcqs case”; EGA I (9.4.3), “qcqs scheme”; EGA I (9.4.7), “(b)”.

Let X be a quasi-compact quasi-separated scheme, F a quasi-coherent 𝒪_X-module, U a quasi-compact open and G a quasi-coherent subobject of F|_U of finite type. Then G extends to a quasi-coherent subobject of F of finite type: there is a quasi-coherent subobject G' of F of finite type and an isomorphism of G'|_U with G compatible with the inclusions into F|_U.

theorem exists_finiteTypeQuasicoherentSubobject_extension
    {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (F : X.Modules) [F.IsQuasicoherent]
    (U : X.Opens) (hU : IsCompact U.1)
    (G : CategoryTheory.Subobject (F.restrict U.ι))
    [(G : U.toScheme.Modules).IsQuasicoherent]
    [(G : U.toScheme.Modules).IsFiniteType] :
    ∃ (G' : CategoryTheory.Subobject F), (G' : X.Modules).IsQuasicoherent ∧
      (G' : X.Modules).IsFiniteType ∧
      ∃ e : (G' : X.Modules).restrict U.ι ≅ (G : U.toScheme.Modules),
        (Scheme.Modules.restrictFunctor U.ι).map G'.arrow = e.hom ≫ G.arrow

Tag 01PG, a lemma

Tag 01PG in the Stacks Project.

Stacks.AlgebraicGeometry.Tag01PGColimitClose.isColimit_finiteTypeQuasicoherentSubobjectCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ColimitClose/Basic.lean, line 203. The attribute's comment: “colimit”.

Stacks Project, Tag 01PG (colimit). On a quasi-compact and quasi-separated scheme, a quasi-coherent module is the colimit of the canonical diagram of all its quasi-coherent finite type submodules.

def isColimit_finiteTypeQuasicoherentSubobjectCocone {X : Scheme.{u}} (F : X.Modules)
    [CompactSpace X] [QuasiSeparatedSpace X] [F.IsQuasicoherent] :
    Limits.IsColimit (finiteTypeQuasicoherentSubobjectCocone F)

AlgebraicGeometry.isColimit_finiteTypeQuasicoherentSubobjectCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionsAndBounds/FiniteTypeSubobjectColimit.lean, line 223. References: EGA I (9.4.9), “quasi-compact scheme”.

Stacks Project, Tag 01PG. On a quasi-compact and quasi-separated scheme, a quasi-coherent module is the colimit of the canonical diagram of all its quasi-coherent finite type submodules.

This is the colimit half of the tag; the other half, that the diagram is filtered — so that the colimit is a directed one — is AlgebraicGeometry.finiteTypeQuasicoherentSubobject_isFiltered. Together the two are the tag's assertion, so the tag is attached to both.

noncomputable def isColimit_finiteTypeQuasicoherentSubobjectCocone
    {X : Scheme.{u}} (F : X.Modules)
    [CompactSpace X] [QuasiSeparatedSpace X] [F.IsQuasicoherent] :
    IsColimit (finiteTypeQuasicoherentSubobjectCocone F)

AlgebraicGeometry.finiteTypeQuasicoherentSubobject_isFiltered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ResolutionsAndBounds/FiniteTypeSubobjects.lean, line 159.

Stacks Project, Tag 01PG. The category of quasi-coherent finite type submodules of a quasi-coherent module is filtered.

This is the directedness half of the tag; the other half, that the canonical cocone over this diagram is a colimit cocone, is AlgebraicGeometry.isColimit_finiteTypeQuasicoherentSubobjectCocone. Together the two are the tag's assertion that a quasi-coherent module is the directed colimit of its quasi-coherent submodules of finite type, so the tag is attached to both.

instance finiteTypeQuasicoherentSubobject_isFiltered {X : Scheme.{u}} (F : X.Modules)
    [F.IsQuasicoherent] :
    IsFiltered (FiniteTypeQuasicoherentSubobject F)

Declarations registered for the tag:

• AlgebraicGeometry.finiteTypeQuasicoherentSubobject_isFiltered, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/AffineSubsheaf/Directedness.lean, line 53 (StacksFrontier): “directedness”.

Tag 01PI, a lemma

Tag 01PI in the Stacks Project.

AlgebraicGeometry.exists_finitePresentation_extension_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/FinitePresentationExtension.lean, line 560. References: EGA I (9.4.8), “special case”.

Stacks Project, Tag 01PI. Extension of a finitely presented module from a quasi-compact open. Let X be a quasi-compact, quasi-separated scheme, U a quasi-compact open, F a quasi-coherent 𝒪_X-module and φ : G ⟶ F|_U a morphism from a finitely presented 𝒪_U-module. Then φ is the restriction of a morphism G' ⟶ F from a finitely presented 𝒪_X-module G' restricting to G.

theorem exists_finitePresentation_extension_of_hom [CompactSpace X] [QuasiSeparatedSpace X]
    (F : X.Modules) [F.IsQuasicoherent] (U : X.Opens) (hU : IsCompact U.1)
    (G : U.toScheme.Modules) [G.IsFinitePresentation] (φ : G ⟶ F.restrict U.ι) :
    ∃ (G' : X.Modules) (_ : G'.IsFinitePresentation)
      (φ' : G' ⟶ F) (e : G'.restrict U.ι ≅ G),
      e.hom ≫ φ = (restrictFunctor U.ι).map φ'

Tag 0G41, a lemma

Tag 0G41 in the Stacks Project.

AlgebraicGeometry.exists_finiteTypeQuasicoherent_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ExtendFiniteType/Basic.lean, line 47. The attribute's comment: “(1)”. References: EGA I (9.4.8); EGA I (9.4.5).

Stacks Project, Tag 0G41 (1). Let X be a quasi-compact and quasi-separated scheme and let U ⊆ X be a quasi-compact open. A quasi-coherent 𝒪_U-module of finite type extends to a quasi-coherent 𝒪_X-module of finite type.

theorem exists_finiteTypeQuasicoherent_extension
    {X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (U : X.Opens) (hU : IsCompact U.1)
    (G : U.toScheme.Modules) [G.IsQuasicoherent] [G.IsFiniteType] :
    ∃ (G' : X.Modules) (_ : G'.IsQuasicoherent) (_ : G'.IsFiniteType),
      Nonempty (G'.restrict U.ι ≅ G)

AlgebraicGeometry.exists_extension_of_isQuasicoherent_isFiniteType, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Extend/Finiteness.lean, line 48. The attribute's comment: “part (1)”. References: EGA I (9.4.8); EGA I (9.4.5).

A quasi-coherent module of finite type on a quasi-compact open of a quasi-compact and quasi-separated scheme extends to a quasi-coherent module of finite type on the whole scheme.

lemma exists_extension_of_isQuasicoherent_isFiniteType {X : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X] (U : X.Opens) (hU : IsCompact U.1)
    (G : U.toScheme.Modules) [G.IsQuasicoherent] [G.IsFiniteType] :
    ∃ (G' : X.Modules) (_ : G'.IsQuasicoherent) (_ : G'.IsFiniteType),
      Nonempty (G'.restrict U.ι ≅ G)

AlgebraicGeometry.exists_extension_of_isFinitePresentation, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Extend/Finiteness.lean, line 70. The attribute's comment: “part (2)”. References: EGA I (9.4.8), “special case”.

A finitely presented module on a quasi-compact open of a quasi-compact and quasi-separated scheme extends to a finitely presented module on the whole scheme.

lemma exists_extension_of_isFinitePresentation {X : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X] (U : X.Opens) (hU : IsCompact U.1)
    (G : U.toScheme.Modules) [G.IsFinitePresentation] :
    ∃ (G' : X.Modules) (_ : G'.IsFinitePresentation), Nonempty (G'.restrict U.ι ≅ G)

Tag 01PJ, a lemma

Tag 01PJ in the Stacks Project.

AlgebraicGeometry.exists_filtered_diagram_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/FinitePresentationColimit.lean, line 337.

A quasi-coherent module on a quasi-compact, quasi-separated scheme is a filtered colimit of finitely presented modules.

theorem exists_filtered_diagram_of_isFinitePresentation (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (F : X.Modules) [F.IsQuasicoherent] :
    ∃ (I : Type u) (inst : SmallCategory I),
      let _ := inst
      ∃ (_ : IsFiltered I) (D : CategoryTheory.Functor I X.Modules)
        (φ : NatTrans D ((Functor.const I).obj F)),
        (∀ i, (D.obj i).IsFinitePresentation) ∧
          Nonempty (IsColimit (Cocone.mk F φ))

Tag 01PK, a lemma

Tag 01PK in the Stacks Project.

AlgebraicGeometry.exists_directed_system_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/FinitePresentationColimit.lean, line 376.

A quasi-coherent module on a quasi-compact, quasi-separated scheme is a directed colimit of finitely presented modules.

theorem exists_directed_system_of_isFinitePresentation (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (F : X.Modules) [F.IsQuasicoherent] :
    ∃ (I : Type u) (_ : PartialOrder I) (_ : Nonempty I)
      (_ : IsDirected I (· ≤ ·)) (D : I ⥤ X.Modules)
      (φ : D ⟶ (Functor.const I).obj F),
      (∀ i, (D.obj i).IsFinitePresentation) ∧
        Nonempty (IsColimit (Cocone.mk F φ))

Tag 086M, a lemma

Tag 086M in the Stacks Project.

AlgebraicGeometry.exists_directed_colimit_finitePresentation_with_epi_maps, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/FiniteTypeSubobjectLimits/EpiTransitionMaps.lean, line 135. References: EGA IV (1.7.9), “I.9.6.5 clause”.

Stacks Project, Tag 086M. A finite type quasi-coherent module on a quasi-compact and quasi-separated scheme is a directed colimit of finitely presented modules with surjective transition maps.

theorem exists_directed_colimit_finitePresentation_with_epi_maps
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (M : X.Modules) [M.IsQuasicoherent] [M.IsFiniteType] :
    ∃ (ι : Type u) (_ : PartialOrder ι) (_ : Nonempty ι) (_ : IsDirected ι (· ≤ ·))
      (F : ι ⥤ X.Modules) (_e : colimit F ≅ M),
      (∀ i, (F.obj i).IsFinitePresentation) ∧
        ∀ ⦃i j : ι⦄ (h : i ≤ j), Epi (F.map (homOfLE h))

Tag 080V, a lemma

Tag 080V in the Stacks Project.

AlgebraicGeometry.exists_finitePresentation_epi_isIso_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/FinitePresentationColimit.lean, line 422.

Let F be a quasi-coherent module of finite type on a quasi-compact, quasi-separated scheme X whose restriction to a quasi-compact open U is of finite presentation. Then there is a morphism φ : G ⟶ F with G of finite presentation, φ surjective, and φ|_U an isomorphism.

theorem exists_finitePresentation_epi_isIso_restrict [CompactSpace X] [QuasiSeparatedSpace X]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType] (U : X.Opens) (hU : IsCompact U.1)
    [(F.restrict U.ι).IsFinitePresentation] :
    ∃ (G : X.Modules) (_ : G.IsFinitePresentation) (φ : G ⟶ F),
      Epi φ ∧ IsIso ((Scheme.Modules.restrictFunctor U.ι).map φ)

Tag 05JS, a lemma

Tag 05JS in the Stacks Project.

Stacks.QcohAlgebraFPColimit.exists_directedSystem_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QcohAlgebraFPColimit/Main.lean, line 57.

Let X be a quasi-compact and quasi-separated scheme and let 𝒜 be a quasi-coherent sheaf of commutative 𝒪_X-algebras. Then there are a directed set I, a system (𝒜ᵢ, φᵢᵢ') over I of 𝒪_X-algebras and morphisms φᵢ : 𝒜ᵢ ⟶ 𝒜 with each 𝒜ᵢ quasi-coherent of finite presentation, such that the φᵢ induce an isomorphism colim 𝒜ᵢ ≅ 𝒜.

theorem exists_directedSystem_of_isFinitePresentation (X : Scheme.{u}) [CompactSpace ↥X]
    [QuasiSeparatedSpace ↥X] (A : X.QuasicoherentAlgebra)
    (hA : Scheme.QuasicoherentAlgebra.IsQuasicoherent A) :
    ∃ (I : Type (u + 1)) (_ : PartialOrder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (F : Functor I X.QuasicoherentAlgebra) (φ : F ⟶ (Functor.const I).obj A),
      (∀ i, Scheme.QuasicoherentAlgebra.IsQuasicoherent (F.obj i) ∧
        Scheme.QuasicoherentAlgebra.IsOfFinitePresentation (F.obj i)) ∧
        Nonempty (IsColimit (Cocone.mk A φ))

Tag 05JT, a lemma

Tag 05JT in the Stacks Project.

Stacks.AlgebraicGeometry.FiniteTypeSubalgebraFiltered.isFiltered_finiteTypeSubalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteTypeSubalgebraFiltered/Basic.lean, line 56. The attribute's comment: “directedness”.

The finite type quasi-coherent subalgebras of a quasi-coherent sheaf of commutative 𝒪_X-algebras form a filtered category. No hypothesis on X is needed.

An upper bound of two subalgebras is the image of the morphism to A out of the pushed-forward structure sheaf of the fibre product of their relative spectra, and the category is nonempty because it contains the image of the initial algebra sheaf 𝒪_X.

theorem isFiltered_finiteTypeSubalgebra {X : Scheme.{u}} (A : AlgebraSheaf X)
    (hA : AlgebraSheaf.IsQuasicoherent A) :
    IsFiltered (FiniteTypeSubalgebras.FiniteTypeSubalgebra A)

Stacks.AlgebraicGeometry.FiniteTypeSubalgebraFiltered.nonempty_isColimit_finiteTypeSubalgebraCocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteTypeSubalgebraFiltered/Basic.lean, line 84. The attribute's comment: “the colimit”. References: EGA I (9.6.6), “partial”.

On a quasi-compact and quasi-separated scheme, a quasi-coherent sheaf of commutative 𝒪_X-algebras is the colimit of the canonical diagram of its finite type quasi-coherent subalgebras, with the inclusions of the subobjects as the structure morphisms.

The affine sections hypothesis of nonempty_isColimit_of_affineSections is Stacks.AlgebraicGeometry.SubalgebraGeneratedByModule.exists_finiteTypeSubalgebra_section: a section over an affine open lies in the subalgebra generated by a finite type quasi-coherent submodule.

theorem nonempty_isColimit_finiteTypeSubalgebraCocone {X : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X] (A : AlgebraSheaf X) (hA : AlgebraSheaf.IsQuasicoherent A) :
    Nonempty (IsColimit (FiniteTypeSubalgebras.finiteTypeSubalgebraCocone A))

Tag 086N, a lemma

Tag 086N in the Stacks Project.

Stacks.FiniteAlgebraLimitPresentation.exists_isColimit_finite_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteAlgebraLimitPresentation/Basic.lean, line 628.

Stacks Project, Tag 086N. On a quasi-compact and quasi-separated scheme, a finite quasi-coherent algebra is a directed colimit of finite and finitely presented quasi-coherent algebras whose transition maps are surjective.

theorem exists_isColimit_finite_finitePresentation (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (A : AlgebraSheaf X) (hAqc : A.IsQuasicoherent)
    (hAfin : A.IsFinite) :
    ∃ (I : Type (u + 1)) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (F : I ⥤ AlgebraSheaf X) (t : F ⟶ (Functor.const I).obj A)
      (_ : IsColimit (Cocone.mk A t)),
      (∀ i, (F.obj i).IsQuasicoherent ∧ (F.obj i).IsFinite ∧
        (F.obj i).IsFinitePresentation) ∧
        ∀ i j (h : i ≤ j), AlgebraSheaf.Hom.IsSurjective (F.map (homOfLE h))

Tag 0817, a lemma

Tag 0817 in the Stacks Project.

Stacks.AlgebraicGeometry.FiniteSubalgebras.isFiltered_finiteSubalgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteSubalgebra/Basic.lean, line 195. The attribute's comment: “part (1), the directedness assertion: the finite quasi-coherent subalgebras of an integral quasi-coherent algebra sheaf form a filtered category; no hypothesis on X”.

[Stacks, Tag 0817], the directedness assertion. The finite quasi-coherent subalgebras of an integral quasi-coherent sheaf of commutative 𝒪_X-algebras form a filtered category.

No hypothesis on X is used: not quasi-compactness, not quasi-separatedness, not Noetherian and not affineness. This is Stacks.AlgebraicGeometry.FiniteTypeSubalgebraFiltered.isFiltered_finiteTypeSubalgebra, which is unconditional, transported along equivFiniteTypeSubalgebra.

This is one of the two declarations covering part (1) of the tag; the other is nonempty_isColimit_finiteSubalgebraCocone.

theorem isFiltered_finiteSubalgebra (A : AlgebraSheaf X) (hAqc : AlgebraSheaf.IsQuasicoherent A)
    (hAint : A.IsIntegral) : IsFiltered (FiniteSubalgebra A)

Stacks.AlgebraicGeometry.FiniteSubalgebras.nonempty_isColimit_finiteSubalgebraCocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteSubalgebra/Basic.lean, line 262. The attribute's comment: “part (1), the colimit assertion: an integral quasi-coherent algebra sheaf is the colimit of its finite quasi-coherent subalgebras, for X quasi-compact and quasi-separated”.

Stacks Project, Tag 0817, the colimit assertion of part (1). On a quasi-compact and quasi-separated scheme an integral quasi-coherent sheaf of commutative 𝒪_X-algebras is the colimit of the canonical diagram of all its finite quasi-coherent subalgebras, with the inclusions of the subobjects as the structure morphisms.

For an integral algebra sheaf a finite type quasi-coherent subalgebra is finite ([Stacks, Tag 02JJ] on affine sections), so this is the tag 05JT form of the same statement, Stacks.AlgebraicGeometry.FiniteTypeSubalgebraFiltered's nonempty_isColimit_finiteTypeSubalgebraCocone, transported along equivFiniteTypeSubalgebra.

theorem nonempty_isColimit_finiteSubalgebraCocone [CompactSpace X] [QuasiSeparatedSpace X]
    (A : AlgebraSheaf X) (hAqc : AlgebraSheaf.IsQuasicoherent A) (hAint : A.IsIntegral) :
    Nonempty (IsColimit (finiteSubalgebraCocone A))

Stacks.AlgebraicGeometry.Tag0817PartTwo.exists_small_index_finite_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PartTwoResidue/Complete.lean, line 109. The attribute's comment: “part (2): A is a directed colimit of finite and finitely presented quasi-coherent algebras, for X quasi-compact and quasi-separated and A quasi-coherent and integral”.

Stacks Project, Tag 0817, part (2). On a quasi-compact and quasi-separated scheme an integral quasi-coherent sheaf of commutative 𝒪_X-algebras is a directed colimit, over a nonempty directed preorder in the universe of the scheme, of quasi-coherent 𝒪_X-algebras that are both finite and of finite presentation.

Part (1) of the tag writes A as the colimit of its finite quasi-coherent subalgebras, [Stacks, Tag 086N] writes each of those as a colimit of finite finitely presented ones, and the two colimits are spliced by Stacks.FinitelyPresentableComposition.exists_directed_index_algebraSheaf; its presentability hypothesis holds along these cocones by Stacks.AlgebraicGeometry.Tag0817Presentable.presentableAlong_of_isFinitePresentation.

theorem exists_small_index_finite_finitePresentation (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (A : AlgebraSheaf X) (hAqc : AlgebraSheaf.IsQuasicoherent A)
    (hAint : AlgebraSheaf.IsIntegral A) :
    ∃ (I : Type u) (_ : Preorder I) (_ : Nonempty I) (_ : IsDirected I (· ≤ ·))
      (F : I ⥤ AlgebraSheaf X) (t : F ⟶ (Functor.const I).obj A)
      (_ : IsColimit (Cocone.mk A t)),
      ∀ i, AlgebraSheaf.IsQuasicoherent (F.obj i) ∧ AlgebraSheaf.IsFinite (F.obj i) ∧
        AlgebraSheaf.IsFinitePresentation (F.obj i)

Sources

• Section 28.23, Tag 01PD
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_quasicoherent_restrict_iso · AlgebraicGeometry.exists_quasicoherent_extension · AlgebraicGeometry.exists_quasicoherentSubobject_restrict · Stacks.AlgebraicGeometry.Tag01PFAffineExtend.exists_isFiniteType_submodule_restrictTo_eq_of_qcqs · AlgebraicGeometry.exists_finiteTypeQuasicoherentSubobject_extension · Stacks.AlgebraicGeometry.Tag01PGColimitClose.isColimit_finiteTypeQuasicoherentSubobjectCocone · AlgebraicGeometry.isColimit_finiteTypeQuasicoherentSubobjectCocone · AlgebraicGeometry.finiteTypeQuasicoherentSubobject_isFiltered

Section28.24 Gabber's result#

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

Tag 077L, a definition

Tag 077L in the Stacks Project.

SheafOfModules.IsCardinalGenerated, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/CardinalGenerated.lean, line 41.

A sheaf of modules is κ-generated if it has local generating families indexed by types of cardinality at most κ.

abbrev IsCardinalGenerated {C : Type u'} [Category.{v} C]
    {J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
    [∀ X : C, HasWeakSheafify (J.over X) AddCommGrpCat.{u}]
    [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
    (M : SheafOfModules.{u} R) (κ : Cardinal.{u}) : Prop

Tag 077M, a lemma

Tag 077M in the Stacks Project.

AlgebraicGeometry.CardinalGenerated.essentiallySmall_isCardinalGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/CardinalGeneratedSmall.lean, line 597.

The κ-generated modules on a ringed space have a set of isomorphism classes.

theorem essentiallySmall_isCardinalGenerated (X : RingedSpace.{v, u})
    (κ : Cardinal.{v})
    [∀ U : Opens X, HasWeakSheafify
        ((Opens.grothendieckTopology X).over U) AddCommGrpCat.{v}]
    [∀ U : Opens X,
        ((Opens.grothendieckTopology X).over U).WEqualsLocallyBijective
          AddCommGrpCat.{v}]
    [(Opens.grothendieckTopology X).HasSheafCompose
      (forget₂ CommRingCat.{v} RingCat.{v})] :
    ObjectProperty.EssentiallySmall.{max u v}
      (fun M : SheafOfModules.{v}
          ((sheafCompose (Opens.grothendieckTopology X)
            (forget₂ CommRingCat.{v} RingCat.{v})).obj X.sheaf) ↦
        SheafOfModules.IsCardinalGenerated M κ)

Tag 077N, a lemma

Tag 077N in the Stacks Project.

Stacks.AlgebraicGeometry.CardinalGeneration.isColimit_cardinalGeneratedQuasicoherentSubobjectCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CardinalGeneratedColimit/Basic.lean, line 505. The attribute's comment: “colimit”.

Stacks 077N, the colimit assertion. Every quasi-coherent module on a scheme is the colimit of the canonical diagram of its quasi-coherent subobjects generated by at most cardinalBound X local sections.

public def isColimit_cardinalGeneratedQuasicoherentSubobjectCocone (X : Scheme.{u})
    (F : X.Modules) [F.IsQuasicoherent] :
    IsColimit (cardinalGeneratedQuasicoherentSubobjectCocone F (cardinalBound X))

Stacks.AlgebraicGeometry.CardinalGeneration.cardinalBound, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CardinalGeneration/Basic.lean, line 71. The attribute's comment: “cardinal”.

The cardinal attached to a scheme X in Gabber's theorem: the size X.size of X.

public def cardinalBound (X : Scheme.{u}) : Cardinal.{u}

Stacks.AlgebraicGeometry.CardinalGeneration.cardinalGeneratedQuasicoherentSubobject_isFiltered, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CardinalGeneration/GabberDirected.lean, line 337. The attribute's comment: “directedness”.

Stacks Project, Tag 077N. For the common cardinal bound of a scheme, the category of bounded quasi-coherent subobjects of every quasi-coherent module is filtered.

instance cardinalGeneratedQuasicoherentSubobject_isFiltered (X : Scheme.{u}) (F : X.Modules)
    [F.IsQuasicoherent] :
    IsFiltered (CardinalGeneratedQuasicoherentSubobject F (cardinalBound X))

Tag 077P, a proposition

Tag 077P in the Stacks Project.

AlgebraicGeometry.quasicoherentModules_abelian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/GabberResult/Abelian.lean, line 63. The attribute's comment: “grothendieck_qcoh”.

The category of quasi-coherent modules on a scheme is abelian.

noncomputable instance quasicoherentModules_abelian (X : Scheme.{u}) :
    Abelian (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory

AlgebraicGeometry.quasicoherentInclusion_isLeftAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/Basic.lean, line 45. The attribute's comment: “coherator_adjoint”. References: SGA 6 II (3.2).

The inclusion of quasi-coherent 𝒪_X-modules into all 𝒪_X-modules has a right adjoint, the coherator.

theorem quasicoherentInclusion_isLeftAdjoint (X : Scheme.{u}) :
    (SheafOfModules.isQuasicoherent X.ringCatSheaf).ι.IsLeftAdjoint

AlgebraicGeometry.quasicoherentModules_hasLimitsOfSize, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/Basic.lean, line 55. The attribute's comment: “all_limits”.

The category of quasi-coherent modules on a scheme has all limits.

instance quasicoherentModules_hasLimitsOfSize (X : Scheme.{u}) :
    HasLimitsOfSize.{u, u}
      (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory

AlgebraicGeometry.isIso_coheratorCounit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/Basic.lean, line 62. The attribute's comment: “coherator_counit”.

The counit of the coherator adjunction is an isomorphism at a quasi-coherent module.

theorem isIso_coheratorCounit_app (X : Scheme.{u}) (M : X.Modules) [M.IsQuasicoherent] :
    letI := quasicoherentInclusion_isLeftAdjoint X
    IsIso ((Adjunction.ofIsLeftAdjoint
      (SheafOfModules.isQuasicoherent X.ringCatSheaf).ι).counit.app M)

AlgebraicGeometry.quasicoherentModules_enoughInjectives, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/Basic.lean, line 72. The attribute's comment: “enough_injectives”. References: SGA 6 II (3.1), “more general”.

The category of quasi-coherent modules on a scheme has enough injectives.

instance quasicoherentModules_enoughInjectives (X : Scheme.{u}) :
    EnoughInjectives (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory

AlgebraicGeometry.quasicoherentModules_isGrothendieckAbelian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Coherator/Grothendieck.lean, line 136. The attribute's comment: “grothendieck_qcoh”.

The category of quasi-coherent modules on a scheme is Grothendieck abelian. This is the second assertion of [Stacks, Tag 077P]: the separator above together with the reduction AlgebraicGeometry.quasicoherentModules_isGrothendieckAbelian_of_hasSeparator.

instance quasicoherentModules_isGrothendieckAbelian (X : Scheme.{u}) :
    IsGrothendieckAbelian.{u}
      (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory

Sources

• Section 28.24, Tag 077K
• AxiomMath/Stacks at 5ed82d14

LeanSheafOfModules.IsCardinalGenerated · AlgebraicGeometry.CardinalGenerated.essentiallySmall_isCardinalGenerated · Stacks.AlgebraicGeometry.CardinalGeneration.isColimit_cardinalGeneratedQuasicoherentSubobjectCocone · Stacks.AlgebraicGeometry.CardinalGeneration.cardinalBound · Stacks.AlgebraicGeometry.CardinalGeneration.cardinalGeneratedQuasicoherentSubobject_isFiltered · AlgebraicGeometry.quasicoherentModules_abelian · AlgebraicGeometry.quasicoherentInclusion_isLeftAdjoint · AlgebraicGeometry.quasicoherentModules_hasLimitsOfSize

Section28.25 Sections with support in a closed subset#

Section 28.25 of the Stacks Project, Tag 07ZM. 7 tags here are carried by 22 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01PH, a lemma

Tag 01PH in the Stacks Project.

AlgebraicGeometry.exists_isFiniteType_idealSheafData_support_eq_compl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ExtendFiniteType/QuasiCompactOpenIdeal.lean, line 320. The attribute's comment: “(2) ⟹ (4)”.

A quasi-compact open of a quasi-compact quasi-separated scheme is the complement of the vanishing locus of a finite type quasi-coherent sheaf of ideals.

theorem exists_isFiniteType_idealSheafData_support_eq_compl
    [CompactSpace X] [QuasiSeparatedSpace X] (U : X.Opens) (hU : IsCompact (U : Set X)) :
    ∃ I : X.IdealSheafData, I.IsFiniteType ∧ (I.support : Set X) = (U : Set X)ᶜ

AlgebraicGeometry.isCompact_iff_exists_finset_affineOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ExtendFiniteType/RetrocompactOpen.lean, line 65. The attribute's comment: “(2) ↔ (3)”. References: EGA IV (1.8.1), “qc open ⟺ finite ∪ aff”.

An open of a scheme is quasi-compact exactly when it is a finite union of affine opens.

theorem isCompact_iff_exists_finset_affineOpens (U : X.Opens) :
    IsCompact (U : Set X) ↔ ∃ s : Finset X.affineOpens, U = s.sup fun V => (V : X.Opens)

AlgebraicGeometry.isCompact_of_isFiniteType_idealSheafData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ExtendFiniteType/RetrocompactOpen.lean, line 116. The attribute's comment: “(4) ⟹ (2)”.

An open subscheme of a quasi-compact scheme whose complement is the vanishing locus of a finite type quasi-coherent sheaf of ideals is quasi-compact.

theorem isCompact_of_isFiniteType_idealSheafData [CompactSpace X] (U : X.Opens)
    (I : X.IdealSheafData) (hI : I.IsFiniteType)
    (hsupp : (I.support : Set X) = (U : Set X)ᶜ) : IsCompact (U : Set X)

Declarations registered for the tag:

• QuasiSeparatedSpace.isRetrocompact_iff_isCompact registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Properties/ExtendFiniteType/RetrocompactOpen.lean, line 50 (StacksFrontier): “(1) ↔ (2)”. References: EGA 0 (9.1.6); SGA 3 VIA (2.6.3), “special case”.
• QuasiSeparatedSpace.isRetrocompact_iff_isCompact registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Sheaves/SectionsWithSupport/QuasiCompactOpenIdealSheaf.lean, line 36 (StacksFrontier): “retrocompact iff quasi-compact”. References: EGA 0 (9.1.6); SGA 3 VIA (2.6.3), “special case”.
• AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Sheaves/SectionsWithSupport/QuasiCompactOpenIdealSheaf.lean, line 38 (StacksFrontier): “quasi-compact iff finite union of affine opens”. References: EGA I (1.1.10), “more general”; EGA IV (1.8.1).

Tag 01PO, a lemma

Tag 01PO in the Stacks Project.

Stacks.AlgebraicGeometry.AnnihilatorQcoh.isAnnihilatorSubsheaf_sSup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AnnihilatorQcoh/Basic.lean, line 169. The attribute's comment: “the subsheaf”.

The subsheaf of [Stacks, Tag 01PO]: the largest submodule sheaf of F that I annihilates, and its sections. The supremum is taken in the complete lattice of submodule sheaves of F, and the conclusion unfolds to the statement that a section over U belongs to it exactly when every restriction of it is annihilated by the sections of I there.

That this supremum is the only submodule sheaf with those sections is IsAnnihilatorSubsheaf.unique, and isAnnihilatorSubsheaf_annihilatorSubmodule exhibits a second, explicit model of it. Neither quasi-coherence nor finiteness is used.

theorem isAnnihilatorSubsheaf_sSup
    (I : (SheafOfModules.unit.{u} X.ringCatSheaf).Submodule) (F : X.Modules) :
    IsAnnihilatorSubsheaf I F
      (sSup {N : F.Submodule | ∀ (U : X.Opens) (s : Γ(F, U)),
        s ∈ N.toSubmodule.obj (op U) →
          ∀ a : Γ(X, U), a ∈ I.toSubmodule.obj (op U) → a • s = 0})

Stacks.AlgebraicGeometry.AnnihilatorQcoh.IsAnnihilatorSubsheaf.mem_iff_of_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AnnihilatorQcoh/Basic.lean, line 345. The attribute's comment: “part (2)”.

Part (2) of [Stacks, Tag 01PO]. Over an affine open U, the sections of the annihilator subsheaf are exactly the sections of F annihilated by Γ(I, U); no restriction has to be tested.

theorem IsAnnihilatorSubsheaf.mem_iff_of_isAffineOpen {N : F.Submodule}
    (hN : IsAnnihilatorSubsheaf I F N) [I.toSheafOfModules.IsQuasicoherent]
    {U : X.Opens} (hU : IsAffineOpen U) (s : Γ(F, U)) :
    s ∈ N.toSubmodule.obj (op U) ↔
      ∀ a : Γ(X, U), a ∈ I.toSubmodule.obj (op U) → a • s = 0

Stacks.AlgebraicGeometry.AnnihilatorQcoh.IsAnnihilatorSubsheaf.isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AnnihilatorQcoh/Qcoh.lean, line 160. The attribute's comment: “part (1)”.

Part (1) of [Stacks, Tag 01PO]. The subsheaf of sections of a quasi-coherent module annihilated by a quasi-coherent ideal sheaf of finite type is quasi-coherent.

Such a subsheaf exists for every I and F (isAnnihilatorSubsheaf_annihilatorSubmodule) and is unique (IsAnnihilatorSubsheaf.unique), so the hypothesis hN is not a restriction.

theorem IsAnnihilatorSubsheaf.isQuasicoherent (hN : IsAnnihilatorSubsheaf I F N)
    [I.toSheafOfModules.IsQuasicoherent] [I.toSheafOfModules.IsFiniteType] [F.IsQuasicoherent] :
    N.toSheafOfModules.IsQuasicoherent

Stacks.AlgebraicGeometry.AnnihilatorQcoh.IsAnnihilatorSubsheaf.exists_stalk_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AnnihilatorQcoh/Stalk.lean, line 172. The attribute's comment: “part (3)”.

Part (3) of [Stacks, Tag 01PO]. A germ of F at x lies in the image of the stalk of the annihilator subsheaf exactly when every section of I over a neighbourhood of x annihilates every representative of that germ, to first order at x.

Quasi-coherence of F is not needed: the forward implication uses no hypothesis beyond the sheaf axiom, and the backward one goes through the affine description of the sections of N, which needs only I.

theorem IsAnnihilatorSubsheaf.exists_stalk_eq_iff (hN : IsAnnihilatorSubsheaf I F N)
    [I.toSheafOfModules.IsQuasicoherent] [I.toSheafOfModules.IsFiniteType]
    (x : X) (s : F.presheaf.stalk x) :
    (∃ t : (Scheme.Modules.presheaf N.toSheafOfModules).stalk x,
        (TopCat.Presheaf.stalkFunctor Ab.{u} x).map
          (Scheme.Modules.Hom.mapPresheaf N.ι) t = s) ↔
      ∀ (U : X.Opens) (hx : x ∈ U) (t : Γ(F, U)), F.presheaf.germ U x hx t = s →
        ∀ r : Γ(X, U), r ∈ I.toSubmodule.obj (op U) →
          F.presheaf.germ U x hx (r • t) = 0

Stacks.AlgebraicGeometry.IdealPowerColimit.isQuasicoherent_idealAnnihilator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/AnnihilatorQuasicoherent.lean, line 314. The attribute's comment: “(1)”.

[Stacks, Tag 01PO] (1). For a quasi-coherent sheaf of ideals I of finite type on a scheme and a quasi-coherent 𝒪_X-module F, the subsheaf of sections annihilated by I is quasi-coherent.

Assertion (2) of the tag is mem_idealAnnihilator_affineOpen below. Assertion (3), the description of the stalks, is not proved, so this is a clause tag.

theorem isQuasicoherent_idealAnnihilator (I : X.IdealSheafData) (F : X.Modules)
    [F.IsQuasicoherent] (hFG : ∀ U : X.affineOpens, (I.ideal U).FG) :
    (idealPowerAnnihilator I.unitSubmodule F 1).toSheafOfModules.IsQuasicoherent

Stacks.AlgebraicGeometry.IdealPowerColimit.mem_idealAnnihilator_affineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/AnnihilatorQuasicoherent.lean, line 326. The attribute's comment: “(2)”.

[Stacks, Tag 01PO] (2). On an affine open U the subsheaf of sections annihilated by I consists of the sections of F over U annihilated by I(U).

No finiteness hypothesis is needed for this half: it is mem_idealPowerAnnihilator_affineOpen at n = 1, and idealPower_unitSubmodule_one identifies the ideal sheaf being annihilated with I rather than its first power.

theorem mem_idealAnnihilator_affineOpen (I : X.IdealSheafData) (F : X.Modules)
    (V : X.affineOpens) (s : Γ(F, V.1)) :
    s ∈ (idealPowerAnnihilator I.unitSubmodule F 1).toSubmodule.obj (op V.1) ↔
      ∀ a ∈ (I.ideal V : Ideal Γ(X, V.1)), a • s = 0

AlgebraicGeometry.mem_annihilatorSubsheaf_iff, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Extend/IdealAnnihilator.lean, line 138. The attribute's comment: “the subsheaf”.

Membership in the annihilator subsheaf means that, on every smaller open, every section of the ideal annihilates the restricted section.

lemma mem_annihilatorSubsheaf_iff [Mono i] (U : X.Opens) (s : Γ(F, U)) :
    s ∈ (annihilatorSubsheaf I F i).toSubmodule.obj (op U) ↔
      ∀ (V : X.Opens) (f : V ⟶ U) (r : Γ(I, V)),
        (show Γ(X, V) from i.app V r) • F.presheaf.map f.op s = 0

AlgebraicGeometry.mem_annihilatorSubsheaf_iff_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Extend/IdealAnnihilatorQuasicoherent.lean, line 327. The attribute's comment: “part (2)”.

Stacks, Tag 01PO (2). On an affine open it suffices to test annihilation by the sections of the ideal over that open itself.

theorem mem_annihilatorSubsheaf_iff_of_isAffine [I.IsQuasicoherent] (U : X.affineOpens)
    (s : Γ(F, U.1)) :
    s ∈ (annihilatorSubsheaf I F i).toSubmodule.obj (op U.1) ↔
      ∀ r : Γ(I, U.1), (show Γ(X, U.1) from i.app U.1 r) • s = 0

AlgebraicGeometry.annihilatorSubsheaf_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Extend/IdealAnnihilatorQuasicoherent.lean, line 415. The attribute's comment: “part (1)”.

Stacks, Tag 01PO (1). The subsheaf of sections annihilated by a quasi-coherent ideal sheaf of finite type is quasi-coherent.

theorem annihilatorSubsheaf_isQuasicoherent [I.IsQuasicoherent] [I.IsFiniteType]
    [F.IsQuasicoherent] :
    (annihilatorSubsheaf I F i).toSheafOfModules.IsQuasicoherent

AlgebraicGeometry.mem_range_stalk_annihilatorSubsheaf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Extend/IdealAnnihilatorQuasicoherent.lean, line 509. The attribute's comment: “part (3)”.

Stacks, Tag 01PO (3). The germs of the annihilator subsheaf at a point are exactly the germs of F annihilated by the stalk of the ideal.

theorem mem_range_stalk_annihilatorSubsheaf_iff [I.IsQuasicoherent] [I.IsFiniteType]
    [F.IsQuasicoherent] (x : X) (s : F.presheaf.stalk x) :
    (∃ t : (Scheme.Modules.presheaf (annihilatorSubsheaf I F i).toSheafOfModules).stalk x,
      ((TopCat.Presheaf.stalkFunctor Ab x).map
        (Scheme.Modules.Hom.mapPresheaf (annihilatorSubsheaf I F i).ι)).hom t = s) ↔
      ∀ (U : X.Opens) (hx : x ∈ U) (t : Γ(F, U)), F.presheaf.germ U x hx t = s →
        ∀ r : Γ(I, U), F.presheaf.germ U x hx ((show Γ(X, U) from i.app U r) • t) = 0

Tag 01PP, a definition

Tag 01PP in the Stacks Project.

AlgebraicGeometry.annihilatorSubsheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Extend/IdealAnnihilator.lean, line 129. The attribute's comment: “the subsheaf of sections annihilated by I”.

The subsheaf of F whose sections are annihilated by the ideal sheaf I: the largest submodule all of whose sections are killed by the sections of I over the same open.

noncomputable def annihilatorSubsheaf [Mono i] : F.Submodule

Tag 07ZN, a lemma

Tag 07ZN in the Stacks Project.

AlgebraicGeometry.pushforward_annihilatorSubsheaf_range_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/Extend/IdealAnnihilatorPushforward.lean, line 322.

Stacks Project, Tag 07ZN. Pushing forward the annihilator of the extended ideal gives the annihilator of the original ideal, as subobjects of the pushed-forward module.

theorem pushforward_annihilatorSubsheaf_range_eq
    {X Y : Scheme.{u}} (f : X ⟶ Y) (I : Y.Modules)
    (i : I ⟶ SheafOfModules.unit Y.ringCatSheaf) [Mono i]
    (F : X.Modules) (U : Y.Opens) :
    Set.range (((Scheme.Modules.pushforward f).map
      (annihilatorSubsheaf
        (extendedIdealSheaf f I i) F
        (extendedIdealSheafι f I i)).ι).app U) =
    Set.range (((annihilatorSubsheaf I
      ((Scheme.Modules.pushforward f).obj F) i).ι).val.app (op U))

Tag 07ZP, a lemma

Tag 07ZP in the Stacks Project.

AlgebraicGeometry.supportedSectionsSubmodule_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/SupportedSections/Basic.lean, line 82. The attribute's comment: “supported_sections_is_quasicoherent”.

The subsheaf of sections supported on a closed subset with retrocompact complement is quasicoherent.

public theorem supportedSectionsSubmodule_isQuasicoherent {X : Scheme.{u}} (Z : Set X)
    (hZ : IsClosed Z) (hZc : IsRetrocompact Zᶜ) (F : X.Modules) [F.IsQuasicoherent] :
    (AlgebraicGeometry.Scheme.Modules.supportedSectionsSubmodule Z
      F).toSheafOfModules.IsQuasicoherent

AlgebraicGeometry.mem_supportedSectionsSubmodule_iff_exists_pow_le_annihilator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/SupportedSections/Basic.lean, line 171. The attribute's comment: “the supported sections over an affine open are the ideal-power torsion”.

Stacks 07ZP, the torsion description of the supported sections. Let Z be a subset of a scheme X, let U be an affine open and let I ⊆ 𝒪_X(U) be a finitely generated ideal whose zero locus meets U in Z. A section of a quasi-coherent 𝒪_X-module over U has all its germs outside Z equal to zero exactly when some power of I annihilates it.

Such an I exists for every closed Z with retrocompact complement, by AlgebraicGeometry.exists_fg_ideal_zeroLocus_eq_inter; so the two together are the tag's description of the sections of the supported-section subsheaf over an affine open.

theorem mem_supportedSectionsSubmodule_iff_exists_pow_le_annihilator {X : Scheme.{u}}
    (Z : Set X) (F : X.Modules) [F.IsQuasicoherent] {U : X.Opens} (hU : IsAffineOpen U)
    {I : Ideal Γ(X, U)} (hIfg : I.FG)
    (hI : Z ∩ (U : Set X) = X.zeroLocus (U := U) (I : Set Γ(X, U)) ∩ (U : Set X))
    (s : Γ(F, U)) :
    s ∈ (supportedSectionsSubmodule Z F).toSubmodule.obj (op U) ↔
      ∃ n : ℕ, ∀ a ∈ I ^ n, a • s = 0

AlgebraicGeometry.exists_fg_ideal_zeroLocus_eq_inter, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/ClosedSubsetIdeal.lean, line 35. The attribute's comment: “finite_ideal_for_closed_subset_on_affine”.

On an affine open of a scheme, a closed subset with retrocompact complement is the zero locus of a finitely generated ideal of the ring of sections.

lemma exists_fg_ideal_zeroLocus_eq_inter (X : Scheme.{u}) (Z : Set X)
    (hZ : IsClosed Z) (hZc : IsRetrocompact Zᶜ) (U : X.Opens) (hU : IsAffineOpen U) :
    ∃ I : Ideal Γ(X, U), I.FG ∧
      Z ∩ (U : Set X) = X.zeroLocus (U := U) I ∩ (U : Set X)

AlgebraicGeometry.mem_supportedSectionsSubmodule_zeroLocus_span_singleton_iff, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/StrictTransform/AffinePrincipalTorsion.lean, line 136. The attribute's comment: “the sections supported on V(a) are the a-power torsion”.

The sections supported on a principal zero locus are the torsion for the powers of its generator. A global section of a quasi-coherent module on Spec R has all its germs outside V(a) zero exactly when some power of a kills it.

This is the affine-open description of [Stacks, Tag 07ZP] at the ideal (a), which is finitely generated; the passage from a power of the ideal to a power of the element is Ideal.span_singleton_pow.

public lemma mem_supportedSectionsSubmodule_zeroLocus_span_singleton_iff
    (F : (Spec R).Modules) [F.IsQuasicoherent] (a : R) (s : Γ(F, ⊤)) :
    s ∈ (supportedSectionsSubmodule (principalZeroLocus R a) F).toSubmodule.obj (op ⊤) ↔
      ∃ n : ℕ, a ^ n • s = 0

Tag 084L, a definition

Tag 084L in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.supportedSectionsSubmodule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/SupportedSections.lean, line 66.

The sub-𝒪-module sheaf of F whose local sections have all their germs outside Z equal to zero.

public noncomputable def supportedSectionsSubmodule (Z : Set X)
    (F : X.Modules) : F.Submodule

AlgebraicGeometry.SheafOfModules.supportedSectionsSubmodule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/SupportedSubmodule.lean, line 64.

The submodule of sections of F supported on Z: its sections over an open U are the sections of F over U all of whose germs at points of U outside Z vanish.

public noncomputable def supportedSectionsSubmodule (Z : Set X)
    (F : _root_.SheafOfModules.{u} R) : F.Submodule

Tag 07ZQ, a lemma

Tag 07ZQ in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.range_pushforward_supportedSectionsSubmodule_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Modules/SupportedSectionsPushforward.lean, line 154.

The pushforward of the subsheaf supported over Z is the subsheaf of the pushforward supported on Z, as subobjects of the pushforward sheaf.

theorem range_pushforward_supportedSectionsSubmodule_eq
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    (Z : Set Y) (hZ : IsClosed Z) (F : X.Modules) (U : Y.Opens) :
    Set.range (((Scheme.Modules.pushforward f).map
      (supportedSectionsSubmodule (f.base ⁻¹' Z) F).ι).app U) =
      Set.range (((supportedSectionsSubmodule Z
      ((Scheme.Modules.pushforward f).obj F)).ι).val.app (op U))

Sources

• Section 28.25, Tag 07ZM
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_isFiniteType_idealSheafData_support_eq_compl · AlgebraicGeometry.isCompact_iff_exists_finset_affineOpens · AlgebraicGeometry.isCompact_of_isFiniteType_idealSheafData · QuasiSeparatedSpace.isRetrocompact_iff_isCompact · AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens · Stacks.AlgebraicGeometry.AnnihilatorQcoh.isAnnihilatorSubsheaf_sSup · Stacks.AlgebraicGeometry.AnnihilatorQcoh.IsAnnihilatorSubsheaf.mem_iff_of_isAffineOpen · Stacks.AlgebraicGeometry.AnnihilatorQcoh.IsAnnihilatorSubsheaf.isQuasicoherent

Section28.26 Sections of quasi-coherent sheaves#

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

Tag 01PM, a lemma

Tag 01PM in the Stacks Project.

Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSectionsData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealPowerSections/Basic.lean, line 370. The attribute's comment: “canonical_map”.

Stacks Project, Tag 01PM (canonical_map). The canonical map colim_n Hom_A(I ^ n, M) → Γ(Spec(A) \ V(I), M̃).

public noncomputable def canonicalMapToSectionsData : CanonicalMapToSectionsData A I M

Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealPowerSections/Basic.lean, line 389. The attribute's comment: “canonical_map”.

The canonical map, with its local evaluation rule supplied by the construction.

public noncomputable def canonicalMapToSections :
    colimit (idealPowersHom A I M) ⟶ sectionsOnComplement A I M

Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections_restrict_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealPowerSections/Basic.lean, line 396. The attribute's comment: “canonical_map”.

On every basic open D(f) with f ∈ I, a colimit representative φ has image φ(fⁿ)/fⁿ.

public theorem canonicalMapToSections_restrict_ι (n : ℕ)
    (φ : (I ^ n : Ideal A) →ₗ[A] M) (f : A) (hf : f ∈ I) :
    restrictToBasicOpen A I M f hf
      (canonicalMapToSections A I M (colimit.ι (idealPowersHom A I M) n φ)) =
        basicOpenFraction A M f n (φ ⟨f ^ n, Ideal.pow_mem_pow hf n⟩)

Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections_injective_of_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealPowerSections/Basic.lean, line 481. The attribute's comment: “injective”.

Stacks Project, Tag 01PM (injective). The canonical map colim_n Hom_A(I ^ n, M) → Γ(Spec(A) \ V(I), M̃) is injective when I is finitely generated.

public theorem canonicalMapToSections_injective_of_fg (hI : I.FG) :
    Function.Injective (canonicalMapToSections A I M)

Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealPowerSections/Surjectivity.lean, line 693. The attribute's comment: “surjectivity when no nonzero element of M is annihilated by I”.

Surjectivity in the torsion-free case. If I is finitely generated and annihilates no nonzero element of M, the canonical map colim_n Hom_A(I ^ n, M) ⟶ Γ(Spec(A) \ V(I), M̃) is surjective.

public theorem canonicalMapToSections_surjective (hI : I.FG)
    (hM : ∀ y : M, (∀ a ∈ I, a • y = 0) → y = 0) :
    Function.Surjective (canonicalMapToSections A I M)

Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealPowerSectionsComparison/Basic.lean, line 169. The attribute's comment: “injectivity”.

For a finitely generated ideal I the canonical map colim_n Hom_A(I ^ n, M) → Γ(Spec(A) \ V(I), M̃) is injective.

public theorem canonicalMapToSections_injective (hI : I.FG) :
    Function.Injective (canonicalMapToSections A I M)

Stacks.AlgebraicGeometry.IdealPowerSections.isIso_canonicalMapToSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealPowerSectionsSurjective/Basic.lean, line 253. The attribute's comment: “torsionfree_isomorphism”.

Stacks Project, Tag 01PM (torsionfree_isomorphism). Let I be a finitely generated ideal of A. If no nonzero element of M is annihilated by all of I, then the canonical map colim_n Hom_A(I ^ n, M) → Γ(Spec(A) \ V(I), M̃) is an isomorphism.

The hypothesis is the vanishing of Submodule.torsionBySet A M I, the submodule of elements annihilated by every element of I; in the source it is used exactly to see that all of the submodules Mₙ vanish, so that the general isomorphism of [Stacks, Tag 01PM] reduces to the canonical map itself.

public theorem isIso_canonicalMapToSections (hI : I.FG)
    (hM : Submodule.torsionBySet A M (I : Ideal A) = ⊥) :
    IsIso (canonicalMapToSections A I M)

Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapModuloAnnihilator_bijective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/IdealPowerQuotientIso.lean, line 981. The attribute's comment: “general_isomorphism”.

Stacks Project, Tag 01PM (general_isomorphism). For a finitely generated ideal I the canonical map from the direct limit of Hom_A(I ^ n, M / Mₙ) to the sections of M̃ on Spec(A) \ V(I) is bijective.

public lemma canonicalMapModuloAnnihilator_bijective (hI : I.FG) :
    Function.Bijective (canonicalMapModuloAnnihilator A I M)

Stacks.AlgebraicGeometry.IdealPowerSections.idealPowersHomModuloAnnihilatorColimitIsoSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/IdealPowerQuotientIso.lean, line 990. The attribute's comment: “general_isomorphism”.

Stacks Project, Tag 01PM (general_isomorphism). For a finitely generated ideal I, the direct limit of Hom_A(I ^ n, M / Mₙ) is canonically isomorphic to the sections of M̃ on Spec(A) \ V(I).

public noncomputable def idealPowersHomModuloAnnihilatorColimitIsoSections (hI : I.FG) :
    colimit (idealPowersHomModuloAnnihilator A I M) ≅ sectionsOnComplement A I M

Declarations registered for the tag:

• Submodule.torsionBySet registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Properties/IdealPowerTorsion.lean, line 30 (StacksFrontier): “i_power_annihilator_submodules”.

Tag 01PN, an example

Tag 01PN in the Stacks Project.

Stacks.AlgebraicGeometry.PrincipalIdealCounterexample.fractionSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PrincipalIdealCounterexample.lean, line 282. The attribute's comment: “first example: the section y/x on Spec(A) minus V(x), A = k[x,y,z_n]/(x^n z_n)”.

The fraction y/x, as a section of 𝒪 on the complement of V(x).

noncomputable def fractionSection :
    sectionsOnComplement (counterexampleRing k) (principalIdeal k) (counterexampleRing k)

Stacks.AlgebraicGeometry.PrincipalIdealCounterexample.fractionSection_restrict, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PrincipalIdealCounterexample.lean, line 290. The attribute's comment: “first example: that section restricts on D(x) to the fraction y/x”.

On D(x), which is all of the complement of V(x), the section is the fraction y/x.

lemma fractionSection_restrict :
    restrictToBasicOpen (counterexampleRing k) (principalIdeal k) (counterexampleRing k)
        (x k) (x_mem_principalIdeal k) (fractionSection k) =
      basicOpenFraction (counterexampleRing k) (counterexampleRing k) (x k) 1 (y k)

Stacks.AlgebraicGeometry.PrincipalIdealCounterexample.fractionSection_not_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PrincipalIdealCounterexample.lean, line 299. The attribute's comment: “first example: y/x is not in the range of the map from colim_n Hom_A((x)^n, A)”.

The fraction y/x is not obtained from a map out of any power of (x).

theorem fractionSection_not_mem_range :
    fractionSection k ∉ Set.range (canonicalMapToSections (counterexampleRing k)
      (principalIdeal k) (counterexampleRing k))

Stacks.AlgebraicGeometry.PrincipalIdealCounterexample.canonicalMapToSections_not_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PrincipalIdealCounterexample.lean, line 350. The attribute's comment: “first example: the canonical map for I = (x) is not surjective”.

The canonical map is not surjective for the principal ideal (x).

theorem canonicalMapToSections_not_surjective :
    ¬ Function.Surjective (canonicalMapToSections (counterexampleRing k)
      (principalIdeal k) (counterexampleRing k))

Stacks.AlgebraicGeometry.PrincipalIdealCounterexample.canonicalMapToSections_not_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PrincipalIdealCounterexample.lean, line 357. The attribute's comment: “first example: the canonical map for I = (x) is not an isomorphism”.

The canonical map is not an isomorphism for the principal ideal (x).

theorem canonicalMapToSections_not_isIso :
    ¬ IsIso (canonicalMapToSections (counterexampleRing k)
      (principalIdeal k) (counterexampleRing k))

Stacks.AlgebraicGeometry.TwoGeneratorCounterexample.gluedFractionSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwoGeneratorCounterexample.lean, line 548. The attribute's comment: “two_generator_counterexample”.

The section on D(f) ∪ D(g) to which the fractions x/f and y/g glue.

noncomputable def gluedFractionSection :
    sectionsOnComplement (counterexampleRing k) (twoGeneratorIdeal k)
      (counterexampleRing k)

Stacks.AlgebraicGeometry.TwoGeneratorCounterexample.gluedFractionSection_f, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwoGeneratorCounterexample.lean, line 554. The attribute's comment: “two_generator_counterexample”.

f times the glued section is x, i.e. the section restricts to x/f on D(f).

theorem gluedFractionSection_f :
    f k • gluedFractionSection k =
      toComplement (counterexampleRing k) (twoGeneratorIdeal k)
        (counterexampleRing k) (x k)

Stacks.AlgebraicGeometry.TwoGeneratorCounterexample.gluedFractionSection_g, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwoGeneratorCounterexample.lean, line 561. The attribute's comment: “two_generator_counterexample”.

g times the glued section is y, i.e. the section restricts to y/g on D(g).

theorem gluedFractionSection_g :
    g k • gluedFractionSection k =
      toComplement (counterexampleRing k) (twoGeneratorIdeal k)
        (counterexampleRing k) (y k)

Stacks.AlgebraicGeometry.TwoGeneratorCounterexample.gluedFractionSection_not_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwoGeneratorCounterexample.lean, line 672. The attribute's comment: “two_generator_counterexample”.

The glued fraction section is not obtained from a map out of any power of (f,g).

theorem gluedFractionSection_not_mem_range :
    gluedFractionSection k ∉ Set.range (canonicalMapToSections (counterexampleRing k)
      (twoGeneratorIdeal k) (counterexampleRing k))

Stacks.AlgebraicGeometry.TwoGeneratorCounterexample.canonicalMapToSections_not_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwoGeneratorCounterexample.lean, line 743. The attribute's comment: “two_generator_counterexample”.

The canonical map is not an isomorphism for the ideal (f,g).

theorem canonicalMapToSections_not_isIso :
    ¬ IsIso (canonicalMapToSections (counterexampleRing k)
      (twoGeneratorIdeal k) (counterexampleRing k))

Tag 01PQ, a lemma

Tag 01PQ in the Stacks Project.

Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/Injectivity.lean, line 449. The attribute's comment: “canonical_map”.

The canonical map colim_n Hom_{𝒪_X}(Iⁿ, F) ⟶ Γ(X \ V(I), F).

noncomputable def canonicalMapToSections (I : X.IdealSheafData) (F : X.Modules) :
    Limits.colimit (idealPowHomSystem I F) ⟶ Γ(F, (I.support.compl : X.Opens))

Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSections_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/Injectivity.lean, line 467. The attribute's comment: “injective: the FIRST display colim Hom(Iⁿ, F) → Γ(U, F) is injective; X quasi-compact, I quasi-coherent of finite type, F quasi-coherent. The second display is canonicalMapToSectionsQuotient_bijective”.

For a quasi-compact scheme X, a quasi-coherent sheaf of ideals I of finite type and a quasi-coherent 𝒪_X-module F, the canonical map colim_n Hom_{𝒪_X}(Iⁿ, F) → Γ(X \ V(I), F) is injective.

theorem canonicalMapToSections_injective [CompactSpace X] (I : X.IdealSheafData)
    (hFT : ∀ V : X.affineOpens, (I.ideal V).FG) (F : X.Modules) [F.IsQuasicoherent] :
    Function.Injective (canonicalMapToSections I F)

Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSectionsQuotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/QuotientColimit.lean, line 187. The attribute's comment: “canonical map of the second display, colim Hom(Iⁿ, F/F_n) → Γ(U, F)”.

The canonical map colim_n Hom_{𝒪_X}(Iⁿ, F/F_n) ⟶ Γ(X \ V(I), F), where F_n is the subsheaf of sections annihilated by Iⁿ, sending the class of φ to the section of F corresponding to φ(1).

noncomputable def canonicalMapToSectionsQuotient :
    Limits.colimit (idealPowHomQuotientSystem I F) ⟶ Γ(F, (I.support.compl : X.Opens))

Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSectionsQuotient_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/QuotientColimit.lean, line 204. The attribute's comment: “second display colim Hom(Iⁿ, F/F_n) → Γ(U, F) is injective; X quasi-compact, I of finite type; surjectivity is canonicalMapToSectionsQuotient_surjective”.

For a quasi-compact scheme X, a quasi-coherent sheaf of ideals I of finite type and a quasi-coherent 𝒪_X-module F, the canonical map colim_n Hom_{𝒪_X}(Iⁿ, F/F_n) → Γ(X \ V(I), F) is injective.

theorem canonicalMapToSectionsQuotient_injective [CompactSpace X] :
    Function.Injective (canonicalMapToSectionsQuotient I F hFG)

Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSectionsQuotient_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/QuotientSurjectivity.lean, line 208. The attribute's comment: “clause (c), surjectivity of the second display colim Hom(Iⁿ, F/F_n) → Γ(U, F); X quasi-compact and quasi-separated, I quasi-coherent of finite type, F quasi-coherent, F_n the subsheaf annihilated by Iⁿ. No torsion hypothesis.”.

Stacks Project, Tag 01PQ, second display, surjectivity. For a quasi-compact and quasi-separated scheme X, a quasi-coherent sheaf of ideals I of finite type and a quasi-coherent 𝒪_X-module F, the canonical map colim_n Hom_{𝒪_X}(Iⁿ, F/F_n) → Γ(X ∖ V(I), F) is surjective.

Quasi-separatedness of X is used exactly here, as in the source: it is what makes the pairwise intersections of a finite affine covering again finitely covered by affine opens, hence what bounds the exponent needed for the local morphisms to agree.

theorem canonicalMapToSectionsQuotient_surjective [CompactSpace X] [QuasiSeparatedSpace X]
    (I : X.IdealSheafData) (F : X.Modules) [F.IsQuasicoherent]
    (hFG : ∀ V : X.affineOpens, (I.ideal V).FG) :
    Function.Surjective (canonicalMapToSectionsQuotient I F hFG)

Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSectionsQuotient_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/QuotientSurjectivity.lean, line 231. The attribute's comment: “clause (c): the second display colim Hom(Iⁿ, F/F_n) → Γ(U, F) is an isomorphism; X quasi-compact and quasi-separated, I quasi-coherent of finite type, F quasi-coherent”.

Stacks Project, Tag 01PQ, clause (c). Let X be a quasi-compact and quasi-separated scheme, let I ⊂ 𝒪_X be a quasi-coherent sheaf of ideals of finite type, let Z = V(I) and U = X ∖ Z, let F be a quasi-coherent 𝒪_X-module and let F_n ⊂ F be the subsheaf of sections annihilated by Iⁿ. Then the canonical map

colim_n Hom_{𝒪_X}(Iⁿ, F/F_n) ⟶ Γ(U, F)

is an isomorphism.

Injectivity is canonicalMapToSectionsQuotient_injective and needs only quasi-compactness; surjectivity is canonicalMapToSectionsQuotient_surjective and is where quasi-separatedness enters.

theorem canonicalMapToSectionsQuotient_bijective [CompactSpace X] [QuasiSeparatedSpace X]
    (I : X.IdealSheafData) (F : X.Modules) [F.IsQuasicoherent]
    (hFG : ∀ V : X.affineOpens, (I.ideal V).FG) :
    Function.Bijective (canonicalMapToSectionsQuotient I F hFG)

Stacks.AlgebraicGeometry.IdealPowerColimit.isIso_canonicalMapToSectionsQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/QuotientSurjectivity.lean, line 247. The attribute's comment: “clause (c): the second display colim Hom(Iⁿ, F/F_n) → Γ(U, F) is an isomorphism in AddCommGrpCat; X quasi-compact and quasi-separated, I quasi-coherent of finite type, F quasi-coherent”.

Stacks Project, Tag 01PQ, clause (c), categorically. The canonical map colim_n Hom_{𝒪_X}(Iⁿ, F/F_n) ⟶ Γ(X ∖ V(I), F) is an isomorphism of abelian groups, for X quasi-compact and quasi-separated, I quasi-coherent of finite type and F quasi-coherent.

This is canonicalMapToSectionsQuotient_bijective read in AddCommGrpCat, where a bijective morphism is invertible.

theorem isIso_canonicalMapToSectionsQuotient [CompactSpace X] [QuasiSeparatedSpace X]
    (I : X.IdealSheafData) (F : X.Modules) [F.IsQuasicoherent]
    (hFG : ∀ V : X.affineOpens, (I.ideal V).FG) :
    IsIso (canonicalMapToSectionsQuotient I F hFG)

Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSections_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/Surjectivity.lean, line 519. The attribute's comment: “surjective (F_n = 0)”.

Stacks Project, Tag 01PQ (surjective), the case F_N = 0. Let X be a quasi-compact scheme, let I be a quasi-coherent sheaf of ideals of finite type and let F be a quasi-coherent 𝒪_X-module with no I-power torsion, that is, with F_N = 0 for every N. Then the canonical map colim_n Hom_{𝒪_X}(Iⁿ, F) → Γ(X \ V(I), F) is surjective.

Together with canonicalMapToSections_injective this is the second assertion of Tag 01PQ in the case F_N = 0, where F/F_N = F; the general assertion, which needs the quotient sheaves F/F_N, is Stacks.AlgebraicGeometry.IdealPowerColimit.canonicalMapToSectionsQuotient_bijective of StacksFrontier/AlgebraicGeometry/Coherent/HomColimit/QuotientSurjectivity.lean. Note that quasi-separatedness of X is not needed for the torsion-free case proved here: the source glues the local morphisms over a finite cover of the pairwise intersections, whereas here the local sections to be glued are unique, by the absence of torsion, so no comparison over the intersections is required.

theorem canonicalMapToSections_surjective [CompactSpace X] (I : X.IdealSheafData)
    (hFT : ∀ V : X.affineOpens, (I.ideal V).FG) (F : X.Modules) [F.IsQuasicoherent]
    (hTF : NoIdealTorsion I F) :
    Function.Surjective (canonicalMapToSections I F)

Stacks.LocalCohomology.canonicalMapToSections_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/CanonicalSectionsInjective.lean, line 605. The attribute's comment: “injectivity”.

Stacks Project, Tag 01PQ (injectivity). The canonical map from the colimit of homomorphisms out of the powers of a finite-type ideal sheaf on a quasi-compact scheme to the sections of a quasi-coherent module on the complement of the support is injective.

public theorem canonicalMapToSections_injective {X : Scheme.{u}} [CompactSpace X]
    (I : X.IdealSheafData) (F : X.Modules) [F.IsQuasicoherent]
    [((idealPowerMultiple I 1 (unitModule X)).toModules).IsFiniteType] :
    Function.Injective (canonicalMapToSections I F).1

AlgebraicGeometry.idealPowerAnnihilator, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/IdealPowerAnnihilator.lean, line 159. The attribute's comment: “ideal_power_annihilator_subsheaf”.

The subsheaf of F whose local sections are annihilated by the n-th power of the ideal subsheaf I.

noncomputable def idealPowerAnnihilator
    (I : (SheafOfModules.unit.{u} X.ringCatSheaf).Submodule) (F : X.Modules) (n : ℕ) :
    F.Submodule

Sources

• Section 28.26, Tag 01PL
• AxiomMath/Stacks at 5ed82d14

LeanStacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSectionsData · Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections · Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections_restrict_ι · Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections_injective_of_fg · Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections_surjective · Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapToSections_injective · Stacks.AlgebraicGeometry.IdealPowerSections.isIso_canonicalMapToSections · Stacks.AlgebraicGeometry.IdealPowerSections.canonicalMapModuloAnnihilator_bijective

Section28.27 Ample invertible sheaves#

Section 28.27 of the Stacks Project, Tag 01PR. 15 tags here are carried by 54 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01PS, a definition

Tag 01PS in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.IsAmple, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Ample/Defs.lean, line 95. References: EGA II (4.5.3).

An invertible sheaf of modules on a scheme is ample if the scheme is quasi-compact and every point has an affine nonvanishing locus for some global section of a tensor power of positive exponent.

public def IsAmple : Prop

Tag 01PT, a lemma

Tag 01PT in the Stacks Project.

Stacks.AmplePositivePower.isAmple_iff_isAmple_tensorPowModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmplePositivePower/Basic.lean, line 72. References: EGA II (4.5.6), “(i)”.

An invertible 𝒪_X-module L is ample if and only if its tensor power L ^⊗ d is ample, for any d ≥ 1.

theorem isAmple_iff_isAmple_tensorPowModule (d : ℕ) (hd : 1 ≤ d) :
    IsAmple X L ↔ IsAmple X (tensorPowModule X L (d : ℤ))

AlgebraicGeometry.isAmple_iff_tensorPower_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AmpleAndExtension/TensorPower.lean, line 589. References: EGA II (4.5.6), “(i)”.

An invertible sheaf is ample if and only if any of its positive tensor powers is ample.

theorem isAmple_iff_tensorPower_isAmple (X : Scheme.{u}) (L : X.Modules)
    [SheafOfModules.IsInvertible X.toRingedSpace.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    (n : ℕ) (hn : 1 ≤ n) :
    Scheme.Modules.IsAmple X L ↔
    Scheme.Modules.IsAmple X
        (Invertible.tensorPower X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L (n : ℤ))

Tag 01PU, a lemma

Tag 01PU in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isAmple_pullback_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmplePullback/Affine.lean, line 108. References: EGA II (4.5.14), “necessity”; EGA II (4.5.13), “necessity”; EGA III (2.6.2.3), “special case”; EGA III (5.2.5), “Ampleness of L'_0 = L/JL”.

Stacks Project, Tag 01PU. The restriction of an ample invertible sheaf of modules to a closed subscheme is ample. The closed immersion is affine, and its source is quasi-compact because its target is.

public theorem isAmple_pullback_of_isClosedImmersion [IsClosedImmersion f] (h : IsAmple Y L) :
    IsAmple X ((Scheme.Modules.pullback f).obj L)

Tag 01PV, a lemma

Tag 01PV in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isAffineOpen_inf_nonvanishingOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineNonvanishing/Basic.lean, line 325. References: EGA II (5.5.8); SGA 6 II (2.2.3.1).

For an invertible module L on a scheme X and a global section s of L, every affine open U ⊆ X meets the nonvanishing locus X_s in an affine open.

public theorem isAffineOpen_inf_nonvanishingOpen {X : Scheme.{u}} (L : X.Modules)
    [Stacks.SheafOfModules.IsInvertible X.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    (s : L.sections) (U : X.Opens) (hU : IsAffineOpen U) :
    IsAffineOpen (U ⊓ nonvanishingOpen (X := X.toRingedSpace) L s)

Stacks.NonvanishingAffineIntersection.isAffineOpen_inf_nonvanishingOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/NonvanishingAffineIntersection/Basic.lean, line 122. References: EGA II (5.5.8); SGA 6 II (2.2.3.1).

Let X be a scheme, M an invertible 𝒪_X-module and s a global section of M. For every affine open U of X, the intersection U ∩ X_s of U with the nonvanishing locus of s is affine.

theorem isAffineOpen_inf_nonvanishingOpen {U : X.Opens} (hU : IsAffineOpen U) :
    IsAffineOpen (U ⊓ Stacks.NonvanishingOpen.nonvanishingOpen X M s)

Tag 0890, a lemma

Tag 0890 in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isAmple_tensor_of_power_sections_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorPowerProduct/Basic.lean, line 213. References: EGA II (4.5.6), “(ii)”.

Stacks Project, Tag 0890. Let L and M be invertible modules on a scheme X. If L is ample and the nonvanishing opens of the global sections of the positive tensor powers of M cover X, then L ⊗ M is ample.

At a point x, ampleness of L gives n ≥ 1 and s ∈ Γ(X, L^{⊗ n}) with x ∈ X_s and X_s affine, and the cover gives m ≥ 1 and t ∈ Γ(X, M^{⊗ m}) with x ∈ X_t. The section s^m ⊗ t^n of (L ⊗ M)^{⊗ nm}, read through tensorPowerProductIso, has nonvanishing open X_s ⊓ X_t, which contains x and is affine by Tag 01PV.

theorem isAmple_tensor_of_power_sections_cover (X : Scheme.{u}) (L M : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
      (structureSheafRing X.toRingedSpace).property L]
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.toRingedSpace.presheaf
      (structureSheafRing X.toRingedSpace).property M]
    (hL : IsAmple X L)
    (hcover : ∀ x : X, ∃ m : ℕ, 1 ≤ m ∧
      ∃ t : (tensorPower X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property M (m : ℤ)).sections,
        x ∈ nonvanishingOpen (X := X.toRingedSpace)
          (tensorPower X.toRingedSpace.presheaf
            (structureSheafRing X.toRingedSpace).property M (m : ℤ)) t) :
    IsAmple X (tensorProductModule X L M)

Tag 01PX, a lemma

Tag 01PX in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isBasis_affine_nonvanishingOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineNonvanishing/Basis.lean, line 59.

Stacks Project, Tag 01PX. If the nonvanishing opens of global sections of the positive tensor powers of an invertible sheaf form a basis of the topology, then the affine ones among them already form a basis.

public theorem isBasis_affine_nonvanishingOpens
    (hBasis : Opens.IsBasis
      {U : X.Opens | ∃ n : ℕ, 1 ≤ n ∧
        ∃ s : (tensorPower X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L (n : ℤ)).sections,
          U = nonvanishingOpen (X := X.toLocallyRingedSpace.toRingedSpace)
            (tensorPower X.toRingedSpace.presheaf
              (structureSheafRing X.toRingedSpace).property L (n : ℤ)) s}) :
    Opens.IsBasis
      {U : X.Opens | (∃ n : ℕ, 1 ≤ n ∧
        ∃ s : (tensorPower X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L (n : ℤ)).sections,
          U = nonvanishingOpen (X := X.toLocallyRingedSpace.toRingedSpace)
            (tensorPower X.toRingedSpace.presheaf
              (structureSheafRing X.toRingedSpace).property L (n : ℤ)) s) ∧
          IsAffineOpen U}

Tag 01PY, a lemma

Tag 01PY in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isSeparated_of_affine_nonvanishingOpen_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AffineNonvanishing/Separated.lean, line 351.

Stacks Project, Tag 01PY. A scheme carrying an invertible sheaf of modules such that every point lies in an affine nonvanishing open of a global section of some positive tensor power is separated.

public theorem isSeparated_of_affine_nonvanishingOpen_cover
    (h : ∀ x : X, ∃ n : ℕ, 1 ≤ n ∧
      ∃ s : (tensorPower X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property L (n : ℤ)).sections,
        x ∈ nonvanishingOpen (X := X.toLocallyRingedSpace.toRingedSpace)
          (tensorPower X.toRingedSpace.presheaf
            (structureSheafRing X.toRingedSpace).property L (n : ℤ)) s ∧
        IsAffineOpen (nonvanishingOpen (X := X.toLocallyRingedSpace.toRingedSpace)
          (tensorPower X.toRingedSpace.presheaf
            (structureSheafRing X.toRingedSpace).property L (n : ℤ)) s)) :
    Scheme.IsSeparated X

Stacks.AmpleNonvanishing.isSeparated_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleNonvanishing/AmpleAffineDiagonal.lean, line 71. The attribute's comment: “at the predicate Stacks.Ample.IsAmple”.

A scheme carrying an ample invertible module is separated, at the predicate Stacks.Ample.IsAmple. This is [Stacks, Tag 01PY], available as AlgebraicGeometry.Scheme.Modules.IsAmple.isSeparated for the other of the two ampleness predicates of [Stacks, Tag 01PS], transported along the hypothesis-free Stacks.AmpleBridge.isAmple_iff_isAmple.

theorem isSeparated_of_isAmple (X : Scheme.{u}) (L : X.Modules) [IsInvertibleModule X L]
    (hL : IsAmple X L) : Scheme.IsSeparated X

AlgebraicGeometry.isSeparated_of_exists_affine_nonvanishingOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AmpleAndExtension/Separated.lean, line 295.

A scheme is separated as soon as every point lies in an affine nonvanishing open of a global section of some positive tensor power of an invertible sheaf.

theorem isSeparated_of_exists_affine_nonvanishingOpen
    (h : ∀ x : X, ∃ n : ℕ, 1 ≤ n ∧
      ∃ s : (Invertible.tensorPower X.toRingedSpace.presheaf
        (structureSheafRing X.toRingedSpace).property L (n : ℤ)).sections,
        x ∈ nonvanishingOpen (X := X.toRingedSpace)
            (Invertible.tensorPower X.toRingedSpace.presheaf
              (structureSheafRing X.toRingedSpace).property L (n : ℤ)) s ∧
          IsAffineOpen (nonvanishingOpen (X := X.toRingedSpace)
            (Invertible.tensorPower X.toRingedSpace.presheaf
              (structureSheafRing X.toRingedSpace).property L (n : ℤ)) s)) :
    Scheme.IsSeparated X

Tag 09MP, a lemma

Tag 09MP in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.IsAmple.isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AmpleAndExtension/Separated.lean, line 342.

A scheme carrying an ample invertible sheaf is separated.

theorem Scheme.Modules.IsAmple.isSeparated (hL : Scheme.Modules.IsAmple X L) :
    Scheme.IsSeparated X

Tag 01PZ, a lemma

Tag 01PZ in the Stacks Project.

Stacks.SectionRingProjMorphism.projHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjMorphism/Basic.lean, line 177.

The canonical morphism ⋃ X_a ⟶ Proj Γ_*(X, L) of Stacks Tag 01PZ. It is glued from the charts Stacks.SectionRingChartMap.chartHom over the cover of ⋃ X_a by the nonvanishing opens of the homogeneous elements of positive degree; the overlap condition is Stacks.SectionRingChartOpen.chartHomOn_eq, which says that the chart at a and the chart at b agree on X_a ∩ X_b.

For L ample the source is all of X (Stacks.SectionRingProjMorphism.projHomOfIsAmple); in general ⋃ X_a is the largest open on which the construction makes sense, and that is where the Stacks project's statement puts it as well.

public noncomputable def projHom : (nvUnion L).toScheme ⟶ Proj (grading L)

Stacks.SectionRingProjMorphism.homOfLE_projHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjMorphism/Basic.lean, line 203. The attribute's comment: “the restriction to a nonvanishing open is the chart”.

On X_a the canonical morphism is the chart at a. This is the second half of the characterisation of the morphism of Stacks Tag 01PZ, not one of the tag's numbered clauses. For a homogeneous of positive degree, the restriction of the canonical morphism to X_a is the morphism X_a ⟶ Proj Γ_*(X, L) determined by the degree-zero part of the localization of Γ_*(X, L) at a, namely Stacks.SectionRingChartMap.chartHom.

public theorem homOfLE_projHom {d : ℕ} (a : powSections L d) (hd : 0 < d) :
    X.homOfLE (nvOpen_le_nvUnion L a hd) ≫ projHom L
      = Stacks.SectionRingChartMap.chartHom L a hd

Stacks.SectionRingProjMorphism.projHom_preimage_projBasicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjMorphism/Basic.lean, line 216. The attribute's comment: “the preimage of a basic open”.

Clause (1) of Stacks Tag 01PZ: the preimage of a basic open. For every homogeneous element a of Γ_*(X, L) of positive degree, the canonical morphism pulls the chart D₊(a) of Proj Γ_*(X, L) back to the nonvanishing open X_a.

The identity is checked on the cover: on the piece X_b the composite is the chart at b, and Stacks.SectionRingChartOpen.chartHomOn_preimage_projBasicOpen computes its preimage of D₊(a) as X_b ∩ X_a, which is also what the right-hand side restricts to.

public theorem projHom_preimage_projBasicOpen {d : ℕ} (a : powSections L d) (hd : 0 < d) :
    projHom L ⁻¹ᵁ Proj.basicOpen (grading L) (DirectSum.of (powSections L) d a)
      = (nvUnion L).ι ⁻¹ᵁ nvOpen L a

Stacks.SectionRingProjMorphism.image_projHom_preimage_projBasicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjMorphism/Basic.lean, line 231. The attribute's comment: “the preimage of a basic open, as an open of X”.

Clause (1) of Stacks Tag 01PZ, read as an open of X. The image in X of the preimage of D₊(a) is the nonvanishing open X_a itself, which is the shape the Stacks project's statement takes.

public theorem image_projHom_preimage_projBasicOpen {d : ℕ} (a : powSections L d) (hd : 0 < d) :
    (nvUnion L).ι ''ᵁ
        (projHom L ⁻¹ᵁ Proj.basicOpen (grading L) (DirectSum.of (powSections L) d a))
      = nvOpen L a

Stacks.SectionRingProjMorphism.Theta.homOfLE_projHom_eq_glued, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjMorphism/Theta.lean, line 104. The attribute's comment: “the canonical morphism is the morphism r_{L,psi} of Tag 01NK at psi the identity map of the section ring, with no hypothesis on L; this is what the clauses below are clauses about”.

The canonical morphism Stacks.SectionRingProjMorphism.projHom is the morphism r_{L, ψ} of [Stacks, Tag 01NK] at ψ the identity map of Γ_*(X, L), with no hypothesis on L: the two morphisms have the same source U(ψ) = ⋃_a X_a (Stacks.SectionRingGluedComparison.coveringOpen_canonicalSections) and agree there.

theorem homOfLE_projHom_eq_glued :
    X.homOfLE (coveringOpen_canonicalSections L).le
        ≫ Stacks.SectionRingProjMorphism.projHom L
      = (canonicalSections L).glued

Stacks.SectionRingProjMorphism.Theta.glued_preimage_projBasicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjMorphism/Theta.lean, line 120. The attribute's comment: “clause (1): f^{-1}(D_+(s)) = X_s for every homogeneous s in S_+, for the morphism f = r_{L,psi} that clauses (2), (3) and (4) are stated at, as opens of its source U(psi)”.

f^{-1}(D₊(s)) = X_s for every homogeneous s ∈ S_+, where f is r_{L, ψ} at ψ the identity map of S = Γ_*(X, L). Both sides are opens of the source U(ψ) = ⋃_a X_a of f, the right-hand side being X_s, which lies inside it.

theorem glued_preimage_projBasicOpen {d : ℕ} (a : powSections L d) (hd : 0 < d) :
    (canonicalSections L).glued ⁻¹ᵁ
        AlgebraicGeometry.Proj.basicOpen (grading L) (DirectSum.of (powSections L) d a)
      = (canonicalSections L).coveringOpen.ι ⁻¹ᵁ nvOpen L a

Stacks.SectionRingProjMorphism.Theta.projTheta, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjMorphism/Theta.lean, line 140. The attribute's comment: “clause (2): the O_X-module maps f^*O_Y(n) -> L^{tensor n} for all n in Z, as a homomorphism of sheaves of Z-graded algebras, whose map_mul is their compatibility with the multiplication maps of Constructions Equation 01MO”.

The 𝒪_X-module maps f^*𝒪_Y(n) ⟶ L^{⊗ n}, compatible with the multiplication maps of Constructions, Equation 01MO. All degrees at once, as a homomorphism of sheaves of ℤ-graded 𝒪_X-algebras f^*(⨁_{n ∈ ℤ} 𝒪_Y(n)) ⟶ ⨁_{n ∈ ℤ} L^{⊗ n}: its component in degree n is the map f^*𝒪_Y(n) ⟶ L^{⊗ n}, and its map_mul field is exactly the compatibility, the multiplication maps of the two graded algebras being those of Equation 01MO on the source and the tensor product of sections on the target. It is θ of [Stacks, Tag 01NK] at ψ the identity map of Γ_*(X, L), taken along f = r_{L, ψ}.

def projTheta : SheafOfModules.GradedAlgebra.Hom
    (Stacks.Conormal.gradedPullback (canonicalSections L).glued
      (Stacks.AlgebraicGeometry.ProjConeTwist.integerTwistAlgebra (grading L)))
    (laurentRestrict (grading L) (canonicalSections L))

Stacks.SectionRingProjMorphism.Theta.projTheta_app_top_degreeSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjMorphism/Theta.lean, line 163. The attribute's comment: “clause (3): the composite S_d -> Gamma(Y, O_Y(d)) -> Gamma(X, L^{tensor d}) is the identity map, read on the open where the canonical morphism is defined”.

The composite S_d ⟶ Γ(Y, 𝒪_Y(d)) ⟶ Γ(X, L^{⊗ d}) is the identity map. For a homogeneous element z of S = Γ_*(X, L) of degree d, the first map sends z to the global section of 𝒪_Y(d) attached to it by [Stacks, Tag 01MP], the second pulls that back along f and applies the degree-d component of projTheta, and the result is z itself: the global section of L^{⊗ d} that the degree-d component z d of z names.

Both sides are sections of L^{⊗ d} over ⋃_a X_a, where f is defined, with L^{⊗ d} read in the family Stacks.AmpleProjectiveImmersion.tensorPowerModule and compared with the iterated tensor power by Stacks.AlgebraicGeometry.CoherentMulSections.powCompare.

theorem projTheta_app_top_degreeSection (d : ℕ) {z : sectionRing L} (hz : z ∈ grading L d) :
    ((projTheta L).app (d : ℤ)).val.app (op ⊤)
        (Scheme.Modules.pullbackSection (canonicalSections L).glued
          (twistM (grading L) (d : ℤ)) ⊤ ⊤ (fun _ _ => trivial)
          (degreeSection (grading L) d ⟨z, hz⟩))
      = resTop (tensorPowerModule X L (d : ℤ))
          ((powCompare L d).hom.app ⊤ (globalSection X (natTensorPow L d) (z d)))
          ((canonicalSections L).coveringOpen.ι ''ᵁ ⊤)

Stacks.SectionRingProjMorphism.Theta.exists_isIso_pullback_projTheta_app_intMul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjMorphism/ThetaIso.lean, line 484. The attribute's comment: “clause (4): every point of the open where the canonical morphism is defined has an integer d >= 1 and an open neighbourhood U of it on which f^*O_Y(dn) -> L^{tensor dn} is an isomorphism for all n in Z, positive, zero and negative; d is the degree of a homogeneous element of the section ring not vanishing at the point and U is the nonvanishing open of that element”.

Every point of ⋃_a X_a has an integer d ≥ 1 and an open neighbourhood U on which f^*𝒪_Y(d n)|_U ⟶ L^{⊗ d n}|_U is an isomorphism for all n ∈ ℤ.

theorem exists_isIso_pullback_projTheta_app_intMul {x : X}
    (hx : x ∈ (canonicalSections L).coveringOpen) :
    ∃ (e : ℕ) (_ : 0 < e) (V : X.Opens) (_ : x ∈ V) (hVU : V ≤ (canonicalSections L).coveringOpen),
      ∀ n : ℤ,
        IsIso ((Scheme.Modules.pullback (X.homOfLE hVU)).map
          ((projTheta L).app ((e : ℤ) * n)))

Tag 01Q0, a lemma

Tag 01Q0 in the Stacks Project.

Stacks.SectionRingProjQuasiCompact.quasiCompact_projHomOfCovers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjQuasiCompact/Basic.lean, line 220. The attribute's comment: “the canonical morphism of 01PZ is quasi-compact, under (a) the X_s cover X and (b) X quasi-compact”.

Stacks Tag 01Q0, the quasi-compactness. Under clause (a) of Stacks Tag 01PZ — the X_s cover X — and X quasi-compact, the canonical morphism f : X ⟶ Proj Γ_*(X, L) of Stacks Tag 01PZ is quasi-compact.

Proj of any graded ring is quasi-separated (Stacks.AlgebraicGeometry.ProjQuasiSeparated.quasiSeparatedSpace_proj), so this is AlgebraicGeometry.quasiCompact_of_compactSpace, which is Stacks Tag 01KO.

theorem quasiCompact_projHomOfCovers [CompactSpace X]
    (hcov : Stacks.SectionRingProjMorphism.nvUnion L = ⊤) :
    QuasiCompact (Stacks.SectionRingProjMorphism.projHomOfCovers L hcov)

Stacks.SectionRingProjQuasiCompact.denseRange_projHomOfCovers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjQuasiCompact/Basic.lean, line 233. The attribute's comment: “the canonical morphism of 01PZ has dense image, under (a) the X_s cover X and (b) X quasi-compact”.

Stacks Tag 01Q0, the dense image. Under clause (a) of Stacks Tag 01PZ — the X_s cover X — and X quasi-compact, the canonical morphism f : X ⟶ Proj Γ_*(X, L) of Stacks Tag 01PZ has dense image.

A nonempty open of Proj Γ_*(X, L) missing the image would contain a nonempty D₊(a) with a homogeneous of positive degree, whose preimage X_a would then be empty; but then a is nilpotent and D₊(a) = ∅.

theorem denseRange_projHomOfCovers [CompactSpace X]
    (hcov : Stacks.SectionRingProjMorphism.nvUnion L = ⊤) :
    DenseRange (Stacks.SectionRingProjMorphism.projHomOfCovers L hcov).base

Tag 01Q1, a lemma

Tag 01Q1 in the Stacks Project.

Stacks.SectionRingProjImmersion.isOpenImmersion_projHomOfIsAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjImmersion/Basic.lean, line 141. The attribute's comment: “open immersion”. References: EGA II (4.5.2), “partial”.

Stacks Tag 01Q1, the open immersion. For L an ample invertible 𝒪_X-module, the canonical morphism X ⟶ Proj Γ_*(X, L) of Stacks Tag 01PZ is an open immersion.

theorem isOpenImmersion_projHomOfIsAmple (hL : IsAmple X L) :
    IsOpenImmersion (Stacks.SectionRingProjMorphism.projHomOfIsAmple L hL)

Stacks.SectionRingProjImmersion.denseRange_projHomOfIsAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjImmersion/Basic.lean, line 166. The attribute's comment: “dense image”.

Stacks Tag 01Q1, the dense image. For L an ample invertible 𝒪_X-module, the canonical morphism X ⟶ Proj Γ_*(X, L) of Stacks Tag 01PZ has dense image.

This is Stacks Tag 01Q0 (Stacks.SectionRingProjQuasiCompact.denseRange_projHomOfCovers), which the source cites here: ampleness gives both of that tag's hypotheses, that the X_s cover X (Stacks.SectionRingProjMorphism.nvUnion_eq_top_of_isAmple) and that X is quasi-compact.

theorem denseRange_projHomOfIsAmple (hL : IsAmple X L) :
    DenseRange (Stacks.SectionRingProjMorphism.projHomOfIsAmple L hL).base

Tag 01Q2, a lemma

Tag 01Q2 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjAmpleTwist.exists_isAmple_pullback_twistingSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AmpleProjOpenImmersion.lean, line 208. References: EGA II (8.14.4), “invertible for some d”.

Stacks Project, Tag 01Q2. Let X be a quasi-compact scheme and S a graded ring, and assume there is an open immersion j : X ⟶ Proj(S). Then j^* 𝒪(d) is an invertible ample 𝒪_X-module for some d > 0.

theorem exists_isAmple_pullback_twistingSheaf {X : Scheme.{u}} [CompactSpace X]
    (j : X ⟶ AlgebraicGeometry.Proj 𝒮) [IsOpenImmersion j] :
    ∃ d : ℕ, 0 < d ∧ ∃ h : IsInvertibleModule X
        ((modulePullback j.toLRSHom.toShHom).obj (twistingSheaf 𝒮 (d : ℤ))),
      @IsAmple X ((modulePullback j.toLRSHom.toShHom).obj (twistingSheaf 𝒮 (d : ℤ))) h

Tag 01Q3, a proposition

Tag 01Q3 in the Stacks Project.

Stacks.AmpleCharacterization.exists_nvUnion_eq_top_and_isOpenImmersion_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/Basic.lean, line 129. The attribute's comment: “clause (2)”. References: EGA II (4.5.2), “(a) ⇒ (a'')”.

Clause (2) of [Stacks, Tag 01Q3] — the clause labelled 01Q5: for L ample the open sets X_s, with s ∈ S₊ homogeneous, cover X, and the associated morphism X ⟶ Proj S is an open immersion.

The covering is Stacks.SectionRingProjMorphism.nvUnion_eq_top_of_isAmple; it is also what makes the morphism Stacks.SectionRingProjMorphism.projHomOfCovers of Stacks Tag 01PZ exist at all. The open immersion is Stacks Tag 01Q1, Stacks.SectionRingProjImmersion.isOpenImmersion_projHomOfIsAmple.

theorem exists_nvUnion_eq_top_and_isOpenImmersion_of_isAmple (hL : IsAmple X L) :
    ∃ h : Stacks.SectionRingProjMorphism.nvUnion L = ⊤,
      IsOpenImmersion (Stacks.SectionRingProjMorphism.projHomOfCovers L h)

Stacks.AmpleCharacterization.isAmple_of_isOpenImmersion_projHomOfCovers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/Basic.lean, line 145. The attribute's comment: “clause (2) implies (1)”. References: EGA II (4.5.2), “(a) ⇐ (a'')”.

Clause (2) of [Stacks, Tag 01Q3] implies clause (1). If the opens X_s cover the quasi-compact scheme X and the resulting morphism j : X ⟶ Proj Γ_*(X, L) is an open immersion, then L is ample.

This is the source's implication (2) ⇒ (4) ⇒ (1) in one step: the basic opens D₊(a) of the homogeneous elements of positive degree are a basis of Proj S and are affine, so every point of X has one of them around its image inside the (open) range of j; its preimage is X_a, is affine because j is an open immersion, and contains the point. That is clause (1) of Stacks Tag 01PS verbatim.

theorem isAmple_of_isOpenImmersion_projHomOfCovers [CompactSpace X]
    (h : Stacks.SectionRingProjMorphism.nvUnion L = ⊤)
    (hj : IsOpenImmersion (Stacks.SectionRingProjMorphism.projHomOfCovers L h)) :
    IsAmple X L

Stacks.AmpleCharacterization.isAmple_of_isBasisNonvanishing_and_isBasisAffineNonvanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/Basic.lean, line 188. The attribute's comment: “(3) and (4) imply (1)”. References: EGA II (4.5.2), “(a) ⇐ (a')”.

Clauses (3) and (4) of [Stacks, Tag 01Q3] imply clause (1) — the converse of Stacks.SheafOfModules.Invertible.exists_sections_mem_nonvanishingOpen_le_of_isAmple, which is the implication (1) ⇒ (3) ∧ (4).

Either clause alone suffices on a quasi-compact scheme: clause (4) applied at the ambient open ⊤ is condition (2) of Stacks Tag 01PS, and clause (3) yields clause (4) by Stacks Tag 01PX, which is unconditional here because Tag 01PV is proved. Both are stated so that the conjunction the forward implication produces can be fed back verbatim.

theorem isAmple_of_isBasisNonvanishing_and_isBasisAffineNonvanishing [CompactSpace X]
    (h : Stacks.AmpleTheory.IsBasisNonvanishing X L ∧
      Stacks.AmpleTheory.IsBasisAffineNonvanishing X L) :
    IsAmple X L

Stacks.AmpleCharacterization.isAmple_of_isBasisNonvanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/Basic.lean, line 232. The attribute's comment: “clause (3) implies (1)”. References: EGA II (4.5.2), “(a) ⇐ (a')”; EGA II (5.1.2), “d) ⇒ c')”; SGA 6 II (2.2.3), “(i) ⇒ (ii)”; SGA 6 II (2.2.4), “partial”.

Clause (3) of [Stacks, Tag 01Q3] implies clause (1), from clause (3) alone: on a quasi-compact scheme, an invertible L whose nonvanishing opens X_s — for s a global section of a positive tensor power of L — form a basis for the topology is ample.

This is the implication the conjunction above does not give, since that one consumes only its clause (4) conjunct. Stacks Tag 01PX supplies the step clause (3) ⇒ clause (4): the affine opens are themselves a basis, so the prescribed open may be shrunk to an affine one before clause (3) is applied, and the resulting X_s, sitting inside an affine open, is affine by Stacks Tag 01PV. Clause (4) at the ambient open ⊤ is then condition (2) of Stacks Tag 01PS.

The implication was already proved, as the mpr of Stacks.SectionExtension.isAmple_iff_compactSpace_and_isBasisNonvanishing, and that is what is invoked here rather than a second derivation; what this declaration adds is the standalone statement of the clause, and its registration, beside the other clauses of the tag. Tag 01PX is likewise already proved and registered — as AlgebraicGeometry.Scheme.Modules.isBasis_affine_nonvanishingOpens, in the Tag 01PS vocabulary — and in the vocabulary these clauses are stated in it is Stacks.NonvanishingAffineIntersection.isBasisAffineNonvanishing_of_isBasisNonvanishing, which carries no hypothesis beyond invertibility because Tag 01PV is proved (AlgebraicGeometry.Scheme.Modules.isAffineOpen_inf_nonvanishingOpen).

The hypotheses are exactly clause (3) and the quasi-compactness standing over the whole source Proposition; nothing is assumed about affineness of the X_s, which is precisely what clause (3) as the tag states it leaves out.

theorem isAmple_of_isBasisNonvanishing [CompactSpace X]
    (h : Stacks.AmpleTheory.IsBasisNonvanishing X L) :
    IsAmple X L

Stacks.AmpleCharacterization.quasiSeparatedSpace_and_exists_epi_biproduct_ideal_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/Basic.lean, line 271. The attribute's comment: “clause (9)”. References: EGA II (2.7.10), “ideals”; EGA II (4.5.5), “(a) ⇒ (d'), ideals”.

Clause (9) of [Stacks, Tag 01Q3] — the clause labelled 01QC: X is quasi-separated, and every sheaf of ideals of finite type on X is a quotient of a direct sum of k copies of L ^⊗ (-n) for some n > 0 and k ≥ 0.

A sheaf of ideals is presented as a module J together with a monomorphism J ⟶ 𝒪_X, which is what "sheaf of ideals" means; k is the cardinality of the finite index type ι, a direct sum over a finite index type being a direct sum of Nat.card ι copies.

The clause is read with its ideals quasi-coherent, as clause (6) of the source states them explicitly, and this is forced rather than chosen: a quotient of a direct sum of quasi-coherent modules is quasi-coherent, so the clause would be false for a sheaf of ideals that is not. It is also what makes the source's "the implication (8) ⇒ (9) is trivial" true, and it is the generality in which clause (8) is registered (Stacks.AmpleLocalGeneration.quasiSeparatedSpace_and_exists_epi_biproduct_of_isAmple).

The proof is exactly the source's: clause (9) is clause (8) with its quantifier restricted, so clause (8) applied to J is the whole content.

theorem quasiSeparatedSpace_and_exists_epi_biproduct_ideal_of_isAmple (hL : IsAmple X L) :
    QuasiSeparatedSpace X ∧ ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j →
      J.IsQuasicoherent → SheafOfModules.IsFiniteType.{u, u, u} J →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : CategoryTheory.Limits.Bicone fun _ : ι => tensorPowModule X L (-n))
            (_ : b.IsBilimit) (p : b.pt ⟶ J), CategoryTheory.Epi p

Stacks.AmpleCharacterization.iSup_range_twistHom_eq_top_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseFive.lean, line 289. The attribute's comment: “clause (5)”. References: EGA II (4.5.5), “(a) ⇒ (b)”.

Clause (5) of [Stacks, Tag 01Q3] — the clause labelled 01Q8: for every quasi-coherent sheaf F on X the sum of the images of the canonical maps Γ(X, F ⊗ L^{⊗ n}) ⊗_𝐙 L^{⊗ -n} ⟶ F, over n ≥ 1, equals F.

The n-th canonical map is the sum over m ∈ Γ(X, F ⊗ L^{⊗ n}) of the maps Stacks.AmpleCharacterization.twistHom L F n m, a tensor product over 𝐙 with a free abelian group being the direct sum; so the sum of the images of the canonical maps is the sum of the images of the twistHom L F n m, which is what is written.

The equality of subsheaves is read on stalks, as Stacks.AmpleLocalGeneration.IsFinGenOn and every other generation statement in this repository is. For sheaves of modules the two readings agree: the stalk functor is exact and commutes with the filtered colimit defining a sum of subsheaves, and a submodule of F whose stalks are all of F is F. What is proved is in fact stronger than the clause and is what the source's proof gives — every germ lies in the image of a single one of the maps, by Stacks.AmpleCharacterization.exists_mem_range_twistHom.

theorem iSup_range_twistHom_eq_top_of_isAmple (hL : IsAmple X L) :
    ∀ F : X.Modules, F.IsQuasicoherent → ∀ x : X,
      (⨆ (n : ℕ) (_ : 1 ≤ n) (m : Γ(F ⊗ tensorPowModule X L (n : ℤ), ⊤)),
        LinearMap.range (Stacks.ModuleStalk.map (twistHom L F (n : ℤ) m) x)) = ⊤

Stacks.AmpleCharacterization.iSup_range_twistHom_ideal_eq_top_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseFive.lean, line 308. The attribute's comment: “clause (6)”. References: EGA II (4.5.5), “(a) ⇒ (b), ideals”.

Clause (6) of [Stacks, Tag 01Q3] — the clause labelled 01Q9: clause (5) with F ranging over the quasi-coherent sheaves of ideals of X.

A sheaf of ideals is a module J with a monomorphism into 𝒪_X. The clause is clause (5) with its quantifier restricted, which is why the source proves it by the single word "clearly"; the restriction is recorded here rather than left implicit because clauses (6) and (9) are the two the source's cycle re-enters ampleness through.

theorem iSup_range_twistHom_ideal_eq_top_of_isAmple (hL : IsAmple X L) :
    ∀ (J : X.Modules) (j : J ⟶ Stacks.Ample.unitModule X), Mono j → J.IsQuasicoherent →
      ∀ x : X, (⨆ (n : ℕ) (_ : 1 ≤ n) (m : Γ(J ⊗ tensorPowModule X L (n : ℤ), ⊤)),
        LinearMap.range (Stacks.ModuleStalk.map (twistHom L J (n : ℤ) m) x)) = ⊤

Stacks.AmpleCharacterization.iSup_range_twistHom_ideal_eq_top_of_exists_epi_biproduct_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseNineDirect.lean, line 167. The attribute's comment: “clause (9) implies (6)”.

Clause (9) of [Stacks, Tag 01Q3] implies clause (6), by the source's own argument through [Stacks, Tag 01PG] rather than through ampleness.

Given a quasi-coherent sheaf of ideals j : ℐ ⟶ 𝒪_X, a point x and a germ u ∈ ℐ_x: the germ comes from a section of ℐ over an affine open V ∋ x, and Tag 01PG in the form AlgebraicGeometry.exists_finiteTypeQuasicoherentSubobject_section — where quasi-separatedness is used — puts that section inside a quasi-coherent subobject G ⊆ ℐ of finite type. Then G.arrow ≫ j is a monomorphism, so clause (9) applies to G and writes it as a quotient of a finite direct sum of copies of L ^⊗ (-n) with n > 0; the germ of G decomposes as a finite sum of germs from the summands (Stacks.ModuleBicone.exists_germ_sum_of_epi), and pushing the decomposition forward along G.arrow writes u as a finite sum of images of morphisms L ^⊗ (-n) ⟶ ℐ, each of which is one of the maps of clause (6) by Stacks.AmpleCharacterization.exists_twistHom_eq.

The other proof of this implication, Stacks.AmpleCharacterization .iSup_range_twistHom_ideal_eq_top_of_quasiSeparatedSpace_and_exists_epi_biproduct_ideal, goes (9) ⇒ (1) ⇒ (6) instead; both are kept, as the tag's implication and as the route the nine-clause equivalence was first closed along.

theorem iSup_range_twistHom_ideal_eq_top_of_exists_epi_biproduct_ideal [CompactSpace X]
    (h : QuasiSeparatedSpace X ∧ ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j →
      J.IsQuasicoherent → SheafOfModules.IsFiniteType.{u, u, u} J →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
            (p : b.pt ⟶ J), Epi p) :
    ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j → J.IsQuasicoherent →
      ∀ x : X, (⨆ (n : ℕ) (_ : 1 ≤ n) (m : Γ(J ⊗ tensorPowModule X L (n : ℤ), ⊤)),
        LinearMap.range (Stacks.ModuleStalk.map (twistHom L J (n : ℤ) m) x)) = ⊤

Stacks.AmpleCharacterization.isAmple_of_iSup_range_twistHom_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseSixConverse.lean, line 445. The attribute's comment: “clause (6) implies (1)”. References: EGA II (4.5.5), “(b) ⇒ (a), ideals”.

Clause (6) of [Stacks, Tag 01Q3] implies clause (1) — the implication the source's cycle re-enters ampleness through. If for every quasi-coherent sheaf of ideals of the quasi-compact scheme X the sum of the images of the canonical maps Γ(X, ℐ ⊗ L^{⊗ n}) ⊗_𝐙 L^{⊗ -n} ⟶ ℐ, n ≥ 1, is all of ℐ, then L is ample.

This is the source's argument verbatim. Given x, choose an affine open U ∋ x and apply the hypothesis to the quasi-coherent sheaf of ideals Stacks.ComplementIdeal.sheaf of the reduced closed subscheme on X ∖ U (Schemes, Section 01IZ, i.e. [Stacks, Tag 01J3]). Its stalk at x contains the germ of 1, so some single map L ^⊗ (-n) ⟶ ℐ composed with the inclusion ℐ ⟶ 𝒪_X has image at x outside 𝔪_x. That composite is multiplication by a global section s of L ^⊗ n (Stacks.AmpleCharacterization.exists_twistUnitHom_eq); s does not vanish at x, and it vanishes along X ∖ U because the composite factors through ℐ, so X_s ⊆ U and X_s is affine by [Stacks, Tag 01PV].

theorem isAmple_of_iSup_range_twistHom_ideal [CompactSpace X]
    (h : ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j → J.IsQuasicoherent →
      ∀ x : X, (⨆ (n : ℕ) (_ : 1 ≤ n) (m : Γ(J ⊗ tensorPowModule X L (n : ℤ), ⊤)),
        LinearMap.range (Stacks.ModuleStalk.map (twistHom L J (n : ℤ) m) x)) = ⊤) :
    IsAmple X L

Stacks.AmpleCharacterization.isAmple_of_iSup_range_twistHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseSixConverse.lean, line 489. The attribute's comment: “clause (5) implies (1)”. References: EGA II (4.5.5), “(b) ⇒ (a)”.

Clause (5) of [Stacks, Tag 01Q3] implies clause (1): clause (5) is clause (6) with its quantifier widened from the quasi-coherent sheaves of ideals to all quasi-coherent sheaves, so this is Stacks.AmpleCharacterization.isAmple_of_iSup_range_twistHom_ideal with the hypothesis restricted.

theorem isAmple_of_iSup_range_twistHom [CompactSpace X]
    (h : ∀ F : X.Modules, F.IsQuasicoherent → ∀ x : X,
      (⨆ (n : ℕ) (_ : 1 ≤ n) (m : Γ(F ⊗ tensorPowModule X L (n : ℤ), ⊤)),
        LinearMap.range (Stacks.ModuleStalk.map (twistHom L F (n : ℤ) m) x)) = ⊤) :
    IsAmple X L

Stacks.AmpleCharacterization.quasiSeparatedSpace_and_exists_epi_biproduct_of_isGeneratedByGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseSixConverse.lean, line 532. The attribute's comment: “clause (7) implies (8)”. References: EGA II (2.7.10), “(d) ⇒ (d')”.

Clause (7) of [Stacks, Tag 01Q3] implies clause (8), at clause (7)'s own strength. The clause asks only that F ⊗ L ^⊗ n be globally generated for every n ≥ n₀ — generated by some family of global sections, [Stacks, Tag 03DE] (3), with no finiteness demanded of that family — and that is the hypothesis carried here. The quasi-compactness of X is the standing hypothesis of the tag and nothing else is added.

The finiteness clause (8) asks for is supplied by that quasi-compactness, which is where the source puts it too. F ⊗ L ^⊗ n is of finite type (isFiniteType_tensor: F is of finite type by the clause's own hypothesis and L ^⊗ n is of finite type, being invertible), and on a quasi-compact scheme a module of finite type generated by global sections is generated by finitely many of them — Modules, Lemma 17.9.7 ([Stacks, Tag 01BB]), available as Stacks.AmpleEventualGeneration.isFinGen_of_generatingSections. From there the step is the one Stacks.AmpleLocalGeneration.quasiSeparatedSpace_and_exists_epi_biproduct_of_isAmple runs: a finite family of global sections generating F ⊗ L ^⊗ n for one n ≥ 1 is exactly an epimorphism onto F from a finite direct sum of copies of L ^⊗ (-n), by Stacks.AmpleGlobalGeneration.exists_epi_biproduct_of_epi_free.

theorem quasiSeparatedSpace_and_exists_epi_biproduct_of_isGeneratedByGlobalSections
    [CompactSpace X]
    (h : QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n →
          _root_.SheafOfModules.IsGeneratedByGlobalSections.{u, u, u}
            ((F ⊗ tensorPowModule X L n : X.Modules))) :
    QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
            (p : b.pt ⟶ F), Epi p

Stacks.AmpleCharacterization.quasiSeparatedSpace_and_exists_epi_biproduct_of_isEventuallyGloballyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseSixConverse.lean, line 570. The attribute's comment: “clause (7) implies (8), under the strengthened hypothesis that the twists are generated by finitely many global sections; the tag's own implication is quasiSeparatedSpace_and_exists_epi_biproduct_of_isGeneratedByGlobalSections above”. References: EGA II (2.7.10), “(d) ⇒ (d')”.

Clause (7) of [Stacks, Tag 01Q3] implies clause (8), from the strengthened hypothesis that the twists are generated by finitely many global sections — which is more than clause (7) says, and so is not the tag's implication; that one is quasiSeparatedSpace_and_exists_epi_biproduct_of_isGeneratedByGlobalSections above, and it is what the equivalences below rest on. This variant is kept because it needs no quasi-compactness: it is the proof Stacks.AmpleLocalGeneration.quasiSeparatedSpace_and_exists_epi_biproduct_of_isAmple runs with ampleness replaced by the strengthened clause, a finite family of global sections generating F ⊗ L ^⊗ n for one n ≥ 1 being exactly an epimorphism onto F from a finite direct sum of copies of L ^⊗ (-n), by Stacks.AmpleGlobalGeneration.exists_epi_biproduct_of_epi_free.

theorem quasiSeparatedSpace_and_exists_epi_biproduct_of_isEventuallyGloballyGenerated
    (h : QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n →
          ∃ σ : (F ⊗ tensorPowModule X L n).GeneratingSections, Finite σ.I) :
    QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
            (p : b.pt ⟶ F), Epi p

Stacks.AmpleCharacterization.quasiSeparatedSpace_and_exists_epi_biproduct_ideal_of_exists_epi_biproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseSixConverse.lean, line 591. The attribute's comment: “clause (8) implies (9)”. References: EGA II (2.7.10), “(d'), ideals”.

Clause (8) of [Stacks, Tag 01Q3] implies clause (9), the source's "trivial" step: clause (9) is clause (8) with its quantifier restricted to the sheaves of ideals.

theorem quasiSeparatedSpace_and_exists_epi_biproduct_ideal_of_exists_epi_biproduct
    (h : QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
            (p : b.pt ⟶ F), Epi p) :
    QuasiSeparatedSpace X ∧ ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j →
      J.IsQuasicoherent → SheafOfModules.IsFiniteType.{u, u, u} J →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
            (p : b.pt ⟶ J), Epi p

Stacks.AmpleCharacterization.isAmple_of_quasiSeparatedSpace_and_exists_epi_biproduct_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseSixConverse.lean, line 630. The attribute's comment: “clause (9) implies (1)”. References: EGA II (2.7.10), “(d') ⇒ (a), ideals”; EGA II (4.5.5), “(d') ⇒ (a), ideals”.

Clause (9) of [Stacks, Tag 01Q3] implies clause (1) — the step the source's second cycle re-enters ampleness through, and with the two implications above the last link of the nine-clause equivalence.

The argument is the source's, with [Stacks, Tag 01PG] where the source puts it. Fix x, choose an affine open U ∋ x and let Z = X ∖ U with its reduced closed subscheme structure. Its sheaf of ideals ℐ_Z is the unit ideal on some affine open V ∋ x, so Tag 01PG — in its ideal-sheaf form Stacks.IdealSheaf.exists_fg_le_of_mem, which is what quasi-separatedness is used for — produces a quasi-coherent sheaf of ideals ℐ ⊆ ℐ_Z, finitely generated on every affine open and still containing the unit section over V. Being finitely generated affine- locally it is of finite type (Stacks.IdealSheafModules.isFiniteType_sheaf), so clause (9) applies to it: ℐ is a quotient of a finite direct sum of copies of L ^⊗ (-n) with n > 0.

The germ at x of that unit section is not in 𝔪_x · (𝒪_X)_x, and Stacks.ModuleBicone.exists_germ_sum_of_epi writes it as a finite sum of germs coming from the summands; since 𝔪_x · (𝒪_X)_x is a submodule, one summand i already escapes it. Its composite L ^⊗ (-n) ⟶ ℐ ⟶ 𝒪_X is multiplication by a global section σ of L ^⊗ n (Stacks.AmpleCharacterization.exists_twistUnitHom_eq), and from here the argument is the one Stacks.AmpleCharacterization.isAmple_of_iSup_range_twistHom_ideal runs: σ does not vanish at x, and it vanishes at every point of Z — which is in the support of ℐ because ℐ ⊆ ℐ_Z — so X_σ ⊆ U and X_σ is affine by [Stacks, Tag 01PV].

theorem isAmple_of_quasiSeparatedSpace_and_exists_epi_biproduct_ideal [CompactSpace X]
    (h : QuasiSeparatedSpace X ∧ ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j →
      J.IsQuasicoherent → SheafOfModules.IsFiniteType.{u, u, u} J →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
            (p : b.pt ⟶ J), Epi p) :
    IsAmple X L

Stacks.AmpleCharacterization.iSup_range_twistHom_ideal_eq_top_of_quasiSeparatedSpace_and_exists_epi_biproduct_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/ClauseSixConverse.lean, line 702. The attribute's comment: “clause (9) implies (6)”. References: EGA II (4.5.5), “(d') ⇒ (b), ideals”.

Clause (9) of [Stacks, Tag 01Q3] implies clause (6), the implication the source's cycle runs through. It is clause (9) implies clause (1) (Stacks.AmpleCharacterization.isAmple_of_quasiSeparatedSpace_and_exists_epi_biproduct_ideal) followed by clause (6) from ampleness, rather than the source's direct argument; the ingredient the source uses for the direct route, [Stacks, Tag 01PG], is the ingredient used there.

theorem iSup_range_twistHom_ideal_eq_top_of_quasiSeparatedSpace_and_exists_epi_biproduct_ideal
    [CompactSpace X]
    (h : QuasiSeparatedSpace X ∧ ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j →
      J.IsQuasicoherent → SheafOfModules.IsFiniteType.{u, u, u} J →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
            (p : b.pt ⟶ J), Epi p) :
    ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j → J.IsQuasicoherent →
      ∀ x : X, (⨆ (n : ℕ) (_ : 1 ≤ n) (m : Γ(J ⊗ tensorPowModule X L (n : ℤ), ⊤)),
        LinearMap.range (Stacks.ModuleStalk.map (twistHom L J (n : ℤ) m) x)) = ⊤

Stacks.AmpleCharacterization.isBasisNonvanishing_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/NineClauses.lean, line 123. The attribute's comment: “clause (3)”. References: EGA II (4.5.2), “(a) ⇒ (a')”.

Clause (1) of [Stacks, Tag 01Q3] implies clause (3) — the clause labelled 01Q6: for L ample the opens X_s, with s ∈ S₊ homogeneous, form a basis for the topology of X.

The clause is written out rather than named, and in the Stacks.Ample.IsAmple vocabulary the other eight clauses of the tag are stated in. The content is Stacks.SectionExtension.isBasisNonvanishing_of_isAmple.

theorem isBasisNonvanishing_of_isAmple (hL : IsAmple X L) :
    ∀ (x : X) (U : X.Opens), x ∈ U → ∃ n : ℕ, 1 ≤ n ∧
      ∃ s : Γ(tensorPowModule X L (n : ℤ), ⊤),
        x ∈ powNonvanishingOpen X L n s ∧ powNonvanishingOpen X L n s ≤ U

Stacks.AmpleCharacterization.isBasisAffineNonvanishing_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/NineClauses.lean, line 137. The attribute's comment: “clause (4)”. References: EGA II (4.5.2), “(a) ⇒ (a')”.

Clause (1) of [Stacks, Tag 01Q3] implies clause (4) — the clause labelled 01Q7: for L ample the opens X_s, with s ∈ S₊ homogeneous, which are affine form a basis for the topology of X.

The content is Stacks.SectionExtension.isBasisAffineNonvanishing_of_isAmple, namely clause (3) followed by [Stacks, Tag 01PX], which is unconditional here because [Stacks, Tag 01PV] is proved.

theorem isBasisAffineNonvanishing_of_isAmple (hL : IsAmple X L) :
    ∀ (x : X) (U : X.Opens), x ∈ U → ∃ n : ℕ, 1 ≤ n ∧
      ∃ s : Γ(tensorPowModule X L (n : ℤ), ⊤),
        IsAffineOpen (powNonvanishingOpen X L n s) ∧
          x ∈ powNonvanishingOpen X L n s ∧ powNonvanishingOpen X L n s ≤ U

Stacks.AmpleCharacterization.isAmple_of_isBasisAffineNonvanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/NineClauses.lean, line 156. The attribute's comment: “clause (4) implies (1)”. References: EGA II (4.5.2), “(a) ⇐ (a')”.

Clause (4) of [Stacks, Tag 01Q3] implies clause (1), with clause (4) as the tag states it and nothing else beyond the standing quasi-compactness: if the affine opens X_s, for s ∈ S₊ homogeneous, form a basis for the topology of the quasi-compact scheme X, then L is ample.

Stacks.AmpleCharacterization.isAmple_of_isBasisNonvanishing_and_isBasisAffineNonvanishing proves the same conclusion from the conjunction of clauses (3) and (4), which is more than this clause supplies; the clause's own strength suffices, because clause (4) applied at the ambient open ⊤ is already condition (2) of [Stacks, Tag 01PS]. That is Stacks.AmpleTheory.isAmple_of_isBasisAffineNonvanishing.

theorem isAmple_of_isBasisAffineNonvanishing [CompactSpace X]
    (h : ∀ (x : X) (U : X.Opens), x ∈ U → ∃ n : ℕ, 1 ≤ n ∧
      ∃ s : Γ(tensorPowModule X L (n : ℤ), ⊤),
        IsAffineOpen (powNonvanishingOpen X L n s) ∧
          x ∈ powNonvanishingOpen X L n s ∧ powNonvanishingOpen X L n s ≤ U) :
    IsAmple X L

Stacks.AmpleCharacterization.quasiSeparatedSpace_and_isGeneratedByGlobalSections_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/NineClauses.lean, line 178. The attribute's comment: “clause (7)”. References: EGA II (4.5.5), “(a) ⇒ (d)”; EGA II (2.7.9).

Clause (1) of [Stacks, Tag 01Q3] implies clause (7) — the clause labelled 01QA — as the tag states it: X is quasi-separated, and for every quasi-coherent sheaf F of finite type there is an n₀ with F ⊗ L ^⊗ n globally generated, [Stacks, Tag 03DE] (3), for all n ≥ n₀. Nothing is asked of the generating family.

Stacks.AmpleLocalGeneration.quasiSeparatedSpace_and_isEventuallyGloballyGenerated_of_isAmple concludes the stronger statement that the generating family may be taken finite, which is more than the clause says; this is the clause itself, and it is the form the equivalence below and the implication (7) ⇒ (8) of Stacks.AmpleCharacterization.quasiSeparatedSpace_and_exists_epi_biproduct_of_isGeneratedByGlobalSections are stated at.

theorem quasiSeparatedSpace_and_isGeneratedByGlobalSections_of_isAmple (hL : IsAmple X L) :
    QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n →
          _root_.SheafOfModules.IsGeneratedByGlobalSections.{u, u, u}
            ((F ⊗ tensorPowModule X L n : X.Modules))

Stacks.AmpleCharacterization.isAmple_of_quasiSeparatedSpace_and_isGeneratedByGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/NineClauses.lean, line 196. The attribute's comment: “clause (7) implies (1)”. References: EGA II (4.5.5), “(d) ⇒ (a)”.

Clause (7) of [Stacks, Tag 01Q3] implies clause (1), from clause (7) at its own strength — the twists merely globally generated, with no bound on the generating family — and with no hypothesis beyond the tag's standing quasi-compactness.

The route is the source's own: clause (7) implies clause (8) (Stacks.AmpleCharacterization.quasiSeparatedSpace_and_exists_epi_biproduct_of_isGeneratedByGlobalSections, where the quasi-compactness cuts the generating family down to a finite one by [Stacks, Tag 01BB]), clause (8) implies clause (9), and clause (9) implies clause (1).

theorem isAmple_of_quasiSeparatedSpace_and_isGeneratedByGlobalSections [CompactSpace X]
    (h : QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n →
          _root_.SheafOfModules.IsGeneratedByGlobalSections.{u, u, u}
            ((F ⊗ tensorPowModule X L n : X.Modules))) :
    IsAmple X L

Stacks.AmpleCharacterization.isAmple_of_quasiSeparatedSpace_and_exists_epi_biproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/NineClauses.lean, line 212. The attribute's comment: “clause (8) implies (1)”. References: EGA II (4.5.5), “(d') ⇒ (a)”.

Clause (8) of [Stacks, Tag 01Q3] implies clause (1): the source's (8) ⇒ (9) ⇒ (1) in one step, Stacks.AmpleCharacterization.quasiSeparatedSpace_and_exists_epi_biproduct_ideal_of_exists_epi_biproduct followed by Stacks.AmpleCharacterization.isAmple_of_quasiSeparatedSpace_and_exists_epi_biproduct_ideal.

theorem isAmple_of_quasiSeparatedSpace_and_exists_epi_biproduct [CompactSpace X]
    (h : QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
            (p : b.pt ⟶ F), Epi p) :
    IsAmple X L

Stacks.AmpleCharacterization.tfae_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCharacterization/NineClauses.lean, line 246. References: EGA II (4.5.2); EGA II (4.5.5); EGA II (2.7.10); SGA 6 II (2.2.3), “single L”.

[Stacks, Tag 01Q3]. Let X be a quasi-compact scheme, L an invertible 𝒪_X-module, and S = Γ_*(X, L). The nine conditions of the source Proposition are equivalent:

1. L is ample;
2. the opens X_s, s ∈ S₊ homogeneous, cover X and the resulting X ⟶ Proj S is an open immersion;
3. those opens form a basis for the topology of X;
4. the affine ones among them form a basis for the topology of X;
5. for every quasi-coherent F the images of the canonical maps Γ(X, F ⊗ L^{⊗ n}) ⊗_𝐙 L^{⊗ -n} ⟶ F, n ≥ 1, sum to F;
6. the same for F a quasi-coherent sheaf of ideals;
7. X is quasi-separated and every finite-type quasi-coherent F has F ⊗ L^{⊗ n} globally generated for all large n;
8. X is quasi-separated and every finite-type quasi-coherent F is a quotient of a finite direct sum of copies of a single L ^⊗ (-n), n > 0;
9. the same for F a finite-type quasi-coherent sheaf of ideals.

The only hypothesis is the source's own: X quasi-compact, which is [CompactSpace X], plus the invertibility of L. Clause (1), Stacks.Ample.IsAmple, carries the quasi-compactness in its own definition, so the instance is what puts the remaining eight clauses at the strength the source gives them. The module docstring says where each 1 ↔ i comes from.

theorem tfae_isAmple [CompactSpace X] :
    List.TFAE
      [ IsAmple X L,
        ∃ h : Stacks.SectionRingProjMorphism.nvUnion L = ⊤,
          IsOpenImmersion (Stacks.SectionRingProjMorphism.projHomOfCovers L h),
        ∀ (x : X) (U : X.Opens), x ∈ U → ∃ n : ℕ, 1 ≤ n ∧
          ∃ s : Γ(tensorPowModule X L (n : ℤ), ⊤),
            x ∈ powNonvanishingOpen X L n s ∧ powNonvanishingOpen X L n s ≤ U,
        ∀ (x : X) (U : X.Opens), x ∈ U → ∃ n : ℕ, 1 ≤ n ∧
          ∃ s : Γ(tensorPowModule X L (n : ℤ), ⊤),
            IsAffineOpen (powNonvanishingOpen X L n s) ∧
              x ∈ powNonvanishingOpen X L n s ∧ powNonvanishingOpen X L n s ≤ U,
        ∀ F : X.Modules, F.IsQuasicoherent → ∀ x : X,
          (⨆ (n : ℕ) (_ : 1 ≤ n) (m : Γ(F ⊗ tensorPowModule X L (n : ℤ), ⊤)),
            LinearMap.range (Stacks.ModuleStalk.map (twistHom L F (n : ℤ) m) x)) = ⊤,
        ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j → J.IsQuasicoherent →
          ∀ x : X, (⨆ (n : ℕ) (_ : 1 ≤ n) (m : Γ(J ⊗ tensorPowModule X L (n : ℤ), ⊤)),
            LinearMap.range (Stacks.ModuleStalk.map (twistHom L J (n : ℤ) m) x)) = ⊤,
        QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
          SheafOfModules.IsFiniteType.{u, u, u} F →
            ∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n →
              _root_.SheafOfModules.IsGeneratedByGlobalSections.{u, u, u}
                ((F ⊗ tensorPowModule X L n : X.Modules)),
        QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
          SheafOfModules.IsFiniteType.{u, u, u} F →
            ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
              ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
                (p : b.pt ⟶ F), Epi p,
        QuasiSeparatedSpace X ∧ ∀ (J : X.Modules) (j : J ⟶ unitModule X), Mono j →
          J.IsQuasicoherent → SheafOfModules.IsFiniteType.{u, u, u} J →
            ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
              ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
                (p : b.pt ⟶ J), Epi p ]

Stacks.AmpleLocalGeneration.quasiSeparatedSpace_and_isEventuallyGloballyGenerated_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleLocalGeneration/FromExtension.lean, line 226. The attribute's comment: “clause (7)”. References: EGA II (4.6.8), “absolute case of (c)”; EGA II (4.5.5), “(a) ⇒ (d)”; EGA II (2.7.9).

Clause (7) of [Stacks, Tag 01Q3] — the clause labelled 01QA: X is quasi-separated, and for every quasi-coherent sheaf F of finite type on X there is an integer n₀ such that F ⊗ L ^⊗ n is globally generated for all n ≥ n₀.

Both conjuncts follow from ampleness of L, which is clause (1): quasi-separatedness by [Stacks, Tag 01PV] (Stacks.AmplePullbackPart1.quasiSeparatedSpace_of_isAmple, the affine nonvanishing opens being a basis), and the generation by Stacks.AmpleLocalGeneration.isEventuallyGloballyGenerated_of_isAmple.

The generation is obtained in the stronger form the source does not ask for: the twist is generated by finitely many global sections, not merely by all of them.

theorem quasiSeparatedSpace_and_isEventuallyGloballyGenerated_of_isAmple (L : X.Modules)
    [IsInvertibleModule X L] (hL : IsAmple X L) :
    QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ n₀ : ℤ, ∀ n : ℤ, n₀ ≤ n →
          ∃ σ : (F ⊗ tensorPowModule X L n).GeneratingSections, Finite σ.I

Stacks.AmpleLocalGeneration.quasiSeparatedSpace_and_exists_epi_biproduct_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleLocalGeneration/FromExtension.lean, line 253. The attribute's comment: “clause (8)”. References: EGA II (2.7.10), “exists n,k quotient”; EGA II (4.5.5), “(a) ⇒ (d')”; SGA 6 II (2.2.3), “(iii), single L”.

Clause (8) of [Stacks, Tag 01Q3] — the clause labelled 01QB: X is quasi-separated, and for every quasi-coherent sheaf F of finite type on X there are integers n > 0 and k ≥ 0 such that F is a quotient of a direct sum of k copies of L ^⊗ (-n).

The summands all carry the same degree -n, as the source's clause does; the weaker statement with varying degrees is Stacks.AmpleLocalGeneration.isQuotientOfNegativeTwists_of_isAmple. The k of the source is the cardinality of the index type ι below: a direct sum over a finite index type is a direct sum of Nat.card ι copies, and the two existence statements are the same.

The proof is clause (7) at a degree n ≥ max n₀ 1, which makes F ⊗ L ^⊗ n a quotient of a finite free module, followed by Stacks.AmpleGlobalGeneration.exists_epi_biproduct_of_epi_free, which untwists: tensoring the epimorphism 𝒪_X^{⊕ ι} ↠ F ⊗ L ^⊗ n by L ^⊗ (-n) presents F as a quotient of (L ^⊗ (-n))^{⊕ ι}.

theorem quasiSeparatedSpace_and_exists_epi_biproduct_of_isAmple (L : X.Modules)
    [IsInvertibleModule X L] (hL : IsAmple X L) :
    QuasiSeparatedSpace X ∧ ∀ F : X.Modules, F.IsQuasicoherent →
      SheafOfModules.IsFiniteType.{u, u, u} F →
        ∃ (n : ℤ) (ι : Type u) (_ : Finite ι), 0 < n ∧
          ∃ (b : Bicone fun _ : ι => tensorPowModule X L (-n)) (_ : b.IsBilimit)
            (p : b.pt ⟶ F), Epi p

Stacks.SheafOfModules.Invertible.exists_sections_mem_nonvanishingOpen_le_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionExtensionAffineCover/Basic.lean, line 380. The attribute's comment: “(1) implies (3) and (4)”. References: EGA II (4.5.2), “(a') => (a)”; SGA 6 II (2.2.3), “(i), single L”.

Tag 01Q6 (item (3) of Tag 01Q3): the nonvanishing opens of the global sections of the positive tensor powers of an ample invertible sheaf form a basis for the topology -- and the members of that basis can be taken affine, which is item (4) of Tag 01Q3 (tag 01Q7) and is the one-point case of Stacks, Tag 09NV.

Affineness is free here: the section produced has nonvanishing open a basic open of the affine X_{σ i₀}, by AlgebraicGeometry.IsAffineOpen.basicOpen.

theorem exists_sections_mem_nonvanishingOpen_le_of_isAmple
    (hL : AlgebraicGeometry.Scheme.Modules.IsAmple Y M)
    (W : Y.Opens) (x : Y) (hx : x ∈ W) :
    ∃ (m : ℕ) (_ : 1 ≤ m) (gg : Mpow[m].sections),
      x ∈ NV[m, gg] ∧ NV[m, gg] ≤ W ∧ IsAffineOpen NV[m, gg]

Tag 0B3E, a lemma

Tag 0B3E in the Stacks Project.

Stacks.AmplePullbackCovering.isAmple_modulePullback_of_immersion_or_isEmbedding, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmplePullbackCovering/Basic.lean, line 84. References: EGA II (4.6.13), “(i bis), absolute case”.

Stacks Tag 0B3E. For L an ample invertible 𝒪_X-module and i : X' ⟶ X a quasi-compact immersion, an immersion of a quasi-compact scheme, a quasi-compact homeomorphism onto its image, or a homeomorphism onto its image out of a quasi-compact scheme, the pullback i^* L is ample on X'.

The proof is Stacks.SectionExtension.isAmple_pullbackModule; see the module documentation for why the attribute sits here rather than there.

theorem isAmple_modulePullback_of_immersion_or_isEmbedding {X X' : Scheme.{u}} (i : X' ⟶ X)
    (L : X.Modules) [IsInvertibleModule X L] (hL : IsAmple X L)
    (hi : (QuasiCompact i ∧ IsImmersion i) ∨ (CompactSpace X' ∧ IsImmersion i) ∨
      (QuasiCompact i ∧ Topology.IsEmbedding i) ∨
      (CompactSpace X' ∧ Topology.IsEmbedding i)) :
    IsAmple X' (Stacks.AmpleLocallyClosed.pullbackModule i L)

Tag 0DNK, a lemma

Tag 0DNK in the Stacks Project.

Stacks.AmpleExternalTensor.isInvertibleModule_externalTensor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AmpleExternalTensorProduct.lean, line 119. The attribute's comment: “invertibility: the half of Tag 0DNK's conclusion saying that pr₁^* L ⊗ pr₂^* N is an invertible module on X ×_S Y. No hypothesis on S and no ampleness; the ample half is isAmple_externalTensor.”.

The external tensor product of two invertible modules is invertible.

instance isInvertibleModule_externalTensor (L : X.Modules) (N : Y.Modules)
    [IsInvertibleModule X L] [IsInvertibleModule Y N] :
    IsInvertibleModule (pullback f g) (externalTensor f g L N)

Stacks.AmpleExternalTensor.isAmple_externalTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AmpleExternalTensorProduct.lean, line 348. The attribute's comment: “the whole lemma: for S quasi-separated, X and Y schemes over S, L ample invertible on X and N ample invertible on Y, the external tensor product pr₁^* L ⊗ pr₂^* N is ample on X ×_S Y. Invertibility of that module, the other half of the tag's conclusion, is the instance isInvertibleModule_externalTensor of this file, which the statement uses. No hypothesis beyond the tag's own.”.

Stacks Tag 0DNK. Let S be a quasi-separated scheme, let X and Y be schemes over S, let L be an ample invertible 𝒪_X-module and N an ample invertible 𝒪_Y-module. Then pr₁^* L ⊗_{𝒪_{X ×_S Y}} pr₂^* N is an ample invertible module on X ×_S Y.

Invertibility is the instance Stacks.AmpleExternalTensor.isInvertibleModule_externalTensor, which the statement of ampleness already presupposes. Ampleness is the composite of the two halves proved above: the absolute case Stacks.AmpleExternalTensor.isAmple_externalTensor_of_isAffine, taken at the terminal scheme Spec ℤ, which is affine, and the descent Stacks.AmpleExternalTensor.isAmple_externalTensor_of_isAmple_absolute along the quasi-compact immersion X ×_S Y ⟶ X ×_{Spec ℤ} Y, which is where quasi-separatedness of S is used.

theorem isAmple_externalTensor [QuasiSeparatedSpace S] (hL : IsAmple X L) (hN : IsAmple Y N) :
    IsAmple (pullback f g) (externalTensor f g L N)

Sources

• Section 28.27, Tag 01PR
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Scheme.Modules.IsAmple · Stacks.AmplePositivePower.isAmple_iff_isAmple_tensorPowModule · AlgebraicGeometry.isAmple_iff_tensorPower_isAmple · AlgebraicGeometry.Scheme.Modules.isAmple_pullback_of_isClosedImmersion · AlgebraicGeometry.Scheme.Modules.isAffineOpen_inf_nonvanishingOpen · Stacks.NonvanishingAffineIntersection.isAffineOpen_inf_nonvanishingOpen · AlgebraicGeometry.Scheme.Modules.isAmple_tensor_of_power_sections_cover · AlgebraicGeometry.Scheme.Modules.isBasis_affine_nonvanishingOpens

Section28.28 Affine and quasi-affine schemes#

Section 28.28 of the Stacks Project, Tag 01QD. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01QE, a lemma

Tag 01QE in the Stacks Project.

Stacks.Ample.isQuasiAffine_iff_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleWire/Basic.lean, line 352. References: EGA II (5.1.2), “more general”; EGA II (6.6.13).

Stacks Tag 01QE, unconditionally. A scheme is quasi-affine if and only if its structure sheaf is ample. The hypothesis ∀ n, NonvanishingBasis (pow n) of Stacks.Ample.isQuasiAffine_iff_isAmpleForPowers, which is not part of the source, is discharged by Stacks.Ample.unitTensorPowBasis: its two ingredients are the identification of the stalk of 𝒪_X as an abelian group with 𝒪_{X,x} as a ring, in the sibling file, and the identification of every tensor power of 𝒪_X with 𝒪_X, above.

theorem isQuasiAffine_iff_isAmple (Y : Scheme.{u}) :
    Y.IsQuasiAffine ↔ IsAmple Y (unitModule Y)

Sources

• Section 28.28, Tag 01QD
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Ample.isQuasiAffine_iff_isAmple

Section28.29 Quasi-coherent sheaves and ample invertible sheaves#

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

Tag 01QH, a situation

Tag 01QH in the Stacks Project.

Stacks.SectionRingVeroneseChart.twistComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingVeroneseChart/IntegerDegree.lean, line 256. The attribute's comment: “the Z-graded O_X-algebra map of the Situation, degreewise in every integer degree. The rest of the Situation's claim is what makes the family a map of graded algebras rather than a family of maps, and is in two further files: multiplicativity in an arbitrary integer bidegree (n, m) is Stacks.SectionRingVeroneseChart.twistComparison_mul in StacksFrontier/AlgebraicGeometry/TwistTensor/VeroneseChartGradedAlgebra.lean, where the graded O_X-algebra structure on the source is pbTwistMul, and unit preservation -- the extra datum of GradedAlgebra.UnitalHom -- is Stacks.SectionRingVeroneseChart.pbTwistUnit_twistComparison in StacksFrontier/AlgebraicGeometry/TwistTensor/VeroneseChartGradedAlgebraUnit.lean. The three together are the Situation's map. See the 'What is not done here' section above”.

Stacks Situation 01QH's map, in degree n: the component f^*𝒪_Y(n) ⟶ 𝓛^{⊗ n} of the ℤ-graded 𝒪_X-algebra map the Situation equips the canonical morphism with. It is the forward map of twistComparisonIso, whose degree-one value is the comparison that Stacks Tag 01N8's uniqueness pins.

def twistComparison (hL : Stacks.Ample.IsAmple X L) (n : ℤ) :
    pbTwist L hL n ⟶ tensorPowModule X L n

Stacks.SectionRingVeroneseChart.twistComparison_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistTensor/VeroneseChartGradedAlgebra.lean, line 488. The attribute's comment: “multiplicativity of the Situation's map in an arbitrary integer bidegree (n, m). With the degreewise family twistComparison this makes the family a homomorphism of sheaves of Z-graded algebras here (SheafOfModules.GradedAlgebra.Hom, registered for 0FQW), which is exactly a degreewise family plus multiplicativity in every bidegree; with unit preservation (pbTwistUnit_twistComparison, the extra datum of GradedAlgebra.UnitalHom) the three jointly give the Z-graded O_X-algebra map the Situation equips the canonical morphism with. The graded algebra structure on the source is pbTwistMul, Tag 01MO's multiplication of the twisting sheaves pulled back along the canonical morphism of Tag 01PZ and conjugated by Tag 01CD; on the target it is Tag 01CU's addition law”.

Situation [Stacks, Tag 01QH]'s map is multiplicative in an arbitrary integer bidegree. The graded 𝒪_X-algebra structure pbTwistMul on ⨁_{n ∈ ℤ} f^*𝒪_Y(n), followed by the comparison in the degree n + m, is the comparisons in the degrees n and m on the two factors, followed by the addition law Stacks.Ample.tensorPowModuleAddIso of [Stacks, Tag 01CU] for the tensor powers of 𝓛.

Together with the degreewise family twistComparison this makes the family a homomorphism of sheaves of ℤ-graded algebras in this repository (Stacks.SheafOfModules.GradedAlgebra.Hom, registered for [Stacks, Tag 0FQW]), which is exactly a degreewise family together with multiplicativity in every bidegree; with unit preservation (Stacks.SectionRingVeroneseChart.pbTwistUnit_twistComparison) the three are the ℤ-graded 𝒪_X-algebra map ⨁_{n ∈ ℤ} f^*𝒪_Y(n) ⟶ ⨁_{n ∈ ℤ} 𝓛^{⊗ n} the Situation equips the canonical morphism with.

The proof is the pasting twistComparison_mul_aux of the five legs' squares, read at the unfolding twistComparison_eq of the composite.

theorem twistComparison_mul (n m : ℤ) :
    pbTwistMul L hL n m ≫ twistComparison L hL (n + m) =
      (twistComparison L hL n ⊗ₘ twistComparison L hL m) ≫
        (tensorPowModuleAddIso X L n m).hom

Stacks.SectionRingVeroneseChart.pbTwistUnit_twistComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistTensor/VeroneseChartGradedAlgebraUnit.lean, line 359. The attribute's comment: “unit preservation: the degree-zero component of the Situation's map carries the unit pbTwistUnit of the source graded O_X-algebra pbTwistMul -- Tag 01MO's multiplication of the twisting sheaves pulled back along the canonical morphism of Tag 01PZ and conjugated by Tag 01CD -- to the unit of Tag 01CU's addition law for the tensor powers of L, whose degree-zero piece is O_X by tensorPowModuleZeroIso. This is the extra datum of SheafOfModules.GradedAlgebra.UnitalHom over GradedAlgebra.Hom (both registered for 0FQW). With the degreewise family twistComparison and the bidegree square twistComparison_mul the three jointly give the Z-graded O_X-algebra map the Situation equips the canonical morphism with. The source unit is unique (pbTwistUnit_eq_of_mul), so no choice is made”.

Situation [Stacks, Tag 01QH]'s map preserves the unit. The degree-zero component of the map carries the unit pbTwistUnit of the source graded 𝒪_X-algebra pbTwistMul — the multiplication of the twisting sheaves of [Stacks, Tag 01MO], pulled back along the canonical morphism of [Stacks, Tag 01PZ] and conjugated by [Stacks, Tag 01CD] — to the unit of [Stacks, Tag 01CU]'s addition law for the tensor powers of 𝓛, whose degree-zero piece is 𝒪_X by Stacks.Ample.tensorPowModuleZeroIso.

Together with the degreewise family twistComparison and the bidegree square twistComparison_mul this is the ℤ-graded 𝒪_X-algebra map ⨁_{n ∈ ℤ} f^*𝒪_Y(n) ⟶ ⨁_{n ∈ ℤ} 𝓛^{⊗ n} the Situation equips the canonical morphism with, including the unit datum that distinguishes Stacks.SheafOfModules.GradedAlgebra.UnitalHom from Stacks.SheafOfModules.GradedAlgebra.Hom (both registered for [Stacks, Tag 0FQW]).

pbTwistUnit_eq_of_mul says the source unit is unique, so no choice is being made here.

theorem pbTwistUnit_twistComparison :
    pbTwistUnit L hL ≫ twistComparison L hL 0 = (tensorPowModuleZeroIso X L).inv

Tag 01QI, a lemma

Tag 01QI in the Stacks Project.

Stacks.SectionRingProjGoodOpen.projHomOfIsAmple_preimage_whereInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjGoodOpen/Basic.lean, line 163. The attribute's comment: “the canonical morphism lands in the good open W₁”.

Stacks Tag 01QI, first claim: the canonical morphism of Stacks Tag 01PZ maps X into the good open W_1. In the situation of Stacks Tag 01QH — L ample on X, S = Γ_*(X, L), Y = Proj S — the morphism f : X ⟶ Y of Stacks Tag 01PZ pulls the open W_1 ⊆ Y of Stacks Tag 01MU back to all of X.

The proof is pointwise. Stacks Tag 01MU's identity Stacks.AlgebraicGeometry.GoodOpenClose.whereInvertible_eq_ratioLocus turns W_1 into the union of the standard opens D₊(a b) with deg a = deg b + 1; ampleness provides at each point a pair of homogeneous sections of consecutive degrees e + 1 and e not vanishing there (Stacks.SectionRingProjGoodOpen.exists_consecutive_mem_nvLocus); their product is a homogeneous element of degree (e + 1) + e not vanishing there (Stacks.AmpleFiniteAvoidance.nvLocus_mul); and clause (1) of Stacks Tag 01PZ (Stacks.SectionRingProjMorphism.projHomOfIsAmple_preimage_projBasicOpen) identifies the preimage of D₊ of that product with the nonvanishing open, which therefore contains the point.

public theorem projHomOfIsAmple_preimage_whereInvertible (hL : Stacks.Ample.IsAmple X L) :
    Stacks.SectionRingProjMorphism.projHomOfIsAmple L hL ⁻¹ᵁ
        Stacks.AlgebraicGeometry.ProjInvertibleLocus.whereInvertible (grading L) 1 = ⊤

Stacks.SectionRingProjTwistIso.isIso_projTheta_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjTwistIso/Basic.lean, line 522. The attribute's comment: “second claim: the maps f^*O_Y(n) -> L^{tensor n} of clause (2) of Tag 01PZ are isomorphisms for every n in Z, positive, zero and negative”.

The second claim of Stacks Tag 01QI: the maps f^*𝒪_Y(n) ⟶ L^{⊗ n} are isomorphisms for every n : ℤ. In Situation Stacks Tag 01QH — X a scheme, L an ample invertible 𝒪_X-module, S = Γ_*(X, L), Y = Proj S and f : X ⟶ Y the canonical morphism of Stacks Tag 01PZ — these maps are the components of clause (2) of that tag (Stacks.SectionRingProjMorphism.Theta.projTheta), and every one of them, in every integer degree, is an isomorphism.

Both sides are invertible modules on U(ψ) = ⋃_a X_a in every degree: the target by Stacks Tag 01CU, the source because the first claim of Stacks Tag 01QI puts the image of f in the good open W₁ of Stacks Tag 01MU, where 𝒪_Y(n) is invertible (isInvertibleModule_pullback_twistM). So isIso_theta_app_of_epi reduces the claim to θ_n being an epimorphism, which is epi_projTheta_app_int.

theorem isIso_projTheta_app (hL : Stacks.Ample.IsAmple X L) (n : ℤ) :
    IsIso ((projTheta L).app n)

Stacks.SectionRingVeroneseChart.isIso_twistComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingVeroneseChart/IntegerDegree.lean, line 265. The attribute's comment: “the second claim: the maps f^*O_Y(n) -> L^{(x)n} are all isomorphisms, in every integer degree. The first claim, that the canonical morphism maps X into W_1, is Stacks.SectionRingProjGoodOpen.projHomOfIsAmple_preimage_whereInvertible”.

The second claim of Stacks Tag 01QI: the maps f^*𝒪_Y(n) → 𝓛^{⊗ n} are all isomorphisms.

theorem isIso_twistComparison (hL : Stacks.Ample.IsAmple X L) (n : ℤ) :
    IsIso (twistComparison L hL n)

Tag 01QJ, a lemma

Tag 01QJ in the Stacks Project.

Stacks.SectionRingProjQuasicoherent.pullbackComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjQuasicoherent/Comparison.lean, line 87. The attribute's comment: “clause (b): the comparison f^*M̃ ⟶ ℱ is functorial in ℱ, carrying Tag 0B5I's morphism M̃ ⟶ f_*ℱ for the twisted-section module as the hypothesis c”.

Clause (b) of Stacks Tag 01QJ: the comparison f^* M̃ ⟶ ℱ is functorial in ℱ.

Stacks Tag 0B5I supplies, for each ℱ, a morphism M̃ ⟶ f_* ℱ on Proj Γ_*(X, L) functorial in ℱ, where M = Γ_*(X, L, ℱ); that family is the hypothesis c. Transposing it along the adjunction f^* ⊣ f_* gives a morphism f^* M̃ ⟶ ℱ for each ℱ, and transposition is natural, so the transposed family is again functorial in ℱ.

def pullbackComparison
    (c : tildeFunctor L ⟶ Scheme.Modules.pushforward (projHomOfIsAmple L hL)) :
    pullbackTildeFunctor L hL ⟶ 𝟭 X.Modules

Stacks.SectionRingProjQuasicoherent.pullbackTildeComparison_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjQuasicoherent/Isomorphism.lean, line 323. The attribute's comment: “the natural transformation f^*M̃ ⟶ ℱ is an isomorphism for ℱ quasi-coherent and is the identity on M_0”.

Stacks Tag 01QJ. In Situation 01QH — X a scheme, L an ample invertible 𝒪_X-module, S = Γ_*(X, L) and f : X ⟶ Proj S the canonical morphism of Tag 01PZ — the comparison pullbackTildeComparison : f^* M̃ ⟶ ℱ, M = Γ_*(X, L, ℱ), is a natural transformation in ℱ (functoriality), it is an isomorphism for every quasi-coherent ℱ, and M_0 ⟶ Γ(Proj S, M̃) ⟶ Γ(X, ℱ) is the identity.

theorem pullbackTildeComparison_spec :
    (∀ (F : X.Modules) [F.IsQuasicoherent], IsIso ((pullbackTildeComparison L hL).app F)) ∧
      ∀ (F : X.Modules) (t : twistSections F L 0),
        ((pullbackTildeComparison L hL).app F).app (projHomOfIsAmple L hL ⁻¹ᵁ ⊤)
            (Stacks.Tag01VSPullbackTensor.modulesPullbackUnit (projHomOfIsAmple L hL)
              ((tildeFunctor L).obj F) ⊤
              (Stacks.AlgebraicGeometry.ProjStalkGlobalSections.degreeZeroToGlobalSections
                (grading L) (Stacks.TwistedSections.moduleGrading F L) (degreeZeroElem L F t))) =
          F.presheaf.map (homOfLE le_top).op (globalSection X F t)

Tag 01QK, a remark

Tag 01QK in the Stacks Project.

Stacks.SectionRingProjTheta.projTheta_app_eq_twistThetaInt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjTheta/TwistRemarkNormalization.lean, line 759. The attribute's comment: “assertion (i): the isomorphism f^O_Y(n) -> L^n of Tag 01QI (the degree-n component of clause (2) of Tag 01PZ, defined on U(psi)) equals theta_{L^n}, theta being the constructed comparison of Tag 01QJ read on f^O_Y(n) through the obvious identification O_Y(n) = (Gamma_*(X, L, L^n))~, for every integer n”.

In Situation Stacks Tag 01QH, the map f^*𝒪_Y(n) ⟶ 𝓛^{⊗ n} of Stacks Tag 01QI — the degree-n component of clause (2) of Stacks Tag 01PZ, projTheta, which lives on U(ψ) = ⋃_a X_a — is θ_{𝓛^{⊗ n}}: Tag 01QJ's comparison for 𝓛^{⊗ n}, read on f^*𝒪_Y(n) through the obvious identification 𝒪_Y(n) ≅ (Γ_*(X, 𝓛, 𝓛^{⊗ n}))~ (twistThetaInt), for every integer n. Since projTheta lives on U(ψ), the right side is θ_{𝓛^{⊗ n}} pulled back along the inclusion U(ψ) ⟶ X, with r_{L, ψ} : U(ψ) ⟶ Y identified with U(ψ) ⟶ X ⟶ Y and the pullback along an open immersion with the restriction.

theorem projTheta_app_eq_twistThetaInt (n : ℤ) :
    (Stacks.SectionRingProjMorphism.Theta.projTheta L).app n =
      ((Scheme.Modules.pullbackCongr (ι_comp_projHom_eq_glued L hL)).inv.app (twistY L n) ≫
    (Scheme.Modules.pullbackComp (canonicalSections L).coveringOpen.ι
      (projHomOfIsAmple L hL)).inv.app (twistY L n) ≫
    (Scheme.Modules.pullback (canonicalSections L).coveringOpen.ι).map (twistThetaInt L hL n) ≫
    (Scheme.Modules.restrictFunctorIsoPullback (canonicalSections L).coveringOpen.ι).inv.app
      (tensorPowerModule X L n))

Stacks.SectionRingProjTheta.twistSquareInt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjTheta/TwistRemarkSquareInt.lean, line 736. The attribute's comment: “assertion (ii): the square commutes -- theta_F (x) theta_{L^n} is the pullback of the multiplication of Equation 01MQ followed by theta_{F (x) L^n}, read through the obvious identification M(n) = Gamma_*(X, L, F (x) L^n), for every O_X-module F and every integer n, theta being the constructed comparison of Tag 01QJ”.

The twist square commutes, for every 𝒪_X-module 𝓕 and every integer n: θ_𝓕 ⊗ θ_{𝓛^{⊗ n}} is the pullback of the multiplication M̃ ⊗ 𝒪_Y(n) ⟶ M(n)~ of Equation 01MQ (twistTop) followed by θ_{𝓕 ⊗ 𝓛^{⊗ n}}, read through twistModuleIdent.

theorem twistSquareInt (F : X.Modules) (n : ℤ) :
    ((pullbackTildeComparison L hL).app F ⊗ₘ twistThetaInt L hL n) =
      twistTop L hL F n ≫
        (Scheme.Modules.pullback (projHomOfIsAmple L hL)).map (twistModuleIdent L F n).hom ≫
        (pullbackTildeComparison L hL).app (F ⊗ tensorPowerModule X L n)

Stacks.SectionRingProjTheta.pullbackComparison_tensorHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionRingProjTheta/TwistSquare.lean, line 478. The attribute's comment: “assertion (ii): the Remark's square commutes, at the Tag 01QJ comparison pullbackComparison, with the top arrow CONSTRUCTED as pullbackTwistTop — the tensorator of restriction along f composed with f^* of Equation 01MQ's multiplication map — rather than left arbitrary, which is what distinguishes this from the sibling file TwistCompatibility's not_forall_twistSquare. Three things are granted as named binders: (a) hmul, the compatibility of Tag 0B5I's family c with that multiplication map on Proj Γ_*(X, L), which is the characterisation of c that not_forall_twistSquare proves to be necessary and add_self_eq_zero_of_mulComm_neg proves is not stable under its perturbation; (b) the multiplication map itself as the binder mult, Equation 01MQ's moduleTwistMap being stated for the other of this repository's two tensor-product sheaves; (c) a monoidal structure on restriction along f as an instance binder, which Mathlib does not provide for Scheme.Modules.restrictFunctor. Assertion (i), that Tag 01QI's map f^*𝒪_Y(n) → 𝓛^{⊗n} is θ_{𝓛^{⊗n}}, is NOT covered: that map does not exist in this repository”.

Assertion (ii) of Stacks Tag 01QK, at the Tag 01QJ comparison.

With θ = Stacks.SectionRingProjQuasicoherent.pullbackComparison L hL c, the natural transformation f^* M̃ ⟶ 𝓕 that carries @[stacks 01QJ], and with the top arrow Stacks.SectionRingProjTheta.pullbackTwistTop built from Equation 01MQ's multiplication map mult, Stacks Tag 01QK's square commutes:

    θ_𝓕 ⊗ₘ θ_𝓖 = pullbackTwistTop mult ≫ θ_{𝓕 ⊗ 𝓖}.

Both lower corners of the Remark's square are the single object 𝓕 ⊗ 𝓖 and its bottom arrow is the identity, so this equation is the whole of assertion (ii).

The hypothesis hmul is the compatibility of Tag 0B5I's family c with mult, on Proj Γ_*(X, L), mentioning no θ. It is the characterisation of c that Stacks.SectionRingProjQuasicoherent.TwistCompatibility.not_forall_twistSquare proves to be necessary; mulComm_of_tensorHom_eq shows it is equivalent to the conclusion across the adjunction, so nothing weaker would do, and add_self_eq_zero_of_mulComm_neg shows it is destroyed by the negation of c that defeats an unconstrained binder.

theorem pullbackComparison_tensorHom
    (c : tildeFunctor L ⟶ Scheme.Modules.pushforward (projHomOfIsAmple L hL))
    (F G : X.Modules)
    (mult : (tildeFunctor L).obj F ⊗ (tildeFunctor L).obj G ⟶ (tildeFunctor L).obj (F ⊗ G))
    (hmul : mult ≫ c.app (F ⊗ G) = (c.app F ⊗ₘ c.app G) ≫
      μ (Scheme.Modules.pushforward (projHomOfIsAmple L hL)) F G) :
    (pullbackComparison L hL c).app F ⊗ₘ (pullbackComparison L hL c).app G
      = pullbackTwistTop L hL F G mult ≫ (pullbackComparison L hL c).app (F ⊗ G)

Tag 0AG5, a lemma

Tag 0AG5 in the Stacks Project.

Stacks.AlgebraicGeometry.ProjTwistComparisonCompact.isIso_integerComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorSectionNonvanishing/ProjTwistComparisonCompact.lean, line 412. The attribute's comment: “the comparison M̃ ⟶ ℱ of Tag 0B5I is an isomorphism, for Proj S quasi-compact and ℱ quasi-coherent”. References: EGA II (8.14.8), “special case”.

[Stacks, Tag 0AG5]. Let S be a graded ring such that X = Proj S is quasi-compact and let ℱ be a quasi-coherent 𝒪_X-module. Set M = ⨁_{n ∈ ℤ} Γ(X, ℱ(n)), the graded S-module of Section 01MM with its canonical graded module structure Stacks.AlgebraicGeometry.ProjTwistedSections.twistedGlobalSectionsModule of Tag 03GK. Then the comparison map M̃ ⟶ ℱ of Tag 0B5I is an isomorphism.

This is isIso_integerComparison_of_compactSpace at the canonical graded module structure, so nothing is quantified over beyond the graded ring and the sheaf: the hypotheses are exactly the source's, quasi-compactness of Proj S and quasi-coherence of ℱ.

public theorem isIso_integerComparison
    [CompactSpace (_root_.AlgebraicGeometry.Proj 𝒮)]
    (hqc : SheafOfModules.IsQuasicoherent
      (R := (_root_.AlgebraicGeometry.Proj 𝒮).ringCatSheaf) F) :
    IsIso (ProjTwistIntegerComparison.integerComparison 𝒮 F
      (ProjTwistedSections.twistedGlobalSectionsModule 𝒮 F))

Stacks.AlgebraicGeometry.ProjTwistComparisonCompact.twistSheafMap_integerComparison_degreeNToTwistedGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TensorSectionNonvanishing/ProjTwistComparisonCompact.lean, line 778. The attribute's comment: “part (2): if Proj S is covered by the standard opens D₊(f) with deg f = 1 then the induced maps M_n → Γ(X, ℱ(n)) are the identity maps”.

[Stacks, Tag 0AG5], second assertion, for the canonical graded module structure of Tag 03GK: if Proj S is covered by the standard opens of the degree-one elements then the induced maps M_n → Γ(X, ℱ(n)) are the identity maps.

This is twistSheafMap_integerComparison_degreeNToTwistedGlobalSections_of_module at the canonical graded module structure Stacks.AlgebraicGeometry.ProjTwistedSections.twistedGlobalSectionsModule, so nothing is quantified over beyond the graded ring, the sheaf and the source's own hypotheses.

public theorem twistSheafMap_integerComparison_degreeNToTwistedGlobalSections
    [CompactSpace (_root_.AlgebraicGeometry.Proj 𝒮)]
    (hqc : SheafOfModules.IsQuasicoherent
      (R := (_root_.AlgebraicGeometry.Proj 𝒮).ringCatSheaf) F)
    (hcover : DegreeOneCover 𝒮) (n : ℤ) (s : twistedSectionsComponent 𝒮 F n) :
    letI := (ProjTwistedSections.twistedGlobalSectionsModule 𝒮 F).moduleInst
    letI := (ProjTwistedSections.twistedGlobalSectionsModule 𝒮 F).gradedSMul
    (twistSheafMap 𝒮
          (integerComparison 𝒮 F (ProjTwistedSections.twistedGlobalSectionsModule 𝒮 F))
          n).val.app (op ⊤)
        (degreeNToTwistedGlobalSections 𝒮 (twistedGlobalSectionsGrading 𝒮 F) hcover n
          (ofTwistedSection 𝒮 F n s)) = s

Sources

• Section 28.29, Tag 01QG
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SectionRingVeroneseChart.twistComparison · Stacks.SectionRingVeroneseChart.twistComparison_mul · Stacks.SectionRingVeroneseChart.pbTwistUnit_twistComparison · Stacks.SectionRingProjGoodOpen.projHomOfIsAmple_preimage_whereInvertible · Stacks.SectionRingProjTwistIso.isIso_projTheta_app · Stacks.SectionRingVeroneseChart.isIso_twistComparison · Stacks.SectionRingProjQuasicoherent.pullbackComparison · Stacks.SectionRingProjQuasicoherent.pullbackTildeComparison_spec

Section28.30 Finding suitable affine opens#

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

Tag 01ZV, a lemma

Tag 01ZV in the Stacks Project.

AlgebraicGeometry.exists_pairwise_disjoint_affine_opens_of_generic_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/GenericPoints.lean, line 113. The attribute's comment: “pairwise disjoint neighborhoods”.

Stacks Project, Tag 01ZV. A finite family of distinct irreducible components of a quasi-separated scheme has pairwise disjoint affine open neighborhoods of its generic points; the union of these neighborhoods is affine.

theorem exists_pairwise_disjoint_affine_opens_of_generic_points
    [QuasiSeparatedSpace X] (Z : ι → Set X)
    (hZ : ∀ i, Z i ∈ irreducibleComponents X) (hZ_injective : Injective Z)
    (η : ι → X) (hη : ∀ i, IsGenericPoint (η i) (Z i)) :
    ∃ U : ι → X.Opens,
      (∀ i, AlgebraicGeometry.IsAffineOpen (U i)) ∧
      (∀ i, η i ∈ U i) ∧
      Pairwise (Disjoint on U) ∧
      AlgebraicGeometry.IsAffineOpen (iSup U)

AlgebraicGeometry.exists_affine_open_containing_generic_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/GenericPoints.lean, line 164. The attribute's comment: “common affine neighborhood”.

Stacks Project, Tag 01ZV. The generic points of a finite family of distinct irreducible components of a quasi-separated scheme lie in a single affine open.

theorem exists_affine_open_containing_generic_points
    [QuasiSeparatedSpace X] (Z : ι → Set X)
    (hZ : ∀ i, Z i ∈ irreducibleComponents X) (hZ_injective : Injective Z)
    (η : ι → X) (hη : ∀ i, IsGenericPoint (η i) (Z i)) :
    ∃ U : X.Opens, AlgebraicGeometry.IsAffineOpen U ∧ ∀ i, η i ∈ U

Tag 03J1, a lemma

Tag 03J1 in the Stacks Project.

AlgebraicGeometry.exists_dense_open_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AmpleAndExtension/SuitableAffineOpens.lean, line 138. References: SGA 3 VIB (5.8.3), “special case”.

A quasi-compact scheme has a separated dense open subscheme.

theorem exists_dense_open_isSeparated (X : Scheme.{u}) [CompactSpace X] :
    ∃ V : X.Opens, Dense (V : Set X) ∧ Scheme.IsSeparated V

Tag 01ZX, a lemma

Tag 01ZX in the Stacks Project.

AlgebraicGeometry.exists_affineOpen_mem_of_genericPoints_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/GenericPoints.lean, line 179.

Stacks Project, Tag 01ZX. In a quasi-separated scheme, any point and the generic points of finitely many pairwise distinct irreducible components are contained in a common affine open.

theorem exists_affineOpen_mem_of_genericPoints_irreducibleComponents
    (X : Scheme.{u}) [QuasiSeparatedSpace X] {n : ℕ}
    (Z : Fin n → Set X) (hZ : ∀ i, Z i ∈ irreducibleComponents X)
    (hZ_injective : Function.Injective Z)
    (η : Fin n → X) (hη : ∀ i, IsGenericPoint (η i) (Z i)) (x : X) :
    ∃ U : X.Opens, IsAffineOpen U ∧ x ∈ U ∧ ∀ i, η i ∈ U

Tag 01ZY, a lemma

Tag 01ZY in the Stacks Project.

Stacks.AmpleAffineAvoidance.exists_affineOpen_containing_finite_of_ample, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleAffineAvoidance/AmpleFiniteSet.lean, line 223. The attribute's comment: “part (3)”.

Stacks Tag 01ZY, part (3). A finite set of points of a scheme carrying an ample invertible 𝒪_X-module lies in an affine open.

theorem exists_affineOpen_containing_finite_of_ample (hL : IsAmple X L) {E : Set X}
    (hE : E.Finite) : ∃ U : X.Opens, IsAffineOpen U ∧ E ⊆ (U : Set X)

Stacks.AmpleCluster.exists_affineOpen_containing_finite_of_immersion_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCluster/ProjImmersion.lean, line 54. The attribute's comment: “part (4)”.

A finite set of points of a scheme X with an immersion X ⟶ Proj 𝒮 lies in an affine open of X.

theorem exists_affineOpen_containing_finite_of_immersion_proj {X : Scheme.{u}} {S : Type u}
    {σ : Type v} [CommRing S] [SetLike σ S] [AddSubgroupClass σ S] (𝒮 : ℕ → σ) [GradedRing 𝒮]
    (i : X ⟶ Proj 𝒮) [IsImmersion i] {E : Set X} (hE : E.Finite) :
    ∃ U : X.Opens, IsAffineOpen U ∧ E ⊆ (U : Set X)

Stacks.AmpleCluster.exists_affineOpen_containing_finite_of_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCluster/QuasiAffineAndImmersion.lean, line 86. The attribute's comment: “part (1)”.

Stacks Tag 01ZY, part (1). A finite set of points of a quasi-affine scheme lies in an affine open.

theorem exists_affineOpen_containing_finite_of_isQuasiAffine {X : Scheme.{u}} [X.IsQuasiAffine]
    {E : Set X} (hE : E.Finite) : ∃ U : X.Opens, IsAffineOpen U ∧ E ⊆ U

Stacks.AmpleCluster.exists_affineOpen_containing_finite_of_immersion_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleCluster/QuasiAffineAndImmersion.lean, line 95. The attribute's comment: “part (2)”.

Stacks Tag 01ZY, part (2). A finite set of points of a locally closed subscheme of an affine scheme lies in an affine open.

theorem exists_affineOpen_containing_finite_of_immersion_affine {X Y : Scheme.{u}} (i : X ⟶ Y)
    [IsImmersion i] [IsAffine Y] {E : Set X} (hE : E.Finite) :
    ∃ U : X.Opens, IsAffineOpen U ∧ E ⊆ U

AlgebraicGeometry.exists_isAffineOpen_of_isImmersion_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/FiniteSetInAffineOpen.lean, line 55. The attribute's comment: “case (2)”.

A scheme X with an immersion i : X ⟶ Y into an affine scheme Y (that is, isomorphic to a locally closed subscheme of an affine scheme) has every finite set of its points inside a single affine open.

theorem exists_isAffineOpen_of_isImmersion_of_isAffine {X Y : Scheme.{u}} [IsAffine Y]
    (i : X ⟶ Y) [IsImmersion i] {E : Set X} (hE : E.Finite) :
    ∃ U : X.Opens, IsAffineOpen U ∧ E ⊆ (U : Set X)

AlgebraicGeometry.exists_isAffineOpen_of_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/FiniteSetInAffineOpen.lean, line 67. The attribute's comment: “case (1)”.

A quasi-affine scheme has every finite set of its points inside a single affine open.

theorem exists_isAffineOpen_of_isQuasiAffine (X : Scheme.{u}) [X.IsQuasiAffine] {E : Set X}
    (hE : E.Finite) : ∃ U : X.Opens, IsAffineOpen U ∧ E ⊆ (U : Set X)

Tag 09NV, a lemma

Tag 09NV in the Stacks Project.

Stacks.AmpleFiniteAffineNonvanishing.exists_affine_nonvanishingOpen_containing_finite_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleFiniteAffineNonvanishing/Basic.lean, line 111. References: EGA II (4.5.4).

Let L be an ample invertible 𝒪_X-module on a scheme X. A finite subset E of an open W of X lies in an affine ringed-space nonvanishing locus of a section of a positive tensor power of L, with that locus contained in W.

theorem exists_affine_nonvanishingOpen_containing_finite_sections (hL : IsAmple X L) {E : Set X}
    (hE : E.Finite) (W : X.Opens) (hEW : E ⊆ (W : Set X)) :
    ∃ n : ℕ, 1 ≤ n ∧
      ∃ s : (toSheafOfModules X (tensorPowModule X L (n : ℤ))).sections,
        IsAffineOpen (Stacks.NonvanishingTrivialize.nonvanishingOpen X.toRingedSpace
            (toSheafOfModules X (tensorPowModule X L (n : ℤ))) s) ∧
          E ⊆ (Stacks.NonvanishingTrivialize.nonvanishingOpen X.toRingedSpace
            (toSheafOfModules X (tensorPowModule X L (n : ℤ))) s : Set X) ∧
            (Stacks.NonvanishingTrivialize.nonvanishingOpen X.toRingedSpace
              (toSheafOfModules X (tensorPowModule X L (n : ℤ))) s : Set X) ⊆ (W : Set X)

Stacks.SheafOfModules.Invertible.exists_sections_finite_subset_nonvanishingOpen_le_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionExtension/FiniteSet.lean, line 148. References: EGA II (4.5.4).

Let L be an ample invertible module on a scheme Y, and let E ⊆ W ⊆ Y with E finite and W open. Then there are an n ≥ 1 and a global section s of L^{⊗ n} whose nonvanishing locus is affine and satisfies E ⊆ Y_s ⊆ W.

theorem exists_sections_finite_subset_nonvanishingOpen_le_of_isAmple
    (hL : AlgebraicGeometry.Scheme.Modules.IsAmple Y M)
    {E : Set Y} (hE : E.Finite) (W : Y.Opens) (hEW : E ⊆ W) :
    ∃ (m : ℕ) (_ : 1 ≤ m) (s : Mpow[m].sections),
      IsAffineOpen NV[m, s] ∧ E ⊆ (NV[m, s] : Set Y) ∧ (NV[m, s] : Set Y) ⊆ W

Tag 0F20, a lemma

Tag 0F20 in the Stacks Project.

Stacks.QuasiAffineGlobalGeneration.exists_affine_nonvanishingOpen_containing_finite_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiAffineGlobalGeneration/Basic.lean, line 106.

Stacks Tag 0F20, at the ringed-space spelling: over L.sections, with the ringed-space nonvanishing open of Stacks Tag 01CY. Transported from Stacks.QuasiAffineGlobalGeneration.exists_affine_nonvanishingOpen_containing_finite along Stacks.NonvanishingSpelling.nonvanishingOpen_symm_eq.

theorem exists_affine_nonvanishingOpen_containing_finite_sections [X.IsQuasiAffine]
    (L : X.Modules) [IsInvertibleModule X L] {E : Set X} (hE : E.Finite) (W : X.Opens)
    (hEW : E ⊆ (W : Set X)) :
    ∃ s : (toSheafOfModules X L).sections,
      IsAffineOpen (Stacks.NonvanishingTrivialize.nonvanishingOpen X.toRingedSpace
        (toSheafOfModules X L) s) ∧
      E ⊆ (Stacks.NonvanishingTrivialize.nonvanishingOpen X.toRingedSpace
        (toSheafOfModules X L) s : Set X) ∧
      Stacks.NonvanishingTrivialize.nonvanishingOpen X.toRingedSpace
        (toSheafOfModules X L) s ≤ W

Tag 0BX3, a lemma

Tag 0BX3 in the Stacks Project.

AlgebraicGeometry.exists_affineOpen_germ_injective_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/GermInjective.lean, line 37. The attribute's comment: “part (1)”.

On an integral scheme, every point admits an affine open neighbourhood whose canonical map from its ring of sections to the local ring at the point is injective.

theorem exists_affineOpen_germ_injective_of_isIntegral (X : Scheme.{u}) (x : X)
    [IsIntegral X] :
    ∃ (U : X.Opens) (hx : x ∈ U),
      IsAffineOpen U ∧ Function.Injective (X.presheaf.germ U x hx)

AlgebraicGeometry.exists_affineOpen_germ_injective_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/GermInjective.lean, line 46. The attribute's comment: “part (2)”.

On a locally Noetherian scheme, every point admits an affine open neighbourhood whose canonical map from its ring of sections to the local ring at the point is injective.

theorem exists_affineOpen_germ_injective_of_isLocallyNoetherian (X : Scheme.{u}) (x : X)
    [IsLocallyNoetherian X] :
    ∃ (U : X.Opens) (hx : x ∈ U),
      IsAffineOpen U ∧ Function.Injective (X.presheaf.germ U x hx)

AlgebraicGeometry.exists_affineOpen_germ_injective_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/GermInjective.lean, line 56. The attribute's comment: “part (3)”.

On a reduced scheme with finitely many irreducible components, every point admits an affine open neighbourhood whose canonical map from its ring of sections to the local ring at the point is injective.

theorem exists_affineOpen_germ_injective_of_isReduced (X : Scheme.{u}) (x : X)
    [IsReduced X] (hX : (irreducibleComponents X).Finite) :
    ∃ (U : X.Opens) (hx : x ∈ U),
      IsAffineOpen U ∧ Function.Injective (X.presheaf.germ U x hx)

Tag 0H9B, a lemma

Tag 0H9B in the Stacks Project.

AlgebraicGeometry.exists_isAffineOpen_mapped_to_basicOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Properties/AffineNeighborhood.lean, line 50.

A point of a scheme admitting open immersions into two affine schemes has an affine open neighbourhood whose image in each scheme is a basic open.

theorem exists_isAffineOpen_mapped_to_basicOpens
    (U V W : Scheme.{u}) [IsAffine U] [IsAffine V]
    (i : W ⟶ U) (j : W ⟶ V) [IsOpenImmersion i] [IsOpenImmersion j] (w : W) :
    ∃ (W' : W.Opens) (f : Γ(U, ⊤)) (g : Γ(V, ⊤)),
      IsAffineOpen W' ∧ w ∈ W' ∧
        i.opensFunctor.obj W' = U.basicOpen f ∧
        j.opensFunctor.obj W' = V.basicOpen g

Sources

• Section 28.30, Tag 01ZU
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_pairwise_disjoint_affine_opens_of_generic_points · AlgebraicGeometry.exists_affine_open_containing_generic_points · AlgebraicGeometry.exists_dense_open_isSeparated · AlgebraicGeometry.exists_affineOpen_mem_of_genericPoints_irreducibleComponents · Stacks.AmpleAffineAvoidance.exists_affineOpen_containing_finite_of_ample · Stacks.AmpleCluster.exists_affineOpen_containing_finite_of_immersion_proj · Stacks.AmpleCluster.exists_affineOpen_containing_finite_of_isQuasiAffine · Stacks.AmpleCluster.exists_affineOpen_containing_finite_of_immersion_affine

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.