56 Functors and Morphisms

Chapter 56 of the Stacks Project, Functors and Morphisms, Tag 0GNG: the 6 sections of its 7 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 44 tags are carried by 100 declarations of the repository (all in StacksFrontier) and 10 registered declarations.

Section56.2 Functors on module categories#

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

Tag 0GNJ, a lemma

Tag 0GNJ in the Stacks Project.

ModuleCat.filteredColimitExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/Extension.lean, line 71. The attribute's comment: “existence”. References: SGA 4 I (8.7.3), “existence, C=Mod^fp_A”.

A functor on finitely presented modules has an extension to all modules which preserves filtered colimits.

public noncomputable def filteredColimitExtension
    [HasFilteredColimitsOfSize.{max u v, max u v} B]
    (F : CategoryTheory.Functor (FinitelyPresentedModuleCat.{u, max u v} A) B) :
    FilteredColimitExtension A F

ModuleCat.FilteredColimitExtension.existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/Extension.lean, line 89. The attribute's comment: “uniqueness”. References: SGA 4 I (8.7.3), “uniqueness, C=Mod^fp_A”; SGA 4 I (8.7.2), “special case”.

Two filtered-colimit-preserving extensions are related by a unique natural isomorphism compatible with their specified identifications on finitely presented modules.

public theorem FilteredColimitExtension.existsUnique_iso
    {F : CategoryTheory.Functor (FinitelyPresentedModuleCat.{u, max u v} A) B}
    (E₁ E₂ : FilteredColimitExtension A F) :
    ∃! e : CategoryTheory.Iso E₁.functor E₂.functor,
      Functor.whiskerLeft (finitelyPresentedModule.{u, max u v} A).ι e.hom =
        (CategoryTheory.Iso.trans E₁.iso E₂.iso.symm).hom
Tag 0GNK, a lemma

Tag 0GNK in the Stacks Project.

ModuleCat.filteredColimitExtension_additive, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/Additivity.lean, line 215. The attribute's comment: “additivity”.

A filtered-colimit-preserving extension of an additive functor from finitely presented modules is additive.

public lemma filteredColimitExtension_additive
    (E : FilteredColimitExtension A F) [F.Additive] :
    E.functor.Additive

ModuleCat.filteredColimitExtension_preservesCoproducts, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/Additivity.lean, line 222. The attribute's comment: “arbitrary direct sums”.

A filtered-colimit-preserving extension of an additive functor from finitely presented modules preserves arbitrary direct sums.

public lemma filteredColimitExtension_preservesCoproducts
    (E : FilteredColimitExtension A F) [F.Additive]
    (J : Type (max u v)) :
    PreservesColimitsOfShape (Discrete J) E.functor
Tag 0GNL, a lemma

Tag 0GNL in the Stacks Project.

ModuleCat.filteredColimitExtension_functor_additive, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/RightExact.lean, line 620. The attribute's comment: “additivity”.

The extension of a right exact functor on finitely presented modules to all modules is additive.

public lemma filteredColimitExtension_functor_additive :
    (filteredColimitExtension A G).functor.Additive

ModuleCat.filteredColimitExtension_functor_preservesFiniteColimits, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/RightExact.lean, line 627. The attribute's comment: “right exactness”.

The extension of a right exact functor on finitely presented modules to all modules is right exact.

public lemma filteredColimitExtension_functor_preservesFiniteColimits :
    PreservesFiniteColimits (filteredColimitExtension A G).functor

ModuleCat.filteredColimitExtension_functor_preservesCoproducts, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/RightExact.lean, line 634. The attribute's comment: “arbitrary direct sums”.

The extension of a right exact functor on finitely presented modules to all modules commutes with arbitrary direct sums.

public lemma filteredColimitExtension_functor_preservesCoproducts (J : Type (max u v)) :
    PreservesColimitsOfShape (Discrete J) (filteredColimitExtension A G).functor
Tag 0GNM, a lemma

Tag 0GNM in the Stacks Project.

ModuleCat.filteredColimitExtension_preservesFiniteLimits, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/LeftExact.lean, line 385. The attribute's comment: “left exactness”.

If filtered colimits commute with kernels in the target, the filtered-colimit extension of a left exact functor on finitely presented modules is left exact.

public lemma filteredColimitExtension_preservesFiniteLimits
    [IsCoherentRing A] (E : FilteredColimitExtension A F) [HasKernels B]
    [PreservesFiniteLimits F]
    [HasFilteredColimitsOfSize.{max u v, max u v} B]
    [∀ (J : Type (max u v)) [Category.{max u v} J] [IsFiltered J],
      ∀ {X Y : J ⥤ B} (f : X ⟶ Y),
        PreservesLimit (parallelPair f 0) (colim : (J ⥤ B) ⥤ B)] :
    PreservesFiniteLimits E.functor

Declarations registered for the tag:

Tag 0GNN, a lemma

Tag 0GNN in the Stacks Project.

ModuleCat.rightExactFunctor_additive, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/ModuleAction.lean, line 235. The attribute's comment: “automatic additivity”.

A right exact functor on finitely presented modules is automatically additive.

public lemma rightExactFunctor_additive (A : Type u) (B : Type v) [Ring A]
    [Category.{w} B] [Preadditive B] [HasFiniteBiproducts B]
    (F : FPModule A ⥤ᵣ B) : F.obj.Additive

ModuleCat.evaluationFunctor_isEquivalence, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/ModuleActionEquivalence.lean, line 889.

Evaluation on the rank-one free module, with its natural action, classifies right exact functors on finitely presented modules.

public lemma evaluationFunctor_isEquivalence (A : Type u) (B : Type v) [Ring A]
    [Category.{w} B] [Preadditive B] [HasFiniteBiproducts B] [HasCokernels B] :
    (evaluationFunctor A B).IsEquivalence
Tag 0GNQ, a lemma

Tag 0GNQ in the Stacks Project.

ModuleCat.functorToRingActions_isEquivalence, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/RingActions.lean, line 475. References: EGA III (7.2.6).

Evaluation on the right regular module, with its natural A-action, classifies right exact functors which preserve arbitrary coproducts.

public lemma functorToRingActions_isEquivalence :
    (functorToRingActions A B).IsEquivalence
Sources
LeanModuleCat.filteredColimitExtension · ModuleCat.FilteredColimitExtension.existsUnique_iso · ModuleCat.filteredColimitExtension_additive · ModuleCat.filteredColimitExtension_preservesCoproducts · ModuleCat.filteredColimitExtension_functor_additive · ModuleCat.filteredColimitExtension_functor_preservesFiniteColimits · ModuleCat.filteredColimitExtension_functor_preservesCoproducts · ModuleCat.filteredColimitExtension_preservesFiniteLimits

Section56.3 Functors between categories of modules#

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

Tag 0GNS, a lemma

Tag 0GNS in the Stacks Project.

ModuleCat.tfae_iso_tensorFunctor_preserves_colimits_isLeftAdjoint, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/BimoduleTensor.lean, line 311. References: EGA III (7.3.1), “(a) <=> (e)”; EGA III (7.2.6), “(1) <=> (2)”; EGA III (7.2.5), “(a) <=> (c)”.

A functor between module categories is tensoring with a bimodule iff it is right exact and commutes with arbitrary direct sums; these are also equivalent to preserving all colimits and to having a right adjoint.

public lemma tfae_iso_tensorFunctor_preserves_colimits_isLeftAdjoint
    (F : ModuleCat.{u} A ⥤ ModuleCat.{u} B) :
    List.TFAE
      [ ∃ K : ModuleCat.{u} (A ⊗[ℤ] B),
          Nonempty (tensorFunctorOverInt A B K ≅ F),
        PreservesFiniteColimits F ∧
          ∀ J : Type u, PreservesColimitsOfShape (Discrete J) F,
        PreservesColimits F,
        F.IsLeftAdjoint ]
Tag 0GNT, an example

Tag 0GNT in the Stacks Project.

ModuleCat.tensorFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/TensorFunctor.lean, line 72. The attribute's comment: “the functor”.

Tensoring with an A ⊗[R] B-module, regarded as a functor from A-modules to B-modules.

public noncomputable def tensorFunctor
    (K : ModuleCat.{u} (A ⊗[R] B)) : ModuleCat.{u} A ⥤ ModuleCat.{u} B

ModuleCat.tensorFunctor_linear, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/TensorFunctor.lean, line 82. The attribute's comment: “R-linearity”.

Tensoring with an A ⊗[R] B-module is R-linear.

public lemma tensorFunctor_linear (K : ModuleCat.{u} (A ⊗[R] B)) :
    (tensorFunctor R A B K).Linear R

ModuleCat.tensorFunctor_preservesFiniteColimits, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/TensorFunctor.lean, line 95. The attribute's comment: “right exactness”.

Tensoring with an A ⊗[R] B-module is right exact.

public lemma tensorFunctor_preservesFiniteColimits (K : ModuleCat.{u} (A ⊗[R] B)) :
    PreservesFiniteColimits (tensorFunctor R A B K)

ModuleCat.tensorFunctor_preservesDirectSums, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/TensorFunctor.lean, line 100. The attribute's comment: “arbitrary direct sums”.

Tensoring with an A ⊗[R] B-module commutes with arbitrary direct sums.

public lemma tensorFunctor_preservesDirectSums (K : ModuleCat.{u} (A ⊗[R] B))
    (J : Type u) :
    PreservesColimitsOfShape (Discrete J) (tensorFunctor R A B K)

ModuleCat.tensorFunctor_preservesColimits, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/TensorFunctor.lean, line 107. The attribute's comment: “all colimits”.

Tensoring with an A ⊗[R] B-module commutes with all colimits.

public lemma tensorFunctor_preservesColimits (K : ModuleCat.{u} (A ⊗[R] B)) :
    PreservesColimits (tensorFunctor R A B K)

ModuleCat.tensorFunctor_isLeftAdjoint, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/TensorFunctor.lean, line 112. The attribute's comment: “right adjoint”.

Tensoring with an A ⊗[R] B-module has a right adjoint.

public lemma tensorFunctor_isLeftAdjoint (K : ModuleCat.{u} (A ⊗[R] B)) :
    (tensorFunctor R A B K).IsLeftAdjoint
Tag 0GNV, a lemma

Tag 0GNV in the Stacks Project.

ModuleCat.tensorFunctorEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/LinearTensorEquivalence.lean, line 782. The attribute's comment: “the equivalence”. References: EGA III (7.2.6), “commutative rings”.

Modules over A ⊗[R] B are equivalent to R-linear right exact functors from A-modules to B-modules which preserve arbitrary direct sums.

public noncomputable def tensorFunctorEquivalence :
    ModuleCat.{u} (A ⊗[R] B) ≌
      ObjectProperty.FullSubcategory
        (IsLinearRightExactAndPreservesDirectSums R A B)

ModuleCat.tensorFunctorEquivalence_functorIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/LinearTensorEquivalence.lean, line 793. The attribute's comment: “given by tensoring”. References: EGA III (7.2.6), “N ↦ T_N”.

The functor underlying tensorFunctorEquivalence is naturally isomorphic to the functor which sends a module K to tensoring with K.

public lemma tensorFunctorEquivalence_functorIso :
    Nonempty
      ((tensorFunctorEquivalence R A B).functor ≅ moduleTensorFunctorLift R A B)
Tag 0GNW, a remark

Tag 0GNW in the Stacks Project.

ModuleCat.moduleTensorFunctor_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/TensorComposition.lean, line 254.

The tensor product over the middle algebra represents the composite of two tensor functors. The equation on pure tensors records the canonical action of A ⊗[R] C, and the functor isomorphism includes naturality in the input A-module.

public lemma moduleTensorFunctor_comp
    (K : ModuleCat.{u} (A ⊗[R] B)) (K' : ModuleCat.{u} (B ⊗[R] C)) :
    letI : Module A K := Module.compHom K
      (Algebra.TensorProduct.includeLeftRingHom (R := R) (A := A) (B := B))
    letI : Module B K := Module.compHom K
      (Algebra.TensorProduct.includeRight (R := R) (A := A) (B := B)).toRingHom
    letI : Module B K' := Module.compHom K'
      (Algebra.TensorProduct.includeLeftRingHom (R := R) (A := B) (B := C))
    letI : Module C K' := Module.compHom K'
      (Algebra.TensorProduct.includeRight (R := R) (A := B) (B := C)).toRingHom
    ∃ inst : Module (A ⊗[R] C) (K ⊗[B] K'),
      letI : Module (A ⊗[R] C) (K ⊗[B] K') := inst
      (∀ (a : A) (c : C) (k : K) (k' : K'),
        (a ⊗ₜ[R] c) • (k ⊗ₜ[B] k') = (a • k) ⊗ₜ[B] (c • k')) ∧
      Nonempty
        ((moduleTensorFunctor R A C).obj
            (ModuleCat.of (A ⊗[R] C) (K ⊗[B] K')) ≅
          ((moduleTensorFunctor R A B).obj K ⋙
            (moduleTensorFunctor R B C).obj K'))
Tag 0GNX, a remark

Tag 0GNX in the Stacks Project.

ModuleCat.tensorFunctor_exact_iff_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/TensorFunctorExactness.lean, line 139. References: EGA 0 (6.1.1), “more general”.

Tensoring with an A ⊗[R] B-module K is an exact functor from A-modules to B-modules if and only if K is flat as an A-module.

public theorem tensorFunctor_exact_iff_flat
    (R A B : Type u) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (K : ModuleCat.{u} (A ⊗[R] B)) :
    exactFunctor (ModuleCat.{u} A) (ModuleCat.{u} B) (tensorFunctor R A B K) ↔
      Module.Flat A ((restrictScalars
        (Algebra.TensorProduct.includeLeftRingHom (R := R) (A := A) (B := B))).obj K)
Tag 0GP0, a lemma

Tag 0GP0 in the Stacks Project.

ModuleCat.exists_ringEquiv_invertible_iso_extensionTensorFunctor, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/ModuleEquivalences.lean, line 627.

Stacks Project, Tag 0GP0. Every equivalence between categories of modules is extension of scalars along an isomorphism of the rings, followed by tensoring with an invertible module.

public lemma exists_ringEquiv_invertible_iso_extensionTensorFunctor
    (A B : Type u) [CommRing A] [CommRing B]
    (F : ModuleCat.{u} A ⥤ ModuleCat.{u} B) [F.IsEquivalence] :
    ∃ (e : A ≃+* B) (L : ModuleCat.{u} B),
      Module.Invertible B L ∧ Nonempty (F ≅ extensionTensorFunctor A B e L)
Tag 0GP1, a lemma

Tag 0GP1 in the Stacks Project.

ModuleCat.exists_algEquiv_invertible_iso_extensionTensorFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/LinearModuleEquivalences.lean, line 89.

Stacks Project, Tag 0GP1. An equivalence of module categories linear over the base ring is extension of scalars along an algebra isomorphism, followed by tensoring with an invertible module.

public theorem exists_algEquiv_invertible_iso_extensionTensorFunctor
    (R : Type v) (A B : Type u) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B]
    (F : ModuleCat.{u} A ⥤ ModuleCat.{u} B) [F.IsEquivalence]
    [F.Linear R] :
    ∃ (e : A ≃ₐ[R] B) (L : ModuleCat.{u} B),
      Module.Invertible B L ∧
        Nonempty (F ≅ extensionTensorFunctor A B e.toRingEquiv L)
Tag 0GP2, a remark

Tag 0GP2 in the Stacks Project.

ModuleCat.monoidHomOfMonoidal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 101. The attribute's comment: “part (2): multiplicative scalar map”.

A monoidal functor canonically induces a multiplicative map on scalars.

public noncomputable def monoidHomOfMonoidal
    (F : ModuleCat.{u} A ⥤ ModuleCat.{u} B) [F.Monoidal] :
    { φ : A →* B // ∀ a, φ a = scalarValue F a }

ModuleCat.scalarValue_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 147. The attribute's comment: “part (4): additive scalar map”.

The scalar map of an additive monoidal functor preserves addition.

public theorem scalarValue_add (F : ModuleCat.{u} A ⥤ ModuleCat.{u} B)
    [F.Monoidal] [F.Additive] (a b : A) :
    scalarValue F (a + b) = scalarValue F a + scalarValue F b

ModuleCat.ringHomOfAdditive, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 172. The attribute's comment: “part (4): ring homomorphism”.

An additive monoidal functor induces a ring homomorphism.

public noncomputable def ringHomOfAdditive
    (F : ModuleCat.{u} A ⥤ ModuleCat.{u} B) [F.Monoidal] [F.Additive] :
    { φ : A →+* B // ∀ a, φ a = scalarValue F a }

ModuleCat.tensorSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 185. The attribute's comment: “part (3): tensor-square example”.

Tensor squaring is a monoidal functor whose scalar map is squaring.

public theorem tensorSquare (A : Type u) [CommRing A] :
    ∃ h : (tensorSquareFunctor A).Monoidal,
      ∀ a : A, letI : (tensorSquareFunctor A).Monoidal := h
        scalarValue (tensorSquareFunctor A) a = a ^ 2

ModuleCat.torsionFreeQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 302. The attribute's comment: “part (5): monoidal torsion-free quotient”.

Quotienting abelian groups by torsion is monoidal.

public theorem torsionFreeQuotient :
    Nonempty torsionFreeQuotientFunctor.{u}.Monoidal

ModuleCat.torsionFreeQuotient_scalarValue, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 383. The attribute's comment: “part (5): induced scalar map is the identity”.

For any monoidal structure on torsion-free quotient, conjugating the image of each scalar endomorphism of the monoidal unit gives that same scalar endomorphism. This expresses that the induced scalar map is the identity in every module universe.

public theorem torsionFreeQuotient_scalarValue
    (h : torsionFreeQuotientFunctor.{u}.Monoidal) (a : ℤ) :
    letI : torsionFreeQuotientFunctor.{u}.Monoidal := h
    (Functor.Monoidal.εIso torsionFreeQuotientFunctor.{u}).hom ≫
      torsionFreeQuotientFunctor.{u}.map
        (a • (𝟙 (𝟙_ (ModuleCat.{u} ℤ)))) ≫
      (Functor.Monoidal.εIso torsionFreeQuotientFunctor.{u}).inv =
        a • (𝟙 (𝟙_ (ModuleCat.{u} ℤ)))

ModuleCat.torsionFreeQuotient_scalar_action, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 409. The attribute's comment: “part (5): scalar endomorphisms on all modules”.

Torsion-free quotient preserves multiplication by every integer on every module.

public theorem torsionFreeQuotient_scalar_action (M : ModuleCat.{u} ℤ) (a : ℤ) :
    torsionFreeQuotientFunctor.{u}.map
        (ModuleCat.ofHom (a • (LinearMap.id : M →ₗ[ℤ] M))) =
      ModuleCat.ofHom (a • (LinearMap.id :
        torsionFreeQuotientFunctor.{u}.obj M →ₗ[ℤ]
          torsionFreeQuotientFunctor.{u}.obj M))

ModuleCat.torsionFreeQuotient_not_iso_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 419. The attribute's comment: “part (5): nonidentity example”.

Torsion-free quotient is not naturally isomorphic to the identity functor.

public theorem torsionFreeQuotient_not_iso_id :
    ¬ Nonempty (torsionFreeQuotientFunctor.{u} ≅ 𝟭 (ModuleCat.{u} ℤ))

ModuleCat.iso_extendScalars_of_rightExact_preservesDirectSums, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 634. The attribute's comment: “part (6): extension of scalars”.

A right-exact monoidal functor commuting with direct sums is extension of scalars along its induced ring map, compatibly with the monoidal structures.

public theorem iso_extendScalars_of_rightExact_preservesDirectSums
    (F : ModuleCat.{u} A ⥤ ModuleCat.{u} B) [F.Monoidal]
    [PreservesFiniteColimits F]
    (hF : ∀ J : Type u, PreservesColimitsOfShape (Discrete J) F) :
    ∃ φ : A →+* B,
      (∀ a, φ a = scalarValue F a) ∧
        ∃ i : F ≅ ModuleCat.extendScalars φ,
          NatTrans.IsMonoidal i.hom

ModuleCat.extendScalars_injective_up_to_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 672. The attribute's comment: “classification: uniqueness”.

Ring maps are uniquely determined by the corresponding monoidal extension-of-scalars functors, up to natural isomorphism.

public theorem extendScalars_injective_up_to_iso (φ ψ : A →+* B)
    (h : Nonempty (ModuleCat.extendScalars.{u, u, u} φ ≅
      ModuleCat.extendScalars.{u, u, u} ψ)) :
    φ = ψ

ModuleCat.extendScalars_monoidal_preservesColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsBetweenCategories/MonoidalFunctors.lean, line 694. The attribute's comment: “classification: existence”.

Every ring map gives a cocontinuous monoidal extension-of-scalars functor.

public theorem extendScalars_monoidal_preservesColimits (φ : A →+* B) :
    Nonempty (ModuleCat.extendScalars.{u, u, u} φ).Monoidal ∧
      PreservesColimits (ModuleCat.extendScalars.{u, u, u} φ)

Declarations registered for the tag:

Sources
LeanModuleCat.tfae_iso_tensorFunctor_preserves_colimits_isLeftAdjoint · ModuleCat.tensorFunctor · ModuleCat.tensorFunctor_linear · ModuleCat.tensorFunctor_preservesFiniteColimits · ModuleCat.tensorFunctor_preservesDirectSums · ModuleCat.tensorFunctor_preservesColimits · ModuleCat.tensorFunctor_isLeftAdjoint · ModuleCat.tensorFunctorEquivalence

Section56.4 Extending functors on categories of modules#

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

Tag 0GP4, a lemma

Tag 0GP4 in the Stacks Project.

ModuleCat.filteredColimitExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/Extension.lean, line 71. The attribute's comment: “existence, at the target category of all B-modules”. References: SGA 4 I (8.7.3), “existence, C=Mod^fp_A”.

A functor on finitely presented modules has an extension to all modules which preserves filtered colimits.

public noncomputable def filteredColimitExtension
    [HasFilteredColimitsOfSize.{max u v, max u v} B]
    (F : CategoryTheory.Functor (FinitelyPresentedModuleCat.{u, max u v} A) B) :
    FilteredColimitExtension A F

ModuleCat.FilteredColimitExtension.existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/FunctorsModuleCategories/Extension.lean, line 89. The attribute's comment: “existence, at the target category of all B-modules”. References: SGA 4 I (8.7.3), “uniqueness, C=Mod^fp_A”; SGA 4 I (8.7.2), “special case”.

Two filtered-colimit-preserving extensions are related by a unique natural isomorphism compatible with their specified identifications on finitely presented modules.

public theorem FilteredColimitExtension.existsUnique_iso
    {F : CategoryTheory.Functor (FinitelyPresentedModuleCat.{u, max u v} A) B}
    (E₁ E₂ : FilteredColimitExtension A F) :
    ∃! e : CategoryTheory.Iso E₁.functor E₂.functor,
      Functor.whiskerLeft (finitelyPresentedModule.{u, max u v} A).ι e.hom =
        (CategoryTheory.Iso.trans E₁.iso E₂.iso.symm).hom
Tag 0GP5, a remark

Tag 0GP5 in the Stacks Project.

ModuleCat.finitelyPresentedModule_isMonoidal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/Monoidal.lean, line 153. The attribute's comment: “monoidal structure on finitely presented modules”.

Finitely presented modules form a monoidal full subcategory of modules.

instance finitelyPresentedModule_isMonoidal :
    (finitelyPresentedModule.{u, max u v} R).IsMonoidal

ModuleCat.filteredColimitExtension_monoidal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/Monoidal.lean, line 302. The attribute's comment: “monoidal extension”.

A monoidal functor on finitely presented modules has a monoidal filtered-colimit-preserving extension to all modules.

theorem filteredColimitExtension_monoidal
    (F : FinitelyPresentedModuleCat.{u, max u v} R ⥤
      FinitelyPresentedModuleCat.{w, max w x} S)
    [F.Monoidal]
    (E : FilteredColimitExtension R
      (F ⋙ (finitelyPresentedModule.{w, max w x} S).ι)) :
    ∃ h : E.functor.Monoidal,
      letI := h
      NatTrans.IsMonoidal E.iso.hom
Tag 0GP6, a lemma

Tag 0GP6 in the Stacks Project.

Declarations registered for the tag:

Tag 0GP8, a lemma

Tag 0GP8 in the Stacks Project.

ModuleCat.filteredColimitExtension_preservesFiniteLimits_moduleValued, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/LeftExactness.lean, line 204.

Stacks Project, Tag 0GP8. The filtered-colimit-preserving extension of a left exact functor on finitely presented modules is left exact when the source ring is coherent. This is the module-valued form: the functor takes values in all modules over the second ring, not only in the finitely presented ones.

theorem filteredColimitExtension_preservesFiniteLimits_moduleValued
    (A : Type u) [CommRing A] [IsCoherentRing A]
    (B : Type w) [Ring B]
    (F : FinitelyPresentedModuleCat.{u, max u v} A ⥤
      ModuleCat.{max w x} B)
    (E : FilteredColimitExtension A F)
    [PreservesFiniteLimits F] :
    PreservesFiniteLimits E.functor
Tag 0GP9, a lemma

Tag 0GP9 in the Stacks Project.

ModuleCat.fgFilteredColimitExtension_additive, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/Additivity.lean, line 46. The attribute's comment: “additivity”.

Stacks Project, Tag 0GP9. Every filtered-colimit-preserving extension of an additive functor on finite modules is additive.

instance fgFilteredColimitExtension_additive
    {F : FGModuleCat.{v} A ⥤ FGModuleCat.{v} B}
    (E : FGFilteredColimitExtension.{u, v, w} A B F) [F.Additive] :
    E.functor.Additive

ModuleCat.FGFilteredColimitExtension.preservesCoproducts, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/DirectSums.lean, line 44. The attribute's comment: “direct_sums”.

Stacks Project, Tag 0GP9. An additive functor on finite modules has a direct-sum-preserving filtered-colimit extension to all modules.

lemma FGFilteredColimitExtension.preservesCoproducts
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (B : Type w) [CommRing B]
    {F : FGModuleCat.{v} A ⥤ FGModuleCat.{v} B}
    (E : FGFilteredColimitExtension.{u, v, w} A B F)
    [F.Additive] (J : Type v) :
    PreservesColimitsOfShape (Discrete J) E.functor

ModuleCat.FGFilteredColimitExtension.exactFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/ExactFunctor.lean, line 43. The attribute's comment: “exactness”.

Stacks Project, Tag 0GP9. A filtered-colimit extension of an exact functor between finite module categories over Noetherian rings is exact.

theorem FGFilteredColimitExtension.exactFunctor
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (B : Type w) [CommRing B] [IsNoetherianRing B]
    (F : FGModuleCat.{v} A ⥤ FGModuleCat.{v} B)
    (E : FGFilteredColimitExtension.{u, v, w} A B F)
    (hF : exactFunctor (FGModuleCat.{v} A) (FGModuleCat.{v} B) F) :
    exactFunctor (ModuleCat.{v} A) (ModuleCat.{v} B) E.functor

ModuleCat.fgFilteredColimitExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/Extension.lean, line 384. The attribute's comment: “extension”.

Stacks Project, Tag 0GP9. A functor between finite module categories over Noetherian rings extends to all modules and commutes with filtered colimits.

noncomputable def fgFilteredColimitExtension
    [IsNoetherianRing A]
    (F : FGModuleCat.{v} A ⥤ FGModuleCat.{v} B) :
    FGFilteredColimitExtension.{u, v, w} A B F

ModuleCat.FGFilteredColimitExtension.existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/Extension.lean, line 443. The attribute's comment: “extension”.

Stacks Project, Tag 0GP9. Two filtered-colimit-preserving extensions are related by a unique natural isomorphism compatible with their specified identifications on finite modules.

theorem FGFilteredColimitExtension.existsUnique_iso
    {F : FGModuleCat.{v} A ⥤ FGModuleCat.{v} B}
    (E₁ E₂ : FGFilteredColimitExtension.{u, v, w} A B F) :
    ∃! e : E₁.functor ≅ E₂.functor,
      Functor.whiskerLeft (forget₂ (FGModuleCat.{v} A) (ModuleCat.{v} A)) e.hom =
        (E₁.iso.trans E₂.iso.symm).hom

ModuleCat.fgFilteredColimitExtension_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/LeftExactness.lean, line 262. The attribute's comment: “left_exactness”.

Stacks Project, Tag 0GP9. A left exact functor on finite modules over Noetherian rings has a left exact filtered-colimit-preserving extension to all modules.

theorem fgFilteredColimitExtension_preservesFiniteLimits
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (B : Type w) [CommRing B] [IsNoetherianRing B]
    (F : FGModuleCat.{v} A ⥤ FGModuleCat.{v} B)
    (E : FGFilteredColimitExtension.{u, v, w} A B F)
    [PreservesFiniteLimits F] :
    PreservesFiniteLimits E.functor

ModuleCat.FGFilteredColimitExtension.preservesFiniteColimits, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/ExtendingFunctorsCategories/RightExactness.lean, line 56. The attribute's comment: “right_exactness”.

Stacks Project, Tag 0GP9. A filtered-colimit extension of a right exact functor on finite modules is right exact. The Noetherian hypothesis on A is what supplies the extension in the first place; the proof below only uses the extension.

lemma FGFilteredColimitExtension.preservesFiniteColimits
    (A : Type u) [CommRing A] [IsNoetherianRing A] (B : Type w) [CommRing B]
    {F : FGModuleCat.{v} A ⥤ FGModuleCat.{v} B}
    (E : FGFilteredColimitExtension.{u, v, w} A B F)
    [PreservesFiniteColimits F] :
    PreservesFiniteColimits E.functor
Sources
LeanModuleCat.filteredColimitExtension · ModuleCat.FilteredColimitExtension.existsUnique_iso · ModuleCat.finitelyPresentedModule_isMonoidal · ModuleCat.filteredColimitExtension_monoidal · ModuleCat.filteredColimitExtension_additive · ModuleCat.filteredColimitExtension_preservesCoproducts · ModuleCat.filteredColimitExtension_preservesFiniteColimits · ModuleCat.filteredColimitExtension_preservesFiniteLimits_moduleValued

Section56.5 Functors between categories of quasi-coherent modules#

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

Tag 0FZB, an example

Tag 0FZB in the Stacks Project.

AlgebraicGeometry.quasicoherentIntegralTransformData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Basic.lean, line 153. The attribute's comment: “the functor”.

Stacks Project, Tag 0FZB (the functor). A quasi-coherent kernel on X ×_R Y defines the pullback--tensor--pushforward functor from quasi-coherent modules on X to quasi-coherent modules on Y.

noncomputable def quasicoherentIntegralTransformData
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R)))
    [CompactSpace X.left] [QuasiSeparatedSpace X.left]
    (K : (SheafOfModules.isQuasicoherent
      (pullback X.hom Y.hom).ringCatSheaf).FullSubcategory) :
    IntegralTransformData R X Y K

AlgebraicGeometry.quasicoherentIntegralTransform_additive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Basic.lean, line 425. The attribute's comment: “additivity”.

The integral transform is additive on morphisms.

theorem quasicoherentIntegralTransform_additive
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R)))
    [CompactSpace X.left] [QuasiSeparatedSpace X.left]
    (K : (SheafOfModules.isQuasicoherent
      (pullback X.hom Y.hom).ringCatSheaf).FullSubcategory) :
    (quasicoherentIntegralTransform R X Y K).Additive

AlgebraicGeometry.quasicoherentIntegralTransform_isLinearOverBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Basic.lean, line 480. The attribute's comment: “R-linearity”.

Stacks Project, Tag 0FZB (linearity). The integral transform associated to a quasi-coherent kernel is linear over the base ring.

theorem quasicoherentIntegralTransform_isLinearOverBase
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R)))
    [CompactSpace X.left] [QuasiSeparatedSpace X.left]
    (K : (SheafOfModules.isQuasicoherent
      (pullback X.hom Y.hom).ringCatSheaf).FullSubcategory) :
    letI : Linear R (SheafOfModules.{u} X.left.ringCatSheaf) := modulesLinear R X
    letI : Linear R (SheafOfModules.{u} Y.left.ringCatSheaf) := modulesLinear R Y
    (quasicoherentIntegralTransform R X Y K).Linear R

AlgebraicGeometry.quasicoherentIntegralTransform_preservesDirectSums, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Basic.lean, line 598. The attribute's comment: “arbitrary direct sums”.

Stacks Project, Tag 0FZB (direct sums). The integral transform associated to a quasi-coherent kernel commutes with arbitrary direct sums.

theorem quasicoherentIntegralTransform_preservesDirectSums
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R)))
    [CompactSpace X.left] [QuasiSeparatedSpace X.left]
    (K : (SheafOfModules.isQuasicoherent
      (pullback X.hom Y.hom).ringCatSheaf).FullSubcategory) (I : Type u) :
    PreservesColimitsOfShape (Discrete I)
      (quasicoherentIntegralTransform R X Y K)

Declarations registered for the tag:

Tag 0FZD, a lemma

Tag 0FZD in the Stacks Project.

AlgebraicGeometry.integralTransformQcohFunctorLift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Equivalence.lean, line 1967. The attribute's comment: “the functor from quasi-coherent kernels to right exact linear functors”.

Stacks Project, Tag 0FZD. For X affine, the integral transform of a quasi-coherent kernel on X ×_R Y, as a functor of the kernel, with codomain the R-linear right exact functors from quasi-coherent modules on X to quasi-coherent modules on Y which commute with arbitrary direct sums.

noncomputable def integralTransformQcohFunctorLift
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R))) [IsAffine X.left] :
    (SheafOfModules.isQuasicoherent
      (pullback X.hom Y.hom).ringCatSheaf).FullSubcategory ⥤
      (rightExactLinearCoproductFunctor R X Y).FullSubcategory

AlgebraicGeometry.integralTransformQcohFunctorLift_obj_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Equivalence.lean, line 1979. The attribute's comment: “the functor sends a kernel to its integral transform”.

Stacks Project, Tag 0FZD. For X affine, the integral transform of a quasi-coherent kernel on X ×_R Y is, on objects, the functor F ↦ pr_{2,*}(pr_1^* F ⊗ K) of Tag 0FZB.

theorem integralTransformQcohFunctorLift_obj_obj
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R))) [IsAffine X.left]
    (K : (SheafOfModules.isQuasicoherent
      (pullback X.hom Y.hom).ringCatSheaf).FullSubcategory) :
    ((integralTransformQcohFunctorLift R X Y).obj K).obj =
      quasicoherentIntegralTransform R X Y K

AlgebraicGeometry.faithful_integralTransformQcohFunctorLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Equivalence.lean, line 1989. The attribute's comment: “the functor is faithful”.

Stacks Project, Tag 0FZD. For X affine, the functor sending a quasi-coherent kernel on X ×_R Y to its integral transform is faithful.

theorem faithful_integralTransformQcohFunctorLift
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R))) [IsAffine X.left] :
    (integralTransformQcohFunctorLift R X Y).Faithful

AlgebraicGeometry.full_integralTransformQcohFunctorLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Equivalence.lean, line 2010. The attribute's comment: “the functor is full”.

Stacks Project, Tag 0FZD. For X affine, the functor sending a quasi-coherent kernel on X ×_R Y to its integral transform is full.

theorem full_integralTransformQcohFunctorLift
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R))) [IsAffine X.left] :
    (integralTransformQcohFunctorLift R X Y).Full

AlgebraicGeometry.essSurj_integralTransformQcohFunctorLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Equivalence.lean, line 2032. The attribute's comment: “the functor is essentially surjective”.

Stacks Project, Tag 0FZD. For X affine, every R-linear right exact functor from quasi-coherent modules on X to quasi-coherent modules on Y which commutes with arbitrary direct sums is the integral transform of a quasi-coherent kernel on X ×_R Y.

theorem essSurj_integralTransformQcohFunctorLift
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R))) [IsAffine X.left] :
    (integralTransformQcohFunctorLift R X Y).EssSurj

AlgebraicGeometry.integralTransformQcohEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Equivalence.lean, line 2044. The attribute's comment: “the equivalence of categories”.

Stacks Project, Tag 0FZD. For X affine, the integral transform of a quasi-coherent kernel is an equivalence from the quasi-coherent modules on X ×_R Y to the R-linear right exact functors from quasi-coherent modules on X to quasi-coherent modules on Y which commute with arbitrary direct sums.

noncomputable def integralTransformQcohEquivalence
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R))) [IsAffine X.left] :
    (SheafOfModules.isQuasicoherent (pullback X.hom Y.hom).ringCatSheaf).FullSubcategory ≌
      (rightExactLinearCoproductFunctor R X Y).FullSubcategory

AlgebraicGeometry.integralTransformQcohEquivalence_functor_obj_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Equivalence.lean, line 2057. The attribute's comment: “the equivalence sends a kernel to its integral transform”.

Stacks Project, Tag 0FZD. The equivalence sends a quasi-coherent kernel on X ×_R Y to its integral transform F ↦ pr_{2,*}(pr_1^* F ⊗ K).

theorem integralTransformQcohEquivalence_functor_obj_obj
    (R : Type u) [CommRing R] (X Y : Over (Spec (.of R))) [IsAffine X.left]
    (K : (SheafOfModules.isQuasicoherent
      (pullback X.hom Y.hom).ringCatSheaf).FullSubcategory) :
    ((integralTransformQcohEquivalence R X Y).functor.obj K).obj =
      quasicoherentIntegralTransform R X Y K
Tag 0FZE, a remark

Tag 0FZE in the Stacks Project.

Stacks.AlgebraicGeometry.ProjectionFormula.isIso_projectionFormulaMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/ProjectionFormulaLocal.lean, line 469.

Let h : T ⟶ S be an affine morphism of schemes, G a quasi-coherent 𝒪_T-module and H a quasi-coherent 𝒪_S-module. Then the canonical projection-formula morphism

h_*G ⊗_{𝒪_S} H ⟶ h_*(G ⊗_{𝒪_T} h^*H)

is invertible.

theorem isIso_projectionFormulaMap [IsAffineHom h] (hG : G.IsQuasicoherent)
    (hH : H.IsQuasicoherent) : IsIso (projectionFormulaMap h G H)
Tag 0FZF, a lemma

Tag 0FZF in the Stacks Project.

AlgebraicGeometry.quasicoherentIntegralTransformSourceChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/ChangeOfSpaces.lean, line 321. The attribute's comment: “affine source change”.

Let X be an affine scheme over R, let f : X' ⟶ X be an affine morphism of schemes over R and let K be a quasi-coherent module on X ×_R Y. Then the integral transform of K precomposed with the direct image along f is the integral transform of (f × id_Y)^*K.

def quasicoherentIntegralTransformSourceChangeIso (R : Type u) [CommRing R]
    (X X' Y : Over (Spec (.of R))) [IsAffine X.left] (f : X' ⟶ X) [IsAffineHom f.left]
    (K : Scheme.QuasicoherentModules (pullback X.hom Y.hom)) :
    letI : IsAffine X'.left := isAffine_of_isAffineHom f.left
    quasicoherentPushforward f.left ⋙ quasicoherentIntegralTransform R X Y K ≅
      quasicoherentIntegralTransform R X' Y (sourceChangeKernel R X X' Y f K)

AlgebraicGeometry.quasicoherentIntegralTransformTargetChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/ChangeOfSpaces.lean, line 420. The attribute's comment: “flat target change”.

Let X be an affine scheme over R, let g : Y' ⟶ Y be a flat morphism of schemes over R and let K be a quasi-coherent module on X ×_R Y. Then the integral transform of K followed by the inverse image along g is the integral transform of (id_X × g)^*K.

def quasicoherentIntegralTransformTargetChangeIso (R : Type u) [CommRing R]
    (X Y Y' : Over (Spec (.of R))) [IsAffine X.left] (g : Y' ⟶ Y) [Flat g.left]
    (K : Scheme.QuasicoherentModules (pullback X.hom Y.hom)) :
    quasicoherentIntegralTransform R X Y K ⋙ quasicoherentPullback g.left ≅
      quasicoherentIntegralTransform R X Y' (targetChangeKernel R X Y Y' g K)

AlgebraicGeometry.quasicoherentIntegralTransformOpenTargetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/ChangeOfSpaces.lean, line 472. The attribute's comment: “open target restriction”.

Let X be an affine scheme over R, let j : V ⟶ Y be an open immersion of schemes and let K be a quasi-coherent module on X ×_R Y. Then the integral transform of K followed by restriction to V is the integral transform of the restriction of K to X ×_R V.

def quasicoherentIntegralTransformOpenTargetIso (R : Type u) [CommRing R]
    (X Y : Over (Spec (.of R))) [IsAffine X.left] {V : Scheme.{u}} (j : V ⟶ Y.left)
    [IsOpenImmersion j] (K : Scheme.QuasicoherentModules (pullback X.hom Y.hom)) :
    quasicoherentIntegralTransform R X Y K ⋙ quasicoherentRestriction j ≅
      quasicoherentIntegralTransform R X (Over.mk (j ≫ Y.hom))
        (openTargetKernel R X Y j K)
Tag 0GPA, a lemma

Tag 0GPA in the Stacks Project.

AlgebraicGeometry.exists_kernel_natTrans_isIso_whiskerLeft_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/KernelOfFunctor.lean, line 957.

Tag 0GPA. Let R be a ring, let X and Y be schemes over R with X quasi-compact with affine diagonal, and let F : QCoh(𝒪_X) ⥤ QCoh(𝒪_Y) be R-linear, right exact and commute with arbitrary direct sums. Then there are a quasi-coherent module K on X ×_R Y and a natural transformation t : F ⟶ F_K such that t ∘ f_* : F ∘ f_* ⟶ F_K ∘ f_* is an isomorphism for every morphism f : X' ⟶ X whose source is an affine scheme.

The kernel is AlgebraicGeometry.AffineChartKernels.glued of AlgebraicGeometry.openKernelSystem, glued from the kernels of F ∘ j_{U,*} over the affine opens U of X, and t is AlgebraicGeometry.kernelTransform.

theorem exists_kernel_natTrans_isIso_whiskerLeft_pushforward [CompactSpace X.left]
    [IsAffineHom (pullback.diagonal (terminal.from X.left))]
    (hF : rightExactLinearCoproductFunctor R X Y F) :
    ∃ (K : Scheme.QuasicoherentModules (pullback X.hom Y.hom))
      (t : F ⟶ quasicoherentIntegralTransform R X Y K),
      ∀ (X' : Scheme.{u}) [IsAffine X'] (f : X' ⟶ X.left),
        letI : IsAffineHom f :=
          Stacks.AlgebraicGeometry.RelativeCechComplex.isAffineHom_of_isAffine_source f
        IsIso (Functor.whiskerLeft (quasicoherentPushforward f) t)
Tag 0FZG, a lemma

Tag 0FZG in the Stacks Project.

AlgebraicGeometry.isFlatOver_kernel_of_exactFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/KernelFlatnessGlued.lean, line 160. The attribute's comment: “the kernel corresponding to an exact functor is flat over X, both for X affine and for X quasi-compact with affine diagonal”.

The kernel of an exact functor is flat. In the situation of Tag 0FZD or of Tag 0GPA, if F is an exact functor, then the corresponding object K of QCoh(𝒪_{X ×_R Y}) is flat over X.

The four conjuncts are: 1. the situation of Tag 0FZD (X affine, Y arbitrary), for every kernel K whose integral transform is isomorphic to F; 2. the same, for the kernel attached to F by the inverse of the equivalence of Tag 0FZD; 3. the situation of Tag 0GPA (X quasi-compact with affine diagonal), for every kernel K with a natural transformation t : F ⟶ F_K such that t ∘ f_* is an isomorphism for every morphism f : X' ⟶ X with X' affine; 4. the same, for the glued kernel constructed in Tag 0GPA from an R-linear right exact functor commuting with arbitrary direct sums.

theorem isFlatOver_kernel_of_exactFunctor (R : Type u) [CommRing R] :
    (∀ (X Y : Over (Spec (.of R))) [IsAffine X.left]
      (K : Scheme.QuasicoherentModules (pullback X.hom Y.hom))
      (F : Scheme.QuasicoherentModules X.left ⥤ Scheme.QuasicoherentModules Y.left),
      (F ≅ quasicoherentIntegralTransform R X Y K) → exactFunctor _ _ F →
        IsFlatOver (pullback.fst X.hom Y.hom).toLRSHom.toShHom K.obj) ∧
    (∀ (X Y : Over (Spec (.of R))) [IsAffine X.left]
      (F : (rightExactLinearCoproductFunctor R X Y).FullSubcategory),
      exactFunctor _ _ F.obj →
        IsFlatOver (pullback.fst X.hom Y.hom).toLRSHom.toShHom
          ((integralTransformQcohEquivalence R X Y).inverse.obj F).obj) ∧
    (∀ (X Y : Over (Spec (.of R))) [CompactSpace X.left]
      [IsAffineHom (pullback.diagonal (terminal.from X.left))]
      (F : Scheme.QuasicoherentModules X.left ⥤ Scheme.QuasicoherentModules Y.left)
      (K : Scheme.QuasicoherentModules (pullback X.hom Y.hom))
      (t : F ⟶ quasicoherentIntegralTransform R X Y K),
      (∀ (X' : Scheme.{u}) [IsAffine X'] (f : X' ⟶ X.left),
        letI : IsAffineHom f :=
          Stacks.AlgebraicGeometry.RelativeCechComplex.isAffineHom_of_isAffine_source f
        IsIso (Functor.whiskerLeft (quasicoherentPushforward f) t)) →
      exactFunctor _ _ F →
        IsFlatOver (pullback.fst X.hom Y.hom).toLRSHom.toShHom K.obj) ∧
    (∀ (X Y : Over (Spec (.of R))) [CompactSpace X.left]
      [IsAffineHom (pullback.diagonal (terminal.from X.left))]
      (F : Scheme.QuasicoherentModules X.left ⥤ Scheme.QuasicoherentModules Y.left)
      (hF : rightExactLinearCoproductFunctor R X Y F),
      exactFunctor _ _ F →
        IsFlatOver (pullback.fst X.hom Y.hom).toLRSHom.toShHom
          (openKernelSystem R X Y F
            (affineOpenRightExactLinearCoproductFunctor_of_rightExact R X Y F hF)).glued.obj)
Tag 0FZH, a lemma

Tag 0FZH in the Stacks Project.

AlgebraicGeometry.isEquivalence_integralTransformExactKernelFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/ExactKernelEquivalence.lean, line 74. The attribute's comment: “the functor sending a kernel K on X ×_R Y to its integral transform is an equivalence from the kernels flat over X with vanishing higher direct images of pr_1^*F ⊗ K onto the R-linear exact functors QCoh(X) ⥤ QCoh(Y) commuting with arbitrary direct sums”.

Let R be a ring and let X and Y be schemes over R with X quasi-compact and with affine diagonal. The functor sending a quasi-coherent kernel K on X ×_R Y to its integral transform F ↦ pr_{2,*}(pr_1^*F ⊗ K) is an equivalence of categories between

  1. the full subcategory of QCoh(𝒪_{X ×_R Y}) of the kernels K which are flat over X and satisfy R^q pr_{2,*}(pr_1^*F ⊗ K) = 0 for all quasi-coherent F on X and all q > 0 (AlgebraicGeometry.integralTransformExactKernel), and
  2. the category of R-linear exact functors QCoh(𝒪_X) ⥤ QCoh(𝒪_Y) which commute with arbitrary direct sums (AlgebraicGeometry.exactLinearCoproductFunctor).
theorem isEquivalence_integralTransformExactKernelFunctor :
    (integralTransformExactKernelFunctor R X Y).IsEquivalence
Tag 0GPB, a remark

Tag 0GPB in the Stacks Project.

AlgebraicGeometry.nonempty_iso_quasicoherentIntegralTransform_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Characterization.lean, line 851.

Stacks Project, Tag 0GPB. Let R be a ring and let X and Y be schemes over R, with X quasi-compact with affine diagonal. A functor F : QCoh(𝒪_X) ⥤ QCoh(𝒪_Y) is isomorphic to the integral transform F_K = pr_{2,*}(pr_1^*(−) ⊗ K) of a quasi-coherent module K on X ×_R Y if and only if

  1. F is R-linear (in particular additive) and commutes with arbitrary direct sums,
  2. F ∘ j_* is right exact for the inclusion j : U ⟶ X of every affine open U (AlgebraicGeometry.PreservesFiniteColimitsAfterAffineOpens), and
  3. 0 ⟶ F(F) ⟶ F(G) ⟶ F(H) is exact for every short exact sequence 0 ⟶ F ⟶ G ⟶ H ⟶ 0 of quasi-coherent modules whose sequences of stalks are split short exact sequences of 𝒪_{X,x}-modules (AlgebraicGeometry.IsStalkwiseSplitLeftExact).
theorem nonempty_iso_quasicoherentIntegralTransform_iff
    (F : Scheme.QuasicoherentModules X.left ⥤ Scheme.QuasicoherentModules Y.left) :
    letI : Linear R (SheafOfModules.{u} X.left.ringCatSheaf) := modulesLinear R X
    letI : Linear R (SheafOfModules.{u} Y.left.ringCatSheaf) := modulesLinear R Y
    (∃ K : Scheme.QuasicoherentModules (pullback X.hom Y.hom),
        Nonempty (F ≅ quasicoherentIntegralTransform R X Y K)) ↔
      ∃ _ : F.Additive, F.Linear R ∧ (∀ I : Type u, PreservesColimitsOfShape (Discrete I) F) ∧
        PreservesFiniteColimitsAfterAffineOpens R X F ∧ IsStalkwiseSplitLeftExact F
Tag 0GPC, a lemma

Tag 0GPC in the Stacks Project.

AlgebraicGeometry.quasicoherentIntegralTransformConvolutionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/Convolution.lean, line 567. The attribute's comment: “the composition formula F_L ∘ F_K ≅ F_{pr13,(pr12^K ⊗ pr23^*L)} as a natural isomorphism of functors QCoh(O_X) to QCoh(O_Z), for L a kernel of category (2) of 0FZH (so F_L is R-linear, exact and commutes with direct sums), K arbitrary, X quasi-compact with affine diagonal and Y quasi-compact and quasi-separated”.

Stacks Project, Tag 0GPC. Let R be a ring and let X, Y, Z be schemes over R, with X quasi-compact with affine diagonal and Y quasi-compact and quasi-separated. Let K be a quasi-coherent kernel on X ×_R Y and L a quasi-coherent kernel on Y ×_R Z in category (2) of Tag 0FZH, that is, flat over Y with vanishing higher direct images, so that its integral transform F_L : QCoh(𝒪_Y) ⥤ QCoh(𝒪_Z) is R-linear, exact and commutes with direct sums. Then

F_L ∘ F_K ≅ F_{pr_{13,*}(pr_{12}^*K ⊗ pr_{23}^*L)}

as functors QCoh(𝒪_X) ⥤ QCoh(𝒪_Z).

This is the source's statement for exact functors F and G with kernels K and L (G ∘ F ≅ F_L ∘ F_K), in greater generality: nothing is assumed of K, and of Y only quasi-compactness and quasi-separatedness. That, when K is of category (2) as well, the convolution is up to isomorphism the kernel of category (2) which Tag 0FZH attaches to G ∘ F is AlgebraicGeometry.exists_integralTransformExactKernel_iso_convolutionKernel.

Exactness of F_L cannot be dropped. Let E be an elliptic curve over a field k with origin o, let C = E ∖ {e} for a point e ≠ o, R = Γ(C, 𝒪_C), X = E ×_k C over R, Y = Spec R, Z = Spec k the point o of C, L = 𝒪_Z on Y ×_R Z = Z, and K = 𝒪(Δ - {o} × C) on X ×_R Y = X, with Δ the graph of C ⊆ E. The fibre of K over c ∈ C is 𝒪_E(c - o), nontrivial of degree zero for c ≠ o, so Γ(X, K), a torsion-free R-module with zero generic fibre, vanishes and F_L(F_K(𝒪_X)) = 0. But X ×_R Y ×_R Z = E, the convolution kernel is K|_{E × {o}} ≅ 𝒪_E, and F_{K * L}(𝒪_X) = Γ(E, 𝒪_E) = k. Here F_L = - ⊗_R k is not left exact.

def quasicoherentIntegralTransformConvolutionIso (hL : integralTransformExactKernel R Y Z L) :
    quasicoherentIntegralTransform R X Y K ⋙ quasicoherentIntegralTransform R Y Z L ≅
      quasicoherentIntegralTransform R X Z (convolutionKernel R X Y Z K L)
Tag 0FZI, a lemma

Tag 0FZI in the Stacks Project.

AlgebraicGeometry.isZero_rightDerived_pushforward_baseChangeKernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/BaseChangeAcyclicity.lean, line 536. The attribute's comment: “the positive higher direct images of pr_12^F ⊗ pr_23^K along pr_13 vanish”.

Higher direct images of an integral-transform kernel after base change. Let R be a ring, let X and Y be schemes over R with the structure morphism of X quasi-compact and quasi-separated, and let K be a quasi-coherent kernel on X ×_R Y satisfying the two conditions of Tag 0FZH part (2). Then for every scheme T over R, R ^q pr_{13,*}(pr_{12}^*F ⊗ pr_{23}^*K) = 0 for every quasi-coherent F on T ×_R X and every q > 0.

theorem isZero_rightDerived_pushforward_baseChangeKernel (T X Y : Over (Spec (.of R)))
    [QuasiCompact X.hom] [QuasiSeparated X.hom]
    (K : Scheme.QuasicoherentModules (pullback X.hom Y.hom))
    (hK : integralTransformExactKernel R X Y K)
    (F : Scheme.QuasicoherentModules (baseChangeSourceOver R T X).left) (q : ℕ) (hq : 0 < q) :
    IsZero (((Scheme.Modules.pushforward (baseChangeTargetMap R T X Y)).rightDerived q).obj
      ((integralTransformIntegrand R (baseChangeSourceOver R T X) Y
        (baseChangeKernel R T X Y K)).obj F))
Tag 0FZJ, a lemma

Tag 0FZJ in the Stacks Project.

AlgebraicGeometry.exists_epi_externalTensorProduct_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/IntegralTransformQcoh/DiagonalSurjection.lean, line 485. The attribute's comment: “the surjection O_X ⊠ F(O_X) ⟶ K”.

Stacks Project, Tag 0FZJ. Let R be a ring, let X and Y be schemes over R with X quasi-compact, separated and flat over R, and let K be a quasi-coherent kernel on X ×_R Y satisfying the two conditions of [Stacks, Tag 0FZH] part (2). Then there is a surjection 𝒪_X ⊠ F_K(𝒪_X) ⟶ K, where F_K is the integral transform of K.

The diagonal short exact sequence 0 → I → 𝒪_{X ×_R X} → 𝒪_Δ → 0 is sent by the exact integrand pr_{12}^*(-) ⊗ pr_{23}^*K to a short exact sequence on X ×_R X ×_R Y, and [Stacks, Tag 0FZI] makes its direct image along pr_{13} short exact again; the surjection it exhibits is the one asserted, once flat base change identifies its source with pr_2^*pr_{2,*}K = 𝒪_X ⊠ F_K(𝒪_X) and the projection formula identifies its target with K.

theorem exists_epi_externalTensorProduct_unit (X Y : Over (Spec (.of R)))
    [CompactSpace X.left] [IsSeparated X.hom] [Flat X.hom]
    (K : Scheme.QuasicoherentModules (pullback X.hom Y.hom))
    (hK : integralTransformExactKernel R X Y K) :
    ∃ e : externalTensorProduct X.hom Y.hom (SheafOfModules.unit X.left.ringCatSheaf)
        ((quasicoherentIntegralTransform R X Y K).obj
          ⟨SheafOfModules.unit X.left.ringCatSheaf,
            Stacks.AlgebraicGeometry.AffineQcohPushforward.isQuasicoherent_unit
              X.left⟩).obj ⟶ K.obj, Epi e
Sources
LeanAlgebraicGeometry.quasicoherentIntegralTransformData · AlgebraicGeometry.quasicoherentIntegralTransform_additive · AlgebraicGeometry.quasicoherentIntegralTransform_isLinearOverBase · AlgebraicGeometry.quasicoherentIntegralTransform_preservesDirectSums · AlgebraicGeometry.quasiCompact_of_compactSpace · AlgebraicGeometry.quasiCompact_isStableUnderBaseChange · AlgebraicGeometry.QuasiSeparated.of_quasiSeparatedSpace · AlgebraicGeometry.quasiSeparated_isStableUnderBaseChange

Section56.6 Gabriel-Rosenberg reconstruction#

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

Tag 0GPE, a lemma

Tag 0GPE in the Stacks Project.

AlgebraicGeometry.isFinitelyPresentable_iff_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/CompactObjects.lean, line 152.

Stacks Project, Tag 0GPE. A quasi-coherent module on a quasi-compact and quasi-separated scheme is a categorically compact object of the category of quasi-coherent modules if and only if it is of finite presentation.

theorem isFinitelyPresentable_iff_isFinitePresentation
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (F : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) :
    IsFinitelyPresentable.{u} F ↔ F.obj.IsFinitePresentation
Tag 0GPF, a lemma

Tag 0GPF in the Stacks Project.

AlgebraicGeometry.exists_nonzero_hom_of_supp_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/SupportedNonzeroHom.lean, line 358. References: SGA 2 VII (1.3), “affine case”.

Stacks Project, Tag 0GPF. If the support of a nonzero quasi-coherent module on an affine scheme is contained in that of a finitely presented module, then there is a nonzero morphism from the latter to the former.

theorem exists_nonzero_hom_of_supp_subset
    (X : Scheme.{u}) [IsAffine X]
    (F E : X.Modules) [F.IsFinitePresentation] [E.IsQuasicoherent]
    (hE : ¬ IsZero E)
    (hsupp : SheafOfModules.supp E ⊆ SheafOfModules.supp F) :
    ∃ f : F ⟶ E, f ≠ 0
Tag 0GPG, a lemma

Tag 0GPG in the Stacks Project.

AlgebraicGeometry.supportContained_eq_serreCoproductClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/SupportedSerreSubcategory.lean, line 780.

Stacks Project, Tag 0GPG. On a quasi-compact and quasi-separated scheme, the quasi-coherent modules supported on the support of a finitely presented module are exactly the smallest Serre subcategory containing it and closed under arbitrary direct sums.

theorem supportContained_eq_serreCoproductClosure (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (F : X.Modules)
    [SheafOfModules.IsFinitePresentation (R := X.ringCatSheaf) F] :
    (fun E : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ↦
        IsSupportedOn E.obj F) =
      serreCoproductClosure
          (C := (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory)
        ⟨F, by
        constructor
        exact ⟨(SheafOfModules.IsFinitePresentation.exists_quasicoherentData F).choose⟩⟩
Tag 0GPH, a lemma

Tag 0GPH in the Stacks Project.

AlgebraicGeometry.quasicoherentSupportedOn_isSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/SupportedSerreQuotient.lean, line 229. The attribute's comment: “the full subcategory of modules supported on Z is a Serre subcategory”.

Quasi-coherent modules supported on a fixed subset of a scheme form a Serre subcategory of the category of all quasi-coherent modules.

public instance quasicoherentSupportedOn_isSerreClass (X : Scheme.{u}) (Z : Set X) :
    (quasicoherentSupportedOn X Z).IsSerreClass

AlgebraicGeometry.quasicoherentRestriction_isLocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/SupportedSerreQuotient.lean, line 307. The attribute's comment: “restriction is the localization at the supported Serre subcategory”.

[Stacks, Tag 0GPH]. Let X be a quasi-compact and quasi-separated scheme and let U be a quasi-compact open whose complement is the closed subset Z. Restriction along U ↪ X exhibits QCoh(𝒪_U) as the localization of QCoh(𝒪_X) at the morphisms whose kernel and cokernel are supported on Z, that is, as the Serre quotient of QCoh(𝒪_X) by the full subcategory of quasi-coherent modules supported on Z.

public theorem quasicoherentRestriction_isLocalization (X : Scheme.{u}) [CompactSpace X]
    [QuasiSeparatedSpace X] (Z : Set X) (U : X.Opens) (hUZ : (U : Set X) = Zᶜ)
    (hU : IsCompact (U : Set X)) :
    (quasicoherentRestriction U.ι).IsLocalization
      (quasicoherentSupportedOn X Z).isoModSerre

AlgebraicGeometry.quasicoherentSupportedQuotientEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/SupportedSerreQuotient.lean, line 378. The attribute's comment: “the induced equivalence from the quotient category”.

[Stacks, Tag 0GPH]. The equivalence QCoh(𝒪_X)/𝒜 ≌ QCoh(𝒪_U) induced by restriction, where 𝒜 is the Serre subcategory of quasi-coherent modules supported on the closed complement Z of the quasi-compact open U, and QCoh(𝒪_X)/𝒜 is the Serre quotient, that is the localization of QCoh(𝒪_X) at the morphisms that are isomorphisms modulo 𝒜.

public noncomputable def quasicoherentSupportedQuotientEquivalence (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] (Z : Set X) (U : X.Opens)
    (hUZ : (U : Set X) = Zᶜ) (hU : IsCompact (U : Set X)) :
    (quasicoherentSupportedOn X Z).isoModSerre.Localization ≌
      (SheafOfModules.isQuasicoherent U.toScheme.ringCatSheaf).FullSubcategory

AlgebraicGeometry.quasicoherentSupportedQuotientEquivalenceFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/SupportedSerreQuotient.lean, line 390. The attribute's comment: “the equivalence is induced by the restriction functor”.

The equivalence QCoh(𝒪_X)/𝒜 ≌ QCoh(𝒪_U) of [Stacks, Tag 0GPH] is the one induced by the restriction functor: composing it with the quotient functor gives back restriction.

public noncomputable def quasicoherentSupportedQuotientEquivalenceFunctorIso (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] (Z : Set X) (U : X.Opens)
    (hUZ : (U : Set X) = Zᶜ) (hU : IsCompact (U : Set X)) :
    (quasicoherentSupportedOn X Z).isoModSerre.Q ⋙
        (quasicoherentSupportedQuotientEquivalence X Z U hUZ hU).functor ≅
      quasicoherentRestriction U.ι
Tag 0GPI, a lemma

Tag 0GPI in the Stacks Project.

AlgebraicGeometry.AffineOfModuleCategory.isAffine_of_quasicoherentModules_equivalent_moduleCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/AffineOfModuleCategory.lean, line 1141. The attribute's comment: “[CommRing R] reads the tag's a ring: the rank-one step needs End P commutative. For noncommutative R the conclusion still holds by Morita equivalence (Mod (M₂ k) ≌ Mod k), but that rank-one step fails outright.”.

Stacks Project, Tag 0GPI. A quasi-compact and quasi-separated scheme whose category of quasi-coherent modules is equivalent to the category of modules over a commutative ring is affine.

The commutativity of R is a reading of the tag's a ring. It is used through the separator P, whose endomorphism ring must be commutative for the rank of P to be forced to be 1.

public theorem isAffine_of_quasicoherentModules_equivalent_moduleCat
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (R : Type v) [CommRing R]
    (e : ModuleCat.{u} R ≌
      (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory) :
    IsAffine X

AlgebraicGeometry.AffineOfModuleCategory.isAffine_of_quasicoherentModules_equivalence_moduleCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/AffineOfModuleCategory.lean, line 1164. The attribute's comment: “the hypothesis in the orientation of the source, QCoh(𝒪_X) ≌ Mod R; [CommRing R] reads the tag's a ring, exactly as for the mirror form isAffine_of_quasicoherentModules_equivalent_moduleCat”.

Stacks Project, Tag 0GPI, with the equivalence written in the orientation of the source: a quasi-compact and quasi-separated scheme whose category of quasi-coherent modules is equivalent to the category of modules over a commutative ring is affine.

As for the mirror form, the commutativity of R is a reading of the tag's a ring.

public theorem isAffine_of_quasicoherentModules_equivalence_moduleCat
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (R : Type v) [CommRing R]
    (e : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ≌
      ModuleCat.{u} R) :
    IsAffine X
Tag 0GPJ, a proposition

Tag 0GPJ in the Stacks Project.

AlgebraicGeometry.exists_schemeIso_invertible_of_quasicoherentEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/AffineReconstruction.lean, line 185. The attribute's comment: “affine case: for X and Y affine, with the tensoring by the invertible module read on ModuleCat Γ(Y, ⊤) through the affine comparison AlgebraicGeometry.affineQuasicoherentModulesEquiv rather than as the tensor product of sheaves of 𝒪_Y-modules. This is the form in which the Tag 0GP0 argument produces the conclusion; the source's own sheaf-level form is AlgebraicGeometry.exists_schemeIso_invertibleSheaf_of_quasicoherentEquivalence, proved from this one in the same file. What is NOT proved here is the general quasi-compact quasi-separated case; its local form, steps 3 to 8 of the source's argument, is AlgebraicGeometry.exists_isAffineOpen_schemeIso_invertibleSheaf_of_isFinitePresentation, and what remains beyond that is step 2 and the gluing step 9 that the source itself omits”.

If X and Y are affine schemes and F : QCoh(𝒪_X) ⥤ QCoh(𝒪_Y) is an equivalence, then there are an isomorphism of schemes f : Y ≅ X and an invertible Γ(Y, ⊤)-module L such that F is inverse image along f followed by tensoring with L.

theorem exists_schemeIso_invertible_of_quasicoherentEquivalence
    (F : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ⥤
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf).FullSubcategory) [F.IsEquivalence] :
    ∃ (f : Y ≅ X) (L : ModuleCat.{u} Γ(Y, ⊤)), Module.Invertible Γ(Y, ⊤) L ∧
      Nonempty (F ≅ (quasicoherentModulesEquivOfSchemeIso f).symm.functor ⋙
        affineTensorFunctor Y L)

AlgebraicGeometry.exists_schemeIso_invertibleSheaf_of_quasicoherentEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/AffineReconstruction.lean, line 438. The attribute's comment: “affine case: for X and Y affine. The invertible object is a sheaf of 𝒪_Y-modules, invertible in the sense of Tag 01CS (Stacks.SheafOfModules.IsInvertible), and the tensoring is - ⊗_{𝒪_Y} L. Two deviations from the source statement. First, the general quasi-compact quasi-separated case is not proved; its local form, steps 3 to 8 of the source's argument, is AlgebraicGeometry.exists_isAffineOpen_schemeIso_invertibleSheaf_of_isFinitePresentation, which quotes this theorem for its affine input, and what remains beyond that is step 2 (the existence of a finitely presented module supported on the complement of a given affine open) and the gluing step 9 that the source itself omits. Second, the comparison of functors is stated after forgetting quasi-coherence, i.e. between functors into all 𝒪_Y-modules, so that the statement does not depend on quasi-coherence being stable under inverse image and tensor product; since the inclusion of the quasi-coherent modules is fully faithful and quasi-coherence is invariant under isomorphism, nothing of the source's content is lost”.

If X and Y are affine schemes and F : QCoh(𝒪_X) ⥤ QCoh(𝒪_Y) is an equivalence, then there are an isomorphism of schemes f : Y ≅ X and an invertible sheaf L of 𝒪_Y-modules such that F is inverse image along f followed by - ⊗_{𝒪_Y} L.

theorem exists_schemeIso_invertibleSheaf_of_quasicoherentEquivalence
    (F : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ⥤
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf).FullSubcategory) [F.IsEquivalence] :
    ∃ (f : Y ≅ X) (L : SheafOfModules.{u} Y.ringCatSheaf),
      Stacks.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.2 L ∧
        Nonempty (F ⋙ ObjectProperty.ι (SheafOfModules.isQuasicoherent Y.ringCatSheaf) ≅
          pullbackTensorFunctor f.hom L)

AlgebraicGeometry.exists_natIso_pullbackTensorFunctor_of_quasicoherentEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/ReconstructionGlobalComparison.lean, line 89. The attribute's comment: “the tag IN FULL, for X and Y quasi-compact and quasi-separated: an equivalence of the categories of quasi-coherent modules gives an isomorphism of schemes g : Y ≅ X, an invertible 𝒪_Y-module M, and a NATURAL isomorphism e(𝓕) ≅ g^*𝓕 ⊗ M. No cover, no affineness and no further hypothesis of any kind beyond qcqs. The scheme half is exists_schemeIso_of_quasicoherentEquivalence and the module half isInvertible_map_quasicoherentUnit_of_quasicoherentEquivalence, both already unconditional; what is new is the comparison of functors, which the Stacks source dismisses with "We omit the details". It is glued from the per-chart comparisons chartComparisonIso by exists_natIso_of_chartComparison, whose agreement hypothesis is discharged by the rigidity natIso_eq_of_app_unit_eq_of_iso once the comparisons are normalised at 𝒪_X; the normalisation is chartComparisonIso_hom_app_quasicoherentUnit and it is automatic, because the module is e(𝒪_X) and the identification of its restriction with the chart's L is restrictMapUnitIsoOfChartIso, built from the same α and β. As in the affine case the comparison is stated after forgetting quasi-coherence, between functors into all 𝒪_Y-modules”.

Stacks Project, Tag 0GPJ. Let X and Y be quasi-compact and quasi-separated schemes and let e : QCoh(𝒪_X) ≌ QCoh(𝒪_Y) be an equivalence of their categories of quasi-coherent modules. Then there are an isomorphism of schemes g : Y ≅ X and an invertible 𝒪_Y-module M with e(𝓕) ≅ g^*𝓕 ⊗ M, naturally in the quasi-coherent 𝒪_X-module 𝓕.

The module is e(𝒪_X); the isomorphism is the one glued from the reconstruction charts. As in the affine case the comparison of functors is stated after forgetting quasi-coherence, between functors into all 𝒪_Y-modules, which loses nothing because the inclusion of the quasi-coherent modules is fully faithful and quasi-coherence is invariant under isomorphism.

Nothing is assumed beyond the equivalence and quasi-compactness and quasi-separatedness of the two schemes.

theorem exists_natIso_pullbackTensorFunctor_of_quasicoherentEquivalence {X Y : Scheme.{u}}
    [CompactSpace X] [QuasiSeparatedSpace X] [CompactSpace Y] [QuasiSeparatedSpace Y]
    (e : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ≌
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf).FullSubcategory) :
    ∃ (g : Y ≅ X) (M : Y.Modules),
      Stacks.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.2 M ∧
        Nonempty (e.functor ⋙ ObjectProperty.ι
            (SheafOfModules.isQuasicoherent Y.ringCatSheaf) ≅
          pullbackTensorFunctor g.hom M)

AlgebraicGeometry.exists_isOpenCover_schemeIso_invertibleSheaf_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/ReconstructionGlobalForm.lean, line 169. The attribute's comment: “the GLOBAL form — X and Y quasi-compact and quasi-separated, no affineness and no restriction to a single open U. Steps 3 to 8 together with the covering assertion of step 9, which is PROVED here and no longer hypothesised: AlgebraicGeometry.isOpenCover_of_supportedCorrespondence shows the opens V_U cover Y, and AlgebraicGeometry.exists_gluedQuasicoherentFunctor_restrictIso runs the functor-level gluing with that hypothesis discharged. The module G of step 2 is a hypothesis here, one per member of the cover; it need not be, and AlgebraicGeometry.exists_isOpenCover_schemeIso_invertibleSheaf_of_isAffineOpenCover below is this statement with G and hG deleted, the module produced instead as 𝒪_X/I for the Tag 01PH ideal. The per-chart data IS glued downstream: the f_U into one isomorphism Y ≅ X by exists_schemeIso_of_quasicoherentEquivalence (ReconstructionGlobalSchemeIso.lean) and the L_U into one invertible 𝒪_Y-module by exists_isOpenCover_invertibleModule_restrictIso_of_isAffineOpenCover (ReconstructionGlobalModule.lean). The single natural isomorphism e(F) ≅ g^*F ⊗ M comparing e with that glued pair — the stated conclusion of 0GPJ, which the source dismisses with "We omit the details" — is exists_natIso_pullbackTensorFunctor_of_quasicoherentEquivalence (ReconstructionGlobalComparison.lean). As in the affine case the comparison of functors is stated after forgetting quasi-coherence, between functors into all 𝒪_V-modules”.

Stacks Project, Tag 0GPJ in its global form. Let X and Y be quasi-compact and quasi-separated schemes and let e : QCoh(𝒪_X) ≌ QCoh(𝒪_Y) be an equivalence. Let U i be an affine open cover of X and let G i be a finitely presented quasi-coherent 𝒪_X-module whose support is the complement of U i. Then there are opens V i ⊆ Y which cover Y and are each affine and quasi-compact, and for each i an equivalence F\_i : QCoh(𝒪\_\{U i}) ≌ QCoh(𝒪\_\{V i}) compatible with e and the two restrictions, an isomorphism of schemes f_i : V i ≅ U i and an invertible sheaf L_i of 𝒪_{V i}-modules such that F_i is inverse image along f_i followed by - ⊗_{𝒪_{V i}} L_i.

The chart V i is the complement of the support of e.functor.obj (G i), as in AlgebraicGeometry.exists_isAffineOpen_schemeIso_invertibleSheaf_of_isFinitePresentation; what is new here is that these opens cover Y, which is AlgebraicGeometry.isOpenCover_of_supportedCorrespondence.

theorem exists_isOpenCover_schemeIso_invertibleSheaf_of_isFinitePresentation {ι : Type u}
    (U : ι → X.Opens) (hUaff : ∀ i, IsAffineOpen (U i)) (hUcover : IsOpenCover U)
    (G : ι → (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory)
    [∀ i, SheafOfModules.IsFinitePresentation (R := X.ringCatSheaf) (G i).obj]
    (hG : ∀ i, supportSet (G i).obj = (U i : Set X)ᶜ) :
    ∃ V : ι → Y.Opens, IsOpenCover V ∧
      ∀ i, IsAffineOpen (V i) ∧ IsCompact (V i : Set Y) ∧
        ∃ (F : (SheafOfModules.isQuasicoherent (U i).toScheme.ringCatSheaf).FullSubcategory ⥤
            (SheafOfModules.isQuasicoherent (V i).toScheme.ringCatSheaf).FullSubcategory)
          (f : (V i).toScheme ≅ (U i).toScheme)
          (L : SheafOfModules.{u} (V i).toScheme.ringCatSheaf),
          F.IsEquivalence ∧
            Stacks.SheafOfModules.IsInvertible (V i).toScheme.presheaf
              (V i).toScheme.ringCatSheaf.2 L ∧
            Nonempty (e.functor ⋙ quasicoherentRestriction (V i).ι ≅
              quasicoherentRestriction (U i).ι ⋙ F) ∧
            Nonempty (F ⋙ ObjectProperty.ι
                (SheafOfModules.isQuasicoherent (V i).toScheme.ringCatSheaf) ≅
              pullbackTensorFunctor f.hom L)

AlgebraicGeometry.exists_isOpenCover_schemeIso_invertibleSheaf_of_isAffineOpenCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/ReconstructionGlobalForm.lean, line 265. The attribute's comment: “the GLOBAL form with step 2 DISCHARGED — X and Y quasi-compact and quasi-separated, an affine open cover U i of X, and no module hypothesised. The G i is 𝒪_X/I i for the finite type ideal sheaf I i of Tag 01PH, finitely presented by Stacks.AlgebraicGeometry.IdealSheafQuotient.isFinitePresentation_structureQuotient and with support V(I i) by Stacks.AlgebraicGeometry.IdealSheafQuotient.supp_structureQuotient. Steps 2 to 8 and the covering assertion of step 9 are therefore all proved. The per-chart data IS glued downstream: the f_i into one isomorphism Y ≅ X by exists_schemeIso_of_quasicoherentEquivalence (ReconstructionGlobalSchemeIso.lean) and the L_i into one invertible 𝒪_Y-module by exists_isOpenCover_invertibleModule_restrictIso_of_isAffineOpenCover (ReconstructionGlobalModule.lean). The single natural isomorphism e(F) ≅ g^*F ⊗ M comparing e with that glued pair — the stated conclusion of 0GPJ, which the Stacks source dismisses with "We omit the details" — is exists_natIso_pullbackTensorFunctor_of_quasicoherentEquivalence (ReconstructionGlobalComparison.lean). As in the affine case the comparison of functors is stated after forgetting quasi-coherence, between functors into all 𝒪_V-modules”.

Stacks Project, Tag 0GPJ in its global form, with step 2 discharged. Let X and Y be quasi-compact and quasi-separated schemes, let e : QCoh(𝒪_X) ≌ QCoh(𝒪_Y) be an equivalence and let U i be an affine open cover of X. Then there are opens V i ⊆ Y which cover Y and are each affine and quasi-compact, and for each i an equivalence F_i : QCoh(𝒪_{U i}) ≌ QCoh(𝒪_{V i}) compatible with e and the two restrictions, an isomorphism of schemes f_i : V i ≅ U i and an invertible sheaf L_i of 𝒪_{V i}-modules such that F_i is inverse image along f_i followed by - ⊗_{𝒪_{V i}} L_i.

This is AlgebraicGeometry.exists_isOpenCover_schemeIso_invertibleSheaf_of_isFinitePresentation with its hypotheses G and hG deleted: the modules are produced by AlgebraicGeometry.exists_isFinitePresentation_supportSet_eq_compl. Only the affine open cover of X is given.

The module family is kept opaque, by choose against the single-index statement above, for the reason recorded in the implementation notes: handing over an explicit composite instead makes the conclusion unfold definitionally once per index and per conjunct.

theorem exists_isOpenCover_schemeIso_invertibleSheaf_of_isAffineOpenCover {ι : Type u}
    (U : ι → X.Opens) (hUaff : ∀ i, IsAffineOpen (U i)) (hUcover : IsOpenCover U) :
    ∃ V : ι → Y.Opens, IsOpenCover V ∧
      ∀ i, IsAffineOpen (V i) ∧ IsCompact (V i : Set Y) ∧
        ∃ (F : (SheafOfModules.isQuasicoherent (U i).toScheme.ringCatSheaf).FullSubcategory ⥤
            (SheafOfModules.isQuasicoherent (V i).toScheme.ringCatSheaf).FullSubcategory)
          (f : (V i).toScheme ≅ (U i).toScheme)
          (L : SheafOfModules.{u} (V i).toScheme.ringCatSheaf),
          F.IsEquivalence ∧
            Stacks.SheafOfModules.IsInvertible (V i).toScheme.presheaf
              (V i).toScheme.ringCatSheaf.2 L ∧
            Nonempty (e.functor ⋙ quasicoherentRestriction (V i).ι ≅
              quasicoherentRestriction (U i).ι ⋙ F) ∧
            Nonempty (F ⋙ ObjectProperty.ι
                (SheafOfModules.isQuasicoherent (V i).toScheme.ringCatSheaf) ≅
              pullbackTensorFunctor f.hom L)

AlgebraicGeometry.isInvertible_map_quasicoherentUnit_of_quasicoherentEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/ReconstructionGlobalModule.lean, line 240. The attribute's comment: “the MODULE half of the tag's conclusion, unconditionally: X and Y quasi-compact and quasi-separated and an equivalence e of their categories of quasi-coherent modules make e(𝒪_X) an invertible 𝒪_Y-module. No cover, no affineness and no further hypothesis of any kind beyond qcqs. This identifies WHICH module the tag's L is and proves it invertible: were the tag's comparison e(F) ≅ f^*F ⊗ L available, F = 𝒪_X would give L ≅ f^*𝒪_X ⊗ L ≅ e(𝒪_X), so no other module can serve. The statement is not an existential — ∃ L, IsInvertible L is satisfied by 𝒪_Y and would say nothing — it names the module. The per-chart invertible sheaves L i of the reconstruction are its restrictions (restrictMapUnitIsoOfChartIso), which is also what supplies the transition data the gluing of ReconstructionGluedModule.lean:197 asks for; that gluing run on the reconstruction's own charts is exists_isOpenCover_invertibleModule_restrictIso_of_isAffineOpenCover below. The SCHEME half is exists_schemeIso_of_quasicoherentEquivalence (ReconstructionGlobalSchemeIso.lean:324). The comparison of functors — 0GPJ also asserts e(F) ≅ f^*F ⊗ L naturally in F — is NOT produced here: it is exists_natIso_pullbackTensorFunctor_of_quasicoherentEquivalence (ReconstructionGlobalComparison.lean), glued from the per-chart chartComparisonIso (ReconstructionGlobalNatIso.lean) by exists_natIso_of_chartComparison (ReconstructionChartGlue.lean), the two comparisons over a common affine open being made equal by the rigidity natIso_eq_of_app_unit_eq_of_iso (ReconstructionChartRigidity.lean) once they are normalised at 𝒪_X (chartComparisonIso_hom_app_quasicoherentUnit). Nothing below assumes any of it”.

The image of the structure sheaf under an equivalence of categories of quasi-coherent modules is invertible. Let X and Y be quasi-compact and quasi-separated schemes and let e : QCoh(𝒪_X) ≌ QCoh(𝒪_Y) be an equivalence. Then e(𝒪_X) is an invertible 𝒪_Y-module.

Invertibility of a module on a scheme is local on the base (Stacks.Modules.isInvertible_of_isInvertible_restrict_isOpenCover), the opens V i of the reconstruction cover Y, and over each of them e(𝒪_X) is the invertible sheaf L i of that chart by AlgebraicGeometry.restrictMapUnitIsoOfChartIso.

theorem isInvertible_map_quasicoherentUnit_of_quasicoherentEquivalence :
    Stacks.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.2
      (e.functor.obj (quasicoherentUnit X)).obj

AlgebraicGeometry.exists_isOpenCover_invertibleModule_restrictIso_of_isAffineOpenCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/ReconstructionGlobalModule.lean, line 288. The attribute's comment: “the GLOBAL form with the per-chart invertible sheaves GLUED into one invertible 𝒪_Y-module: X and Y quasi-compact and quasi-separated, an affine open cover U i of X, and no further hypothesis. The chart data is exists_isOpenCover_schemeIso_invertibleSheaf_of_isAffineOpenCover (ReconstructionGlobalForm.lean:236) with the families pulled out of the per-index existential; what is new is the last conjunct, a SINGLE invertible 𝒪_Y-module restricting to every L i. It is exists_invertibleModule_of_isOpenCover_of_overlapCompatible (ReconstructionGluedModule.lean:197) run on these charts, its transition data being transOfRestrictIso for the module e(𝒪_X), which restricts to each L i by restrictMapUnitIsoOfChartIso. The SCHEME half of the tag is exists_schemeIso_of_quasicoherentEquivalence (ReconstructionGlobalSchemeIso.lean:324). The comparison of functors e(F) ≅ f^*F ⊗ M, naturally in F, is NOT produced here: it is exists_natIso_pullbackTensorFunctor_of_quasicoherentEquivalence (ReconstructionGlobalComparison.lean), and it is stated for the module e(𝒪_X) rather than for the M glued here — taking e(𝒪_X) is what makes the per-chart comparisons agree at 𝒪_X, because then the identification of its restriction with L i is restrictMapUnitIsoOfChartIso, built from the same α i and β i. Nothing in this statement assumes it”.

The global form of [Stacks, Tag 0GPJ] with the per-chart invertible sheaves glued into one invertible module. Let X and Y be quasi-compact and quasi-separated schemes, let e : QCoh(𝒪_X) ≌ QCoh(𝒪_Y) be an equivalence and let U i be an affine open cover of X. Then there are opens V i covering Y, each affine, and for each i an equivalence F i : QCoh(𝒪_{U i}) ≌ QCoh(𝒪_{V i}) compatible with e and the two restrictions, an isomorphism of schemes f i : V i ≅ U i and an invertible sheaf L i of 𝒪_{V i}-modules with F i inverse image along f i followed by - ⊗ L i — and a single invertible 𝒪_Y-module M whose restriction to each V i is L i.

This is AlgebraicGeometry.exists_isOpenCover_schemeIso_invertibleSheaf_of_isAffineOpenCover with the families pulled out of the per-index existential, together with AlgebraicGeometry.exists_invertibleModule_of_isOpenCover_of_overlapCompatible run on those charts. The three transition hypotheses of the gluing are AlgebraicGeometry.transOfRestrictIso, AlgebraicGeometry.transOfRestrictIso_resLE and AlgebraicGeometry.transOfRestrictIso_trans for the module e(𝒪_X), which restricts to each L i by AlgebraicGeometry.restrictMapUnitIsoOfChartIso.

theorem exists_isOpenCover_invertibleModule_restrictIso_of_isAffineOpenCover {κ : Type u}
    (U : κ → X.Opens) (hUaff : ∀ i, IsAffineOpen (U i)) (hUcover : IsOpenCover U) :
    ∃ (V : κ → Y.Opens)
      (F : ∀ i, (SheafOfModules.isQuasicoherent (U i).toScheme.ringCatSheaf).FullSubcategory ⥤
        (SheafOfModules.isQuasicoherent (V i).toScheme.ringCatSheaf).FullSubcategory)
      (f : ∀ i, (V i).toScheme ≅ (U i).toScheme)
      (L : ∀ i, SheafOfModules.{u} (V i).toScheme.ringCatSheaf) (M : Y.Modules),
      IsOpenCover V ∧ (∀ i, IsAffineOpen (V i)) ∧ (∀ i, (F i).IsEquivalence) ∧
        (∀ i, Stacks.SheafOfModules.IsInvertible (V i).toScheme.presheaf
          (V i).toScheme.ringCatSheaf.2 (L i)) ∧
        (∀ i, Nonempty (e.functor ⋙ quasicoherentRestriction (V i).ι ≅
          quasicoherentRestriction (U i).ι ⋙ F i)) ∧
        (∀ i, Nonempty (F i ⋙ ObjectProperty.ι
            (SheafOfModules.isQuasicoherent (V i).toScheme.ringCatSheaf) ≅
          pullbackTensorFunctor (f i).hom (L i))) ∧
        Stacks.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.2 M ∧
        ∀ i, Nonempty (Scheme.Modules.restrict M (V i).ι ≅ L i)

AlgebraicGeometry.exists_schemeIso_of_quasicoherentEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/ReconstructionGlobalSchemeIso.lean, line 369. The attribute's comment: “the SCHEME HALF of the tag's conclusion, unconditionally: X and Y quasi-compact and quasi-separated and an equivalence of their categories of quasi-coherent modules give an isomorphism of schemes Y ≅ X. No cover, no affineness, no invertible module and no further hypothesis of any kind beyond qcqs. This is the step the Stacks source dismisses with "We omit the details", carried out: the charts are matched (ReconstructionGlobalForm.lean), they cover Y (ReconstructionCover.lean:164), they agree on overlaps in both directions (ReconstructionOverlapCompatible.lean:256, ReconstructionGlobalSchemeIso.lean:223) because the matched pair is rigid (ReconstructionRigidity.lean:141), and they glue (ReconstructionGluedIso.lean:113). The MODULE half — 0GPJ also asserts a single invertible 𝒪_Y-module L with e(F) ≅ f^*F ⊗ L — is NOT produced here: it is isInvertible_map_quasicoherentUnit_of_quasicoherentEquivalence (ReconstructionGlobalModule.lean), the module being e(𝒪_X), and the comparison of functors is exists_natIso_pullbackTensorFunctor_of_quasicoherentEquivalence (ReconstructionGlobalComparison.lean). Nothing in this statement assumes either”.

The scheme half of [Stacks, Tag 0GPJ] with no cover hypothesised. Two quasi-compact quasi-separated schemes with equivalent categories of quasi-coherent modules are isomorphic.

This is the statement above with the affine open cover of X deleted: X is covered by its own affine opens, AlgebraicGeometry.iSup_affineOpens_eq_top, and that family is indexed by AlgebraicGeometry.Scheme.affineOpens, a type in the same universe.

theorem exists_schemeIso_of_quasicoherentEquivalence {X Y : Scheme.{u}} [CompactSpace X]
    [QuasiSeparatedSpace X] [CompactSpace Y] [QuasiSeparatedSpace Y]
    (e : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory ≌
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf).FullSubcategory) :
    Nonempty (Y ≅ X)

AlgebraicGeometry.exists_isAffineOpen_schemeIso_invertibleSheaf_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/ReconstructionLocalForm.lean, line 78. The attribute's comment: “steps 3 to 8 only: the statement LOCALIZED at one affine open U ⊆ X, with the module G of step 2 given as a hypothesis. This is the per-chart building block; the statement over a whole cover is AlgebraicGeometry.exists_isOpenCover_schemeIso_invertibleSheaf_of_isAffineOpenCover, where the covering of Y is proved (AlgebraicGeometry.isOpenCover_of_supportedCorrespondence) and G is produced rather than hypothesised, so nothing in this clause is left open by this file alone. Step 9's descent datum is available too: AlgebraicGeometry.restrictionSquareFunctor makes F_U explicit with rfl section formulas (the localization lift has no formula on sections, which is why it is rebuilt), and AlgebraicGeometry.ReconstructionGlue.glueData is a complete FunctorGlueData, all five fields, its covering hypothesis discharged by AlgebraicGeometry.exists_gluedQuasicoherentFunctor_restrictIso. What remains open for 0GPJ as a whole is the gluing of the per-chart f_U and L_U into a single isomorphism Y ≅ X and a single invertible 𝒪_Y-module, which the source dismisses with "We omit the details". As in the affine case the comparison of functors is stated after forgetting quasi-coherence, between functors into all 𝒪_V-modules”.

Stacks Project, Tag 0GPJ, steps 3 to 8: the local form of the proposition. Let X and Y be quasi-compact and quasi-separated schemes and let e : QCoh(𝒪_X) ≌ QCoh(𝒪_Y) be an equivalence. Let U ⊆ X be an affine open and let G be a finitely presented quasi-coherent 𝒪_X-module whose support is the complement of U. Then there is a quasi-compact open V ⊆ Y — namely the complement of the support of e.functor.obj G — which is affine, and there are an equivalence F_U : QCoh(𝒪_U) ≌ QCoh(𝒪_V) compatible with e and the two restrictions, an isomorphism of schemes f_U : V ≅ U and an invertible sheaf L_U of 𝒪_V-modules such that F_U is inverse image along f_U followed by - ⊗_{𝒪_V} L_U.

theorem exists_isAffineOpen_schemeIso_invertibleSheaf_of_isFinitePresentation (U : X.Opens)
    (hUaff : IsAffineOpen U)
    (G : (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory)
    [SheafOfModules.IsFinitePresentation (R := X.ringCatSheaf) G.obj]
    (hG : supportSet G.obj = (U : Set X)ᶜ) :
    ∃ V : Y.Opens, IsAffineOpen V ∧ IsCompact (V : Set Y) ∧
      ∃ (F : (SheafOfModules.isQuasicoherent U.toScheme.ringCatSheaf).FullSubcategory ⥤
          (SheafOfModules.isQuasicoherent V.toScheme.ringCatSheaf).FullSubcategory)
        (f : V.toScheme ≅ U.toScheme) (L : SheafOfModules.{u} V.toScheme.ringCatSheaf),
        F.IsEquivalence ∧
          Stacks.SheafOfModules.IsInvertible V.toScheme.presheaf V.toScheme.ringCatSheaf.2 L ∧
          Nonempty (e.functor ⋙ quasicoherentRestriction V.ι ≅
            quasicoherentRestriction U.ι ⋙ F) ∧
          Nonempty (F ⋙ ObjectProperty.ι
              (SheafOfModules.isQuasicoherent V.toScheme.ringCatSheaf) ≅
            pullbackTensorFunctor f.hom L)
Sources
LeanAlgebraicGeometry.isFinitelyPresentable_iff_isFinitePresentation · AlgebraicGeometry.exists_nonzero_hom_of_supp_subset · AlgebraicGeometry.supportContained_eq_serreCoproductClosure · AlgebraicGeometry.quasicoherentSupportedOn_isSerreClass · AlgebraicGeometry.quasicoherentRestriction_isLocalization · AlgebraicGeometry.quasicoherentSupportedQuotientEquivalence · AlgebraicGeometry.quasicoherentSupportedQuotientEquivalenceFunctorIso · AlgebraicGeometry.AffineOfModuleCategory.isAffine_of_quasicoherentModules_equivalent_moduleCat

Section56.7 Functors between categories of coherent modules#

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

Tag 0FZL, a lemma

Tag 0FZL in the Stacks Project.

AlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.preservesCoproducts, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/DirectSums.lean, line 269. The attribute's comment: “direct_sums”.

Stacks Project, Tag 0FZL. An extension of an additive functor on coherent modules commutes with arbitrary direct sums of quasi-coherent modules.

lemma FilteredColimitExtension.preservesCoproducts (E : FilteredColimitExtension X Y F)
    (J : Type u) : PreservesColimitsOfShape (Discrete J) E.functor

AlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/Exactness.lean, line 554. The attribute's comment: “left_exactness”.

Stacks Project, Tag 0FZL. The extension of a left exact functor on the coherent modules of a Noetherian scheme is left exact.

theorem FilteredColimitExtension.preservesFiniteLimits {X Y : Scheme.{u}}
    [IsNoetherian X] [IsNoetherian Y]
    {F : CoherentModules X.ringCatSheaf ⥤ CoherentModules Y.ringCatSheaf}
    (E : FilteredColimitExtension X Y F) [PreservesFiniteLimits F] :
    PreservesFiniteLimits E.functor

AlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/Exactness.lean, line 567. The attribute's comment: “right_exactness”.

Stacks Project, Tag 0FZL. The extension of a right exact functor on the coherent modules of a Noetherian scheme is right exact.

theorem FilteredColimitExtension.preservesFiniteColimits {X Y : Scheme.{u}}
    [IsNoetherian X] [IsNoetherian Y]
    {F : CoherentModules X.ringCatSheaf ⥤ CoherentModules Y.ringCatSheaf}
    (E : FilteredColimitExtension X Y F) [PreservesFiniteColimits F] :
    PreservesFiniteColimits E.functor

AlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.exactFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/Exactness.lean, line 580. The attribute's comment: “exactness”.

Stacks Project, Tag 0FZL. The extension of an exact functor on the coherent modules of a Noetherian scheme is exact.

theorem FilteredColimitExtension.exactFunctor {X Y : Scheme.{u}}
    [IsNoetherian X] [IsNoetherian Y]
    {F : CoherentModules X.ringCatSheaf ⥤ CoherentModules Y.ringCatSheaf}
    (E : FilteredColimitExtension X Y F)
    (hF : exactFunctor (CoherentModules X.ringCatSheaf) (CoherentModules Y.ringCatSheaf) F) :
    exactFunctor (SheafOfModules.isQuasicoherent X.ringCatSheaf).FullSubcategory
      (SheafOfModules.isQuasicoherent Y.ringCatSheaf).FullSubcategory E.functor

AlgebraicGeometry.CoherentModuleFunctors.filteredColimitExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/Extension.lean, line 389. The attribute's comment: “extension”.

Stacks Project, Tag 0FZL. A functor from the coherent modules on a Noetherian scheme to the coherent modules on a scheme extends to a functor on quasi-coherent modules which commutes with filtered colimits.

noncomputable def filteredColimitExtension (X Y : Scheme.{u}) [IsNoetherian X]
    (F : CoherentModules X.ringCatSheaf ⥤
      CoherentModules Y.ringCatSheaf) :
    FilteredColimitExtension X Y F

AlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.existsUnique_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/Extension.lean, line 416. The attribute's comment: “extension”.

Stacks Project, Tag 0FZL. Two filtered-colimit-preserving extensions are related by a unique natural isomorphism compatible with their specified identifications on the coherent modules.

theorem FilteredColimitExtension.existsUnique_iso {X Y : Scheme.{u}} [IsNoetherian X]
    {F : CoherentModules X.ringCatSheaf ⥤
      CoherentModules Y.ringCatSheaf}
    (E₁ E₂ : FilteredColimitExtension X Y F) :
    ∃! e : E₁.functor ≅ E₂.functor,
      Functor.whiskerLeft (coherentToQuasicoherent X) e.hom =
        (E₁.iso.trans E₂.iso.symm).hom
Tag 0GPK, a lemma

Tag 0GPK in the Stacks Project.

AlgebraicGeometry.CoherentModuleFunctors.exists_iso_pullbackTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/EquivalenceReconstruction.lean, line 193.

Stacks Project, Tag 0GPK. Let X and Y be Noetherian schemes and let F : Coh(𝒪_X) ⥤ Coh(𝒪_Y) be an equivalence of categories. Then there are an isomorphism of schemes f : Y ⟶ X and an invertible 𝒪_Y-module ℒ with F(𝓕) = f^*𝓕 ⊗ ℒ, naturally in the coherent 𝒪_X-module 𝓕. The corresponding description of an equivalence of the categories of quasi-coherent modules is Tag 0GPJ, available here as exists_iso_pullbackTensor_quasicoherent; the coherent case follows from it by extending F to the quasi-coherent modules. Nothing is hypothesised.

theorem exists_iso_pullbackTensor {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    (F : CoherentModules X.ringCatSheaf ⥤ CoherentModules Y.ringCatSheaf) [F.IsEquivalence] :
    ∃ (f : Y ≅ X) (L : Y.Modules),
      Stacks.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.2 L ∧
      Nonempty (coherentToModules X ⋙ pullbackTensor f.hom L ≅ F ⋙ coherentToModules Y)
Tag 0GPL, a remark

Tag 0GPL in the Stacks Project.

AlgebraicGeometry.CoherentModuleFunctors.exists_iso_pullbackTensor_over_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/EquivalenceOverBase.lean, line 281.

Stacks Project, Tag 0GPL. Let R be a commutative ring, let X and Y be Noetherian schemes over R, and let F : Coh(𝒪_X) ⥤ Coh(𝒪_Y) be an equivalence of categories which is linear over R. Then the isomorphism of schemes f : Y ≅ X and the invertible 𝒪_Y-module ℒ of Tag 0GPK with F(𝓕) = f^*𝓕 ⊗ ℒ may be chosen with f a morphism of schemes over R, that is with f ≫ (X → Spec R) = (Y → Spec R).

Nothing is hypothesised. Tag 0GPK is unconditional, so the content here is only the refinement over R: R-linearity of F forces f to be a morphism over R.

theorem exists_iso_pullbackTensor_over_base (X Y : Over (Spec (.of R)))
    [IsNoetherian X.left] [IsNoetherian Y.left]
    (F : CoherentModules X.left.ringCatSheaf ⥤ CoherentModules Y.left.ringCatSheaf)
    [F.IsEquivalence] :
    letI : Linear R (SheafOfModules.{u} X.left.ringCatSheaf) := modulesLinear R X
    letI : Linear R (SheafOfModules.{u} Y.left.ringCatSheaf) := modulesLinear R Y
    F.Linear R →
      ∃ (f : Y.left ≅ X.left) (L : Y.left.Modules),
        Stacks.SheafOfModules.IsInvertible Y.left.presheaf Y.left.ringCatSheaf.2 L ∧
        Nonempty (coherentToModules X.left ⋙ pullbackTensor f.hom L ≅
          F ⋙ coherentToModules Y.left) ∧
        f.hom ≫ X.hom = Y.hom
Tag 0FZM, a lemma

Tag 0FZM in the Stacks Project.

Stacks.AlgebraicGeometry.CoherentModuleFunctors.isFinite_of_isCoherent_pushforward_of_isZero_higherDirectImages, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/FinitenessCriterion.lean, line 369.

A finiteness criterion. Let f : V ⟶ X be a quasi-finite separated morphism of Noetherian schemes. If there is a coherent 𝒪_V-module 𝒦 whose support is all of V such that f_*𝒦 is coherent and R^q f_*𝒦 = 0 for every q > 0, then f is finite.

Quasi-finiteness is [Stacks, Tag 02NG] — locally quasi-finite and of finite type — which in Mathlib's vocabulary is AlgebraicGeometry.LocallyQuasiFinite, AlgebraicGeometry.LocallyOfFiniteType and AlgebraicGeometry.QuasiCompact together. The existential over 𝒦 of the source is taken as an explicit hypothesis.

Finiteness is Zariski-local on the target, and every hypothesis restricts to an affine open U of X: coherence and the support condition because they are local, and the vanishing of the higher direct images by the comparison R^q(f|_U)_*(𝒦|_{f^{-1}U}) ≅ (R^q f_*𝒦)|_U of [Stacks, Tag 01E5]. Over an affine target the statement is isFinite_of_isAffine_target.

public theorem isFinite_of_isCoherent_pushforward_of_isZero_higherDirectImages
    {V X : Scheme.{u}} (f : V ⟶ X) [IsNoetherian V] [IsNoetherian X]
    [LocallyOfFiniteType f] [LocallyQuasiFinite f] [QuasiCompact f] [IsSeparated f]
    (K : V.Modules) [K.IsCoherent] (hsupp : SheafOfModules.supp K = Set.univ)
    (hpush : ((Scheme.Modules.pushforward f).obj K).IsCoherent)
    (hvanish : ∀ q : ℤ, 0 < q →
      IsZero (((Scheme.Modules.pushforward f).rightDerivedPlus q).obj K)) :
    IsFinite f
Tag 0FZN, a lemma

Tag 0FZN in the Stacks Project.

AlgebraicGeometry.CoherentKernels.isEquivalence_coherentIntegralTransformFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentKernels/Equivalence.lean, line 216. The attribute's comment: “sending a coherent kernel flat over X with support finite over Y to the restriction to Coh of its integral transform is an equivalence onto the k-linear exact functors Coh(O_X) to Coh(O_Y)”.

Stacks Project, Tag 0FZN. Let k be a field and let X and Y be schemes of finite type over k with X separated. Sending a coherent 𝒪_{X ×_k Y}-module 𝒦, flat over X and with support finite over Y, to the restriction to Coh(𝒪_X) of its integral transform 𝓕 ↦ pr_{2,*}(pr_1^*𝓕 ⊗ 𝒦) is an equivalence of categories onto the k-linear exact functors Coh(𝒪_X) ⥤ Coh(𝒪_Y).

Finite type over k is LocallyOfFiniteType together with QuasiCompact; X ×_k Y is the fibre product over Spec k. The functor is coherentIntegralTransformFunctor, whose value at 𝒦 is by definition the restriction of quasicoherentIntegralTransform k X Y 𝒦 (coherentIntegralTransformFunctor_obj_obj_comp), the pullback--tensor--pushforward formula integralTransformFormula after forgetting quasi-coherence.

theorem isEquivalence_coherentIntegralTransformFunctor :
    (coherentIntegralTransformFunctor k X Y).IsEquivalence
Tag 0FZP, a lemma

Tag 0FZP in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.exists_section_iso_pushforward_of_invertible_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/InvertiblePushforwardSection.lean, line 372.

Let f : X ⟶ Y be a separated morphism of finite type and let F be a quasi-coherent 𝒪_X-module of finite type whose scheme-theoretic support is finite over Y. If the direct image f_* F is invertible, then f admits a section s, and F is the direct image along s of f_* F.

public theorem exists_section_iso_pushforward_of_invertible_pushforward
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    [IsFinite ((Scheme.Modules.annihilatorIdeal F).subschemeι ≫ f)]
    [AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.property
      ((Scheme.Modules.pushforward f).obj F)] :
    ∃ s : Y ⟶ X, s ≫ f = 𝟙 Y ∧
      Nonempty (F ≅ (Scheme.Modules.pushforward s).obj
        ((Scheme.Modules.pushforward f).obj F))
Tag 0FZQ, a lemma

Tag 0FZQ in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.iso_pushforward_section_of_invertible_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/QuasiCoherent/InvertiblePushforwardSection.lean, line 654.

Let f : X ⟶ Y be a separated morphism of finite type with a section s, and let Y be reduced. A quasi-coherent 𝒪_X-module F of finite type supported on the image of s and with invertible direct image f_* F is the direct image along s of f_* F.

public theorem iso_pushforward_section_of_invertible_pushforward
    {X Y : Scheme.{u}} (f : X ⟶ Y) (s : Y ⟶ X)
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f]
    (hs : s ≫ f = 𝟙 Y) [IsReduced Y]
    (F : X.Modules) [F.IsQuasicoherent] [F.IsFiniteType]
    (hsupp : SheafOfModules.supp F ⊆ Set.range s.base)
    [AlgebraicGeometry.SheafOfModules.IsInvertible Y.presheaf Y.ringCatSheaf.property
      ((Scheme.Modules.pushforward f).obj F)] :
    Nonempty (F ≅ (Scheme.Modules.pushforward s).obj
      ((Scheme.Modules.pushforward f).obj F))
Tag 0FZR, a lemma

Tag 0FZR in the Stacks Project.

AlgebraicGeometry.CoherentModuleFunctors.exists_iso_pullbackTensor_over_field, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FunctorsAndMorphisms/CoherentModuleFunctors/EquivalenceOverField.lean, line 107. The attribute's comment: “with X SEPARATED and Y REDUCED deleted: the source uses those two hypotheses in its second proof only, and the deduction carried out here — from Tag 0GPL, with finite type over the field giving Noetherian by isNoetherian_of_finiteType_over_field — does not need them, so the statement is more general than the source's and implies it. Finite type is LocallyOfFiniteType together with QuasiCompact. As in Tags 0GPK and 0GPL the prescribed form of the functor is stated after the fully faithful inclusions of the coherent modules into all 𝒪-modules, where the inverse image and the tensor product live”.

Stacks Project, Tag 0FZR. Let k be a field, let X and Y be schemes of finite type over k, and let F : Coh(𝒪_X) ⥤ Coh(𝒪_Y) be an equivalence of categories which is k-linear. Then there are an isomorphism of schemes f : Y ≅ X over k, that is with f ≫ (X → Spec k) = (Y → Spec k), and an invertible 𝒪_Y-module ℒ with F(𝓕) = f^*𝓕 ⊗ ℒ, naturally in the coherent 𝒪_X-module 𝓕.

Finite type is LocallyOfFiniteType X.hom together with QuasiCompact X.hom; this makes X and Y Noetherian by isNoetherian_of_finiteType_over_field, which is what Tag 0GPL needs, and k-linearity is what makes its f a morphism over k.

Nothing is hypothesised: Tag 0GPL is unconditional, so the content here is only the passage from Noetherian to finite type over k.

The source states the lemma with X separated and Y reduced. Those hypotheses are used by its second proof only; the deduction from Tag 0GPK and Tag 0GPL carried out here does not need them, so they are absent and the statement is correspondingly more general.

theorem exists_iso_pullbackTensor_over_field (k : Type u) [Field k]
    (X Y : Over (Spec (.of k)))
    [LocallyOfFiniteType X.hom] [QuasiCompact X.hom]
    [LocallyOfFiniteType Y.hom] [QuasiCompact Y.hom]
    (F : CoherentModules X.left.ringCatSheaf ⥤ CoherentModules Y.left.ringCatSheaf)
    [F.IsEquivalence] :
    letI : Linear k (SheafOfModules.{u} X.left.ringCatSheaf) := modulesLinear k X
    letI : Linear k (SheafOfModules.{u} Y.left.ringCatSheaf) := modulesLinear k Y
    F.Linear k →
      ∃ (f : Y.left ≅ X.left) (L : Y.left.Modules),
        Stacks.SheafOfModules.IsInvertible Y.left.presheaf Y.left.ringCatSheaf.2 L ∧
        Nonempty (coherentToModules X.left ⋙ pullbackTensor f.hom L ≅
          F ⋙ coherentToModules Y.left) ∧
        f.hom ≫ X.hom = Y.hom
Sources
LeanAlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.preservesCoproducts · AlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.preservesFiniteLimits · AlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.preservesFiniteColimits · AlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.exactFunctor · AlgebraicGeometry.CoherentModuleFunctors.filteredColimitExtension · AlgebraicGeometry.CoherentModuleFunctors.FilteredColimitExtension.existsUnique_iso · AlgebraicGeometry.CoherentModuleFunctors.exists_iso_pullbackTensor · AlgebraicGeometry.CoherentModuleFunctors.exists_iso_pullbackTensor_over_base

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.