24.3 Sheaves of graded algebras to 24.23 Flat resolutions

Section24.3 Sheaves of graded algebras#

Section 24.3 of the Stacks Project, Tag 0FQV. 2 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FQW, a definition

Tag 0FQW in the Stacks Project.

SheafOfModules.GradedAlgebra.UnitalHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExteriorAlgebraPullback.lean, line 121. The attribute's comment: “unital homomorphisms of sheaves of graded algebras”.

A unital homomorphism of sheaves of graded algebras.

structure UnitalHom (A B : GradedAlgebra.{t, a} R)

SheafOfModules.GradedAlgebra.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedAlgebraBridge.lean, line 118. The attribute's comment: “homomorphisms of sheaves of graded algebras, and the category they form”.

A homomorphism of sheaves of graded algebras: a morphism of sheaves of modules in each degree, preserving products of homogeneous local sections. The distinguished degree-zero unit need not be preserved; the homomorphisms that preserve it are UnitalHom.

structure Hom (A B : GradedAlgebra.{t, a} R)

SheafOfModules.GradedAlgebra, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedDegreeColimits.lean, line 123. The attribute's comment: “sheaves of graded algebras, over a sheaf of rings on an arbitrary site”.

A sheaf of ℤ-graded algebras over a sheaf of rings.

structure GradedAlgebra (R : Sheaf J RingCat.{t})

SheafOfModules.reesGradedAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/IdealSheafPowers.lean, line 513. The attribute's comment: “the graded algebra of the powers of a sheaf of ideals”. References: SGA 2 XII (4.2), “partial”.

The sheaf of graded algebras ⨁_{n ≥ 0} 𝓘ⁿ of a sheaf of ideals. Its degree-n homogeneous piece is the n-th power of 𝓘 for n ≥ 0 and the zero sheaf of ideals otherwise, and its multiplication is the multiplication of sections of the structure sheaf.

noncomputable def reesGradedAlgebra : GradedAlgebra.{t, t} R
Tag 0FQX, a remark

Tag 0FQX in the Stacks Project.

Stacks.Sheaves.GradedAlgebraEssentiallySmall.gradedAlgebraPullbackPushforwardAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedAlgebraCounitEssentiallySmall.lean, line 673. The attribute's comment: “part (3): adjunction for graded algebras”.

Part (3) of Stacks 0FQX: pullback of sheaves of graded algebras along a morphism of ringed topoi is left adjoint to the direct image, and the right adjoint has the direct-image graded algebras as its values on objects.

The unit and the counit are unitApp and counitApp, whose degreewise components are those of the Stacks 03D7 adjunction for sheaves of modules; everything else is adjunctionOfGradedUnitCounit.

public noncomputable def gradedAlgebraPullbackPushforwardAdjunction :
    Σ G : SheafOfModules.GradedAlgebra.{w, w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O) ⥤
        SheafOfModules.GradedAlgebra.{w, w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O),
      { _adj : (gradedAlgebraPullbackSpecification f.toRingedToposModulesHom).1 ⊣ G //
        ∀ A, G.obj A = pushforwardGradedAlgebra f A }

SheafOfModules.GradedAlgebra.transport, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedAlgebraFunctoriality.lean, line 340. The attribute's comment: “graded_algebra_pushforward, graded_algebra_pullback”.

The transport of a sheaf of graded algebras along a lax monoidal functor between categories of sheaves of modules, with homogeneous pieces the images F(A_n) of those of A.

noncomputable def transport : GradedAlgebra.{w, w} (toRingCat K Psharp)

SheafOfModules.GradedAlgebra.transportFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedAlgebraFunctoriality.lean, line 425. The attribute's comment: “graded_algebra_pushforward, graded_algebra_pullback: functoriality”.

A lax monoidal functor between categories of sheaves of modules induces a functor between the categories of sheaves of graded algebras.

noncomputable def transportFunctor :
    GradedAlgebra.{w, w} (toRingCat J Osharp) ⥤ GradedAlgebra.{w, w} (toRingCat K Psharp)

SheafOfModules.GradedAlgebra.transportAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedAlgebraMonoidalAdjunction.lean, line 221. The attribute's comment: “part (3): adjunction for graded algebras”.

The transport of sheaves of graded algebras along the left adjoint of a monoidal adjunction is left adjoint to the transport along the right adjoint. For a morphism of ringed topoi this is part (3) of the functoriality of sheaves of graded algebras: the pullback of graded algebras is left adjoint to the pushforward, so homomorphisms f^*B ⟶ A correspond to homomorphisms B ⟶ f_*A, naturally in both arguments.

noncomputable def transportAdjunction :
    transportFunctor L hP hO ⊣ transportFunctor G hO hP

Stacks.Sheaves.GradedAlgebraPullback.gradedAlgebraPullbackSpecification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedAlgebraPullback.lean, line 206. The attribute's comment: “graded_algebra_pullback”.

The degreewise module pullbacks assemble into a functor of sheaves of graded algebras, with the induced multiplication and unit.

This is the pullback half of Stacks 0FQX.

public noncomputable def gradedAlgebraPullbackSpecification :
    GradedAlgebraPullbackSpecification f

Stacks.Sheaves.GradedAlgebraPullback.nonempty_gradedAlgebraPullbackSpecification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedAlgebraPullback.lean, line 222. The attribute's comment: “graded_algebra_pullback”.

A pullback of sheaves of graded algebras exists.

This is the pullback half of Stacks 0FQX; see gradedAlgebraPullbackSpecification.

public theorem nonempty_gradedAlgebraPullbackSpecification :
    Nonempty (GradedAlgebraPullbackSpecification f)

Stacks.Sheaves.GradedAlgebraPushforward.exists_pushforwardGradedAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedAlgebraPushforward/Construction.lean, line 264. The attribute's comment: “graded_algebra_pushforward”.

A graded algebra whose pieces and operations are the canonical direct images of those of the source exists.

public theorem exists_pushforwardGradedAlgebra
    {X : RingedTopos.{u, u, u}}
    {Y : RingedTopos.{u', u', u'}}
    (f : RingedToposHom X Y)
    (A : SheafOfModules.GradedAlgebra
      (Stacks.SheafOfModules.Tensor.ringSheaf (RingedTopos.ringedSite X).O)) :
    ∃ B : SheafOfModules.GradedAlgebra
        (Stacks.SheafOfModules.Tensor.ringSheaf (RingedTopos.ringedSite Y).O),
      IsPushforwardGradedAlgebra f A B

Stacks.Sheaves.GradedAlgebraPushforward.pushforwardGradedAlgebraData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedAlgebraPushforward/Construction.lean, line 277. The attribute's comment: “graded_algebra_pushforward”.

A graded algebra together with its direct-image specification.

public noncomputable def pushforwardGradedAlgebraData
    {X : RingedTopos.{u, u, u}}
    {Y : RingedTopos.{u', u', u'}}
    (f : RingedToposHom X Y)
    (A : SheafOfModules.GradedAlgebra
      (Stacks.SheafOfModules.Tensor.ringSheaf (RingedTopos.ringedSite X).O)) :
    { B : SheafOfModules.GradedAlgebra
        (Stacks.SheafOfModules.Tensor.ringSheaf (RingedTopos.ringedSite Y).O) //
      IsPushforwardGradedAlgebra f A B }
Sources
LeanSheafOfModules.GradedAlgebra.UnitalHom · SheafOfModules.GradedAlgebra.Hom · SheafOfModules.GradedAlgebra · SheafOfModules.reesGradedAlgebra · Stacks.Sheaves.GradedAlgebraEssentiallySmall.gradedAlgebraPullbackPushforwardAdjunction · SheafOfModules.GradedAlgebra.transport · SheafOfModules.GradedAlgebra.transportFunctor · SheafOfModules.GradedAlgebra.transportAdjunction

Section24.4 Sheaves of graded modules#

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

Tag 0FQZ, a definition

Tag 0FQZ in the Stacks Project.

SheafOfModules.GradedModule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedDegreeColimits.lean, line 144. The attribute's comment: “right graded modules, over a sheaf of rings on an arbitrary site”.

A right graded module over a sheaf of graded algebras.

structure GradedModule (A : GradedAlgebra.{t, a} R)

SheafOfModules.GradedModule.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedDegreeColimits.lean, line 178. The attribute's comment: “homomorphisms of right graded modules”.

A homomorphism of right graded modules over a sheaf of graded algebras.

structure Hom (M N : GradedModule.{t, a, m} A)

An instance with no name in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedDegreeColimits.lean, line 219. The attribute's comment: “the category of right graded modules”.

The category of right graded modules over a fixed sheaf of graded algebras.

instance : Category (GradedModule.{t, a, m} A)

SheafOfModules.GradedModule.regularModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedRelativeTensorUnitor.lean, line 108. The attribute's comment: “a sheaf of graded algebras as a right graded module over itself”.

A sheaf of graded algebras, acting on itself on the right. This is the graded counterpart of SheafOfModules.DifferentialGradedModule.regularModule.

def regularModule (A : GradedAlgebra.{t, m} R) : GradedModule.{t, m, m} A

SheafOfModules.LeftGradedModule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftGradedModule.lean, line 58. The attribute's comment: “left graded modules, over a sheaf of rings on an arbitrary site”.

A left graded module over a sheaf of graded algebras.

structure LeftGradedModule (A : GradedAlgebra.{t, a} R)

SheafOfModules.LeftGradedModule.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftGradedModule.lean, line 93. The attribute's comment: “homomorphisms of left graded modules”.

A homomorphism of left graded modules over a sheaf of graded algebras.

structure Hom (M N : LeftGradedModule.{t, a, m} A)

SheafOfModules.LeftGradedModule.instCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftGradedModule.lean, line 135. The attribute's comment: “the category of left graded modules”.

The category of left graded modules over a fixed sheaf of graded algebras.

instance instCategory : Category (LeftGradedModule.{t, a, m} A)
Tag 0FR0, a lemma

Tag 0FR0 in the Stacks Project.

SheafOfModules.GradedModule.hasCoproducts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModuleAbelian.lean, line 1522. The attribute's comment: “direct_sums”.

Graded modules over a sheaf of graded algebras have arbitrary direct sums, formed degreewise.

instance hasCoproducts : HasColimitsOfShape (Discrete ι) (GradedModule.{t, a, m} A)

SheafOfModules.GradedModule.pieceFunctor_preservesCoproducts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModuleAbelian.lean, line 1530. The attribute's comment: “direct_sums”.

Taking a fixed homogeneous component commutes with set-indexed direct sums.

instance pieceFunctor_preservesCoproducts (n : ℤ) :
    PreservesColimitsOfShape (Discrete ι) (pieceFunctor.{t, a, m} A n)

SheafOfModules.GradedModule.abelian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModuleAbelian.lean, line 1570. The attribute's comment: “abelian”.

The category of right graded modules over a sheaf of graded algebras is abelian.

Kernels and cokernels are formed degreewise, and the coimage-image comparison of a homomorphism is an isomorphism because it is one in each homogeneous degree.

noncomputable instance abelian : Abelian (GradedModule.{t, a, m} A)

SheafOfModules.GradedModule.pieceFunctor_preservesColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModuleAbelian.lean, line 1610. The attribute's comment: “degree_preserves_colimits”.

Taking a fixed homogeneous component of a graded module commutes with all colimits.

The module universe is max u m' for a site C : Type u, because that is the hom universe of SheafOfModules.{max u m'} R and PreservesColimits quantifies over diagrams of that size; pieceFunctor_preservesColimitsOfSize' is the same content with the size universe free.

instance pieceFunctor_preservesColimits (n : ℤ) :
    PreservesColimits (pieceFunctor.{t, a, max u m'} A n)

SheafOfModules.GradedModule.pieceFunctor_preservesLimitsOfSize, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModuleDegreeLimits.lean, line 62. The attribute's comment: “degree_preserves_limits”. References: SGA 6 VI (2.7), “partial”.

Taking a fixed homogeneous component of a graded module commutes with all limits.

A limit of any shape of the size of the module universe is built from products and equalizers, and the degree-n component preserves both: products and kernels of graded modules are formed degreewise.

instance pieceFunctor_preservesLimitsOfSize (n : ℤ) :
    PreservesLimitsOfSize.{m, m} (pieceFunctor.{t, a, m} A n)

SheafOfModules.GradedModule.filteredColimits_exact, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModuleFilteredColimits.lean, line 133. The attribute's comment: “filtered_colimits_exact”.

Filtered colimits of right graded modules over a sheaf of graded algebras are exact, at every size at which those colimits exist.

instance filteredColimits_exact (A : GradedAlgebra.{t, a} R)
    [HasFilteredColimitsOfSize.{s, s'} (GradedModule.{t, a, max u m'} A)] :
    AB5OfSize.{s, s'} (GradedModule.{t, a, max u m'} A)

SheafOfModules.GradedModule.ab5OfSize, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModuleFilteredColimits.lean, line 146. The attribute's comment: “filtered_colimits_exact”.

Filtered colimits of right graded modules are exact, unconditionally, at the module universe max u m' of a site C : Type u.

The graded modules have all colimits of that size, so the size hypothesis of filteredColimits_exact is discharged rather than assumed.

theorem ab5OfSize (A : GradedAlgebra.{t, a} R) :
    AB5OfSize.{max u m', max u m'} (GradedModule.{t, a, max u m'} A)

SheafOfModules.GradedModule.hasLimitsOfSize, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModuleLimits.lean, line 62. The attribute's comment: “limits”.

Graded modules over a sheaf of graded algebras admit all small limits.

A limit of any shape of the size of the module universe is built from degreewise products and from equalizers, the latter being the kernel of a difference.

instance hasLimitsOfSize : HasLimitsOfSize.{m, m} (GradedModule.{t, a, m} A)

Declarations registered for the tag:

Sources
LeanSheafOfModules.GradedModule · SheafOfModules.GradedModule.Hom · SheafOfModules.GradedModule.regularModule · SheafOfModules.LeftGradedModule · SheafOfModules.LeftGradedModule.Hom · SheafOfModules.LeftGradedModule.instCategory · SheafOfModules.GradedModule.hasCoproducts · SheafOfModules.GradedModule.pieceFunctor_preservesCoproducts

Section24.5 The graded category of sheaves of graded modules#

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

Tag 0FR1, the section

Tag 0FR1 in the Stacks Project.

SheafOfModules.GradedHomOfDegree, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedInternalHom.lean, line 287. The attribute's comment: “homogeneous homomorphisms of degree n of right graded modules”.

A homomorphism of right graded A-modules homogeneous of degree n: a family of morphisms M^i ⟶ L^{i + n} of sheaves of modules compatible with the right action. These are the elements of Hom^n in the graded category of right graded A-modules.

structure GradedHomOfDegree (M L : GradedModule.{t, a, w} A) (n : ℤ)
Sources
LeanSheafOfModules.GradedHomOfDegree

Section24.6 Tensor product for sheaves of graded modules#

Section 24.6 of the Stacks Project, Tag 0FR2. 1 tag here is carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FR2, the section

Tag 0FR2 in the Stacks Project.

SheafOfModules.RelativeTensor.balanceMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedRelativeTensor.lean, line 735. The attribute's comment: “the map of the presentation, sending x ⊗ a ⊗ y to xa ⊗ y - x ⊗ ay”.

The balance map ⨁_{r+s+t=n} P^r ⊗_O A^s ⊗_O N^t ⟶ ⨁_{p+q=n} P^p ⊗_O N^q of degree n, sending x ⊗ a ⊗ y to xa ⊗ y - x ⊗ ay.

noncomputable def balanceMap (n : ℤ) : relationSum P N n ⟶ tensorSum P N n

SheafOfModules.RelativeTensor.gradedTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedRelativeTensor.lean, line 762. The attribute's comment: “degree n of the graded tensor product, as the cokernel of the balance map”.

Degree n of the relative tensor product P ⊗_A N of a right graded A-module with a left graded A-module: the associated sheaf of the cokernel of the balance map.

noncomputable def gradedTensor (n : ℤ) : SheafOfModules.{m} (toRingCat J Osharp)

SheafOfModules.RelativeTensor.gradedTensorFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedRelativeTensor.lean, line 1032. The attribute's comment: “the functor - ⊗_A N on right graded modules”.

The functor - ⊗_A N from right graded A-modules to graded O-modules, for a fixed left graded A-module N.

noncomputable def gradedTensorFunctor :
    GradedModule.{t, m, m} A ⥤ GradedObject ℤ (SheafOfModules.{m} (toRingCat J Osharp))

SheafOfModules.RelativeTensor.unitorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedRelativeTensorUnitor.lean, line 298. The attribute's comment: “the unit isomorphism A ⊗_A N ≅ N of the relative tensor product, in degree n”.

The unit isomorphism of the relative tensor product: A ⊗_A N ≅ N in degree n, for A a sheaf of graded algebras acting on itself on the right and N a left graded A-module.

noncomputable def unitorIso (n : ℤ) :
    gradedTensor (GradedModule.regularModule A) N n ≅ N.piece n

SheafOfModules.RelativeTensor.isGradedFlat_regularModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedRelativeTensorUnitor.lean, line 337. The attribute's comment: “the regular right graded module is flat, by the unit isomorphism”.

A sheaf of graded algebras is flat as a right graded module over itself. The functor N ↦ A ⊗_A N is isomorphic to the identity by SheafOfModules.RelativeTensor.unitorIso, so it carries a degreewise short exact sequence to a degreewise short exact sequence.

theorem isGradedFlat_regularModule (A : GradedAlgebra.{t, m} (toRingCat J Osharp)) :
    IsGradedFlat (GradedModule.regularModule A)

SheafOfModules.GradedLocalBalanced, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedTensorProduct.lean, line 89. The attribute's comment: “local balanced bilinear families out of a graded module and a bimodule”.

An A-balanced bilinear family of degree n over an object U of the site, from a right graded A-module M and a graded (A, B)-bimodule N to a right graded B-module L: maps M^i|_U × N^j|_U → L^{i + j + n}|_U which are bilinear over the sheaf of rings, compatible with restriction, A-balanced and B-linear in the second variable.

structure GradedLocalBalanced (M : GradedModule.{t, a, w} A) (N : GradedBimodule.{t, a, z} A B)
    (L : GradedModule.{t, a, s} B) (n : ℤ) (U : C)

SheafOfModules.GradedGlobalBalanced, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedTensorProduct.lean, line 208. The attribute's comment: “balanced bilinear families out of a graded module and a bimodule”.

An A-balanced bilinear family of degree n over the whole site: maps M^i × N^j → L^{i + j + n} on sections which are bilinear over the sheaf of rings, compatible with restriction, A-balanced and B-linear in the second variable.

structure GradedGlobalBalanced (M : GradedModule.{t, a, w} A) (N : GradedBimodule.{t, a, z} A B)
    (L : GradedModule.{t, a, s} B) (n : ℤ)

SheafOfModules.IsGradedTensorProduct, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedTensorProduct.lean, line 292. The attribute's comment: “the graded tensor product, by its universal property”.

A right graded B-module T is the tensor product M ⊗_A N of a right graded A-module M with a graded (A, B)-bimodule N when it carries an A-balanced bilinear map tmul of degree zero whose right B-action is (x ⊗ y) b = x ⊗ y b and which is universal: composing a degree-n local homomorphism out of T with tmul is a bijection onto the A-balanced bilinear families of degree n.

structure IsGradedTensorProduct (M : GradedModule.{t, a, w} A)
    (N : GradedBimodule.{t, a, z} A B) (T : GradedModule.{t, a, s} B)
Sources
LeanSheafOfModules.RelativeTensor.balanceMap · SheafOfModules.RelativeTensor.gradedTensor · SheafOfModules.RelativeTensor.gradedTensorFunctor · SheafOfModules.RelativeTensor.unitorIso · SheafOfModules.RelativeTensor.isGradedFlat_regularModule · SheafOfModules.GradedLocalBalanced · SheafOfModules.GradedGlobalBalanced · SheafOfModules.IsGradedTensorProduct

Section24.7 Internal hom for sheaves of graded modules#

Section 24.7 of the Stacks Project, Tag 0FR3. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FR3, the section

Tag 0FR3 in the Stacks Project.

SheafOfModules.GradedLocalHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedInternalHom.lean, line 157. The attribute's comment: “local sections of the graded internal hom”.

A local section of SheafHom^n_A(M, L) over an object U of the site: a map M|_U → L|_U of right graded A|_U-modules homogeneous of degree n, written out as a family of maps on sections over the objects V ⟶ U of the slice site.

structure GradedLocalHom (M : GradedModule.{t, a, w} A) (L : GradedModule.{t, a, z} A) (n : ℤ)
    (U : C)

SheafOfModules.IsGradedSheafHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedInternalHom.lean, line 417. The attribute's comment: “the graded internal hom of two right graded modules”.

A graded sheaf of R-modules G is the graded internal hom SheafHom^gr_A(M, L) of two right graded A-modules when its degree-n sections over U are the degree-n local homomorphisms M|_U → L|_U, additively, R-linearly and compatibly with restriction.

structure IsGradedSheafHom (M : GradedModule.{t, a, w} A) (L : GradedModule.{t, a, z} A)
    (G : ℤ → SheafOfModules.{h} R)
Sources
LeanSheafOfModules.GradedLocalHom · SheafOfModules.IsGradedSheafHom

Section24.8 Sheaves of graded bimodules and tensor-hom adjunction#

Section 24.8 of the Stacks Project, Tag 0FR4. 3 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FR4, the section

Tag 0FR4 in the Stacks Project.

SheafOfModules.GradedLocalHom.actRight, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedInternalHom.lean, line 243. The attribute's comment: “the right A-action on the local sections of the graded internal hom”.

Right multiplication of a local section f of SheafHom^n_B(N, L) over U by a section a of A^m over U, defined by (f a)(y) = f (a y). This involves no signs.

noncomputable def GradedLocalHom.actRight {N : GradedBimodule.{t, a, z} A B}
    {L : GradedModule.{t, a, s} B} {n : ℤ} {U : C}
    (f : GradedLocalHom N.toGradedModule L n U) (m : ℤ)
    (a : (A.piece m).val.obj (Opposite.op U)) :
    GradedLocalHom N.toGradedModule L (n + m) U

SheafOfModules.IsGradedInternalHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedInternalHom.lean, line 503. The attribute's comment: “SheafHom^gr_B(N, L) as a right graded A-module”.

A right graded A-module H is the graded internal hom SheafHom^gr_B(N, L) of a graded (A, B)-bimodule N and a right graded B-module L when its underlying graded sheaf of R-modules is that internal hom and its right A-action is (f a)(y) = f (a y).

structure IsGradedInternalHom (N : GradedBimodule.{t, a, z} A B) (L : GradedModule.{t, a, s} B)
    (H : GradedModule.{t, a, h} A) extends IsGradedSheafHom N.toGradedModule L H.piece

SheafOfModules.balancedEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedTensorHomAdjunction.lean, line 361. The attribute's comment: “local homomorphisms into the internal hom are balanced bilinear families”.

The degree-n local homomorphisms M|_U → SheafHom^gr_B(N, L)|_U of right graded A-modules are the A-balanced bilinear families of degree n over U. This is the local form of the tensor-hom adjunction.

noncomputable def balancedEquiv (hH : IsGradedInternalHom N L H)
    (M : GradedModule.{t, a, w} A) (n : ℤ) (U : C) :
    GradedLocalHom M H n U ≃ GradedLocalBalanced M N L n U
Tag 0FR5, a definition

Tag 0FR5 in the Stacks Project.

SheafOfModules.GradedBimodule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedBimodule.lean, line 59. The attribute's comment: “graded bimodules”.

A graded (A, B)-bimodule is a family of sheaves of modules indexed by ℤ carrying commuting unital left A- and right B-actions.

structure GradedBimodule (A B : GradedAlgebra.{t, a} R)

SheafOfModules.GradedBimodule.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedBimodule.lean, line 95. The attribute's comment: “homomorphisms of graded bimodules”.

A homomorphism of graded (A, B)-bimodules is a degreewise morphism of sheaves of modules which respects both actions.

structure Hom (M N : GradedBimodule.{t, a, m} A B)
Tag 0FR6, a lemma

Tag 0FR6 in the Stacks Project.

SheafOfModules.tensorHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedTensorHomAdjunction.lean, line 390. The attribute's comment: “Hom_{Mod^gr(B)}(M ⊗_A N, L) = Hom_{Mod^gr(A)}(M, SheafHom^gr_B(N, L))”.

Tensor-hom adjunction for sheaves of graded modules, first identity: the degree-n homomorphisms M ⊗_A N → L of right graded B-modules are the degree-n homomorphisms M → SheafHom^gr_B(N, L) of right graded A-modules.

noncomputable def tensorHomEquiv (hT : IsGradedTensorProduct M N T)
    (hH : IsGradedInternalHom N L H) (n : ℤ) :
    GradedHomOfDegree T L n ≃ GradedHomOfDegree M H n

SheafOfModules.isGradedSheafHom_tensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedTensorHomAdjunction.lean, line 423. The attribute's comment: “SheafHom^gr_B(M ⊗_A N, L) = SheafHom^gr_A(M, SheafHom^gr_B(N, L))”.

Tensor-hom adjunction for sheaves of graded modules, second identity: a graded sheaf of R-modules which is the internal hom SheafHom^gr_B(M ⊗_A N, L) is also the internal hom SheafHom^gr_A(M, SheafHom^gr_B(N, L)).

noncomputable def isGradedSheafHom_tensor (hT : IsGradedTensorProduct M N T)
    (hH : IsGradedInternalHom N L H) {G : ℤ → SheafOfModules.{g} R}
    (hG : IsGradedSheafHom T L G) : IsGradedSheafHom M H G
Sources
LeanSheafOfModules.GradedLocalHom.actRight · SheafOfModules.IsGradedInternalHom · SheafOfModules.balancedEquiv · SheafOfModules.GradedBimodule · SheafOfModules.GradedBimodule.Hom · SheafOfModules.tensorHomEquiv · SheafOfModules.isGradedSheafHom_tensor

Section24.9 Pull and push for sheaves of graded modules#

Section 24.9 of the Stacks Project, Tag 0FR7. 2 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FR7, the section

Tag 0FR7 in the Stacks Project.

SheafOfModules.GradedModule.semilinearHomOfDegreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModulePullback.lean, line 442. The attribute's comment: “f_*M corepresents the φ-semilinear homomorphisms into M homogeneous of degree n, the morphisms of the graded category Mod^gr”.

f_*M corepresents the φ-semilinear homomorphisms into M homogeneous of degree n: such a homomorphism out of N is exactly a homomorphism N ⟶ f_*M of right graded B-modules homogeneous of degree n.

noncomputable def semilinearHomOfDegreeEquiv (N : GradedModule.{t, a', m} B)
    (M : GradedModule.{t, a, m} A) (n : ℤ) :
    SemilinearHomOfDegree φ N M n ≃ GradedHomOfDegree N (pushforwardObj φ M) n

SheafOfModules.GradedModule.pushforwardObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedPushforward.lean, line 187. The attribute's comment: “the direct image f_M of a graded module, with multiplication f_μ ∘ (id, φ)”.

The direct image f_*M of a right graded A-module along a morphism of ringed sites and a homomorphism φ : B ⟶ f_*A of sheaves of graded algebras: its degree-n piece is the direct image of the degree-n piece of M, and a homogeneous section b of B acts through φ b.

noncomputable def pushforwardObj (φ : GradedAlgebra.SemilinearHom u σ B A)
    (M : GradedModule.{t, a, m} A) : GradedModule.{t, a', m} B

SheafOfModules.GradedModule.pushforwardMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedPushforward.lean, line 228. The attribute's comment: “the direct image is functorial in the graded module”.

The direct image of a homomorphism of right graded A-modules is its degreewise direct image.

noncomputable def pushforwardMap (φ : GradedAlgebra.SemilinearHom u σ B A)
    {M N : GradedModule.{t, a, m} A} (g : M ⟶ N) :
    pushforwardObj φ M ⟶ pushforwardObj φ N

SheafOfModules.GradedModule.pushforwardFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedPushforward.lean, line 244. The attribute's comment: “the functor f_* : Mod(A) ⥤ Mod(B)”.

The direct image functor f_* : Mod(A) ⥤ Mod(B) on sheaves of graded modules.

noncomputable def pushforwardFunctor (φ : GradedAlgebra.SemilinearHom u σ B A) :
    GradedModule.{t, a, m} A ⥤ GradedModule.{t, a', m} B

SheafOfModules.GradedModule.pushforwardHomOfDegree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedPushforward.lean, line 273. The attribute's comment: “f_* as a functor of graded categories, on homogeneous morphisms of degree n”.

The direct image of a homomorphism of right graded A-modules homogeneous of degree n: the degreewise direct image again, which is homogeneous of degree n. This is the action on morphisms of the induced functor f_* : Mod^gr(A) ⥤ Mod^gr(B) of graded categories, whose action on objects is SheafOfModules.GradedModule.pushforwardObj.

noncomputable def pushforwardHomOfDegree (φ : GradedAlgebra.SemilinearHom u σ B A)
    {M L : GradedModule.{t, a, m} A} {n : ℤ} (g : GradedHomOfDegree M L n) :
    GradedHomOfDegree (pushforwardObj φ M) (pushforwardObj φ L) n

SheafOfModules.GradedModule.semilinearHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedPushforward.lean, line 350. The attribute's comment: “f_*M corepresents the φ-semilinear homomorphisms into M”.

A φ-semilinear homomorphism P ⟶ M is exactly a homomorphism P ⟶ f_*M of right graded B-modules.

noncomputable def semilinearHomEquiv (φ : GradedAlgebra.SemilinearHom u σ B A)
    (P : GradedModule.{t, a', m} B) (M : GradedModule.{t, a, m} A) :
    SemilinearHom φ P M ≃ (P ⟶ pushforwardObj φ M)
Tag 0FR8, a lemma

Tag 0FR8 in the Stacks Project.

SheafOfModules.GradedModule.pullbackHomOfDegreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedModulePullbackConstruction.lean, line 217. The attribute's comment: “Hom_{Mod^gr(B)}(N, f_M) = Hom_{Mod^gr(A)}(f^N, M), in every homogeneous degree, for the pullback f^* of sheaves of graded modules obtained as the left adjoint of the direct image”.

Tag 0FR8: for a morphism of ringed sites f, a sheaf of graded R-algebras A on the source, a sheaf of graded R'-algebras B on the target and a homomorphism φ : B ⟶ f_*A of sheaves of graded algebras, the homomorphisms f^*N ⟶ M of right graded A-modules homogeneous of degree n are exactly the homomorphisms N ⟶ f_*M of right graded B-modules homogeneous of degree n:

Hom_{Mod^gr(B)}(N, f_*M) = Hom_{Mod^gr(A)}(f^*N, M)

Both sides of the source's identification are taken in the graded categories, so the statement is the identification in every homogeneous degree at once.

noncomputable def pullbackHomOfDegreeEquiv (φ : GradedAlgebra.SemilinearHom u σ B A)
    (N : GradedModule.{t, a', max u v a u' v' a' w} B)
    (M : GradedModule.{t, a, max u v a u' v' a' w} A) (n : ℤ) :
    GradedHomOfDegree ((pullbackFunctor.{t, a, w, v, u, a', v', u'} φ).obj N) M n ≃
      GradedHomOfDegree N (pushforwardObj φ M) n
Sources
LeanSheafOfModules.GradedModule.semilinearHomOfDegreeEquiv · SheafOfModules.GradedModule.pushforwardObj · SheafOfModules.GradedModule.pushforwardMap · SheafOfModules.GradedModule.pushforwardFunctor · SheafOfModules.GradedModule.pushforwardHomOfDegree · SheafOfModules.GradedModule.semilinearHomEquiv · SheafOfModules.GradedModule.pullbackHomOfDegreeEquiv

Section24.10 Localization and sheaves of graded modules#

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

Tag 0FRA, a lemma

Tag 0FRA in the Stacks Project.

SheafOfModules.gradedExtendHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedExtensionByZero.lean, line 426. The attribute's comment: “Hom(j_! M, N) = Hom(M, j^* N)”.

Tag 0FRA. The homomorphisms j_!M ⟶ N of right graded A-modules are the homomorphisms M ⟶ j^*N of right graded A_U-modules. The bijection is the degreewise adjunction j_{U!} ⊣ j_U^* of ordinary sheaves of modules; the content is that it matches the A-linear maps with the A_U-linear maps.

noncomputable def gradedExtendHomEquiv
    (M : GradedModule.{w, max u v m, max u v m} (A.over U))
    (N : GradedModule.{w, max u v m, max u v m} A) :
    (gradedExtensionByZero.{m} O U A M ⟶ N) ≃ (M ⟶ N.over U)

SheafOfModules.gradedExtensionByZeroAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedExtensionByZero.lean, line 452. The attribute's comment: “the identification is an adjunction j_! ⊣ j^* of graded modules”.

Tag 0FRA, as an adjunction. j_! : Mod^gr(A_U) ⥤ Mod^gr(A) is left adjoint to j^* : Mod^gr(A) ⥤ Mod^gr(A_U).

noncomputable def gradedExtensionByZeroAdjunction :
    gradedExtensionByZeroFunctor.{m} O U A ⊣ GradedModule.overFunctor A U

SheafOfModules.gradedHomOfDegreeExtendEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedExtensionByZero.lean, line 525. The attribute's comment: “Hom(j_! M, N) = Hom(M, j^* N), in each degree”.

Tag 0FRA. In every degree d the homogeneous homomorphisms j_!M ⟶ N of right graded A-modules are the homogeneous homomorphisms M ⟶ j^*N of right graded A_U-modules. The bijection is the degreewise adjunction j_{U!} ⊣ j_U^* of ordinary sheaves of modules; the content is that it matches the A-linear maps with the A_U-linear maps. In degree 0, read together with the naturality below, this is the adjunction j_! ⊣ j^* of the source.

noncomputable def gradedHomOfDegreeExtendEquiv (d : ℤ) :
    GradedHomOfDegree (gradedExtensionByZero.{m} O U A M) N d ≃
      GradedHomOfDegree M (N.over U) d

SheafOfModules.gradedHomOfDegreeExtendEquiv_naturality_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedExtensionByZero.lean, line 548. The attribute's comment: “naturality of Hom(j_! M, N) = Hom(M, j^* N) in M”.

Tag 0FRA, naturality in the source.

theorem gradedHomOfDegreeExtendEquiv_naturality_left
    {M' : GradedModule.{w, max u v m, max u v m} (A.over U)} (g : M' ⟶ M) (d : ℤ)
    (f : GradedHomOfDegree (gradedExtensionByZero.{m} O U A M) N d) :
    gradedHomOfDegreeExtendEquiv.{m} O U A d
        (GradedHomOfDegree.compLeft (gradedExtensionByZeroMap.{m} O U A g) f) =
      GradedHomOfDegree.compLeft g (gradedHomOfDegreeExtendEquiv.{m} O U A d f)

SheafOfModules.gradedHomOfDegreeExtendEquiv_naturality_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedExtensionByZero.lean, line 559. The attribute's comment: “naturality of Hom(j_! M, N) = Hom(M, j^* N) in N”.

Tag 0FRA, naturality in the target.

theorem gradedHomOfDegreeExtendEquiv_naturality_right
    {N' : GradedModule.{w, max u v m, max u v m} A} (k : N ⟶ N') (d : ℤ)
    (f : GradedHomOfDegree (gradedExtensionByZero.{m} O U A M) N d) :
    gradedHomOfDegreeExtendEquiv.{m} O U A d (f.compRight k) =
      (gradedHomOfDegreeExtendEquiv.{m} O U A d f).compRight
        (GradedModule.overMap k U)
Tag 0FRB, a lemma

Tag 0FRB in the Stacks Project.

SheafOfModules.extendTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedExtensionByZeroTensor.lean, line 299. The attribute's comment: “j_! M ⊗_A N = j_!(M ⊗_{A_U} N|_U) as graded O-modules”.

Tag 0FRB. In every degree n the relative tensor product of the extension by zero of a right graded A_U-module M with a left graded A-module N is the extension by zero of the relative tensor product of M with the restriction of N: j_!M ⊗_A N = j_!(M ⊗_{A_U} N|_U) as sheaves of O-modules. The isomorphism sends the local section j_!x ⊗ y to j_!(x ⊗ y), and it is natural in M and in N by SheafOfModules.extendTensorHom_naturality_left and ..._naturality_right.

noncomputable def extendTensorIso (n : ℤ) :
    extendTensor.{m} O U A M N n ≅
      (extendSheaf.{m} O U).obj (sliceTensor.{m} O U A M N n)

SheafOfModules.extendTensorHom_naturality_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedExtensionByZeroTensor.lean, line 311. The attribute's comment: “functoriality of j_! M ⊗_A N = j_!(M ⊗_{A_U} N|_U) in N”.

Tag 0FRB, functoriality in the left graded module. The identification j_!M ⊗_A N = j_!(M ⊗_{A_U} N|_U) commutes with a homomorphism N ⟶ N' of left graded A-modules.

theorem extendTensorHom_naturality_right {N' : LeftGradedModule.{w, max u v m, max u v m} A}
    (f : N ⟶ N') (n : ℤ) :
    RelativeTensor.gradedTensorMap (gradedExtensionByZero.{m} O U A M) f n ≫
        extendTensorHom.{m} O U A M N' n =
      extendTensorHom.{m} O U A M N n ≫ (extendSheaf.{m} O U).map
        (RelativeTensor.gradedTensorMap (J := J.over U) (Osharp := O.over U) M
          (LeftGradedModule.overMap f U) n)

SheafOfModules.extendTensorHom_naturality_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedExtensionByZeroTensor.lean, line 368. The attribute's comment: “functoriality of j_! M ⊗_A N = j_!(M ⊗_{A_U} N|_U) in M”.

Tag 0FRB, functoriality in the right graded module. The identification j_!M ⊗_A N = j_!(M ⊗_{A_U} N|_U) commutes with a homomorphism M ⟶ M' of right graded A_U-modules.

theorem extendTensorHom_naturality_left {M' : GradedModule.{w, max u v m, max u v m} (A.over U)}
    (h : M ⟶ M') (n : ℤ) :
    RelativeTensor.gradedTensorMapRight (gradedExtensionByZeroMap.{m} O U A h) N n ≫
        extendTensorHom.{m} O U A M' N n =
      extendTensorHom.{m} O U A M N n ≫ (extendSheaf.{m} O U).map
        (RelativeTensor.gradedTensorMapRight (J := J.over U) (Osharp := O.over U) h
          (N.over U) n)
Sources
LeanSheafOfModules.gradedExtendHomEquiv · SheafOfModules.gradedExtensionByZeroAdjunction · SheafOfModules.gradedHomOfDegreeExtendEquiv · SheafOfModules.gradedHomOfDegreeExtendEquiv_naturality_left · SheafOfModules.gradedHomOfDegreeExtendEquiv_naturality_right · SheafOfModules.extendTensorIso · SheafOfModules.extendTensorHom_naturality_right · SheafOfModules.extendTensorHom_naturality_left

Section24.11 Shift functors on sheaves of graded modules#

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

Tag 0FRD, a lemma

Tag 0FRD in the Stacks Project.

SheafOfModules.GradedModule.isGrothendieckAbelian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafModulesGrothendieck.lean, line 240.

The category of right graded modules over a sheaf of graded algebras on a site is a Grothendieck abelian category.

It is abelian and has filtered colimits by Tag 0FR0, those colimits are exact by gradedModule_ab5, it is locally small, and it has the separator ⨁_{k, U} j_{U!} A_U[k].

noncomputable instance isGrothendieckAbelian (A : GradedAlgebra.{t, a} R) :
    IsGrothendieckAbelian.{max u v a w} (GradedModule.{t, a, max u v a w} A)
Sources
LeanSheafOfModules.GradedModule.isGrothendieckAbelian

Section24.12 Sheaves of differential graded algebras#

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

Tag 0FRF, a definition

Tag 0FRF in the Stacks Project.

SheafOfModules.DifferentialGradedAlgebra.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraHom.lean, line 55. The attribute's comment: “homomorphisms of differential graded algebras”.

A homomorphism of sheaves of differential graded algebras: a morphism of the underlying cochain complexes which respects the graded multiplication.

structure Hom (A B : DifferentialGradedAlgebra.{t, a} R)

SheafOfModules.DifferentialGradedAlgebra.op, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedOppositeAlgebra.lean, line 260. The attribute's comment: “the opposite of a sheaf of differential graded algebras”.

The opposite sheaf of differential graded algebras. The underlying complex and the unit are those of A, and the multiplication interchanges its variables and twists by the Koszul sign.

noncomputable def op : DifferentialGradedAlgebra.{t, a} R

SheafOfModules.DifferentialGradedAlgebra, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedForgetColimits.lean, line 221. The attribute's comment: “sheaves of differential graded algebras”.

A sheaf of differential graded algebras over a sheaf of rings on a site.

structure DifferentialGradedAlgebra (R : Sheaf J RingCat.{t})
Tag 0FRG, a remark

Tag 0FRG in the Stacks Project.

SheafOfModules.DifferentialGradedAlgebra.pushforwardDifferentialGradedAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraFunctoriality.lean, line 525. The attribute's comment: “part (1): pushforward”.

An additive lax monoidal functor between categories of sheaves of modules induces a functor between the categories of sheaves of differential graded algebras. This is part (1) of the functoriality of sheaves of differential graded algebras: for a morphism of ringed topoi (f, f♯) and F = f_* — lax monoidal because it is right adjoint to the strong monoidal pullback, and additive because it is a right adjoint between abelian categories — it is the pushforward A ↦ (f_*A, f_*d).

noncomputable def pushforwardDifferentialGradedAlgebra :
    DifferentialGradedAlgebra.{w, w} (toRingCat J Osharp) ⥤
      DifferentialGradedAlgebra.{w, w} (toRingCat K Psharp)

SheafOfModules.DifferentialGradedAlgebra.pullbackDifferentialGradedAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraFunctoriality.lean, line 583. The attribute's comment: “part (2): pullback”.

An additive strong monoidal functor between categories of sheaves of modules induces a functor between the categories of sheaves of differential graded algebras. This is part (2) of the functoriality of sheaves of differential graded algebras: for a morphism of ringed topoi (f, f♯) and L = f^* — strong monoidal for the tensor product of Tag 01CA, and additive because it is a left adjoint between abelian categories — it is the pullback B ↦ (f^*B, f^*d).

noncomputable def pullbackDifferentialGradedAlgebra :
    DifferentialGradedAlgebra.{w, w} (toRingCat K Psharp) ⥤
      DifferentialGradedAlgebra.{w, w} (toRingCat J Osharp)

SheafOfModules.DifferentialGradedAlgebra.differentialGradedAlgebraAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraFunctoriality.lean, line 710. The attribute's comment: “part (3): adjunction”.

Pullback of sheaves of differential graded algebras is left adjoint to pushforward. This is part (3) of the functoriality of sheaves of differential graded algebras: for a morphism of ringed topoi (f, f♯), homomorphisms f^*B ⟶ A correspond to homomorphisms B ⟶ f_*A, naturally in both arguments. The two functors are the constructions of parts (1) and (2), not functors merely asserted to exist.

noncomputable def differentialGradedAlgebraAdjunction :
    pullbackDifferentialGradedAlgebra L hP hO ⊣ pushforwardDifferentialGradedAlgebra G hO hP

AlgebraicGeometry.RingedSite.Hom.dgaPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraRingedSite.lean, line 256. The attribute's comment: “part (1) at a morphism of ringed sites: (f_*A, f_*d), functorially”.

The direct image of a sheaf of differential graded algebras along a morphism of ringed sites. Its underlying sheaf of graded algebras is the direct image of that of A and its differential is f_*d; this is part (1) of the functoriality of sheaves of differential graded algebras.

noncomputable def dgaPushforward :
    SheafOfModules.DifferentialGradedAlgebra.{u, u} (Sheaf.toRingCat X.J X.O) ⥤
      SheafOfModules.DifferentialGradedAlgebra.{u, u} (Sheaf.toRingCat Y.J Y.O)

AlgebraicGeometry.RingedSite.Hom.dgaPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraRingedSite.lean, line 266. The attribute's comment: “part (2) at a morphism of ringed sites: (f^*B, f^*d), functorially”.

The inverse image of a sheaf of differential graded algebras along a morphism of ringed sites. Its underlying sheaf of graded algebras is the inverse image of that of B and its differential is f^*d; this is part (2) of the functoriality of sheaves of differential graded algebras.

noncomputable def dgaPullback :
    SheafOfModules.DifferentialGradedAlgebra.{u, u} (Sheaf.toRingCat Y.J Y.O) ⥤
      SheafOfModules.DifferentialGradedAlgebra.{u, u} (Sheaf.toRingCat X.J X.O)

AlgebraicGeometry.RingedSite.Hom.dgaPushforward_obj_complex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraRingedSite.lean, line 295. The attribute's comment: “part (1) at a morphism of ringed sites: (f_*A, f_*d), functorially”.

The differential of f_*A is f_*d: its cochain complex is the direct image of the cochain complex of A degreewise.

theorem dgaPushforward_obj_complex
    (A : SheafOfModules.DifferentialGradedAlgebra.{u, u} (Sheaf.toRingCat X.J X.O)) :
    ((dgaPushforward f hY hX).obj A).complex =
      ((SheafOfModules.pushforward.{u} (Stacks.DifferentialGradedInverseImage.inverseImageRingHom
            (structureMapPresheaf f) hY hX)).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        A.complex

AlgebraicGeometry.RingedSite.Hom.dgaPullback_obj_complex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraRingedSite.lean, line 306. The attribute's comment: “part (2) at a morphism of ringed sites: (f^*B, f^*d), functorially”.

The differential of f^*B is f^*d: its cochain complex is the inverse image of the cochain complex of B degreewise.

theorem dgaPullback_obj_complex
    (B : SheafOfModules.DifferentialGradedAlgebra.{u, u} (Sheaf.toRingCat Y.J Y.O)) :
    ((dgaPullback f hY hX).obj B).complex =
      ((Stacks.DifferentialGradedInverseImage.inverseImageModules
          (structureMapPresheaf f) hY hX).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        B.complex

AlgebraicGeometry.RingedSite.Hom.dgaPushforward_obj_toGradedAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraRingedSite.lean, line 318. The attribute's comment: “part (1) at a morphism of ringed sites: (f_*A, f_*d), functorially”.

The underlying sheaf of graded algebras of f_*A is the direct image of that of A, in the sense of the functoriality of sheaves of graded algebras: so f_*A really is the sheaf of graded algebras of that remark, equipped with the differential f_*d.

theorem dgaPushforward_obj_toGradedAlgebra
    (A : SheafOfModules.DifferentialGradedAlgebra.{u, u} (Sheaf.toRingCat X.J X.O)) :
    ((dgaPushforward f hY hX).obj A).toGradedAlgebra =
      SheafOfModules.GradedAlgebra.transport
        (SheafOfModules.pushforward.{u} (Stacks.DifferentialGradedInverseImage.inverseImageRingHom
          (structureMapPresheaf f) hY hX)) A.toGradedAlgebra hX hY

AlgebraicGeometry.RingedSite.Hom.dgaPullback_obj_toGradedAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraRingedSite.lean, line 330. The attribute's comment: “part (2) at a morphism of ringed sites: (f^*B, f^*d), functorially”.

The underlying sheaf of graded algebras of f^*B is the inverse image of that of B, in the sense of the functoriality of sheaves of graded algebras: so f^*B really is the sheaf of graded algebras of that remark, equipped with the differential f^*d.

theorem dgaPullback_obj_toGradedAlgebra
    (B : SheafOfModules.DifferentialGradedAlgebra.{u, u} (Sheaf.toRingCat Y.J Y.O)) :
    ((dgaPullback f hY hX).obj B).toGradedAlgebra =
      SheafOfModules.GradedAlgebra.transport
        (Stacks.DifferentialGradedInverseImage.inverseImageModules
          (structureMapPresheaf f) hY hX) B.toGradedAlgebra hY hX

AlgebraicGeometry.RingedSite.Hom.dgaAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAlgebraRingedSite.lean, line 342. The attribute's comment: “part (3) at a morphism of ringed sites: (f^*B ⟶ A) ≃ (B ⟶ f_*A)”.

The inverse image of sheaves of differential graded algebras along a morphism of ringed sites is left adjoint to the direct image. This is part (3) of the functoriality of sheaves of differential graded algebras, its two functors being those of parts (2) and (1).

noncomputable def dgaAdjunction : dgaPullback f hY hX ⊣ dgaPushforward f hY hX
Sources
LeanSheafOfModules.DifferentialGradedAlgebra.Hom · SheafOfModules.DifferentialGradedAlgebra.op · SheafOfModules.DifferentialGradedAlgebra · SheafOfModules.DifferentialGradedAlgebra.pushforwardDifferentialGradedAlgebra · SheafOfModules.DifferentialGradedAlgebra.pullbackDifferentialGradedAlgebra · SheafOfModules.DifferentialGradedAlgebra.differentialGradedAlgebraAdjunction · AlgebraicGeometry.RingedSite.Hom.dgaPushforward · AlgebraicGeometry.RingedSite.Hom.dgaPullback

Section24.13 Sheaves of differential graded modules#

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

Tag 0FRI, a definition

Tag 0FRI in the Stacks Project.

SheafOfModules.LeftDifferentialGradedModule.opRight, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedOppositeModule.lean, line 210. The attribute's comment: “left differential graded modules as right modules over the opposite algebra”.

A left differential graded A-module read as a right differential graded A.op-module. The cochain complex is unchanged and the action is interchanged and twisted by the Koszul sign.

noncomputable def opRight : DifferentialGradedModule.{t, a, w} A.op

SheafOfModules.DifferentialGradedModule.opLeft, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedOppositeModule.lean, line 313. The attribute's comment: “right differential graded modules as left modules over the opposite algebra”.

A right differential graded A-module read as a left differential graded A.op-module. The cochain complex is unchanged and the action is interchanged and twisted by the Koszul sign.

noncomputable def opLeft : LeftDifferentialGradedModule.{t, a, w} A.op

SheafOfModules.DifferentialGradedModule.unopLeft, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedOppositeModule.lean, line 417. The attribute's comment: “right differential graded modules over the opposite algebra as left modules”.

A right differential graded A.op-module read as a left differential graded A-module. The cochain complex is unchanged and the action is interchanged and twisted by the Koszul sign.

noncomputable def unopLeft : LeftDifferentialGradedModule.{t, a, w} A

SheafOfModules.DifferentialGradedModule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedForgetColimits.lean, line 302. The attribute's comment: “right differential graded modules”.

A right differential graded module over a sheaf of differential graded algebras.

structure DifferentialGradedModule (A : DifferentialGradedAlgebra.{t, a} R)

SheafOfModules.DifferentialGradedModule.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedForgetColimits.lean, line 331. The attribute's comment: “homomorphisms of differential graded modules”.

A morphism of right differential graded modules.

structure Hom (M N : DifferentialGradedModule.{t, a, m} A)

SheafOfModules.LeftDifferentialGradedModule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftDifferentialGradedModule.lean, line 64. The attribute's comment: “left differential graded modules”.

A left differential graded module over a sheaf of differential graded algebras. The sign in the Leibniz rule is determined by the degree of the algebra section.

structure LeftDifferentialGradedModule (A : DifferentialGradedAlgebra.{t, a} R)

SheafOfModules.LeftDifferentialGradedModule.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftDifferentialGradedModule.lean, line 93. The attribute's comment: “homomorphisms of left differential graded modules”.

A morphism of left differential graded modules.

structure Hom (M N : LeftDifferentialGradedModule.{t, a, m} A)
Tag 0FRJ, a lemma

Tag 0FRJ in the Stacks Project.

SheafOfModules.differentialGradedModule_abelian_ab5_hasLimits_hasColimits_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedModuleCategoryProperties.lean, line 107.

Stacks 0FRJ. Let R be a sheaf of rings on a site (C, J) and let A be a sheaf of differential graded R-algebras. The category Mod(A, d) of right differential graded A-modules is abelian and has

  1. arbitrary direct sums,
  2. arbitrary colimits,
  3. exact filtered colimits,
  4. arbitrary products,
  5. arbitrary limits,

and the functor Mod(A, d) ⥤ Mod(A) forgetting the differential commutes with all limits and with all colimits.

Abelianness is phrased as Nonempty (Abelian _) because CategoryTheory.Abelian is data; the seven remaining clauses are propositions on the nose.

theorem differentialGradedModule_abelian_ab5_hasLimits_hasColimits_forget
    (A : DifferentialGradedAlgebra.{t, a} R)
    [HasSheafify J AddCommGrpCat.{m}] [J.WEqualsLocallyBijective AddCommGrpCat.{m}] :
    Nonempty (Abelian (DifferentialGradedModule.{t, a, m} A)) ∧
      HasCoproducts.{m} (DifferentialGradedModule.{t, a, m} A) ∧
      HasColimitsOfSize.{m, m} (DifferentialGradedModule.{t, a, m} A) ∧
      AB5OfSize.{m, m} (DifferentialGradedModule.{t, a, m} A) ∧
      HasProducts.{m} (DifferentialGradedModule.{t, a, m} A) ∧
      HasLimitsOfSize.{m, m} (DifferentialGradedModule.{t, a, m} A) ∧
      PreservesLimitsOfSize.{s₁, s₂} (forgetToGradedModule.{t, a, m} A) ∧
      PreservesColimitsOfSize.{s₁, s₂} (forgetToGradedModule.{t, a, m} A)
Tag 0FRK, an equation

Tag 0FRK in the Stacks Project.

SheafOfModules.DifferentialGradedModule.toCochainComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedCohomologySequence.lean, line 138. The attribute's comment: “underlying short exact sequence”.

A short exact sequence of differential graded modules has an underlying short exact sequence of cochain complexes of sheaves of modules.

theorem toCochainComplex_shortExact
    (S : ShortComplex (DifferentialGradedModule.{t, a, m} A)) (hS : S.ShortExact) :
    (S.map (toCochainComplex.{t, a, m} A)).ShortExact

SheafOfModules.DifferentialGradedModule.cohomologyExactAtFirst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedCohomologySequence.lean, line 155. The attribute's comment: “exactness at the first cohomology sheaf”.

Exactness of the cohomology sequence at the cohomology of the first module, including the connecting map from the preceding degree.

theorem cohomologyExactAtFirst
    (S : ShortComplex (DifferentialGradedModule.{t, a, m} A)) (hS : S.ShortExact) (n : ℤ) :
    (ShortComplex.mk
      ((toCochainComplex_shortExact A S hS).δ (n - 1) n (by simp))
      (HomologicalComplex.homologyMap S.f.toHomologicalComplex n)
      ((toCochainComplex_shortExact A S hS).δ_comp (n - 1) n (by simp))).Exact

SheafOfModules.DifferentialGradedModule.cohomologyExactAtMiddle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedCohomologySequence.lean, line 165. The attribute's comment: “exactness at the middle cohomology sheaf”.

Exactness of the cohomology sequence at the cohomology of the middle module.

theorem cohomologyExactAtMiddle
    (S : ShortComplex (DifferentialGradedModule.{t, a, m} A)) (hS : S.ShortExact) (n : ℤ) :
    ((S.map (toCochainComplex.{t, a, m} A)).map
      (HomologicalComplex.homologyFunctor (SheafOfModules.{m} R) (ComplexShape.up ℤ) n)).Exact

SheafOfModules.DifferentialGradedModule.cohomologyExactAtThird, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedCohomologySequence.lean, line 174. The attribute's comment: “exactness at the third cohomology sheaf”.

Exactness of the cohomology sequence at the cohomology of the third module, before the canonical connecting map to the next degree.

theorem cohomologyExactAtThird
    (S : ShortComplex (DifferentialGradedModule.{t, a, m} A)) (hS : S.ShortExact) (n : ℤ) :
    (ShortComplex.mk
      (HomologicalComplex.homologyMap S.g.toHomologicalComplex n)
      ((toCochainComplex_shortExact A S hS).δ n (n + 1) (by simp))
      ((toCochainComplex_shortExact A S hS).comp_δ n (n + 1) (by simp))).Exact
Sources
LeanSheafOfModules.LeftDifferentialGradedModule.opRight · SheafOfModules.DifferentialGradedModule.opLeft · SheafOfModules.DifferentialGradedModule.unopLeft · SheafOfModules.DifferentialGradedModule · SheafOfModules.DifferentialGradedModule.Hom · SheafOfModules.LeftDifferentialGradedModule · SheafOfModules.LeftDifferentialGradedModule.Hom · SheafOfModules.differentialGradedModule_abelian_ab5_hasLimits_hasColimits_forget

Section24.15 Tensor product for sheaves of differential graded modules#

Section 24.15 of the Stacks Project, Tag 0FRM. 1 tag here is carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FRM, the section

Tag 0FRM in the Stacks Project.

SheafOfModules.RelativeTensor.dgTensorOpIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedOppositeTensor.lean, line 324. The attribute's comment: “the relative tensor product of the opposite algebra, interchanged”.

The relative tensor product read over the opposite algebra. Interchanging the two factors and twisting by the Koszul sign identifies P ⊗_{A.op} M.opLeft with M ⊗_A P.unopLeft.

noncomputable def dgTensorOpIso : dgTensor P M.opLeft ≅ dgTensor M P.unopLeft

SheafOfModules.RelativeTensor.dgTensorSumDiff_balance, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRelativeTensor.lean, line 301. The attribute's comment: “the differential is well defined: it kills xa ⊗ y - x ⊗ ay”.

The signed differential of the direct sums is compatible with the balance maps: this is the two Leibniz rules, and it is what makes the differential descend to P ⊗_A N.

theorem dgTensorSumDiff_balance (n : ℤ) :
    balanceMap (gP P) (gN N) n ≫ dgTensorSumDiff P N n =
      relationSumDiff P N n ≫ balanceMap (gP P) (gN N) (n + 1)

SheafOfModules.RelativeTensor.dgTensorDiffPre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRelativeTensor.lean, line 382. The attribute's comment: “the differential d (x ⊗ y) = dx ⊗ y + (-1)^{deg x} x ⊗ dy”.

The differential of degree n of the relative tensor product P ⊗_A N, as a morphism of presheaves of modules: the descent of the signed differential to the cokernel of the balance map.

noncomputable def dgTensorDiffPre (n : ℤ) :
    gradedTensorPre (gP P) (gN N) n ⟶ gradedTensorPre (gP P) (gN N) (n + 1)

SheafOfModules.RelativeTensor.dgTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRelativeTensor.lean, line 419. The attribute's comment: “the relative tensor product as a complex of O-modules”.

The relative tensor product P ⊗_A N of a right differential graded A-module with a left differential graded A-module, as a cochain complex of sheaves of modules.

noncomputable def dgTensor : CochainComplex (SheafOfModules.{m} (toRingCat J Osharp)) ℤ

SheafOfModules.RelativeTensor.dgTensorFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRelativeTensor.lean, line 585. The attribute's comment: “the functor - ⊗_A N to complexes of O-modules”.

The functor - ⊗_A N from right differential graded A-modules to complexes of O-modules, for a fixed left differential graded A-module N.

noncomputable def dgTensorFunctor :
    DifferentialGradedModule.{t, m, m} A ⥤
      CochainComplex (SheafOfModules.{m} (toRingCat J Osharp)) ℤ

SheafOfModules.RelativeTensor.dgUnitorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRelativeTensorUnitor.lean, line 135. The attribute's comment: “the unit isomorphism A ⊗_A N ≅ N of complexes, for A the regular right module”.

The unit isomorphism of the relative tensor product of differential graded modules: A ⊗_A N ≅ N as cochain complexes of sheaves of modules, for A a sheaf of differential graded algebras acting on itself on the right and N a left differential graded A-module.

noncomputable def dgUnitorIso :
    dgTensor (DifferentialGradedModule.regularModule A) N ≅ N.complex

SheafOfModules.LocalBalancedBilinear, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensor.lean, line 270. The attribute's comment: “local balanced bilinear families, the universal property of the tensor product”.

An A-balanced bilinear family of degree n over U, from a right differential graded A-module M and a differential graded (A, B)-bimodule N to a right differential graded B-module L: maps M^i|_U × N^j|_U → L^{i + j + n}|_U which are bilinear over the sheaf of rings, compatible with restriction, A-balanced and B-linear in the second variable.

structure LocalBalancedBilinear (M : DifferentialGradedModule.{t, a, w} A)
    (N : DifferentialGradedBimodule.{t, a, z} A B)
    (L : DifferentialGradedModule.{t, a, s} B) (n : ℤ) (U : C)
Sources
LeanSheafOfModules.RelativeTensor.dgTensorOpIso · SheafOfModules.RelativeTensor.dgTensorSumDiff_balance · SheafOfModules.RelativeTensor.dgTensorDiffPre · SheafOfModules.RelativeTensor.dgTensor · SheafOfModules.RelativeTensor.dgTensorFunctor · SheafOfModules.RelativeTensor.dgUnitorIso · SheafOfModules.LocalBalancedBilinear

Section24.16 Internal hom for sheaves of differential graded modules#

Section 24.16 of the Stacks Project, Tag 0FRN. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FRN, the section

Tag 0FRN in the Stacks Project.

SheafOfModules.LocalHom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedInternalHom.lean, line 161. The attribute's comment: “local sections of the graded internal hom”.

A local section of SheafHom^n_A(M, L) over U: a map M|_U → L|_U of right differential graded A|_U-modules homogeneous of degree n.

structure LocalHom (M : DifferentialGradedModule.{t, a, w} A)
    (L : DifferentialGradedModule.{t, a, z} A) (n : ℤ) (U : C)
    extends LocalGradedHom M L n U

SheafOfModules.LocalHom.comp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedInternalHom.lean, line 226. The attribute's comment: “the composition map of the internal hom”.

The composition of local homomorphisms of right differential graded A|_U-modules.

def LocalHom.comp {K : DifferentialGradedModule.{t, a, s} A}
    {M : DifferentialGradedModule.{t, a, w} A} {L : DifferentialGradedModule.{t, a, z} A}
    {n m nm : ℤ} {U : C} (g : LocalHom K M n U) (f : LocalHom M L m U) (h : n + m = nm) :
    LocalHom K L nm U
Sources
LeanSheafOfModules.LocalHom · SheafOfModules.LocalHom.comp

Section24.17 Sheaves of differential graded bimodules and tensor-hom adjunction#

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

Tag 0FRP, the section

Tag 0FRP in the Stacks Project.

SheafOfModules.DifferentialGradedBimodule.equivLeftStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedBimoduleStructures.lean, line 182. The attribute's comment: “a dg (A,B)-bimodule is a right dg B-module with a commuting left dg A-structure”.

A differential graded (A, B)-bimodule is exactly a right differential graded B-module which is also a left differential graded A-module on the same complex, the two actions commuting.

def equivLeftStructure (A B : DifferentialGradedAlgebra.{t, a} R) :
    DifferentialGradedBimodule.{t, a, m} A B ≃
      Σ M : DifferentialGradedModule.{t, a, m} B, LeftStructure A M

SheafOfModules.DifferentialGradedAlgebra.asBimodule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedBimoduleStructures.lean, line 240. The attribute's comment: “B as a differential graded (A,B)-bimodule through a homomorphism φ : A ⟶ B”.

{}_A B_B: a sheaf of differential graded algebras B is a differential graded (A, B)-bimodule through a unital homomorphism φ : A ⟶ B, with a acting on the left as φ a and B acting on the right by its own multiplication.

def asBimodule (φ : A ⟶ B) (hφ : φ.IsUnital) : DifferentialGradedBimodule.{t, a, a} A B

SheafOfModules.DifferentialGradedModule.restrictScalars, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedBimoduleStructures.lean, line 354. The attribute's comment: “restriction res_φ along a homomorphism of sheaves of differential graded algebras”.

The restriction functor res_φ : Mod^dg(B, d) ⥤ Mod^dg(A, d) attached to a unital homomorphism φ : A ⟶ B of sheaves of differential graded algebras.

def restrictScalars (φ : A ⟶ B) (hφ : φ.IsUnital) :
    DifferentialGradedModule.{t, a, m} B ⥤ DifferentialGradedModule.{t, a, m} A

SheafOfModules.DifferentialGradedAlgebra.Hom.toBimodule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRestriction.lean, line 205. The attribute's comment: “the bimodule _A B_B attached to a homomorphism of differential graded algebras”.

The target of a unit-preserving homomorphism φ : A ⟶ B of sheaves of differential graded algebras, read as a differential graded (A, B)-bimodule {}_A B_B: the underlying complex is that of B, the right action is the multiplication of B, and a homogeneous local section a of A acts on the left through φ(a).

This is SheafOfModules.DifferentialGradedAlgebra.asBimodule.

def Hom.toBimodule (φ : A ⟶ B) (hφ : φ.PreservesOne) :
    DifferentialGradedBimodule.{t, a, a} A B

SheafOfModules.DifferentialGradedModule.restrictionObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRestriction.lean, line 245. The attribute's comment: “the restriction functor res_φ on objects”. References: EGA II (2.8.6), “more general”.

Restriction of scalars of a right differential graded B-module along a unit-preserving homomorphism φ : A ⟶ B of sheaves of differential graded algebras: the underlying cochain complex of sheaves of modules is unchanged and a homogeneous local section a of A acts through φ(a).

This is SheafOfModules.DifferentialGradedModule.restrictScalarsObj.

def restrictionObj (φ : A ⟶ B) (hφ : φ.PreservesOne)
    (N : DifferentialGradedModule.{t, a, m} B) : DifferentialGradedModule.{t, a, m} A

SheafOfModules.DifferentialGradedModule.restrictionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRestriction.lean, line 268. The attribute's comment: “the restriction functor res_φ on homomorphisms”.

Restriction of scalars of a homomorphism of right differential graded B-modules: the same morphism of underlying cochain complexes.

def restrictionMap (φ : A ⟶ B) (hφ : φ.PreservesOne)
    {M N : DifferentialGradedModule.{t, a, m} B} (g : M ⟶ N) :
    restrictionObj φ hφ M ⟶ restrictionObj φ hφ N

SheafOfModules.DifferentialGradedModule.restriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRestriction.lean, line 285. The attribute's comment: “the restriction functor res_φ”.

Restriction of scalars res_φ : Mod(B, d) ⥤ Mod(A, d) along a unit-preserving homomorphism φ : A ⟶ B of sheaves of differential graded algebras.

This is SheafOfModules.DifferentialGradedModule.restrictScalars.

def restriction (φ : A ⟶ B) (hφ : φ.PreservesOne) :
    DifferentialGradedModule.{t, a, m} B ⥤ DifferentialGradedModule.{t, a, m} A

SheafOfModules.DifferentialGradedModule.extensionRestrictionAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedRestrictionAdjunction.lean, line 836. The attribute's comment: “base change is left adjoint to res_phi, given a TensorFunctorData of 0FTE”.

Extension of scalars is left adjoint to restriction of scalars. For a unit-preserving homomorphism φ : A ⟶ B of sheaves of differential graded R-algebras and a tensor product functor - ⊗_{A, φ} B with the bimodule {}_A B_B, that functor is left adjoint to res_φ. This is the adjunction of Stacks, Tag 0FRP.

def extensionRestrictionAdjunction : D.functor ⊣ restriction.{t, a, m} φ hφ
Tag 0FRQ, a definition

Tag 0FRQ in the Stacks Project.

SheafOfModules.DifferentialGradedBimodule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedBimodule.lean, line 65. The attribute's comment: “differential graded bimodules”.

A differential graded bimodule between two sheaves of differential graded algebras: a cochain complex of sheaves of modules with commuting unital left and right actions, each obeying the signed Leibniz rule.

structure DifferentialGradedBimodule (A B : DifferentialGradedAlgebra.{t, a} R)

SheafOfModules.DifferentialGradedBimodule.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedBimodule.lean, line 119. The attribute's comment: “homomorphisms of differential graded bimodules”.

A homomorphism of differential graded bimodules: a morphism of the underlying complexes compatible with both actions.

structure Hom (M N : DifferentialGradedBimodule.{t, a, m} A B)
Tag 0FRR, a lemma

Tag 0FRR in the Stacks Project.

SheafOfModules.isEndomorphismAlgebra_endomorphismAlgebraOfIsInternalHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedEndomorphismAlgebra.lean, line 485. The attribute's comment: “the differential graded endomorphism algebra”.

The sheafified differential graded endomorphisms of a right differential graded B-module N carry a differential graded R-algebra structure, with composition of local endomorphisms as multiplication and the identity as unit.

noncomputable def isEndomorphismAlgebra_endomorphismAlgebraOfIsInternalHom
    (hH : IsInternalHom N N H) :
    IsEndomorphismAlgebra N (endomorphismAlgebraOfIsInternalHom hH)

SheafOfModules.bimoduleStructureEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedEndomorphismAlgebra.lean, line 1004. The attribute's comment: “bimodule structures correspond to maps into the endomorphism algebra”.

Compatible (A, B)-bimodule structures on a right differential graded B-module N are in one-to-one correspondence with identity-preserving homomorphisms of sheaves of differential graded R-algebras A ⟶ SheafHom^dg_B(N, N).

noncomputable def bimoduleStructureEquiv (hE : IsEndomorphismAlgebra N E) :
    BimoduleStructure A N ≃ UnitalHom A E

SheafOfModules.bimoduleStructureEquiv_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedEndomorphismAlgebra.lean, line 1016. The attribute's comment: “bimodule structures correspond to maps into the endomorphism algebra”.

The correspondence between compatible bimodule structures and identity-preserving homomorphisms into the endomorphism algebra is pinned down by the requirement that the homomorphism attached to a structure act on local sections of N by left multiplication for that structure.

theorem bimoduleStructureEquiv_app (hE : IsEndomorphismAlgebra N E) (s : BimoduleStructure A N)
    (n i j : ℤ) (hij : i + n = j) (U : C) (V : Over U)
    (a : (A.complex.X n).val.obj (Opposite.op U))
    (x : (N.complex.X i).val.obj (Opposite.op V.left)) :
    HEq ((hE.isInternalHom.sectionsEquiv n U
        (((bimoduleStructureEquiv hE s).toHom.toHomologicalComplex.f n).val.app
          (Opposite.op U) a)).app i j hij V x)
      ((s.leftMul n i).app (Opposite.op V.left) ((A.complex.X n).val.map V.hom.op a) x)
Tag 0FRS, a lemma

Tag 0FRS in the Stacks Project.

SheafOfModules.isInternalHom_tensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomAdjunction.lean, line 787. The attribute's comment: “SheafHom^dg_B(M ⊗_A N, L) = SheafHom^dg_A(M, SheafHom^dg_B(N, L))”.

Tensor-hom adjunction for sheaves of differential graded modules, second identity: a complex of sheaves of R-modules which is the internal hom SheafHom^dg_B(M ⊗_A N, L) is also the internal hom SheafHom^dg_A(M, SheafHom^dg_B(N, L)), differentials included.

noncomputable def isInternalHom_tensor (hT : IsTensorProduct M N T)
    (hH : IsSheafHom N L H) (hG : IsInternalHom T L G) :
    IsInternalHom M H G

SheafOfModules.tensorSectionsEquiv_naturality_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomAdjunction.lean, line 841. The attribute's comment: “functoriality of the internal-hom identity in M, on local sections”.

Tensor-hom adjunction for sheaves of differential graded modules, second identity, functoriality in M: a morphism u : M' ⟶ M of right differential graded A-modules induces t : M' ⊗_A N ⟶ M ⊗_A N and hence α : SheafHom^dg_B(M ⊗_A N, L) ⟶ SheafHom^dg_B(M' ⊗_A N, L), and α is also the map that the second identity attaches to u, namely precomposition with u on SheafHom^dg_A(M, SheafHom^dg_B(N, L)).

theorem tensorSectionsEquiv_naturality_left (hT : IsTensorProduct M N T)
    (hT' : IsTensorProduct M' N T') (hH : IsSheafHom N L H) (hG : IsInternalHom T L G)
    (hG' : IsInternalHom T' L G') (u : M' ⟶ M) (t : T' ⟶ T) (α : G ⟶ G')
    (ht : ∀ (i j : ℤ) (U : Cᵒᵖ) (x : (M'.complex.X i).val.obj U)
      (y : (N.complex.X j).val.obj U),
      (t.toHomologicalComplex.f (i + j)).val.app U (hT'.tmul i j U x y) =
        hT.tmul i j U ((u.toHomologicalComplex.f i).val.app U x) y)
    (hα : ∀ (n : ℤ) (U : C) (p : (G.X n).val.obj (Opposite.op U)) (i j : ℤ) (hij : i + n = j)
      (V : Over U) (x : (T'.complex.X i).val.obj (Opposite.op V.left)),
      (hG'.sectionsEquiv n U ((α.f n).val.app (Opposite.op U) p)).app i j hij V x =
        (hG.sectionsEquiv n U p).app i j hij V
          ((t.toHomologicalComplex.f i).val.app (Opposite.op V.left) x))
    (n : ℤ) (U : C) (p : (G.X n).val.obj (Opposite.op U)) (i j : ℤ) (hij : i + n = j)
    (V : Over U) (x : (M'.complex.X i).val.obj (Opposite.op V.left)) :
    (tensorSectionsEquiv hT' hH hG' n U ((α.f n).val.app (Opposite.op U) p)).app i j hij V x =
      (tensorSectionsEquiv hT hH hG n U p).app i j hij V
        ((u.toHomologicalComplex.f i).val.app (Opposite.op V.left) x)

SheafOfModules.tensorSectionsEquiv_naturality_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomAdjunction.lean, line 877. The attribute's comment: “functoriality of the internal-hom identity in L, on local sections”.

Tensor-hom adjunction for sheaves of differential graded modules, second identity, functoriality in L: a morphism k : L ⟶ L' of right differential graded B-modules induces α : SheafHom^dg_B(M ⊗_A N, L) ⟶ SheafHom^dg_B(M ⊗_A N, L') and g : SheafHom^dg_B(N, L) ⟶ SheafHom^dg_B(N, L'), and under the second identity α is postcomposition with g.

theorem tensorSectionsEquiv_naturality_right (hT : IsTensorProduct M N T)
    (hH : IsSheafHom N L H) (hH' : IsSheafHom N L' H') (hG : IsInternalHom T L G)
    (hG' : IsInternalHom T L' G') (k : L ⟶ L') (g : H ⟶ H') (α : G ⟶ G')
    (hg : ∀ (m : ℤ) (U : C) (q : (H.complex.X m).val.obj (Opposite.op U)) (i j : ℤ)
      (hij : i + m = j) (V : Over U)
      (y : (N.complex.X i).val.obj (Opposite.op V.left)),
      (hH'.isInternalHom.sectionsEquiv m U
          ((g.toHomologicalComplex.f m).val.app (Opposite.op U) q)).app i j hij V y =
        (k.toHomologicalComplex.f j).val.app (Opposite.op V.left)
          ((hH.isInternalHom.sectionsEquiv m U q).app i j hij V y))
    (hα : ∀ (n : ℤ) (U : C) (p : (G.X n).val.obj (Opposite.op U)) (i j : ℤ) (hij : i + n = j)
      (V : Over U) (x : (T.complex.X i).val.obj (Opposite.op V.left)),
      (hG'.sectionsEquiv n U ((α.f n).val.app (Opposite.op U) p)).app i j hij V x =
        (k.toHomologicalComplex.f j).val.app (Opposite.op V.left)
          ((hG.sectionsEquiv n U p).app i j hij V x))
    (n : ℤ) (U : C) (p : (G.X n).val.obj (Opposite.op U)) (i j : ℤ) (hij : i + n = j)
    (V : Over U) (x : (M.complex.X i).val.obj (Opposite.op V.left)) :
    (tensorSectionsEquiv hT hH' hG' n U ((α.f n).val.app (Opposite.op U) p)).app i j hij V x =
      (g.toHomologicalComplex.f j).val.app (Opposite.op V.left)
        ((tensorSectionsEquiv hT hH hG n U p).app i j hij V x)

SheafOfModules.tensorSectionsEquiv_naturality_bimodule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomAdjunction.lean, line 910. The attribute's comment: “functoriality of the internal-hom identity in N, on local sections”.

Tensor-hom adjunction for sheaves of differential graded modules, second identity, functoriality in N: a morphism σ : N ⟶ N' of differential graded (A, B)-bimodules induces t : M ⊗_A N ⟶ M ⊗_A N', hence α : SheafHom^dg_B(M ⊗_A N', L) ⟶ SheafHom^dg_B(M ⊗_A N, L), and g : SheafHom^dg_B(N', L) ⟶ SheafHom^dg_B(N, L); under the second identity α is postcomposition with g.

theorem tensorSectionsEquiv_naturality_bimodule (hT : IsTensorProduct M N T)
    (hT' : IsTensorProduct M N' T') (hH : IsSheafHom N L H) (hH' : IsSheafHom N' L H')
    (hG : IsInternalHom T L G) (hG' : IsInternalHom T' L G')
    (σ : N ⟶ N') (t : T ⟶ T') (g : H' ⟶ H) (α : G' ⟶ G)
    (ht : ∀ (i j : ℤ) (U : Cᵒᵖ) (x : (M.complex.X i).val.obj U)
      (y : (N.complex.X j).val.obj U),
      (t.toHomologicalComplex.f (i + j)).val.app U (hT.tmul i j U x y) =
        hT'.tmul i j U x ((σ.toHomologicalComplex.f j).val.app U y))
    (hg : ∀ (m : ℤ) (U : C) (q : (H'.complex.X m).val.obj (Opposite.op U)) (i j : ℤ)
      (hij : i + m = j) (V : Over U)
      (y : (N.complex.X i).val.obj (Opposite.op V.left)),
      (hH.isInternalHom.sectionsEquiv m U
          ((g.toHomologicalComplex.f m).val.app (Opposite.op U) q)).app i j hij V y =
        (hH'.isInternalHom.sectionsEquiv m U q).app i j hij V
          ((σ.toHomologicalComplex.f i).val.app (Opposite.op V.left) y))
    (hα : ∀ (n : ℤ) (U : C) (p : (G'.X n).val.obj (Opposite.op U)) (i j : ℤ) (hij : i + n = j)
      (V : Over U) (x : (T.complex.X i).val.obj (Opposite.op V.left)),
      (hG.sectionsEquiv n U ((α.f n).val.app (Opposite.op U) p)).app i j hij V x =
        (hG'.sectionsEquiv n U p).app i j hij V
          ((t.toHomologicalComplex.f i).val.app (Opposite.op V.left) x))
    (n : ℤ) (U : C) (p : (G'.X n).val.obj (Opposite.op U)) (i j : ℤ) (hij : i + n = j)
    (V : Over U) (x : (M.complex.X i).val.obj (Opposite.op V.left)) :
    (tensorSectionsEquiv hT hH hG n U ((α.f n).val.app (Opposite.op U) p)).app i j hij V x =
      (g.toHomologicalComplex.f j).val.app (Opposite.op V.left)
        ((tensorSectionsEquiv hT' hH' hG' n U p).app i j hij V x)

SheafOfModules.DifferentialGradedModule.tensorHomHomogeneousEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomHomComplex.lean, line 328. The attribute's comment: “Hom_{Mod^dg(B, d)}(M ⊗_A N, L) = Hom_{Mod^dg(A, d)}(M, SheafHom^dg_B(N, L)) as hom-complexes: degreewise, additively, and compatibly with the differentials”.

Tensor-hom adjunction for sheaves of differential graded modules, first identity, in a fixed degree: the degree-n homogeneous right-linear maps M ⊗_A N → L of right differential graded B-modules are the degree-n homogeneous right-linear maps M → SheafHom^dg_B(N, L) of right differential graded A-modules.

noncomputable def tensorHomHomogeneousEquiv (hT : IsTensorProduct M N T) (hH : IsSheafHom N L H)
    (n : ℤ) : HomogeneousMap B T L n ≃ HomogeneousMap A M H n

SheafOfModules.DifferentialGradedModule.homogeneousEquiv_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomHomComplex.lean, line 420. The attribute's comment: “Hom_{Mod^dg(B, d)}(M ⊗_A N, L) = Hom_{Mod^dg(A, d)}(M, SheafHom^dg_B(N, L)) as hom-complexes: degreewise, additively, and compatibly with the differentials”.

Tensor-hom adjunction for sheaves of differential graded modules, first identity, on the additions: the identification of the homogeneous morphisms is additive, so each degree of the two hom-complexes is identified as an abelian group.

theorem homogeneousEquiv_add (hT : IsTensorProduct M N T) (hH : IsSheafHom N L H) (n : ℤ)
    (φ φ' χ : HomogeneousMap B T L n) (hχ : χ.val = φ.val + φ'.val) :
    (tensorHomHomogeneousEquiv hT hH n χ).val =
      (tensorHomHomogeneousEquiv hT hH n φ).val + (tensorHomHomogeneousEquiv hT hH n φ').val

SheafOfModules.DifferentialGradedModule.homogeneousEquiv_delta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomHomComplex.lean, line 438. The attribute's comment: “Hom_{Mod^dg(B, d)}(M ⊗_A N, L) = Hom_{Mod^dg(A, d)}(M, SheafHom^dg_B(N, L)) as hom-complexes: degreewise, additively, and compatibly with the differentials”.

Tensor-hom adjunction for sheaves of differential graded modules, first identity, on the differentials: the identification of the homogeneous morphisms commutes with the commutator differential of the two hom-complexes.

theorem homogeneousEquiv_delta (hT : IsTensorProduct M N T) (hH : IsSheafHom N L H) (n : ℤ)
    (φ : HomogeneousMap B T L n) (ψ : HomogeneousMap B T L (n + 1))
    (hψ : ψ.val = δ n (n + 1) φ.val) :
    (tensorHomHomogeneousEquiv hT hH (n + 1) ψ).val =
      δ n (n + 1) (tensorHomHomogeneousEquiv hT hH n φ).val

SheafOfModules.DifferentialGradedModule.dgHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomHomComplex.lean, line 490. The attribute's comment: “Hom_{Mod^dg(B, d)}(M ⊗_A N, L) = Hom_{Mod^dg(A, d)}(M, SheafHom^dg_B(N, L)) as hom-complexes: degreewise, additively, and compatibly with the differentials”.

Tensor-hom adjunction for sheaves of differential graded modules, first identity: the degree-n homogeneous morphisms M ⊗_A N → L of the differential graded category Mod^dg(B, d) are the degree-n homogeneous morphisms M → SheafHom^dg_B(N, L) of the differential graded category Mod^dg(A, d).

noncomputable def dgHomEquiv (hT : IsTensorProduct M N T) (hH : IsSheafHom N L H) (n : ℤ) :
    (dgCategoryData B).category.Hom (moduleObject B (dgCategoryData B) T)
        (moduleObject B (dgCategoryData B) L) n ≃
      (dgCategoryData A).category.Hom (moduleObject A (dgCategoryData A) M)
        (moduleObject A (dgCategoryData A) H) n

SheafOfModules.DifferentialGradedModule.dgHomEquiv_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomHomComplex.lean, line 503. The attribute's comment: “Hom_{Mod^dg(B, d)}(M ⊗_A N, L) = Hom_{Mod^dg(A, d)}(M, SheafHom^dg_B(N, L)) as hom-complexes: degreewise, additively, and compatibly with the differentials”.

Tensor-hom adjunction for sheaves of differential graded modules, first identity: the identification of the two hom-complexes commutes with their differentials, so it is an equality of complexes and not only of their degreewise components.

theorem dgHomEquiv_d (hT : IsTensorProduct M N T) (hH : IsSheafHom N L H) (n : ℤ)
    (f : (dgCategoryData B).category.Hom (moduleObject B (dgCategoryData B) T)
      (moduleObject B (dgCategoryData B) L) n) :
    (dgCategoryData A).category.d (dgHomEquiv hT hH n f) =
      dgHomEquiv hT hH (n + 1) ((dgCategoryData B).category.d f)

SheafOfModules.DifferentialGradedModule.homogeneousEquiv_naturality_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomHomComplex.lean, line 535. The attribute's comment: “functoriality of the hom-complex identity in M: a morphism M' ⟶ M compatible with the tensor products carries the identification at M to the one at M'”.

Tensor-hom adjunction for sheaves of differential graded modules, first identity, functoriality in M: a morphism u : M' ⟶ M of right differential graded A-modules induces t : M' ⊗_A N ⟶ M ⊗_A N, and the identification of the hom-complexes carries precomposition with t to precomposition with u.

theorem homogeneousEquiv_naturality_left (hT : IsTensorProduct M N T)
    (hT' : IsTensorProduct M' N T') (hH : IsSheafHom N L H) (u : M' ⟶ M) (t : T' ⟶ T)
    (ht : ∀ (i j : ℤ) (U : X.Cᵒᵖ) (x : (M'.complex.X i).val.obj U)
      (y : (N.complex.X j).val.obj U),
      (t.toHomologicalComplex.f (i + j)).val.app U (hT'.tmul i j U x y) =
        hT.tmul i j U ((u.toHomologicalComplex.f i).val.app U x) y)
    (n : ℤ) (φ : HomogeneousMap B T L n) (φ' : HomogeneousMap B T' L n)
    (hφ' : φ'.val = (Cochain.ofHom t.toHomologicalComplex).comp φ.val (zero_add n)) :
    (tensorHomHomogeneousEquiv hT' hH n φ').val =
      (Cochain.ofHom u.toHomologicalComplex).comp
        (tensorHomHomogeneousEquiv hT hH n φ).val (zero_add n)

SheafOfModules.DifferentialGradedModule.homogeneousEquiv_naturality_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomHomComplex.lean, line 567. The attribute's comment: “functoriality of the hom-complex identity in L: a morphism L ⟶ L', with the induced map of internal homs, commutes with the identification”.

Tensor-hom adjunction for sheaves of differential graded modules, first identity, functoriality in L: a morphism k : L ⟶ L' of right differential graded B-modules induces g : SheafHom^dg_B(N, L) ⟶ SheafHom^dg_B(N, L'), and the identification of the hom-complexes carries postcomposition with k to postcomposition with g.

theorem homogeneousEquiv_naturality_right (hT : IsTensorProduct M N T)
    (hH : IsSheafHom N L H) (hH' : IsSheafHom N L' H') (k : L ⟶ L') (g : H ⟶ H')
    (hg : ∀ (m : ℤ) (U : X.C) (p : (H.complex.X m).val.obj (Opposite.op U)) (i j : ℤ)
      (hij : i + m = j) (V : Over U) (y : (N.complex.X i).val.obj (Opposite.op V.left)),
      (hH'.isInternalHom.sectionsEquiv m U
          ((g.toHomologicalComplex.f m).val.app (Opposite.op U) p)).app i j hij V y =
        (k.toHomologicalComplex.f j).val.app (Opposite.op V.left)
          ((hH.isInternalHom.sectionsEquiv m U p).app i j hij V y))
    (n : ℤ) (φ : HomogeneousMap B T L n) (φ' : HomogeneousMap B T L' n)
    (hφ' : φ'.val = φ.val.comp (Cochain.ofHom k.toHomologicalComplex) (add_zero n)) :
    (tensorHomHomogeneousEquiv hT hH' n φ').val =
      (tensorHomHomogeneousEquiv hT hH n φ).val.comp
        (Cochain.ofHom g.toHomologicalComplex) (add_zero n)

SheafOfModules.DifferentialGradedModule.homogeneousEquiv_naturality_bimodule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedTensorHomHomComplex.lean, line 596. The attribute's comment: “functoriality of the hom-complex identity in N: a morphism N ⟶ N' of bimodules, compatible with the tensor products and the internal homs, commutes with the identification”.

Tensor-hom adjunction for sheaves of differential graded modules, first identity, functoriality in N: a morphism σ : N ⟶ N' of differential graded (A, B)-bimodules induces t : M ⊗_A N ⟶ M ⊗_A N' and g : SheafHom^dg_B(N', L) ⟶ SheafHom^dg_B(N, L), and the identification of the hom-complexes carries precomposition with t to postcomposition with g.

theorem homogeneousEquiv_naturality_bimodule (hT : IsTensorProduct M N T)
    (hT' : IsTensorProduct M N' T') (hH : IsSheafHom N L H) (hH' : IsSheafHom N' L H')
    (σ : N ⟶ N') (t : T ⟶ T') (g : H' ⟶ H)
    (ht : ∀ (i j : ℤ) (U : X.Cᵒᵖ) (x : (M.complex.X i).val.obj U)
      (y : (N.complex.X j).val.obj U),
      (t.toHomologicalComplex.f (i + j)).val.app U (hT.tmul i j U x y) =
        hT'.tmul i j U x ((σ.toHomologicalComplex.f j).val.app U y))
    (hg : ∀ (m : ℤ) (U : X.C) (p : (H'.complex.X m).val.obj (Opposite.op U)) (i j : ℤ)
      (hij : i + m = j) (V : Over U) (y : (N.complex.X i).val.obj (Opposite.op V.left)),
      (hH.isInternalHom.sectionsEquiv m U
          ((g.toHomologicalComplex.f m).val.app (Opposite.op U) p)).app i j hij V y =
        (hH'.isInternalHom.sectionsEquiv m U p).app i j hij V
          ((σ.toHomologicalComplex.f i).val.app (Opposite.op V.left) y))
    (n : ℤ) (φ : HomogeneousMap B T L n) (φ' : HomogeneousMap B T' L n)
    (hφ : φ.val = (Cochain.ofHom t.toHomologicalComplex).comp φ'.val (zero_add n)) :
    (tensorHomHomogeneousEquiv hT hH n φ).val =
      (tensorHomHomogeneousEquiv hT' hH' n φ').val.comp
        (Cochain.ofHom g.toHomologicalComplex) (add_zero n)
Sources
LeanSheafOfModules.DifferentialGradedBimodule.equivLeftStructure · SheafOfModules.DifferentialGradedAlgebra.asBimodule · SheafOfModules.DifferentialGradedModule.restrictScalars · SheafOfModules.DifferentialGradedAlgebra.Hom.toBimodule · SheafOfModules.DifferentialGradedModule.restrictionObj · SheafOfModules.DifferentialGradedModule.restrictionMap · SheafOfModules.DifferentialGradedModule.restriction · SheafOfModules.DifferentialGradedModule.extensionRestrictionAdjunction

Section24.18 Pull and push for sheaves of differential graded modules#

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

Tag 0FRU, a lemma

Tag 0FRU in the Stacks Project.

Stacks.DifferentialGradedPullbackConstruction.exists_pullbackPushforwardHomEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedPushPullAdjunction.lean, line 121.

Pull and push for sheaves of differential graded modules: for the direct image f_* and the pullback f^*M = f⁻¹M ⊗_{f⁻¹A'} A along a morphism of small ringed sites, together with a unital homomorphism φ₀ : f⁻¹A' ⟶ A, Hom_{Mod^dg(A', d)}(M, f_*N) = Hom_{Mod^dg(A, d)}(f^*M, N).

The identification e of the two differential graded Hom objects is given in every degree n, it is precomposition with the unit M ⟶ f^*M of the pullback — so in particular it is additive and natural — and it carries the differential of the one Hom complex to the differential of the other. Its degree-zero closed part is the bijection e₀ of hom-sets of the adjunction f^* ⊣ f_*, which sends a morphism g : f^*M ⟶ N to the unit followed by g, read as a morphism M ⟶ f_*N.

theorem exists_pullbackPushforwardHomEquiv (φ₀ : inverseImageAlgebra α hO hP A' ⟶ A)
    (hφ₀ : φ₀.IsUnital) :
    ∃ (e : ∀ (M : SheafOfModules.DifferentialGradedModule.{u, u, u} A')
          (N : SheafOfModules.DifferentialGradedModule.{u, u, u} A) (n : ℤ),
          HomogeneousMap (X := ⟨D, K, Psharp⟩) A (pullbackObj α hO hP φ₀ hφ₀ M) N n ≃
            HomogeneousMap (X := ⟨C, J, Osharp⟩) A' M
              (pushforwardObj (semilinearHom α hO hP φ₀ hφ₀) N) n)
        (e₀ : ∀ (M : SheafOfModules.DifferentialGradedModule.{u, u, u} A')
          (N : SheafOfModules.DifferentialGradedModule.{u, u, u} A),
          (pullbackObj α hO hP φ₀ hφ₀ M ⟶ N) ≃
            (M ⟶ pushforwardObj (semilinearHom α hO hP φ₀ hφ₀) N)),
      (∀ M N n w, (e M N n w).val =
          precompCochain (pullbackUnit α hO hP φ₀ hφ₀ M) w.val) ∧
      (∀ M N n w w' w'', w''.val = w.val + w'.val →
          (e M N n w'').val = (e M N n w).val + (e M N n w').val) ∧
      (∀ M N n w w', w'.val = δ n (n + 1) w.val →
          (e M N (n + 1) w').val = δ n (n + 1) (e M N n w).val) ∧
      (∀ M N g, e₀ M N g = semilinearHomEquiv (semilinearHom α hO hP φ₀ hφ₀) M N
          ((pullbackUnit α hO hP φ₀ hφ₀ M).postcomp g))
Sources
LeanStacks.DifferentialGradedPullbackConstruction.exists_pullbackPushforwardHomEquiv

Section24.19 Localization and sheaves of differential graded modules#

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

Tag 0FRW, a lemma

Tag 0FRW in the Stacks Project.

SheafOfModules.dgExtendHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedExtensionByZero.lean, line 689. The attribute's comment: “Hom(j_! M, N) = Hom(M, j^* N) in degree zero”.

Tag 0FRW in degree zero. The homomorphisms j_!M ⟶ N of right differential graded A-modules are the homomorphisms M ⟶ j^*N of right differential graded A_U-modules. The bijection is the degreewise adjunction j_{U!} ⊣ j_U^* of ordinary sheaves of modules; the content is that it matches the A-linear chain maps with the A_U-linear ones. This is the degree-zero closed part of the hom-complex identification of the source; the identification in every degree is SheafOfModules.dgHomOfDegreeExtendEquiv_isHomComplexDifferential.

noncomputable def dgExtendHomEquiv (N : DifferentialGradedModule.{w, max u v m, max u v m} A) :
    (dgExtensionByZero.{m} O U A M ⟶ N) ≃ (M ⟶ N.over U)

SheafOfModules.dgExtensionByZeroAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedExtensionByZero.lean, line 706. The attribute's comment: “the identification is an adjunction j_! ⊣ j^* of differential graded modules”.

Tag 0FRW in degree zero, as an adjunction. j_! : Mod^dg(A_U, d) ⥤ Mod^dg(A, d) is left adjoint to j^* : Mod^dg(A, d) ⥤ Mod^dg(A_U, d), which is the displayed identification of Hom-sets of the source together with its naturality in both variables.

noncomputable def dgExtensionByZeroAdjunction :
    dgExtensionByZeroFunctor.{m} O U A ⊣ DifferentialGradedModule.overFunctor A U

SheafOfModules.dgHomOfDegreeExtendEquiv_isHomComplexDifferential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedExtensionByZero.lean, line 756. The attribute's comment: “Hom(j_! M, N) = Hom(M, j^* N) as complexes: compatibility with the differentials”.

Tag 0FRW. The identification of Tag 0FRA of the homogeneous homomorphisms of degree d out of j_!M with those into j^*N matches the differentials of the two hom-complexes. Read in every degree together with SheafOfModules.gradedHomOfDegreeExtendEquiv and its naturality, this is the displayed identification Hom_{Mod^dg(A, d)}(j_!M, N) = Hom_{Mod^dg(A_U, d)}(M, j^*N) of complexes of abelian groups.

theorem dgHomOfDegreeExtendEquiv_isHomComplexDifferential
    (N : DifferentialGradedModule.{w, max u v m, max u v m} A) (d : ℤ)
    (f : GradedHomOfDegree (GradedModule.ofDifferentialGraded (dgExtensionByZero.{m} O U A M))
      (GradedModule.ofDifferentialGraded N) d)
    (g : GradedHomOfDegree (GradedModule.ofDifferentialGraded (dgExtensionByZero.{m} O U A M))
      (GradedModule.ofDifferentialGraded N) (d + 1)) :
    IsHomComplexDifferential f g ↔
      IsHomComplexDifferential (A := A.over U) (M := M) (N := N.over U) (d := d)
        (gradedHomOfDegreeExtendEquiv.{m} (M := GradedModule.ofDifferentialGraded M)
          (N := GradedModule.ofDifferentialGraded N) O U A.toGradedAlgebra d f)
        (gradedHomOfDegreeExtendEquiv.{m} (M := GradedModule.ofDifferentialGraded M)
          (N := GradedModule.ofDifferentialGraded N) O U A.toGradedAlgebra (d + 1) g)
Tag 0FRX, a lemma

Tag 0FRX in the Stacks Project.

SheafOfModules.dgExtendTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedExtensionByZeroTensor.lean, line 332. The attribute's comment: “j_! M ⊗_A N = j_!(M ⊗_{A_U} N|_U) as complexes of O-modules”.

Tag 0FRX. The relative tensor product of the extension by zero of a right differential graded A_U-module M with a left differential graded A-module N is the extension by zero of the relative tensor product of M with the restriction of N: j_!M ⊗_A N = j_!(M ⊗_{A_U} N|_U) as complexes of O-modules. In each degree it is the isomorphism of Tag 0FRB, which sends the local section j_!x ⊗ y to j_!(x ⊗ y) and is natural in M and in N; what is proved here is that it commutes with the differentials.

noncomputable def dgExtendTensorIso :
    dgExtendTensor.{m} O U A M N ≅ dgExtendSliceTensor.{m} O U A M N

SheafOfModules.dgExtendTensorIso_naturality_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedExtensionByZeroTensor.lean, line 362. The attribute's comment: “functoriality of j_! M ⊗_A N = j_!(M ⊗_{A_U} N|_U) in M, in each degree”.

Tag 0FRX, functoriality in the right differential graded module. In every degree the identification j_!M ⊗_A N = j_!(M ⊗_{A_U} N|_U) commutes with a homomorphism M ⟶ M' of right differential graded A_U-modules; its components are the degreewise maps of the relative tensor products induced by j_!M ⟶ j_!M', respectively by M ⟶ M'.

theorem dgExtendTensorIso_naturality_left
    {M' : DifferentialGradedModule.{w, max u v m, max u v m} (A.over U)} (h : M ⟶ M') (n : ℤ) :
    RelativeTensor.gradedTensorMapRight (gradedExtensionByZeroMap.{m} O U A.toGradedAlgebra
          (GradedModule.ofDifferentialGradedMap h))
          (LeftGradedModule.ofDifferentialGraded N) n ≫
        (dgExtendTensorIso.{m} O U A M' N).hom.f n =
      (dgExtendTensorIso.{m} O U A M N).hom.f n ≫ (extendSheaf.{m} O U).map
        (RelativeTensor.gradedTensorMapRight (J := J.over U) (Osharp := O.over U)
          (GradedModule.ofDifferentialGradedMap h)
          ((LeftGradedModule.ofDifferentialGraded N).over U) n)

SheafOfModules.dgExtendTensorIso_naturality_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedExtensionByZeroTensor.lean, line 380. The attribute's comment: “functoriality of j_! M ⊗_A N = j_!(M ⊗_{A_U} N|_U) in N, in each degree”.

Tag 0FRX, functoriality in the left differential graded module. In every degree the identification j_!M ⊗_A N = j_!(M ⊗_{A_U} N|_U) commutes with a homomorphism N ⟶ N' of left differential graded A-modules.

theorem dgExtendTensorIso_naturality_right
    {N' : LeftDifferentialGradedModule.{w, max u v m, max u v m} A} (f : N ⟶ N') (n : ℤ) :
    RelativeTensor.gradedTensorMap (gradedExtensionByZero.{m} O U A.toGradedAlgebra
          (GradedModule.ofDifferentialGraded M))
          (LeftGradedModule.ofDifferentialGradedMap f) n ≫
        (dgExtendTensorIso.{m} O U A M N').hom.f n =
      (dgExtendTensorIso.{m} O U A M N).hom.f n ≫ (extendSheaf.{m} O U).map
        (RelativeTensor.gradedTensorMap (J := J.over U) (Osharp := O.over U)
          (GradedModule.ofDifferentialGraded M)
          (LeftGradedModule.overMap (LeftGradedModule.ofDifferentialGradedMap f) U) n)
Sources
LeanSheafOfModules.dgExtendHomEquiv · SheafOfModules.dgExtensionByZeroAdjunction · SheafOfModules.dgHomOfDegreeExtendEquiv_isHomComplexDifferential · SheafOfModules.dgExtendTensorIso · SheafOfModules.dgExtendTensorIso_naturality_left · SheafOfModules.dgExtendTensorIso_naturality_right

Section24.20 Shift functors on sheaves of differential graded modules#

Section 24.20 of the Stacks Project, Tag 0FRY. 1 tag here is carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FRY, the section

Tag 0FRY in the Stacks Project.

SheafOfModules.DifferentialGradedModule.dgShiftFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedShiftFunctor.lean, line 105. The attribute's comment: “the shift functor [k] on Mod^dg(A, d)”.

Stacks Project, Tag 0FRY. The k-th shift functor [k] on the differential graded category Mod^dg(A, d) of right differential graded A-modules: a functor of differential graded categories, so additive and linear on Hom modules and compatible with the differential, the composition and the identities.

noncomputable def dgShiftFunctor (k : ℤ) :
    DGCategory.DGFunctor (dgCategoryData.{u, v, w} A).category
      (dgCategoryData.{u, v, w} A).category

SheafOfModules.DifferentialGradedModule.dgShiftFunctor_complex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedShiftFunctor.lean, line 113. The attribute's comment: “clauses (1) and (2): the underlying complex of M[k]”.

Stacks Project, Tag 0FRY, clauses (1) and (2). The complex of sheaves of modules underlying M[k] is the k-th shift of the complex underlying M.

theorem dgShiftFunctor_complex (k : ℤ) (M : DifferentialGradedModule.{u, v, w} A) :
    (asModule A ((dgShiftFunctor.{u, v, w} A k).obj (asObject A M))).complex =
      (CochainComplex.shiftFunctor
        (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) k).obj M.complex

SheafOfModules.DifferentialGradedModule.dgShiftFunctor_map_v, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedShiftFunctor.lean, line 149. The attribute's comment: “the components of f[k]”.

Stacks Project, Tag 0FRY. The components of the shift f[k] of a homogeneous morphism f of degree n are those of f, multiplied by (-1)^{k n}. See the implementation notes: the sign is forced by the requirement that [k] be a functor of differential graded categories, and it is +1 in the degree the source's clause is about.

theorem dgShiftFunctor_map_v (k n : ℤ) (M N : DifferentialGradedModule.{u, v, w} A)
    (f : (dgCategoryData.{u, v, w} A).category.Hom (asObject A M) (asObject A N) n)
    (p q : ℤ) (h : p + n = q) :
    HEq ((asCochain A ((dgShiftFunctor.{u, v, w} A k).map f)).v p q h)
      ((Int.negOnePow (k * n) : ℤ) • (asCochain A f).v (p + k) (q + k) (by omega))

SheafOfModules.DifferentialGradedModule.dgShiftFunctor_map_v_of_degree_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedShiftFunctor.lean, line 160. The attribute's comment: “f[k] has the same component maps as f in degree zero”.

Stacks Project, Tag 0FRY. On a homogeneous morphism of degree zero — in particular on a morphism of Mod(A, d) — the shift f[k] has literally the same component maps as f, which is the source's formulation.

theorem dgShiftFunctor_map_v_of_degree_zero (k : ℤ)
    (M N : DifferentialGradedModule.{u, v, w} A)
    (f : (dgCategoryData.{u, v, w} A).category.Hom (asObject A M) (asObject A N) 0)
    (p q : ℤ) (h : p + 0 = q) :
    HEq ((asCochain A ((dgShiftFunctor.{u, v, w} A k).map f)).v p q h)
      ((asCochain A f).v (p + k) (q + k) (by omega))

SheafOfModules.DifferentialGradedModule.dgShiftFunctor_zero_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedShiftFunctor.lean, line 174. The attribute's comment: “[0] is the identity”.

Stacks Project, Tag 0FRY. The zeroth shift is the identity on objects.

theorem dgShiftFunctor_zero_obj (M : (dgCategoryData.{u, v, w} A).category.Obj) :
    (dgShiftFunctor.{u, v, w} A 0).obj M = M

SheafOfModules.DifferentialGradedModule.dgShiftFunctor_add_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedShiftFunctor.lean, line 186. The attribute's comment: “[k + l] = [k] ∘ [l]”.

Stacks Project, Tag 0FRY. [k + l] = [k] ∘ [l] on objects.

theorem dgShiftFunctor_add_obj (k l : ℤ) (M : (dgCategoryData.{u, v, w} A).category.Obj) :
    (dgShiftFunctor.{u, v, w} A (k + l)).obj M =
      (dgShiftFunctor.{u, v, w} A k).obj ((dgShiftFunctor.{u, v, w} A l).obj M)

SheafOfModules.DifferentialGradedModule.dgShiftFunctor_add_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedShiftFunctor.lean, line 193. The attribute's comment: “[k + l] = [k] ∘ [l] on morphisms”.

Stacks Project, Tag 0FRY. [k + l] = [k] ∘ [l] on homogeneous morphisms.

theorem dgShiftFunctor_add_map (k l : ℤ) {M N : (dgCategoryData.{u, v, w} A).category.Obj}
    {n : ℤ} (f : (dgCategoryData.{u, v, w} A).category.Hom M N n) :
    HEq ((dgShiftFunctor.{u, v, w} A (k + l)).map f)
      ((dgShiftFunctor.{u, v, w} A k).map ((dgShiftFunctor.{u, v, w} A l).map f))

SheafOfModules.DifferentialGradedModule.dgShiftHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedShiftFunctor.lean, line 204. The attribute's comment: “Hom(L, M[k]) = Hom(L, M)[k]”.

Stacks Project, Tag 0FRY. The identification Hom(L, M[k])^n = Hom(L, M)^{n + k}, as modules over the global sections of the structure sheaf.

noncomputable def dgShiftHomEquiv (k : ℤ) (L M : (dgCategoryData.{u, v, w} A).category.Obj)
    (n : ℤ) :
    (dgCategoryData.{u, v, w} A).category.Hom L M (n + k) ≃ₗ[(limit X.O.obj : CommRingCat.{u})]
      (dgCategoryData.{u, v, w} A).category.Hom L ((dgShiftFunctor.{u, v, w} A k).obj M) n

SheafOfModules.DifferentialGradedModule.dgShiftHomEquiv_d, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedShiftFunctor.lean, line 214. The attribute's comment: “Hom(L, M[k]) = Hom(L, M)[k] is compatible with the differentials”.

Stacks Project, Tag 0FRY. The identification Hom(L, M[k]) = Hom(L, M)[k] is compatible with the differentials: on the right hand side the differential of a shifted complex carries the sign (-1)^k.

theorem dgShiftHomEquiv_d (k : ℤ) (L M : (dgCategoryData.{u, v, w} A).category.Obj) (n : ℤ)
    (f : (dgCategoryData.{u, v, w} A).category.Hom L M (n + k)) :
    dgShiftHomEquiv.{u, v, w} A k L M (n + 1)
        ((dgCategoryData.{u, v, w} A).category.d' (by omega : (n + k) + 1 = (n + 1) + k) f) =
      (-1 : (limit X.O.obj : CommRingCat.{u})) ^ k.natAbs •
        (dgCategoryData.{u, v, w} A).category.d (dgShiftHomEquiv.{u, v, w} A k L M n f)
Sources
LeanSheafOfModules.DifferentialGradedModule.dgShiftFunctor · SheafOfModules.DifferentialGradedModule.dgShiftFunctor_complex · SheafOfModules.DifferentialGradedModule.dgShiftFunctor_map_v · SheafOfModules.DifferentialGradedModule.dgShiftFunctor_map_v_of_degree_zero · SheafOfModules.DifferentialGradedModule.dgShiftFunctor_zero_obj · SheafOfModules.DifferentialGradedModule.dgShiftFunctor_add_obj · SheafOfModules.DifferentialGradedModule.dgShiftFunctor_add_map · SheafOfModules.DifferentialGradedModule.dgShiftHomEquiv

Section24.21 The homotopy category#

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

Tag 0FRZ, the section

Tag 0FRZ in the Stacks Project.

SheafOfModules.DifferentialGradedModule.homotopyCategoryEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryTriangulated.lean, line 571.

The homotopy category of right differential graded modules over a sheaf of differential graded algebras is the homotopy category of their differential graded category.

noncomputable def homotopyCategoryEquivalence :
    HomotopyCategory.{u, v, w} A ≌ (dgCategoryData.{u, v, w} A).category.K

SheafOfModules.DifferentialGradedModule.homotopyCategoryEquivalence_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryTriangulated.lean, line 578.

The identification of the two homotopy categories sends a differential graded module to itself.

theorem homotopyCategoryEquivalence_obj (M : DifferentialGradedModule.{u, v, w} A) :
    (homotopyCategoryEquivalence A).functor.obj ((HomotopyCategory.quotient A).obj M) =
      asObject A M

SheafOfModules.DifferentialGradedModule.homotopyCategoryEquivalence_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryTriangulated.lean, line 586.

The identification of the two homotopy categories sends the homotopy class of a morphism to the homotopy class of the closed degree-zero homogeneous map with the same underlying cochain.

theorem homotopyCategoryEquivalence_map {M N : DifferentialGradedModule.{u, v, w} A}
    (f : M ⟶ N) :
    ∃ c : (dgCategoryData.{u, v, w} A).category.Cocycle (asObject A M) (asObject A N),
      HEq (asCochain A c.val) (Cochain.ofHom f.toHomologicalComplex) ∧
        HEq ((homotopyCategoryEquivalence A).functor.map
            ((HomotopyCategory.quotient A).map f))
          (Quotient.mk ((dgCategoryData A).category.homotopySetoid _ _) c)
Tag 0FS0, a definition

Tag 0FS0 in the Stacks Project.

SheafOfModules.DifferentialGradedModule.Homotopy, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopy.lean, line 58. The attribute's comment: “homotopies”.

A homotopy between two morphisms of right differential graded modules: a map of graded modules of degree -1 whose commutator with the differentials is the difference of the two morphisms.

structure Homotopy {M N : DifferentialGradedModule.{t, a, m} A} (f g : M ⟶ N)

SheafOfModules.DifferentialGradedModule.Homotopic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopy.lean, line 74. The attribute's comment: “homotopic morphisms”.

Two morphisms of right differential graded modules are homotopic if there is a homotopy between them.

abbrev Homotopic {M N : DifferentialGradedModule.{t, a, m} A} (f g : M ⟶ N) : Prop
Tag 0FS1, a definition

Tag 0FS1 in the Stacks Project.

SheafOfModules.DifferentialGradedModule.HomotopyCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategory.lean, line 149. The attribute's comment: “the homotopy category”.

The homotopy category of right differential graded modules over a sheaf of differential graded algebras: the quotient of the category of right differential graded modules by the homotopy relation.

abbrev HomotopyCategory (A : DifferentialGradedAlgebra.{t, a} R) : Type _

SheafOfModules.DifferentialGradedModule.homotopic_congruence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategory.lean, line 155. The attribute's comment: “homotopy classes form a congruence”.

Being homotopic is an equivalence relation compatible with composition on either side.

theorem homotopic_congruence (A : DifferentialGradedAlgebra.{t, a} R) :
    CategoryTheory.Congruence
      (fun {M N : DifferentialGradedModule.{t, a, m} A} (f g : M ⟶ N) => Homotopic f g)
Tag 0FS2, a lemma

Tag 0FS2 in the Stacks Project.

SheafOfModules.DifferentialGradedModule.HomotopyCategory.hasProducts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryProducts.lean, line 108. The attribute's comment: “homotopy_products”.

The homotopy category of right differential graded modules admits arbitrary products.

noncomputable instance hasProducts (A : DifferentialGradedAlgebra.{t, a} R) :
    HasProducts.{m} (HomotopyCategory.{t, a, m} A)

SheafOfModules.DifferentialGradedModule.HomotopyCategory.hasCoproducts_ringedSite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryRingedSite.lean, line 120. The attribute's comment: “homotopy_direct_sums”.

The homotopy category of right differential graded modules over a sheaf of differential graded algebras on a ringed site admits arbitrary direct sums.

No side condition is carried: the two sheafification conditions of SheafOfModules.DifferentialGradedModule.HomotopyCategory.hasCoproducts are discharged here from the essential smallness of the site.

instance hasCoproducts_ringedSite {X : AlgebraicGeometry.RingedSite.{u, v, w}}
    (A : DifferentialGradedAlgebra.{w, a} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    HasCoproducts.{max u v m} (HomotopyCategory.{w, a, max u v m} A)
Sources
LeanSheafOfModules.DifferentialGradedModule.homotopyCategoryEquivalence · SheafOfModules.DifferentialGradedModule.homotopyCategoryEquivalence_obj · SheafOfModules.DifferentialGradedModule.homotopyCategoryEquivalence_map · SheafOfModules.DifferentialGradedModule.Homotopy · SheafOfModules.DifferentialGradedModule.Homotopic · SheafOfModules.DifferentialGradedModule.HomotopyCategory · SheafOfModules.DifferentialGradedModule.homotopic_congruence · SheafOfModules.DifferentialGradedModule.HomotopyCategory.hasProducts

Section24.22 Cones and triangles#

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

Tag 0FS4, a lemma

Tag 0FS4 in the Stacks Project.

SheafOfModules.DifferentialGradedModule.hasZeroObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAxiomA.lean, line 740. The attribute's comment: “axiom_a”.

The zero differential graded module has unique homogeneous maps to and from every object in every degree.

theorem hasZeroObject :
    ∃ Z : (dgCategoryData A).category.Obj,
      (∀ (M : (dgCategoryData A).category.Obj) (n : ℤ),
        Nonempty ((dgCategoryData A).category.Hom Z M n) ∧
          Subsingleton ((dgCategoryData A).category.Hom Z M n)) ∧
      (∀ (M : (dgCategoryData A).category.Obj) (n : ℤ),
        Nonempty ((dgCategoryData A).category.Hom M Z n) ∧
          Subsingleton ((dgCategoryData A).category.Hom M Z n))

SheafOfModules.DifferentialGradedModule.hasBinaryBiproducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAxiomA.lean, line 856. The attribute's comment: “axiom_a”.

Any two right differential graded modules admit a differential graded direct sum with closed degree-zero structure maps.

theorem hasBinaryBiproducts
    (M N : (dgCategoryData A).category.Obj) :
    Nonempty (DGCategory.BinaryBiproductData (dgCategoryData A).category M N)

SheafOfModules.DifferentialGradedModule.shiftAxiomB, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAxiomB.lean, line 1421. The attribute's comment: “axiom_b”.

The canonical DG shifts and Hom-complex shift isomorphisms for sheaf DG modules.

noncomputable def shiftAxiomB : CanonicalShiftAxiomB.{u, v, w} A
Tag 0FS5, a definition

Tag 0FS5 in the Stacks Project.

SheafOfModules.DifferentialGradedModule.shiftPackage_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedCone.lean, line 324. The attribute's comment: “fixed shifted module for the canonical cone projection”.

The degree-one shift of a right differential graded module exists with the unchanged right action.

theorem shiftPackage_nonempty {A : DifferentialGradedAlgebra.{t, a} R}
    (K : DifferentialGradedModule.{t, a, m} A) : Nonempty (ShiftPackage K)

SheafOfModules.DifferentialGradedModule.conePackage_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedCone.lean, line 613. The attribute's comment: “existence of the cone with its canonical maps”.

The mapping-cone construction exists with its componentwise action and canonical inclusion and projection.

theorem conePackage_nonempty {A : DifferentialGradedAlgebra.{t, a} R}
    {K L : DifferentialGradedModule.{t, a, m} A} (f : K ⟶ L) : Nonempty (ConePackage f)

SheafOfModules.DifferentialGradedModule.conePackage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedCone.lean, line 695. The attribute's comment: “the cone construction”.

The cone and its canonical maps, characterized by the mapping-cone complex and the direct-sum action.

noncomputable def conePackage {A : DifferentialGradedAlgebra.{t, a} R}
    {K L : DifferentialGradedModule.{t, a, m} A} (f : K ⟶ L) : ConePackage f
Tag 0FS6, a lemma

Tag 0FS6 in the Stacks Project.

SheafOfModules.DifferentialGradedModule.coneSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAxiomC.lean, line 861.

The differential graded category of right sheaf modules admits cones whose connecting arrows are the shifts of the original morphisms, using the fixed axiom (B) shift.

theorem coneSituation {X : AlgebraicGeometry.RingedSite.{u, u, u}}
    (A : DifferentialGradedAlgebra.{u, v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    ∃ S : DGCategory.ConeSituation
        (dgCategoryData.{u, v, w} A).category,
      S.shift = (shiftAxiomB A).axiomB
Tag 0FS7, a proposition

Tag 0FS7 in the Stacks Project.

SheafOfModules.DifferentialGradedModule.HomotopyCategory.instHasShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryTriangulated.lean, line 702. The attribute's comment: “part (1): the shift functors”.

The translation functors of the homotopy category of right differential graded modules, lifted from the differential graded shifts along the identification of the two homotopy categories.

noncomputable instance instHasShift : HasShift (HomotopyCategory.{u, v, w} A) ℤ

SheafOfModules.DifferentialGradedModule.HomotopyCategory.instPretriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryTriangulated.lean, line 727. The attribute's comment: “the pre-triangulated structure”.

The homotopy category of right differential graded modules is pretriangulated.

noncomputable instance instPretriangulated :
    Pretriangulated (HomotopyCategory.{u, v, w} A)

SheafOfModules.DifferentialGradedModule.HomotopyCategory.instIsTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryTriangulated.lean, line 734.

Tag 0FS7. The homotopy category of right differential graded modules over a sheaf of differential graded algebras on a ringed site is a triangulated category.

instance instIsTriangulated : IsTriangulated (HomotopyCategory.{u, v, w} A)

SheafOfModules.DifferentialGradedModule.HomotopyCategory.distinguished_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryTriangulated.lean, line 795. The attribute's comment: “part (2): the distinguished triangles”.

A triangle of the homotopy category of right differential graded modules is distinguished exactly when it is isomorphic to the triangle built from an admissible short exact sequence of right differential graded modules, the connecting arrow being the class of π d s.

theorem distinguished_iff (T : Pretriangulated.Triangle (HomotopyCategory.{u, v, w} A)) :
    T ∈ Pretriangulated.distinguishedTriangles (C := HomotopyCategory.{u, v, w} A) ↔
      ∃ (M N P : DifferentialGradedModule.{u, v, w} A) (f : M ⟶ N) (g : N ⟶ P)
        (δ : (quotient A).obj P ⟶
          (shiftFunctor (HomotopyCategory.{u, v, w} A) (1 : ℤ)).obj ((quotient A).obj M))
        (E : DGCategory.GradedSplitShortExact (A := (dgCategoryData.{u, v, w} A).category)
          (asObject A M) (asObject A N) (asObject A P)),
        cocycleOfHom A (dgCategoryData A) f = E.a ∧
          cocycleOfHom A (dgCategoryData A) g = E.b ∧
          Nonempty (T ≅ Pretriangulated.Triangle.mk ((quotient A).map f)
            ((quotient A).map g) δ) ∧
          Nonempty ((homotopyCategoryToDG A).mapTriangle.obj
              (Pretriangulated.Triangle.mk ((quotient A).map f) ((quotient A).map g) δ) ≅
            DGCategory.GradedSplitShortExact.associatedKTriangle
              (dgConeSituation A).shift E)

SheafOfModules.DifferentialGradedModule.HomotopyCategory.shiftFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedHomotopyCategoryTriangulated.lean, line 828. The attribute's comment: “part (1): the shift functors are those of Section 24.20”.

The degree-one translation of the homotopy category is the shift of differential graded modules of Stacks 0FS5.

theorem shiftFunctor_obj (M : DifferentialGradedModule.{u, v, w} A) :
    (shiftFunctor (HomotopyCategory.{u, v, w} A) (1 : ℤ)).obj ((quotient A).obj M) =
      (quotient A).obj (shift M)
Tag 0FS8, a remark

Tag 0FS8 in the Stacks Project.

SheafOfModules.DifferentialGradedModule.coneIdentity_hom_equiv_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedConeIdentity.lean, line 944.

A morphism from the identity cone is uniquely specified by a pair of global sections (x,y) with x = d y; the equivalence evaluates at the canonical unit elements in degrees zero and minus one.

theorem coneIdentity_hom_equiv_sections (A : DifferentialGradedAlgebra.{t, a} R)
    (M : DifferentialGradedModule.{t, a, a} A) :
    ∃ e : (identityCone A ⟶ M) ≃
        { p : (M.complex.X 0).sections × (M.complex.X (-1)).sections //
          ∀ U : Cᵒᵖ,
            p.1.eval U =
              (M.complex.d (-1) 0).val.app U (p.2.eval U) },
      ∀ (f : identityCone A ⟶ M) (U : Cᵒᵖ),
        (e f).1.1.eval U =
          (f.toHomologicalComplex.f 0).val.app U
            (((conePackage (𝟙 (regularModule A))).componentIso 0).inv.val.app U
              ((biprod.inr : (regularModule A).complex.X 0 ⟶
                  (regularModule A).complex.X 1 ⊞ (regularModule A).complex.X 0).val.app U
                (A.one.eval U))) ∧
        (e f).1.2.eval U =
          (f.toHomologicalComplex.f (-1)).val.app U
            (((conePackage (𝟙 (regularModule A))).componentIso (-1)).inv.val.app U
              ((biprod.inl : (regularModule A).complex.X 0 ⟶
                  (regularModule A).complex.X 0 ⊞ (regularModule A).complex.X (-1)).val.app U
                (A.one.eval U)))
Tag 0FS9, a lemma

Tag 0FS9 in the Stacks Project.

SheafOfModules.DifferentialGradedModule.isGrothendieckAbelian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedGrothendieck.lean, line 129.

Stacks Project, Tag 0FS9. Let (C, O) be a ringed site and let (A, d) be a differential graded O-algebra. The category Mod(A, d) of right differential graded A-modules is a Grothendieck abelian category.

It is abelian and has filtered colimits by Tag 0FRJ, those colimits are exact by filteredColimits_exact, it is locally small, and it has the separator ⨁_{k, U} j_{U!} C_U[k], the direct sum of the shifts of the cones on the identities of the restrictions of A to the objects of the site.

noncomputable instance isGrothendieckAbelian (A : DifferentialGradedAlgebra.{t, a} R) :
    IsGrothendieckAbelian.{max u v a w} (DifferentialGradedModule.{t, a, max u v a w} A)
Sources
LeanSheafOfModules.DifferentialGradedModule.hasZeroObject · SheafOfModules.DifferentialGradedModule.hasBinaryBiproducts · SheafOfModules.DifferentialGradedModule.shiftAxiomB · SheafOfModules.DifferentialGradedModule.shiftPackage_nonempty · SheafOfModules.DifferentialGradedModule.conePackage_nonempty · SheafOfModules.DifferentialGradedModule.conePackage · SheafOfModules.DifferentialGradedModule.coneSituation · SheafOfModules.DifferentialGradedModule.HomotopyCategory.instHasShift

Section24.23 Flat resolutions#

Section 24.23 of the Stacks Project, Tag 0FSA. 9 tags here are carried by 36 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0FSA, the section

Tag 0FSA in the Stacks Project.

SheafOfModules.IsGoodToposBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FreeDifferentialGradedModuleToposPullback.lean, line 431.

A good right differential graded module, with condition (3) read over the source's own base changes. A right differential graded A-module is good when it is flat as a graded module, K-flat, and for every base change along a morphism of ringed topoi — a second ringed topos X, a morphism of ringed topoi f : X ⟶ Y, a sheaf of differential graded algebras B on X and a unital homomorphism ψ : A ⟶ f_*B, which is the adjoint form of the source's φ : f⁻¹A ⟶ B — a pullback of P exists, as an object corepresenting Q ↦ Hom_A(P, f_{*,ψ}Q), and every such object is flat as a graded module and K-flat.

This is the quantification of Tag 0FSA's condition (3), binder for binder: a morphism of ringed topoi, a differential graded algebra on its source, a homomorphism over it, and conditions (1) and (2) required of the base-changed module. Nothing weaker and nothing stronger is quantified; in particular condition (3) is not vacuous and not an assumption of the sought-for isomorphism, the existential conjunct being part of the conclusion, and the second conjunct then transports to every chosen pullback by Functor.CorepresentableBy.uniqueUpToIso.

The direct image of sheaves of modules is toposDirectImageModules f, whose lax monoidal structure is toposDirectImageModules_laxMonoidal — unconditional, the coherence of Tag 03EL being proved in RingedToposPullbackCoherence.lean — so the target f_*B of ψ is formed from f alone and no monoidal datum is quantified beside it.

This is not SheafOfModules.DifferentialGradedModule.IsGood with its binders rewritten, and the two are incomparable, which is why no implication between them is proved here in either direction. IsGood quantifies bare functors of the two underlying categories: such a functor induces no morphism of topoi and yet can carry a PullbackData — the identity functor of a site at the trivial topology does, every presheaf being a sheaf there — so IsGood has clauses this definition has none at. In the other direction a morphism of topoi need not be induced by any functor of the two given sites, only by one of a site equivalent to the target (Tag 03CR, the first step of the source's own proof of Tag 0FSB), so IsGood has no clause at such a base change. What the two do share is conditions (1) and (2), verbatim; isGradedFlat and isKFlat below are the comparison that exists.

IsGoodCocontinuousBaseChange and IsGoodSiteBaseChange restrict IsGood's condition (3) to fewer base changes, so each is implied by IsGood and each is incomparable with this definition for the second of the two reasons above: a morphism of topoi induced by no functor of the two given sites is a clause of this definition and of neither of theirs.

Two restrictions on condition (3), stated rather than hidden. First, the second ringed topos carries HasSheafify X.J (Type w) and HasSheafify X.J AddCommGrpCat.{w}, together with the three GrothendieckTopology.HasSheafCompose instances a morphism of ringed topoi and its direct image need. The sheafification of abelian groups is what the relative tensor product of the conclusion needs; the sheafification of types is what lets a sheaf of graded sets and its degree fibres be formed there, and it is the instance the proof for A[S] consumes. Mathlib supplies both at Type (max u v) for a site C : Type u with [Category.{v} C], so they hold wherever the source's sites live, but a reading of condition (3) without them would be strictly stronger and this is not it. Second, the coefficient universe w is common to the two ringed topoi, where Stacks.Sheaves.RingedToposModules.RingedToposHom allows them independent; that boundary comes from the differential graded transport and is recorded in DifferentialGradedToposDirectImage.lean. Neither restriction is a hypothesis on a functor between the two underlying categories — there is none — and neither is a smallness assumption.

def IsGoodToposBaseChange (P : DifferentialGradedModule.{w, w, w} A) : Prop
Tag 0FSB, a lemma

Tag 0FSB in the Stacks Project.

SheafOfModules.dgExtensionByZeroRegular_isGoodToposBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodExtensionByZeroToposBaseChange.lean, line 255.

Tag 0FSB: the extension by zero j_!A_U of the restriction of A to the slice site at U is a good right differential graded A-module. It is flat as a graded module, it is K-flat, and after every base change along a morphism of ringed topoi a pullback of it exists and every pullback of it is again flat as a graded module and K-flat.

Conditions (1) and (2) are the two theorems of StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodExtensionByZero.lean, which run the source's argument from Tags 0FRB, 0FRX and 0FSB. Condition (3) is Tag 0FSG's, read through the identification of j_!A_U with the free differential graded module on the sheaf represented by U in degree zero.

theorem dgExtensionByZeroRegular_isGoodToposBaseChange :
    IsGoodToposBaseChange.{u, v₁, u₁} (dgExtensionByZeroRegular.{u} Y.O U A)
Tag 0FSC, a lemma

Tag 0FSC in the Stacks Project.

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGradedFlat_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAdmissibleFlat.lean, line 315. The attribute's comment: “condition (1) only — flatness of the underlying right graded module, two out of three along an admissible short exact sequence; condition (2) is the isKFlat_* lemmas and condition (3) the isGood_* lemmas, which together give the tag”.

Two out of three for flatness of the underlying right graded module: if the middle and the third term of an admissible short exact sequence of right differential graded modules are flat, so is the first one.

theorem isGradedFlat_left (h : IsAdmissibleShortExact f g)
    (hL : IsGradedFlat (GradedModule.ofDifferentialGraded L))
    (hM : IsGradedFlat (GradedModule.ofDifferentialGraded M)) :
    IsGradedFlat (GradedModule.ofDifferentialGraded K)

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGradedFlat_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAdmissibleFlat.lean, line 327. The attribute's comment: “condition (1) only — flatness of the underlying right graded module, two out of three along an admissible short exact sequence; condition (2) is the isKFlat_* lemmas and condition (3) the isGood_* lemmas, which together give the tag”.

Two out of three for flatness of the underlying right graded module: if the first and the middle term of an admissible short exact sequence of right differential graded modules are flat, so is the third one.

theorem isGradedFlat_right (h : IsAdmissibleShortExact f g)
    (hK : IsGradedFlat (GradedModule.ofDifferentialGraded K))
    (hL : IsGradedFlat (GradedModule.ofDifferentialGraded L)) :
    IsGradedFlat (GradedModule.ofDifferentialGraded M)

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGradedFlat_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAdmissibleFlat.lean, line 339. The attribute's comment: “condition (1) only — flatness of the underlying right graded module, two out of three along an admissible short exact sequence; condition (2) is the isKFlat_* lemmas and condition (3) the isGood_* lemmas, which together give the tag”.

Two out of three for flatness of the underlying right graded module: if the two outer terms of an admissible short exact sequence of right differential graded modules are flat, so is the middle one.

theorem isGradedFlat_middle (h : IsAdmissibleShortExact f g)
    (hK : IsGradedFlat (GradedModule.ofDifferentialGraded K))
    (hM : IsGradedFlat (GradedModule.ofDifferentialGraded M)) :
    IsGradedFlat (GradedModule.ofDifferentialGraded L)

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isKFlat_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAdmissibleTensor.lean, line 179. The attribute's comment: “condition (2) only — K-flatness, two out of three along an admissible short exact sequence; condition (1) is the isGradedFlat_* lemmas and condition (3) the isGood_* lemmas, which together give the tag”.

Two out of three for K-flatness: if the two outer terms of an admissible short exact sequence are K-flat, so is the middle one.

theorem isKFlat_middle (h : IsAdmissibleShortExact f g) (hK : RelativeTensor.IsKFlat K)
    (hM : RelativeTensor.IsKFlat M) : RelativeTensor.IsKFlat L

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isKFlat_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAdmissibleTensor.lean, line 188. The attribute's comment: “condition (2) only — K-flatness, two out of three along an admissible short exact sequence; condition (1) is the isGradedFlat_* lemmas and condition (3) the isGood_* lemmas, which together give the tag”.

Two out of three for K-flatness: if the middle and the third term of an admissible short exact sequence are K-flat, so is the first one.

theorem isKFlat_left (h : IsAdmissibleShortExact f g) (hL : RelativeTensor.IsKFlat L)
    (hM : RelativeTensor.IsKFlat M) : RelativeTensor.IsKFlat K

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isKFlat_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedAdmissibleTensor.lean, line 197. The attribute's comment: “condition (2) only — K-flatness, two out of three along an admissible short exact sequence; condition (1) is the isGradedFlat_* lemmas and condition (3) the isGood_* lemmas, which together give the tag”.

Two out of three for K-flatness: if the first and the middle term of an admissible short exact sequence are K-flat, so is the third one.

theorem isKFlat_right (h : IsAdmissibleShortExact f g) (hK : RelativeTensor.IsKFlat K)
    (hL : RelativeTensor.IsKFlat L) : RelativeTensor.IsKFlat M

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGood_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedAdmissible.lean, line 200. The attribute's comment: “two out of three for goodness: the first term, from the middle and the third”.

Two out of three for goodness: if the middle and the third term of an admissible short exact sequence of right differential graded modules are good, so is the first one.

theorem isGood_left (h : IsAdmissibleShortExact f g)
    (hL : IsGood.{t, m, v, u, m₁, v₁, u₁} L) (hM : IsGood.{t, m, v, u, m₁, v₁, u₁} M) :
    IsGood.{t, m, v, u, m₁, v₁, u₁} K

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGood_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedAdmissible.lean, line 212. The attribute's comment: “two out of three for goodness: the third term, from the first and the middle”.

Two out of three for goodness: if the first and the middle term of an admissible short exact sequence of right differential graded modules are good, so is the third one.

theorem isGood_right (h : IsAdmissibleShortExact f g)
    (hK : IsGood.{t, m, v, u, m₁, v₁, u₁} K) (hL : IsGood.{t, m, v, u, m₁, v₁, u₁} L) :
    IsGood.{t, m, v, u, m₁, v₁, u₁} M

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGood_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedAdmissible.lean, line 224. The attribute's comment: “two out of three for goodness: the middle term, from the two outer ones”.

Two out of three for goodness: if the two outer terms of an admissible short exact sequence of right differential graded modules are good, so is the middle one.

theorem isGood_middle (h : IsAdmissibleShortExact f g)
    (hK : IsGood.{t, m, v, u, m₁, v₁, u₁} K) (hM : IsGood.{t, m, v, u, m₁, v₁, u₁} M) :
    IsGood.{t, m, v, u, m₁, v₁, u₁} L

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGoodCocontinuousBaseChange_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedAdmissible.lean, line 239. The attribute's comment: “two out of three for goodness in the sense of IsGoodCocontinuousBaseChange — condition (3) quantified over the base changes whose pullback preserves colimits — the first term, from the middle and the third”.

Two out of three for goodness, goodness taken in the sense of IsGoodCocontinuousBaseChange: if the middle and the third term of an admissible short exact sequence are good, so is the first one.

theorem isGoodCocontinuousBaseChange_left (h : IsAdmissibleShortExact f g)
    (hL : IsGoodCocontinuousBaseChange.{t, m, v, u, m₁, v₁, u₁} L)
    (hM : IsGoodCocontinuousBaseChange.{t, m, v, u, m₁, v₁, u₁} M) :
    IsGoodCocontinuousBaseChange.{t, m, v, u, m₁, v₁, u₁} K

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGoodCocontinuousBaseChange_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedAdmissible.lean, line 255. The attribute's comment: “two out of three for goodness in the sense of IsGoodCocontinuousBaseChange — condition (3) quantified over the base changes whose pullback preserves colimits — the third term, from the first and the middle”.

Two out of three for goodness, goodness taken in the sense of IsGoodCocontinuousBaseChange: if the first and the middle term of an admissible short exact sequence are good, so is the third one.

theorem isGoodCocontinuousBaseChange_right (h : IsAdmissibleShortExact f g)
    (hK : IsGoodCocontinuousBaseChange.{t, m, v, u, m₁, v₁, u₁} K)
    (hL : IsGoodCocontinuousBaseChange.{t, m, v, u, m₁, v₁, u₁} L) :
    IsGoodCocontinuousBaseChange.{t, m, v, u, m₁, v₁, u₁} M

SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGoodCocontinuousBaseChange_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedAdmissible.lean, line 271. The attribute's comment: “two out of three for goodness in the sense of IsGoodCocontinuousBaseChange — condition (3) quantified over the base changes whose pullback preserves colimits — the middle term, from the two outer ones”.

Two out of three for goodness, goodness taken in the sense of IsGoodCocontinuousBaseChange: if the two outer terms of an admissible short exact sequence are good, so is the middle one.

theorem isGoodCocontinuousBaseChange_middle (h : IsAdmissibleShortExact f g)
    (hK : IsGoodCocontinuousBaseChange.{t, m, v, u, m₁, v₁, u₁} K)
    (hM : IsGoodCocontinuousBaseChange.{t, m, v, u, m₁, v₁, u₁} M) :
    IsGoodCocontinuousBaseChange.{t, m, v, u, m₁, v₁, u₁} L
Tag 0FSD, a lemma

Tag 0FSD in the Stacks Project.

SheafOfModules.DifferentialGradedModule.PullbackData.preservesColimitsOfSize_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedPullbackColimits.lean, line 77. The attribute's comment: “colimits commute with pullback: the pullback along a morphism of ringed sites preserves every colimit, being the left adjoint of the direct image”.

The pullback of sheaves of differential graded modules along a morphism of ringed sites preserves colimits of every shape. The pullback is a left adjoint, the direct image along the morphism being its right adjoint, and a left adjoint preserves colimits.

theorem preservesColimitsOfSize_functor : PreservesColimitsOfSize.{w, w'} P.functor

SheafOfModules.RelativeTensor.isColimit_dgTensorFunctor_mapCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedColimit.lean, line 126. The attribute's comment: “the relative tensor product with a fixed left differential graded module commutes, as a functor to complexes, with the colimits of right differential graded modules”.

The relative tensor product - ⊗_A N carries a colimit cocone of right differential graded modules to a colimit cocone of complexes of O-modules. A cocone of complexes is colimiting as soon as it is in every degree, and in degree n the functor is the composite of forgetting the differential, a left adjoint, with degree n of the relative tensor product of graded modules.

noncomputable def isColimit_dgTensorFunctor_mapCocone
    (N : LeftDifferentialGradedModule.{t, m, m} A) {K : D ⥤ DifferentialGradedModule.{t, m, m} A}
    {c : Cocone K} (hc : IsColimit c) : IsColimit ((dgTensorFunctor N).mapCocone c)

SheafOfModules.RelativeTensor.isKFlat_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedColimit.lean, line 141. The attribute's comment: “a colimit of K-flat right differential graded modules is K-flat, the K-flatness half of the lemma, for an index category whose colimits of sheaves of modules are exact”.

A colimit of K-flat right differential graded modules is K-flat, along any shape whose colimits of sheaves of modules are exact.

theorem isKFlat_of_isColimit {K : D ⥤ DifferentialGradedModule.{t, m, m} A} {c : Cocone K}
    (hc : IsColimit c) (hK : ∀ d : D, IsKFlat (K.obj d)) : IsKFlat c.pt

SheafOfModules.RelativeTensor.isKFlat_of_isColimitCofan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedColimit.lean, line 151. The attribute's comment: “an arbitrary direct sum of K-flat right differential graded modules is K-flat, the K-flatness half of the direct sum clause”.

An arbitrary direct sum of K-flat right differential graded modules is K-flat.

theorem isKFlat_of_isColimitCofan {ι : Type m} {P : ι → DifferentialGradedModule.{t, m, m} A}
    {c : Cofan P} (hc : IsColimit c) (hP : ∀ i, IsKFlat (P i)) : IsKFlat c.pt

SheafOfModules.RelativeTensor.isKFlat_of_isColimit_isFiltered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedColimit.lean, line 159. The attribute's comment: “a filtered colimit of K-flat right differential graded modules is K-flat, the K-flatness half of the filtered colimit clause”.

A filtered colimit of K-flat right differential graded modules is K-flat.

theorem isKFlat_of_isColimit_isFiltered {D : Type m} [SmallCategory D] [IsFiltered D]
    {K : D ⥤ DifferentialGradedModule.{t, m, m} A} {c : Cocone K} (hc : IsColimit c)
    (hK : ∀ d : D, IsKFlat (K.obj d)) : IsKFlat c.pt

SheafOfModules.DifferentialGradedModule.isGradedFlat_and_isKFlat_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedColimit.lean, line 180. The attribute's comment: “flatness of the underlying graded module and K-flatness pass to a colimit of right differential graded modules, for an index category whose colimits of sheaves of modules are exact”.

Flatness of the underlying graded module and K-flatness pass together to a colimit of right differential graded modules, along any shape whose colimits of sheaves of modules are exact. This is the conjunction that appears both as conditions (1) and (2) of IsGoodCocontinuousBaseChange and as its condition (3) after a base change.

theorem isGradedFlat_and_isKFlat_of_isColimit {D : Type m} [Category.{m} D]
    [HasColimitsOfShape D (SheafOfModules.{m} (toRingCat J Osharp))]
    [HasExactColimitsOfShape D (SheafOfModules.{m} (toRingCat J Osharp))]
    {K : D ⥤ DifferentialGradedModule.{t, m, m} A} {c : Cocone K} (hc : IsColimit c)
    (hK : ∀ d : D, RelativeTensor.IsGradedFlat (GradedModule.ofDifferentialGraded (K.obj d)) ∧
      RelativeTensor.IsKFlat (K.obj d)) :
    RelativeTensor.IsGradedFlat (GradedModule.ofDifferentialGraded c.pt) ∧
      RelativeTensor.IsKFlat c.pt

SheafOfModules.isGoodToposBaseChange_of_isColimitCofan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedToposDirectSum.lean, line 67.

An arbitrary direct sum of good right differential graded modules is good, goodness being SheafOfModules.IsGoodToposBaseChange: conditions (1) and (2) of Tag 0FSA together with condition (3) read over the morphisms of ringed topoi out of the base.

theorem isGoodToposBaseChange_of_isColimitCofan {ι : Type w}
    {P : ι → DifferentialGradedModule.{w, w, w} A} {c : Cofan P} (hc : IsColimit c)
    (hP : ∀ i, IsGoodToposBaseChange.{w, v₁, u₁} (P i)) :
    IsGoodToposBaseChange.{w, v₁, u₁} c.pt

SheafOfModules.isGoodToposBaseChange_of_isColimit_isFiltered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedToposDirectSum.lean, line 79.

A filtered colimit of good right differential graded modules is good, goodness being SheafOfModules.IsGoodToposBaseChange.

theorem isGoodToposBaseChange_of_isColimit_isFiltered {D : Type w} [SmallCategory D]
    [IsFiltered D] {K : D ⥤ DifferentialGradedModule.{w, w, w} A} {c : Cocone K}
    (hc : IsColimit c) (hK : ∀ d : D, IsGoodToposBaseChange.{w, v₁, u₁} (K.obj d)) :
    IsGoodToposBaseChange.{w, v₁, u₁} c.pt

SheafOfModules.RelativeTensor.isGradedFlat_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedFlatColimit.lean, line 100. The attribute's comment: “a colimit of flat right graded modules is flat, the graded-flatness half of the lemma, for an index category whose colimits of sheaves of modules are exact”.

A colimit of flat right graded modules is flat, along any shape whose colimits of sheaves of modules are exact.

theorem isGradedFlat_of_isColimit {K : D ⥤ GradedModule.{t, m, m} A} {c : Cocone K}
    (hc : IsColimit c) (hK : ∀ d : D, IsGradedFlat (K.obj d)) : IsGradedFlat c.pt

SheafOfModules.RelativeTensor.isGradedFlat_of_isColimitCofan, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedFlatColimit.lean, line 140. The attribute's comment: “an arbitrary direct sum of flat right graded modules is flat, the graded-flatness half of the direct sum clause”.

An arbitrary direct sum of flat right graded modules is flat.

theorem isGradedFlat_of_isColimitCofan {ι : Type m} {P : ι → GradedModule.{t, m, m} A}
    {c : Cofan P} (hc : IsColimit c) (hP : ∀ i, IsGradedFlat (P i)) : IsGradedFlat c.pt

SheafOfModules.RelativeTensor.isGradedFlat_of_isColimit_isFiltered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GradedFlatColimit.lean, line 148. The attribute's comment: “a filtered colimit of flat right graded modules is flat, the graded-flatness half of the filtered colimit clause”.

A filtered colimit of flat right graded modules is flat.

theorem isGradedFlat_of_isColimit_isFiltered {D : Type m} [SmallCategory D] [IsFiltered D]
    {K : D ⥤ GradedModule.{t, m, m} A} {c : Cocone K} (hc : IsColimit c)
    (hK : ∀ d : D, IsGradedFlat (K.obj d)) : IsGradedFlat c.pt
Tag 0FSE, a lemma

Tag 0FSE in the Stacks Project.

SheafOfModules.DifferentialGradedModule.exists_flat_surjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedResolutionQuotient.lean, line 376. The attribute's comment: “the resolution is built from M alone: the first stage of the tower of Tag 0FSH, the twisted extension of the free module on the closed sections of M by the free module on the boundary pairs of its homomorphism to M. Clause (2) is concluded as surjectivity on the sections killed by the differential, which is stronger than surjectivity of Ker(d_P) to Ker(d_M), and also as an epimorphism on the sheaves of cocycles. Clause (3) is concluded here as conditions (1) and (2) of the definition of good in Section 0FSA, flatness of the underlying graded module and K-flatness, over a ringed site and with the ring universe and the module universe independent, and the whole of condition (3) for this same module is concluded over a ringed topos by exists_good_surjection”.

Tag 0FSE. Every right differential graded A-module M receives a homomorphism from a right differential graded A-module which is surjective, which is surjective on the sheaves of cocycles, and whose source is flat as a graded module and K-flat.

The source is the first stage of the tower of the first proof of Tag 0FSH: the twisted extension of the free differential graded module on the sheaf of graded sets of closed sections of M by the free module on the sheaf of graded sets of boundary pairs of its homomorphism to M. It is built from M alone.

Clause (2) is available on sections as well, as SheafOfModules.DifferentialGradedModule.exists_closed_preimage_towerStepMap: every local section of M^n killed by the differential is the image of a local section of the source killed by the differential. Clause (3) is read here as conditions (1) and (2) of the definition of good in Section 0FSA, flatness of the underlying graded module and K-flatness, over a ringed site and with the ring universe and the module universe independent; SheafOfModules.DifferentialGradedModule.exists_good_surjection concludes the same three clauses for the same module with the third at the whole of goodness, over a ringed topos.

theorem exists_flat_surjection (M : DifferentialGradedModule.{t, m, m} A) :
    ∃ (Q : DifferentialGradedModule.{t, m, m} A) (π : Q ⟶ M),
      (∀ n : ℤ, Epi (π.toHomologicalComplex.f n)) ∧
        (∀ n : ℤ, Epi (HomologicalComplex.cyclesMap π.toHomologicalComplex n)) ∧
          RelativeTensor.IsGradedFlat (GradedModule.ofDifferentialGraded Q) ∧
            RelativeTensor.IsKFlat Q

SheafOfModules.DifferentialGradedModule.exists_good_surjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedResolutionToposQuotient.lean, line 124.

Tag 0FSE. Every right differential graded A-module M receives a homomorphism from a right differential graded A-module which is surjective, which is surjective on the sheaves of cocycles, and whose source is good — SheafOfModules.IsGoodToposBaseChange, which is flat as a graded module, K-flat, and such that along every morphism of ringed topoi out of the base, every sheaf of differential graded algebras on its source and every unital homomorphism over it a pullback exists and is again flat and K-flat.

The source is the first stage of the tower of the first proof of Tag 0FSH: the twisted extension of the free differential graded module on the sheaf of graded sets of closed sections of M by the free module on the sheaf of graded sets of boundary pairs of its homomorphism to M. It is built from M alone.

Clause (2) is available on sections as well, as SheafOfModules.DifferentialGradedModule.exists_closed_preimage_towerStepMap: every local section of M^n killed by the differential is the image of a local section of the source killed by the differential.

SheafOfModules.DifferentialGradedModule.exists_flat_surjection is the same three clauses with the third read as conditions (1) and (2) of Section 0FSA alone, over a ringed site and with the ring universe and the module universe independent.

theorem exists_good_surjection [HasWeakSheafify Y.J (Type w)]
    (M : DifferentialGradedModule.{w, w, w} A) :
    ∃ (Q : DifferentialGradedModule.{w, w, w} A) (π : Q ⟶ M),
      (∀ n : ℤ, Epi (π.toHomologicalComplex.f n)) ∧
        (∀ n : ℤ, Epi (HomologicalComplex.cyclesMap π.toHomologicalComplex n)) ∧
          IsGoodToposBaseChange.{w, v₁, u₁} Q
Tag 0FSF, a remark

Tag 0FSF in the Stacks Project.

Stacks.SheafOfGradedSets, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FreeGradedModule.lean, line 181. The attribute's comment: “sheaf_of_graded_sets”.

A sheaf of graded sets on a site: a sheaf of sets together with a degree morphism to the constant sheaf of integers.

structure SheafOfGradedSets (J : GrothendieckTopology C) [HasWeakSheafify J (Type w)]

SheafOfModules.freeGradedModuleData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FreeGradedModule.lean, line 1770. The attribute's comment: “free_graded_mathcal_a_module_mathcal_a_mathcal_s”.

The free graded A-module on a sheaf of graded sets, with its presentation, its generators, its universal property and — whenever A is the graded algebra underlying a differential graded algebra — its closed-generator differential.

noncomputable def freeGradedModuleData : FreeGradedModuleData A S
Tag 0FSG, a lemma

Tag 0FSG in the Stacks Project.

SheafOfModules.freeDGModule_isGoodToposBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FreeDifferentialGradedModuleToposPullback.lean, line 502. The attribute's comment: “the free differential graded module on a sheaf of graded sets is good, with condition (3) of 0FSA read over morphisms of ringed topoi”.

Tag 0FSG: the free differential graded module A[S] on a sheaf of graded sets is good, at the source's own quantification. Conditions (1) and (2) are the two unconditional theorems of FreeGradedModuleFlat.lean; condition (3) is the corepresentability of B[f⁻¹S] together with the flatness of every object corepresenting the same functor, which is SheafOfModules.nonempty_corepresentableBy_and_flat at the geometric direct image. There is no hypothesis beyond those under which A[S] exists.

theorem freeDGModule_isGoodToposBaseChange [HasWeakSheafify Y.J (Type w)]
    (S : Stacks.SheafOfGradedSets.{w} Y.J) :
    IsGoodToposBaseChange.{w, v₁, u₁} (freeDGModule S A)

SheafOfModules.freeDGModule_isGradedFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FreeGradedModuleFlat/FlatAndKFlat.lean, line 483. The attribute's comment: “condition (1) of good (Stacks 0FSA) for the free graded module A[S] on a sheaf of graded sets: the underlying graded module is flat. No hypotheses; the source's own argument. Condition (2) is SheafOfModules.freeDGModule_isKFlat in this file; condition (3) is not proved here, and goodness is concluded at SheafOfModules.freeDGModule_isGoodToposBaseChange, where condition (3) is read over morphisms of ringed topoi as 0FSA states it. At the three site-indexed readings IsGood, IsGoodCocontinuousBaseChange and IsGoodSiteBaseChange condition (3) is still open -- see the implementation notes”.

Tag 0FSG, condition (1) of Tag 0FSA. The graded module underlying the free differential graded A-module A[S] on a sheaf of graded sets is flat. The differential plays no part: the underlying graded module of A[S] as a differential graded module is the free graded module on S over the graded algebra underlying A, so this is SheafOfModules.freeGradedModule_isGradedFlat.

theorem freeDGModule_isGradedFlat (D : DifferentialGradedAlgebra.{t, m} (toRingCat J Osharp))
    (S : SheafOfGradedSets.{m} J) :
    RelativeTensor.IsGradedFlat (GradedModule.ofDifferentialGraded (freeDGModule S D))

SheafOfModules.freeDGModule_isKFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FreeGradedModuleFlat/FlatAndKFlat.lean, line 519. The attribute's comment: “condition (2) of good (Stacks 0FSA) for the free differential graded module D[S] on a sheaf of graded sets: D[S] tensor_D N is acyclic for every acyclic left differential graded D-module N. No hypotheses; the source's own argument. Condition (1) is SheafOfModules.freeDGModule_isGradedFlat in this file; condition (3) is not proved here, and goodness is concluded at SheafOfModules.freeDGModule_isGoodToposBaseChange, where condition (3) is read over morphisms of ringed topoi as 0FSA states it. At the three site-indexed readings IsGood, IsGoodCocontinuousBaseChange and IsGoodSiteBaseChange condition (3) is still open -- see the implementation notes”.

Tag 0FSG, condition (2) of Tag 0FSA. The free differential graded D-module D[S] on a sheaf of graded sets is K-flat: D[S] ⊗_D N is acyclic for every acyclic left differential graded D-module N.

The proof is the source's. Degree n of D[S] ⊗_D N is the free graded module N[S] on S with coefficients in N, by SheafOfModules.freeTensorCoeffIso, and under that identification the differential is the signed degree-raising map of N[S], by SheafOfModules.freeTensorCoeff_dgTensorDiff. Exactness in degree n + 1 is then the exactness of a short complex of pieces of N[S] twisted by the sign automorphism, which SheafOfModules.coeffPiece_exact_sign deduces from the exactness of N in the three adjacent degrees; the transports matching the degrees of the three terms are SheafOfModules.coeffCastPieceIso.

theorem freeDGModule_isKFlat : RelativeTensor.IsKFlat (freeDGModule S D)
Tag 0FSH, a lemma

Tag 0FSH in the Stacks Project.

SheafOfModules.DifferentialGradedModule.exists_good_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedResolutionToposTower.lean, line 138.

Tag 0FSH: every right differential graded A-module receives a quasi-isomorphism from a good one. Goodness is SheafOfModules.IsGoodToposBaseChange: flat as a graded module, K-flat, and a pullback exists and is again flat and K-flat along every morphism of ringed topoi out of the base, every sheaf of differential graded algebras on its source and every unital homomorphism over it.

The source's tower is built here rather than assumed: the first stage is the free differential graded module on the sheaf of graded sets of closed sections of M, good by Tag 0FSG; each further stage is the twisted extension of the previous one by the free module on the boundary pairs of its homomorphism to M, good by SheafOfModules.cone_freeDGModule_isGoodToposBaseChange since a twisted extension is the cone of a homomorphism out of a free module; and the resolution is the colimit of the resulting sequence, good by SheafOfModules.isGoodToposBaseChange_of_isColimit_nat, the sequential shape being filtered.

theorem exists_good_quasiIso [HasWeakSheafify Y.J (Type w)]
    (M : DifferentialGradedModule.{w, w, w} A) :
    ∃ (Q : DifferentialGradedModule.{w, w, w} A) (f : Q ⟶ M),
      QuasiIso f.toHomologicalComplex ∧ IsGoodToposBaseChange.{w, v₁, u₁} Q

SheafOfModules.DifferentialGradedModule.exists_flat_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodDifferentialGradedResolutionTower.lean, line 150. The attribute's comment: “the tower of the first proof, built from M alone: the free differential graded module on the sheaf of graded sets of closed sections of M, then the twisted extensions by the free modules on the boundary pairs of each stage, then the colimit. The ring universe and the module universe stay independent here; at a common universe the same tower reaches the full goodness of Section 0FSA in SheafOfModules.DifferentialGradedModule.exists_good_quasiIso”.

Every right differential graded A-module receives a quasi-isomorphism from a right differential graded A-module which is flat as a graded module and K-flat.

The source's tower is built here rather than assumed: the first stage is the free differential graded module on the sheaf of graded sets of closed sections of M, each further stage is the twisted extension of the previous one by the free module on the boundary pairs of its homomorphism to M, and the resolution is the colimit of the resulting sequence.

theorem exists_flat_quasiIso (M : DifferentialGradedModule.{t, m, m} A) :
    ∃ (Q : DifferentialGradedModule.{t, m, m} A) (f : Q ⟶ M),
      QuasiIso f.toHomologicalComplex ∧
        RelativeTensor.IsGradedFlat (GradedModule.ofDifferentialGraded Q) ∧
          RelativeTensor.IsKFlat Q
Tag 0FSI, a lemma

Tag 0FSI in the Stacks Project.

SheafOfModules.DifferentialGradedModule.acyclic_dgTensor_of_isGood_of_acyclic_topos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodAcyclicDifferentialGradedToposPullback.lean, line 123. The attribute's comment: “part (1)”.

Tag 0FSI (1). "Let (C, O) be a ringed site. Let A be a sheaf of differential graded algebras on (C, O). Let P be a good acyclic right differential graded A-module. Then for any differential graded left A-module N the tensor product P ⊗_A N is acyclic."

Goodness is SheafOfModules.IsGoodToposBaseChange, the definition of Tag 0FSA.

theorem acyclic_dgTensor_of_isGood_of_acyclic_topos {Y : AlgebraicGeometry.RingedTopos.{u, u, u}}
    {A : DifferentialGradedAlgebra.{u, u} (toRingCat Y.J Y.O)}
    {P : DifferentialGradedModule.{u, u, u} A} (good : IsGoodToposBaseChange.{u, u, u} P)
    (acyclic : P.complex.Acyclic) (N : LeftDifferentialGradedModule.{u, u, u} A) :
    (RelativeTensor.dgTensor P N).Acyclic

SheafOfModules.DifferentialGradedModule.exists_toposCorepresentableBy_and_acyclic_and_isGood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/GoodAcyclicDifferentialGradedToposPullback.lean, line 141. The attribute's comment: “part (2)”.

Tag 0FSI (2). "Let (C, O) be a ringed site. Let A be a sheaf of differential graded algebras on (C, O). Let P be a good acyclic right differential graded A-module. Then for any morphism (f, f♯) : (Sh(C'), O') ⟶ (Sh(C), O) of ringed topoi and any differential graded O'-algebra A' and any map φ : f⁻¹A ⟶ A' of differential graded f⁻¹O-algebras the pullback f^*P is acyclic and good."

The map φ is written in its adjoint form, a unital ψ : A ⟶ f_*A'. The pullback f^*P along (f, A', ψ) is an object corepresenting Q ↦ Hom_A(P, f_{*,ψ}Q): one exists, and every one is acyclic and good, goodness being SheafOfModules.IsGoodToposBaseChange, the definition of Tag 0FSA.

theorem exists_toposCorepresentableBy_and_acyclic_and_isGood
    {X Y : AlgebraicGeometry.RingedTopos.{u, u, u}}
    {A : DifferentialGradedAlgebra.{u, u} (toRingCat Y.J Y.O)}
    {P : DifferentialGradedModule.{u, u, u} A} (good : IsGoodToposBaseChange.{u, u, u} P)
    (acyclic : P.complex.Acyclic) (f : RingedToposHom X Y)
    (A' : DifferentialGradedAlgebra.{u, u} (toRingCat X.J X.O))
    (ψ : A ⟶ toposPushforwardAlgebra (toposDirectImageModules (X := X) (Y := Y) f) A')
    (hψ : ψ.IsUnital) :
    (∃ T : DifferentialGradedModule.{u, u, u} A',
        Nonempty ((toposPushforward (toposDirectImageModules (X := X) (Y := Y) f) ψ hψ ⋙
          coyoneda.obj (Opposite.op P)).CorepresentableBy T)) ∧
      ∀ T : DifferentialGradedModule.{u, u, u} A',
        (toposPushforward (toposDirectImageModules (X := X) (Y := Y) f) ψ hψ ⋙
            coyoneda.obj (Opposite.op P)).CorepresentableBy T →
          T.complex.Acyclic ∧ IsGoodToposBaseChange.{u, u, u} T
Sources
LeanSheafOfModules.IsGoodToposBaseChange · SheafOfModules.dgExtensionByZeroRegular_isGoodToposBaseChange · SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGradedFlat_left · SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGradedFlat_right · SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isGradedFlat_middle · SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isKFlat_middle · SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isKFlat_left · SheafOfModules.DifferentialGradedModule.IsAdmissibleShortExact.isKFlat_right

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.