18.28 Flat modules to 18.39 Pullbacks of flat modules

Section18.28 Flat modules#

Section 18.28 of the Stacks Project, Tag 03EQ. 16 tags here are carried by 42 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03ER, a definition

Tag 03ER in the Stacks Project.

Stacks.IsFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorExactness.lean, line 391. The attribute's comment: “part (1), for the objectwise tensor product Stacks.tensorRight of this file, whose two module universes are independent of each other and of the ring universe. The tree carries a second objectwise tensor product, and part (1) for that one is AlgebraicGeometry.SheafOfModules.PresheafOfModules.IsFlat, which is also where parts (2) and (4) of the tag are registered”.

A presheaf of modules is flat when tensoring on the right with it is an exact endofunctor.

abbrev IsFlat (F : PresheafOfModules.{z} (ringPresheaf O)) : Prop

Stacks.SheafOfModules.IsFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorExactness.lean, line 590. The attribute's comment: “part (3), for Stacks.sheafTensorRight, the sheafified tensor product over Stacks.commRingSheafToRingSheaf. Part (3) over Stacks.SheafOfModules.Tensor.ringSheaf is AlgebraicGeometry.SheafOfModules.IsFlat, which is also where part (4) of the tag is registered”.

A sheaf of modules is flat when tensoring on the right with it is an exact endofunctor on sheaves of modules.

abbrev IsFlat {O : Sheaf J CommRingCat.{w}}
    [J.WEqualsLocallyBijective AddCommGrpCat.{z}]
    [HasWeakSheafify J AddCommGrpCat.{z}]
    (F : _root_.SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf O)) : Prop

AlgebraicGeometry.SheafOfModules.PresheafOfModules.IsFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Flat.lean, line 256. The attribute's comment: “part (1), for the objectwise tensor product AlgebraicGeometry.SheafOfModules.PresheafOfModules.tensorRight of this file; part (2) just below is stated in terms of it. Part (1) for the other objectwise tensor product in the tree, Stacks.tensorRight of StacksFrontier.Algebra.Category.ModuleCat.Sheaf.TensorExactness, is Stacks.IsFlat”.

A presheaf of modules is flat when tensoring on the right with it is an exact endofunctor.

abbrev IsFlat {O : Cᵒᵖ ⥤ CommRingCat.{w}}
    (F : _root_.PresheafOfModules.{z} (ringPresheaf O)) : Prop

AlgebraicGeometry.SheafOfModules.PresheafOfModules.IsFlatMap, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Flat.lean, line 263. The attribute's comment: “part (2)”.

A morphism of presheaves of rings is flat when its target ring presheaf, viewed as a module over the source by restriction of scalars, is flat.

abbrev IsFlatMap {O O' : Cᵒᵖ ⥤ CommRingCat.{w}} (f : O ⟶ O') : Prop

AlgebraicGeometry.SheafOfModules.IsFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Flat.lean, line 285. The attribute's comment: “part (3), over Stacks.SheafOfModules.Tensor.ringSheaf; cf. Stacks.SheafOfModules.IsFlat”. References: SGA 4 V (1.1), “commutative case”.

A sheaf of modules is flat when tensoring on the right with it is an exact endofunctor on sheaves of modules.

This is part (3) of tag 03ER for the native tensor bifunctor, and part (4) just below is stated in terms of it. Stacks.SheafOfModules.IsFlat uses the same native tensor functor.

abbrev IsFlat {O : Sheaf J CommRingCat.{w}}
    [J.WEqualsLocallyBijective AddCommGrpCat.{z}]
    [HasWeakSheafify J AddCommGrpCat.{z}]
    (F : _root_.SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf O)) : Prop

AlgebraicGeometry.SheafOfModules.IsFlatMap, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Flat.lean, line 294. The attribute's comment: “part (4)”.

A morphism of sheaves of rings is flat when its target ring sheaf, viewed as a module over the source by restriction of scalars, is flat.

abbrev IsFlatMap {O O' : Sheaf J CommRingCat.{w}} (f : O ⟶ O') : Prop

Tag 03ES, a lemma

Tag 03ES in the Stacks Project.

AlgebraicGeometry.SheafOfModules.PresheafOfModules.isFlat_of_objectwise_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/ObjectwiseFlat.lean, line 91.

A presheaf of modules whose sections over every object are flat is flat. Finite limits and finite colimits of presheaves of modules are computed objectwise, so exactness of the objectwise tensor endofunctor is an objectwise condition, and over each object it is exactness of tensoring modules by the sections there.

theorem isFlat_of_objectwise_flat {O : Cᵒᵖ ⥤ CommRingCat.{w}}
    (F : _root_.PresheafOfModules.{z} (ringPresheaf O))
    (hF : ∀ U : Cᵒᵖ, Module.Flat ((ringPresheaf O).obj U) (F.obj U)) :
    IsFlat F

Tag 03ET, a lemma

Tag 03ET in the Stacks Project.

Stacks.SheafOfModules.FlatSheafification.isFlat_sheafification, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatSheafification.lean, line 425.

The sheaf associated to a flat presheaf of modules is flat over the associated sheaf of rings.

public lemma isFlat_sheafification
    {O : Cᵒᵖ ⥤ CommRingCat.{w}} {Osharp : Sheaf J CommRingCat.{w}}
    (a : O ⋙ forget₂ CommRingCat.{w} RingCat.{w} ⟶
      (Stacks.SheafOfModules.Tensor.ringSheaf Osharp).obj)
    [Presheaf.IsLocallyInjective J a]
    [Presheaf.IsLocallySurjective J a]
    (F : PresheafOfModules.{z} (O ⋙ forget₂ CommRingCat.{w} RingCat.{w}))
    (hF : AlgebraicGeometry.SheafOfModules.PresheafOfModules.IsFlat F) :
    AlgebraicGeometry.SheafOfModules.IsFlat
      ((PresheafOfModules.sheafification
        (R := Stacks.SheafOfModules.Tensor.ringSheaf Osharp) a).obj F)

Tag 0GN1, a lemma

Tag 0GN1 in the Stacks Project.

Stacks.SheafOfModules.FlatSheafification.isFlat_sheafification_of_locally_objectwise_flat, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatSheafification.lean, line 393.

If a presheaf of modules is objectwise flat after passing to a covering of every object, then its associated sheaf is flat.

public lemma isFlat_sheafification_of_locally_objectwise_flat
    {O : Cᵒᵖ ⥤ CommRingCat.{w}} {Osharp : Sheaf J CommRingCat.{w}}
    (a : O ⋙ forget₂ CommRingCat.{w} RingCat.{w} ⟶
      (Stacks.SheafOfModules.Tensor.ringSheaf Osharp).obj)
    [Presheaf.IsLocallyInjective J a]
    [Presheaf.IsLocallySurjective J a]
    (F : PresheafOfModules.{z} (O ⋙ forget₂ CommRingCat.{w} RingCat.{w}))
    (hF : ∀ U : C,
      ∃ (I : Type (max u v)) (X : I → C) (f : ∀ i, X i ⟶ U),
        Sieve.ofArrows X f ∈ J U ∧
          ∀ i, Module.Flat (O.obj (Opposite.op (X i))) (F.obj (Opposite.op (X i)))) :
    AlgebraicGeometry.SheafOfModules.IsFlat
      ((PresheafOfModules.sheafification
        (R := Stacks.SheafOfModules.Tensor.ringSheaf Osharp)
        a).obj F)

Tag 03EU, a lemma

Tag 03EU in the Stacks Project.

Stacks.isFlat_coproduct, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/FlatColimits.lean, line 236. The attribute's comment: “part (1), direct sums”.

Stacks 03EU, direct sums. A coproduct of flat presheaves of modules is flat.

lemma isFlat_coproduct {O : Cᵒᵖ ⥤ CommRingCat.{w}} {ι : Type z}
    (F : ι → PresheafOfModules.{z} (ringPresheaf O))
    (hF : ∀ i, IsFlat (F i)) : IsFlat (∐ F)

Stacks.isFlat_colimit, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/FlatColimits.lean, line 446. The attribute's comment: “part (1), filtered colimits”.

Stacks 03EU, filtered colimits. A filtered colimit of flat presheaves of modules is flat.

lemma isFlat_colimit {O : Cᵒᵖ ⥤ CommRingCat.{w}}
    {J : Type ju} [Category.{jv} J] [IsFiltered J] [UnivLE.{ju, z}]
    (F : J ⥤ PresheafOfModules.{z} (ringPresheaf O))
    (hF : ∀ j, IsFlat (F.obj j)) : IsFlat (colimit F)

Stacks.SheafOfModules.FlatColimits.isFlat_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatColimits.lean, line 225. The attribute's comment: “part (2), filtered colimits”.

Stacks Project, Tag 03EU part (2), filtered colimits. A filtered colimit of flat sheaves of modules is flat.

theorem isFlat_colimit {O : Sheaf J CommRingCat.{w}}
    {I : Type z} [Category.{z} I] [IsFiltered I]
    (F : I ⥤ _root_.SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf O))
    (hF : ∀ i, IsFlat (F.obj i)) :
    IsFlat (colimit F)

Stacks.SheafOfModules.FlatColimits.isFlat_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatColimits.lean, line 241. The attribute's comment: “part (2), direct sums”.

Stacks Project, Tag 03EU part (2), direct sums. An arbitrary direct sum of flat sheaves of modules is flat. An arbitrary coproduct is the filtered colimit of its finite subcoproducts, so this follows from the finite case isFlat_coproduct_finite and the filtered-colimit case isFlat_colimit.

theorem isFlat_coproduct {O : Sheaf J CommRingCat.{w}} {ι : Type z}
    (F : ι → _root_.SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf O))
    (hF : ∀ i, IsFlat (F i)) :
    IsFlat (∐ F)

Stacks.SheafOfModules.FlatCoproduct.isFlat_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatCoproduct.lean, line 234.

A direct sum of flat sheaves of modules is flat.

theorem isFlat_coproduct {O : Sheaf J CommRingCat.{max u v}} {ι : Type (max u v)}
    (F : ι → _root_.SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf O))
    (hF : ∀ i, IsFlat (F i)) :
    IsFlat (∐ F)

Tag 0E8J, a lemma

Tag 0E8J in the Stacks Project.

Stacks.SheafOfModules.FlatRestriction.OfEssentiallySmall.isFlat_over_of_essentiallySmall, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FlatRestrictionEssentiallySmall.lean, line 108. The attribute's comment: “for a site essentially u-small, objects in Type c, morphisms and modules in u”.

Restriction to an object of a ringed site whose objects form a type in a universe of their own, with morphisms, sections and modules in one universe u and the site essentially u-small, preserves flatness of sheaves of modules.

theorem isFlat_over_of_essentiallySmall
    (X : AlgebraicGeometry.RingedSite.{c, u, u}) [EssentiallySmall.{u} X.C] (U : X.C)
    [X.J.HasSheafCompose (forget₂ CommRingCat.{u} RingCat.{u})]
    [(X.J.over U).HasSheafCompose (forget₂ CommRingCat.{u} RingCat.{u})]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{u}] [HasWeakSheafify X.J AddCommGrpCat.{u}]
    [(X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasWeakSheafify (X.J.over U) AddCommGrpCat.{u}]
    (F : SheafOfModules.{u} (ringSheaf X.O))
    (hF : AlgebraicGeometry.SheafOfModules.IsFlat F) :
    AlgebraicGeometry.SheafOfModules.IsFlat (O := X.O.over U) (F.over U)

Stacks.SheafOfModules.FlatRestriction.isFlat_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Gate18b/FlatRestriction.lean, line 215. References: SGA 4 V (1.6.1).

Stacks Project, Tag 0E8J. Restriction to an object of a ringed site preserves flatness of module sheaves.

public theorem isFlat_over
    (F : SheafOfModules.{u} (ringSheaf X.O))
    (hF : AlgebraicGeometry.SheafOfModules.IsFlat F) :
    AlgebraicGeometry.SheafOfModules.IsFlat (O := X.O.over U) (F.over U)

Stacks.SheafOfModules.FlatRestriction.FreeModuleUniverse.isFlat_over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Gate18b/FlatRestrictionFreeModuleUniverse.lean, line 157. The attribute's comment: “objects in Type u, morphisms in v, ring sections in w, modules in max v a, and no smallness assumption on the site”. References: SGA 4 V (1.6.1).

Restriction preserves flatness, at a free module universe. Restriction to an object of a ringed site preserves flatness of module sheaves, for objects of the site in Type u, morphisms in v, the structure sheaf in w and the modules in max v a, with no smallness assumption on the site.

public theorem isFlat_over
    (F : SheafOfModules.{max v a} (ringSheaf X.O))
    (hF : AlgebraicGeometry.SheafOfModules.IsFlat F) :
    AlgebraicGeometry.SheafOfModules.IsFlat (O := X.O.over U) (F.over U)

Tag 03EV, a lemma

Tag 03EV in the Stacks Project.

Stacks.Sites.OverModules.presheafExtensionUnit_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/FlatSliceExtension.lean, line 47. The attribute's comment: “part (1)”.

The extension from the slice category over U of the rank-one module is a flat presheaf of modules.

theorem presheafExtensionUnit_isFlat {C : Type u} [Category.{v} C]
    (O : Cᵒᵖ ⥤ CommRingCat.{max u v w}) (U : C) :
    AlgebraicGeometry.SheafOfModules.PresheafOfModules.IsFlat
      ((presheafModuleAdjunctionsOver (ringPresheaf O) U).extension.obj
        (PresheafOfModules.unit (overRingPresheaf (ringPresheaf O) U)))

Stacks.Sites.OverModules.sheafExtensionUnit_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/FlatSliceExtension.lean, line 72. The attribute's comment: “part (2)”.

The extension by zero from the localized site of the structure sheaf is a flat sheaf of modules.

theorem sheafExtensionUnit_isFlat {C : Type u} [Category.{u} C]
    (J : GrothendieckTopology C)
    [J.HasSheafCompose (forget₂ CommRingCat.{u} RingCat.{u})]
    [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasWeakSheafify J AddCommGrpCat.{u}]
    (O : Sheaf J CommRingCat.{u}) (U : C) :
    AlgebraicGeometry.SheafOfModules.IsFlat
      ((SheafOfModules.pullback.{u} (F := Over.forget U)
        (𝟙 ((Stacks.SheafOfModules.Tensor.ringSheaf O).over U) :
          ((Stacks.SheafOfModules.Tensor.ringSheaf O).over U) ⟶
            ((Stacks.SheafOfModules.Tensor.ringSheaf O).over U))).obj
        (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf O).over U)))

Tag 03EW, a lemma

Tag 03EW in the Stacks Project.

Stacks.SimplicialModules.exists_epi_isFlat_simplicial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Simplicial/SimplicialFlatResolution.lean, line 171. The attribute's comment: “part (4) at the simplicial site Δ × C of 09D0”.

[Stacks, Tag 03EW] part (4) at the simplicial site of [Stacks, Tag 09D0]. Every simplicial A_•-module — that is, every sheaf of modules over the sheaf of rings on Δ × C associated to a simplicial sheaf of commutative rings A_•, as in [Stacks, Tag 09D1] — receives an epimorphism from a flat one.

theorem exists_epi_isFlat_simplicial
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} (simplicialCommRingSheaf J A))) :
    ∃ (N : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf.{u, u, u} (simplicialCommRingSheaf J A)))
      (p : N ⟶ M),
      AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u}
        (O := simplicialCommRingSheaf J A) N ∧ Epi p

SheafOfModules.exists_epi_from_coproduct_extensionByZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ExtensionByZeroGenerators.lean, line 308. The attribute's comment: “part (3)”.

Every sheaf of O-modules is a quotient of a direct sum of extensions by zero j_{U!}O_U of the structure sheaves of slices. The sum is indexed by the sections of M, the summand attached to a section over U being j_{U!}O_U, and the map sends the tautological generating section of that summand to the section.

theorem exists_epi_from_coproduct_extensionByZero (M : SheafOfModules.{u} O) :
    ∃ (ι : Type u) (U : ι → C)
      (π : (∐ fun i ↦ (extensionByZero.{u, u, u, u} O (U i)).obj (unit (O.over (U i)))) ⟶ M),
        Epi π

Stacks.SheafOfModules.FlatResolution.exists_epi_from_coproduct_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FlatResolution/PresheafFlatQuotient.lean, line 199. The attribute's comment: “part (1)”.

Stacks 03EW, part (1). Every presheaf of modules is a quotient of a direct sum of extensions from slice categories of the rank-one module. The sum is indexed by all pairs (U, s) with s a section of F over U, and the component at (U, s) is the morphism adjoint to s.

theorem exists_epi_from_coproduct_extension (O : Cᵒᵖ ⥤ RingCat.{w})
    (F : _root_.PresheafOfModules.{max u v w z} O) :
    ∃ (ι : Type (max u v w z)) (U : ι → C),
      ∃ (p : (∐ fun i : ι =>
        ((presheafModuleAdjunctionsOver.{v, u, w, max w z} O (U i)).extension.obj
          (uliftUnit.{max u v w z} (overRingPresheaf O (U i))))) ⟶ F), Epi p

Stacks.SheafOfModules.FlatResolution.exists_epi_from_flat_presheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FlatResolution/PresheafFlatQuotient.lean, line 249. The attribute's comment: “part (2)”.

Stacks 03EW, part (2). Every presheaf of modules over a presheaf of commutative rings is a quotient of a flat presheaf of modules: the direct sum produced by part (1) is a direct sum of slice extensions of the rank-one module, each of which is flat.

theorem exists_epi_from_flat_presheaf (O : Cᵒᵖ ⥤ CommRingCat.{w})
    (F : _root_.PresheafOfModules.{max u v w z} (ringPresheaf O)) :
    ∃ P : _root_.PresheafOfModules.{max u v w z} (ringPresheaf O),
      AlgebraicGeometry.SheafOfModules.PresheafOfModules.IsFlat P ∧
        ∃ (p : P ⟶ F), Epi p

Stacks.SheafOfModules.FlatResolution.exists_epi_from_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FlatResolution/SheafFlatQuotient.lean, line 60. The attribute's comment: “part (4)”.

Stacks 03EW, part (4). Every sheaf of modules over a sheaf of commutative rings is a quotient of a flat sheaf of modules.

theorem exists_epi_from_flat (O : Sheaf J CommRingCat.{w})
    (F : _root_.SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf O)) :
    ∃ P : _root_.SheafOfModules.{max u v w z} (Stacks.SheafOfModules.Tensor.ringSheaf O),
      AlgebraicGeometry.SheafOfModules.IsFlat P ∧ ∃ (p : P ⟶ F), Epi p

Declarations registered for the tag:

• Stacks.SheafOfModules.FlatCover.exists_epi_from_isFlat, declared in the repository, registered with add_to_stacks in StacksFrontier/Deformation/ToposThickening/ModulesOnThickening/TensorSheafSections.lean, line 153 (StacksFrontier): “part (4): every sheaf of modules is a quotient of a flat one”.

Tag 03EX, a lemma

Tag 03EX in the Stacks Project.

Stacks.sheafTensorRight_shortExact_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafFlatCover.lean, line 792. The attribute's comment: “sheaf_tensor_exactness”. References: SGA 1 IV (1.1), “(i)”; SGA 4 XVII (4.1.1), “(ii), f = id”.

Stacks Project, Tag 03EX, sheaf case. If the final term of a short exact sequence of sheaves of modules is flat, then tensoring the sequence with any sheaf of modules gives a short exact sequence of sheaves of modules.

theorem sheafTensorRight_shortExact_of_flat
    (S : ShortComplex (SheafOfModules.{max t w} (Stacks.SheafOfModules.Tensor.ringSheaf O)))
    (G : SheafOfModules.{max t w} (Stacks.SheafOfModules.Tensor.ringSheaf O))
    (hS : S.ShortExact) (hflat : SheafOfModules.IsFlat S.X₃) :
    ∃ h : ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, max t w, max t w} O).flip.obj
          G).map S.f ≫
        ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, max t w, max t w} O).flip.obj
          G).map S.g = 0,
      (ShortComplex.mk
        (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, max t w, max t w} O).flip.obj
          G).map S.f)
        (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, max t w, max t w} O).flip.obj
          G).map S.g) h).ShortExact

Stacks.SheafOfModules.shortExact_map_sheafTensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedTensor/TensorOfAShortExactSequence.lean, line 166. The attribute's comment: “part (2)”. References: SGA 1 IV (1.1), “(i)”; SGA 4 XVII (4.1.1), “(ii), f = id”.

Tensoring a short exact sequence of sheaves of modules whose third term is flat with any sheaf of modules gives a short exact sequence.

theorem shortExact_map_sheafTensorObj
    (S : ShortComplex (SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hS : S.ShortExact)
    (hflat : AlgebraicGeometry.SheafOfModules.IsFlat.{u, u, u, u} (O := X.O) S.X₃)
    (M : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    (S.map ((Stacks.SheafOfModules.Tensor.sheafTensor X.O).obj M)).ShortExact

Stacks.SheafOfModules.FlatResolution.Presheaf.shortExact_map_tensorRight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FlatResolution/TensorExactness.lean, line 243. The attribute's comment: “part (1)”. References: EGA IV (2.1.10), “special case”; SGA 1 IV (1.1), “more general”; SGA 4 XVII (4.1.1), “(ii), special case”.

Stacks 03EX, part (1). If the third term of a short exact sequence of presheaves of modules is flat, then tensoring the sequence with an arbitrary presheaf of modules gives a short exact sequence.

The proof is the source's. Right exactness of the objectwise tensor product gives exactness in the middle and an epimorphism on the right, so the content is injectivity on the left. For that, resolve the second tensor factor G by a flat presheaf of modules P (Stacks 03EW part (2)), let K be the kernel of P ⟶ G, and chase the 3-by-3 diagram whose columns are the sequence tensored with K, P and G and whose rows are K ⟶ P ⟶ G tensored with the three terms of the sequence: the first column and the second row are exact because tensoring is right exact in each variable, the second column is left exact because P is flat, and the bottom row is left exact because the third term of the sequence is flat.

theorem shortExact_map_tensorRight
    {S : ShortComplex (_root_.PresheafOfModules.{max u v w z} (ringPresheaf O))}
    (hS : S.ShortExact) (h₃ : PresheafOfModules.IsFlat S.X₃)
    (G : _root_.PresheafOfModules.{max u v w z} (ringPresheaf O)) :
    (S.map (PresheafOfModules.tensorRight G)).ShortExact

Tag 03EY, a lemma

Tag 03EY in the Stacks Project.

Stacks.SheafOfModules.FlatTwoOutOfThree.isFlat_middle_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatTwoOutOfThree.lean, line 170. The attribute's comment: “sheaves, part (1)”.

Tag 03EY, part (1) for sheaves. In a short exact sequence of sheaves of modules whose outer terms are flat, the middle term is flat.

theorem isFlat_middle_of_shortExact
    (S : ShortComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)))
    (hS : S.ShortExact)
    (h₁ : AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) S.X₁)
    (h₃ : AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) S.X₃) :
    AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) S.X₂

Stacks.SheafOfModules.FlatTwoOutOfThree.isFlat_left_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatTwoOutOfThree.lean, line 188. The attribute's comment: “sheaves, part (2)”. References: SGA 4 XVII (4.1.1), “(i)”.

Tag 03EY, part (2) for sheaves. In a short exact sequence of sheaves of modules whose middle and right terms are flat, the left term is flat.

theorem isFlat_left_of_shortExact
    (S : ShortComplex (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)))
    (hS : S.ShortExact)
    (h₂ : AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) S.X₂)
    (h₃ : AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) S.X₃) :
    AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) S.X₁

Stacks.SheafOfModules.FlatTwoOutOfThree.Presheaf.isFlat_middle_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatTwoOutOfThree.lean, line 350. The attribute's comment: “presheaves, part (1)”.

Tag 03EY, part (1) for presheaves. In a short exact sequence of presheaves of modules whose outer terms are flat, the middle term is flat.

theorem isFlat_middle_of_shortExact
    (S : ShortComplex (_root_.PresheafOfModules.{u} (ringPresheaf O)))
    (hS : S.ShortExact)
    (h₁ : PresheafOfModules.IsFlat S.X₁)
    (h₃ : PresheafOfModules.IsFlat S.X₃) :
    PresheafOfModules.IsFlat S.X₂

Stacks.SheafOfModules.FlatTwoOutOfThree.Presheaf.isFlat_left_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatTwoOutOfThree.lean, line 367. The attribute's comment: “presheaves, part (2)”. References: SGA 4 XVII (4.1.1), “(i), presheaves”.

Tag 03EY, part (2) for presheaves. In a short exact sequence of presheaves of modules whose middle and right terms are flat, the left term is flat.

theorem isFlat_left_of_shortExact
    (S : ShortComplex (_root_.PresheafOfModules.{u} (ringPresheaf O)))
    (hS : S.ShortExact)
    (h₂ : PresheafOfModules.IsFlat S.X₂)
    (h₃ : PresheafOfModules.IsFlat S.X₃) :
    PresheafOfModules.IsFlat S.X₁

Tag 03EZ, a lemma

Tag 03EZ in the Stacks Project.

Stacks.SheafOfModules.FlatResolution.acyclic_map_sheafTensorRight_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FlatResolution/TensorExactness.lean, line 140. The attribute's comment: “sheaves”. References: EGA IV (2.1.10), “Absolute case f = id”.

Stacks 03EZ, sheaf case. An exact ℕ-indexed complex of sheaves of modules all of whose terms are flat stays exact after tensoring with an arbitrary sheaf of modules.

This is also Stacks 05NL, the same statement for a ringed space: a ringed space is the ringed site of its lattice of opens, its O_X-modules are the sheaves of modules over the structure ring sheaf of that site, and the tensor product is sheafTensorRight. The site-level statement is recorded against the ringed-space tag for the same reason that the site-level flatness of Stacks 03ER(3) is recorded against Stacks 05ND in StacksFrontier/CategoryTheory/Sites/Modules/Flat.lean.

theorem acyclic_map_sheafTensorRight_of_isFlat
    (K : ChainComplex
      (_root_.SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) ℕ)
    (hK : K.Acyclic)
    (hflat : ∀ i, AlgebraicGeometry.SheafOfModules.IsFlat.{v, u, w, w} (O := R) (K.X i))
    (G : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf R)) :
    ((Functor.mapHomologicalComplex
      ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} R).flip.obj G)
      (ComplexShape.down ℕ)).obj K).Acyclic

Stacks.SheafOfModules.FlatResolution.Presheaf.acyclic_map_tensorRight_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FlatResolution/TensorExactness.lean, line 284. The attribute's comment: “presheaves”. References: EGA IV (2.1.10), “special case”.

Stacks 03EZ, presheaf case. An exact ℕ-indexed complex of presheaves of modules all of whose terms are flat stays exact after tensoring with an arbitrary presheaf of modules.

theorem acyclic_map_tensorRight_of_isFlat
    (K : ChainComplex (_root_.PresheafOfModules.{u} (ringPresheaf O)) ℕ)
    (hK : K.Acyclic)
    (hflat : ∀ i, PresheafOfModules.IsFlat (K.X i))
    (G : _root_.PresheafOfModules.{u} (ringPresheaf O)) :
    (((PresheafOfModules.tensorRight G).mapHomologicalComplex
      (ComplexShape.down ℕ)).obj K).Acyclic

Tag 0G6Q, a lemma

Tag 0G6Q in the Stacks Project.

Stacks.SheafOfModules.FlatTensor.isFlat_tensor, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Gate18/FlatTensorProduct.lean, line 473.

Stacks Project, Tag 0G6Q. The tensor product of two flat sheaves of modules is flat.

public lemma isFlat_tensor {O : Sheaf J CommRingCat.{w}}
    [J.WEqualsLocallyBijective AddCommGrpCat.{w}] [HasWeakSheafify J AddCommGrpCat.{w}]
    (G F : _root_.SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf O))
    (hG : AlgebraicGeometry.SheafOfModules.IsFlat G)
    (hF : AlgebraicGeometry.SheafOfModules.IsFlat F) :
    AlgebraicGeometry.SheafOfModules.IsFlat
      (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, z, z} O).flip.obj F).obj G)

Tag 05V4, a lemma

Tag 05V4 in the Stacks Project.

Stacks.FlatChangeOfRings.isFlat_extendScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatChangeOfRings.lean, line 373.

Stacks Project, Tag 05V4. Extension of scalars along a morphism of sheaves of commutative rings takes a flat sheaf of modules to a flat sheaf of modules.

theorem isFlat_extendScalars (hG : SheafOfModules.IsFlat G) :
    SheafOfModules.IsFlat ((extendScalars f).obj G)

Stacks.FlatChangeOfRings.isFlat_pullback_ringSheafMapId, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SiteUpSheafificationPullback.lean, line 320. The attribute's comment: “read for SheafOfModules.pullback along the identity functor of the site”.

Stacks 05V4 for SheafOfModules.pullback. Pullback along a change of rings on a fixed site takes a flat sheaf of modules to a flat sheaf of modules.

theorem isFlat_pullback_ringSheafMapId
    (G : _root_.SheafOfModules.{w} (commRingSheafToRingSheaf O₁))
    (hG : SheafOfModules.IsFlat G) :
    SheafOfModules.IsFlat
      ((_root_.SheafOfModules.pullback.{w} (structureMap (ringSheafMap f))).obj G)

Tag 08FC, a lemma

Tag 08FC in the Stacks Project.

Stacks.SheafOfModules.isFlat_iff_hasLocalSingleRelationFactorizations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatCriterionConverse.lean, line 458. The attribute's comment: “parts (1) and (2)”.

Stacks 08FC, parts (1) and (2). A sheaf of modules on a ringed site is flat exactly when every single finite relation among its sections locally factors through a finite free module by a matrix annihilating that relation.

theorem isFlat_iff_hasLocalSingleRelationFactorizations
    (F : _root_.SheafOfModules.{max v w} (commRingSheafToRingSheaf O)) :
    IsFlat F ↔ HasLocalSingleRelationFactorizations O F

Stacks.SheafOfModules.hasLocalSingleRelationFactorizations_of_isFlat_freeUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatEquivalence.lean, line 1036. The attribute's comment: “part (1) implies part (2)”. References: SGA 4 V (8.2.11), “(a), special case”.

A flat sheaf of modules satisfies the single-relation form of the local equational criterion: every relation ∑ᵢ aᵢ • sᵢ = 0 among its sections over an object U admits, on a covering sieve of U, a factorisation of the restricted sections through a finite free module by a matrix annihilating the restricted relation. The universe w of the sections of the structure sheaf is independent of the universes of the site.

theorem hasLocalSingleRelationFactorizations_of_isFlat_freeUniverse
    {F : _root_.SheafOfModules.{w} (commRingSheafToRingSheaf O)} (hF : IsFlat F) :
    HasLocalSingleRelationFactorizations O F

Stacks.SheafOfModules.isFlat_of_hasLocalSingleRelationFactorizations_freeUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatEquivalenceConverse.lean, line 280. The attribute's comment: “part (2) implies part (1)”.

Stacks 08FC, (2) implies (1). A sheaf of modules satisfying the single-relation form of the local equational criterion is flat: every relation ∑ᵢ aᵢ • sᵢ = 0 among its sections factoring locally through a finite free module annihilating the relation forces the tensor endofunctor - ⊗ F on sheaves of modules to be exact.

This is the universe-general form of Stacks.SheafOfModules.isFlat_of_hasLocalSingleRelationFactorizations, which proves the same implication for a structure sheaf O : Sheaf J CommRingCat.{max v w} on a site with morphisms in Type v. Here the section universe w is independent of u and v, and HasWeakSheafify is assumed in place of HasSheafify. A ringed site whose sections are unrelated to its morphisms cannot be fed to the max v w form, because w =?= max v u is not a solvable universe constraint. The proof sheafifies the local injectivity of the presheaf-level tensor map through Stacks.SheafOfModules.mono_shf_map_of_isLocallyInjective.

Together with Stacks.SheafOfModules.hasLocalSingleRelationFactorizations_of_isFlat_freeUniverse this gives the equivalence of parts (1) and (2) of the source at those universes.

theorem isFlat_of_hasLocalSingleRelationFactorizations_freeUniverse
    (F : _root_.SheafOfModules.{w} (commRingSheafToRingSheaf O))
    (hF : HasLocalSingleRelationFactorizations O F) : IsFlat F

Stacks.SheafOfModules.hasLocalSingleRelationFactorizations_iff_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatRelations.lean, line 280. The attribute's comment: “parts (2) and (3)”.

For a sheaf of modules on a ringed site, the single-relation and the finite-matrix forms of the local equational criterion for flatness are equivalent.

theorem hasLocalSingleRelationFactorizations_iff_finite
    (O : Sheaf J CommRingCat.{w}) (F : _root_.SheafOfModules.{w} (commRingSheafToRingSheaf O)) :
    HasLocalSingleRelationFactorizations O F ↔ HasLocalFiniteRelationFactorizations O F

Tag 08M4, a lemma

Tag 08M4 in the Stacks Project.

Stacks.SheafOfModules.FlatSquareZero.isFlat_iff_reduction_isFlat_and_multiplication_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatSquareZeroThickening.lean, line 2709.

Flatness over a square-zero thickening is equivalent to flatness of the reduction and injectivity of the canonical multiplication map from the kernel tensored with the reduction.

Here i identifies I with the kernel of f, nu is multiplication I ⊗[O'] F' ⟶ F', and q exhibits F as its cokernel. The last displayed formula identifies mu with the canonical map I ⊗[O] F ⟶ F'.

public theorem isFlat_iff_reduction_isFlat_and_multiplication_mono
    {O' O : Sheaf J CommRingCat.{w}} (f : O' ⟶ O)
    (hf : Presheaf.IsLocallySurjective J f.hom)
    (I : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf O))
    (F' : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf O'))
    (F : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf O))
    (i : (SheafOfModules.restrictScalars (ringMap f)).obj I ⟶
      SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf O'))
    (hi_zero : ∀ (U : Cᵒᵖ) (a : I.val.obj U),
      f.hom.app U (show O'.obj.obj U from i.val.app U a) = 0)
    (hi_univ : ∀ (U : Cᵒᵖ) (x : O'.obj.obj U), f.hom.app U x = 0 →
      ∃! a : I.val.obj U, (show O'.obj.obj U from i.val.app U a) = x)
    (hsq : ∀ (U : Cᵒᵖ) (a b : I.val.obj U),
      (show O'.obj.obj U from i.val.app U a) *
        (show O'.obj.obj U from i.val.app U b) = 0)
    (nu : (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} O').flip.obj F')).obj
        ((SheafOfModules.restrictScalars (ringMap f)).obj I) ⟶ F')
    (hnu : ∀ (U : Cᵒᵖ) (a : I.val.obj U) (x : F'.val.obj U),
      nu.val.app U
          (((PresheafOfModules.sheafificationAdjunction.{w, v, w, u} (R :=
              Stacks.SheafOfModules.Tensor.ringSheaf
              O')
        (𝟙 (Stacks.SheafOfModules.Tensor.ringSheaf O').obj)).unit.app
      (PresheafOfModules.tensorObj ((SheafOfModules.restrictScalars (ringMap f)).obj I).val
          F'.val)).app U
              (a ⊗ₜ[O'.obj.obj U] x)) =
        (show (Stacks.SheafOfModules.Tensor.ringSheaf O').obj.obj U from
          i.val.app U a) • x)
    (q : F' ⟶ (SheafOfModules.restrictScalars (ringMap f)).obj F)
    (hnuq : nu ≫ q = 0)
    (hq : IsColimit (CokernelCofork.ofπ q hnuq))
    (mu : (SheafOfModules.restrictScalars (ringMap f)).obj
        ((((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} O).flip.obj F)).obj I) ⟶ F')
    (hmu : ∀ (U : Cᵒᵖ) (a : I.val.obj U) (x : F'.val.obj U),
      mu.val.app U
          (((PresheafOfModules.sheafificationAdjunction.{w, v, w, u} (R :=
              Stacks.SheafOfModules.Tensor.ringSheaf
              O)
        (𝟙 (Stacks.SheafOfModules.Tensor.ringSheaf O).obj)).unit.app
      (PresheafOfModules.tensorObj I.val F.val)).app U
            (a ⊗ₜ[O.obj.obj U] q.val.app U x)) =
        (show (Stacks.SheafOfModules.Tensor.ringSheaf O').obj.obj U from
          i.val.app U a) • x) :
    AlgebraicGeometry.SheafOfModules.IsFlat F' ↔
      (AlgebraicGeometry.SheafOfModules.IsFlat F ∧ Mono mu)

Tag 0GLY, a lemma

Tag 0GLY in the Stacks Project.

Stacks.Sheaves.FlatNeighbourhood.isIso_tensorUnitMap_of_pow_smul_eq_zero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatNeighbourhoodTensorUnit.lean, line 724.

Stacks Project, Tag 0GLY. If a flat map of ring sheaves is an isomorphism modulo an ideal I, then extension of scalars is an isomorphism on every module annihilated by a power of I.

lemma isIso_tensorUnitMap_of_pow_smul_eq_zero
    {O O' : Sheaf J CommRingCat.{w}} (f : O ⟶ O')
    (hf : IsFlatMap f)
    {I : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf O)}
    (i : I ⟶ RingModule O) [Mono i]
    (hquot : ∃ q : cokernel i ⟶
        cokernel (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} O).flip.obj
            (RestrictedRingModule f)).map i),
      IsIso q ∧ cokernel.π i ≫ q = (tensorUnitMap f (RingModule O)).val ≫
        cokernel.π (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} O).flip.obj
            (RestrictedRingModule f)).map i))
    (F : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf O))
    (hF : ∃ n : ℕ, ∀ (X : Cᵒᵖ) (a : Fin n → I.val.obj X) (x : F.val.obj X),
      ((F.val.obj X).smul
        (show (Stacks.SheafOfModules.Tensor.ringSheaf O).obj.obj X from
          (Finset.univ.prod (fun k ↦ show O.obj.obj X from (i.val.app X) (a k)) :
            O.obj.obj X))).asHom x = 0) :
    IsIso (tensorUnitMap f F).val

Sources

• Section 18.28, Tag 03EQ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.IsFlat · Stacks.SheafOfModules.IsFlat · AlgebraicGeometry.SheafOfModules.PresheafOfModules.IsFlat · AlgebraicGeometry.SheafOfModules.PresheafOfModules.IsFlatMap · AlgebraicGeometry.SheafOfModules.IsFlat · AlgebraicGeometry.SheafOfModules.IsFlatMap · AlgebraicGeometry.SheafOfModules.PresheafOfModules.isFlat_of_objectwise_flat · Stacks.SheafOfModules.FlatSheafification.isFlat_sheafification

Section18.29 Duals#

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

Tag 0FNY, an example

Tag 0FNY in the Stacks Project.

Stacks.SheafOfModules.isIso_tensorDualToEndomorphism_of_localSummand, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftDualRingedSite.lean, line 194. The attribute's comment: “the map ℱ ⊗ 𝓗om(ℱ,𝒪) ⟶ 𝓗om(ℱ,ℱ) is an ISOMORPHISM, with the local hypothesis in the per-object form the tag states it in”. References: SGA 5 IIIB (5.0), “partial”.

Stacks Project, Tag 0FNY, first assertion. For a sheaf of modules which is locally a direct summand of a finite free sheaf of modules, the canonical map F ⊗_𝒪 SheafHom(F, 𝒪) ⟶ SheafHom(F, F) is an isomorphism.

The map is Stacks.SheafOfModules.tensorDualToEndomorphism, pinned down on local sections by Stacks.SheafOfModules.tensorDualToEndomorphism_toTensorSheafSection.

theorem isIso_tensorDualToEndomorphism_of_localSummand
    (hF : IsLocallyDirectSummandOfFiniteFree 𝒪 h𝒪 F) :
    IsIso (tensorDualToEndomorphism 𝒪 h𝒪 F)

Stacks.SheafOfModules.exactPairingDualSheafOfLocalSummand, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftDualRingedSite.lean, line 211. The attribute's comment: “the LEFT-DUAL assertion: 𝓗om(ℱ,𝒪) with the canonical coevaluation and evaluation satisfies the two triangle identities, with the local hypothesis in the per-object form the tag states it in”. References: SGA 5 IIIB (5.0), “5.0.3 iso”.

Stacks Project, Tag 0FNY, second assertion. For a sheaf of modules F which is locally a direct summand of a finite free sheaf of modules, the dual F^∨ = SheafHom(F, 𝒪), with the canonical coevaluation η : 𝒪 ⟶ F ⊗ F^∨ and the canonical evaluation ε : F^∨ ⊗ F ⟶ 𝒪, is a left dual of F in the monoidal category of sheaves of 𝒪-modules of Tag 01CA. That is, the two triangle identities hold.

noncomputable def exactPairingDualSheafOfLocalSummand
    (hF : IsLocallyDirectSummandOfFiniteFree 𝒪 h𝒪 F) :
    ExactPairing F (dualSheaf 𝒪 h𝒪 F)

Stacks.SheafOfModules.dualSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHom.lean, line 279. The attribute's comment: “the dual SheafHom(ℱ, 𝒪) whose left-dual property is the content of the tag; the construction is for an arbitrary site, so the ringed-space and the ringed-site tags name the same object”. References: SGA 3 III (0.6).

The dual of a sheaf of modules, F^∨ = SheafHom(F, 𝒪): the sheaf-hom into the structure sheaf.

noncomputable def dualSheaf
    (F : SheafOfModules.{max u v} (Stacks.SheafOfModules.TensorSheafification.structureSheaf 𝒪 h𝒪))
      :
    SheafOfModules.{max u v} (Stacks.SheafOfModules.TensorSheafification.structureSheaf 𝒪 h𝒪)

Stacks.SheafOfModules.evaluation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafHom.lean, line 696. The attribute's comment: “the evaluation map ε : ℱ^∨ ⊗ ℱ ⟶ 𝒪”.

The evaluation pairing of sheaves of modules, F^∨ ⊗_𝒪 F ⟶ 𝒪. The tensor product of sheaves of modules is the sheafification of the pointwise one (Tag 05NA), so this is the morphism which evaluationPresheaf induces through the sheafification adjunction.

noncomputable def evaluation
    (F : SheafOfModules.{max u v} (Stacks.SheafOfModules.TensorSheafification.structureSheaf 𝒪 h𝒪))
      :
    ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, max u v, max u v, max u v}
      ⟨𝒪, Presheaf.isSheaf_of_isSheaf_comp J 𝒪
        (forget₂ CommRingCat RingCat) h𝒪⟩).obj (dualSheaf 𝒪 h𝒪 F)).obj F ⟶
      SheafOfModules.unit (Stacks.SheafOfModules.TensorSheafification.structureSheaf 𝒪 h𝒪)

Stacks.SheafOfModules.tensorDualToEndomorphism_toTensorSheafSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorDualEndomorphism.lean, line 655. The attribute's comment: “the map ℱ ⊗ 𝓗om(ℱ,𝒪) ⟶ 𝓗om(ℱ,ℱ) read on sections, which pins it down”.

The canonical morphism on a local pure tensor is the rank-one operator. This pins the morphism down: its value on the image of f ⊗ lam is the endomorphism g ↦ lam(g) • f.

theorem tensorDualToEndomorphism_toTensorSheafSection
    (F : SheafOfModules.{max u v} (Stacks.SheafOfModules.TensorSheafification.structureSheaf 𝒪 h𝒪))
      (U : Cᵒᵖ)
    (f : F.val.obj U) (lam : (dualSheaf 𝒪 h𝒪 F).val.obj U) :
    ((tensorDualToEndomorphism 𝒪 h𝒪 F).val.app U).hom
        (toTensorSheafSection 𝒪 h𝒪 F (dualSheaf 𝒪 h𝒪 F) U
          (f ⊗ₜ[(Stacks.SheafOfModules.TensorSheafification.structureRingPresheaf 𝒪).obj U] lam)) =
      rankOneSection 𝒪 h𝒪 (U := U.unop) f lam

Tag 0FNZ, a lemma

Tag 0FNZ in the Stacks Project.

Stacks.SheafOfModules.dualSheafIsoOfLeftDual, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftDualSheafHomIso.lean, line 149. The attribute's comment: “(2), the isomorphism 𝓗om(ℱ,𝒪) ≅ 𝒢; that it is the map λ ↦ (λ ⊗ 1)(η) of the tag is dualSheafIsoOfLeftDual_hom_val_app”.

Stacks Project, Tag 0FNZ (2). A left dual G of a sheaf of 𝒪-modules F on a ringed site is isomorphic to SheafHom(F, 𝒪).

Both SheafHom(F, 𝒪) and G are left duals of F — the first by exactPairingDualSheafOfLeftDual — and two left duals of one object are isomorphic through the adjoint mate of the identity. That this isomorphism is the map Tag 0FNZ (2) names, namely λ ↦ (λ ⊗ 1)(η), is dualSheafIsoOfLeftDual_hom_val_app.

noncomputable def dualSheafIsoOfLeftDual : dualSheaf 𝒪 h𝒪 F ≅ G

Stacks.SheafOfModules.dualSheafIsoOfLeftDual_hom_val_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftDualSheafHomIso.lean, line 210. The attribute's comment: “(2), that the isomorphism is the map λ ↦ (λ ⊗ 1)(η) the tag describes”.

Stacks Project, Tag 0FNZ (2), the formula for the isomorphism. On an object U over which the coevaluation expands as η(1) = ∑ fᵢ ⊗ gᵢ, the isomorphism SheafHom(F, 𝒪) ≅ G of Tag 0FNZ (2) sends a local section λ to ∑ λ(fᵢ) • gᵢ, which is (λ ⊗ 1)(η). In particular that expression does not depend on the chosen expansion.

Such an expansion exists on a covering of every object of the site, by Stacks.SheafOfModules.exists_cover_localDualBasis_tensorSheaf, so these formulas determine the isomorphism.

theorem dualSheafIsoOfLeftDual_hom_val_app (U : C) {n : ℕ}
    (f : Fin n → F.val.obj (op U)) (g : Fin n → G.val.obj (op U))
    (hη : (η_ F G).val.app (op U)
        (1 : (TensorSheafification.structureSheaf 𝒪 h𝒪).obj.obj (op U)) =
      ∑ i, tensorPt 𝒪 h𝒪 F G (op U) (f i) (g i))
    (lam : (dualSheaf 𝒪 h𝒪 F).val.obj (op U)) :
    (dualSheafIsoOfLeftDual 𝒪 h𝒪 F G).hom.val.app (op U) lam =
      ∑ i, dualEval lam (f i) • g i

Stacks.SheafOfModules.evaluation_eq_dualEval_dualSheafIsoOfLeftDual_inv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LeftDualSheafHomIso.lean, line 254. The attribute's comment: “(3), the evaluation formula ε(f, g) = e⁻¹(g)(f)”.

Stacks Project, Tag 0FNZ (3). Pairing a local section g of a left dual G of F against a local section f of F under the given evaluation ε is the value at f of the local homomorphism e⁻¹(g) : F ⟶ 𝒪, where e is the isomorphism of Tag 0FNZ (2).

theorem evaluation_eq_dualEval_dualSheafIsoOfLeftDual_inv (U : C)
    (y : G.val.obj (op U)) (x : F.val.obj (op U)) :
    (ε_ F G).val.app (op U) (tensorPt 𝒪 h𝒪 G F (op U) y x) =
      dualEval ((dualSheafIsoOfLeftDual 𝒪 h𝒪 F G).inv.val.app (op U) y) x

Stacks.SheafOfModules.exists_cover_retract_finiteFree_of_exactPairing_tensorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorAssociatorSections.lean, line 329. The attribute's comment: “local_finite_free_summand”.

Let (C, O) be a ringed site and let F be a sheaf of O-modules with a left dual G for the monoidal structure given by the tensor product sheaf. Then every object U of the site has a covering on whose members F restricts to a direct summand of a finite free module.

theorem exists_cover_retract_finiteFree_of_exactPairing_tensorSheaf
    [HasSheafify J AddCommGrpCat.{w}]
    [∀ V : C, HasWeakSheafify (J.over V) AddCommGrpCat.{w}]
    [∀ V : C, (J.over V).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (p : ExactPairing F G) (U : C) :
    ∃ S : Sieve U, S ∈ J U ∧
      ∀ (V : C) (i : V ⟶ U), S i →
        ∃ I : Type w, Finite I ∧
          Nonempty (Retract (F.over V)
            (SheafOfModules.free (R := (Stacks.SheafOfModules.TensorSheafification.structureSheaf O
              hO).over V) I))

AlgebraicGeometry.Space.exists_cover_retract_finiteFree_of_exactPairing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleLeftDualLocalSummand.lean, line 88. The attribute's comment: “(1), for the modules of an algebraic space”.

Stacks 0FNZ (1) for the 𝒪_F-modules of an algebraic space. If an 𝒪_F-module M has a left dual N in the monoidal category of 𝒪_F-modules, then every object U of the small étale site of F has a covering on whose members M restricts to a direct summand of a free module on a finite index type.

theorem exists_cover_retract_finiteFree_of_exactPairing
    (M N : Modules.{u, u} B S hS F hF) (p : ExactPairing M N)
    (U : (smallEtaleRingedSite B S hS F hF).C) :
    ∃ T : Sieve U, T ∈ (smallEtaleRingedSite B S hS F hF).J U ∧
      ∀ (V : (smallEtaleRingedSite B S hS F hF).C) (i : V ⟶ U), T i →
        ∃ I : Type u, Finite I ∧
          Nonempty (Retract (M.over V)
            (SheafOfModules.free (R := (Stacks.SheafOfModules.Tensor.ringSheaf
              (smallEtaleRingedSite B S hS F hF).O).over V) I))

Tag 08FD, a lemma

Tag 08FD in the Stacks Project.

Stacks.SheafOfModules.exists_coveringSieve_retract_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatFiniteFreeSummand.lean, line 685.

On a ringed site, a sheaf of modules which is flat and locally of finite presentation is, locally on the site, a direct summand of a finite free sheaf of modules: every object U carries a covering sieve on each member f : V ⟶ U of which F|_V is a retract of O_V^{⊕ I} for some finite I.

theorem exists_coveringSieve_retract_free
    {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
    [J.HasSheafCompose (forget₂ CommRingCat.{max v w} RingCat.{max v w})]
    [HasWeakSheafify J AddCommGrpCat.{max v w}]
    [J.WEqualsLocallyBijective AddCommGrpCat.{max v w}]
    [∀ T : C, HasWeakSheafify (J.over T) AddCommGrpCat.{max v w}]
    [∀ T : C, (J.over T).WEqualsLocallyBijective AddCommGrpCat.{max v w}]
    (O : Sheaf J CommRingCat.{max v w})
    (F : _root_.SheafOfModules.{max v w} (commRingSheafToRingSheaf O))
    [F.IsFinitePresentation] (hF : IsFlat F) (U : C) :
    ∃ S : Sieve U, S ∈ J U ∧ ∀ {V : C} (f : V ⟶ U), S f →
      ∃ I : Type (max v w), Finite I ∧
        ∃ (i : F.over V ⟶ _root_.SheafOfModules.free
            (R := (commRingSheafToRingSheaf O).over V) I)
          (r : _root_.SheafOfModules.free (R := (commRingSheafToRingSheaf O).over V) I ⟶
            F.over V), i ≫ r = 𝟙 (F.over V)

Sources

• Section 18.29, Tag 0FNX
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.isIso_tensorDualToEndomorphism_of_localSummand · Stacks.SheafOfModules.exactPairingDualSheafOfLocalSummand · Stacks.SheafOfModules.dualSheaf · Stacks.SheafOfModules.evaluation · Stacks.SheafOfModules.tensorDualToEndomorphism_toTensorSheafSection · Stacks.SheafOfModules.dualSheafIsoOfLeftDual · Stacks.SheafOfModules.dualSheafIsoOfLeftDual_hom_val_app · Stacks.SheafOfModules.evaluation_eq_dualEval_dualSheafIsoOfLeftDual_inv

Section18.30 Towards constructible modules#

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

Tag 0934, a lemma

Tag 0934 in the Stacks Project.

Stacks.SheafOfModules.cechShortComplex_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExtensionByZeroCech.lean, line 278. The attribute's comment: “exactness in the middle, i.e. the relations among the generators j_{U_i!} O_{U_i} of j_{U!} O_U are generated by the fibre products”.

Stacks Project, Tag 0934, exactness in the middle. For a covering family {U_i → U} with existing pairwise fibre products, the Čech sequence ⊕_{i, j} j_{U_i ×_U U_j!} O_{U_i ×_U U_j} ⟶ ⊕_i j_{U_i!} O_{U_i} ⟶ j_{U!} O_U is exact at ⊕_i j_{U_i!} O_{U_i}.

theorem cechShortComplex_exact (h𝒰 : 𝒰.sieve₀ ∈ J U) :
    (cechShortComplex.{u₁, v₁, w, t} R 𝒰).Exact

Stacks.SheafOfModules.epi_cechShortComplex_g, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExtensionByZeroCech.lean, line 288. The attribute's comment: “exactness at j_{U!} O_U, i.e. the right-hand map is an epimorphism”.

Stacks Project, Tag 0934, exactness at j_{U!} O_U. This is Stacks.SheafOfModules.epi_sigmaDesc_extensionByZeroUnitMap — the surjectivity half of Stacks 0G1W, which needs neither the fibre products nor quasi-compactness — read off the Čech short complex.

theorem epi_cechShortComplex_g (h𝒰 : 𝒰.sieve₀ ∈ J U) :
    Epi (cechShortComplex.{u₁, v₁, w, t} R 𝒰).g

Tag 0G1W, a lemma

Tag 0G1W in the Stacks Project.

Stacks.SheafOfModules.exists_finite_restrictIndex_cechShortComplex_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExtensionByZeroCech.lean, line 311. The attribute's comment: “the middle exactness: a finite subfamily of a covering of a quasi-compact object already has exact Čech sequence”.

Stacks Project, Tag 0G1W, the middle exactness half. If U is a quasi-compact object and {U_i → U}_{i ∈ I} is a covering family whose pairwise fibre products exist, then there is a finite subset I' ⊆ I for which the Čech sequence of the subfamily {U_i → U}_{i ∈ I'} is exact in the middle as well as at j_{U!} O_U.

Quasi-compactness is used only through Stacks.SheafOfModules.QuasiCompact.exists_finite_restrictIndex_sieve₀_mem: a covering family of a quasi-compact object has a finite subfamily which is still a covering, and Stacks 0934 applies to that subfamily directly.

theorem exists_finite_restrictIndex_cechShortComplex_exact
    (hU : J.IsQuasiCompactObject U) (𝒰 : PreZeroHypercover.{max u₁ v₁} U)
    (h𝒰 : 𝒰.sieve₀ ∈ J U) [hpb𝒰 : ∀ i j, HasPullback (𝒰.f i) (𝒰.f j)] :
    ∃ T : Set 𝒰.I₀, T.Finite ∧
      (cechShortComplex.{u₁, v₁, w, t} R (𝒰.restrictIndex (Subtype.val : T → 𝒰.I₀))
          (hpb := fun _ _ ↦ hpb𝒰 _ _)).Exact ∧
        Epi (cechShortComplex.{u₁, v₁, w, t} R (𝒰.restrictIndex (Subtype.val : T → 𝒰.I₀))
          (hpb := fun _ _ ↦ hpb𝒰 _ _)).g

Stacks.SheafOfModules.exists_finite_epi_sigmaDesc_extensionByZeroUnitMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExtensionByZeroQuasiCompact.lean, line 184. The attribute's comment: “the surjectivity half: a finite subfamily of a covering of a quasi-compact object already gives an epimorphism onto the extension by zero”.

Stacks Project, Tag 0G1W, the surjectivity half. If U is a quasi-compact object of a ringed site and {U_i → U}_{i ∈ I} is a covering of U, then there is a finite subset I' ⊆ I for which ⊕_{i ∈ I'} j_{U_i!} O_{U_i} ⟶ j_{U!} O_U is already an epimorphism, i.e. the sequence of the source is exact at j_{U!} O_U.

theorem exists_finite_epi_sigmaDesc_extensionByZeroUnitMap {U : C}
    (hU : J.IsQuasiCompactObject U) (𝒰 : PreZeroHypercover.{max u₁ v₁} U)
    (h𝒰 : 𝒰.sieve₀ ∈ J U) :
    ∃ T : Set 𝒰.I₀, T.Finite ∧
      Epi (Sigma.desc fun i : T => extensionByZeroUnitMap.{u₁, v₁, w, t} R (𝒰.f i.1))

Tag 0935, a lemma

Tag 0935 in the Stacks Project.

Stacks.Sites.sheafOfModules_sections_preserves_coproducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/ModuleSections.lean, line 309. The attribute's comment: “part (2)”. References: EGA IV (16.8.11), “(i), special case”.

Stacks 0935, part (2). For a sheaf of rings, sections of sheaves of modules over a quasi-compact object preserve arbitrary direct sums.

theorem sheafOfModules_sections_preserves_coproducts
    {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
    (R : Sheaf J RingCat.{r}) (W : C) (hW : J.IsQuasiCompactObject W) (ι : Type w) :
    PreservesColimitsOfShape (Discrete ι)
      (SheafOfModules.toSheaf.{s} R ⋙
        (sheafSections J AddCommGrpCat.{s}).obj (op W))

Stacks.Sites.isColimitSectionsFiniteSubcoproductsCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/SetCoproductSections.lean, line 136. The attribute's comment: “part (1), the assertion the source's proof establishes: sections over a quasi-compact object carry the presentation of an arbitrary coproduct of sheaves of sets as the filtered colimit of its finite sub-coproducts to a colimit of sets. The source's part (1), that sections commute with coproducts, is false as stated; see the module documentation.”.

Stacks 0935, the content of the proof of part (1). Let W be a quasi-compact object of a site and let f be a family of sheaves of sets. Sections over W carry the presentation of ∐ f as the filtered colimit of its finite sub-coproducts to a colimit of sets: the sections over W of ∐_{i ∈ I} f i are the filtered colimit, over the finite subsets E ⊆ I, of the sections over W of ∐_{i ∈ E} f i.

This is the whole of the source's argument for part (1). Part (1) itself, that sections over W commute with coproducts, is false as stated; see the module documentation and not_preservesColimitsOfShape_pempty_of_bot_mem.

noncomputable def isColimitSectionsFiniteSubcoproductsCocone (J : GrothendieckTopology C)
    (W : C) (hW : J.IsQuasiCompactObject W) {ι : Type max u v}
    (f : ι → Sheaf J (Type max u v)) :
    IsColimit (((sheafSections J (Type max u v)).obj (op W)).mapCocone
      (finiteSubcoproductsCocone f))

Stacks.Sites.bijective_colimit_post_sheafSections_of_isQuasiCompactObject_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/SetCoproductSections.lean, line 168. The attribute's comment: “part (1), CORRECTED per the approved erratum: evaluation at a quasi-compact object carries a filtered colimit with monomorphic transition maps to a colimit of sets, which is Stacks 0738 part (3). The source's part (1), that sections commute with arbitrary coproducts, is false; the counterexamples are preserved in this module's documentation and in not_preservesColimitsOfShape_pempty_of_bot_mem.”.

Stacks 0935, part (1), corrected. Evaluation of sheaves of sets at a quasi-compact object carries a filtered colimit whose transition maps are monomorphisms to a colimit of sets: the canonical map colim_i F_i(U) ⟶ (colim_i F_i)(U) is bijective.

This is the approved erratum for part (1). The source's part (1) — that sections over a quasi-compact object commute with arbitrary coproducts — is false; the counterexamples are in this module's documentation and not_preservesColimitsOfShape_pempty_of_bot_mem. The corrected statement is Stacks 0738 part (3), so this is an exact wrapper of that theorem's third conjunct and introduces no new machinery.

isColimitSectionsFiniteSubcoproductsCocone below is this statement specialized to the filtered diagram of finite sub-coproducts, whose transition maps are monomorphisms; that specialization alone does not state the corrected part (1), which is why it is registered separately.

theorem bijective_colimit_post_sheafSections_of_isQuasiCompactObject_of_mono
    (J : GrothendieckTopology C) {I : Type w₁} [Category.{w₂} I] [IsFiltered I]
    [HasColimitsOfShape I (Type max u v)] (F : I ⥤ Sheaf J (Type max u v)) (U : C)
    (hU : J.IsQuasiCompactObject U)
    (hmono : ∀ (i j : I) (f : i ⟶ j), Mono (F.map f)) :
    Function.Bijective (colimit.post F ((sheafSections J (Type max u v)).obj (op U)))

Tag 0936, a lemma

Tag 0936 in the Stacks Project.

Stacks.Sites.homFromExtensionByZeroUnit_preservesCoproducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/ExtensionByZeroCompactObject.lean, line 113.

Stacks 0936. On a ringed site, morphisms out of the extension by zero of the structure sheaf of the slice site over a quasi-compact object commute with arbitrary direct sums.

theorem homFromExtensionByZeroUnit_preservesCoproducts
    (hU : X.J.IsQuasiCompactObject U) (ι : Type w) :
    PreservesColimitsOfShape (Discrete ι)
      (preadditiveCoyoneda.obj (op
        ((SheafOfModules.pullback.{u}
          (F := Over.forget U)
          (𝟙 (((Stacks.SheafOfModules.Tensor.ringSheaf X.O)).over U) :
            (((Stacks.SheafOfModules.Tensor.ringSheaf X.O)).over U) ⟶
              (((Stacks.SheafOfModules.Tensor.ringSheaf X.O)).over U))).obj
            (SheafOfModules.unit
              (((Stacks.SheafOfModules.Tensor.ringSheaf X.O)).over U)))))

Tag 0937, a situation

Tag 0937 in the Stacks Project.

Stacks.Sites.QuasiCompactObjectsSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/ObjectsSituation.lean, line 51. The attribute's comment: “the standing data”.

A site together with a distinguished collection of its objects. This is the standing data of the Stacks Project's discussion of presentations of sheaves of modules.

structure QuasiCompactObjectsSituation (C : Type u) [Category.{v} C]

Stacks.Sites.QuasiCompactObjectsSituation.HasEnoughObjects, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/ObjectsSituation.lean, line 64. The attribute's comment: “condition (1)”.

Condition (1): every object of the site has a covering family all of whose members belong to the distinguished collection.

def HasEnoughObjects (S : QuasiCompactObjectsSituation C) : Prop

Stacks.Sites.QuasiCompactObjectsSituation.ObjectsAreQuasiCompact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/ObjectsSituation.lean, line 70. The attribute's comment: “condition (2)”.

Condition (2): every object of the distinguished collection is quasi-compact.

def ObjectsAreQuasiCompact (S : QuasiCompactObjectsSituation C) : Prop

Stacks.Sites.QuasiCompactObjectsSituation.CoverPullbacksAreQuasiCompact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/ObjectsSituation.lean, line 76. The attribute's comment: “condition (3)”.

Condition (3): for a covering family of a distinguished object whose members are distinguished, every pairwise fibre product exists and is quasi-compact.

def CoverPullbacksAreQuasiCompact (S : QuasiCompactObjectsSituation C) : Prop

Stacks.QuasiCompactObjectsSituation.CoverPullbacksAreQuasiCompact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Spectral/CompactBasisColimit.lean, line 130. The attribute's comment: “condition (3)”.

Condition (3) of Stacks Project, Tag 0937: for a cover whose source objects and target belong to the distinguished collection, every pairwise fibre product is quasi-compact.

The HasPullback conjunct records the existence implicit in the source. The second conjunct is quantified over the instance used to choose a pullback, so the condition does not depend on a global choice of pullbacks.

def QuasiCompactObjectsSituation.CoverPullbacksAreQuasiCompact {C : Type u} [Category.{v} C]
    (S : QuasiCompactObjectsSituation C) : Prop

Tag 093B, a lemma

Tag 093B in the Stacks Project.

AlgebraicGeometry.exists_epi_sigma_moduleShriekConstant_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleSheafGenerationByQCQS.lean, line 196. The attribute's comment: “part (2), sheaves of modules, generation by qcqs étale objects”.

Stacks 093B part (2) for sheaves of Λ-modules on the small étale site. Every sheaf of Λ-modules on the small étale site of a scheme X is a quotient of a direct sum ⊕ j_{U_a!}\underline{\Lambda}_{U_a} of extensions by zero of constant free rank-one module sheaves at quasi-compact quasi-separated étale objects U_a of X.

The source takes the objects of the direct sum from a collection which covers the site and consists of quasi-compact objects; on the small étale site that collection is the quasi-compact quasi-separated étale objects, which cover every étale object by AlgebraicGeometry.SmallEtale.hasEnoughObjects_quasiCompactObjectsSituation. Maps out of j_{U!}\underline{\Lambda}_U are sections over U by AlgebraicGeometry.moduleShriekConstantCoyonedaIso, so the index set is the pairs of a quasi-compact quasi-separated étale object and a section of the sheaf over it.

This strengthens AlgebraicGeometry.epi_desc_moduleShriekConstant, whose direct sum runs over all étale objects, and it is the generation step of Stacks 093C for sheaves of modules: compactness of the generators, AlgebraicGeometry.isFinitelyPresentable_moduleShriekConstant, is available exactly at the quasi-compact objects.

public theorem exists_epi_sigma_moduleShriekConstant_qcqs (B : BigEtaleSite.{u}) (X : B.Scheme)
    (Λ : Type r) [CommRing Λ]
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{max (u + 1) r} Λ)) :
    ∃ (A : Type max (u + 1) r) (U : A → SmallEtale B X.1 X.property),
      (∀ a, IsQCQSEtaleObject B X (U a)) ∧
        ∃ p : (∐ fun a => moduleShriekConstant.{u, r, r} B X Λ (U a)) ⟶ F, Epi p

AlgebraicGeometry.exists_epi_sigma_moduleShriekConstant_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleShriekFiniteGeneration.lean, line 559. The attribute's comment: “part (2), sheaves of modules, generation by affine étale objects”.

Stacks 093B part (2) for sheaves of Λ-modules, generation by affine étale objects. Every sheaf of Λ-modules on the small étale site of X is a quotient of a direct sum ⊕ j_{U_a!}\underline{\Lambda}_{U_a} of extensions by zero of constant free rank-one module sheaves at affine étale objects U_a of X.

This is AlgebraicGeometry.exists_epi_sigma_moduleShriekConstant_qcqs with the distinguished collection of the source taken to be the affine étale objects rather than the quasi-compact quasi-separated ones; they cover every étale object just as well.

public theorem exists_epi_sigma_moduleShriekConstant_affine
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{max (u + 1) r} Λ)) :
    ∃ (A : Type max (u + 1) r) (U : A → SmallEtale B X.1 X.property),
      (∀ a, SmallEtale.IsAffine B X.1 X.property (U a)) ∧
        ∃ p : (∐ fun a => moduleShriekConstant.{u, r, r} B X Λ (U a)) ⟶ F, Epi p

Stacks.Sites.exists_epi_coproduct_extensionByZeroUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/ModulePresentationColimits.lean, line 296. The attribute's comment: “part (2), modules”.

Stacks Project, Tag 093B (2). Every sheaf of R-modules is a quotient of a direct sum ⊕ j_{U_i!} R|_{U_i} of extensions by zero of the restricted structure sheaf at distinguished objects: one summand for each pair of a distinguished object and a section of the module over it. This is the generation step on which the presentations of Tag 093C rest.

theorem exists_epi_coproduct_extensionByZeroUnit
    (S : QuasiCompactObjectsSituation C) (hEnough : S.HasEnoughObjects)
    (R : Sheaf S.topology RingCat.{w}) (M : SheafOfModules.{max u₁ v₁ w v} R) :
    ∃ (A : Type (max u₁ v₁ w v)) (U : A → C), (∀ i, U i ∈ S.objects) ∧
      ∃ p : (∐ fun i => extensionByZeroUnit.{u₁, v₁, w, v} R (U i)) ⟶ M, Epi p

Stacks.exists_epi_coproduct_sheafifiedYoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Spectral/CompactBasisColimit.lean, line 145. The attribute's comment: “part (1), sheaves of sets”.

Stacks Project, Tag 093B (1). Every sheaf of sets is covered by a coproduct of sheafified representables from the distinguished collection: it is the target of a surjective map whose source is a coproduct of the sheaves h_{U_i}^# with U_i distinguished.

theorem exists_epi_coproduct_sheafifiedYoneda
    {C : Type u} [Category.{v} C]
    (S : QuasiCompactObjectsSituation C)
    (hEnough : S.HasEnoughObjects) (F : Sheaf S.topology (Type max u v)) :
    letI : HasColimitsOfSize.{max u v, max u v}
        (Sheaf S.topology (Type max u v)) := CategoryTheory.Sheaf.instHasColimitsOfSize
    ∃ (I : Type max u v) (U : I → C),
      (∀ i, U i ∈ S.objects) ∧
        ∃ (f : (∐ fun i ↦ (Sheaf.sheafifiedYoneda S.topology).obj (U i)) ⟶ F),
          Epi f

Tag 093C, a lemma

Tag 093C in the Stacks Project.

AlgebraicGeometry.moduleSheavesAreFilteredColimitsOfPresentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleSheafPresentationColimits.lean, line 366. The attribute's comment: “part (2), sheaves of modules on the small étale site, shriek spelling”.

Stacks 093C for sheaves of Λ-modules on the small étale site. Every sheaf of Λ-modules on the small étale site of a scheme X is a filtered colimit of sheaves carrying a finite shriek presentation by quasi-compact quasi-separated étale objects, that is, of cokernels of maps between finite direct sums of the sheaves j_{U!}\underline{\Lambda}_U at such objects.

This is the source's own proof. Two applications of Stacks 093B part (2), AlgebraicGeometry.exists_epi_sigma_moduleShriekConstant_qcqs, write F as the cokernel of a map g between two direct sums of the sheaves j_{U!}\underline{\Lambda}_U at quasi-compact quasi-separated étale objects: the first gives an epimorphism p onto F, the second an epimorphism q onto the kernel of p, and q ≫ ker p has cokernel F. Those generators are compact, by AlgebraicGeometry.isFinitelyPresentable_moduleShriekConstant together with AlgebraicGeometry.SmallEtale.hasFiniteQuasiCompactCoverings, so g restricts to maps between finite subsums; and the cokernels of those restrictions form a filtered diagram with colimit the cokernel of g, which is CategoryTheory.Limits.exists_isFilteredColimit_cokernel_finiteSubcoproducts.

The quasi-compactness and quasi-separatedness of X are used only for the compactness of the generators, which asks for AlgebraicGeometry.SmallEtale.hasFiniteQuasiCompactCoverings; the generation step itself needs neither. This discharges the hypothesis h093C of AlgebraicGeometry.exists_isFilteredColimit_isConstructibleModuleSheaf, Stacks 03SA (3), which carries the same two assumptions on X.

Stacks Tag 093C part (2) is stated for an arbitrary situation of Stacks 0937 and an arbitrary sheaf of rings by Stacks.Sites.isFilteredColimit_of_hasEnoughQuasiCompactObjects, which carries the tag; this is that statement at the small étale site with constant coefficients Λ, in the shriek spelling the étale development consumes.

public theorem moduleSheavesAreFilteredColimitsOfPresentations :
    ModuleSheavesAreFilteredColimitsOfPresentations B X Λ

AlgebraicGeometry.setSheavesAreFilteredColimitsOfPresentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/SetSheafPresentationColimits.lean, line 104. The attribute's comment: “part (1), sheaves of sets, étale site”.

Stacks 093C (1) for the small étale site. Every sheaf of sets on the small étale site of X is a filtered colimit of sheaves which are coequalizers of a pair of maps between finite coproducts of sheaves represented by quasi-compact quasi-separated étale objects of X.

This is the hypothesis h093C of AlgebraicGeometry.exists_isFilteredColimit_isConstructibleSetSheaf, Stacks 03SA (1). It is the specialisation to the collection of quasi-compact quasi-separated étale objects of Stacks.isFilteredColimit_of_hasEnoughQuasiCompactObjects, which states Stacks Tag 093C part (1) for an arbitrary situation and carries the tag.

public theorem setSheavesAreFilteredColimitsOfPresentations :
    SetSheavesAreFilteredColimitsOfPresentations B X

Stacks.Sites.isFilteredColimit_of_hasEnoughQuasiCompactObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/ModulePresentationColimits.lean, line 627. The attribute's comment: “modules”.

Stacks Project, Tag 093C (modules). Every module sheaf is a filtered colimit of finite cokernel presentations by extensions by zero from distinguished objects.

theorem isFilteredColimit_of_hasEnoughQuasiCompactObjects
    (S : QuasiCompactObjectsSituation C)
    (hEnough : S.HasEnoughObjects) (hqc : S.ObjectsAreQuasiCompact)
    (R : Sheaf S.topology RingCat.{w}) (F : SheafOfModules.{v} R) :
    ∃ (I : Type (max u₁ v₁ w v)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ SheafOfModules.{max u₁ v₁ w v} R)
      (ι : D ⟶ (Functor.const I).obj ((moduleULift.{max u₁ v₁ w v} R).obj F)),
      Nonempty (IsColimit (Cocone.mk ((moduleULift.{max u₁ v₁ w v} R).obj F) ι)) ∧
        ∀ i, HasFiniteExtensionByZeroPresentation S R (D.obj i)

Stacks.isFilteredColimit_of_hasEnoughQuasiCompactObjects, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Spectral/CompactBasisColimit.lean, line 804. The attribute's comment: “part (1), sheaves of sets”.

Stacks Project, Tag 093C (1). Under conditions (1) and (2) of Situation 0937, every sheaf of sets is a filtered colimit of coequalizers between finite coproducts of sheafified representables of distinguished objects.

theorem isFilteredColimit_of_hasEnoughQuasiCompactObjects
    (S : QuasiCompactObjectsSituation C)
    (hEnough : S.HasEnoughObjects) (hqc : S.ObjectsAreQuasiCompact)
    (F : Sheaf S.topology (Type max u v)) :
    ∃ (I : Type max u v) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf S.topology (Type max u v))
      (ι : D ⟶ (Functor.const I).obj F),
      ∃ (_ : IsColimit (Cocone.mk F ι)),
        ∀ i, HasFiniteRepresentableCoequalizerPresentation S (D.obj i)

Tag 093D, an equation

Tag 093D in the Stacks Project.

Stacks.SheafOfModules.HasFiniteExtensionByZeroPresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FiniteExtensionByZeroPresentation.lean, line 232. The attribute's comment: “the modules of Equation 18.30.7.2”.

Stacks Project, Equation 18.30.7.2 (Tag 093D). A sheaf of R-modules has a finite presentation by extensions by zero if it is isomorphic to the cokernel of a morphism between two finite direct sums of extensions by zero j_{U!} O_U of the structure sheaf at distinguished objects U.

def HasFiniteExtensionByZeroPresentation.{u₁', v₁', w', t'} {C : Type u₁'} [Category.{v₁'} C]
    (S : QuasiCompactObjectsSituation C) (R : Sheaf S.topology RingCat.{w'})
    (G : SheafOfModules.{max u₁' v₁' w' t'} R) : Prop

Stacks.Sites.HasFiniteExtensionByZeroPresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/QuasiCompact/ModulePresentationColimits.lean, line 586. The attribute's comment: “the modules of Equation 18.30.7.2, after the canonical universe lift”.

A finite presentation as a cokernel between finite coproducts of extensions by zero of the structure sheaf restricted to distinguished objects. All comparisons take place after the canonical universe lift; no size assumption is imposed on G.

def HasFiniteExtensionByZeroPresentation
    (S : QuasiCompactObjectsSituation C)
    (R : Sheaf S.topology RingCat.{w}) (G : SheafOfModules.{v} R) : Prop

Tag 093E, a lemma

Tag 093E in the Stacks Project.

Stacks.SheafOfModules.hasFiniteExtensionByZeroPresentation_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FiniteExtensionByZeroPresentation.lean, line 460.

Stacks Project, Tag 093E. On a site with a distinguished collection of objects which covers every object and consists of quasi-compact objects, the cokernel of a morphism between two sheaves of modules with finite presentations by extensions by zero again has a finite presentation by extensions by zero.

theorem hasFiniteExtensionByZeroPresentation_cokernel (hEnough : S.HasEnoughObjects)
    (hqc : S.ObjectsAreQuasiCompact) {F G : SheafOfModules.{max u₁ v₁ w t} R} (f : F ⟶ G)
    (hF : HasFiniteExtensionByZeroPresentation.{u₁, v₁, w, t} S R F)
    (hG : HasFiniteExtensionByZeroPresentation.{u₁, v₁, w, t} S R G) :
    HasFiniteExtensionByZeroPresentation.{u₁, v₁, w, t} S R (cokernel f)

Tag 093F, a lemma

Tag 093F in the Stacks Project.

Stacks.SheafOfModules.exists_finite_refinement_isIso_cokernelMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExtensionByZeroRefinePresentation.lean, line 512.

Stacks Project, Tag 093F. A finite presentation by extensions by zero can be changed along coverings of its target generators without changing its cokernel: finite subfamilies K'_i of the given coverings and a finite family {W_l} of distinguished objects can be chosen so that the resulting square over f induces an isomorphism on the cokernels of its horizontal maps.

theorem exists_finite_refinement_isIso_cokernelMap
    (hEnough : S.HasEnoughObjects) (hqc : S.ObjectsAreQuasiCompact)
    (hqs : S.CoverPullbacksAreQuasiCompact)
    {n m : ℕ} {U : Fin n → C} (V : Fin m → C)
    (hU : ∀ i, U i ∈ S.objects) (hV : ∀ j, V j ∈ S.objects)
    (𝒰 : ∀ i, PreZeroHypercover.{max u₁ v₁} (U i))
    (h𝒰 : ∀ i, (𝒰 i).sieve₀ ∈ S.topology (U i))
    (h𝒰obj : ∀ i k, (𝒰 i).X k ∈ S.objects)
    (f : (∐ fun j ↦ extensionByZeroUnit.{u₁, v₁, w, t} R (V j)) ⟶
      ∐ fun i ↦ extensionByZeroUnit.{u₁, v₁, w, t} R (U i)) :
    ∃ (T : ∀ i, Set (𝒰 i).I₀) (𝒱 : ∀ i, PreZeroHypercover.{max u₁ v₁} (U i)),
      (∀ i, (T i).Finite) ∧
        (∀ i, 𝒱 i = (𝒰 i).restrictIndex (Subtype.val : T i → (𝒰 i).I₀)) ∧
        (∀ i, (𝒱 i).sieve₀ ∈ S.topology (U i)) ∧
        ∃ (L : Type (max u₁ v₁)) (_ : Finite L) (W : L → C), (∀ l, W l ∈ S.objects) ∧
          ∃ (g : (∐ fun l ↦ extensionByZeroUnit.{u₁, v₁, w, t} R (W l)) ⟶
                ∐ fun x : Σ i, (𝒱 i).I₀ ↦ extensionByZeroUnit.{u₁, v₁, w, t} R ((𝒱 x.1).X x.2))
              (p : (∐ fun l ↦ extensionByZeroUnit.{u₁, v₁, w, t} R (W l)) ⟶
                ∐ fun j ↦ extensionByZeroUnit.{u₁, v₁, w, t} R (V j)),
            g ≫ refinementAugmentation.{u₁, v₁, w, t} R 𝒱 = p ≫ f ∧
              Epi (refinementAugmentation.{u₁, v₁, w, t} R 𝒱) ∧
              ∀ h : g ≫ refinementAugmentation.{u₁, v₁, w, t} R 𝒱 = p ≫ f,
                IsIso (cokernel.map g f p (refinementAugmentation.{u₁, v₁, w, t} R 𝒱) h)

Tag 093G, a lemma

Tag 093G in the Stacks Project.

Stacks.SheafOfModules.hasFiniteExtensionByZeroPresentation_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExtensionByZeroExtension.lean, line 659.

Stacks Project, Tag 093G. On a site with a distinguished collection of objects which covers every object, consists of quasi-compact objects and whose coverings have quasi-compact pairwise fibre products, the sheaves of modules with a finite presentation by extensions by zero are stable under extensions: if E is a short exact sequence of sheaves of modules whose outer terms have such presentations, so does its middle term.

This is Stacks' own argument. Choose presentations ⊕A_{V_j} ⟶ ⊕A_{U_i} ⟶ F₁ ⟶ 0 and ⊕A_{T_j} ⟶ ⊕A_{W_i} ⟶ F₃ ⟶ 0. Since F₂ ⟶ F₃ is an epimorphism, each generator A_{W_i} lifts to F₂ after passing to a covering of W_i by distinguished objects (Stacks.SheafOfModules.exists_hypercover_lift_extensionByZeroUnit), and Stacks 093F (Stacks.SheafOfModules.exists_finite_refinement_isIso_cokernelMap) replaces the W_i by a finite subfamily of that covering without changing the cokernel. The rest is Stacks.SheafOfModules.hasFiniteExtensionByZeroPresentation_of_lifted_generators.

theorem hasFiniteExtensionByZeroPresentation_of_shortExact (hEnough : S.HasEnoughObjects)
    (hqc : S.ObjectsAreQuasiCompact) (hqs : S.CoverPullbacksAreQuasiCompact)
    (E : ShortComplex (SheafOfModules.{max u₁ v₁ w t} R)) (hE : E.ShortExact)
    (h₁ : HasFiniteExtensionByZeroPresentation.{u₁, v₁, w, t} S R E.X₁)
    (h₃ : HasFiniteExtensionByZeroPresentation.{u₁, v₁, w, t} S R E.X₃) :
    HasFiniteExtensionByZeroPresentation.{u₁, v₁, w, t} S R E.X₂

Tag 093H, a lemma

Tag 093H in the Stacks Project.

Stacks.SheafOfModules.isWeakSerreClass_hasFiniteExtensionByZeroPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ExtensionByZeroWeakSerre.lean, line 207.

Stacks Project, Tag 093H. On a site with a distinguished collection of objects which covers every object, consists of quasi-compact objects and whose coverings have quasi-compact pairwise fibre products, the sheaves of modules with a finite presentation by extensions by zero form a weak Serre subcategory of the category of all sheaves of modules, as soon as the kernel of every morphism between finite direct sums of extensions by zero of the restricted structure sheaf at distinguished objects has such a presentation.

Closure under cokernels is Stacks 093E and closure under extensions is Stacks 093G; closure under kernels is Stacks.SheafOfModules.isClosedUnderKernels_of_presentations applied to the family of finite direct sums of extensions by zero at distinguished objects, which is exactly where the hypothesis enters.

theorem isWeakSerreClass_hasFiniteExtensionByZeroPresentation (hEnough : S.HasEnoughObjects)
    (hqc : S.ObjectsAreQuasiCompact) (hqs : S.CoverPullbacksAreQuasiCompact)
    (hKernel : ∀ (n m : ℕ) (U : Fin n → C) (V : Fin m → C),
      (∀ i, U i ∈ S.objects) → (∀ j, V j ∈ S.objects) →
      ∀ f : (∐ fun j => extensionByZeroUnit.{u₁, v₁, w, t} R (V j)) ⟶
          (∐ fun i => extensionByZeroUnit.{u₁, v₁, w, t} R (U i)),
        HasFiniteExtensionByZeroPresentation.{u₁, v₁, w, t} S R (kernel f)) :
    ObjectProperty.IsWeakSerreClass
      (fun F : SheafOfModules.{max u₁ v₁ w t} R =>
        HasFiniteExtensionByZeroPresentation.{u₁, v₁, w, t} S R F)

Sources

• Section 18.30, Tag 0933
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.cechShortComplex_exact · Stacks.SheafOfModules.epi_cechShortComplex_g · Stacks.SheafOfModules.exists_finite_restrictIndex_cechShortComplex_exact · Stacks.SheafOfModules.exists_finite_epi_sigmaDesc_extensionByZeroUnitMap · Stacks.Sites.sheafOfModules_sections_preserves_coproducts · Stacks.Sites.isColimitSectionsFiniteSubcoproductsCocone · Stacks.Sites.bijective_colimit_post_sheafSections_of_isQuasiCompactObject_of_mono · Stacks.Sites.homFromExtensionByZeroUnit_preservesCoproducts

Section18.31 Flat morphisms#

Section 18.31 of the Stacks Project, Tag 04JA. 4 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04JB, a definition

Tag 04JB in the Stacks Project.

AlgebraicGeometry.RingedToposHom.IsFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FlatMorphisms/RingedTopoi.lean, line 49. The attribute's comment: “flat morphisms of ringed topoi”. References: SGA 4 Vbis (2.4.3.1), “non-fibered case”; SGA 4 V (1.8), “left flat”.

A morphism of ringed topoi is flat when its inverse-image structure map is flat.

abbrev IsFlat {X : RingedTopos.{v, u, w}} {Y : RingedTopos.{v', u', w'}}
    [X.J.HasSheafCompose (forget RingCat.{w})]
    [Y.J.HasSheafCompose (forget RingCat.{w'})]
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [Y.J.HasSheafCompose (forget₂ CommRingCat.{w'} RingCat.{w'})]
    (f : RingedToposHom X Y) : Prop

Declarations registered for the tag:

• AlgebraicGeometry.RingedSite.Hom.IsFlat, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/FlatMorphisms/RingedTopoi.lean, line 59 (StacksFrontier): “flat morphisms of ringed sites”.

Tag 04JC, a lemma

Tag 04JC in the Stacks Project.

Stacks.SheafOfModules.InternalHom.preservesFiniteLimits_ringedSitePullback_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/PullbackInternalHomFlat.lean, line 1147. The attribute's comment: “left exactness of the flat pullback, for a morphism of ringed sites”.

Stacks 04JC for a morphism of ringed sites. If f is flat — that is, if O_C is flat as an f⁻¹O_D-module — then the pullback f^* : Mod(O_D) ⥤ Mod(O_C) of sheaves of modules preserves finite limits.

This is Stacks.Sheaves.RingedToposModules.pullbackModules_exact_of_isFlatMap at the morphism of ringed topoi of f. That result is stated for the pullback built over the four-field morphism of ringed topoi of the modules development, whereas ringedSitePullback is built over the two-field morphism of Stacks 01D3; the two are left adjoints of one and the same direct image, by AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModulesViaComparison and AlgebraicGeometry.RingedToposHom.pullbackAdjPushforwardModules, so they are identified by uniqueness of left adjoints and left exactness transfers along that isomorphism.

theorem preservesFiniteLimits_ringedSitePullback_of_isFlat
    (hf : AlgebraicGeometry.SheafOfModules.IsFlatMapULift
      f.ringedToposHom.fSharpInverseImage) :
    Limits.PreservesFiniteLimits (ringedSitePullback f)

CategoryTheory.Sites.abelianInverseImage_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InverseImage/AbelianSheaf.lean, line 446. The attribute's comment: “inverse_image_exact”.

The inverse image of a morphism of topoi is exact on ordinary abelian sheaves.

theorem abelianInverseImage_exact :
    exactFunctor (Sheaf K AddCommGrpCat.{w'}) (Sheaf J AddCommGrpCat.{w})
      (abelianInverseImage f)

Stacks.Sheaves.RingedToposModules.pullbackModules_exact_of_isFlatMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/RingedLocalization/FlatPullbackExact.lean, line 369. The attribute's comment: “flat_pullback_exact”.

Stacks 04JC, second assertion. Pullback of sheaves of modules along a flat morphism of ringed topoi is exact: it preserves finite limits and finite colimits. The first assertion, exactness of the inverse image of abelian sheaves, is CategoryTheory.Sites.abelianInverseImage_exact.

theorem pullbackModules_exact_of_isFlatMap (f : AlgebraicGeometry.RingedToposHom X Y)
    (hf : AlgebraicGeometry.SheafOfModules.IsFlatMapULift.{w, u, v} f.fSharpInverseImage) :
    exactFunctor (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
      (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
      (f.toRingedToposModulesHom.pullbackModules)

Tag 08M5, a definition

Tag 08M5 in the Stacks Project.

AlgebraicGeometry.SheafOfModules.IsFlat, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Flat.lean, line 285. The attribute's comment: “flatness over a morphism of ringed topoi: this predicate for the pullback ring”. References: SGA 4 V (1.1), “commutative case”.

A sheaf of modules is flat when tensoring on the right with it is an exact endofunctor on sheaves of modules.

This is part (3) of tag 03ER for the native tensor bifunctor, and part (4) just below is stated in terms of it. Stacks.SheafOfModules.IsFlat uses the same native tensor functor.

abbrev IsFlat {O : Sheaf J CommRingCat.{w}}
    [J.WEqualsLocallyBijective AddCommGrpCat.{z}]
    [HasWeakSheafify J AddCommGrpCat.{z}]
    (F : _root_.SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf O)) : Prop

AlgebraicGeometry.RingedToposHom.IsFlatOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/RingedToposFlatModule.lean, line 62. The attribute's comment: “the definition: a sheaf of modules flat over the target ringed topos”.

A sheaf F of O-modules on X = (Sh(C), O) is flat over the ringed topos Y = (Sh(D), O') along a morphism of ringed topoi f : X ⟶ Y when F, regarded as a sheaf of f⁻¹O'-modules by restriction of scalars along the inverse-image form f⁻¹O' ⟶ O of the structure map of f, is flat.

noncomputable abbrev IsFlatOver
    {X : RingedTopos.{v, u, w}} {Y : RingedTopos.{v', u', w'}}
    [X.J.HasSheafCompose (forget RingCat.{w})] [Y.J.HasSheafCompose (forget RingCat.{w'})]
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [Y.J.HasSheafCompose (forget₂ CommRingCat.{w'} RingCat.{w'})]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}] [HasWeakSheafify X.J AddCommGrpCat.{w}]
    (f : RingedToposHom X Y)
    (F : _root_.SheafOfModules.{w}
      (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) : Prop

Tag 0GN2, a lemma

Tag 0GN2 in the Stacks Project.

Stacks.SheafOfModules.InternalHom.isIso_pullbackInternalHomMap_of_isFinitePresentationOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/PullbackInternalHomFinitePresentation.lean, line 81. The attribute's comment: “the isomorphism under the source's own hypotheses: F of finite presentation in the local sense of Tag 03DL and f flat; stated for a site and coefficients in one universe”.

Flat pullback commutes with the canonical internal-Hom map for a module which is locally finitely presented. This statement uses a single universe for the site and coefficients.

theorem isIso_pullbackInternalHomMap_of_isFinitePresentationOnSite
    [F.IsFinitePresentationOnSite]
    (hf : AlgebraicGeometry.SheafOfModules.IsFlatMapULift
      f.ringedToposHom.fSharpInverseImage) : IsIso (pullbackInternalHomMap f F G)

Stacks.SheafOfModules.InternalHom.isIso_pullbackInternalHomMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/PullbackInternalHomFlat.lean, line 1189. The attribute's comment: “the isomorphism, for a global rather than local (Tag 03DL) finite presentation of F”. References: EGA 0 (6.7.6), “special case”.

Stacks 0GN2, for a globally finitely presented F. Let f : (C, O_C) ⟶ (D, O_D) be a flat morphism of ringed sites and let F, G be sheaves of O_D-modules with F presented, over the whole site D, as the cokernel of a morphism between finite coproducts of copies of O_D. Then the canonical map

f^* Hom_{O_D}(F, G) ⟶ Hom_{O_C}(f^*F, f^*G)

of Stacks 0GMX is an isomorphism.

Flatness is the hypothesis hf, that O_C is flat as an f⁻¹O_D-module, which is the definition of a flat morphism of Tag 04JB. It enters through the left exactness of f^* (Tag 04JC, preservesFiniteLimits_ringedSitePullback_of_isFlat), because that is what makes F ↦ f^* Hom_{O_D}(F, G) carry the finite colimit presenting F to a limit of internal Hom sheaves; the other composite needs only that f^* is a left adjoint. The continuity of internal Hom in its first variable is Tag 03EN, preservesFiniteColimits_internalHomFirstMate, and the remaining two inputs the source's proof names are pullbackInternalHomNatural, the first-variable functoriality of the canonical map of Stacks 0GMX, and isIso_toposPullbackInternalHomMap_structureSheaf, its invertibility at the structure sheaf.

The presentation of F is a global one, not the local finite presentation of Tag 03DL that the source assumes: ι, κ, hP, hQ, a, b, hab and hF exhibit F as a cokernel of a morphism between finite coproducts of copies of the structure sheaf over the whole site D. That is strictly stronger than finite presentation, so the statement here is the global special case of Stacks 0GN2; the local case is reduced to it by PullbackInternalHomFinitePresentation.isIso_pullbackInternalHomMap_of_isFinitePresentationOnSite, which states the source's own hypotheses.

theorem isIso_pullbackInternalHomMap
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    (hf : AlgebraicGeometry.SheafOfModules.IsFlatMapULift
      f.ringedToposHom.fSharpInverseImage)
    {n m : ℕ} {P Q : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)}
    (ι : Fin n → (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) ⟶ P))
    (κ : Fin m → (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) ⟶ Q))
    (hP : Limits.IsColimit (Limits.Cofan.mk P ι))
    (hQ : Limits.IsColimit (Limits.Cofan.mk Q κ))
    (a : Q ⟶ P) (b : P ⟶ F) (hab : a ≫ b = 0)
    (hF : Limits.IsColimit (Limits.CokernelCofork.ofπ b hab)) :
    IsIso (pullbackInternalHomMap f F G)

Stacks.SheafOfModules.InternalHom.isIso_pullbackInternalHomMap_structureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/PullbackInternalHomFlat.lean, line 1242. The attribute's comment: “the isomorphism for F the structure sheaf”. References: EGA 0 (6.7.6), “partial, special case”.

Stacks 0GN2 for F the structure sheaf. Let f : (C, O_C) ⟶ (D, O_D) be a morphism of ringed sites and G a sheaf of O_D-modules. The canonical map

f^* Hom_{O_D}(O_D, G) ⟶ Hom_{O_C}(f^*O_D, f^*G)

of Stacks 0GMX is an isomorphism.

The structure sheaf is finitely presented, and at it both sides of the canonical map are identified with f^*G: the inputs are the identification f^*O_D = O_C of Stacks 03D6 and the identity Hom_O(O, -) = id of Stacks 03EM. Flatness of f is not used — the source needs it only to carry a presentation of a general F across the pullback.

theorem isIso_pullbackInternalHomMap_structureSheaf :
    IsIso (pullbackInternalHomMap f
      (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf (J := Y.J)) Y.O)) G)

Sources

• Section 18.31, Tag 04JA
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedToposHom.IsFlat · AlgebraicGeometry.RingedSite.Hom.IsFlat · Stacks.SheafOfModules.InternalHom.preservesFiniteLimits_ringedSitePullback_of_isFlat · CategoryTheory.Sites.abelianInverseImage_exact · Stacks.Sheaves.RingedToposModules.pullbackModules_exact_of_isFlatMap · AlgebraicGeometry.SheafOfModules.IsFlat · AlgebraicGeometry.RingedToposHom.IsFlatOver · Stacks.SheafOfModules.InternalHom.isIso_pullbackInternalHomMap_of_isFinitePresentationOnSite

Section18.32 Invertible modules#

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

Tag 0409, a definition

Tag 0409 in the Stacks Project.

Stacks.SheafOfModules.IsInvertible, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorInvertible.lean, line 130. The attribute's comment: “invertible”.

Stacks Project, Tag 01CS, equivalently Tag 0409 (2). A sheaf of O-modules is invertible when its tensor functor is an equivalence. The universal property specifies that tensor functor independently of any chosen construction of sheafification, hence on every site; so the ringed-space form of the definition and the ringed-site form coincide here.

class IsInvertible
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)) : Prop

Stacks.SheafOfModules.Invertible.isInvertible_iff_tensorRightFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/TensorPower.lean, line 132. The attribute's comment: “invertible”.

Stacks Project, Tag 0409 (2), equivalently Tag 01CS, in the source's own form: a sheaf of O-modules L is invertible exactly when the functor F ↦ (F ⊗_O L)^# of the source is an equivalence. The invertibility predicate is phrased through the universal property of tensoring on the left, so this is the criterion the source states and the predicate agreeing, the two tensor functors being identified by tensorLeftIsoTensorRight.

theorem isInvertible_iff_tensorRightFunctor_isEquivalence
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)) :
    IsInvertible O hO L ↔ ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w}
      ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ O (forget₂ CommRingCat RingCat) hO⟩).flip.obj
        L).IsEquivalence

AlgebraicGeometry.RingedSite.IsFiniteLocallyFreeOfRank, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FiniteLocallyFreeOfRank.lean, line 62. The attribute's comment: “rank”. References: EGA 0 (5.4.1), “rank n”.

A sheaf of modules on a ringed site is finite locally free of rank r if it is, over a covering family of every object, a coproduct of r copies of the structure sheaf. This is the rank clause of Stacks 0409.

abbrev IsFiniteLocallyFreeOfRank (X : RingedSite.{u, v, w})
    (F : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) (r : ℕ) : Prop

AlgebraicGeometry.RingedSite.unitsSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/UnitsSheaf.lean, line 50. The attribute's comment: “units sheaf”.

The sheaf of units O_X^* of the structure sheaf of a ringed site.

noncomputable def unitsSheaf (X : RingedSite.{u, v, w}) : Sheaf X.J CommGrpCat.{w}

AlgebraicGeometry.RingedSite.unitsSheafι_mono, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/UnitsSheaf.lean, line 64. The attribute's comment: “subsheaf”.

The canonical inclusion of the units sheaf into the structure sheaf is a monomorphism.

instance unitsSheafι_mono (X : RingedSite.{u, v, w}) : Mono (unitsSheafι X)

AlgebraicGeometry.RingedSite.exists_unitsSheaf_iff_exists_mul_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/UnitsSheaf.lean, line 84. The attribute's comment: “defining rule”.

A section belongs to the units subsheaf exactly when it has a right inverse: the units subsheaf is U ↦ {f ∈ O(U) | ∃ g ∈ O(U), fg = 1}.

theorem exists_unitsSheaf_iff_exists_mul_eq_one (X : RingedSite.{u, v, w}) (U : X.Cᵒᵖ)
    (f : X.O.obj.obj U) :
    (∃ x : ((unitsSheaf X).obj.obj U : Type w), (unitsSheafι X).hom.app U x = f) ↔
      ∃ g : X.O.obj.obj U, f * g = 1

AlgebraicGeometry.RingedSite.unitsSheafι_hom_app_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/UnitsSheaf.lean, line 103. The attribute's comment: “group law”.

The group law on the sheaf of units is multiplication: the subsheaf inclusion O_X^* ⟶ O_X is multiplicative.

theorem unitsSheafι_hom_app_mul (X : RingedSite.{u, v, w}) (U : X.Cᵒᵖ)
    (x y : (X.O.obj.obj U)ˣ) :
    (unitsSheafι X).hom.app U (x * y) =
      (x : X.O.obj.obj U) * (y : X.O.obj.obj U)

Tag 0B8N, a lemma

Tag 0B8N in the Stacks Project.

Stacks.SheafOfModules.Invertible.tensorInverseIsoDualSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleDualEvaluation.lean, line 307. The attribute's comment: “(c)”. References: SGA 6 VIII (3.5), “partial”.

Stacks Project, Tag 0B8N (c). A sheaf of 𝒪-modules N whose tensor product with L is isomorphic to the structure sheaf is isomorphic to SheafHom(L, 𝒪).

The hypothesis is clause (2) of the tag, so L is invertible and the evaluation pairing SheafHom(L, 𝒪) ⊗_𝒪 L ⟶ 𝒪 is an isomorphism by isIso_evaluation. That exhibits SheafHom(L, 𝒪) as a two-sided tensor inverse of L, the braiding supplying the other order, while the given isomorphism exhibits N as one; a two-sided tensor inverse in a monoidal category is unique up to isomorphism (CategoryTheory.MonoidalCategory.HasInverse.inv_iso).

noncomputable def tensorInverseIsoDualSheaf
    (N : SheafOfModules.{max u v} (TensorSheafification.structureSheaf 𝒪 h𝒪))
    (e : ((Tensor.sheafTensor
      ⟨𝒪, Presheaf.isSheaf_of_isSheaf_comp _ 𝒪 (forget₂ CommRingCat RingCat) h𝒪⟩).obj L).obj N ≅
      SheafOfModules.unit (TensorSheafification.structureSheaf 𝒪 h𝒪)) :
    N ≅ dualSheaf 𝒪 h𝒪 L

Stacks.SheafOfModules.isFlat_of_isInvertible_ringedSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleEquivalence.lean, line 207. The attribute's comment: “(a), the flatness half”.

An invertible sheaf of modules on a ringed site is flat.

theorem isFlat_of_isInvertible_ringedSite
    (L : SheafOfModules.{w} (TensorSheafification.structureSheaf O.obj hO))
    (hL : IsInvertible O.obj hO L) :
    IsFlat (O := O) L

Stacks.SheafOfModules.isFinitePresentation_of_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleFinitePresentation.lean, line 289. The attribute's comment: “(a), the finite-presentation half”.

An invertible sheaf of modules is of finite presentation.

This is the step of Tag 0B8M's converse that Stacks attributes to Tag 0B8K. By Tag 0B8N (b) every object of the site has a covering family on whose members L is a split subobject of a finite product of copies of the structure sheaf, hence has a finite presentation there; the union over all objects of those families covers the terminal object, and finite presentation is local.

This is also the finite-presentation half of Tag 0B8N (a).

theorem isFinitePresentation_of_isInvertible
    (hO : Presheaf.IsSheaf J (Stacks.SheafOfModules.TensorSheafification.structureRingPresheaf O))
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)) (hL :
      IsInvertible O hO L) :
    L.IsFinitePresentation

Stacks.SheafOfModules.isInvertible_iff_exists_tensor_iso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleRankOne.lean, line 298. The attribute's comment: “(1) ⟺ (2)”.

Stacks Project, Tag 0B8K and Tag 0B8N, (1) ⟺ (2). A sheaf of O-modules L is invertible if and only if there is a sheaf of O-modules N whose tensor product with L is isomorphic to O.

For the forward implication the tensor functor of L is an equivalence, so O has a preimage N under it, and the universal property identifies the image of that preimage with L ⊗_O N. For the converse the isomorphism L ⊗_O N ≅ O is turned into a pairing of presheaves of modules by composing with the sheafification unit, and isInvertible_of_pairing applies.

Tag 0B8K states this for a ringed space and Tag 0B8N for an arbitrary ringed site; the statement here is the one on a ringed site, so it carries both.

theorem isInvertible_iff_exists_tensor_iso_unit
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)) :
    IsInvertible O hO L ↔ ∃ N : SheafOfModules.{w}
      (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO),
      Nonempty (((Tensor.sheafTensor.{u, v, w, w, w}
        ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ O (forget₂ CommRingCat RingCat) hO⟩).obj L).obj N ≅
        SheafOfModules.unit (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))

Stacks.SheafOfModules.exists_cover_isDirectSummand_finiteFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleSummandNoSliceSheafify.lean, line 378. The attribute's comment: “(b), invertible_local_summand”.

Stacks Project, Tag 0B8N (b). On a cover of any object, an invertible module embeds as a direct summand of a finite free module. The two sheafification hypotheses are used only by Stacks.SheafOfModules.isLocallyInjective_of_universal; none is needed on the slice sites.

theorem exists_cover_isDirectSummand_finiteFree
    (hO : Presheaf.IsSheaf J (Stacks.SheafOfModules.TensorSheafification.structureRingPresheaf O))
    (L : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
      [IsInvertible O hO L] (U : C) :
    ∃ (I : Type (max u v)) (V : I → C) (f : ∀ i, V i ⟶ U),
      Sieve.generate (Presieve.ofArrows V f) ∈ J U ∧
        ∀ i : I, ∃ n : ℕ,
          ∃ s : L.over (V i) ⟶
              ∏ᶜ (fun _ : Fin n ↦
                SheafOfModules.unit ((Stacks.SheafOfModules.TensorSheafification.structureSheaf O
                  hO).over (V i))),
            IsSplitMono s

Tag 0B8P, a lemma

Tag 0B8P in the Stacks Project.

Stacks.SheafOfModules.isInvertible_pullbackModules_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackInvertible/RingedTopos.lean, line 86.

Stacks Project, Tag 0B8P. The pullback of an invertible module along a morphism of ringed topoi is invertible.

theorem isInvertible_pullbackModules_obj (f : RingedToposHom X Y)
    (L : SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    [hL : IsInvertible Y.O.obj (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).property L] :
    IsInvertible X.O.obj (Stacks.SheafOfModules.Tensor.ringSheaf X.O).property
      ((f.pullbackModules).obj L)

Stacks.SheafOfModules.isInvertible_pullbackModules_obj_ringedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackInvertible/RingedTopos.lean, line 102.

Stacks Project, Tag 0B8P for a morphism of ringed topoi in the two-field sense of Tag 01D3 part (2): the pullback of an invertible module is invertible.

theorem isInvertible_pullbackModules_obj_ringedToposHom
    (f : AlgebraicGeometry.RingedToposHom X Y)
    (L : SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    [IsInvertible Y.O.obj (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).property L] :
    IsInvertible X.O.obj (Stacks.SheafOfModules.Tensor.ringSheaf X.O).property
      ((f.toRingedToposModulesHom.pullbackModules).obj L)

AlgebraicGeometry.Space.modulePullbackInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Quot/PicardFunctor.lean, line 234. The attribute's comment: “the inverse image of an invertible module along a morphism of algebraic spaces is invertible”.

The inverse image of an invertible module along a morphism of algebraic spaces is invertible. This is AlgebraicGeometry.Space.isInvertible_modulePullback_obj, read through the two spellings of invertibility of StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleCompare.lean.

theorem modulePullbackInvertible : ModulePullbackInvertible B S hS

Tag 040A, a lemma

Tag 040A in the Stacks Project.

Stacks.SheafOfModules.Invertible.isIso_evaluation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleDualEvaluation.lean, line 261. The attribute's comment: “part (2)”. References: EGA 0 (5.4.3), “more general”.

Stacks Project, Tag 040A (2), the evaluation clause. For an invertible sheaf of 𝒪-modules L on a ringed site the evaluation pairing SheafHom(L, 𝒪) ⊗_𝒪 L ⟶ 𝒪 is an isomorphism.

The dual is a left dual of L by exactPairingDualSheafOfIsInvertible, and the evaluation of an exact pairing is an isomorphism whenever tensoring on the right by the first object is an equivalence, which for an invertible sheaf of modules it is.

A ringed space is a ringed site, so this is also the evaluation clause of Tag 01CT (2); see Stacks.SheafOfModules.isIso_evaluation_of_isInvertible for that reading.

theorem isIso_evaluation [IsInvertible 𝒪 h𝒪 L] : IsIso (evaluation 𝒪 h𝒪 L)

Stacks.SheafOfModules.Invertible.isIso_tensorSheafBraiding_hom_comp_evaluation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleDualEvaluation.lean, line 277. The attribute's comment: “part (2)”. References: EGA 0 (5.4.3), “more general”.

Stacks Project, Tag 040A (2) and Tag 01CT (2), the evaluation clause in the order the tags write it. The evaluation map L ⊗_𝒪 SheafHom(L, 𝒪) ⟶ 𝒪 is an isomorphism. It is the canonical pairing of Stacks.SheafOfModules.evaluation, whose factors come in the order Tag 0FNV writes them, preceded by the braiding of the tensor product sheaf, which is what exchanges the two factors; in this order it is the trivializing pairing identifying L^∨ as a tensor inverse of L.

theorem isIso_tensorSheafBraiding_hom_comp_evaluation [IsInvertible 𝒪 h𝒪 L] :
    IsIso ((tensorSheafBraiding 𝒪 h𝒪 L (dualSheaf 𝒪 h𝒪 L)).hom ≫ evaluation 𝒪 h𝒪 L)

Stacks.SheafOfModules.Invertible.isInvertible_dualSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InvertibleDualEvaluation.lean, line 287. The attribute's comment: “part (2)”.

Stacks Project, Tag 040A (2) and Tag 01CT (2), the invertibility clause. The dual L^∨ = SheafHom(L, 𝒪) of an invertible sheaf of 𝒪-modules is again invertible: the evaluation pairing is an isomorphism L^∨ ⊗_𝒪 L ≅ 𝒪, which is Tag 0B8K (2) for L^∨.

theorem isInvertible_dualSheaf [IsInvertible 𝒪 h𝒪 L] :
    IsInvertible 𝒪 h𝒪 (dualSheaf 𝒪 h𝒪 L)

Stacks.SheafOfModules.tensorProduct_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorInvertible.lean, line 474. The attribute's comment: “part (1)”.

Stacks Project, Tag 01CT (1), Tag 040A (1). The tensor product of two invertible sheaves of modules is invertible.

theorem tensorProduct_isInvertible
    (L N : SheafOfModules.{w} (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    [IsInvertible O hO L] [IsInvertible O hO N] :
    IsInvertible O hO ((((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w}
      ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ O (forget₂ CommRingCat RingCat) hO⟩).obj L)).obj N)

Tag 040B, a lemma

Tag 040B in the Stacks Project.

Stacks.SheafOfModules.essentiallySmall_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Picard/EssentiallySmall/Invertible.lean, line 249.

Stacks 040B. The invertible sheaves of modules on a ringed site form an essentially small class: there is a set of invertible modules such that every invertible module is isomorphic to exactly one of them. Equivalently, the isomorphism classes of invertible O-modules form a set of size max u v w.

The two instance hypotheses are the standing hypotheses of the invertible-module API of this development — they are what makes the sheafified tensor product and the locally bijective pairing of Tag 0B8N available — and they are satisfied wherever Tag 01CX builds the Picard group.

theorem essentiallySmall_isInvertible
    (O : Cᵒᵖ ⥤ CommRingCat.{w})
    (hO : Presheaf.IsSheaf J (Stacks.SheafOfModules.TensorSheafification.structureRingPresheaf O)) :
    ObjectProperty.EssentiallySmall.{max u v w} (IsInvertible O hO)

Tag 040C, a definition

Tag 040C in the Stacks Project.

Stacks.SheafOfModules.Picard.PicardGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Picard.lean, line 170. The attribute's comment: “the Picard group”. References: EGA IV (21.3.2), “Pic(X) definition”; SGA 6 X (5.1), “Pic(X) definition”.

The Picard group of O: the group of isomorphism classes of invertible sheaves of O-modules, as a small type.

noncomputable def PicardGroup : Type (max (max u v) w)

Stacks.SheafOfModules.Picard.instAddCommGroupPicardGroup, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Picard.lean, line 176. The attribute's comment: “abelian group structure”.

The abelian group structure on the Picard group; its addition is the tensor product sheaf, by classOf_tensor.

noncomputable instance instAddCommGroupPicardGroup : AddCommGroup (PicardGroup O hO)

Stacks.SheafOfModules.Picard.classOf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Picard.lean, line 181. The attribute's comment: “class of an invertible module”. References: EGA IV (21.3.2), “cl(L)”.

The class in the Picard group of an invertible sheaf of modules.

noncomputable abbrev classOf (L : SheafOfModules.{w}
  (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    (hL : IsInvertible O hO L) : PicardGroup O hO

Stacks.SheafOfModules.Picard.classOf_eq_classOf_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Picard.lean, line 200. The attribute's comment: “elements are isomorphism classes of invertible modules”. References: EGA IV (21.3.2), “cl(L)=cl(L') iff iso”.

Two invertible sheaves of modules determine the same Picard class exactly when they are isomorphic, so the elements of the Picard group are the isomorphism classes.

theorem classOf_eq_classOf_iff (L N : SheafOfModules.{w}
  (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    (hL : IsInvertible O hO L) (hN : IsInvertible O hO N) :
    classOf O hO L hL = classOf O hO N hN ↔ Nonempty (L ≅ N)

Stacks.SheafOfModules.Picard.classOf_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Picard.lean, line 211. The attribute's comment: “addition is tensor product”.

Addition in the Picard group is the tensor product sheaf.

theorem classOf_tensor (L N : SheafOfModules.{w}
  (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO))
    (hL : IsInvertible O hO L) (hN : IsInvertible O hO N)
    (hLN : IsInvertible O hO ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ (O) (forget₂ CommRingCat RingCat) (hO)⟩).obj
        (L)).obj (N)))) :
    classOf O hO L hL + classOf O hO N hN =
      classOf O hO ((((Stacks.SheafOfModules.Tensor.sheafTensor
        ⟨O, Presheaf.isSheaf_of_isSheaf_comp _ (O) (forget₂ CommRingCat RingCat) (hO)⟩).obj
          (L)).obj (N))) hLN

Sources

• Section 18.32, Tag 0408
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafOfModules.IsInvertible · Stacks.SheafOfModules.Invertible.isInvertible_iff_tensorRightFunctor_isEquivalence · AlgebraicGeometry.RingedSite.IsFiniteLocallyFreeOfRank · AlgebraicGeometry.RingedSite.unitsSheaf · AlgebraicGeometry.RingedSite.unitsSheafι_mono · AlgebraicGeometry.RingedSite.exists_unitsSheaf_iff_exists_mul_eq_one · AlgebraicGeometry.RingedSite.unitsSheafι_hom_app_mul · Stacks.SheafOfModules.Invertible.tensorInverseIsoDualSheaf

Section18.33 Modules of differentials#

Section 18.33 of the Stacks Project, Tag 04BJ. 12 tags here are carried by 39 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04BK, a definition

Tag 04BK in the Stacks Project.

Declarations registered for the tag:

• PresheafOfModulesOfCommRing.Derivation' registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch18.lean, line 71 (StacksFrontier): “for the underlying presheaves of rings and of modules”. References: EGA IV (16.5.1), “more general”.

Tag 04BL, a lemma

Tag 04BL in the Stacks Project.

Stacks.Sheaves.Differentials.universalDerivation_isUniversal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialsRepresentable.lean, line 115.

Every relative derivation with values in a sheaf of modules factors through the universal derivation by a unique morphism of sheaves of modules.

theorem universalDerivation_isUniversal
    (F : SheafOfModules.{u} (underlyingRingSheaf O₂))
    (D : SheafDerivation O₁ O₂ φ F) :
    ∃! f : moduleOfDifferentials O₁ O₂ φ ⟶ F,
      (universalDerivation O₁ O₂ φ).postcomp f.val = D

AlgebraicGeometry.SheafOfModules.existsUnique_descDerivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PrincipalPartsUniversal.lean, line 138. The attribute's comment: “unique-factorization form, on an arbitrary site”.

Stacks 04BL, in unique-factorization form: every relative derivation with values in a sheaf of modules factors through the universal derivation by a unique morphism of sheaves of modules.

theorem existsUnique_descDerivation
    (F : _root_.SheafOfModules.{max u v w m} (Stacks.SheafOfModules.Tensor.ringSheaf O₂))
    (D : PresheafOfModulesOfCommRing.Derivation' F.val φ.hom) :
    ∃! f : moduleOfDifferentialsOfSite.{v, u, w, m} O₁ O₂ φ ⟶ F,
      (universalDerivationOfSite.{v, u, w, m} O₁ O₂ φ).postcomp f.val = D

AlgebraicGeometry.SheafOfModules.derivationsFunctor_isCorepresentable, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Differentials.lean, line 366.

For a homomorphism of sheaves of commutative rings, the functor sending a sheaf of modules to the type of relative derivations is represented by a sheaf of modules.

instance derivationsFunctor_isCorepresentable {C : Type u₁} [Category.{v₁} C]
    {J : GrothendieckTopology C}
    [J.HasSheafCompose (forget₂ CommRingCat.{u} RingCat.{u})]
    (O₁ O₂ : Sheaf J CommRingCat.{u}) (φ : O₁ ⟶ O₂) :
    (derivationsFunctor.{v} O₁ O₂ φ).IsCorepresentable

Tag 04BM, an equation

Tag 04BM in the Stacks Project.

AlgebraicGeometry.SheafOfModules.moduleDifferentialsRelationMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RecoveryAux/ModuleDifferentialsRelationMap.lean, line 160.

The map O₂[O₂ × O₂] ⊕ O₂[O₂ × O₂] ⊕ O₂[O₁] ⟶ O₂[O₂] whose three components send generators respectively to [a+b]-[a]-[b], [fg]-g[f]-f[g], and [φ(h)].

Here every free module presheaf and the displayed morphism have been sheafified.

noncomputable def moduleDifferentialsRelationMap
    (O₁ O₂ : Sheaf J RingCat.{u}) (φ : O₁ ⟶ O₂)
    [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasWeakSheafify J AddCommGrpCat.{u}] :
    (sheafification (𝟙 O₂.obj)).obj
      ((freeObj (R := O₂.obj) (ringElementPairs O₂) ⨿
        freeObj (R := O₂.obj) (ringElementPairs O₂)) ⨿
        freeObj (R := O₂.obj) (ringElements O₁)) ⟶
    (sheafification (𝟙 O₂.obj)).obj
      (freeObj (R := O₂.obj) (ringElements O₂))

AlgebraicGeometry.SheafOfModules.moduleDifferentialsRelationMap_additive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RecoveryAux/ModuleDifferentialsRelationMap.lean, line 205. The attribute's comment: “additive summand”.

The additive summand sends [(a,b)] to [a+b]-[a]-[b].

theorem moduleDifferentialsRelationMap_additive
    (O₁ O₂ : Sheaf J RingCat.{u}) (φ : O₁ ⟶ O₂)
    [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasWeakSheafify J AddCommGrpCat.{u}]
    (X : Cᵒᵖ) (a b : O₂.obj.obj X) :
    ((sheafificationHomEquiv (𝟙 O₂.obj)
      ((sheafification (𝟙 O₂.obj)).map (coprod.inl ≫ coprod.inl) ≫
        moduleDifferentialsRelationMap O₁ O₂ φ)).app X) (ModuleCat.freeMk (a, b)) =
      sheafifiedFreeGenerator O₂ (ringElements O₂) X (a + b) -
        sheafifiedFreeGenerator O₂ (ringElements O₂) X a -
        sheafifiedFreeGenerator O₂ (ringElements O₂) X b

AlgebraicGeometry.SheafOfModules.moduleDifferentialsRelationMap_leibniz, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RecoveryAux/ModuleDifferentialsRelationMap.lean, line 224. The attribute's comment: “Leibniz summand”.

The multiplicative summand sends [(f,g)] to [fg]-g[f]-f[g].

theorem moduleDifferentialsRelationMap_leibniz
    (O₁ O₂ : Sheaf J RingCat.{u}) (φ : O₁ ⟶ O₂)
    [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasWeakSheafify J AddCommGrpCat.{u}]
    (X : Cᵒᵖ) (f g : O₂.obj.obj X) :
    ((sheafificationHomEquiv (𝟙 O₂.obj)
      ((sheafification (𝟙 O₂.obj)).map (coprod.inr ≫ coprod.inl) ≫
        moduleDifferentialsRelationMap O₁ O₂ φ)).app X) (ModuleCat.freeMk (f, g)) =
      sheafifiedFreeGenerator O₂ (ringElements O₂) X (f * g) -
        g • sheafifiedFreeGenerator O₂ (ringElements O₂) X f -
        f • sheafifiedFreeGenerator O₂ (ringElements O₂) X g

AlgebraicGeometry.SheafOfModules.moduleDifferentialsRelationMap_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/RecoveryAux/ModuleDifferentialsRelationMap.lean, line 243. The attribute's comment: “base-ring summand”.

The base-ring summand sends [h] to [φ(h)].

theorem moduleDifferentialsRelationMap_base
    (O₁ O₂ : Sheaf J RingCat.{u}) (φ : O₁ ⟶ O₂)
    [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasWeakSheafify J AddCommGrpCat.{u}]
    (X : Cᵒᵖ) (h : O₁.obj.obj X) :
    ((sheafificationHomEquiv (𝟙 O₂.obj)
      ((sheafification (𝟙 O₂.obj)).map coprod.inr ≫
        moduleDifferentialsRelationMap O₁ O₂ φ)).app X) (ModuleCat.freeMk h) =
      sheafifiedFreeGenerator O₂ (ringElements O₂) X (φ.hom.app X h)

Tag 04BN, a definition

Tag 04BN in the Stacks Project.

AlgebraicGeometry.SheafOfModules.moduleOfDifferentialsOfSite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PrincipalPartsUniversal.lean, line 121. The attribute's comment: “the module of differentials Ω_{O₂/O₁}”.

The sheaf of relative differentials Ω_{O₂/O₁}: the sheaf of modules corepresenting the functor of relative derivations.

noncomputable abbrev moduleOfDifferentialsOfSite :
    _root_.SheafOfModules.{max u v w m} (Stacks.SheafOfModules.Tensor.ringSheaf O₂)

AlgebraicGeometry.SheafOfModules.universalDerivationOfSite, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PrincipalPartsUniversal.lean, line 129. The attribute's comment: “the module of differentials Ω_{O₂/O₁}”. References: EGA IV (16.3.6), “dt”; EGA IV (16.5.3), “(i)”.

The universal relative derivation with values in Ω_{O₂/O₁}.

noncomputable def universalDerivationOfSite :
    PresheafOfModulesOfCommRing.Derivation' (moduleOfDifferentialsOfSite.{v, u, w, m} O₁ O₂ φ).val
      φ.hom

Tag 08TP, a lemma

Tag 08TP in the Stacks Project.

AlgebraicGeometry.SheafOfModules.differentialsSheafificationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialsSheafification.lean, line 396. The attribute's comment: “isomorphism”.

Stacks Project, Tag 08TP. Relative differentials commute with passing from presheaves of commutative rings to their associated sheaves: the sheaf of differentials of O₂^# over O₁^# is canonically the sheaf associated to the presheaf X ↦ Ω[O₂(X)⁄O₁(X)].

noncomputable def differentialsSheafificationIso (O₁ O₂ : Cᵒᵖ ⥤ CommRingCat.{u})
    (f : O₁ ⟶ O₂) :
    (derivationsFunctor.{v} (associatedCommRingSheaf J O₁) (associatedCommRingSheaf J O₂)
        (associatedCommRingSheafMap J f)).coreprX ≅
      sheafifiedObjectwiseDifferentials.{v, v₁} J f

AlgebraicGeometry.SheafOfModules.differentialsSheafificationIso_inv_unit_d, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialsSheafification.lean, line 409. The attribute's comment: “canonicality”.

Stacks Project, Tag 08TP, the canonicality of the comparison: the inverse of differentialsSheafificationIso carries the image of the objectwise universal differential d b to the sheaf-level universal derivation evaluated on the image of b.

lemma differentialsSheafificationIso_inv_unit_d (O₁ O₂ : Cᵒᵖ ⥤ CommRingCat.{u})
    (f : O₁ ⟶ O₂) (X : Cᵒᵖ) (b : O₂.obj X) :
    ((differentialsSheafificationIso.{v, v₁} J O₁ O₂ f).inv.val.app X)
        (objectwiseDifferentialInSheafification.{v, v₁} J f X b) =
      (derivationsFunctor.{v} (associatedCommRingSheaf J O₁) (associatedCommRingSheaf J O₂)
        (associatedCommRingSheafMap J f)).coreprx.d
          ((toAssociatedRingSheaf J O₂).app X b)

AlgebraicGeometry.SheafOfModules.isIso_objectwiseDifferentialsSheafificationHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ObjectwiseDifferentialsLocallyBijective.lean, line 134. The attribute's comment: “for sheaves of rings, as an isomorphism out of the sheafification”.

The sheafification of the objectwise Kähler differentials is the sheaf of relative differentials: objectwiseDifferentialsSheafificationHom is an isomorphism.

theorem isIso_objectwiseDifferentialsSheafificationHom :
    IsIso (objectwiseDifferentialsSheafificationHom.{v} O₁ O₂ φ)

AlgebraicGeometry.SheafOfModules.isLocallyInjective_objectwiseDifferentialsToSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ObjectwiseDifferentialsLocallyBijective.lean, line 193. The attribute's comment: “for sheaves of rings, local injectivity”.

Stacks 08TP, injectivity half: the comparison from the objectwise Kähler differentials to the sheaf of relative differentials is locally injective.

theorem isLocallyInjective_objectwiseDifferentialsToSheaf :
    PresheafOfModules.IsLocallyInjective J (objectwiseDifferentialsToSheaf.{v} O₁ O₂ φ)

AlgebraicGeometry.SheafOfModules.isLocallySurjective_objectwiseDifferentialsToSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ObjectwiseDifferentialsLocallyBijective.lean, line 207. The attribute's comment: “for sheaves of rings, local surjectivity”.

Stacks 08TP, surjectivity half: the comparison from the objectwise Kähler differentials to the sheaf of relative differentials is locally surjective.

theorem isLocallySurjective_objectwiseDifferentialsToSheaf :
    PresheafOfModules.IsLocallySurjective J (objectwiseDifferentialsToSheaf.{v} O₁ O₂ φ)

Tag 08TQ, a lemma

Tag 08TQ in the Stacks Project.

Stacks.Sheaves.Differentials.pullbackDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialsInverseImage.lean, line 590. The attribute's comment: “the canonical identification, with the morphism of topoi presented by a continuous functor of the underlying sites, both sites small in the single universe of the sections of the sheaves of rings and of the modules, and the inverse image of sheaves of commutative rings assumed to exist”.

Stacks Project, Tag 08TQ. For a morphism of topoi presented by a continuous functor of the underlying sites, the inverse image of the sheaf of relative differentials is canonically the sheaf of relative differentials of the inverse-image morphism of sheaves of rings.

noncomputable def pullbackDifferentialsIso :
    inverseImageModule J K F O₂ (moduleOfDifferentials O₁ O₂ φ) ≅
      moduleOfDifferentials (inverseImageRing J K F O₁) (inverseImageRing J K F O₂)
        ((F.sheafPullback CommRingCat.{u} J K).map φ)

Stacks.Sheaves.Differentials.pullbackDifferentialsIso_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialsInverseImage.lean, line 624. The attribute's comment: “compatibility with universal derivations”.

Stacks Project, Tag 08TQ. The canonical identification carries the inverse image of the universal derivation to the universal derivation.

theorem pullbackDifferentialsIso_compatible :
    (inverseImageDerivation J K F φ (moduleOfDifferentials O₁ O₂ φ)
          (universalDerivation O₁ O₂ φ)).postcomp
        (pullbackDifferentialsIso J K F φ).hom.val =
      universalDerivation (inverseImageRing J K F O₁) (inverseImageRing J K F O₂)
        ((F.sheafPullback CommRingCat.{u} J K).map φ)

Stacks.Sheaves.Differentials.pullbackDifferentialsIso_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialsInverseImage.lean, line 635. The attribute's comment: “canonicity”.

Stacks Project, Tag 08TQ. Compatibility with universal derivations characterises the canonical identification.

theorem pullbackDifferentialsIso_unique
    (e : inverseImageModule J K F O₂ (moduleOfDifferentials O₁ O₂ φ) ≅
      moduleOfDifferentials (inverseImageRing J K F O₁) (inverseImageRing J K F O₂)
        ((F.sheafPullback CommRingCat.{u} J K).map φ))
    (he : (inverseImageDerivation J K F φ (moduleOfDifferentials O₁ O₂ φ)
        (universalDerivation O₁ O₂ φ)).postcomp e.hom.val =
      universalDerivation (inverseImageRing J K F O₁) (inverseImageRing J K F O₂)
        ((F.sheafPullback CommRingCat.{u} J K).map φ)) :
    e = pullbackDifferentialsIso J K F φ

Stacks.Sheaves.RingedToposModules.inverseImageDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/InverseImageDerivations.lean, line 964. The attribute's comment: “for an arbitrary morphism of topoi, with the object, arrow and section universes of the two sites independent”.

Stacks 08TQ. The inverse image of the sheaf of relative differentials of a homomorphism of sheaves of commutative rings along a morphism of topoi is the sheaf of relative differentials of the inverse image: f⁻¹Ω_{P/A} ≅ Ω_{f⁻¹P/f⁻¹A}.

noncomputable def inverseImageDifferentialsIso :
    inverseImageDifferentials f a ≅
      moduleOfDifferentialsOfSite.{v, u, max u v w, max u v w}
        (f.inverseImageRing.obj A) (f.inverseImageRing.obj P) (f.inverseImageRing.map a)

Stacks.Sheaves.RingedToposModules.homEquiv_inverseImageDifferentialsIso_hom, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/InverseImageDerivations.lean, line 976. The attribute's comment: “compatibility with the universal derivations”.

Stacks 08TQ. The identification is the one carrying the inverse image of the universal derivation of Ω_{P/A} to the universal derivation of Ω_{f⁻¹P/f⁻¹A}: transposing it along f⁻¹ ⊣ f_* and the universal property of Ω_{P/A} returns the universal derivation.

lemma homEquiv_inverseImageDifferentialsIso_hom :
    (inverseImageDifferentialsCorepresentableBy f a).homEquiv
        (inverseImageDifferentialsIso f a).hom =
      universalDerivationOfSite.{v, u, max u v w, max u v w}
        (f.inverseImageRing.obj A) (f.inverseImageRing.obj P) (f.inverseImageRing.map a)

Tag 04BO, a lemma

Tag 04BO in the Stacks Project.

AlgebraicGeometry.SheafOfModules.overDifferentialsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/Differentials.lean, line 340. The attribute's comment: “the canonical isomorphism, with the object, arrow and section universes of the site independent”.

Stacks 04BO. For a homomorphism φ : O₁ ⟶ O₂ of sheaves of commutative rings on a site and an object U of that site, the restriction of the sheaf of relative differentials to the slice site over U is the sheaf of relative differentials of the restrictions: Ω_{O₂/O₁}|_U ≅ Ω_{(O₂|_U)/(O₁|_U)}.

noncomputable def overDifferentialsIso :
    (moduleOfDifferentialsOfSite.{v, u, max u v w, max u v w} O₁ O₂ φ).over U ≅
      moduleOfDifferentialsOfSite.{v, max u v, max u v w, max u v w}
        (O₁.over U) (O₂.over U) ((J.overPullback CommRingCat.{max u v w} U).map φ)

AlgebraicGeometry.SheafOfModules.homEquiv_overDifferentialsIso_hom, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/Differentials.lean, line 354. The attribute's comment: “compatibility with the universal derivations”.

Stacks 04BO. The identification is the one carrying the restriction of the universal derivation of Ω_{O₂/O₁} to the universal derivation of Ω_{(O₂|_U)/(O₁|_U)}: transposing it along the corepresentation of AlgebraicGeometry.SheafOfModules.overDifferentialsCorepresentableBy returns that universal derivation.

lemma homEquiv_overDifferentialsIso_hom :
    (overDifferentialsCorepresentableBy.{w} J U φ).homEquiv
        (overDifferentialsIso.{w} J U φ).hom =
      universalDerivationOfSite.{v, max u v, max u v w, max u v w}
        (O₁.over U) (O₂.over U) ((J.overPullback CommRingCat.{max u v w} U).map φ)

Tag 08TR, a lemma

Tag 08TR in the Stacks Project.

AlgebraicGeometry.SheafOfModules.functorialDifferentials, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialsFunctorial.lean, line 115. The attribute's comment: “the canonical map and uniqueness”.

Stacks 08TR. The canonical morphism on sheaves of relative differentials associated to a commutative square, together with its characterisation on local differentials.

noncomputable def functorialDifferentials {O₁ O₂ O₁' O₂' : Sheaf J CommRingCat.{w}}
    (a : O₁ ⟶ O₂) (a' : O₁' ⟶ O₂') (f₁ : O₁ ⟶ O₁') (f₂ : O₂ ⟶ O₂')
    (sq : a ≫ f₂ = f₁ ≫ a') :
    DifferentialsMapData.{v, u, w, m} a a' f₁ f₂ sq

AlgebraicGeometry.SheafOfModules.mapDifferentials_id_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialsFunctorial.lean, line 183. The attribute's comment: “identity law”.

The canonical map on differentials associated to the identity square is the identity on every local section.

theorem mapDifferentials_id_apply {O₁ O₂ : Sheaf J CommRingCat.{w}} (a : O₁ ⟶ O₂)
    (X : Cᵒᵖ) (x : (moduleOfDifferentialsOfSite.{v, u, w, m} O₁ O₂ a).val.obj X) :
    (mapDifferentials.{v, u, w, m} a a (𝟙 O₁) (𝟙 O₂) (by simp)).val.app X x = x

AlgebraicGeometry.SheafOfModules.mapDifferentials_comp_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialsFunctorial.lean, line 200. The attribute's comment: “composition law”.

Canonical maps on differentials respect composition of commutative squares, on every local section.

theorem mapDifferentials_comp_apply {O₁ O₂ O₁' O₂' O₁'' O₂'' : Sheaf J CommRingCat.{w}}
    (a : O₁ ⟶ O₂) (a' : O₁' ⟶ O₂') (a'' : O₁'' ⟶ O₂'')
    (f₁ : O₁ ⟶ O₁') (f₂ : O₂ ⟶ O₂') (g₁ : O₁' ⟶ O₁'') (g₂ : O₂' ⟶ O₂'')
    (sqf : a ≫ f₂ = f₁ ≫ a') (sqg : a' ≫ g₂ = g₁ ≫ a'')
    (X : Cᵒᵖ) (x : (moduleOfDifferentialsOfSite.{v, u, w, m} O₁ O₂ a).val.obj X) :
    (mapDifferentials.{v, u, w, m} a a'' (f₁ ≫ g₁) (f₂ ≫ g₂)
      (by
        calc
          a ≫ (f₂ ≫ g₂) = (a ≫ f₂) ≫ g₂ := (Category.assoc _ _ _).symm
          _ = (f₁ ≫ a') ≫ g₂ := by rw [sqf]
          _ = f₁ ≫ (a' ≫ g₂) := Category.assoc _ _ _
          _ = f₁ ≫ (g₁ ≫ a'') := by rw [sqg]
          _ = (f₁ ≫ g₁) ≫ a'' := (Category.assoc _ _ _).symm)).val.app X x =
      (mapDifferentials.{v, u, w, m} a' a'' g₁ g₂ sqg).val.app X
        ((mapDifferentials.{v, u, w, m} a a' f₁ f₂ sqf).val.app X x)

Tag 08TS, a lemma

Tag 08TS in the Stacks Project.

Stacks.Sites.Conormal.differentialSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 888. The attribute's comment: “the canonical exact sequence of O'₂-modules”.

The conormal sequence I/I² ⟶ B ⊗_A Ω_{A/R} ⟶ Ω_{B/R} ⟶ 0, with its middle and right terms expressed by the sheaves of relative differentials that corepresent derivations.

noncomputable def differentialSequence :
    ShortComplex
      (_root_.SheafOfModules.{max w u v z} (Stacks.SheafOfModules.Tensor.ringSheaf B))

Stacks.Sites.Conormal.differentialSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 928. The attribute's comment: “exactness at the middle term”. References: SGA 3 III (4.25), “exactness of (+)”.

The transported sequence is exact at the extension of scalars of Ω_{A/R}.

theorem differentialSequence_exact :
    (differentialSequence.{v, u, w, z} J R A B a φ).Exact

Stacks.Sites.Conormal.differentialSequence_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 936. The attribute's comment: “exactness on the right”. References: SGA 3 III (4.25), “surjectivity in (+)”.

The transported sequence surjects onto Ω_{B/R}.

theorem differentialSequence_epi :
    Epi (differentialSequence.{v, u, w, z} J R A B a φ).g

Stacks.Sites.Conormal.differentialSequence_f_class, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 946. The attribute's comment: “the rule f ↦ d f ⊗ 1 for the leftmost map”.

The left-hand map carries the conormal class of a local section of the kernel to the source's d x ⊗ 1.

theorem differentialSequence_f_class (X : Cᵒᵖ) (x : kernelIdeal φ.hom X) :
    ((differentialSequence.{v, u, w, z} J R A B a φ).f.val.app X)
      (conormalClass.{v, u, w, z} J R A B a φ X x) =
      ((_root_.SheafOfModules.pullbackPushforwardAdjunction
        (underlyingRingHomForPullback J A B φ)).unit.app
          (moduleOfDifferentialsOfSite.{v, u, w, z} R A a)).val.app X
        ((universalDerivationOfSite.{v, u, w, z} R A a).d x.1)

Stacks.Sites.Conormal.differentialSequence_g_differential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 962. The attribute's comment: “the right-hand map on local differentials”.

The right-hand map carries d x ⊗ 1 to the universal differential of the image of x.

theorem differentialSequence_g_differential (X : Cᵒᵖ) (x : A.obj.obj X) :
    ((differentialSequence.{v, u, w, z} J R A B a φ).g.val.app X)
      (((_root_.SheafOfModules.pullbackPushforwardAdjunction
        (underlyingRingHomForPullback J A B φ)).unit.app
          (moduleOfDifferentialsOfSite.{v, u, w, z} R A a)).val.app X
        ((universalDerivationOfSite.{v, u, w, z} R A a).d x)) =
      (universalDerivationOfSite.{v, u, w, z} R B (a ≫ φ)).d (φ.hom.app X x)

Stacks.Sites.Conormal.differentialSequence_g_eq_mapDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 982. The attribute's comment: “the map on the right is the one of Stacks 08TR”.

Under extension/restriction of scalars, the right-hand map is exactly the canonical map on relative differentials attached to the square R → A → B by Stacks 08TR.

theorem differentialSequence_g_eq_mapDifferentials :
    (_root_.SheafOfModules.pullbackPushforwardAdjunction
      (underlyingRingHomForPullback J A B φ)).homEquiv
      (moduleOfDifferentialsOfSite.{v, u, w, z} R A a)
        (moduleOfDifferentialsOfSite.{v, u, w, z} R B (a ≫ φ))
        (differentialSequence.{v, u, w, z} J R A B a φ).g =
      mapDifferentials.{v, u, w, z} a (a ≫ φ) (𝟙 R) φ (by simp)

Stacks.Sites.Conormal.differentialSequence_f_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 1010. The attribute's comment: “the rule f ↦ d f ⊗ 1 characterises the leftmost map”.

The formula on local conormal classes determines the left-hand map.

theorem differentialSequence_f_unique
    (g : (differentialSequence.{v, u, w, z} J R A B a φ).X₁ ⟶
      (differentialSequence.{v, u, w, z} J R A B a φ).X₂)
    (hg : ∀ (X : Cᵒᵖ) (x : kernelIdeal φ.hom X),
      g.val.app X (conormalClass.{v, u, w, z} J R A B a φ X x) =
        ((_root_.SheafOfModules.pullbackPushforwardAdjunction
          (underlyingRingHomForPullback J A B φ)).unit.app
            (moduleOfDifferentialsOfSite.{v, u, w, z} R A a)).val.app X
          ((universalDerivationOfSite.{v, u, w, z} R A a).d x.1)) :
    g = (differentialSequence.{v, u, w, z} J R A B a φ).f

Stacks.Sites.Conormal.differentialSequence_X₁_desc_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/CorepresentingConormalSequence.lean, line 1057. The attribute's comment: “the leftmost term is I/I², by its universal property”.

The leftmost term of the sequence is I/I². A morphism of sheaves of O'₂-modules out of it is the same thing as an O₂-linear natural family of maps I(U) ⟶ N(U) out of the kernel ideal: every such family descends to the term, uniquely, by the rule that the conormal class of a local section f of I goes to the value of the family at f. The family annihilates I² automatically, a local section of I acting as zero on a sheaf of O'₂-modules.

theorem differentialSequence_X₁_desc_unique
    (N : _root_.SheafOfModules.{max w u v z} (Stacks.SheafOfModules.Tensor.ringSheaf B))
    (ρ : IdealRestriction.{v, u, w, z} φ N) :
    ∃! g : (differentialSequence.{v, u, w, z} J R A B a φ).X₁ ⟶ N,
      ∀ (X : Cᵒᵖ) (x : kernelIdeal φ.hom X),
        g.val.app X (conormalClass.{v, u, w, z} J R A B a φ X x) = ρ.app X x

Tag 04BP, a lemma

Tag 04BP in the Stacks Project.

Stacks.Sites.SquareZeroExtension.statement₁, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DerivationsSqZeroExtension.lean, line 306. References: EGA 0 (20.1.3), “action of Der”.

Statement 1. For every φ-derivation D, the map s + D : O₂ → A (Definition 5) is again a section of π: it underlies a homomorphism of sheaves of O₁-algebras with π ∘ (s + D) = id.

We express this by producing a Section whose objectwise function is s + D.

theorem statement₁ (s : E.Section) (D : E.Derivation) :
    ∃ s' : E.Section, ∀ (U : Cᵒᵖ) (a : E.O₂.obj U), s'.app U a = E.addDeriv s D U a

Stacks.Sites.SquareZeroExtension.statement₂_bijection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DerivationsSqZeroExtension.lean, line 383. References: EGA 0 (20.1.3), “section case (u = id)”.

Statement 2 (the bijection / torsor). Fixing a section s, the map D ↦ s + D is a bijection from φ-derivations to sections of π, with inverse s' ↦ s' - s. We package the bijection as an explicit Equiv between Der_{O₁}(O₂, F) and the sections of π, characterized on underlying objectwise functions by s + D and s' - s. This exhibits the set of sections of π as a torsor under (an affine space over) Der_{O₁}(O₂, F).

theorem statement₂_bijection (s : E.Section) :
    ∃ e : E.Derivation ≃ E.Section,
      (∀ (D : E.Derivation) (U : Cᵒᵖ) (a : E.O₂.obj U),
        (e D).app U a = E.addDeriv s D U a) ∧
      (∀ (s' : E.Section) (U : Cᵒᵖ) (a : E.O₂.obj U),
        (e.symm s').toFun U a = E.subSection s s' U a)

Tag 04BQ, a definition

Tag 04BQ in the Stacks Project.

AlgebraicGeometry.RingedToposHom.Derivation, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposHomologyZero.lean, line 73. The attribute's comment: “a Y-derivation is an f♯-derivation”. References: EGA IV (16.5.1), “more general”.

Stacks 04BQ, part (1). A Y-derivation D : 𝒪_C ⟶ F with values in a sheaf F of 𝒪_C-modules, for a morphism of ringed topoi (f, f♯) : (Sh(C), 𝒪_C) ⟶ (Sh(D), 𝒪_D): by definition an f♯-derivation, that is, a derivation of 𝒪_C relative to the inverse-image form f♯ : f⁻¹𝒪_D ⟶ 𝒪_C of the structure map.

abbrev Derivation (F : Sheaf.targetModules.{u, v, w} X.J X.O)

AlgebraicGeometry.RingedToposHom.differentials, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposHomologyZero.lean, line 81. The attribute's comment: “the sheaf of differentials”.

Stacks 04BQ, part (2). The sheaf of differentials Ω_{X/Y} = Ω_f = Ω_{𝒪_C/f⁻¹𝒪_D} of a morphism of ringed topoi (f, f♯) : (Sh(C), 𝒪_C) ⟶ (Sh(D), 𝒪_D): the sheaf of differentials of the inverse-image form f⁻¹𝒪_D ⟶ 𝒪_C of its structure map, a sheaf of 𝒪_C-modules on the source site.

noncomputable abbrev differentials : Sheaf.targetModules.{u, v, w} X.J X.O

AlgebraicGeometry.RingedToposHom.universalDerivation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposHomologyZero.lean, line 89. The attribute's comment: “the universal Y-derivation d_{X/Y}”.

Stacks 04BQ. The universal Y-derivation d_{X/Y} : 𝒪_C ⟶ Ω_{X/Y} that the sheaf of differentials comes equipped with: the universal derivation of the inverse-image form of the structure map.

noncomputable def universalDerivation : f.Derivation f.differentials

AlgebraicGeometry.RingedToposHom.existsUnique_descDerivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposHomologyZero.lean, line 97. The attribute's comment: “universality of d_{X/Y}”.

Stacks 04BQ. d_{X/Y} is universal among Y-derivations: every Y-derivation with values in a sheaf of 𝒪_C-modules factors through it by a unique morphism of sheaves of modules.

theorem existsUnique_descDerivation (F : Sheaf.targetModules.{u, v, w} X.J X.O)
    (D : f.Derivation F) :
    ∃! g : f.differentials ⟶ F, (f.universalDerivation).postcomp g.val = D

Tag 04BR, a lemma

Tag 04BR in the Stacks Project.

Stacks.Sheaves.Differentials.statement3_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialsComparisonMap.lean, line 420. References: EGA 0 (20.5.2), “(20.5.2.4) & (20.5.2.6)”; EGA IV (16.4.3), “(16.4.3.6),(16.4.3.7)”.

Statement 3 (characterization and uniqueness of c_f).

The comparison map c_f : f^* Ω_{X/Y} ⟶ Ω_{X'/Y'} is uniquely characterized by the local-section property of Statement 3 (corrected formulation): c_f ∘ (f^* d_{X/Y}(t)) = d_{X'/Y'} ∘ (f^* t) as maps f⁻¹ h_U^# ⟶ Ω_{X'/Y'}.

We state this directly in terms of c_f (not its adjoint transpose): for every object U and every local section t ∈ O_X(U), c_f sends the pulled-back universal section f^* d_{X/Y}(t) (the image of d_{X/Y}(t) under the adjunction unit, i.e. MorphismOverBase.pullbackDiff, lying in (f^* Ω_{X/Y})(Ff U)) to d_{X'/Y'}(f♯ t) (the local section d_{X'/Y'} ∘ (f^* t) evaluated at Ff U). Here c_f acts via its component c_f.val.app (Ff U) : (f^* Ω_{X/Y})(Ff U) ⟶ Ω_{X'/Y'}(Ff U), so the left-hand side is literally c_f composed with the pulled-back section f^* d_{X/Y}(t).

Uniqueness holds because the local sections d_{X/Y}(t) generate Ω_{X/Y} as an O_X-module, so the sections f^* d_{X/Y}(t) generate f^* Ω_{X/Y} as an O_{X'}-module (Stacks Tag 04BR).

theorem statement3_unique :
    ∃! cf : f.pullΩ ⟶ X'.Ω,
      ∀ (U : X.Cᵒᵖ) (t : X.ringSheaf'.obj.obj U),
        (cf.val.app (f.Ff.op.obj U)).hom (f.pullbackDiff U t)
          = (X'.d.app (f.Ff.op.obj U)).d (f.fsharpApp U t)

Sources

• Section 18.33, Tag 04BJ
• AxiomMath/Stacks at 5ed82d14

LeanPresheafOfModulesOfCommRing.Derivation' · Stacks.Sheaves.Differentials.universalDerivation_isUniversal · AlgebraicGeometry.SheafOfModules.existsUnique_descDerivation · AlgebraicGeometry.SheafOfModules.derivationsFunctor_isCorepresentable · AlgebraicGeometry.SheafOfModules.moduleDifferentialsRelationMap · AlgebraicGeometry.SheafOfModules.moduleDifferentialsRelationMap_additive · AlgebraicGeometry.SheafOfModules.moduleDifferentialsRelationMap_leibniz · AlgebraicGeometry.SheafOfModules.moduleDifferentialsRelationMap_base

Section18.34 Finite order differential operators#

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

Tag 09CR, a definition

Tag 09CR in the Stacks Project.

Declarations registered for the tag:

• DiffOp.IsGlobalDiffOpOfOrder, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialOperators.lean, line 71 (StacksFrontier).

Tag 09CS, a lemma

Tag 09CS in the Stacks Project.

DiffOp.isGlobalDiffOpOfOrder_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialOperatorsOrder.lean, line 523. References: EGA IV (16.8.9), “more general”; EGA IV (16.8.10), “more general”; SGA 3 VIIA (1.2), “sheaf, deviations of id”; SGA 3 VIIA (1.4), “partial”; SGA 6 II (AppII.1.2.4), “more general”.

The composition of a differential operator of order k with a differential operator of order k' is a differential operator of order k + k'.

The argument: IsGlobalDiffOpOfOrder is ∀ U, IsDiffOpOfOrder on restrict; by GlobalOp.restrict_comp the restriction of the composite is the raw composite of the restrictions; then apply the raw composition lemma isDiffOpOfOrder_comp_raw (strong induction on k + k' via the commutator-of-composition identity).

theorem isGlobalDiffOpOfOrder_comp (φ : O₁ ⟶ O₂)
    {E F G : SheafOfModules O₂} {k k' : ℕ}
    (D : GlobalOp E F) (D' : GlobalOp F G)
    (hD : IsGlobalDiffOpOfOrder φ k D) (hD' : IsGlobalDiffOpOfOrder φ k' D') :
    IsGlobalDiffOpOfOrder φ (k + k') (D'.comp D)

Tag 09CT, a lemma

Tag 09CT in the Stacks Project.

AlgebraicGeometry.SheafOfModules.existsUnique_descDiffOp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PrincipalPartsUniversal.lean, line 187. The attribute's comment: “unique-factorization form”. References: EGA IV (16.8.3), “(16.8.3.1)”; SGA 6 II (AppII.1.2.3); SGA 6 II (AppII.1.2.2), “(1.2.2.1)”.

Stacks 09CT, in unique-factorization form: every differential operator of order at most k out of F factors through the universal one by a unique morphism of sheaves of modules.

theorem existsUnique_descDiffOp
    (F G : _root_.SheafOfModules.{max u v w m} O₂) (k : ℕ)
    (D : DiffOp.GlobalOp F G) (hD : DiffOp.IsGlobalDiffOpOfOrder phi k D) :
    ∃! f : moduleOfPrincipalParts.{v, u, w, m} phi F k ⟶ G,
      postcomp (universalDiffOp.{v, u, w, m} phi F k) f = D

AlgebraicGeometry.SheafOfModules.differentialOperatorsFunctor_isCorepresentable, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/DifferentialOperators.lean, line 571. References: EGA IV (16.8.3), “(16.8.3.1)”; SGA 6 II (AppII.1.2.3); SGA 6 II (AppII.1.2.2), “(1.2.2.1)”.

Differential operators of order at most k out of a fixed module sheaf are represented by a sheaf of modules (the sheaf of principal parts).

noncomputable instance differentialOperatorsFunctor_isCorepresentable (phi : O₁ ⟶ O₂)
    (F : _root_.SheafOfModules.{max u v w m} O₂) (k : ℕ) :
    (differentialOperatorsFunctor.{v, u, w, m} phi F k).IsCorepresentable

Tag 09CU, a definition

Tag 09CU in the Stacks Project.

AlgebraicGeometry.SheafOfModules.moduleOfPrincipalParts, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PrincipalPartsUniversal.lean, line 164. The attribute's comment: “the module of principal parts of order k”. References: SGA 6 II (AppII.1.2.2), “P^n_{X/S}(E)”.

The sheaf of principal parts Pᵏ_{O₂/O₁}(F): the sheaf of modules corepresenting the functor of differential operators of order at most k out of F.

noncomputable abbrev moduleOfPrincipalParts
    (F : _root_.SheafOfModules.{max u v w m} O₂) (k : ℕ) :
    _root_.SheafOfModules.{max u v w m} O₂

Tag 09CV, a lemma

Tag 09CV in the Stacks Project.

Stacks.Sheaves.PrincipalParts.principalPartsSheafification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsSheafification.lean, line 697. References: EGA IV (16.4.24), “(ii)”.

Stacks Project, Tag 0G3U, which read as a statement about the sheaf of principal parts is Tag 09CV. Let φ : O₁ ⟶ O₂ be a morphism of presheaves of commutative rings on a site and let F be a presheaf of O₂-modules. Then the sheaf of principal parts of order k of F^# relative to O₂^# / O₁^# is the sheaf associated to the presheaf X ↦ Pᵏ_{O₂(X)/O₁(X)}(F X) of sectionwise modules of principal parts, and the sectionwise universal operators are compatible with restriction.

noncomputable def principalPartsSheafification [HasWeakSheafify J CommRingCat.{u}]
    [J.WEqualsLocallyBijective CommRingCat.{u}]
    [J.HasSheafCompose (forget₂ CommRingCat.{u} RingCat.{u})]
    [J.WEqualsLocallyBijective AddCommGrpCat.{max u u₁ v₁ v}]
    [HasWeakSheafify J AddCommGrpCat.{max u u₁ v₁ v}] {O₁ O₂ : Cᵒᵖ ⥤ CommRingCat.{u}}
    (φ : O₁ ⟶ O₂)
    (F : PresheafOfModules.{max u u₁ v₁ v} (O₂ ⋙ forget₂ CommRingCat.{u} RingCat.{u}))
    (k : ℕ) :
    Σ' P : PresheafOfModules.{max u u₁ v₁ v}
        (O₂ ⋙ forget₂ CommRingCat.{u} RingCat.{u}),
      Σ' D : F.presheaf ⟶ P.presheaf,
        Σ' _e : (AlgebraicGeometry.SheafOfModules.differentialOperatorsFunctor.{v₁, u₁, u,
            max u u₁ v₁ v}
            ((sheafCompose J (forget₂ CommRingCat.{u} RingCat.{u})).map
              (associatedCommRingSheafMap J φ))
            ((PresheafOfModules.sheafification (toAssociatedRingSheaf J O₂)).obj F)
            k).coreprX (hF :=
              AlgebraicGeometry.SheafOfModules.differentialOperatorsFunctor_isCorepresentable
                ((sheafCompose J (forget₂ CommRingCat.{u} RingCat.{u})).map
                  (associatedCommRingSheafMap J φ))
                ((PresheafOfModules.sheafification (toAssociatedRingSheaf J O₂)).obj F) k) ≅
          (PresheafOfModules.sheafification (toAssociatedRingSheaf J O₂)).obj P,
        ∀ X : Cᵒᵖ,
          letI : Algebra (O₁.obj X) (O₂.obj X) := (φ.app X).hom.toAlgebra
          letI : Module (O₁.obj X) (F.obj X) :=
            Module.compHom (F.obj X) (φ.app X).hom
          letI : Module (O₁.obj X) (P.obj X) :=
            Module.compHom (P.obj X) (φ.app X).hom
          letI : IsScalarTower (O₁.obj X) (O₂.obj X) (F.obj X) :=
            IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
          letI : IsScalarTower (O₁.obj X) (O₂.obj X) (P.obj X) :=
            IsScalarTower.of_algebraMap_smul fun _ _ ↦ rfl
          ∃ d : F.obj X →ₗ[O₁.obj X] P.obj X,
            (∀ x, d x = (D.app X).hom x) ∧
              d.IsUniversalDifferentialOperatorOfOrderLE (O₂.obj X) k

Tag 09CW, a lemma

Tag 09CW in the Stacks Project.

AlgebraicGeometry.SheafOfModules.exists_shortExact_principalPartsSequence', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsJet.lean, line 1178. The attribute's comment: “field 8 ALONE: the short exact sequence of the principal-parts sequence, now”. References: SGA 6 II (AppII.1.2.4), “n = 1”.

The sequence of principal parts is a short exact sequence.

theorem exists_shortExact_principalPartsSequence' :
    ∃ h : (principalPartsInclusion.{v, u, w, m} φ).app F ≫
        (principalPartsProjection.{v, u, w, m}
          (underlyingRingSheafMapOfSite φ) 1).app F = 0,
      (ShortComplex.mk ((principalPartsInclusion.{v, u, w, m} φ).app F)
        ((principalPartsProjection.{v, u, w, m}
          (underlyingRingSheafMapOfSite φ) 1).app F) h).ShortExact

AlgebraicGeometry.SheafOfModules.principalPartsSequence_nonempty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsSequenceStructure.lean, line 190. The attribute's comment: “the tag's OWN assertion: a functorial first-principal-parts sequence exists, i.e. the eight-field record is inhabited. The individual clauses of field 8 are carried separately in PrincipalPartsJet.lean and PrincipalPartsSequence.lean.”. References: SGA 6 II (AppII.1.2.4), “n = 1”.

The functorial short exact sequence of first principal parts exists.

theorem principalPartsSequence_nonempty (O₁ O₂ : Sheaf J CommRingCat.{w})
    (φ : O₁ ⟶ O₂) : Nonempty (PrincipalPartsSequence.{v, u, w, m} O₁ O₂ φ)

Tag 09CX, a remark

Tag 09CX in the Stacks Project.

AlgebraicGeometry.SheafOfModules.principalPartsMapOfSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsChangeOfRings.lean, line 255. The attribute's comment: “maps”.

Stacks 09CX. The map on order-k principal parts induced by a commutative square of sheaves of rings together with a compatible linear map of module sheaves.

noncomputable def principalPartsMapOfSquare
    (φ : A ⟶ B) (φ' : A' ⟶ B') (α : A ⟶ A') (β : B ⟶ B')
    (h : φ ≫ β = α ≫ φ')
    (F : _root_.SheafOfModules.{max u v w m} B)
    (F' : _root_.SheafOfModules.{max u v w m} B')
    (uF : F ⟶ (_root_.SheafOfModules.restrictScalars.{max u v w m} β).obj F')
    (k : ℕ) :
    moduleOfPrincipalParts.{v, u, w, m} φ F k ⟶
      (_root_.SheafOfModules.restrictScalars.{max u v w m} β).obj
        (moduleOfPrincipalParts.{v, u, w, m} φ' F' k)

AlgebraicGeometry.SheafOfModules.principalPartsMapOfSquare_universalOperator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsChangeOfRings.lean, line 282. The attribute's comment: “maps”.

The induced map sends each universal local generator to the generator associated to its image under the module map.

theorem principalPartsMapOfSquare_universalOperator (k : ℕ) (X : Cᵒᵖ) (s : F.val.obj X) :
    ((principalPartsMapOfSquare φ φ' α β h F F' uF k).val.app X).hom
      ((differentialOperatorsFunctor.{v, u, w, m} φ F k).coreprx.1 X s) =
      (differentialOperatorsFunctor.{v, u, w, m} φ' F' k).coreprx.1 X
        ((uF.val.app X).hom s)

AlgebraicGeometry.SheafOfModules.principalPartsMapOfSquare_comp_orderReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsChangeOfRings.lean, line 323. The attribute's comment: “maps”.

The induced maps commute with the canonical maps reducing the order from k + 1 to k.

theorem principalPartsMapOfSquare_comp_orderReduction (k : ℕ) :
    principalPartsOrderReduction.{v, u, w, m} φ F k ≫
        principalPartsMapOfSquare φ φ' α β h F F' uF k =
      principalPartsMapOfSquare φ φ' α β h F F' uF (k + 1) ≫
        (_root_.SheafOfModules.restrictScalars.{max u v w m} β).map
          (principalPartsOrderReduction.{v, u, w, m} φ' F' k)

AlgebraicGeometry.SheafOfModules.principalPartsMapOfSquare_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsChangeOfRings.lean, line 407. The attribute's comment: “composition of the maps”.

Stacks 09CX. The map on principal parts associated to two successive compatible squares is the composite of their maps on principal parts.

theorem principalPartsMapOfSquare_comp
    (φ : A ⟶ B) (φ' : A' ⟶ B') (φ'' : A'' ⟶ B'')
    (α : A ⟶ A') (β : B ⟶ B')
    (α' : A' ⟶ A'') (β' : B' ⟶ B'')
    (h : φ ≫ β = α ≫ φ') (h' : φ' ≫ β' = α' ≫ φ'')
    (F : _root_.SheafOfModules.{max u v w m} B)
    (F' : _root_.SheafOfModules.{max u v w m} B')
    (F'' : _root_.SheafOfModules.{max u v w m} B'')
    (uF : F ⟶ (_root_.SheafOfModules.restrictScalars.{max u v w m} β).obj F')
    (uF' : F' ⟶ (_root_.SheafOfModules.restrictScalars.{max u v w m} β').obj F'')
    (k : ℕ) :
    principalPartsMapOfSquare.{v, u, w, m} φ φ'' (α ≫ α') (β ≫ β')
        (by rw [← Category.assoc, h, Category.assoc, h', ← Category.assoc])
        F F'' (uF ≫ (_root_.SheafOfModules.restrictScalars.{max u v w m} β).map uF') k =
      principalPartsMapOfSquare.{v, u, w, m} φ φ' α β h F F' uF k ≫
        (_root_.SheafOfModules.restrictScalars.{max u v w m} β).map
          (principalPartsMapOfSquare.{v, u, w, m} φ' φ'' α' β' h' F' F'' uF' k)

AlgebraicGeometry.SheafOfModules.principalPartsSequence_naturality_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsSequenceNaturality.lean, line 280. The attribute's comment: “sequence naturality: the projection square”.

Stacks 09CX. The change-of-rings maps on first principal parts are compatible with the projections of the short exact sequences of Tag 09CW: the right-hand square of the naturality diagram commutes, the comparison of its two right-hand terms being uF.

theorem principalPartsSequence_naturality_projection
    (φ : O₁ ⟶ O₂) (φ' : O₁' ⟶ O₂') (α : O₁ ⟶ O₁') (β : O₂ ⟶ O₂')
    (hsq : φ ≫ β = α ≫ φ')
    (F : _root_.SheafOfModules.{max u v w m} (Stacks.SheafOfModules.Tensor.ringSheaf O₂))
    (F' : _root_.SheafOfModules.{max u v w m} (Stacks.SheafOfModules.Tensor.ringSheaf O₂'))
    (uF : F ⟶ (_root_.SheafOfModules.restrictScalars.{max u v w m}
      (underlyingRingSheafMapOfSite β)).obj F') :
    principalPartsSquareMap.{v, u, w, m} φ φ' α β hsq F F' uF ≫
        (_root_.SheafOfModules.restrictScalars.{max u v w m}
          (underlyingRingSheafMapOfSite β)).map
          ((principalPartsProjection.{v, u, w, m}
            (underlyingRingSheafMapOfSite φ') 1).app F') =
      (principalPartsProjection.{v, u, w, m}
        (underlyingRingSheafMapOfSite φ) 1).app F ≫ uF

AlgebraicGeometry.SheafOfModules.principalPartsSequence_naturality_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/PrincipalPartsSequenceNaturality.lean, line 658. The attribute's comment: “sequence naturality: the inclusion square”.

Stacks 09CX. The change-of-rings maps on first principal parts are compatible with the inclusions of the short exact sequences of Tag 09CW: the left-hand square of the naturality diagram commutes, with the tensor product of uF and the map on differentials on the left.

theorem principalPartsSequence_naturality_inclusion
    (φ : O₁ ⟶ O₂) (φ' : O₁' ⟶ O₂') (α : O₁ ⟶ O₁') (β : O₂ ⟶ O₂') (hsq : φ ≫ β = α ≫ φ')
    (F : _root_.SheafOfModules.{max u v w m} (Stacks.SheafOfModules.Tensor.ringSheaf O₂))
    (F' : _root_.SheafOfModules.{max u v w m} (Stacks.SheafOfModules.Tensor.ringSheaf O₂'))
    (uF : F ⟶ (_root_.SheafOfModules.restrictScalars.{max u v w m}
      (underlyingRingSheafMapOfSite β)).obj F') :
    (principalPartsInclusion.{v, u, w, m} φ).app F ≫
        principalPartsSquareMap.{v, u, w, m} φ φ' α β hsq F F' uF =
      differentialsTensorMap.{v, u, w, m} φ φ' α β hsq F F' uF ≫
        (_root_.SheafOfModules.restrictScalars.{max u v w m}
          (underlyingRingSheafMapOfSite β)).map
          ((principalPartsInclusion.{v, u, w, m} φ').app F')

Sources

• Section 18.34, Tag 09CQ
• AxiomMath/Stacks at 5ed82d14

LeanDiffOp.IsGlobalDiffOpOfOrder · DiffOp.isGlobalDiffOpOfOrder_comp · AlgebraicGeometry.SheafOfModules.existsUnique_descDiffOp · AlgebraicGeometry.SheafOfModules.differentialOperatorsFunctor_isCorepresentable · AlgebraicGeometry.SheafOfModules.moduleOfPrincipalParts · Stacks.Sheaves.PrincipalParts.principalPartsSheafification · AlgebraicGeometry.SheafOfModules.exists_shortExact_principalPartsSequence' · AlgebraicGeometry.SheafOfModules.principalPartsSequence_nonempty

Section18.35 The naive cotangent complex#

Section 18.35 of the Stacks Project, Tag 08TT. 7 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08TU, an equation

Tag 08TU in the Stacks Project.

Stacks.Sites.FreeAlgebra.canonicalPresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FreeAlgebraSheaf.lean, line 154. The attribute's comment: “the canonical morphism”.

Stacks 08TU. The canonical morphism A[B] → B.

noncomputable def canonicalPresentation (A B : Sheaf J CommRingCat.{w}) (a : A ⟶ B) :
    freeAlgebraSheaf J A (underlyingPresheaf J B) ⟶ B

Stacks.Sites.FreeAlgebra.canonicalPresentation_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FreeAlgebraSheaf.lean, line 193. The attribute's comment: “evaluation on coefficients and variables”.

The canonical presentation is induced by coefficient evaluation and [b] ↦ b.

theorem canonicalPresentation_spec (A B : Sheaf J CommRingCat.{w}) (a : A ⟶ B) :
    (toSheafification J CommRingCat.{w}).app
        (polynomialPresheaf J A (underlyingPresheaf J B)) ≫
      (sheafToPresheaf J CommRingCat.{w}).map (canonicalPresentation J A B a) =
        canonicalEvaluation J A B a

Stacks.Sites.FreeAlgebra.canonicalPresentation_comp_coefficientMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FreeAlgebraSheaf.lean, line 202. The attribute's comment: “compatibility with the A-algebra structures”.

The canonical presentation A[B] → B respects the structural maps from A.

theorem canonicalPresentation_comp_coefficientMap
    (A B : Sheaf J CommRingCat.{w}) (a : A ⟶ B) :
    freeAlgebraSheafCoefficientMap J A (underlyingPresheaf J B) ≫
      canonicalPresentation J A B a = a

Stacks.Sites.FreeAlgebra.canonicalPresentation_isLocallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FreeAlgebraSheaf.lean, line 211. The attribute's comment: “surjectivity”.

The canonical presentation A[B] → B is surjective as a morphism of sheaves.

theorem canonicalPresentation_isLocallySurjective
    (A B : Sheaf J CommRingCat.{w}) (a : A ⟶ B) :
    Presheaf.IsLocallySurjective J
      (Functor.whiskerRight
        ((sheafToPresheaf J CommRingCat.{w}).map (canonicalPresentation J A B a))
        (forget CommRingCat.{w}))

Tag 08TV, an equation

Tag 08TV in the Stacks Project.

Stacks.SheafOfModules.canonicalConormalSequence, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangent.lean, line 87. The attribute's comment: “the canonical map is the left-hand map of this sequence”.

The conormal sequence for the canonical polynomial presentation of B over A. Its first two terms are I/I² and B ⊗[A[B]] Ω[A[B]/A].

noncomputable abbrev canonicalConormalSequence
    (A B : Sheaf J CommRingCat.{w}) (a : A ⟶ B) :
    ShortComplex
      (_root_.SheafOfModules.{max w u v z} (Stacks.SheafOfModules.Tensor.ringSheaf B))

Tag 08TW, a definition

Tag 08TW in the Stacks Project.

Stacks.SheafOfModules.naiveCotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangent.lean, line 107. References: SGA 6 0 (4.4), “NL_{B/A} construction”.

Stacks 08TW. The naive cotangent complex of B over A, with I/I² in degree -1 and B ⊗[A[B]] Ω[A[B]/A] in degree 0. This two-term complex is the one displayed in Stacks 08TI, and 08TJ names it for a morphism of sheaves of rings.

noncomputable def naiveCotangentComplex
    (A B : Sheaf J CommRingCat.{w}) (a : A ⟶ B) :
    CochainComplex
      (_root_.SheafOfModules.{max w u v z} (Stacks.SheafOfModules.Tensor.ringSheaf B)) ℤ

Tag 08TX, an equation

Tag 08TX in the Stacks Project.

Stacks.SheafOfModules.freeAlgebraMapOfSquare_comp_canonicalPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangentSquare.lean, line 176. The attribute's comment: “the canonical map A[B] ⟶ A'[B'] attached to the square”.

The morphism A[B] ⟶ A'[B'] attached to a commutative square is compatible with the two canonical presentations.

theorem freeAlgebraMapOfSquare_comp_canonicalPresentation :
    canonicalFreeAlgebraMapOfSquare J A A' B B' f β ≫
        Stacks.Sites.FreeAlgebra.canonicalPresentation J A' B' a' =
      Stacks.Sites.FreeAlgebra.canonicalPresentation J A B a ≫ β

Stacks.SheafOfModules.naiveCotangentComplexMapOfSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangentSquare.lean, line 312. The attribute's comment: “the canonical B-linear map of complexes NL_{B/A} ⟶ NL_{B'/A'}”.

Stacks 08TX. The canonical B-linear chain map NL_{B/A} ⟶ NL_{B'/A'} attached to a commutative square of sheaves of rings: it is the map of conormal sheaves in degree -1 and the map of the scalar extensions of the differentials in degree 0.

noncomputable def naiveCotangentComplexMapOfSquare :
    naiveCotangentComplex.{v, u, w, z} J A B a ⟶
      ((_root_.SheafOfModules.restrictScalars.{max w u v z}
          (underlyingRingHomOfSite β)).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (naiveCotangentComplex.{v, u, w, z} J A' B' a')

Stacks.SheafOfModules.naiveCotangentComplexMapOfSquare_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangentSquare.lean, line 608. The attribute's comment: “compatibility of the canonical map of complexes with compositions”.

Stacks 08TX. The canonical chain map attached to a commutative square of sheaves of rings is compatible with compositions: given a commutative diagram

B ──β──▸ B' ──β'──▸ B''
▲         ▲          ▲
a         a'         a''
│         │          │
A ──f──▸ A' ──f'──▸ A''

the composition NL_{B/A} ⟶ NL_{B'/A'} ⟶ NL_{B''/A''} is the map attached to the outer rectangle. The target of the composite is the iterated restriction of scalars along β and β', which is the restriction of scalars along β ≫ β'.

theorem naiveCotangentComplexMapOfSquare_comp :
    naiveCotangentComplexMapOfSquare.{v, u, w, z} J A B a A' B' a' f β hsq ≫
        ((_root_.SheafOfModules.restrictScalars.{max w u v z}
            (underlyingRingHomOfSite β)).mapHomologicalComplex (ComplexShape.up ℤ)).map
          (naiveCotangentComplexMapOfSquare.{v, u, w, z} J A' B' a' A'' B'' a'' f' β' hsq') =
      naiveCotangentComplexMapOfSquare.{v, u, w, z} J A B a A'' B'' a'' (f ≫ f') (β ≫ β')
        (square_comp hsq hsq')

Tag 08TY, a lemma

Tag 08TY in the Stacks Project.

Stacks.SheafOfModules.naiveCotangentComplexComparison_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangent.lean, line 614. The attribute's comment: “normalisation: the canonical comparison map is the identity at the canonical presentation”.

Stacks 08TY, normalisation at the canonical presentation. The canonical presentation is the one whose family of generators is the identity of B, and there the comparison map NL(α) ⟶ NL_{B/A} is the identity; so the identification of NL(α) with NL_{B/A} is the identity for α = id_B.

theorem naiveCotangentComplexComparison_id :
    naiveCotangentComplexComparison.{v, u, w, z} J A B a
      (Stacks.Sites.FreeAlgebra.underlyingPresheaf J B) (𝟙 _) = 𝟙 _

Stacks.SheafOfModules.naiveCotangentComplexComparison_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangent.lean, line 735. The attribute's comment: “canonicality: the comparison maps are compatible with every morphism of presentations”.

Stacks 08TY, compatibility with functorialities. The comparison maps NL(α) ⟶ NL_{B/A} of two polynomial presentations of B over A are compatible with every morphism of presentations between them, so the identification of NL(α) with NL_{B/A} is canonical.

theorem naiveCotangentComplexComparison_naturality :
    presentationNaiveCotangentComplexMap.{v, u, w, z} J A E₁ E₂ h B a α₁ α₂ hα ≫
        naiveCotangentComplexComparison.{v, u, w, z} J A B a E₂ α₂ =
      naiveCotangentComplexComparison.{v, u, w, z} J A B a E₁ α₁

Stacks.SheafOfModules.presentationNaiveCotangentComplexHomologyZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangent.lean, line 800. The attribute's comment: “degree 0 of the canonical isomorphism: H⁰(NL(α)) is Ω_{B/A} for every presentation”.

Stacks 08TY in degree 0. For every polynomial presentation α : E ⟶ B of B over A the degree 0 cohomology sheaf of NL(α) is the sheaf of relative differentials Ω_{B/A}, one and the same sheaf of B-modules for all α; in particular it agrees with the degree 0 cohomology sheaf of NL_{B/A}, which is the case α = id_B.

noncomputable def presentationNaiveCotangentComplexHomologyZeroIso :
    (presentationNaiveCotangentComplex.{v, u, w, z} J A B a E α).homology 0 ≅
      moduleOfDifferentialsOfSite.{v, u, w, z} A B a

Stacks.SheafOfModules.isIso_cokernel_map_presentationConormalSequence_f, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/NaiveCotangent.lean, line 834. The attribute's comment: “degree 0: a morphism of presentations induces an isomorphism on H⁰”.

Stacks 08TY in degree 0, for the comparison map. A morphism of polynomial presentations induces an isomorphism on the degree 0 cohomology sheaves of the two naive cotangent complexes, these being the cokernels of the two conormal maps: both are Ω_{B/A} and the induced map is the identity there.

theorem isIso_cokernel_map_presentationConormalSequence_f :
    IsIso (cokernel.map
      (presentationConormalSequence.{v, u, w, z} J A B a E₁ α₁).f
      (presentationConormalSequence.{v, u, w, z} J A B a E₂ α₂).f
      (presentationConormalMap.{v, u, w, z} J A E₁ E₂ h B a α₁ α₂ hα)
      (presentationTensorMap.{v, u, w, z} J A E₁ E₂ h B a α₁ α₂ hα)
      (Stacks.Sites.Conormal.conormalSequence_f_naturality.{v, u, w, z} J A B
        (Stacks.Sites.FreeAlgebra.freeAlgebraSheaf J A E₁)
        (Stacks.Sites.FreeAlgebra.freeAlgebraSheaf J A E₂)
        (Stacks.Sites.FreeAlgebra.freeAlgebraSheafCoefficientMap J A E₁)
        (Stacks.Sites.FreeAlgebra.freeAlgebraSheafCoefficientMap J A E₂)
        (presentation J A B a E₁ α₁) (presentation J A B a E₂ α₂)
        (freeAlgebraMap J A E₁ E₂ h)
        (freeAlgebraMap_comp_presentation J A E₁ E₂ h B a α₁ α₂ hα)
        (freeAlgebraSheafCoefficientMap_comp_freeAlgebraMap J A E₁ E₂ h)))

Stacks.SheafOfModules.quasiIso_naiveCotangentComplexComparison_site, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/NaiveCotangentPresentationComparison.lean, line 159. The attribute's comment: “the canonical isomorphism NL(α) ≅ NL_{B/A} in D(B): the comparison map of a polynomial presentation is a quasi-isomorphism”.

Stacks 08TY. For every polynomial presentation α : E ⟶ B of B over A the canonical comparison map NL(α) ⟶ NL_{B/A} is a quasi-isomorphism, so NL(α) and NL_{B/A} are canonically isomorphic in the derived category of B-modules: the naive cotangent complex does not depend on the presentation.

The comparison map is the chain map of the morphism of presentations α : (E, α) ⟶ (B, id), so this is Stacks.SheafOfModules.quasiIso_presentationNaiveCotangentComplexMap at the canonical presentation.

theorem quasiIso_naiveCotangentComplexComparison_site :
    QuasiIso (naiveCotangentComplexComparison.{v, u, w, z} J A B a E α)

Tag 08TZ, a lemma

Tag 08TZ in the Stacks Project.

Stacks.Sheaves.RingedToposModules.inverseImageConormalIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ConormalInverseImage.lean, line 1021. The attribute's comment: “the degree -1 term, for an arbitrary locally surjective homomorphism of sheaves of rings, of which the conormal term of the tag is the instance at the canonical polynomial presentation. The instantiation is Stacks.SheafOfModules.inverseImageNaiveCotangentNegOneIso and the isomorphism of complexes is Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso”.

The inverse image of the conormal sheaf is the conormal sheaf of the inverse image: f⁻¹(ℐ/ℐ²) ≅ ℐ'/(ℐ')², where ℐ = Ker φ and ℐ' = Ker(f⁻¹φ). This is the degree -1 term of the identification f⁻¹ NL_{ℬ/𝒜} = NL_{f⁻¹ℬ/f⁻¹𝒜} of Stacks 08TZ.

noncomputable def inverseImageConormalIso :
    (inverseImageCommModules.{w, w', v, u, v', u'} f B).obj
        (conormalModule.{w', v', u'} K φ) ≅
      conormalModule.{w, v, u} J (f.inverseImageRing.map φ)

Stacks.Sites.FreeAlgebra.inverseImageFreeAlgebraHom_comp_canonicalPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/NaiveCotangentInverseImage.lean, line 407. The attribute's comment: “the inverse image of the canonical polynomial presentation is the canonical polynomial presentation of the inverse image, from which both terms of the complex are built”.

Stacks Project, Tag 08TZ. The inverse image of the canonical polynomial presentation A[B] ⟶ B is the canonical polynomial presentation (f⁻¹A)[f⁻¹B] ⟶ f⁻¹B of the inverse-image homomorphism of sheaves of commutative rings.

theorem inverseImageFreeAlgebraHom_comp_canonicalPresentation (a : A ⟶ B) :
    inverseImageFreeAlgebraHom f A B ≫
        canonicalPresentation J (f.inverseImageRing.obj A) (f.inverseImageRing.obj B)
          (f.inverseImageRing.map a) =
      f.inverseImageRing.map (canonicalPresentation K A B a)

Stacks.SheafOfModules.inverseImageNaiveCotangentZeroHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/NaiveCotangentInverseImage.lean, line 675. The attribute's comment: “the degree 0 term: its inverse image and the degree 0 term of the inverse image represent the same functor of derivations. Naturality of this bijection is inverseImageNaiveCotangentZeroHomEquiv_naturality and the resulting isomorphism of degree 0 terms is inverseImageNaiveCotangentZeroIso; the isomorphism of complexes assembled from it is Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso”.

Stacks Project, Tag 08TZ. The inverse image of the degree-0 term of the naive cotangent complex of a and the degree-0 term of the naive cotangent complex of f⁻¹a have the same morphisms into every sheaf of f⁻¹B-modules: both represent the f⁻¹A-derivations of the canonical polynomial presentation of f⁻¹B over f⁻¹A.

noncomputable def inverseImageNaiveCotangentZeroHomEquiv
    (M : _root_.SheafOfModules.{max u v w}
      (Stacks.SheafOfModules.Tensor.ringSheaf (f.inverseImageRing.obj B))) :
    ((inverseImageModules f
        ((Stacks.SheafOfModules.Tensor.ringSheaf.{u', v', max u' v' w'} (J := K)) B)).obj
        (canonicalConormalSequence.{v', u', max u' v' w', max u' v' w'} K A B a).X₂ ⟶ M) ≃
      ((canonicalConormalSequence.{v, u, max u v w, max u v w} J (f.inverseImageRing.obj A)
        (f.inverseImageRing.obj B) (f.inverseImageRing.map a)).X₂ ⟶ M)

Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/NaiveCotangentInverseImageComplex/CommutingSquare.lean, line 677. The attribute's comment: “the inverse image of the naive cotangent complex is the naive cotangent complex of the inverse image, as an isomorphism of complexes: the identification the tag states, assembled from the degree -1 and the degree 0 comparison and their commutation with the conormal differentials”.

The inverse image of the naive cotangent complex is the naive cotangent complex of the inverse image: f⁻¹ NL_{B/A} ≅ NL_{f⁻¹B/f⁻¹A}, as an isomorphism of two-term complexes of sheaves of f⁻¹B-modules, with the identification of the degree -1 terms in degree -1 and the identification of the degree 0 terms in degree 0.

noncomputable def inverseImageNaiveCotangentComplexIso :
    ((inverseImageTargetModules.{u, v, w, u', v', w'} J K f
            (B := B)).mapHomologicalComplex (ComplexShape.up ℤ)).obj
        (naiveCotangentComplex.{v', u', max u' v' w', max u' v' w'} K A B a) ≅
      naiveCotangentComplex.{v, u, max u v w, max u v w} J (f.inverseImageRing.obj A)
        (f.inverseImageRing.obj B) (f.inverseImageRing.map a)

Stacks.SheafOfModules.inverseImageNaiveCotangentZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/NaiveCotangentInverseImageNaturality.lean, line 557. The attribute's comment: “the degree 0 term as an isomorphism, obtained from naturality of the corepresentability bijection by Yoneda. The degree -1 term is inverseImageConormalIso and the isomorphism of complexes assembled from the two is Stacks.SheafOfModules.inverseImageNaiveCotangentComplexIso”.

The inverse image of the degree-0 term of the naive cotangent complex is the degree-0 term of the naive cotangent complex of the inverse image: f⁻¹(B ⊗_{A[B]} Ω_{A[B]/A}) ≅ f⁻¹B ⊗_{(f⁻¹A)[f⁻¹B]} Ω_{(f⁻¹A)[f⁻¹B]/f⁻¹A}.

noncomputable def inverseImageNaiveCotangentZeroIso :
    (inverseImageModules f (Tensor.ringSheaf.{u', v', max u' v' w'} B)).obj
        (canonicalConormalSequence.{v', u', max u' v' w', max u' v' w'} K A B a).X₂ ≅
      (canonicalConormalSequence.{v, u, max u v w, max u v w} J (f.inverseImageRing.obj A)
        (f.inverseImageRing.obj B) (f.inverseImageRing.map a)).X₂

Tag 08U0, a definition

Tag 08U0 in the Stacks Project.

AlgebraicGeometry.RingedToposHom.naiveCotangentComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Cotangent/SheavesOfRings/RingedToposNaiveComparison.lean, line 326. The attribute's comment: “the complex NL_f, with the free algebra sheaf of the source's presentation spelled by the degree-zero term P₀ of the standard resolution of f⁻¹𝒪_D ⟶ 𝒪_C; the identification of that presentation with Stacks.Sites.FreeAlgebra.canonicalPresentation is not carried”.

The naive cotangent complex NL_f = NL_{𝒪_C/f⁻¹𝒪_D} of a morphism of ringed topoi (f, f♯) : (Sh(C), 𝒪_C) ⟶ (Sh(D), 𝒪_D): the two-term complex I/I² ⟶ 𝒪_C ⊗_{P₀} Ω_{P₀/f⁻¹𝒪_D} in cohomological degrees -1 and 0, formed from the inverse-image form f⁻¹𝒪_D ⟶ 𝒪_C of its structure map.

noncomputable def naiveCotangentComplex :
    CochainComplex (Sheaf.targetModules.{u, v, w} X.J X.O) ℤ

Sources

• Section 18.35, Tag 08TT
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Sites.FreeAlgebra.canonicalPresentation · Stacks.Sites.FreeAlgebra.canonicalPresentation_spec · Stacks.Sites.FreeAlgebra.canonicalPresentation_comp_coefficientMap · Stacks.Sites.FreeAlgebra.canonicalPresentation_isLocallySurjective · Stacks.SheafOfModules.canonicalConormalSequence · Stacks.SheafOfModules.naiveCotangentComplex · Stacks.SheafOfModules.freeAlgebraMapOfSquare_comp_canonicalPresentation · Stacks.SheafOfModules.naiveCotangentComplexMapOfSquare

Section18.36 Stalks of modules#

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

Tag 04EN, a lemma

Tag 04EN in the Stacks Project.

stalkSheafificationComparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkPreservesFiniteLimits.lean, line 305. The attribute's comment: “(1)”. References: SGA 4 IV (6.8.2), “formula (6.8.4)”.

The comparison natural transformation stalkSheafificationComparison p, from the stalk at p of a presheaf of sets to the stalk at p of its sheafification, is an isomorphism.

theorem stalkSheafificationComparison_isIso [HasWeakSheafify J (Type w)] :
    IsIso (stalkSheafificationComparison.{w} p)

sheafStalk_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkPreservesFiniteLimits.lean, line 323. The attribute's comment: “(2)”. References: SGA 4 VIII (3.5), “more general”.

The sheaf stalk functor at p preserves finite limits.

theorem sheafStalk_preservesFiniteLimits [HasWeakSheafify J (Type w)] :
    PreservesFiniteLimits (p.sheafFiber (A := Type w))

sheafStalk_preservesColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkPreservesFiniteLimits.lean, line 333. The attribute's comment: “(2)”. References: SGA 4 VIII (3.5), “more general”.

The sheaf stalk functor at p preserves all small colimits.

theorem sheafStalk_preservesColimits [HasWeakSheafify J (Type w)] :
    PreservesColimits (p.sheafFiber (A := Type w))

sheafStalk_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkPreservesFiniteLimits.lean, line 338. The attribute's comment: “(2)”. References: SGA 4 VIII (3.5), “Clause a)”.

The sheaf stalk functor at p preserves finite colimits.

theorem sheafStalk_preservesFiniteColimits [HasWeakSheafify J (Type w)] :
    PreservesFiniteColimits (p.sheafFiber (A := Type w))

presheafStalk_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkPreservesFiniteLimits.lean, line 348. The attribute's comment: “(3)”. References: SGA 4 VIII (3.5), “a) finite limits”; SGA 4 IV (6.8.6), “left-exactness clause of”; SGA 4 IV (6.8.7), “(iii)⇒(i), special case”.

The presheaf stalk functor at p preserves finite limits.

theorem presheafStalk_preservesFiniteLimits :
    PreservesFiniteLimits (p.presheafFiber (A := Type w))

presheafStalk_preservesColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkPreservesFiniteLimits.lean, line 354. The attribute's comment: “(3)”. References: SGA 4 VIII (3.5), “a) colimits”; SGA 4 IV (6.8.6), “partial”.

The presheaf stalk functor at p preserves all small colimits.

theorem presheafStalk_preservesColimits :
    PreservesColimits (p.presheafFiber (A := Type w))

presheafStalk_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkPreservesFiniteLimits.lean, line 359. The attribute's comment: “(3)”.

The presheaf stalk functor at p preserves finite colimits.

theorem presheafStalk_preservesFiniteColimits :
    PreservesFiniteColimits (p.presheafFiber (A := Type w))

Tag 04EP, a lemma

Tag 04EP in the Stacks Project.

Stacks.exactFunctor_abelianSheafFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/AbelianStalkExact.lean, line 54. The attribute's comment: “part (1)”.

Stacks Project, Tag 04EP, part (1). Taking the stalk at a point of a site is an exact functor from abelian sheaves to abelian groups.

theorem exactFunctor_abelianSheafFiber :
    exactFunctor (Sheaf J AddCommGrpCat.{w}) AddCommGrpCat.{w}
      (Φ.sheafFiber (A := AddCommGrpCat.{w}))

Stacks.exactFunctor_abelianPresheafFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/AbelianStalkExact.lean, line 62. The attribute's comment: “part (2)”.

Stacks Project, Tag 04EP, part (2). Taking the stalk at a point of a site is an exact functor from abelian presheaves to abelian groups.

theorem exactFunctor_abelianPresheafFiber :
    exactFunctor (Cᵒᵖ ⥤ AddCommGrpCat.{w}) AddCommGrpCat.{w}
      (Φ.presheafFiber (A := AddCommGrpCat.{w}))

Stacks.isIso_abelianPresheafFiber_map_toSheafify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/AbelianStalkExact.lean, line 73. The attribute's comment: “part (3)”.

Stacks Project, Tag 04EP, part (3). Sheafification of an abelian presheaf F does not change its stalk: the stalk at Φ of the canonical map F ⟶ F^# is an isomorphism F_p ≅ (F^#)_p.

theorem isIso_abelianPresheafFiber_map_toSheafify [HasWeakSheafify J AddCommGrpCat.{w}]
    (F : Cᵒᵖ ⥤ AddCommGrpCat.{w}) :
    IsIso ((Φ.presheafFiber (A := AddCommGrpCat.{w})).map (toSheafify J F))

Tag 04EQ, a lemma

Tag 04EQ in the Stacks Project.

Stacks.exactFunctor_presheafModuleFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/ModuleStalkPresheafExact.lean, line 54. The attribute's comment: “part (2)”.

Stacks 04EQ, part (2). Taking the stalk at a point of a site is an exact functor from presheaves of R-modules to modules over the stalk of R.

theorem exactFunctor_presheafModuleFiber :
    exactFunctor (PresheafOfModules.{w} R)
      (ModuleCat.{w} ((Φ.presheafFiber (A := RingCat.{w})).obj R))
      (presheafModuleFiber Φ R)

Stacks.exactFunctor_sheafModuleFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/ModuleStalkSheafExact.lean, line 63. The attribute's comment: “part (1)”.

Stacks Project, Tag 04EQ, part (1). Taking the stalk at a point of a site is an exact functor from sheaves of R-modules to modules over the stalk of R.

theorem exactFunctor_sheafModuleFiber :
    exactFunctor (SheafOfModules.{w} R)
      (ModuleCat.{w} ((Φ.presheafFiber (A := RingCat.{w})).obj R.obj))
      (sheafModuleFiber Φ R)

Stacks.isIso_moduleFiberSheafificationComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/ModuleStalkSheafExact.lean, line 113. The attribute's comment: “part (3)”.

Stacks Project, Tag 04EQ, part (3). Sheafification of a presheaf of modules does not change its module-valued stalk.

theorem isIso_moduleFiberSheafificationComparison :
    IsIso (moduleFiberSheafificationComparison Φ R)

Tag 05V5, a lemma

Tag 05V5 in the Stacks Project.

AlgebraicGeometry.RingedToposHom.pullbackModulesSquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedToposPullbackModulesComp.lean, line 140. The attribute's comment: “the formula, for a commutative square of morphisms of ringed topoi; the square over a point p and the point q = f ∘ p is not constructed”.

The formula of Stacks 05V5. Let

  P ⟶ X
  ↓     ↓
  Q ⟶ Y

be a commutative square of morphisms of ringed topoi — the hypothesis h says that the two composites P ⟶ Y agree. Then pulling a sheaf of O_Y-modules back along the bottom and then down the right is the same as pulling it back down the left and then along the top:

f^* ⋙ π^* ≅ ρ^* ⋙ γ^*.

Stacks 05V5 is this applied to the square whose left column is a point p of Sh(C), whose right column is the point q = f ∘ p of Sh(D), and whose bottom row is the induced morphism of ringed points: the left-hand composite is then F ↦ (f^*F)_p and the right-hand one is F ↦ F_q ⊗_{O_{D,q}} O_{C,p}. The square itself is not constructed here — see the module docstring.

def pullbackModulesSquareIso {P : RingedTopos.{v, u, w}} {Q : RingedTopos.{v', u', w'}}
    [P.J.HasSheafCompose (forget RingCat.{w})]
    [P.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [P.J.HasSheafCompose (forget AddCommGrpCat.{w})]
    [HasWeakSheafify P.J AddCommGrpCat.{w}] [P.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [Q.J.HasSheafCompose (forget RingCat.{w'})]
    [Q.J.HasSheafCompose (forget₂ CommRingCat.{w'} RingCat.{w'})]
    [Q.J.HasSheafCompose (forget AddCommGrpCat.{w'})]
    [HasWeakSheafify Q.J AddCommGrpCat.{w'}] [Q.J.WEqualsLocallyBijective AddCommGrpCat.{w'}]
    (f : RingedToposHom X Y) (π : RingedToposHom P X) (ρ : RingedToposHom Q Y)
    (γ : RingedToposHom P Q) (h : f.comp π = ρ.comp γ) :
    f.toModulesHom.pullbackModules ⋙ π.toModulesHom.pullbackModules ≅
      ρ.toModulesHom.pullbackModules ⋙ γ.toModulesHom.pullbackModules

Stacks.Sheaves.StalkPullback.pointStalkFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/StalkPullbackAtAPoint.lean, line 124. The attribute's comment: “the formula (f^*𝓕)_p ≅ 𝓕_q ⊗_{𝒪'_q} 𝒪_p, naturally in 𝓕, for an arbitrary morphism of ringed topoi and a point p of the source site, with q = f ∘ p built from the morphism and the point by Stacks 00YA”.

Stacks 05V5, for a morphism of ringed topoi f : (Sh(C), 𝒪) ⟶ (Sh(D), 𝒪') and a point Φ of the source site C: the stalk at Φ of the pullback of a sheaf of 𝒪'-modules is the extension of scalars along 𝒪'_q ⟶ 𝒪_Φ of its stalk at the composite point q = f ∘ Φ, naturally in the module.

The point q of the target site is targetSitePoint, built from f and Φ by Stacks 00YA; nothing about it is assumed.

def pointStalkFunctorIso :
    f.pullbackModules ⋙ Stacks.sheafModuleFiberOfCommRing Φ X.O ≅
      Stacks.sheafModuleFiberOfCommRing (targetSitePoint f Φ) Y.O ⋙
        ModuleCat.extendScalars (pointStalkRingMap f Φ)

Stacks.Sheaves.StalkPullback.toposPointStalkFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/StalkPullbackAtAPoint.lean, line 176. The attribute's comment: “the formula (f^*𝓕)_p ≅ 𝓕_q ⊗_{𝒪'_q} 𝒪_p, naturally in 𝓕, for an arbitrary morphism of ringed topoi and a point p of the source topos Sh(C), with q = f ∘ p built from the morphism and the point by Stacks 00YA”.

Stacks 05V5, for a morphism of ringed topoi and a point p of the source topos Sh(C): the stalk at p of the pullback of a sheaf of 𝒪'-modules is the extension of scalars along 𝒪'_q ⟶ 𝒪_p of its stalk at q = f ∘ p, naturally in the module.

The stalk functor on sheaves of modules is taken over a point of the site, so p is presented by p.sitePoint through Stacks 00YA part (2); on sheaves of sets that is p⁻¹ itself, by CategoryTheory.PointOfTopos.sheafFiberIsoInverseImage.

def toposPointStalkFunctorIso :
    f.pullbackModules ⋙ Stacks.sheafModuleFiberOfCommRing p.sitePoint X.O ≅
      Stacks.sheafModuleFiberOfCommRing (toposTargetSitePoint f p) Y.O ⋙
        ModuleCat.extendScalars (toposPointStalkRingMap f p)

Stacks.Sheaves.StalkPullback.stalkFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/StalkPullbackAtAPointPair.lean, line 375. The attribute's comment: “the formula (f^*G)_Φ ≅ G_Ψ ⊗_{O'_Ψ} O_Φ, naturally in the O'-module G, for a morphism of ringed topoi together with a point Ψ of the target site whose stalk functor on sheaves of sets is the inverse image followed by the stalk functor at Φ”.

Stacks 05V5 at a matched pair of points, as a natural isomorphism of stalk functors: the stalk at Φ of the pullback of a sheaf of 𝒪'-modules is the extension of scalars along 𝒪'_Ψ ⟶ 𝒪_Φ of its stalk at Ψ.

This is the clause of Stacks 05V5 that AlgebraicGeometry.RingedToposHom.pullbackModulesSquareIso states for a commutative square of morphisms of ringed topoi without constructing the square over a point; here the point of the target topos and the identification of stalk functors are the data Ψ and e.

def stalkFunctorIso :
    f.pullbackModules ⋙ Stacks.sheafModuleFiberOfCommRing Φ X.O ≅
      Stacks.sheafModuleFiberOfCommRing Ψ Y.O ⋙
        ModuleCat.extendScalars (stalkRingMap f Φ Ψ e)

Stacks.Sheaves.DerivedPullback.KFlatPullbackMorphismOfSites.stalkFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/StalkBaseChangeAtTheTargetPoint.lean, line 258. The attribute's comment: “the formula (f^*F)_p ≅ F_q ⊗_{O'_q} O_p at a point p of the source site, naturally in the O'-module F, with q = f ∘ p the point of the target site induced by p; for a morphism of ringed topoi whose underlying functor is a morphism of the underlying sites, at RingedTopos.{u, u, u}”. References: EGA 0 (4.3.1), “more general”.

Stacks 05V5 at the point Ψ of the target site, as a natural isomorphism of stalk functors: the stalk at Φ of the pullback of a sheaf of O'-modules is the extension of scalars along O'_Ψ ⟶ O_Φ of its stalk at Ψ.

This is the clause of Stacks 05V5 that AlgebraicGeometry.RingedToposHom.pullbackModulesSquareIso names as missing: there the formula is proved for a commutative square of morphisms of ringed topoi, with the square over a point p and the point q = f ∘ p left unconstructed, and Ψ = targetPoint f hu Φ is that point.

def stalkFunctorIso :
    f.pullbackTopos ⋙ Stacks.sheafModuleFiberOfCommRing Φ X.O ≅
      Stacks.sheafModuleFiberOfCommRing (targetPoint f hu Φ) Y.O ⋙
        ModuleCat.extendScalars (stalkRingMap f hu Φ)

Stacks.Sheaves.DerivedPullback.StalkBaseChangeOfToposHom.stalkFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/StalkBaseChangeOfToposHom.lean, line 305. The attribute's comment: “the formula (f^*F)_p ≅ F_q ⊗_{O'_q} O_p at a point p of the source site, naturally in the O'-module F, with q = f ∘ p the point of the target site induced by p; for an arbitrary morphism of ringed topoi, at RingedTopos.{u, u, u}”.

Stacks 05V5 at the point Ψ of the target site, for an arbitrary morphism of ringed topoi, as a natural isomorphism of stalk functors: the stalk at Φ of the pullback of a sheaf of O'-modules is the extension of scalars along O'_Ψ ⟶ O_Φ of its stalk at Ψ.

Nothing is assumed about the underlying sites: the pullback of Stacks 03D6 part (2) is built from the inverse image of Stacks 03D2, so the geometric half of the comparison is the one of Stacks 05V1 at Ψ and the algebraic half is the stalkwise formula for the extension of scalars.

def stalkFunctorIso :
    g.pullbackModules ⋙ Stacks.sheafModuleFiberOfCommRing Φ X.O ≅
      Stacks.sheafModuleFiberOfCommRing (targetPoint g Φ) Y.O ⋙
        ModuleCat.extendScalars (stalkRingMap g Φ)

Sources

• Section 18.36, Tag 04EM
• AxiomMath/Stacks at 5ed82d14

LeanstalkSheafificationComparison_isIso · sheafStalk_preservesFiniteLimits · sheafStalk_preservesColimits · sheafStalk_preservesFiniteColimits · presheafStalk_preservesFiniteLimits · presheafStalk_preservesColimits · presheafStalk_preservesFiniteColimits · Stacks.exactFunctor_abelianSheafFiber

Section18.37 Skyscraper sheaves#

Section 18.37 of the Stacks Project, Tag 05V6. 3 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05V7, a lemma

Tag 05V7 in the Stacks Project.

Stacks.Topos.Skyscraper.skyscraperAb_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperExact.lean, line 157. The attribute's comment: “(1) p_* is exact”.

The direct image p_* : Ab ⥤ Ab(C) of a point of a topos is exact.

theorem skyscraperAb_exact [HasSheafify J AddCommGrpCat.{w}] :
    exactFunctor AddCommGrpCat.{w} (Sheaf J AddCommGrpCat.{w}) (skyscraperAb p)

Stacks.Topos.Skyscraper.abelianEta, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperStalkSplitting.lean, line 94. The attribute's comment: “skyscraper_splitting”.

The canonical map from an abelian group into the stalk of its skyscraper, natural in the abelian group. Its underlying map is the elementwise map of Stacks Project, Tag 05UX.

noncomputable def abelianEta (p : PointOfTopos.{w, v, u} J) :
    NatTrans (Functor.id (CommGrp (Type w))) (stalkSkyscraperAbFunctor p)

Stacks.Topos.Skyscraper.abelianEta_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperStalkSplitting.lean, line 106. The attribute's comment: “skyscraper_splitting”.

The natural section on abelian group objects has the canonical underlying map of Stacks Project, Tag 05UX.

theorem abelianEta_hom (p : PointOfTopos.{w, v, u} J)
    (A : CommGrp (Type w)) :
    ((abelianEta p).app A).hom.hom.hom = (p.counitSection.app A.X)

Stacks.Topos.Skyscraper.stalkSkyscraperAbFunctorIsoBiprod, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperStalkSplitting.lean, line 203. The attribute's comment: “skyscraper_splitting”.

Stacks Project, Tag 05V7. The decomposition p⁻¹p_*A = A ⊕ Iₚ(A) is functorial in the abelian group A.

noncomputable def stalkSkyscraperAbFunctorIsoBiprod
    (p : PointOfTopos.{w, v, u} J) :
    Iso (stalkSkyscraperAbFunctor p ⋙ commGrpAddEquivalence.functor)
      (commGrpAddEquivalence.functor ⊞ kernelComplementAbFunctor p)

Stacks.Topos.Skyscraper.stalkSkyscraperAbFunctorIsoBiprod_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperStalkSplitting.lean, line 211. The attribute's comment: “skyscraper_splitting”.

The first projection of the splitting is the canonical counit.

theorem stalkSkyscraperAbFunctorIsoBiprod_fst
    (p : PointOfTopos.{w, v, u} J) :
    (stalkSkyscraperAbFunctorIsoBiprod p).hom ≫ biprod.fst =
      Functor.whiskerRight (abelianCounit p) commGrpAddEquivalence.functor

Stacks.Topos.Skyscraper.stalkSkyscraperAbFunctorIsoBiprod_inl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperStalkSplitting.lean, line 226. The attribute's comment: “skyscraper_splitting”.

The first inclusion of the splitting is the canonical map from an abelian group into the stalk of its skyscraper.

theorem stalkSkyscraperAbFunctorIsoBiprod_inl
    (p : PointOfTopos.{w, v, u} J) :
    Functor.whiskerRight (abelianEta p) commGrpAddEquivalence.functor ≫
      (stalkSkyscraperAbFunctorIsoBiprod p).hom = biprod.inl

Stacks.Topos.Skyscraper.auxKernelComplementAbFunctorObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperStalkSplitting.lean, line 243. The attribute's comment: “skyscraper_splitting”.

Objectwise, the auxiliary kernel functor is canonically isomorphic to the prescribed Iₚ.

noncomputable def auxKernelComplementAbFunctorObjIso
    (p : PointOfTopos.{w, v, u} J)
    (A : CommGrp (Type w)) :
    (auxKernelComplementAbFunctor p).obj A ≅ PointOfTopos.kernelComplementOfCounit p A

Stacks.Topos.Skyscraper.kernelComplementAbFunctorNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperStalkSplitting.lean, line 266. The attribute's comment: “skyscraper_splitting”.

The identification of the kernel summand with Iₚ is natural, not merely an objectwise identification.

noncomputable def kernelComplementAbFunctorNatIso
    (p : PointOfTopos.{w, v, u} J) :
    Iso (kernelComplementAbFunctor p ⋙ commGrpAddEquivalence.inverse)
      (auxKernelComplementAbFunctor p)

Tag 05V8, a lemma

Tag 05V8 in the Stacks Project.

Stacks.Sheaves.RingedPoint.RingedPointSituation.pushforwardModules_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedPointPushforward.lean, line 265. The attribute's comment: “exactness of the direct image”.

Stacks 05V8. The direct image of modules from a ringed point is exact.

theorem pushforwardModules_exact
    [HasWeakSheafify s.point.J AddCommGrpCat.{w}]
    [s.point.J.WEqualsLocallyBijective AddCommGrpCat.{w}] :
    exactFunctor
      (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf s.point.O))
      (SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
      (pushforwardModules s.toRingedToposHom)

Stacks.Sheaves.RingedPoint.RingedPointSituation.pullbackPushforwardModules_counit_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedPointPushforward.lean, line 333. The attribute's comment: “surjectivity of the counit”.

Stacks 05V8. The canonical map p^*p_*M ⟶ M is a surjection of O_p-modules: it is the counit of the pullback-pushforward adjunction of Stacks 03D7, hence a morphism of sheaves of modules, and it is an epimorphism because the direct image is faithful.

theorem pullbackPushforwardModules_counit_epi
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [HasWeakSheafify s.point.J AddCommGrpCat.{w}]
    [s.point.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    (M : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf s.point.O)) :
    Epi ((pullbackAdjPushforwardModules s.toRingedToposHom).counit.app M)

Stacks.Sheaves.RingedPoint.RingedPointSituation.pullbackPushforwardModules_counit_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedPointPushforward.lean, line 456. The attribute's comment: “(2) the canonical surjection p⁻¹p_*M → M is O_p-linear”.

Stacks 05V8. The canonical surjection p⁻¹p_*M ⟶ M of Stacks 05V7 — the counit of the adjunction p⁻¹ ⊣ p_* of the point — is O_p-linear: under the canonical identification p⁻¹p_*M = (p^*p_*M)^♭ it is the underlying map of the counit p^*p_*M ⟶ M of the adjunction of Stacks 03D7 for modules, which is a morphism of sheaves of O_p-modules by construction.

This is the source's argument: p⁻¹O = O_p, hence p^* = p⁻¹, hence the map of Stacks 05V7 is the counit of the adjunction for modules, "whence linear".

theorem pullbackPushforwardModules_counit_stalk
    [HasWeakSheafify s.point.J AddCommGrpCat.{w}]
    [s.point.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    (M : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf s.point.O)) :
    (Sheaf.moduleSheafFunctor (Stacks.SheafOfModules.Tensor.ringSheaf s.point.O) ⋙
      s.pointEquiv.functor).map
        ((pullbackAdjPushforwardModules s.toRingedToposHom).counit.app M) =
      (s.pullbackPushforwardStalkIso M).hom ≫
        p.adj.counit.app (s.pointEquiv.functor.obj
          ((Sheaf.moduleSheafFunctor
            (Stacks.SheafOfModules.Tensor.ringSheaf s.point.O)).obj M))

Stacks.Sheaves.RingedPoint.GSets.realSMul_eq_twistedSMul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedPointSplittingNotLinear.lean, line 261. The attribute's comment: “(3) the O_p-module structure on p⁻¹p_*M is (r f)(σ) = σ(r) f(σ)”.

Stacks Project, Tag 05V8, part (3). The 𝒪_p-module structure on p⁻¹p_*M = Map(G, M) is (r f)(σ) = σ(r) f(σ).

This is the source's own justification, and it is applied to the actual structure rather than assumed of it: realSMul is G-equivariant (translate_realSMul) and evaluation at 1_G is R-linear for it (realSMul_one), and by twistedSMul_eq_of_equivariant_of_evalOne there is exactly one such scalar action, namely twistedSMul.

theorem realSMul_eq_twistedSMul (r : R) (f : G → M) :
    realSMul G R M r f = twistedSMul G R M r f

Stacks.Sheaves.RingedPoint.GSets.not_isRealLinear_skyscraperSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedPointSplittingNotLinear.lean, line 339. The attribute's comment: “(3) the splitting is not O_p-linear in general”.

Stacks Project, Tag 05V8, part (3). The functorial direct sum decomposition p⁻¹p_*M = M ⊕ I(M) of Stacks 05V7 is not 𝒪_p-linear in general.

Take for p the point of the topos of G-sets whose inverse image forgets the action, and for 𝒪 the sheaf of rings attached to a commutative ring R with an action of G, so that 𝒪_p = R. Then p⁻¹p_*R = Map(G, R), the counit is evaluation at 1_G and the canonical section of the splitting sends r to the constant function with value r. That section is not linear for the actual 𝒪_p-module structure on p⁻¹p_*R — the pointwise action of the sections of 𝒪 over {}_G G, read through 𝒪_p = R, which is realSMul — as soon as some σ moves some r: by realSMul_eq_twistedSMul that action carries the constant function 1 to σ ↦ σ(r₀), which is not constant.

theorem not_isRealLinear_skyscraperSection
    (e : Action (Type w) G ≌ Sheaf J (Type w)) {σ₀ : G} {r₀ : R} (h : σ₀ • r₀ ≠ r₀) :
    ¬ IsRealLinear G R R (fun r =>
      skyscraperStalkEquiv G e R ((forgetfulPoint G e).counitSection.app R r))

Tag 05V9, an example

Tag 05V9 in the Stacks Project.

Stacks.Sites.GSets.skyscraperStalkEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperOnGSets.lean, line 196. The attribute's comment: “p⁻¹p_*M = Map(G, M)”.

Stacks Project, Tag 05V9. The identification p⁻¹p_*E = Map(G, E): the direct image of E is the G-set Map(G, E) and the inverse image forgets the action.

def skyscraperStalkEquiv (E : Type w) :
    ((forgetfulPoint G e).pushforward ⋙ (forgetfulPoint G e).inverseImage).obj E ≃ (G → E)

Stacks.Sites.GSets.counit_app_eq_skyscraperStalkEquiv_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperOnGSets.lean, line 213. The attribute's comment: “the counit p⁻¹p_*M → M is evaluation at 1_G”.

Stacks Project, Tag 05V9. Under the identification of p⁻¹p_*E with Map(G, E) the counit p⁻¹p_*E ⟶ E is evaluation at 1_G.

theorem counit_app_eq_skyscraperStalkEquiv_one (E : Type w)
    (x : ((forgetfulPoint G e).pushforward ⋙ (forgetfulPoint G e).inverseImage).obj E) :
    (forgetfulPoint G e).adj.counit.app E x = skyscraperStalkEquiv G e E x 1

Stacks.Sites.GSets.skyscraperStalkEquiv_counitSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperOnGSets.lean, line 220. The attribute's comment: “M → Map(G, M) assigns to m the constant function with value m”.

Stacks Project, Tag 05V9. Under the identification of p⁻¹p_*E with Map(G, E) the canonical section of the counit sends m to the constant function with value m.

theorem skyscraperStalkEquiv_counitSection (E : Type w) (m : E) :
    skyscraperStalkEquiv G e E ((forgetfulPoint G e).counitSection.app E m) =
      Function.const G m

Stacks.Sites.GSets.kernelCounitEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperOnGSets.lean, line 234. The attribute's comment: “I(M) = {f : G → M | f(1_G) = 0}”.

Stacks Project, Tag 05V9. I(M) = {f : G → M | f(1_G) = 0}: the kernel of the counit at an abelian group object A is the set of functions G → A vanishing at 1_G. An abelian group object is written multiplicatively, so its zero is denoted 1.

def kernelCounitEquiv (A : CommGrp (Type w)) :
    {x : ((forgetfulPoint G e).pushforward ⋙ (forgetfulPoint G e).inverseImage).obj A.X //
        (forgetfulPoint G e).adj.counit.app A.X x =
          (1 : commGrpTypeEquivalenceCommGrp.functor.obj A)} ≃
      {f : G → A.X // f 1 = (1 : commGrpTypeEquivalenceCommGrp.functor.obj A)}

Stacks.Sites.GSets.stalkEquivSectionsAtRegular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperOnGSets.lean, line 344. The attribute's comment: “𝒪_p = R forgetting the G-action: the stalk is the ring of sections over {}_G G”.

Stacks Project, Tag 05V9. The stalk 𝒪_p of the sheaf of rings attached to R is its ring of sections over an object presenting the regular G-set; with sectionsAtRegularRingEquiv this is 𝒪_p = R.

def stalkEquivSectionsAtRegular :
    (forgetfulPoint G e).inverseImage.obj (e.functor.obj (Action.ofMulAction G R)) ≃
      (equivariantSubring G R (ι.obj u₀))

Stacks.Sites.GSets.sectionsAtRegularRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SkyscraperOnGSets.lean, line 355. The attribute's comment: “𝒪_p = R forgetting the G-action: that ring is R”.

Stacks Project, Tag 05V9. 𝒪_p = R where we forget the G-action: evaluation at the base point is a ring isomorphism from the sections of the sheaf of rings attached to R over an object presenting the regular G-set onto R.

def sectionsAtRegularRingEquiv : (equivariantSubring G R (ι.obj u₀)) ≃+* R

Sources

• Section 18.37, Tag 05V6
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Topos.Skyscraper.skyscraperAb_exact · Stacks.Topos.Skyscraper.abelianEta · Stacks.Topos.Skyscraper.abelianEta_hom · Stacks.Topos.Skyscraper.stalkSkyscraperAbFunctorIsoBiprod · Stacks.Topos.Skyscraper.stalkSkyscraperAbFunctorIsoBiprod_fst · Stacks.Topos.Skyscraper.stalkSkyscraperAbFunctorIsoBiprod_inl · Stacks.Topos.Skyscraper.auxKernelComplementAbFunctorObjIso · Stacks.Topos.Skyscraper.kernelComplementAbFunctorNatIso

Section18.38 Localization and points#

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

Tag 0710, a lemma

Tag 0710 in the Stacks Project.

Stacks.Sites.ExtensionByZero.stalkExtensionByZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Gate18/StalkOfExtensionByZero.lean, line 611.

The stalk of extension by zero from C/U is the direct sum of the stalks at the points of C/U above the given point.

noncomputable def stalkExtensionByZeroIso
    (X : RingedSite.{u, u, u}) (p : GrothendieckTopology.Point.{u, u, u} X.J)
    (U : X.C) (G : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))
    [HasWeakSheafify X.J AddCommGrpCat.{u}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{u}] :
    (p.presheafFiber.obj (((SheafOfModules.pullback.{u}
      (F := Over.forget U)
        (𝟙 ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))).obj G).val.presheaf)) ≅
      ∐ fun x : p.fiber.obj U => (p.over x).presheafFiber.obj G.val.presheaf

Stacks.Sites.ExtensionByZero.OfEssentiallySmall.stalkExtensionByZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Gate18/StalkOfExtensionByZeroEssentiallySmall.lean, line 602.

The stalk of extension by zero from C/U is the direct sum of the stalks at the points of C/U above the given point, for a ringed site whose objects may live in a universe above its morphisms, structure rings and module sections.

noncomputable def stalkExtensionByZeroIso
    (X : RingedSite.{c, u, u}) [EssentiallySmall.{u} X.C]
    (p : GrothendieckTopology.Point.{u, u, c} X.J)
    (U : X.C) (G : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))
    [HasWeakSheafify X.J AddCommGrpCat.{u}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{u}] :
    (p.presheafFiber.obj (((SheafOfModules.pullback.{u}
      (F := Over.forget U) (𝟙 ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))).obj
        G).val.presheaf)) ≅
      ∐ fun x : p.fiber.obj U => (p.over x).presheafFiber.obj G.val.presheaf

Sources

• Section 18.38, Tag 070Z
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Sites.ExtensionByZero.stalkExtensionByZeroIso · Stacks.Sites.ExtensionByZero.OfEssentiallySmall.stalkExtensionByZeroIso

Section18.39 Pullbacks of flat modules#

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

Tag 05VD, a lemma

Tag 05VD in the Stacks Project.

Stacks.Sheaves.RingedToposModules.isFlat_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackFlatInverseImage.lean, line 359. The attribute's comment: “ringed topoi, at free universes, assuming on each site the HasSheafCompose, HasWeakSheafify, WEqualsLocallyBijective and HasSheafify instances of the variable block; isFlat_pullbackModules_maxSectionUniverse is the same statement with all of them derived”. References: SGA 4 V (8.2.9); SGA 4 V (1.7.1).

Stacks Project, Tag 05VD. The pullback of a flat sheaf of modules along a morphism of ringed topoi is flat.

All five universe parameters of the tagged statement are free here; what the tag does not state are the sheafification hypotheses in the variable block above — HasSheafCompose for the three forgetful functors, HasWeakSheafify and WEqualsLocallyBijective for AddCommGrpCat, and HasSheafify for Type — on each of the two sites. They arise because Stacks.ringSheaf and Stacks.SheafOfModules.IsFlat take them as instance binders where a ringSheaf construction could build them internally, so they are a formulation difference rather than added mathematical strength; but they are not nothing, and a consumer whose binder context lacks them cannot apply this theorem without supplying them.

They need not be supplied when each ringed topos has its section universe equal to the max of its site's object and morphism universes, which is what Stacks.Sheaves.RingedToposModules.isFlat_pullbackModules_maxSectionUniverse below records: at that shape every one of them is an instance of the pinned Mathlib, so that statement of Stacks 05VD assumes nothing beyond the source's own hypotheses. Both object universes and both morphism universes stay free there; it is only the two section universes that are determined.

theorem isFlat_pullbackModules (hG : Stacks.SheafOfModules.IsFlat (O := Y.O) G) :
    Stacks.SheafOfModules.IsFlat (O := X.O) ((f.pullbackModules).obj G)

Stacks.Sheaves.RingedToposModules.isFlat_pullbackModules_maxSectionUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackFlatInverseImage.lean, line 421. The attribute's comment: “ringed topoi whose section universe is the max of their site's object and morphism universes -- object and morphism universes free and independent -- with no sheafification hypothesis assumed: HasSheafCompose, HasWeakSheafify, WEqualsLocallyBijective and HasSheafify are all derived”. References: SGA 4 V (8.2.9); SGA 4 V (1.7.1); SGA 4 VI (8.6.4), “special case”.

Stacks Project, Tag 05VD, assuming nothing the source does not assume. The pullback of a flat sheaf of modules along a morphism of ringed topoi is flat.

This is Stacks.Sheaves.RingedToposModules.isFlat_pullbackModules with every one of its sheafification hypotheses discharged by instance search instead of assumed. That is possible exactly when each ringed topos has its section universe equal to the max u v of its site's object and morphism universes, which is the shape above; the two object universes and the two morphism universes remain free and independent.

Where each hypothesis comes from, and which of them need the section universe at all:

• the three HasSheafCompose hypotheses hold at every universe and for every site, so they were never where the narrowing lived: forget AddCommGrpCat by CategoryTheory.hasSheafCompose_of_preservesMulticospan, and forget RingCat and forget₂ CommRingCat RingCat by CategoryTheory.hasSheafComposeEssentiallySmallSite;
• HasSheafify J (Type (max u v)) is CategoryTheory.instHasSheafifyType, and it too is less rigid than it looks: HasSheafify J (Type w) holds for a free w under UnivLE.{max u v, w}, by CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover;
• HasWeakSheafify J AddCommGrpCat.{max u v} is CategoryTheory.instHasWeakSheafifyOfHasSheafify applied to that same plus-construction instance at AddCommGrpCat;
• J.WEqualsLocallyBijective AddCommGrpCat.{max u v} follows from the previous one by the concrete-category instance of Mathlib/CategoryTheory/Sites/LocallyBijective.lean, built on CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.mk'.

Why the section universe cannot be left free. Exactly one of the five resists: HasWeakSheafify J AddCommGrpCat.{w} for a free w, which fails even under UnivLE.{max u v, w}. The plus construction needs PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget AddCommGrpCat.\{w}), and the only instance supplying it is AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits, which is PreservesFilteredColimits (forget AddCommGrpCat.{w}) — filtered shapes in the same universe w as the groups, while the cover categories live in max u v. The two agree precisely at w = max u v. Since Stacks.SheafOfModules.IsFlat takes HasWeakSheafify as an instance binder, this blocks the statement and not merely the proof. For a w strictly below max u v there is nothing to lift at all: sheafification of AddCommGrpCat.{w}-valued presheaves on a site whose covers are max u v-large does not exist in general. So isFlat_pullbackModules above, with the hypotheses carried and all five universes free, and this statement, with the section universes determined and no hypotheses, are each the strongest available in their own direction, and neither subsumes the other.

theorem isFlat_pullbackModules_maxSectionUniverse
    (hG : Stacks.SheafOfModules.IsFlat (J := Y.J) (O := Y.O) G) :
    Stacks.SheafOfModules.IsFlat (J := X.J) (O := X.O) ((f.pullbackModules).obj G)

Stacks.ModuleUp.isFlat_pullback_of_representablyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SiteUpSheafificationPullback.lean, line 654. The attribute's comment: “ringed sites, for a morphism of sites given by a continuous representably flat functor, with no sheafification hypothesis assumed: the HasWeakSheafify, HasSheafCompose, WEqualsLocallyBijective and HasLeftKanExtension instances are all derived. The reduction of an arbitrary morphism of ringed sites to this case is Stacks 03CR”. References: SGA 4 V (8.2.9), “representably flat u”; SGA 4 V (1.7.1), “representably flat u”.

Stacks 05VD for a morphism of ringed sites, assuming nothing the source does not assume.

This is Stacks.ModuleUp.isFlat_pullback with every sheafification hypothesis of the section above discharged by instance search instead of assumed: HasWeakSheafify for CommRingCat, RingCat and AddCommGrpCat on both sites, HasSheafCompose for forget₂ CommRingCat RingCat on both sites, WEqualsLocallyBijective for RingCat and AddCommGrpCat on both sites, and the two HasLeftKanExtension families. All eleven are instances of the pinned Mathlib for a small site, so what is left — RepresentablyFlat u and u.IsContinuous K J — is exactly the situation the source's proof reduces to.

They are kept as binders in the section above because they are wanted at elaboration time by the definitions there: with them removed, Stacks.ModuleUp.upSheafUnitRingOfCommRing no longer elaborates and Stacks.ModuleUp.upSheafify_comp_bridge exhausts the isDefEq heartbeat budget re-deriving J.PreservesSheafification (forget₂ CommRingCat RingCat), the synthesis already recorded as too expensive in the implementation notes. Discharging them once, here, at the statement of the theorem costs nothing.

The single-universe restriction is not liftable on this branch. The sites are small categories in Type w with the structure sheaves and modules also at w. This is forced by PresheafOfModules.pullbackObjIsDefined_eq_top, the only unconditional source of (PresheafOfModules.pushforward φ).IsRightAdjoint and hence of SheafOfModules.pullback itself, which Mathlib states for {C D : Type u} [SmallCategory C] [SmallCategory D] and RingCat.{u}. Nothing weaker is available, so the object, morphism and section universes cannot be separated here without first generalizing that Mathlib declaration.

theorem isFlat_pullback_of_representablyFlat {R : Sheaf J CommRingCat.{w}}
    {O : Sheaf K CommRingCat.{w}}
    (η : O ⟶ (u.sheafPushforwardContinuous CommRingCat.{w} K J).obj R)
    (F : _root_.SheafOfModules.{w} (Stacks.commRingSheafToRingSheaf (J := K) O))
    (hF : Stacks.SheafOfModules.IsFlat (J := K) (O := O) F) :
    Stacks.SheafOfModules.IsFlat (J := J) (O := R)
      ((SheafOfModules.pullback.{w} (ringSheafMapOfPushforward u J η)).obj F)

Tag 05VB, a lemma

Tag 05VB in the Stacks Project.

Stacks.SheafOfModules.isFlatModuleStalk_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/FlatStalk.lean, line 297. References: SGA 4 V (1.6), “assertion 1”.

Stacks Project, Tag 05VB. Let (C, O) be a ringed site and let Φ be a point of C. If F is a flat sheaf of O-modules, then the stalk of F at Φ is a flat module over the stalk of O at Φ.

The proof runs the equational criterion for flatness on both sides. A relation ∑ fᵢ xᵢ = 0 in the stalk is lifted to a relation among sections over a neighbourhood of Φ; the local equational criterion for a flat sheaf of modules, Stacks 08FC part (2), factors those sections through a finite free module on a covering of that neighbourhood; the point's fibre meets one member of the covering, and the germs of that factorisation exhibit the original relation as trivial, which is flatness of the stalk by Mathlib's equational criterion.

theorem isFlatModuleStalk_of_isFlat (Φ : J.Point.{max v w})
    (O : Sheaf J CommRingCat.{max v w})
    (F : _root_.SheafOfModules.{max v w} (commRingSheafToRingSheaf O)) (hF : IsFlat F) :
    IsFlatModuleStalk Φ O F

Stacks.isFlatModuleStalk_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/FlatModuleStalk.lean, line 165.

Stacks 05VB. The stalk at a point of a site of a flat sheaf of O-modules is a flat module over the stalk of O.

theorem isFlatModuleStalk_of_isFlat
    (F : _root_.SheafOfModules.{max v w} (commRingSheafToRingSheaf O))
    (hF : SheafOfModules.IsFlat F) (Φ : J.Point.{max v w}) :
    IsFlatModuleStalk Φ O F

Tag 05VC, a lemma

Tag 05VC in the Stacks Project.

Stacks.isFlat_iff_forall_isFlatModuleStalk_of_weakSheafify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/StalkTensorComparisonWeak.lean, line 37. References: SGA 4 V (1.6), “2)”.

A sheaf of modules is flat if and only if its stalks at a conservative family of points are flat, assuming HasWeakSheafify J AddCommGrpCat.{w} and J.WEqualsLocallyBijective AddCommGrpCat.{w}.

theorem isFlat_iff_forall_isFlatModuleStalk_of_weakSheafify {C : Type u} [Category.{v} C]
    [LocallySmall.{w} C] {J : GrothendieckTopology C}
    [J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [J.WEqualsLocallyBijective AddCommGrpCat.{w}] [HasWeakSheafify J AddCommGrpCat.{w}]
    {t : Type*} (p : t → J.Point.{w})
    (hp : (ObjectProperty.ofObj p).IsConservativeFamilyOfPoints) (O : Sheaf J CommRingCat.{w})
    (F : SheafOfModules.{w} (commRingSheafToRingSheaf O)) :
    SheafOfModules.IsFlat F ↔ ∀ i, IsFlatModuleStalk (p i) O F

Tag 0G6R, a lemma

Tag 0G6R in the Stacks Project.

Stacks.Sheaves.RingedToposModules.shortExact_map_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackShortExactFlat.lean, line 140. References: EGA IV (2.1.8), “(i), G' = O_{Y'}”.

Stacks Project, Tag 0G6R. Let (f, f♯) : (Sh(C), O_C) ⟶ (Sh(D), O_D) be a morphism of ringed topoi and let 0 → F → G → H → 0 be a short exact sequence of sheaves of O_D-modules with H a flat O_D-module. Then 0 → f^*F → f^*G → f^*H → 0 is short exact.

The pullback of Stacks 03D6 part (2) is the inverse image of Stacks 03D2 followed by extension of scalars along f♯. The inverse image is exact (Stacks 04JC) and carries H to a flat f⁻¹O_D-module (Stacks 05VD), and extension of scalars keeps a short exact sequence with flat third term short exact (Stacks 03EX).

theorem shortExact_map_pullbackModules
    (S : ShortComplex (SheafOfModules.{w'} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    (hS : S.ShortExact)
    (hflat : Stacks.SheafOfModules.IsFlat (O := Y.O) S.X₃) :
    (S.map (f.pullbackModules)).ShortExact

AlgebraicGeometry.RingedToposHom.exists_shortExact_map_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/PullbackOfAShortExactSequence.lean, line 83. The attribute's comment: “morphisms of ringed topoi, with the source ringed topos's site small in the universe of its sections and the target's section universe equal to the max of its object and morphism universes”. References: EGA IV (2.1.8), “(i), G' = O_{Y'}”.

Stacks Project, Tag 0G6R. For a morphism of ringed topoi (f, f♯) : (Sh(C), O_C) ⟶ (Sh(D), O_D) and a short exact sequence of sheaves of O_D-modules whose final term is flat, the pullback sequence 0 ⟶ f^*F₁ ⟶ f^*F₂ ⟶ f^*F₃ ⟶ 0 is short exact.

The pullback is the one of Stacks 03D6 part (2), O_C ⊗_{f⁻¹O_D} f⁻¹(-). The composite-is-zero witness is carried in the statement, so that the statement does not mention preservation of zero morphisms by the pullback, which is not part of that functor's public interface.

theorem exists_shortExact_map_pullbackModules (hS : S.ShortExact)
    (hflat : Stacks.SheafOfModules.IsFlat (O := Y.O) S.X₃) :
    ∃ h : (f.pullbackModules).map S.f ≫ (f.pullbackModules).map S.g = 0,
      (ShortComplex.mk ((f.pullbackModules).map S.f)
        ((f.pullbackModules).map S.g) h).ShortExact

Sources

• Section 18.39, Tag 05VA
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Sheaves.RingedToposModules.isFlat_pullbackModules · Stacks.Sheaves.RingedToposModules.isFlat_pullbackModules_maxSectionUniverse · Stacks.ModuleUp.isFlat_pullback_of_representablyFlat · Stacks.SheafOfModules.isFlatModuleStalk_of_isFlat · Stacks.isFlatModuleStalk_of_isFlat · Stacks.isFlat_iff_forall_isFlatModuleStalk_of_weakSheafify · Stacks.Sheaves.RingedToposModules.shortExact_map_pullbackModules · AlgebraicGeometry.RingedToposHom.exists_shortExact_map_pullbackModules

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.