106.16 Tensor functors

Section106.16 Tensor functors#

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

Tag 0GRJ, a lemma

Tag 0GRJ in the Stacks Project.

AlgebraicGeometry.Stack.existsUnique_tensorExtension_coherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TensorFunctorExtensionNoetherian.lean, line 57.

Stacks 0GRJ. Let 𝒳 and 𝒴 be Noetherian algebraic stacks. Any right exact tensor functor F' : Coh(π’ͺ_𝒳) ⟢ Coh(π’ͺ_𝒴) β€” additive, preserving finite colimits, and a functor of monoidal categories (Stacks 0FFL) β€” extends to a right exact tensor functor F : QCoh(π’ͺ_𝒳) ⟢ QCoh(π’ͺ_𝒴) commuting with all (small) colimits, in particular with direct sums: there is an identification e of the restriction of F to Coh(π’ͺ_𝒳) with F' (followed by the inclusion of Coh(π’ͺ_𝒴)), compatible with the tensor structures. The extension is unique up to unique isomorphism: for any other functor G commuting with filtered colimits and identification e', there is a unique isomorphism F β‰… G restricting to e' ⁻¹ ∘ e on coherent modules, and it is compatible with any tensor structure on G for which e' is.

The input "every quasi-coherent module is a filtered colimit of coherent ones" is Stacks 0GRF (AlgebraicGeometry.Stack.AlgebraicStacks.isFiltered_coherentSubobject_and_isColimit), in the form AlgebraicGeometry.Stack.ind_coherentQuasicoherent.

theorem existsUnique_tensorExtension_coherent
    (𝒳 𝒴 : AlgebraicStacks.{u, w} B S hS) (h𝒳 : IsNoetherianStack.{u, w, w'} B S hS 𝒳)
    (h𝒴 : IsNoetherianStack.{u, w, w'} B S hS 𝒴) :
    haveI := coherentQuasicoherent_isMonoidal B S hS 𝒳 h𝒳.2.2
    haveI := coherentQuasicoherent_isMonoidal B S hS 𝒴 h𝒴.2.2
    βˆ€ (F' : (coherentQuasicoherent B S hS 𝒳).FullSubcategory β₯€
        (coherentQuasicoherent B S hS 𝒴).FullSubcategory) [F'.Additive]
      [PreservesFiniteColimits F'] (hF' : F'.TensorStructure),
      βˆƒ (F : FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
          𝒳.val.isFiberedInGroupoids β₯€
          FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒴.val.val.p
            𝒴.val.isFiberedInGroupoids)
        (e : (coherentQuasicoherent B S hS 𝒳).ΞΉ β‹™ F β‰… F' β‹™ (coherentQuasicoherent B S hS 𝒴).ΞΉ)
        (hF : F.TensorStructure),
        (F.Additive ∧ PreservesFiniteColimits F ∧ PreservesColimitsOfSize.{u, u} F ∧
          (hF.restrict (coherentQuasicoherent B S hS 𝒳)).IsCompatible
            (hF'.compΞΉ (coherentQuasicoherent B S hS 𝒴)) e) ∧
        βˆ€ (G : FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
            𝒳.val.isFiberedInGroupoids β₯€
            FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒴.val.val.p
              𝒴.val.isFiberedInGroupoids),
          PreservesFilteredColimitsOfSize.{u, u} G β†’
            βˆ€ (e' : (coherentQuasicoherent B S hS 𝒳).ΞΉ β‹™ G β‰…
                F' β‹™ (coherentQuasicoherent B S hS 𝒴).ΞΉ),
              βˆƒ! Ο† : F β‰… G, Functor.whiskerLeft (coherentQuasicoherent B S hS 𝒳).ΞΉ Ο†.hom =
                  (e β‰ͺ≫ e'.symm).hom ∧
                βˆ€ hG : G.TensorStructure,
                  (hG.restrict (coherentQuasicoherent B S hS 𝒳)).IsCompatible
                    (hF'.compΞΉ (coherentQuasicoherent B S hS 𝒴)) e' β†’
                    hF.IsCompatible hG Ο†
Tag 0GRK, a lemma

Tag 0GRK in the Stacks Project.

AlgebraicGeometry.Stack.exists_ringHom_tensorFunctor_comp_quasicoherentPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TensorFunctors/TensorFunctorAffineDiagonal.lean, line 146.

Stacks 0GRK. Let 𝒳 be an algebraic stack with affine diagonal, R a ring and F : QCoh(π’ͺ_𝒳) β₯€ Mod_R a right exact tensor functor (additive, preserving finite colimits, lax symmetric monoidal) which commutes with direct sums. Let g : U ⟢ 𝒳 be a morphism with U an affine scheme, with ring of global functions A. Then g is affine, and

  1. C = F(g_{QCoh,*}π’ͺ_U) is a commutative R-algebra (AlgebraicGeometry.Stack.affineTensorAlgebra with its CommRing and Algebra R instances), and
  2. there is a ring map Ο† : A β†’ C

such that F ∘ g_{QCoh,*} sends M to M βŠ—_A C seen as an R-module: both as a functor Mod_A β₯€ Mod_R through M ↦ M~, and as a functor QCoh(π’ͺ_U) β₯€ Mod_R through N ↦ Ξ“(U, N), which is how QCoh(π’ͺ_U) is Mod_A (AlgebraicGeometry.Stack.tildeCounitIso).

"Affine diagonal" is absolute, as in the source (Morphisms of Stacks, Definition 050D): it is the diagonal of the view of 𝒳 over the terminal scheme Spec β„€ (AlgebraicGeometry.Stack.AlgebraicStacks.viewOverIntegers), which lies in every big fppf site (AlgebraicGeometry.Stack.contains_terminalScheme). That g is affine is AlgebraicGeometry.Stack.AlgebraicStacks.isAffineHom_of_isAffineHom_diagonal_viewOverIntegers (Stacks 0GQE over Spec β„€).

theorem exists_ringHom_tensorFunctor_comp_quasicoherentPushforward
    (hΞ” : Stack.IsAffineHom B (⊀_ Scheme.{u}) (contains_terminalScheme B)
      (diagonal.{u, u, u + 1} B (⊀_ Scheme.{u}) (contains_terminalScheme B)
        (AlgebraicStacks.viewOverIntegers B S hS (contains_terminalScheme B) 𝒳).val))
    (hUaff : IsAffineOver B S hS U) (g : schemeStack.{u, w} B S hS U ⟢ 𝒳) :
    βˆƒ hg : AlgebraicStacks.IsAffineHom B S hS g,
      βˆƒ Ο† : schemeGlobalRing U β†’+* affineTensorAlgebra g hg F,
        Nonempty (tildeQuasicoherent.{u, w} U β‹™ affineQuasicoherentPushforward g hg β‹™ F β‰…
          ModuleCat.extendScalars Ο† β‹™
            ModuleCat.restrictScalars (algebraMap R (affineTensorAlgebra g hg F))) ∧
        Nonempty (affineQuasicoherentPushforward g hg β‹™ F β‰…
          quasicoherentGlobalSections.{u, w} U β‹™ ModuleCat.extendScalars Ο† β‹™
            ModuleCat.restrictScalars (algebraMap R (affineTensorAlgebra g hg F)))
Tag 0GRL, a lemma

Tag 0GRL in the Stacks Project.

AlgebraicGeometry.Stack.universallyInjective_affineTensorAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/TensorFunctors/AffineTensorAlgebraUniversallyInjective.lean, line 60.

Stacks 0GRL. Let 𝒳 be a Noetherian algebraic stack with affine diagonal, R a ring and F : QCoh(π’ͺ_𝒳) β₯€ Mod_R a right exact tensor functor (additive, preserving finite colimits, symmetric monoidal) which commutes with direct sums. Let g : U ⟢ 𝒳 be a flat and surjective morphism from an affine scheme U. Then g is affine, and the structure map R ⟢ C of the commutative R-algebra C = F(g_{QCoh,*}π’ͺ_U) of Stacks 0GRK (AlgebraicGeometry.Stack.affineTensorAlgebra) is universally injective.

"Affine diagonal" is absolute, as in Stacks 0GRK: the diagonal of the view of 𝒳 over the terminal scheme Spec β„€ (AlgebraicGeometry.Stack.AlgebraicStacks.viewOverIntegers). The proof is AlgebraicGeometry.Stack.universallyInjective_affineTensorAlgebra_of_coherentGeneration with Stacks 0GRF (AlgebraicGeometry.Stack.AlgebraicStacks.isFiltered_coherentSubobject_and_isColimit, in the form AlgebraicGeometry.Stack.ind_coherentQuasicoherent) as its input.

theorem universallyInjective_affineTensorAlgebra
    (hΞ” : Stack.IsAffineHom B (⊀_ Scheme.{u}) (contains_terminalScheme B)
      (diagonal.{u, u, u + 1} B (⊀_ Scheme.{u}) (contains_terminalScheme B)
        (AlgebraicStacks.viewOverIntegers B S hS (contains_terminalScheme B) 𝒳).val))
    (h𝒳 : IsNoetherianStack.{u, w, w'} B S hS 𝒳) (hUaff : IsAffineOver B S hS U)
    {R : Type u} [CommRing R]
    (F : AlgebraicStacks.quasicoherentModules B S hS 𝒳 β₯€ ModuleCat.{u} R) [F.Braided]
    [F.Additive] [PreservesFiniteColimits F] [βˆ€ J : Type u, PreservesColimitsOfShape (Discrete J) F]
    (g : schemeStack.{u, w} B S hS U ⟢ 𝒳) (hflat : AlgebraicStacks.IsFlat B S hS g)
    (hsurj : IsSurjective B S hS g) :
    βˆƒ hg : AlgebraicStacks.IsAffineHom B S hS g,
      Algebra.UniversallyInjective R (affineTensorAlgebra g hg F)
Tag 0GRM, a lemma

Tag 0GRM in the Stacks Project.

Algebra.faithfullyFlat_of_flat_selfTensor_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Exercises/NonExercises/FaithfullyFlatSelfBaseChange.lean, line 41.

A universally injective ring map whose two self-base-change coprojections are flat is faithfully flat.

theorem faithfullyFlat_of_flat_selfTensor_of_universallyInjective
    {B : Type u} [CommRing B] {C : Type u} [CommRing C] [Algebra B C]
    (hleft : ((Algebra.TensorProduct.includeLeft : C →ₐ[B] C βŠ—[B] C).toRingHom).Flat)
    (_hright : ((Algebra.TensorProduct.includeRight : C →ₐ[B] C βŠ—[B] C).toRingHom).Flat)
    (hBC : Algebra.UniversallyInjective B C) :
    (algebraMap B C).FaithfullyFlat
Tag 0GRN, a lemma

Tag 0GRN in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.isIso_tensorPushforwardMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/TensorPushforwardAffineLeg.lean, line 1037. The attribute's comment: β€œcorrected (one leg affine): for a : 𝒴 ⟢ 𝒳 affine, quasi-compact, quasi-separated and flat and b : 𝒡 ⟢ 𝒳 representable, quasi-compact and quasi-separated, the canonical map a_{QCoh,}O_𝒴 βŠ— b_{QCoh,}O_𝒡 ⟢ f_{QCoh,}O_{𝒴 Γ—_𝒳 𝒡} is an isomorphism. Added relative to the source: a affine (as printed the tag is false, not_forall_nonempty_tensorPushforwardUnits_iso: two disjoint punctured planes, where HΒΉ(V,O) β‰  0 and Ξ“(V,O) is not flat over the base, so H⁰ of the derived tensor product is not the tensor product). Affineness makes a_O be Ξ“(V,O) with V affine and flat over the base, so the last step is flat base change of H⁰. Dropped: flatness of b (not needed)”. References: SGA 3 VIB (11.1), β€œmore general”.

Stacks 0GRN, corrected: one leg affine. Let a : 𝒴 ⟢ 𝒳 be an affine (Stacks 0CHQ), quasi-compact, quasi-separated and flat 1-morphism of algebraic stacks and b : 𝒡 ⟢ 𝒳 one which is representable (by schemes), quasi-compact and quasi-separated. For the projection f = pr₁ ≫ a : 𝒴 Γ—_𝒳 𝒡 ⟢ 𝒳 of the canonical 2-fibre product, the canonical map ΞΌ : a_{QCoh,*}π’ͺ_𝒴 βŠ—_{π’ͺ_𝒳} b_{QCoh,*}π’ͺ_𝒡 ⟢ f_{QCoh,*}π’ͺ_{𝒴 Γ—_𝒳 𝒡} (AlgebraicGeometry.Stack.AlgebraicStacks.tensorPushforwardMap, s βŠ— t ↦ pr₁^*s Β· prβ‚‚^*t) is an isomorphism in QCoh(π’ͺ_𝒳); here g_{QCoh,*} = quasicoherentDirectImage g, βŠ— is the tensor product sheaf of Stacks 0GQM and π’ͺ = πŸ™_.

Relative to the source: a is in addition affine. Without it the statement is false (AlgebraicGeometry.Stack.AlgebraicStacks.not_forall_nonempty_tensorPushforwardUnits_iso: for the two disjoint punctured planes V, W of Spec k[x,y,z,w]/(xz,xw,yz,yw) the right hand side is 0 and the left hand side has global sections Ξ“(V, π’ͺ) βŠ— Ξ“(W, π’ͺ) = k); the source's proof breaks at reading off H⁰ of the derived tensor product, which needs HΒΉ(V, π’ͺ) = 0 and flatness of Ξ“(V, π’ͺ) over the base. With a affine, a_*π’ͺ is computed by Ξ“(V, π’ͺ) with V affine and flat over the base, and the last step is flat base change of H⁰. Flatness of b, and representability of a beyond what affineness gives, are not needed and are dropped.

theorem isIso_tensorPushforwardMap (ha : AlgebraicStacks.IsAffineHom B S hS a)
    (haqc : IsQuasiCompactMorphism B S hS a) (haqs : AlgebraicStacks.IsQuasiSeparated B S hS a)
    (haf : AlgebraicStacks.IsFlat B S hS a)
    (hbr : Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒡.val.val.p 𝒳.val.val.p
      (CatFiberedInGroupoids.homFunctor b.hom))
    (hbqc : IsQuasiCompactMorphism B S hS b) (hbqs : AlgebraicStacks.IsQuasiSeparated B S hS b) :
    IsIso (tensorPushforwardMap a b)

AlgebraicGeometry.Stack.AlgebraicStacks.nonempty_iso_tensorPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/TensorPushforwardAffineLeg.lean, line 1100. The attribute's comment: β€œcorrected (one leg affine), the asserted isomorphism a_{QCoh,}O_𝒴 βŠ— b_{QCoh,}O_𝒡 β‰… f_{QCoh,*}O_{𝒴 Γ—_𝒳 𝒡}, for a affine, quasi-compact, quasi-separated and flat and b representable, quasi-compact and quasi-separated; see isIso_tensorPushforwardMap for the added hypothesis (a affine) and why it is needed”.

Stacks 0GRN, corrected (one leg affine), the asserted isomorphism a_{QCoh,*}π’ͺ_𝒴 βŠ— b_{QCoh,*}π’ͺ_𝒡 β‰… f_{QCoh,*}π’ͺ_{𝒴 Γ—_𝒳 𝒡}, under the hypotheses of AlgebraicGeometry.Stack.AlgebraicStacks.isIso_tensorPushforwardMap.

theorem nonempty_iso_tensorPushforward (ha : AlgebraicStacks.IsAffineHom B S hS a)
    (haqc : IsQuasiCompactMorphism B S hS a) (haqs : AlgebraicStacks.IsQuasiSeparated B S hS a)
    (haf : AlgebraicStacks.IsFlat B S hS a)
    (hbr : Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒡.val.val.p 𝒳.val.val.p
      (CatFiberedInGroupoids.homFunctor b.hom))
    (hbqc : IsQuasiCompactMorphism B S hS b) (hbqs : AlgebraicStacks.IsQuasiSeparated B S hS b) :
    Nonempty ((quasicoherentDirectImage B S hS a).obj (πŸ™_ _) βŠ—
        (quasicoherentDirectImage B S hS b).obj (πŸ™_ _) β‰…
      (quasicoherentDirectImage B S hS
        ((twoFibreProductSquareAlgebraicStacks B S hS a b).fst ≫ a)).obj (πŸ™_ _))

AlgebraicGeometry.Stack.AlgebraicStacks.not_forall_nonempty_tensorPushforwardUnits_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/TensorPushforwardStackCounterexample.lean, line 604. The attribute's comment: β€œas printed it is false: a counterexample at X = Spec A, A = k[x,y,z,w]/(xz,xw,yz,yw), with a, b the open immersions of the two punctured planes D(z) βˆͺ D(w) and D(x) βˆͺ D(y); the 2-fibre product is empty so f_{QCoh,}O = 0, while a_{QCoh,}O βŠ— b_{QCoh,*}O β‰  0 since Ξ“(V,O) βŠ—_A Ξ“(W,O) = k (HΒΉ(V,O) β‰  0 and Ξ“(V,O) is not A-flat)”.

Stacks 0GRN, as printed, is false. It is not true that for all 1-morphisms a : 𝒴 ⟢ 𝒳, b : 𝒡 ⟢ 𝒳 of algebraic stacks which are representable (by schemes), quasi-compact, quasi-separated and flat, a_{QCoh,*}π’ͺ_𝒴 βŠ—_{π’ͺ_𝒳} b_{QCoh,*}π’ͺ_𝒡 β‰… f_{QCoh,*}π’ͺ_{𝒴 Γ—_𝒳 𝒡} for the projection f : 𝒴 Γ—_𝒳 𝒡 ⟢ 𝒳 of the 2-fibre product; not even an abstract isomorphism exists in general.

The counterexample: X = Spec A, A = k[x, y, z, w] / (xz, xw, yz, yw) the union of two planes meeting at the origin, viewed as an algebraic stack over itself, and a, b the open immersions of the punctured planes V = D(z) βˆͺ D(w) and W = D(x) βˆͺ D(y). They are disjoint, so the right hand side is 0, while on global sections the left hand side is Ξ“(V, π’ͺ) βŠ—_A Ξ“(W, π’ͺ) = k[z, w] βŠ—_A k[x, y] = k. Here quasicoherentDirectImage is f_{QCoh,*} of Stacks 077A, βŠ— the tensor product of QCoh(π’ͺ_𝒳) of Stacks 0GQM (the local instance fppfModulesMonoidal, the tensor product sheaf) and πŸ™_ the structure sheaf. The source's proof breaks at its last step: the KΓΌnneth formula (Lemma 0FLQ) computes Rf_*π’ͺ = Ra_*π’ͺ βŠ—^𝐋 Rb_*π’ͺ, and reading off H⁰ of the right hand side as a_*π’ͺ βŠ— b_*π’ͺ needs HΒΉ(V, π’ͺ) = 0 or flatness; here HΒΉ(V, π’ͺ) β‰  0 (a punctured plane) and Ξ“(V, π’ͺ) = A / (x, y) is not flat over A. The same failure occurs with a = b the open immersion D(x) βˆͺ D(z) β†’ Spec k[x, y, z, w] / (xy - zw) (AlgebraicGeometry.TensorPushforwardCounterexample.not_injective_lmul'_coneSections). The statement holds when one leg is affine (AlgebraicGeometry.Stack.AlgebraicStacks.isIso_tensorPushforwardMap).

theorem not_forall_nonempty_tensorPushforwardUnits_iso :
    Β¬ βˆ€ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      (𝒳 𝒴 𝒡 : AlgebraicStacks.{u, w} B S hS) (a : 𝒴 ⟢ 𝒳) (b : 𝒡 ⟢ 𝒳),
      Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒴.val.val.p 𝒳.val.val.p
        (CatFiberedInGroupoids.homFunctor a.hom) β†’
      IsQuasiCompactMorphism B S hS a β†’ AlgebraicStacks.IsQuasiSeparated B S hS a β†’
      AlgebraicStacks.IsFlat B S hS a β†’
      Stacks.RepresentableMorphism.IsRepresentableMorphism 𝒡.val.val.p 𝒳.val.val.p
        (CatFiberedInGroupoids.homFunctor b.hom) β†’
      IsQuasiCompactMorphism B S hS b β†’ AlgebraicStacks.IsQuasiSeparated B S hS b β†’
      AlgebraicStacks.IsFlat B S hS b β†’
      Nonempty ((quasicoherentDirectImage B S hS a).obj (πŸ™_ _) βŠ—
          (quasicoherentDirectImage B S hS b).obj (πŸ™_ _) β‰…
        (quasicoherentDirectImage B S hS
          ((twoFibreProductSquareAlgebraicStacks B S hS a b).fst ≫ a)).obj (πŸ™_ _))

AlgebraicGeometry.Stack.quasicoherentTensorPushforwardMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasicoherentTensorPushforward.lean, line 358. The attribute's comment: β€œTHE CANONICAL MAP ONLY, NOT THE ASSERTION. This is ΞΌ : a_{QCoh,}π’ͺ_𝒴 βŠ— b_{QCoh,}π’ͺ_𝒡 ⟢ f_{QCoh,*}π’ͺ_𝒫, built from the two relative pullback maps of Stacks 06UM and the comparison of Remark 0GQR. Its INVERTIBILITY, which is what the tag asserts, is NOT PROVED here: the Γ©tale-local step (the content of Cohomology of Stacks Section 103.12, namely Lemma 0GQH plus the scheme-level KΓΌnneth of Lemma 0FLQ) does not compose with the stack-level QCoh monoidal product without further infrastructure. The reduction lemmas below that conclude invertibility from invertibility after a reflecting functor are deliberately left UNTAGGED, being instances of CategoryTheory.isIso_of_reflects_iso rather than content of this tag”.

The canonical map ΞΌ. For 1-morphisms a : 𝒴 ⟢ 𝒳, b : 𝒡 ⟢ 𝒳 of algebraic stacks and a 2-fibre product square sq over the cospan (a, b) with apex 𝒫 = 𝒴 Γ—_𝒳 𝒡 and projection f = sq.fst ≫ a, the map

ΞΌ : a_{QCoh, *}π’ͺ_𝒴 βŠ—_{π’ͺ_𝒳} b_{QCoh, *}π’ͺ_𝒡 ⟢ f_{QCoh, *}π’ͺ_𝒫

given by the tensor product of the two relative pullback maps AlgebraicGeometry.Stack.quasicoherentRelativePullbackMap along the legs sq.fst and sq.snd, followed by the comparison of Remark 0GQR attached to the coherator of Lemma 0778 at the relative cup product cup.

def quasicoherentTensorPushforwardMap :
    FibredSite.quasicoherentTensorObj B S hS 𝒳.val.val.p 𝒳.val.property
        ((flatBaseChangeQuasicoherator B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX hclosed
            hpres hls hlsD hwp hsep).obj
          (aStar.obj ((quasicoherentToFlatBaseChange B E hE S hS 𝒴.val.val.p 𝒴.val.property
            hincY).obj (FibredSite.quasicoherentTensorUnit B S hS 𝒴.val.val.p 𝒴.val.property))))
        ((flatBaseChangeQuasicoherator B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX hclosed
            hpres hls hlsD hwp hsep).obj
          (bStar.obj ((quasicoherentToFlatBaseChange B E hE S hS 𝒡.val.val.p 𝒡.val.property
            hincZ).obj (FibredSite.quasicoherentTensorUnit B S hS 𝒡.val.val.p
              𝒡.val.property)))) ⟢
      (flatBaseChangeQuasicoherator B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX hclosed hpres
          hls hlsD hwp hsep).obj
        (fStar.obj ((quasicoherentToFlatBaseChange B E hE S hS sq.pt.val.val.p
          sq.pt.val.property hincP).obj
            (FibredSite.quasicoherentTensorUnit B S hS sq.pt.val.val.p sq.pt.val.property)))

AlgebraicGeometry.Stack.quasicoherentTensorPushforwardMap_eq_coheratorCupProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasicoherentTensorPushforward.lean, line 393. The attribute's comment: β€œthe identification of ΞΌ with Q of the relative cup product precomposed with the two relative pullback maps on LQCoh^fbc, i.e. that applying the coherator commutes with tensoring the two maps of Stacks 06UM in”.

ΞΌ is the comparison of Remark 0GQR at a single map out of a tensor product. Tensoring the two relative pullback maps and then applying the comparison of the coherator is the same as applying the comparison to the relative cup product precomposed with those two maps on LQCoh^fbc(π’ͺ_𝒳).

theorem quasicoherentTensorPushforwardMap_eq_coheratorCupProduct :
    (quasicoherentTensorPushforwardMap B E hE S hS a b sq hincX hincY hincZ hincP hclosed hpres hls
        hlsD hwp hsep
        aStar bStar fStar hlqY prStarY adjPrY cmpY hlqZ prStarZ adjPrZ cmpZ
        TLQ tcmp cup) =
      coheratorCupProduct (flatBaseChangeQuasicoheratorAdjunction B E hE S hS 𝒳.val.val.p
          𝒳.val.property hincX
      hclosed hpres hls hlsD hwp hsep)
        (Functor.uncurry.obj (FibredSite.quasicoherentTensorBifunctor B S hS
      𝒳.val.val.p 𝒳.val.property)) TLQ tcmp
        (TLQ.map ((locallyQuasicoherentStructurePullbackMap B E hE S hS hincY hincP aStar fStar
      sq.fst hlqY prStarY adjPrY cmpY) Γ—β‚˜
            (locallyQuasicoherentStructurePullbackMap B E hE S hS hincZ hincP bStar fStar
      sq.snd hlqZ prStarZ adjPrZ cmpZ)) ≫ cup)

AlgebraicGeometry.Stack.map_quasicoherentTensorPushforwardMap_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasicoherentTensorPushforward.lean, line 427. The attribute's comment: β€œcommutativity of the diagram of Remark 0GQR at ΞΌ, over the same carried data”.

The diagram of Remark 0GQR commutes at ΞΌ. The inclusion of Lemma 0778 applied to ΞΌ, followed by the counit of the coherator adjunction, is the comparison tcmp of Lemma 0GQM followed by the counit in each tensor factor and then by the relative cup product precomposed with the two relative pullback maps.

theorem map_quasicoherentTensorPushforwardMap_comp_counit :
    (quasicoherentToFlatBaseChange B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX).map
          (quasicoherentTensorPushforwardMap B E hE S hS a b sq hincX hincY hincZ hincP hclosed
              hpres hls hlsD hwp hsep
        aStar bStar fStar hlqY prStarY adjPrY cmpY hlqZ prStarZ adjPrZ cmpZ
        TLQ tcmp cup) ≫
        (flatBaseChangeQuasicoheratorAdjunction B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX
      hclosed hpres hls hlsD hwp hsep).counit.app
          (fStar.obj ((quasicoherentToFlatBaseChange B E hE S hS sq.pt.val.val.p sq.pt.val.property
              hincP).obj
        (FibredSite.quasicoherentTensorUnit B S hS sq.pt.val.val.p sq.pt.val.property))) =
      tcmp.app ((flatBaseChangeQuasicoherator B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX hclosed
          hpres hls hlsD hwp hsep).obj (aStar.obj
            ((quasicoherentToFlatBaseChange B E hE S hS 𝒴.val.val.p 𝒴.val.property hincY).obj
                (FibredSite.quasicoherentTensorUnit B S hS 𝒴.val.val.p 𝒴.val.property))),
          (flatBaseChangeQuasicoherator B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX hclosed hpres
              hls hlsD hwp hsep).obj (bStar.obj
            ((quasicoherentToFlatBaseChange B E hE S hS 𝒡.val.val.p 𝒡.val.property hincZ).obj
                (FibredSite.quasicoherentTensorUnit B S hS 𝒡.val.val.p 𝒡.val.property)))) ≫
        TLQ.map ((flatBaseChangeQuasicoheratorAdjunction B E hE S hS 𝒳.val.val.p 𝒳.val.property
            hincX
      hclosed hpres hls hlsD hwp hsep).counit.app
              (aStar.obj ((quasicoherentToFlatBaseChange B E hE S hS 𝒴.val.val.p 𝒴.val.property
                  hincY).obj
                (FibredSite.quasicoherentTensorUnit B S hS 𝒴.val.val.p 𝒴.val.property))) Γ—β‚˜
            (flatBaseChangeQuasicoheratorAdjunction B E hE S hS 𝒳.val.val.p 𝒳.val.property hincX
      hclosed hpres hls hlsD hwp hsep).counit.app
              (bStar.obj ((quasicoherentToFlatBaseChange B E hE S hS 𝒡.val.val.p 𝒡.val.property
                  hincZ).obj
                (FibredSite.quasicoherentTensorUnit B S hS 𝒡.val.val.p 𝒡.val.property)))) ≫
          (TLQ.map ((locallyQuasicoherentStructurePullbackMap B E hE S hS hincY hincP aStar fStar
      sq.fst hlqY prStarY adjPrY cmpY) Γ—β‚˜
              (locallyQuasicoherentStructurePullbackMap B E hE S hS hincZ hincP bStar fStar
      sq.snd hlqZ prStarZ adjPrZ cmpZ)) ≫ cup)
Tag 0GRP, a lemma

Tag 0GRP in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.eq_and_exists_iso_pointPullbackTransportIso_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/PointPullbackFullyFaithful.lean, line 631. The attribute's comment: β€œpoints over possibly different structure morphisms; they agree”.

Stacks 0GRP. Let 𝒳 be an algebraic stack with affine diagonal and B a ring. Let f₁, fβ‚‚ : Spec B ⟢ 𝒳 be two morphisms, given as points x₁, xβ‚‚ of 𝒳 over Spec B, with structure morphisms q₁, qβ‚‚ : Spec B ⟢ S, and let t : f₁^* β‰… fβ‚‚^* be an isomorphism of the tensor functors f_i^* : QCoh(π’ͺ_𝒳) β₯€ Mod_B (AlgebraicGeometry.Stack.AlgebraicStacks.pointPullback, a braided monoidal additive functor; t is monoidal). Then q₁ = qβ‚‚, and there is a 2-arrow f₁ ⟢ fβ‚‚, an isomorphism a : x₁ β‰… xβ‚‚ lying over the identity of Spec B, inducing t.

"Affine diagonal" is absolute, as in the source (Morphisms of Stacks, Definition 050D): it is the diagonal of the view of 𝒳 over Spec β„€, AlgebraicGeometry.Stack.AlgebraicStacks.viewOverIntegers. The structure morphisms to S are not assumed equal: that they agree is part of the conclusion, read off from the functions B ⟢ Ξ“(x_i, π’ͺ) which t preserves (it is monoidal). The form with equal structure morphisms is AlgebraicGeometry.Stack.AlgebraicStacks.exists_iso_pointPullbackTransportIso_eq_of_over.

The proof does not follow the source's chart and descent, but takes the chart g = f₁ : Spec B ⟢ 𝒳 itself (affine, the diagonal being affine): with W_i = Spec B Γ—_{f_i, 𝒳, f₁} Spec B and g_*π’ͺ = g_{QCoh,*}π’ͺ_{Spec B}, f_i^*(g_*π’ͺ) = Ξ“(W_i), and t gives a ring isomorphism Ξ“(Wβ‚‚) ⟢ Ξ“(W₁) over both copies of B (it is monoidal and natural, the multiplication of g_*π’ͺ being AlgebraicGeometry.Stack.AlgebraicStacks.affineDirectImageMul), hence an arrow W₁ ⟢ Wβ‚‚; the image of the identity 2-arrow of f₁ in W₁ is the 2-arrow f₁ β‰… fβ‚‚. That it induces t follows from naturality of t and the units M ⟢ g_* g^* M. This is the content of Stacks 0GRK (the algebra C = F(g_{QCoh,*}π’ͺ_U) with its map A ⟢ C) for the point pullbacks, computed directly.

theorem eq_and_exists_iso_pointPullbackTransportIso_eq
    (hΞ” : Stack.IsAffineHom B (⊀_ Scheme.{u}) (contains_terminalScheme B)
      (Stack.diagonal.{u, u, u + 1} B (⊀_ Scheme.{u}) (contains_terminalScheme B)
        (AlgebraicStacks.viewOverIntegers B S hS (contains_terminalScheme B) 𝒳).val))
    {q₁ qβ‚‚ : B.obj hR ⟢ B.obj hS} {x₁ xβ‚‚ : 𝒳.val.val.obj}
    (hx₁ : 𝒳.val.val.p.obj x₁ = Over.mk q₁) (hxβ‚‚ : 𝒳.val.val.p.obj xβ‚‚ = Over.mk qβ‚‚)
    (t : pointPullback B S hS 𝒳 x₁ (overSpecIso B S hS 𝒳 hx₁) β‰…
      pointPullback B S hS 𝒳 xβ‚‚ (overSpecIso B S hS 𝒳 hxβ‚‚)) [NatTrans.IsMonoidal t.hom] :
    q₁ = qβ‚‚ ∧ βˆƒ (a : x₁ β‰… xβ‚‚) (ha : (BigFppfOver.toScheme B S hS).map (𝒳.val.val.p.map a.hom) ≫
        (overSpecIso B S hS 𝒳 hxβ‚‚).hom = (overSpecIso B S hS 𝒳 hx₁).hom),
      pointPullbackTransportIso B S hS 𝒳 (overSpecIso B S hS 𝒳 hx₁) (overSpecIso B S hS 𝒳 hxβ‚‚)
        a ha = t

AlgebraicGeometry.Stack.AlgebraicStacks.exists_iso_pointPullbackTransportIso_eq_of_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/PointPullbackFullyFaithful.lean, line 662. The attribute's comment: β€œthe source's form, with equal structure morphisms”.

Stacks 0GRP, with equal structure morphisms (the source's statement). Let 𝒳 be an algebraic stack with affine diagonal (over Spec β„€), B a ring and f₁, fβ‚‚ : Spec B ⟢ 𝒳 two morphisms over S, given as points x₁, xβ‚‚ of 𝒳 lying over the same object Spec B ⟢ S of the site. Every isomorphism t : f₁^* β‰… fβ‚‚^* of the tensor functors f_i^* : QCoh(π’ͺ_𝒳) β₯€ Mod_B is induced by a 2-arrow f₁ ⟢ fβ‚‚: an isomorphism a : x₁ β‰… xβ‚‚ of the fibre over Spec B.

theorem exists_iso_pointPullbackTransportIso_eq_of_over
    (hΞ” : Stack.IsAffineHom B (⊀_ Scheme.{u}) (contains_terminalScheme B)
      (Stack.diagonal.{u, u, u + 1} B (⊀_ Scheme.{u}) (contains_terminalScheme B)
        (AlgebraicStacks.viewOverIntegers B S hS (contains_terminalScheme B) 𝒳).val))
    {q : B.obj hR ⟢ B.obj hS} {x₁ xβ‚‚ : 𝒳.val.val.obj}
    (hx₁ : 𝒳.val.val.p.obj x₁ = Over.mk q) (hxβ‚‚ : 𝒳.val.val.p.obj xβ‚‚ = Over.mk q)
    (t : pointPullback B S hS 𝒳 x₁ (overSpecIso B S hS 𝒳 hx₁) β‰…
      pointPullback B S hS 𝒳 xβ‚‚ (overSpecIso B S hS 𝒳 hxβ‚‚)) [NatTrans.IsMonoidal t.hom] :
    βˆƒ (a : x₁ β‰… xβ‚‚) (ha : 𝒳.val.val.p.map a.hom = eqToHom (hx₁.trans hxβ‚‚.symm)),
      pointPullbackTransportIso B S hS 𝒳 (overSpecIso B S hS 𝒳 hx₁) (overSpecIso B S hS 𝒳 hxβ‚‚)
        a (toScheme_map_comp_overSpecIso B S hS 𝒳 hx₁ hxβ‚‚ a ha) = t
Tag 0GRQ, a lemma

Tag 0GRQ in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.existsUnique_pointPullback_iso_of_tensorFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/TensorFunctorPoint.lean, line 110. The attribute's comment: β€œthe morphism Spec R ⟢ 𝒳 is a point over Spec R in the site; uniqueness is up to the unique 2-arrow inducing the given isomorphism of tensor functors”.

Stacks 0GRQ. Let 𝒳 be a Noetherian algebraic stack with affine diagonal (over Spec β„€, as in the source), R a ring (with Spec R in the site) and F : QCoh(π’ͺ_𝒳) β₯€ Mod_R a right exact tensor functor (additive, preserving finite colimits, braided monoidal) which commutes with direct sums. Then F comes from a unique morphism Spec R ⟢ 𝒳:

  1. there are a point x of 𝒳 over Spec R (lying over some q : Spec R ⟢ S) and an isomorphism of tensor functors e : F β‰… x^*;
  2. if e₁ : F β‰… x₁^* and eβ‚‚ : F β‰… xβ‚‚^* are two such, over q₁ and qβ‚‚, then q₁ = qβ‚‚ and there is a unique 2-arrow a : x₁ β‰… xβ‚‚ over the identity of Spec R whose induced isomorphism x₁^* β‰… xβ‚‚^* is e₁⁻¹ ≫ eβ‚‚.
theorem existsUnique_pointPullback_iso_of_tensorFunctor
    (h𝒳 : IsNoetherianStack.{u, w, w'} B S hS 𝒳)
    (hΞ” : Stack.IsAffineHom B (⊀_ Scheme.{u}) (contains_terminalScheme B)
      (Stack.diagonal.{u, u, u + 1} B (⊀_ Scheme.{u}) (contains_terminalScheme B)
        (viewOverIntegers B S hS (contains_terminalScheme B) 𝒳).val))
    {R : Type u} [CommRing R] (hR : B.Contains (Spec (CommRingCat.of R)))
    (F : quasicoherentModules B S hS 𝒳 β₯€ ModuleCat.{u} R) [F.Additive] [F.Braided]
    [PreservesFiniteColimits F] [βˆ€ J : Type u, PreservesColimitsOfShape (Discrete J) F] :
    (βˆƒ (q : B.obj hR ⟢ B.obj hS) (x : 𝒳.val.val.obj) (hx : 𝒳.val.val.p.obj x = Over.mk q)
        (e : F β‰… pointPullback B S hS 𝒳 x (overSpecIso B S hS 𝒳 hx)), NatTrans.IsMonoidal e.hom) ∧
    βˆ€ {q₁ qβ‚‚ : B.obj hR ⟢ B.obj hS} {x₁ xβ‚‚ : 𝒳.val.val.obj}
      (hx₁ : 𝒳.val.val.p.obj x₁ = Over.mk q₁) (hxβ‚‚ : 𝒳.val.val.p.obj xβ‚‚ = Over.mk qβ‚‚)
      (e₁ : F β‰… pointPullback B S hS 𝒳 x₁ (overSpecIso B S hS 𝒳 hx₁))
      (eβ‚‚ : F β‰… pointPullback B S hS 𝒳 xβ‚‚ (overSpecIso B S hS 𝒳 hxβ‚‚)),
      NatTrans.IsMonoidal e₁.hom β†’ NatTrans.IsMonoidal eβ‚‚.hom β†’
      q₁ = qβ‚‚ ∧ βˆƒ (a : x₁ β‰… xβ‚‚) (ha : (BigFppfOver.toScheme B S hS).map (𝒳.val.val.p.map a.hom) ≫
          (overSpecIso B S hS 𝒳 hxβ‚‚).hom = (overSpecIso B S hS 𝒳 hx₁).hom),
        pointPullbackTransportIso B S hS 𝒳 (overSpecIso B S hS 𝒳 hx₁) (overSpecIso B S hS 𝒳 hxβ‚‚)
            a ha = e₁.symm β‰ͺ≫ eβ‚‚ ∧
          βˆ€ (b : x₁ β‰… xβ‚‚) (hb : (BigFppfOver.toScheme B S hS).map (𝒳.val.val.p.map b.hom) ≫
              (overSpecIso B S hS 𝒳 hxβ‚‚).hom = (overSpecIso B S hS 𝒳 hx₁).hom),
            pointPullbackTransportIso B S hS 𝒳 (overSpecIso B S hS 𝒳 hx₁)
              (overSpecIso B S hS 𝒳 hxβ‚‚) b hb = e₁.symm β‰ͺ≫ eβ‚‚ β†’ b = a
Tag 0GRR, a theorem

Tag 0GRR in the Stacks Project.

AlgebraicGeometry.Stack.AlgebraicStacks.existsUnique_coherentPointPullback_iso_of_tensorFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/CoherentTensorFunctorPoint.lean, line 61. The attribute's comment: β€œthe morphism Spec R ⟢ 𝒳 is a point over Spec R in the site; uniqueness is up to a 2-arrow inducing the given isomorphism of tensor functors”.

Stacks 0GRR. Let 𝒳 be a Noetherian algebraic stack with affine diagonal (over Spec β„€, as in the source), R a Noetherian ring (with Spec R in the site) and F : Coh(π’ͺ_𝒳) β₯€ Mod^{fg}_R a right exact tensor functor (additive, preserving finite colimits, braided monoidal). Then F comes from a unique morphism Spec R ⟢ 𝒳:

  1. there are a point x of 𝒳 over Spec R (lying over some q : Spec R ⟢ S) and an isomorphism of tensor functors F β‰… x^*|_{Coh};
  2. if E₁ : F β‰… x₁^*|_{Coh} and Eβ‚‚ : F β‰… xβ‚‚^*|_{Coh} are two such, over q₁ and qβ‚‚, then q₁ = qβ‚‚ and there is a 2-arrow a : x₁ β‰… xβ‚‚ over the identity of Spec R inducing E₁⁻¹ ≫ Eβ‚‚ on coherent modules.
theorem existsUnique_coherentPointPullback_iso_of_tensorFunctor
    (h𝒳 : IsNoetherianStack.{u, w, w'} B S hS 𝒳)
    (hΞ” : Stack.IsAffineHom B (⊀_ Scheme.{u}) (contains_terminalScheme B)
      (Stack.diagonal.{u, u, u + 1} B (⊀_ Scheme.{u}) (contains_terminalScheme B)
        (AlgebraicStacks.viewOverIntegers B S hS (contains_terminalScheme B) 𝒳).val))
    [IsNoetherianRing R] (hR : B.Contains (Spec (CommRingCat.of R)))
    (F : Coh.{u, u, w} B S hS 𝒳 β₯€ FGModuleCat.{u} R) [F.Additive] [F.Braided]
    [PreservesFiniteColimits F] :
    (βˆƒ (q : B.obj hR ⟢ B.obj hS) (x : 𝒳.val.val.obj) (hx : 𝒳.val.val.p.obj x = Over.mk q)
      (E : F β‰… coherentPointPullback B S hS 𝒳 x (overSpecIso B S hS 𝒳 hx)),
        NatTrans.IsMonoidal E.hom) ∧
    βˆ€ {q₁ qβ‚‚ : B.obj hR ⟢ B.obj hS} {x₁ xβ‚‚ : 𝒳.val.val.obj}
      (hx₁ : 𝒳.val.val.p.obj x₁ = Over.mk q₁) (hxβ‚‚ : 𝒳.val.val.p.obj xβ‚‚ = Over.mk qβ‚‚)
      (E₁ : F β‰… coherentPointPullback B S hS 𝒳 x₁ (overSpecIso B S hS 𝒳 hx₁))
      (Eβ‚‚ : F β‰… coherentPointPullback B S hS 𝒳 xβ‚‚ (overSpecIso B S hS 𝒳 hxβ‚‚)),
      NatTrans.IsMonoidal E₁.hom β†’ NatTrans.IsMonoidal Eβ‚‚.hom β†’
      q₁ = qβ‚‚ ∧ βˆƒ (a : x₁ β‰… xβ‚‚) (ha : (BigFppfOver.toScheme B S hS).map
          (𝒳.val.val.p.map a.hom) ≫ (overSpecIso B S hS 𝒳 hxβ‚‚).hom =
            (overSpecIso B S hS 𝒳 hx₁).hom),
        Functor.whiskerLeft (coherentQuasicoherentInclusion B S hS 𝒳)
            (pointPullbackTransportIso B S hS 𝒳 (overSpecIso B S hS 𝒳 hx₁)
              (overSpecIso B S hS 𝒳 hxβ‚‚) a ha).hom =
          (coherentPointPullbackCompIso B S hS 𝒳 x₁ _).inv ≫
            Functor.whiskerRight (E₁.inv ≫ Eβ‚‚.hom)
              (forgetβ‚‚ (FGModuleCat.{u} R) (ModuleCat.{u} R)) ≫
              (coherentPointPullbackCompIso B S hS 𝒳 xβ‚‚ _).hom
Sources
LeanAlgebraicGeometry.Stack.existsUnique_tensorExtension_coherent Β· AlgebraicGeometry.Stack.exists_ringHom_tensorFunctor_comp_quasicoherentPushforward Β· AlgebraicGeometry.Stack.universallyInjective_affineTensorAlgebra Β· Algebra.faithfullyFlat_of_flat_selfTensor_of_universallyInjective Β· AlgebraicGeometry.Stack.AlgebraicStacks.isIso_tensorPushforwardMap Β· AlgebraicGeometry.Stack.AlgebraicStacks.nonempty_iso_tensorPushforward Β· AlgebraicGeometry.Stack.AlgebraicStacks.not_forall_nonempty_tensorPushforwardUnits_iso Β· AlgebraicGeometry.Stack.quasicoherentTensorPushforwardMap

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.