46 Adequate Modules

Chapter 46 of the Stacks Project, Adequate Modules, Tag 06Z1: the 8 sections of its 10 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 69 tags are carried by 159 declarations of the repository (all in StacksFrontier) and 4 registered declarations.

Section46.3 Adequate functors#

Section 46.3 of the Stacks Project, Tag 06US. 20 tags here are carried by 27 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06Z4, a definition

Tag 06Z4 in the Stacks Project.

Declarations registered for the tag:

Tag 06UT, a definition

Tag 06UT in the Stacks Project.

AdequateFunctor.IsAdequate, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Defs.lean, line 476. The attribute's comment: “part (1)”.

A module-valued functor is adequate if it is the kernel of the base changes of a map of A-modules.

public abbrev IsAdequate {A : Type u} [CommRing A]
    {C : Type u₁} [Category.{v₁} C] (ι : C ⥤ CommAlgCat.{max u v} A)
    (F : ModuleValuedFunctorOn.{w} ι) : Prop

AdequateFunctor.IsLinearlyAdequate, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Defs.lean, line 488. The attribute's comment: “part (2)”.

A module-valued functor is linearly adequate if it is the kernel of a morphism between the module-valued functors associated to two finite free modules.

public abbrev IsLinearlyAdequate {A : Type u} [CommRing A]
    {C : Type u₁} [Category.{v₁} C] (ι : C ⥤ CommAlgCat.{max u v} A)
    (F : ModuleValuedFunctorOn.{w} ι) : Prop
Tag 06UU, a lemma

Tag 06UU in the Stacks Project.

AdequateFunctor.isColimit_mapCocone_of_isAdequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Colimit.lean, line 616.

An adequate functor sends filtered colimits of commutative algebras to colimits of its underlying additive groups.

public theorem isColimit_mapCocone_of_isAdequate
    {A : Type u} [CommRing A] (F : AdequateFunctor.ModuleValuedFunctor.{w, v} A)
    (hF : AdequateFunctor.IsAdequate (𝟭 _) F)
    {I : Type i} [Category.{j} I] [IsFiltered I]
    [UnivLE.{i, max u v}] [UnivLE.{j, max u v}]
    {D : I ⥤ ((CommAlgCat.{max u v} A)ᵒᵖ)ᵒᵖ}
    {c : Cocone D} (hc : IsColimit c) :
    Nonempty (IsColimit (F.presheaf.mapCocone c))
Tag 06UW, a lemma

Tag 06UW in the Stacks Project.

AdequateFunctor.moduleValuedFunctorBaseChangeMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/BaseChange.lean, line 313.

An adequate functor on a chosen algebra domain commutes with flat base change along every morphism in that domain.

public theorem moduleValuedFunctorBaseChangeMap_bijective {A : Type u} [CommRing A]
    {D : Type u₁} [Category.{v₁} D] (ι : D ⥤ CommAlgCat.{max u v} A)
    (F : ModuleValuedFunctorOn.{w} ι) (hF : IsAdequate ι F)
    {B C : D} (f : B ⟶ C) (hf : RingHom.Flat (ι.map f).hom.toRingHom) :
    Function.Bijective (moduleValuedFunctorBaseChangeMap ι F f)
Tag 06UX, a lemma

Tag 06UX in the Stacks Project.

AdequateFunctor.exists_coproduct_linearlyAdequate_surjective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Colimit.lean, line 1150.

An adequate functor is a pointwise quotient of a direct sum of linearly adequate functors.

public lemma exists_coproduct_linearlyAdequate_surjective
    {A : Type u} [CommRing A]
    (F : AdequateFunctor.ModuleValuedFunctor.{w, v} A)
    (hF : AdequateFunctor.IsAdequate (𝟭 _) F) :
    ∃ (ι : Type (max u v w))
      (L : ι → AdequateFunctor.ModuleValuedFunctor.{max u v w, v} A),
      (∀ i, AdequateFunctor.IsLinearlyAdequate (𝟭 _) (L i)) ∧
        ∃ (f : (∐ L) ⟶
          (AdequateFunctor.presheafOfModulesUliftFunctor.{max u v, w}
            (AdequateFunctor.algebraRingDiagram.{v} A)).obj F),
          ∀ X, Function.Surjective (f.app X)

AdequateFunctor.exists_jointlyEpi_isLinearlyAdequate, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/Vanishing.lean, line 212. The attribute's comment: “the linearly adequate functors jointly cover an adequate functor”.

Every adequate module-valued functor carries a jointly epimorphic family of morphisms from linearly adequate functors.

public lemma exists_jointlyEpi_isLinearlyAdequate
    (K : ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A) (hK : IsAdequate (𝟭 _) K) :
    ∃ (J : Type (max (u + 1) (v + 1) w))
      (L : J → ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A) (g : ∀ j, L j ⟶ K),
      (∀ j, IsLinearlyAdequate (𝟭 _) (L j)) ∧
        ∀ {Z : ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A} (a b : K ⟶ Z),
          (∀ j, g j ≫ a = g j ≫ b) → a = b

AdequateFunctor.isSeparating_adequateOfLinearPresentation, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/Coreflection.lean, line 183. The attribute's comment: “the linearly adequate functors separate the adequate functors”.

The linearly adequate functors form a separating family for the adequate functors: by [Stacks, Tag 06UX] every adequate functor is a pointwise quotient of a direct sum of linearly adequate functors, and each summand is isomorphic to one of the chosen family.

public lemma isSeparating_adequateOfLinearPresentation :
    (ObjectProperty.ofObj (adequateOfLinearPresentation.{u, v, w} A)).IsSeparating
Tag 06UY, an equation

Tag 06UY in the Stacks Project.

AdequateFunctor.Laurent.weightSpace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Laurent.lean, line 94.

The weight-k part of F(B) consists of those elements whose images under the constant and grading maps differ by multiplication by T k.

public def weightSpace (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (F : ModuleValuedFunctor A) (𝒜 : ℕ → Submodule A B) [GradedAlgebra 𝒜] (k : ℤ) :
    Set (F.obj (Opposite.op (Opposite.op (CommAlgCat.of A B))))
Tag 06UZ, a lemma

Tag 06UZ in the Stacks Project.

AdequateFunctor.Laurent.existsUnique_finsupp_weightSpace_eq, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Laurent.lean, line 1004. The attribute's comment: “part (1)”.

Every element of the value of a flat-base-change-compatible module-valued functor on a graded algebra has a unique finite decomposition into elements of its integer weight spaces.

public lemma existsUnique_finsupp_weightSpace_eq (A B : Type u) [CommRing A] [CommRing B]
    [Algebra A B] (F : ModuleValuedFunctor A) (hF : PreservesFlatBaseChange A F)
    (𝒜 : ℕ → Submodule A B) [GradedAlgebra 𝒜]
    (x : F.obj (Opposite.op (Opposite.op (CommAlgCat.of A B)))) :
    ∃! y : ℤ →₀ F.obj (Opposite.op (Opposite.op (CommAlgCat.of A B))),
      (∀ k, y k ∈ weightSpace A B F 𝒜 k) ∧ y.sum (fun _ z ↦ z) = x

AdequateFunctor.Laurent.map_degreeZeroProjection_mem_weightSpace_zero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Laurent.lean, line 1049. The attribute's comment: “part (2)”.

The endomorphism induced by projection of a graded algebra onto degree zero takes every element of the functor's value into its weight-zero space.

public lemma map_degreeZeroProjection_mem_weightSpace_zero (A B : Type u) [CommRing A]
    [CommRing B] [Algebra A B] (F : ModuleValuedFunctor A)
    (𝒜 : ℕ → Submodule A B) [GradedAlgebra 𝒜]
    (x : F.obj (Opposite.op (Opposite.op (CommAlgCat.of A B)))) :
    F.map ((CommAlgCat.ofHom (degreeZeroProjection A B 𝒜)).op.op) x ∈
      weightSpace A B F 𝒜 0
Tag 06V0, a lemma

Tag 06V0 in the Stacks Project.

AdequateFunctor.exists_lift_from_finite_free_kernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/FiniteFreeLift/LargeAndDomainLift.lean, line 253.

Stacks Lemma 06V0. A morphism from the kernel of a morphism between finite free module-valued functors to a module-valued functor extends to the middle finite free functor.

public theorem exists_lift_from_finite_free_kernel
    (A : Type u) [CommRing A] (M : Type (max u w)) [AddCommGroup M] [Module A M]
    (n m : ℕ) (L : ModuleValuedFunctor.{max u v w, v} A)
    (i : L ⟶ moduleExtensionOfCarrier A (finiteFreeModule.{w} A n))
    (d : moduleExtensionOfCarrier A (finiteFreeModule.{w} A n) ⟶
      moduleExtensionOfCarrier A (finiteFreeModule.{w} A m))
    (φ : L ⟶ moduleExtensionOfCarrier A M) [Mono i] (hd : i ≫ d = 0)
    (h : (ShortComplex.mk i d hd).Exact) :
    ∃ ψ : moduleExtensionOfCarrier A (finiteFreeModule.{w} A n) ⟶
      moduleExtensionOfCarrier A M, i ≫ ψ = φ
Tag 06V1, a lemma

Tag 06V1 in the Stacks Project.

AdequateFunctor.isAdequate_cokernel_to_moduleExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/CokernelToExtension.lean, line 220.

The cokernel of a map from an adequate functor to the functor of a module is adequate.

public theorem isAdequate_cokernel_to_moduleExtension
    (A : Type u) [CommRing A]
    (F : ModuleValuedFunctor.{max u v w, v} A)
    (M : ModuleCat.{w} A)
    (φ : F ⟶ moduleExtension.{w, v} A M)
    (hF : IsAdequate (𝟭 _) F) : IsAdequate (𝟭 _) (cokernel φ)
Tag 06V2, a lemma

Tag 06V2 in the Stacks Project.

AdequateFunctor.isAdequate_cokernel, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/Cokernels.lean, line 82.

Cokernels of morphisms between adequate functors are adequate.

public lemma isAdequate_cokernel {A : Type u} [CommRing A]
    {F G : ModuleValuedFunctor.{w, v} A} (φ : F ⟶ G)
    (hF : IsAdequate (𝟭 _) F) (hG : IsAdequate (𝟭 _) G) :
    IsAdequate (𝟭 _) (cokernel φ)
Tag 06V3, a lemma

Tag 06V3 in the Stacks Project.

AdequateFunctor.isAdequate_kernel, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/Kernels.lean, line 132.

The kernel of a map of adequate module-valued functors is adequate.

public lemma isAdequate_kernel {A : Type u} [CommRing A]
    {F G : ModuleValuedFunctor.{w, v} A} (φ : F ⟶ G)
    (hF : IsAdequate (𝟭 _) F) (hG : IsAdequate (𝟭 _) G) :
    IsAdequate (𝟭 _) (kernel φ)
Tag 06V4, a lemma

Tag 06V4 in the Stacks Project.

AdequateFunctor.isAdequate_coproduct, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/Colimits.lean, line 153. The attribute's comment: “direct sums”.

Stacks Lemma 06V4, direct sums. A direct sum of adequate functors is adequate.

public lemma isAdequate_coproduct {ι : Type i} [Small.{max u v w} ι]
    (F : ι → ModuleValuedFunctor.{max u v w, v} A) [HasCoproduct F]
    (hF : ∀ a, IsAdequate (𝟭 _) (F a)) :
    IsAdequate (𝟭 _) (∐ F)

AdequateFunctor.isAdequate_colimit, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/Colimits.lean, line 164. The attribute's comment: “colimits”.

Stacks Lemma 06V4, colimits. A colimit of adequate functors is adequate.

public lemma isAdequate_colimit {J : Type j} [Category.{k} J]
    [EssentiallySmall.{max u v w} J]
    (F : J ⥤ ModuleValuedFunctor.{max u v w, v} A) [HasColimit F]
    (hF : ∀ a, IsAdequate (𝟭 _) (F.obj a)) :
    IsAdequate (𝟭 _) (colimit F)
Tag 06V5, a lemma

Tag 06V5 in the Stacks Project.

AdequateFunctor.Laurent.naturalTransformation_lifts_of_units_of_flatBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Laurent.lean, line 1086.

An additive natural transformation of module-valued functors which commutes with multiplication by units is induced by a morphism of module-valued functors, provided the target commutes with flat base change.

public theorem naturalTransformation_lifts_of_units_of_flatBaseChange
    (A : Type u) [CommRing A]
    (F G : PresheafOfModules.{v} (algebraRingFunctor A))
    (φ : F.presheaf ⟶ G.presheaf)
    (hunit : ∀ (B : ((CommAlgCat.{u} A)ᵒᵖ)ᵒᵖ)
      (x : F.obj B) (a : Units ((algebraRingFunctor A).obj B)),
      φ.app B ((a : (algebraRingFunctor A).obj B) • x) =
        (a : (algebraRingFunctor A).obj B) • (φ.app B x : G.obj B))
    (hbase : ∀ {B B' : ((CommAlgCat.{u} A)ᵒᵖ)ᵒᵖ} (f : B ⟶ B'),
      letI : Algebra ((algebraCommRingFunctor A).obj B)
          ((algebraCommRingFunctor A).obj B') :=
        ((algebraCommRingFunctor A).map f).hom.toAlgebra
      Module.Flat ((algebraCommRingFunctor A).obj B)
          ((algebraCommRingFunctor A).obj B') →
        ∃ e : TensorProduct ((algebraCommRingFunctor A).obj B)
              ((algebraCommRingFunctor A).obj B') (G.obj B) ≃ₗ[
                (algebraCommRingFunctor A).obj B'] G.obj B',
          ∀ x : G.obj B,
            e ((1 : (algebraCommRingFunctor A).obj B') ⊗ₜ[
              (algebraCommRingFunctor A).obj B] x) = G.map f x) :
    ∃ ψ : F ⟶ G,
      (PresheafOfModules.toPresheaf (algebraRingFunctor A)).map ψ = φ
Tag 06V6, a lemma

Tag 06V6 in the Stacks Project.

AdequateFunctor.isAdequate_of_moduleExtension_shortExact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Splitting.lean, line 1615.

Stacks 06V6. Let A be a ring and let 0 → M → G → L → 0 be a short exact sequence of module-valued functors on Alg_A, where M is the functor B ↦ B ⊗[A] M of an A-module M and L is linearly adequate. Then G is adequate.

public lemma isAdequate_of_moduleExtension_shortExact {A : Type u} [CommRing A]
    (M : ModuleCat.{u} A) (G L : ModuleValuedFunctor.{u, u} A)
    (i : moduleExtension.{u, u} A M ⟶ G) (p : G ⟶ L) (hip : i ≫ p = 0)
    (hS : (ShortComplex.mk i p hip).ShortExact)
    (hL : AdequateFunctor.IsLinearlyAdequate (𝟭 _) L) :
    AdequateFunctor.IsAdequate (𝟭 _) G
Tag 06V7, a remark

Tag 06V7 in the Stacks Project.

AdequateFunctor.weightOne_eq_add_images, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Splitting.lean, line 624. The attribute's comment: “degree-one generation by the two factors”.

The weight-one part over the symmetric algebra on two copies of a finitely presented module is the sum of the images from each copy.

public lemma weightOne_eq_add_images {A M : Type u} [CommRing A]
    [AddCommGroup M] [Module A M] [Module.FinitePresentation A M]
    (F : Laurent.ModuleValuedFunctor A) (hF : AdequateFunctor.IsAdequate (𝟭 _) F)
    (𝒜 : ℕ → Submodule A (SymmetricAlgebra A M)) [GradedAlgebra 𝒜]
    (ℬ : ℕ → Submodule A (SymmetricAlgebra A (M × M))) [GradedAlgebra ℬ]
    (h𝒜 : ∀ m, SymmetricAlgebra.ι A M m ∈ 𝒜 1)
    (hℬ : ∀ m, SymmetricAlgebra.ι A (M × M) m ∈ ℬ 1) :
    let p₁ : SymmetricAlgebra A M →ₐ[A] SymmetricAlgebra A (M × M) :=
      SymmetricAlgebra.lift ((SymmetricAlgebra.ι A (M × M)).comp (LinearMap.inl A M M))
    let p₂ : SymmetricAlgebra A M →ₐ[A] SymmetricAlgebra A (M × M) :=
      SymmetricAlgebra.lift ((SymmetricAlgebra.ι A (M × M)).comp (LinearMap.inr A M M))
    ∀ z, z ∈ AdequateFunctor.Laurent.weightSpace A (SymmetricAlgebra A (M × M)) F ℬ 1 ↔
      ∃ x y, ∃ z₁ z₂ : F.obj (Opposite.op (Opposite.op
          (CommAlgCat.of A (SymmetricAlgebra A (M × M))))),
        x ∈ AdequateFunctor.Laurent.weightSpace A (SymmetricAlgebra A M) F 𝒜 1 ∧
        y ∈ AdequateFunctor.Laurent.weightSpace A (SymmetricAlgebra A M) F 𝒜 1 ∧
        z₁ = F.map ((CommAlgCat.ofHom p₁).op.op) x ∧
        z₂ = F.map ((CommAlgCat.ofHom p₂).op.op) y ∧ z = z₁ + z₂

AdequateFunctor.weightOne_images_disjoint, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Splitting.lean, line 699. The attribute's comment: “directness of the degree-one sum”.

The two factor images in weight one have zero intersection.

public lemma weightOne_images_disjoint {A M : Type u} [CommRing A]
    [AddCommGroup M] [Module A M] [Module.FinitePresentation A M]
    (F : Laurent.ModuleValuedFunctor A) (hF : AdequateFunctor.IsAdequate (𝟭 _) F)
    (𝒜 : ℕ → Submodule A (SymmetricAlgebra A M)) [GradedAlgebra 𝒜]
    (ℬ : ℕ → Submodule A (SymmetricAlgebra A (M × M))) [GradedAlgebra ℬ]
    (h𝒜 : ∀ m, SymmetricAlgebra.ι A M m ∈ 𝒜 1)
    (hℬ : ∀ m, SymmetricAlgebra.ι A (M × M) m ∈ ℬ 1) :
    let p₁ : SymmetricAlgebra A M →ₐ[A] SymmetricAlgebra A (M × M) :=
      SymmetricAlgebra.lift ((SymmetricAlgebra.ι A (M × M)).comp (LinearMap.inl A M M))
    let p₂ : SymmetricAlgebra A M →ₐ[A] SymmetricAlgebra A (M × M) :=
      SymmetricAlgebra.lift ((SymmetricAlgebra.ι A (M × M)).comp (LinearMap.inr A M M))
    ∀ x y, ∀ z₁ z₂ : F.obj (Opposite.op (Opposite.op
        (CommAlgCat.of A (SymmetricAlgebra A (M × M))))),
      x ∈ AdequateFunctor.Laurent.weightSpace A (SymmetricAlgebra A M) F 𝒜 1 →
      y ∈ AdequateFunctor.Laurent.weightSpace A (SymmetricAlgebra A M) F 𝒜 1 →
      z₁ = F.map ((CommAlgCat.ofHom p₁).op.op) x →
      z₂ = F.map ((CommAlgCat.ofHom p₂).op.op) y → z₁ + z₂ = 0 →
        x = 0 ∧ y = 0

AdequateFunctor.exists_retraction_of_shortExact_of_baseChange_weightOne, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Splitting.lean, line 1564. The attribute's comment: “splitting under flat base change and weight-one decomposition”.

An extension of a linearly adequate functor splits if its kernel functor commutes with flat base change and has a direct weight-one coproduct decomposition.

public lemma exists_retraction_of_shortExact_of_baseChange_weightOne
    {A : Type u} [CommRing A]
    {F E L : ModuleValuedFunctor.{u, u} A}
    (i : F ⟶ E) (p : E ⟶ L) (hip : i ≫ p = 0)
    (hS : (ShortComplex.mk i p hip).ShortExact)
    (hflat : Laurent.PreservesFlatBaseChange A F)
    (hweight : HasWeightOneCoproduct F)
    (hL : AdequateFunctor.IsLinearlyAdequate (𝟭 _) L) :
    ∃ r : E ⟶ F, i ≫ r = 𝟙 F

AdequateFunctor.exists_retraction_of_shortExact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Splitting.lean, line 1589. The attribute's comment: “splitting of extensions”.

Stacks 06V7. An extension of a linearly adequate functor by an adequate functor admits a retraction onto its kernel term. An adequate functor commutes with flat base change by Stacks 06UW, and its weight-one part decomposes by Stacks 06UZ, which are the only two properties of the kernel the splitting uses.

public lemma exists_retraction_of_shortExact {A : Type u} [CommRing A]
    {F E L : ModuleValuedFunctor.{u, u} A}
    (i : F ⟶ E) (p : E ⟶ L) (hip : i ≫ p = 0)
    (hS : (ShortComplex.mk i p hip).ShortExact)
    (hF : AdequateFunctor.IsAdequate (𝟭 _) F)
    (hL : AdequateFunctor.IsLinearlyAdequate (𝟭 _) L) :
    ∃ r : E ⟶ F, i ≫ r = 𝟙 F

Declarations registered for the tag:

Tag 06V8, a lemma

Tag 06V8 in the Stacks Project.

AdequateFunctor.isAdequate_of_shortExact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/Extensions.lean, line 107.

Stacks Lemma 06V8. Let A be a ring and let 0 → F → G → H → 0 be a short exact sequence of module-valued functors on Alg_A. If F and H are adequate, so is G.

public lemma isAdequate_of_shortExact {A : Type u} [CommRing A]
    (S : ShortComplex (ModuleValuedFunctor.{u, u} A)) (hS : S.ShortExact)
    (h₁ : IsAdequate (𝟭 _) S.X₁) (h₃ : IsAdequate (𝟭 _) S.X₃) :
    IsAdequate (𝟭 _) S.X₂
Tag 06V9, a lemma

Tag 06V9 in the Stacks Project.

AdequateFunctor.IsAdequate.restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/Restriction.lean, line 242.

An adequate functor stays adequate after restriction along a ring homomorphism, with its values lifted to include the source ring universe.

public theorem IsAdequate.restrict (f : A →+* A')
    (F : ModuleValuedFunctor.{w, max u u' v} A)
    (hF : IsAdequate.{w, max u u' v} (𝟭 _) F) :
    IsAdequate.{max u w, max u u' v} (𝟭 _)
      ((presheafOfModulesUliftFunctor.{u} (algebraRingDiagram.{max u u' v} A')).obj
        ((restrictFunctor.{w, v} f).obj F))
Tag 06VA, a lemma

Tag 06VA in the Stacks Project.

AdequateFunctor.isAdequate_pushforward, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Pushforward.lean, line 76.

Adequacy is preserved by extension of the base ring in the argument.

public lemma isAdequate_pushforward
    (F' : AdequateFunctor.ModuleValuedFunctor.{w, u} A')
    (hF' : AdequateFunctor.IsAdequate.{w, u} (A := A') (𝟭 _) F') :
    AdequateFunctor.IsAdequate.{w, u} (A := A) (𝟭 _) (pushforward f F')
Tag 06VB, a lemma

Tag 06VB in the Stacks Project.

AdequateFunctor.adequateFunctorProductEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/Products/Equivalence.lean, line 544.

Adequate module-valued functors over a finite product of rings correspond to families of adequate module-valued functors over its factors. The inverse equivalence has a componentwise comparison natural in both the algebra and the family of factors.

public noncomputable def adequateFunctorProductEquivalence (n : ℕ)
    (A : Fin n → Type u) [∀ i, CommRing (A i)] :
    { e : (ObjectProperty.FullSubcategory
        (fun F : ModuleValuedFunctor.{w, v} (∀ i, A i) =>
          IsAdequate (𝟭 _) F)) ≌
        (∀ i : Fin n,
          ObjectProperty.FullSubcategory
            (fun F : ModuleValuedFunctor.{w, v} (A i) =>
              IsAdequate (𝟭 _) F)) //
      ProductEquivalenceSpecification n A e }
Tag 06VH, a lemma

Tag 06VH in the Stacks Project.

AdequateFunctor.isAdequate_of_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateFunctors/Descent.lean, line 586.

Adequacy descends through an exact Čech equalizer.

public theorem isAdequate_of_descent {A A' : Type u}
    [CommRing A] [CommRing A'] (f : A →+* A')
    (F : ModuleValuedFunctor.{w, u} A)
    (F' : ModuleValuedFunctor.{w, u} A')
    (hF' : IsAdequate (𝟭 _) F')
    (hrestrict : Nonempty
      (F' ≅ (PresheafOfModules.pushforward₀ (restrictScalars f).op
        (algebraRingDiagram A)).obj F))
    (hexact : CechExact f F) :
    IsAdequate (𝟭 _) F
Sources
LeanAdequateFunctor.ModuleValuedFunctor · AdequateFunctor.IsAdequate · AdequateFunctor.IsLinearlyAdequate · AdequateFunctor.isColimit_mapCocone_of_isAdequate · AdequateFunctor.moduleValuedFunctorBaseChangeMap_bijective · AdequateFunctor.exists_coproduct_linearlyAdequate_surjective · AdequateFunctor.exists_jointlyEpi_isLinearlyAdequate · AdequateFunctor.isSeparating_adequateOfLinearPresentation

Section46.4 Higher exts of adequate functors#

Section 46.4 of the Stacks Project, Tag 06Z5. 11 tags here are carried by 43 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06Z6, a lemma

Tag 06Z6 in the Stacks Project.

AdequateFunctor.exists_adequate_homEquiv, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/Coreflection.lean, line 264.

Stacks Project, Tag 06Z6. For every module-valued functor F there is an adequate functor Q F and a morphism Q F ⟶ F of module-valued functors such that every morphism to F from an adequate functor factors uniquely through it.

public lemma exists_adequate_homEquiv
    (F : ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A) :
    ∃ (QF : ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A)
      (_ : IsAdequate (𝟭 _) QF) (q : QF ⟶ F),
      ∀ (G : ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A), IsAdequate (𝟭 _) G →
        ∀ φ : G ⟶ F, ∃! ψ : G ⟶ QF, ψ ≫ q = φ
Tag 06Z7, a lemma

Tag 06Z7 in the Stacks Project.

AdequateFunctor.moduleValuedFunctor_enoughInjectives, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/Basic.lean, line 49. The attribute's comment: “module_valued_functors_enough_injectives”.

Stacks Project, Tag 06Z7. Module-valued functors on any category of algebras, in particular the algebras admitted by a big site, have enough injectives.

instance moduleValuedFunctor_enoughInjectives (C : Type u) [Category.{v} C]
    (R : Cᵒᵖ ⥤ RingCat.{w}) :
    EnoughInjectives (PresheafOfModules.{max u v w t} R)

AdequateFunctor.fullyFaithful_adequateInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/Coreflection.lean, line 93. The attribute's comment: “part (1), i is fully faithful”.

Stacks Project, Tag 06Z7, part (1), the full faithfulness of i. The adequate functors form a full subcategory of the module-valued functors, so their inclusion is fully faithful.

public noncomputable def fullyFaithful_adequateInclusion :
    (adequate.{u, v, max u v w} A).ι.FullyFaithful

AdequateFunctor.preservesFiniteLimits_adequateInclusion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/Coreflection.lean, line 101. The attribute's comment: “part (1), i is left exact”.

Stacks Project, Tag 06Z7, part (1), the left exactness of i. The adequate functors are closed under kernels, so a kernel of adequate functors is already the kernel of the underlying module-valued functors.

public lemma preservesFiniteLimits_adequateInclusion :
    PreservesFiniteLimits (adequate.{u, v, max u v w} A).ι

AdequateFunctor.preservesFiniteColimits_adequateInclusion, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/Coreflection.lean, line 111. The attribute's comment: “part (1), i is right exact”.

Stacks Project, Tag 06Z7, part (1), the right exactness of i. The adequate functors are closed under cokernels, so a cokernel of adequate functors is already the cokernel of the underlying module-valued functors.

public lemma preservesFiniteColimits_adequateInclusion :
    PreservesFiniteColimits (adequate.{u, v, max u v w} A).ι

AdequateFunctor.adequateCoreflectionAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/Coreflection.lean, line 255. The attribute's comment: “part (3), Q is a right adjoint to i”.

Stacks Project, Tag 06Z7, part (3), the adjunction itself: the functor Q of [Stacks, Tag 06Z6] is a right adjoint to the inclusion i of the adequate module-valued functors into all module-valued functors.

public noncomputable def adequateCoreflectionAdjunction :
    (adequate.{u, v, max (u + 1) (v + 1) w} A).ι ⊣ adequateCoreflection.{u, v, w} A

AdequateFunctor.preservesFiniteLimits_adequateCoreflection, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/Coreflection.lean, line 292. The attribute's comment: “part (3), Q is left exact”.

Stacks Project, Tag 06Z7, part (3), the left exactness: a right adjoint preserves all limits, in particular the finite ones.

public lemma preservesFiniteLimits_adequateCoreflection :
    PreservesFiniteLimits (adequateCoreflection.{u, v, w} A)

AdequateFunctor.preservesInjectiveObjects_adequateCoreflection, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/Coreflection.lean, line 301. The attribute's comment: “part (4)”.

Stacks Project, Tag 06Z7, part (4). The functor Q transforms injectives into injectives: it is right adjoint to the exact functor i, so [Stacks, Tag 015Z] applies.

public lemma preservesInjectiveObjects_adequateCoreflection :
    (adequateCoreflection.{u, v, w} A).PreservesInjectiveObjects

AdequateFunctor.adequateFunctor_enoughInjectives, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/EnoughInjectives.lean, line 91. The attribute's comment: “adequate_functors_enough_injectives”.

Stacks Project, Tag 06Z7. The adequate module-valued functors on the commutative A-algebras have enough injectives: every one of them embeds into the extension of a pure injective A-module, and such an extension is an injective object.

public instance adequateFunctor_enoughInjectives {A : Type u} [CommRing A] :
    EnoughInjectives ((adequate.{u, v, max u v w} A).FullSubcategory)

AdequateFunctor.adequate_isWeakSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/WeakSerre.lean, line 79. The attribute's comment: “part (1), the image of i is a weak Serre subcategory”.

Stacks Project, Tag 06Z7, part (1), the image of i is a weak Serre subcategory. The adequate module-valued functors are a strictly full subcategory containing the zero functor and closed under kernels, cokernels and extensions, which is the characterisation of a weak Serre subcategory of [Stacks, Tag 0754].

public instance adequate_isWeakSerreClass :
    (adequate.{u, u, u} A).IsWeakSerreClass

AdequateFunctor.adequateInclusion_fullyFaithful_exact_isWeakSerreClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/WeakSerre.lean, line 95. The attribute's comment: “part (1)”.

Stacks Project, Tag 06Z7, part (1), in full and at one instantiation: the inclusion i of the adequate module-valued functors into all module-valued functors on Alg_A is fully faithful and exact, and its image is a weak Serre subcategory.

The three conjuncts other than the last are instantiations of AdequateFunctor.fullyFaithful_adequateInclusion, AdequateFunctor.preservesFiniteLimits_adequateInclusion and AdequateFunctor.preservesFiniteColimits_adequateInclusion, which hold at the wider adequate.{u, v, max u v w}; the last holds at the universes of AdequateFunctor.isAdequate_of_shortExact. This conjunction records that all four are simultaneously available for one and the same category, namely the module-valued functors on the A-algebras whose carriers lie in the universe of A.

public theorem adequateInclusion_fullyFaithful_exact_isWeakSerreClass :
    (adequate.{u, u, u} A).ι.Full ∧ (adequate.{u, u, u} A).ι.Faithful ∧
      PreservesFiniteLimits (adequate.{u, u, u} A).ι ∧
      PreservesFiniteColimits (adequate.{u, u, u} A).ι ∧
      (adequate.{u, u, u} A).IsWeakSerreClass
Tag 06Z8, a lemma

Tag 06Z8 in the Stacks Project.

AdequateFunctor.tangentKernel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 213. The attribute's comment: “parts (1) and (2): the kernel with its restricted module structure”.

The tangent kernel, with scalars restricted along the zero section B → B[N].

noncomputable def tangentKernel (X : AlgebraModulePair.{v} A) :
    Submodule X.algebra (extensionValue A F X)

AdequateFunctor.tangentFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 269. The attribute's comment: “part (3): the canonical tangent functor”.

The canonical tangent functor on pairs of algebras and modules.

noncomputable def tangentFunctor : TangentFunctorData A F

AdequateFunctor.tangentDecompositionData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 327. The attribute's comment: “the canonical direct-sum decomposition”.

The canonical decomposition, specified by the sum of the zero section and the kernel inclusion as its inverse.

noncomputable def tangentDecompositionData (X : AlgebraModulePair.{v} A) :
    TangentDecompositionData A F X

AdequateFunctor.tangentMultiplicationData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 404. The attribute's comment: “part (4): the canonical multiplication map”.

Multiplication by the square-zero ideal, specified on pure tensors.

noncomputable def tangentMultiplicationData (X : AlgebraModulePair.{v} A) :
    {μ : TensorProduct X.algebra X.module (moduleValue A F X.algebra) →ₗ[X.algebra]
        tangentModule A F X //
      ∀ (n : X.module) (y : moduleValue A F X.algebra),
        (μ (TensorProduct.tmul X.algebra n y) : extensionValue A F X) =
          squareZeroInr A X n •
            moduleValueMap A F (squareZeroSection A X) y}

AdequateFunctor.tangentDecomposition_fst, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 478. The attribute's comment: “the augmentation coordinate of the decomposition”.

The first coordinate of the canonical decomposition is the augmentation.

lemma tangentDecomposition_fst (X : AlgebraModulePair.{v} A) (x : extensionValue A F X) :
    (tangentDecomposition A F X x).1 =
      moduleValueMap A F (squareZeroAugmentation A X) x

AdequateFunctor.tangentDecomposition_naturality, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 493. The attribute's comment: “naturality of the decomposition”.

The decomposition is natural for morphisms of pairs, including changes of base algebra.

lemma tangentDecomposition_naturality {X Y : AlgebraModulePair.{v} A} (f : X ⟶ Y)
    (x : extensionValue A F X) :
    tangentDecomposition A F Y (moduleValueMap A F (squareZeroMap A f) x) =
      (moduleValueMap A F f.base (tangentDecomposition A F X x).1,
        (tangentFunctor A F).map f (tangentDecomposition A F X x).2)

AdequateFunctor.tangentMultiplication_naturality, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 520. The attribute's comment: “part (4): naturality of multiplication”.

The multiplication maps form a natural transformation on the category of pairs.

lemma tangentMultiplication_naturality {X Y : AlgebraModulePair.{v} A} (f : X ⟶ Y)
    (t : TensorProduct X.algebra X.module (moduleValue A F X.algebra)) :
    (tangentFunctor A F).map f (tangentMultiplication A F X t) =
      tangentMultiplication A F Y
        (TensorProduct.map f.linear (moduleValueMap A F f.base) t)

AdequateFunctor.tangentModule_subsingleton, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 549. The attribute's comment: “part (5): vanishing at the zero module”.

The tangent module of a zero module is zero.

lemma tangentModule_subsingleton (X : AlgebraModulePair.{v} A) [Subsingleton X.module] :
    Subsingleton (tangentModule A F X)

AdequateFunctor.tangentFunctor_map_eq_zero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 584. The attribute's comment: “part (5): zero module maps induce zero tangent maps”.

A morphism of pairs whose module map is zero induces the zero tangent map.

lemma tangentFunctor_map_eq_zero {X Y : AlgebraModulePair.{v} A} (f : X ⟶ Y)
    (hf : f.linear = 0) : (tangentFunctor A F).map f = 0
Tag 06ZA, a lemma

Tag 06ZA in the Stacks Project.

AdequateFunctor.epi_tangentFunctorAt_map_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/InjectiveTangentSurjective.lean, line 221. The attribute's comment: “Stacks erratum: only the surjectivity at TI(B, N₂). Exactness at TI(B, N), the other conjunct of the source's assertion that TI(B,N₁) → TI(B,N) → TI(B,N₂) → 0 is exact, is false as stated, and is refuted by AdequateFunctor.not_forall_hasRightExactTangentFunctor_of_injective. The module universe of I is taken to be the universe of the algebras.”.

Tag 06ZA, corrected. Stacks erratum. Let I be an injective object of the category of module-valued functors on Alg_A. For every A-algebra B and every short exact sequence 0 → N₁ → N → N₂ → 0 of B-modules, the map TI(B, N) → TI(B, N₂) is an epimorphism.

The source asserts more: that the whole sequence TI(B, N₁) → TI(B, N) → TI(B, N₂) → 0 is exact, which in this library is the predicate AdequateFunctor.HasRightExactTangentFunctor of Tag 06ZF. The other conjunct, exactness at TI(B, N), is false, and is refuted by AdequateFunctor.not_forall_hasRightExactTangentFunctor_of_injective: the counterexample takes the field k = ℚ, the algebra C = k[ε]/(ε²), the injective C-module J = Hom_k(C, k) and the coinduced functor I(D) = ∏_{α : D →ₐ C} J, whose tangent module TI(k, V) is the functions V^* → J vanishing at 0; on 0 → k → k² → k → 0 the function sending the first-coordinate functional to 0 ≠ j ∈ J and everything else to 0 is killed by TI(k, k²) → TI(k, k) and is not in the image of TI(k, k) → TI(k, k²), every element of which takes equal values at (1, 0) and (1, 1).

Surjectivity at TI(B, N₂) — the statement proved here, and the whole of what the source's assertion leaves standing — is unaffected: its proof does not use the coequalizer step that the counterexample refutes.

theorem epi_tangentFunctorAt_map_of_injective
    (I : PresheafOfModules.{v} (algebraStructurePresheaf.{v} A)) [Injective I]
    (B : Type v) [CommRing B] [Algebra A B] (S : ShortComplex (ModuleCat.{v} B))
    (hS : S.ShortExact) :
    Epi ((tangentFunctorAt A I B).map S.g)
Tag 06ZB, a lemma

Tag 06ZB in the Stacks Project.

AdequateFunctor.tangentTensorEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/FinitelyPresentedTangent.lean, line 763. The attribute's comment: “tensor_finitely_presented”.

The canonical tensor-product description of the tangent module of a finitely presented module, using the second action on both tangent modules.

noncomputable def tangentTensorEquiv
    (S : RightExactTangentFunctor.{u, v, w})
    (B : Type v) [CommRing B] [Algebra S.A B]
    (N : Type v) [AddCommGroup N] [Module B N]
    [Module.FinitePresentation B N] :
    let X : AlgebraModulePair.{v} S.A := { algebra := B, module := B }
    let Y : AlgebraModulePair.{v} S.A := { algebra := B, module := N }
    letI : Module B (tangentModule S.A S.F X) :=
      (secondModuleStructure S X).1
    letI : Module B (tangentModule S.A S.F Y) :=
      (secondModuleStructure S Y).1
    { e : TensorProduct B (tangentModule S.A S.F X) N ≃ₗ[B]
        tangentModule S.A S.F Y //
      ∀ (x : tangentModule S.A S.F X) (n : N),
        e (TensorProduct.tmul B x n) =
          (tangentFunctor S.A S.F).map
            ({ base := AlgHom.id S.A B
               linear := (LinearMap.id : B →ₗ[B] B).smulRight n } : X ⟶ Y) x }

AdequateFunctor.tangentModule_prod_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/SecondModuleStructure.lean, line 62. The attribute's comment: “direct_sum”.

A right exact tangent functor carries a binary direct sum of modules to the direct sum of their tangent modules, via the two projections.

theorem tangentModule_prod_bijective
    (T : RightExactTangentFunctor.{u, v, w})
    (B : Type v) [CommRing B] [Algebra T.A B]
    (N₁ N₂ : Type v) [AddCommGroup N₁] [Module B N₁]
    [AddCommGroup N₂] [Module B N₂] :
    Function.Bijective
      (fun x : tangentModule T.A T.F
          ({ algebra := B, module := N₁ × N₂ } : AlgebraModulePair.{v} T.A) =>
        ((tangentFunctor T.A T.F).map
            ({ base := AlgHom.id T.A B
               linear := LinearMap.fst B N₁ N₂ } :
              ({ algebra := B, module := N₁ × N₂ } : AlgebraModulePair.{v} T.A) ⟶
              ({ algebra := B, module := N₁ } : AlgebraModulePair.{v} T.A)) x,
         (tangentFunctor T.A T.F).map
            ({ base := AlgHom.id T.A B
               linear := LinearMap.snd B N₁ N₂ } :
              ({ algebra := B, module := N₁ × N₂ } : AlgebraModulePair.{v} T.A) ⟶
              ({ algebra := B, module := N₂ } : AlgebraModulePair.{v} T.A)) x))

AdequateFunctor.secondModuleStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/SecondModuleStructure.lean, line 299. The attribute's comment: “second_module_structure”.

The second module structure on a tangent module, characterized by the action induced by multiplication on the module variable.

noncomputable def secondModuleStructure (X : AlgebraModulePair.{v} S.A) :
    { m : Module X.algebra (tangentModule S.A S.F X) //
      ∀ (b : X.algebra) (x : tangentModule S.A S.F X),
        m.toDistribMulAction.toSMul.smul b x =
          secondScalarAction S.A S.F X x b }

AdequateFunctor.secondScalarAction_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/SecondModuleStructure.lean, line 403. The attribute's comment: “second_module_structure”.

Tangent maps commute with the second scalar action, semilinearly over their maps of base algebras.

theorem secondScalarAction_naturality {X Y : AlgebraModulePair.{v} S.A}
    (f : X ⟶ Y) (x : tangentModule S.A S.F X) (b : X.algebra) :
    (tangentFunctor S.A S.F).map f (secondScalarAction S.A S.F X x b) =
      secondScalarAction S.A S.F Y ((tangentFunctor S.A S.F).map f x) (f.base b)

AdequateFunctor.tangentMultiplication_smul_second, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/SecondModuleStructure.lean, line 455. The attribute's comment: “multiplication_map_linear”.

The canonical tangent multiplication map is linear for the second B-module structure on the tangent module.

theorem tangentMultiplication_smul_second (S : RightExactTangentFunctor.{u, v, w})
    (X : AlgebraModulePair.{v} S.A) (b : X.algebra)
    (t : TensorProduct X.algebra X.module (moduleValue S.A S.F X.algebra)) :
    (secondModuleStructure S X).val.toDistribMulAction.toSMul.smul b
        (tangentMultiplication S.A S.F X t) =
      tangentMultiplication S.A S.F X (b • t)

AdequateFunctor.secondScalarAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 619. The attribute's comment: “second_scalar_action”.

The second scalar operation on a tangent module, induced by multiplication on the module variable.

noncomputable def secondScalarAction (X : AlgebraModulePair.{v} A)
    (x : tangentModule A F X) (b : X.algebra) : tangentModule A F X
Tag 06ZC, an item

Tag 06ZC in the Stacks Project.

AdequateFunctor.tangentMultiplication_smul_second, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/SecondModuleStructure.lean, line 455.

The canonical tangent multiplication map is linear for the second B-module structure on the tangent module.

theorem tangentMultiplication_smul_second (S : RightExactTangentFunctor.{u, v, w})
    (X : AlgebraModulePair.{v} S.A) (b : X.algebra)
    (t : TensorProduct X.algebra X.module (moduleValue S.A S.F X.algebra)) :
    (secondModuleStructure S X).val.toDistribMulAction.toSMul.smul b
        (tangentMultiplication S.A S.F X t) =
      tangentMultiplication S.A S.F X (b • t)
Tag 06ZD, an item

Tag 06ZD in the Stacks Project.

AdequateFunctor.tangentTensorEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/FinitelyPresentedTangent.lean, line 763.

The canonical tensor-product description of the tangent module of a finitely presented module, using the second action on both tangent modules.

noncomputable def tangentTensorEquiv
    (S : RightExactTangentFunctor.{u, v, w})
    (B : Type v) [CommRing B] [Algebra S.A B]
    (N : Type v) [AddCommGroup N] [Module B N]
    [Module.FinitePresentation B N] :
    let X : AlgebraModulePair.{v} S.A := { algebra := B, module := B }
    let Y : AlgebraModulePair.{v} S.A := { algebra := B, module := N }
    letI : Module B (tangentModule S.A S.F X) :=
      (secondModuleStructure S X).1
    letI : Module B (tangentModule S.A S.F Y) :=
      (secondModuleStructure S Y).1
    { e : TensorProduct B (tangentModule S.A S.F X) N ≃ₗ[B]
        tangentModule S.A S.F Y //
      ∀ (x : tangentModule S.A S.F X) (n : N),
        e (TensorProduct.tmul B x n) =
          (tangentFunctor S.A S.F).map
            ({ base := AlgHom.id S.A B
               linear := (LinearMap.id : B →ₗ[B] B).smulRight n } : X ⟶ Y) x }
Tag 06ZF, a lemma

Tag 06ZF in the Stacks Project.

AdequateFunctor.rightExactTangentFunctor_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/RightExactPermanence.lean, line 260. The attribute's comment: “extension_permanence”.

Property (*) is stable under extensions of module-valued functors.

theorem rightExactTangentFunctor_of_shortExact
    (S : ShortComplex (PresheafOfModules.{w} (algebraStructurePresheaf.{v} A)))
    (hS : S.ShortExact)
    (hF : HasRightExactTangentFunctor A S.X₁)
    (hH : HasRightExactTangentFunctor A S.X₃) :
    HasRightExactTangentFunctor A S.X₂

AdequateFunctor.hasRightExactTangentFunctor_of_shortExact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/RightExactPermanence.lean, line 372. The attribute's comment: “quotient_permanence”.

Property (*) passes to the quotient in a short exact sequence of module-valued functors.

public lemma hasRightExactTangentFunctor_of_shortExact
    (A : Type u) [CommRing A]
    (S : ShortComplex (PresheafOfModules.{w} (AdequateFunctor.algebraStructurePresheaf.{v} A)))
    (hS : S.ShortExact)
    (hF : AdequateFunctor.HasRightExactTangentFunctor A S.X₁)
    (hG : AdequateFunctor.HasRightExactTangentFunctor A S.X₂) :
    AdequateFunctor.HasRightExactTangentFunctor A S.X₃

AdequateFunctor.hasRightExactTangentFunctor_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/RightExactPermanence.lean, line 508. The attribute's comment: “pullback_permanence”.

Property (*) passes to a pullback of a short exact sequence of module-valued functors.

public theorem hasRightExactTangentFunctor_pullback
    {A : Type u} [CommRing A]
    (S : ShortComplex (PresheafOfModules.{w} (algebraStructurePresheaf.{v} A)))
    (hS : S.ShortExact)
    {H' : PresheafOfModules.{w} (algebraStructurePresheaf.{v} A)}
    (f : H' ⟶ S.X₃)
    (hF : HasRightExactTangentFunctor A S.X₁)
    (hH' : HasRightExactTangentFunctor A H') :
    HasRightExactTangentFunctor A (pullback S.g f)

AdequateFunctor.HasRightExactTangentFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Adequate/Tangent/TangentFunctor.lean, line 683. The attribute's comment: “property”.

Property (*): over every A-algebra, the tangent functor sends a short exact sequence of modules to an exact sequence ending in an epimorphism.

abbrev HasRightExactTangentFunctor : Prop
Tag 06ZG, a lemma

Tag 06ZG in the Stacks Project.

AdequateFunctor.subsingleton_zExt_moduleExtension_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/FinitelyPresentedExtAll.lean, line 152. The attribute's comment: “every degree i > 0; the published proof via Tag 06ZA is replaced by the transfer along phi_N^ -| psi_N^ and a dual-number scaling argument”.

Stacks Project, Tag 06ZG. For A-modules M and P with P of finite presentation, Ext^i(P̲, M̲) = 0 for every i > 0 in the category of module-valued functors on the commutative A-algebras, where X̲ is B ↦ B ⊗[A] X.

theorem subsingleton_zExt_moduleExtension_of_finitePresentation
    (M P : ModuleCat.{max (u + 1) (v + 1) w} A) [Module.FinitePresentation A P]
    (i : ℤ) (hi : 0 < i) :
    Subsingleton (Abelian.zExt (moduleExtension.{max (u + 1) (v + 1) w, v} A P)
      (moduleExtension.{max (u + 1) (v + 1) w, v} A M) i)

AdequateFunctor.subsingleton_zExt_moduleExtension_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/FinitelyPresentedExtHigher.lean, line 129. The attribute's comment: “degree 3, by a double dimension shift to Ext¹ out of a linearly adequate functor, which vanishes by Tag 06V7”.

Stacks Project, Tag 06ZG in degree three. For an A-module P of finite presentation, Ext³ from the module-valued functor B ↦ B ⊗[A] P to B ↦ B ⊗[A] M vanishes in the category of module-valued functors on the commutative A-algebras.

theorem subsingleton_zExt_moduleExtension_three [Module.FinitePresentation A P] :
    Subsingleton (Abelian.zExt (moduleExtension.{max u v w, v} A P)
      (moduleExtension.{max u v w, v} A M) 3)

AdequateFunctor.subsingleton_zExt_moduleExtension_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/FinitelyPresentedExtTwo.lean, line 826. The attribute's comment: “degree 1, via the universal section over the square-zero extension by the cokernel of the transpose of a presentation”.

Stacks Project, Tag 06ZG in degree one. For an A-module P of finite presentation, Ext¹ from the module-valued functor B ↦ B ⊗[A] P to B ↦ B ⊗[A] M vanishes in the category of module-valued functors on the commutative A-algebras.

theorem subsingleton_zExt_moduleExtension_one [Module.FinitePresentation A P] :
    Subsingleton (Abelian.zExt (moduleExtension.{max u v w, v} A P)
      (moduleExtension.{max u v w, v} A M) 1)

AdequateFunctor.subsingleton_zExt_moduleExtension_two_large, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/FinitelyPresentedExtTwo.lean, line 837. The attribute's comment: “degree 2, via Tag 06V0 and projectivity of the free module functors”.

Stacks Project, Tag 06ZG in degree two. For an A-module P of finite presentation, Ext² from the module-valued functor B ↦ B ⊗[A] P to B ↦ B ⊗[A] M vanishes in the category of module-valued functors on the commutative A-algebras.

theorem subsingleton_zExt_moduleExtension_two_large [Module.FinitePresentation A P] :
    Subsingleton (Abelian.zExt (moduleExtension.{max u v w, v} A P)
      (moduleExtension.{max u v w, v} A M) 2)

AdequateFunctor.subsingleton_zExt_moduleExtension_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/FinitelyPresentedExtTwo.lean, line 867. The attribute's comment: “degree 2, via Tag 06V0 and projectivity of the free module functors”.

Stacks Project, Tag 06ZG in degree two. For an A-module P of finite presentation, Ext² from the module-valued functor B ↦ B ⊗[A] P to B ↦ B ⊗[A] M vanishes in the category of module-valued functors on the commutative A-algebras.

theorem subsingleton_zExt_moduleExtension_two [Module.FinitePresentation A P] :
    Subsingleton (Abelian.zExt (moduleExtension.{max u v, v} A P)
      (moduleExtension.{max u v, v} A M) 2)
Tag 06ZH, a lemma

Tag 06ZH in the Stacks Project.

AdequateFunctor.subsingleton_zExt_isLinearlyAdequate_moduleExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/FinitelyPresentedExtAll.lean, line 177. The attribute's comment: “every degree i > 0, by the source's two dimension shifts from Tag 06ZG”.

Stacks Project, Tag 06ZH. Let A be a ring, M an A-module and L a linearly adequate module-valued functor on the commutative A-algebras. Then Ext^i(L, M̲) = 0 for every i > 0, where M̲ is B ↦ B ⊗[A] M.

theorem subsingleton_zExt_isLinearlyAdequate_moduleExtension
    (L : ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A) (hL : IsLinearlyAdequate (𝟭 _) L)
    (M : ModuleCat.{max (u + 1) (v + 1) w} A) (i : ℤ) (hi : 0 < i) :
    Subsingleton (Abelian.zExt L (moduleExtension.{max (u + 1) (v + 1) w, v} A M) i)

AdequateFunctor.subsingleton_zExt_of_isLinearlyAdequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/LinearlyAdequate.lean, line 183. The attribute's comment: “The positive-degree vanishing for the functor of a finitely presented module, Tag 06ZG, is a hypothesis. Only its degree-two case is proved in this library, in AdequateFunctor.subsingleton_zExt_moduleExtension_two, while this proof needs degrees at least three: both short exact sequences used here are flanked by projective objects, so the degree shift along them is an isomorphism and those degrees of Tag 06ZG carry the content of this tag itself. The source derives Tag 06ZG from Tag 06ZA, which is false as stated and is refuted by AdequateFunctor.not_forall_hasRightExactTangentFunctor_of_injective.”.

Let A be a commutative ring, M an A-module and L a linearly adequate module-valued functor on the commutative A-algebras. Then Ext^i(L, M̲) vanishes for i > 0, where M̲ is the module-valued functor B ↦ B ⊗[A] M.

public theorem subsingleton_zExt_of_isLinearlyAdequate {A : Type u} [CommRing A]
    (L : ModuleValuedFunctor.{max u v w, v} A) (hL : IsLinearlyAdequate (𝟭 _) L)
    (M : ModuleCat.{max u v w} A)
    (hM : ∀ P : ModuleCat.{max u v w} A, Module.FinitePresentation A P → ∀ j : ℤ, 0 < j →
      Subsingleton (Abelian.zExt (moduleExtension.{max u v w, v} A P)
        (moduleExtension.{max u v w, v} A M) j))
    (i : ℤ) (hi : 0 < i) :
    Subsingleton (Abelian.zExt L (moduleExtension.{max u v w, v} A M) i)
Tag 06ZI, a lemma

Tag 06ZI in the Stacks Project.

AdequateFunctor.isZero_rightDerivedPlus_adequateCoreflection_of_isAdequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/FinitelyPresentedExtAll.lean, line 188. The attribute's comment: “every degree p > 0 and every adequate F”.

Stacks Project, Tag 06ZI. The higher right derived functors of the coreflection Q onto the adequate module-valued functors vanish: R^p Q(F) = 0 for every p > 0 and every adequate functor F.

theorem isZero_rightDerivedPlus_adequateCoreflection_of_isAdequate
    (F : ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A) (hF : IsAdequate (𝟭 _) F)
    (p : ℤ) (hp : 0 < p) :
    IsZero (((adequateCoreflection.{u, v, w} A).rightDerivedPlus p).obj F)

AdequateFunctor.isZero_rightDerivedPlus_one_adequateCoreflection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/Vanishing.lean, line 273. The attribute's comment: “degree 1, from Tag 06V7 and the covering of Tag 06UX”.

Stacks Project, Tag 06ZI in degree one. The first right derived functor of the coreflection Q onto the adequate module-valued functors vanishes on every adequate functor F. On an injective resolution F → I ⁎, a degree-one cycle of Q(I ⁎) restricted along a linearly adequate functor L is a boundary, because Ext¹(L, F) vanishes by Tag 06V7; the linearly adequate functors cover every adequate functor by Tag 06UX.

public theorem isZero_rightDerivedPlus_one_adequateCoreflection
    (F : ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A) (hF : IsAdequate (𝟭 _) F) :
    IsZero (((adequateCoreflection.{u, v, w} A).rightDerivedPlus 1).obj F)

AdequateFunctor.isZero_rightDerivedPlus_adequateCoreflection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/Vanishing.lean, line 334. The attribute's comment: “the positive-degree vanishing of the extension groups between extensions of modules, one finitely presented, is a hypothesis: that is Tag 06ZG, which is absent from this library.”.

Stacks Project, Tag 06ZI. The higher right derived functors of the coreflection Q onto the adequate module-valued functors vanish in positive degrees on every adequate functor.

public theorem isZero_rightDerivedPlus_adequateCoreflection
    (hFP : ∀ M P : ModuleCat.{max (u + 1) (v + 1) w} A, Module.FinitePresentation A P →
      ∀ j : ℤ, 0 < j → Subsingleton (Abelian.zExt
        (moduleExtension.{max (u + 1) (v + 1) w, v} A P)
        (moduleExtension.{max (u + 1) (v + 1) w, v} A M) j))
    (F : ModuleValuedFunctor.{max (u + 1) (v + 1) w, v} A) (hF : IsAdequate (𝟭 _) F)
    (p : ℤ) (hp : 0 < p) :
    IsZero (((adequateCoreflection.{u, v, w} A).rightDerivedPlus p).obj F)
Sources
LeanAdequateFunctor.exists_adequate_homEquiv · AdequateFunctor.moduleValuedFunctor_enoughInjectives · AdequateFunctor.fullyFaithful_adequateInclusion · AdequateFunctor.preservesFiniteLimits_adequateInclusion · AdequateFunctor.preservesFiniteColimits_adequateInclusion · AdequateFunctor.adequateCoreflectionAdjunction · AdequateFunctor.preservesFiniteLimits_adequateCoreflection · AdequateFunctor.preservesInjectiveObjects_adequateCoreflection

Section46.5 Adequate modules#

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

Tag 06VF, the section

Tag 06VF in the Stacks Project.

Declarations registered for the tag:

Tag 06VG, a definition

Tag 06VG in the Stacks Project.

Stacks.Adequate.IsAdequate, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/AdequateSheafOfModules.lean, line 313.

Adequacy of a sheaf of modules on the selected big site.

public abbrev IsAdequate
    {τ : CoveringTopology} {S : Scheme.{u}} (B : BigSite τ S)
    (F : SheafOfModules.{m} B.structureSheaf) : Prop
Tag 06VI, a lemma

Tag 06VI in the Stacks Project.

Stacks.Adequate.isAdequate_affineSectionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AffineLocalUnconditional.lean, line 72.

[Stacks, Tag 06VI]: for an adequate sheaf of modules F on the big τ-site over S, the affine-section functor F_{F, A} is adequate for every affine scheme Spec A of the site over S, not only for the members of the covering witnessing adequacy of F.

All three steps of the source's proof are supplied by the library: Stacks.Adequate.standardAffineRefinement and Stacks.Adequate.affineSectionRestriction, which discharge StandardAffineRefinement and AffineSectionRestriction, and Stacks.Adequate.standardAffineDescent, which discharges StandardAffineDescent. See the module documentation.

public theorem isAdequate_affineSectionFunctor
    {τ : CoveringTopology} {S : Scheme.{u}} (B : BigSite τ S)
    (F : SheafOfModules.{max u m} B.structureSheaf)
    (hF : IsAdequate B F)
    (A : CommRingCat.{u}) (f : Spec A ⟶ S)
    (hA : schemeSizeBelow B.cutoff (Spec A)) :
    AdequateFunctor.IsAdequate
      (AdequateFunctor.siteAlgebraInclusion A (schemeSizeBelow B.cutoff))
      (affineSectionFunctor B F A f)
Tag 06ZJ, a lemma

Tag 06ZJ in the Stacks Project.

Stacks.Adequate.isEquivalence_adequateComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AffineEquivalence.lean, line 78. The attribute's comment: “the equivalence itself: the comparison functor 𝓕 ↦ F_{𝓕, A} from adequate 𝒪-modules on (Sch/Spec A)_τ to adequate module-valued functors on the A-algebras of the site is an equivalence of categories, with no hypothesis, at the value universe u of the site. The functor is Stacks.Adequate.adequateComparison, which carries the tag for the functor alone; full faithfulness and essential surjectivity are Stacks.Adequate.fullyFaithful_of_affineSectionsFunctor and Stacks.Adequate.essSurj_of_affineSectionsFunctor, the latter being the quasi-inverse the source builds from an exact sequence 0 → F → M̲ → N̲”.

[Stacks, Tag 06ZJ]. For S = Spec A affine, the comparison functor 𝓕 ↦ F_{𝓕, A} from the category Adeq(𝒪) of adequate 𝒪-modules on (Sch/S)_τ to the category of adequate module-valued functors on the A-algebras of the site is an equivalence of categories. So the two categories are equivalent, by the source's own comparison.

Full faithfulness is full faithfulness of the affine-section functor over an affine base and essential surjectivity is the quasi-inverse Stacks.Adequate.exists_isAdequate_affineSectionsFunctor_iso, which builds the adequate 𝒪-module from an exact sequence 0 → F → M̲ → N̲ as Ker(M^a → N^a); both are packaged in Stacks.Adequate.isEquivalence_of_affineSectionsFunctor, and Stacks.Adequate.adequateComparison_ι is the identification that theorem asks for.

public theorem isEquivalence_adequateComparison {τ : CoveringTopology} {A : CommRingCat.{u}}
    (B : BigSite τ (Spec A)) : (adequateComparison.{u, u} B).IsEquivalence
Tag 06VJ, a lemma

Tag 06VJ in the Stacks Project.

Stacks.Adequate.isAdequate_pullbackSheafOfAmbient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/Pullback.lean, line 393. The attribute's comment: “the pullback of an adequate 𝒪-module along a morphism of schemes is adequate, for the two sites the localizations of one ambient big site, as they are in the source”.

[Stacks, Tag 06VJ]: the pullback f^*𝓕 of an adequate 𝒪-module 𝓕 on (Sch/S)_τ is an adequate 𝒪-module on (Sch/T)_τ, where (Sch/S)_τ and (Sch/T)_τ are the localizations at S and at T of one ambient big τ-site, as they are in the source.

The pullback is the restriction of 𝓕 along the index functor, which is a sheaf by isSheaf_pullbackVal; its affine-section functor at an affine Spec A over T is the affine-section functor of 𝓕 at Spec A over S by affineSectionFunctor_pullbackSheaf, which [Stacks, Tag 06VI] shows to be adequate; and adequacy of f^*𝓕 follows because the affine open cover of T is a τ-covering by affine schemes of the site.

By BigSite.exists_eq_ofAmbient every chosen big site is a localization of an ambient big site, so no generality is lost in stating the lemma this way.

Nothing is assumed beyond adequacy of 𝓕: Tag 06VI is itself unconditional, so the appeal to it in the source's proof carries no hypothesis here either. See the module documentation.

public theorem isAdequate_pullbackSheafOfAmbient (f : T ⟶ S)
    (F : SheafOfModules.{max u m} (BigSite.ofAmbient 𝒮 S hS).structureSheaf)
    (hF : IsAdequate (BigSite.ofAmbient 𝒮 S hS) F) :
    IsAdequate (BigSite.ofAmbient 𝒮 T hT) (pullbackSheafOfAmbient 𝒮 hS hT f F)
Tag 06VK, a lemma

Tag 06VK in the Stacks Project.

Stacks.Adequate.isAdequate_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/CharacterizationsTFAE.lean, line 86. The attribute's comment: “the whole tag as one statement: all five conditions on an 𝒪-module on the big τ-site over a scheme are equivalent, listed in the source's order and with no hypotheses”.

[Stacks, Tag 06VK]. For an 𝒪-module 𝓕 on the big τ-site over a scheme S the following five conditions are equivalent, in the source's order:

  1. 𝓕 is adequate;
  2. there is an affine open covering S = ⋃ Sᵢ and, for each i, a map 𝓖ᵢ ⟶ 𝓗ᵢ of quasi-coherent 𝒪_{Sᵢ}-modules presenting 𝓕|_(Sch/Sᵢ)_τ as the kernel of 𝓖ᵢᵃ ⟶ 𝓗ᵢᵃ;
  3. the same over a τ-covering {Sᵢ → S} of S rather than an affine open covering;
  4. there is a τ-covering {fᵢ : Sᵢ → S} of S with every pullback fᵢ^*𝓕 adequate;
  5. for every affine scheme Spec A of the site over S the restriction 𝓕|_(Sch/Spec A)_τ is the kernel of a map 𝓖ᵃ ⟶ 𝓗ᵃ of associated modules of quasi-coherent 𝒪_{Spec A}-modules.

The statement is unconditional: each of the four equivalences with condition (1) holds with no hypotheses, and tfae_finish assembles the remaining edges.

public theorem isAdequate_tfae (F : SheafOfModules.{u} B.structureSheaf) :
    [IsAdequate B F,
      HasAffineOpenAssociatedKernelCover B F,
      HasCoveringAssociatedKernel B F,
      HasAdequatePullbackCover B F,
      HasAssociatedKernelOnEveryAffine B F].TFAE
Tag 06VL, a lemma

Tag 06VL in the Stacks Project.

Stacks.Adequate.cechExact_and_isSheaf_of_isAdequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AdequateCechExactnessAndSheafConditions.lean, line 129. The attribute's comment: “the whole statement: for an adequate 𝒪-module on a chosen big τ-site over S, the extended Čech complex 0 → F(Spec A) → F(Spec B) → F(Spec (B ⊗_A B)) → ⋯ of every surjective flat morphism of affines of the site is exact at every spot -- at the two left-hand spots as the sheaf condition for the one-member presieve, at the rest as the vanishing of the Čech cohomology in positive degrees -- and the two in particular conclusions, the fpqc sheaf condition and being a sheaf of 𝒪-modules for the fppf coverings, the latter both as the sheaf axiom for the fppf topology and as a term of the category of 𝒪-modules on (Sch/S)_fppf.”.

[Stacks, Tag 06VL], the whole statement.

Let F be an adequate 𝒪-module on a chosen big τ-site over S. Then:

  1. for every surjective flat morphism f : Spec B ⟶ Spec A between affine objects of the site, the extended Čech complex 0 → F(Spec A) → F(Spec B) → F(Spec (B ⊗_A B)) → ⋯ is exact — at its two left-hand spots, which is the sheaf condition for the one-member presieve {f}, and at every remaining spot, which is the vanishing of the Čech cohomology of {f} in every positive degree;
  2. F satisfies the sheaf condition for the fpqc covering families of the site; and
  3. F is a sheaf of 𝒪-modules for the fppf covering families of the site, that is, its underlying presheaf of abelian groups satisfies the fppf sheaf condition; and
  4. equivalently, read as a statement about the object rather than about the sheaf axiom, there is a sheaf of 𝒪-modules on (Sch/S)_fppf — a term of CategoryTheory.SheafOfModules over Stacks.Adequate.BigSite.fppfStructureSheaf, the structure sheaf of rings of the site read at the fppf topology by [Stacks, Tag 03OJ] — whose underlying presheaf of 𝒪-modules is that of F.

Clause (1) is the body of the tag and clauses (2) and (3) are its two "in particular"s, clause (4) being clause (3) repackaged.

public theorem cechExact_and_isSheaf_of_isAdequate
    {τ : CoveringTopology} {S : Scheme.{u}}
    (B : BigSite τ S) (F : SheafOfModules.{max u m} B.structureSheaf)
    (hF : IsAdequate B F) :
    letI : HasFiniteLimits B.category := B.hasFiniteLimits_category
    (∀ (X Y : B.category) (f : Y ⟶ X), X ∈ B.affineObjects → Y ∈ B.affineObjects →
        Flat (B.toOver.map f).left → Surjective (B.toOver.map f).left →
          Presieve.IsSheafFor (F.val.presheaf ⋙ forget AddCommGrpCat.{max u m})
              (Presieve.singleton f) ∧
            ∀ n : ℕ, 0 < n →
              IsZero (Stacks.CechSite.cechCohomology (PreZeroHypercover.singleton.{0} f)
                F.val.presheaf n)) ∧
      Presheaf.IsSheaf (fpqcPrecoverageOn B).toGrothendieck F.val.presheaf ∧
      Presheaf.IsSheaf (fppfPrecoverageOn B).toGrothendieck F.val.presheaf ∧
      ∃ G : SheafOfModules.{max u m} B.fppfStructureSheaf, G.val = F.val
Tag 07AH, a definition

Tag 07AH in the Stacks Project.

Stacks.Adequate.adequate, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/AdequateSheafOfModules.lean, line 329.

The category Adeq(𝒪) of adequate 𝒪-modules on the selected big site: the strictly full subcategory of the sheaves of modules on the site cut out by adequacy.

public abbrev adequate
    {τ : CoveringTopology} {S : Scheme.{u}} (B : BigSite τ S) :
    ObjectProperty (SheafOfModules.{m} B.structureSheaf)
Tag 06VM, a lemma

Tag 06VM in the Stacks Project.

Stacks.Adequate.BigSite.isZero_rightDerived_sections_of_isAdequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AffineCohomologyVanishingUnconditional.lean, line 141. The attribute's comment: “(3): for an adequate 𝒪-module F on (Sch/S)_τ and every affine scheme U over S, H^q(U, F) = 0 for all q > 0; cohomology is the right derived functor of sections over U of the abelian sheaf underlying F”.

[Stacks, Tag 06VM] (3). Let 𝓕 be an adequate 𝒪-module on a chosen big τ-site (Sch/S)_τ over a scheme S. For every affine scheme U over S belonging to the site, H^q(U, 𝓕) = 0 for all q > 0, where H^q(U, −) is the q-th right derived functor of sections over U on abelian sheaves on the site, applied to the abelian sheaf underlying 𝓕.

This is [Stacks, Tag 03F9] at the collection of affine objects of the site and the collection of finite affine τ-coverings of those objects: the objects occurring in such a covering are affine by Stacks.Adequate.BigSite.isAffine_product_of_mem_affineCov, the coverings are cofinal by Stacks.Adequate.BigSite.affineCovCofinal, and the Čech cohomology of an adequate module vanishes on them by Stacks.Adequate.BigSite.cechCohomology_isZero_of_isAdequate.

public theorem BigSite.isZero_rightDerived_sections_of_isAdequate (B : BigSite τ S)
    (F : SheafOfModules.{max u m} B.structureSheaf) (hF : IsAdequate B F)
    (U : B.category) [IsAffine U.left.obj] (q : ℕ) (hq : 0 < q) :
    IsZero ((((sheafSections B.topology AddCommGrpCat.{max u m}).obj (op U)).rightDerived q).obj
      ((SheafOfModules.toSheaf B.structureSheaf).obj F))

Stacks.Adequate.BigSite.adequateCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/CohomologyComparison.lean, line 421. The attribute's comment: “(4): for an adequate 𝒪-module F on (Sch/S)_τ, the canonical isomorphism H^q(S, F|_{S_Zar}) = H^q((Sch/S)_τ, F) in every degree q, cohomology being the right derived functor of global sections”.

[Stacks, Tag 06VM] (4). For an adequate 𝒪-module 𝓕 on a chosen big τ-site (Sch/S)_τ over a scheme S, the canonical isomorphism

H^q(S, 𝓕|_{S_Zar}) ≅ H^q((Sch/S)_τ, 𝓕)

in every degree q, where 𝓕|_{S_Zar} is Stacks.Adequate.BigSite.zariskiRestrictModule and cohomology is the right derived functor of global sections of the underlying abelian sheaves. It is the Grothendieck edge isomorphism of the composite Γ(S_Zar, −) ∘ (−)|_{S_Zar} = Γ, the higher direct images of 𝓕 vanishing by Stacks.Adequate.BigSite.higherZariskiRestrictionVanishing.

public noncomputable def BigSite.adequateCohomologyIso (F : SheafOfModules.{u} B.structureSheaf)
    (hF : IsAdequate B F) (q : ℕ) :
    ((zariskiGlobalSections S).rightDerived q).obj
        ((SheafOfModules.toSheaf S.ringCatSheaf).obj (B.zariskiRestrictModule.obj F)) ≅
      (B.globalSections.rightDerived q).obj ((SheafOfModules.toSheaf B.structureSheaf).obj F)

Stacks.Adequate.BigSite.isIso_etaleRestrictionComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/EtaleRestriction.lean, line 191. The attribute's comment: “(2), for the small étale site of any big étale site whose schemes are schemes of (Sch/S)_τ: the restriction F|_{S_étale} of an adequate 𝒪-module F is the quasi-coherent module associated to F|_{S_Zar}, the canonical map (F|_{S_Zar})^a → F|_{S_étale} being an isomorphism”.

[Stacks, Tag 06VM] (2). Let 𝓕 be an adequate 𝒪-module on a chosen big τ-site (Sch/S)_τ over a scheme S. The restriction 𝓕|_{S_étale} of 𝓕 to the small étale site of S is the quasi-coherent module associated to 𝓕|_{S_Zar}: the canonical comparison (𝓕|_{S_Zar})^a ⟶ 𝓕|_{S_étale} is an isomorphism.

public theorem BigSite.isIso_etaleRestrictionComparison
    (F : SheafOfModules.{u} B.structureSheaf) (hF : IsAdequate B F) :
    IsIso (B.etaleRestrictionComparison E hSE hle F hF)

Stacks.Adequate.BigSite.isIso_etaleSiteRestrictionComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/EtaleRestriction.lean, line 247. The attribute's comment: “(2): for an adequate 𝒪-module F on (Sch/S)_τ the restriction F|_{S_étale} to the small étale site of S is the quasi-coherent module associated to F|_{S_Zar}, the canonical map (F|_{S_Zar})^a → F|_{S_étale} being an isomorphism”.

[Stacks, Tag 06VM] (2) for the small étale site S_étale of (Sch/S)_τ itself. Let 𝓕 be an adequate 𝒪-module on a chosen big τ-site (Sch/S)_τ, for any of the five topologies, and let S_étale be the small étale site of S in the same category of schemes, Stacks.Adequate.BigSite.etaleSite. The restriction 𝓕|_{S_étale} is the quasi-coherent module associated to 𝓕|_{S_Zar}: the canonical comparison (𝓕|_{S_Zar})^a ⟶ 𝓕|_{S_étale} is an isomorphism.

public theorem BigSite.isIso_etaleSiteRestrictionComparison
    (F : SheafOfModules.{u} B.structureSheaf) (hF : IsAdequate B F) :
    IsIso (B.etaleRestrictionComparison B.etaleSite B.contains_etaleSite B.etaleSite_cutoff.le
      F hF)

Stacks.Adequate.BigSite.isQuasicoherent_zariskiRestrictModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/ZariskiRestriction.lean, line 61. The attribute's comment: “(1): for an adequate 𝒪-module F on (Sch/S)_τ the restriction F|_{S_Zar} is a quasi-coherent 𝒪_S-module on the scheme S”.

[Stacks, Tag 06VM] (1). Let 𝓕 be an adequate 𝒪-module on a chosen big τ-site (Sch/S)_τ over a scheme S. The restriction 𝓕|_{S_Zar} of 𝓕 to the small Zariski site of S is a quasi-coherent 𝒪_S-module on the scheme S.

The sections of 𝓕|_{S_Zar} over the basic open D(a) of an affine open U are the base change of the sections over U along 𝒪(U) → 𝒪(D(a)), by Stacks.Adequate.BigSite.affineOpenBaseChange, hence their localization away from a.

public theorem BigSite.isQuasicoherent_zariskiRestrictModule (B : BigSite τ S)
    (F : SheafOfModules.{u} B.structureSheaf) (hF : IsAdequate B F) :
    (B.zariskiRestrictModule.obj F).IsQuasicoherent
Tag 06VN, a remark

Tag 06VN in the Stacks Project.

Stacks.Adequate.BigSite.nonempty_associatedModuleFunctor_obj_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AssociatedModuleAdjunction.lean, line 188. The attribute's comment: “F^a is the pullback of F under the morphism of ringed topoi ((Sch/S)_τ, 𝒪) → (S_Zar, 𝒪_S) whose pushforward is restriction to S_Zar”.

The pullback of a quasi-coherent 𝒪_S-module is its associated module 𝓕^a of [Stacks, Tag 03DU], whose sections over T/S are the global sections of the pullback of 𝓕 to T. This is the description of 𝓕^a as a pullback in Descent, [Stacks, Tag 03FH], which [Stacks, Tag 06VN] invokes. After Stacks.Adequate.BigSite.exists_baseOverTopology substitutes the topology it is AlgebraicGeometry.BigFppfOver.baseAssociatedModuleIsoSectionsSheaf.

public theorem BigSite.nonempty_associatedModuleFunctor_obj_iso (B : BigSite τ S)
    (F : S.Modules) [F.IsQuasicoherent] :
    Nonempty (B.associatedModuleFunctor.obj F ≅
      B.associatedModule F (isSheaf_associatedPresheaf B F))

Stacks.Adequate.BigSite.associatedModuleAdeq, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AssociatedModuleAdjunction.lean, line 304. The attribute's comment: “the functor u : QCoh(𝒪_S) ⥤ Adeq(𝒪), F ↦ F^a”.

[Stacks, Tag 06VN], the functor u. The associated-module functor u : QCoh(𝒪_S) ⥤ Adeq(𝒪), 𝓕 ↦ 𝓕^a, on a chosen big τ-site over S; it lands in the adequate modules by [Stacks, Tag 06VK].

public noncomputable abbrev BigSite.associatedModuleAdeq (B : BigSite τ S) :
    (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory ⥤
      (adequate.{u, u} B).FullSubcategory

Stacks.Adequate.BigSite.restrictModuleQCoh, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AssociatedModuleAdjunction.lean, line 313. The attribute's comment: “the functor v : Adeq(𝒪) ⥤ QCoh(𝒪_S), G ↦ G|_{S_Zar}”.

[Stacks, Tag 06VN], the functor v. Restriction to the small Zariski site of S as a functor v : Adeq(𝒪) ⥤ QCoh(𝒪_S), 𝓖 ↦ 𝓖|_{S_Zar}, on a chosen big τ-site over S; it lands in the quasi-coherent modules by [Stacks, Tag 06VM] (1).

public noncomputable abbrev BigSite.restrictModuleQCoh (B : BigSite τ S) :
    (adequate.{u, u} B).FullSubcategory ⥤
      (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory

Stacks.Adequate.BigSite.adeqAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AssociatedModuleAdjunction.lean, line 356. The attribute's comment: “the adjunction u ⊣ v between QCoh(𝒪_S) and Adeq(𝒪), whose hom-set bijection is Hom_{𝒪_S}(F, vG) = Hom_𝒪(uF, G)”.

[Stacks, Tag 06VN], the adjunction. On a chosen big τ-site over S, for each of the five topologies, the associated-module functor u : QCoh(𝒪_S) ⥤ Adeq(𝒪) is left adjoint to restriction v : Adeq(𝒪) ⥤ QCoh(𝒪_S), so Hom_{𝒪_S}(𝓕, v𝓖) = Hom_𝒪(u𝓕, 𝓖) (Stacks.Adequate.BigSite.adeqAdjunction.homEquiv). It is the pullback–pushforward adjunction of the morphism of ringed sites ((Sch/S)_τ, 𝒪) → (S_Zar, 𝒪_S), restricted to the two full subcategories.

public noncomputable def BigSite.adeqAdjunction (B : BigSite τ S) :
    B.associatedModuleAdeq ⊣ B.restrictModuleQCoh

Stacks.Adequate.BigSite.isIso_adeqAdjunction_unit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AssociatedModuleAdjunction.lean, line 366. The attribute's comment: “the map F → vuF is an isomorphism for every F in QCoh(𝒪_S)”.

[Stacks, Tag 06VN], the unit. The unit 𝓕 → vu𝓕 of the adjunction between QCoh(𝒪_S) and Adeq(𝒪) is an isomorphism at every quasi-coherent 𝒪_S-module, on a chosen big τ-site over S for each of the five topologies.

public theorem BigSite.isIso_adeqAdjunction_unit_app (B : BigSite τ S)
    (M : (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory) :
    IsIso (B.adeqAdjunction.unit.app M)

Stacks.Adequate.BigSite.fullyFaithfulAssociatedModuleAdeq, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AssociatedModuleAdjunction.lean, line 389. The attribute's comment: “consequence of F → vuF being an isomorphism: u : QCoh(𝒪_S) ⥤ Adeq(𝒪) is fully faithful”.

[Stacks, Tag 06VN], consequence of the unit. u : QCoh(𝒪_S) ⥤ Adeq(𝒪) is fully faithful, on a chosen big τ-site over S for each of the five topologies: the unit 𝓕 → vu𝓕 of the adjunction u ⊣ v is an isomorphism at every object of QCoh(𝒪_S) (Stacks.Adequate.BigSite.isIso_adeqAdjunction_unit_app).

public noncomputable def BigSite.fullyFaithfulAssociatedModuleAdeq (B : BigSite τ S) :
    B.associatedModuleAdeq.FullyFaithful
Tag 06VP, a lemma

Tag 06VP in the Stacks Project.

Stacks.Adequate.isAdequate_sheafification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/Sheafification.lean, line 216. The attribute's comment: “assuming AffineAdequateSheafTopology.{u, m}, which is a theorem for m = u (Stacks.Adequate.affineAdequateSheafTopology) and open for a general m”.

[Stacks, Tag 06VP]: let F be a presheaf of O-modules on the big τ-site over S. If for every affine scheme Spec A over S belonging to the site the functor F_{F, A} is adequate, then the sheafification of F is an adequate O-module.

The sheafification enters as a locally injective and locally surjective map η : F ⟶ G.val to a sheaf of modules G, and the conclusion is adequacy of G. The hypothesis htop is the input of the source's proof; it is a theorem at m = u, Stacks.Adequate.affineAdequateSheafTopology, and open for a general m, and it is kept as a hypothesis here because the statement ranges over sheaves of modules of value universe max u m; see the module documentation.

public theorem isAdequate_sheafification
    {τ : CoveringTopology} {S : Scheme.{u}} (B : BigSite τ S)
    (htop : AffineAdequateSheafTopology.{u, m} B)
    (F : PresheafOfModules.{max u m} B.structureSheaf.obj)
    (G : SheafOfModules.{max u m} B.structureSheaf) (η : F ⟶ G.val)
    (hinj : PresheafOfModules.IsLocallyInjective B.topology η)
    (hsurj : PresheafOfModules.IsLocallySurjective B.topology η)
    (hF : ∀ (A : CommRingCat.{u}) (f : Spec A ⟶ S),
      schemeSizeBelow B.cutoff (Spec A) →
        AdequateFunctor.IsAdequate
          (AdequateFunctor.siteAlgebraInclusion A (schemeSizeBelow B.cutoff))
          (presheafAffineSectionFunctor B F A f)) :
    IsAdequate B G

Stacks.Adequate.isAdequate_sheafification', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/SheafificationTopology.lean, line 343.

[Stacks, Tag 06VP]. Let S be a scheme and let F be a presheaf of O-modules on the big τ-site over S. If for every affine scheme Spec A over S belonging to the site the functor F_{F, A} is adequate, then the sheafification of F is an adequate O-module.

The sheafification enters, as in Stacks.Adequate.isAdequate_sheafification, as a locally injective and locally surjective map η : F ⟶ G.val to a sheaf of modules G, which is the universal property of the associated sheaf; the conclusion is adequacy of G.

Nothing is assumed beyond the source's own hypothesis: the input of the source's proof that was named Stacks.Adequate.AffineAdequateSheafTopology is discharged by Stacks.Adequate.affineAdequateSheafTopology_of_moduleExtensionSheaf applied to Stacks.Adequate.affineModuleExtensionSheaf, which is the proof of Stacks.Adequate.affineAdequateSheafTopology and is spelled out here because that declaration lives in a file importing this one. The attribute sits here rather than on Stacks.Adequate.isAdequate_sheafification, which is this statement under that input as an assumption and which the proof of this one calls.

public theorem isAdequate_sheafification'
    {τ' : CoveringTopology} {S' : Scheme.{u}} (B' : BigSite τ' S')
    (F : PresheafOfModules.{max u m} B'.structureSheaf.obj)
    (G : SheafOfModules.{max u m} B'.structureSheaf) (η : F ⟶ G.val)
    (hinj : PresheafOfModules.IsLocallyInjective B'.topology η)
    (hsurj : PresheafOfModules.IsLocallySurjective B'.topology η)
    (hF : ∀ (A : CommRingCat.{u}) (f : Spec A ⟶ S'),
      schemeSizeBelow B'.cutoff (Spec A) →
        AdequateFunctor.IsAdequate
          (AdequateFunctor.siteAlgebraInclusion A (schemeSizeBelow B'.cutoff))
          (presheafAffineSectionFunctor B' F A f)) :
    IsAdequate B' G
Tag 06VQ, a lemma

Tag 06VQ in the Stacks Project.

Stacks.Adequate.isAdequate_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/Abelian.lean, line 197. The attribute's comment: “(3)”.

[Stacks, Tag 06VQ] (3). Let 0 → 𝓕₁ → 𝓕₂ → 𝓕₃ → 0 be a short exact sequence of 𝒪-modules on the chosen big τ-site over S. If 𝓕₁ and 𝓕₃ are adequate, then 𝓕₂ is adequate.

As in the source: over every affine scheme Spec A of the site the induced sequence of affine-section functors is short exact, because H¹ of the adequate 𝓕₁ vanishes on affines ([Stacks, Tag 06VM] (3), through Stacks.Adequate.shortExact_affineSections_of_isAdequate); its outer terms are adequate ([Stacks, Tag 06VI]), so its middle term is adequate ([Stacks, Tag 06V8] on the algebras of the site, Stacks.Adequate.affineAdequateExtensions). The values of the modules lie in the universe of the site.

public theorem isAdequate_of_shortExact
    (T : ShortComplex (SheafOfModules.{u} B.structureSheaf)) (hT : T.ShortExact)
    (h₁ : IsAdequate B T.X₁) (h₃ : IsAdequate B T.X₃) :
    IsAdequate B T.X₂

Stacks.Adequate.abelian_adequate, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AbelianUnconditional.lean, line 125. The attribute's comment: “(1)”.

[Stacks, Tag 06VQ] (1). The adequate 𝒪-modules on the chosen big τ-site over S form an abelian category: they contain the zero sheaf and are closed under kernels, cokernels and finite products inside the abelian category of all sheaves of modules on the site.

public noncomputable def abelian_adequate : Abelian (adequate.{u, u} B).FullSubcategory

Stacks.Adequate.exact_ι_adequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AbelianUnconditional.lean, line 141. The attribute's comment: “(2)”.

[Stacks, Tag 06VQ] (2). The inclusion of the adequate 𝒪-modules into all 𝒪-modules on the chosen big τ-site over S is exact: it preserves finite limits and finite colimits, kernels and cokernels of adequate modules being adequate.

public theorem exact_ι_adequate :
    PreservesFiniteLimits (adequate.{u, u} B).ι ∧ PreservesFiniteColimits (adequate.{u, u} B).ι

Stacks.Adequate.hasColimits_adequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AbelianUnconditional.lean, line 167. The attribute's comment: “(4)”.

[Stacks, Tag 06VQ] (4). The category of adequate 𝒪-modules on the chosen big τ-site over S has all small colimits, and the inclusion into all 𝒪-modules preserves them: a colimit of adequate modules formed in all 𝒪-modules is adequate.

public theorem hasColimits_adequate :
    HasColimitsOfSize.{u, u} (adequate.{u, u} B).FullSubcategory ∧
      PreservesColimitsOfSize.{u, u} (adequate.{u, u} B).ι
Tag 06VR, a lemma

Tag 06VR in the Stacks Project.

Stacks.Adequate.isAdequate_directImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DirectImageAdequacy.lean, line 681. The attribute's comment: “f_*𝓕 is adequate”.

[Stacks, Tag 06VR] for the direct image. Let f : T ⟶ S be a quasi-compact and quasi-separated morphism of schemes and let 𝓕 be an adequate 𝒪-module on a chosen big τ-site over T. Then the direct image f_*𝓕 is an adequate 𝒪-module on a chosen big τ-site over S.

The direct image is restriction along the base-change functor Φ of the two sites, with the scalars transported along the first projection ν of the fibre squares (Stacks.Adequate.directImage); hbc says that Φ and ν are base change along f. Over an affine Spec A of the site over S the affine sections of f_*𝓕 are B ↦ 𝓕(T ×_S Spec B), the degree-zero case of Stacks.Adequate.isAdequate_rightDerived_sectionsAlong_baseChangeFamily.

public theorem isAdequate_directImage
    (F : SheafOfModules.{u} C.structureSheaf) (hF : IsAdequate C F)
    (hqc : QuasiCompact f) (hqs : QuasiSeparated f) (hbc : IsBaseChangeAlong B C f Φ ν) :
    IsAdequate B ((directImage.{u, u} B C Φ ν).obj F)

Stacks.Adequate.isAdequate_higherDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DirectImageAdequacy.lean, line 742. The attribute's comment: “R^i f_*𝓕 is adequate for every i”.

[Stacks, Tag 06VR] for the higher direct images. Let f : T ⟶ S be a quasi-compact and quasi-separated morphism of schemes and let 𝓕 be an adequate 𝒪-module on a chosen big τ-site over T. Then every higher direct image R^i f_*𝓕 is an adequate 𝒪-module on a chosen big τ-site over S.

R^i f_* is the i-th right derived functor of Stacks.Adequate.directImage, the source's definition. It is the sheafification of the presheaf V ↦ H^i(V ×_S T, 𝓕) (Stacks.Adequate.higherDirectImageIsoSheafification), whose affine sections over Spec A are B ↦ H^i(T ×_S Spec B, 𝓕) because evaluation is exact; these are adequate by Stacks.Adequate.isAdequate_rightDerived_sectionsAlong_baseChangeFamily, so the sheafification is adequate by [Stacks, Tag 06VP].

The statement assumes nothing beyond the source. The typeclass arguments of Stacks.Adequate.higherDirectImage are supplied by proved instances on the two sites: the sheafification of abelian presheaves and the identification of its weak equivalences with the locally bijective maps are Stacks.Adequate.BigSite.hasSheafify_addCommGrpCat and Stacks.Adequate.BigSite.wEqualsLocallyBijective_addCommGrpCat, and the injectives in the category of sheaves of modules on the site over T are Stacks.Adequate.BigSite.enoughInjectives_sheafOfModules, which is [Stacks, Tag 01DU] on that site (sheaves of modules on it form a Grothendieck abelian category).

public theorem isAdequate_higherDirectImage
    (F : SheafOfModules.{u} C.structureSheaf) (hF : IsAdequate C F)
    (hqc : QuasiCompact f) (hqs : QuasiSeparated f) (hbc : IsBaseChangeAlong B C f Φ ν)
    (i : ℕ) :
    IsAdequate B ((higherDirectImage.{u, u} B C Φ ν i).obj F)
Sources
LeanStacks.Adequate.IsAdequate · Stacks.Adequate.isAdequate_affineSectionFunctor · Stacks.Adequate.isEquivalence_adequateComparison · Stacks.Adequate.isAdequate_pullbackSheafOfAmbient · Stacks.Adequate.isAdequate_tfae · Stacks.Adequate.cechExact_and_isSheaf_of_isAdequate · Stacks.Adequate.adequate · Stacks.Adequate.BigSite.isZero_rightDerived_sections_of_isAdequate

Section46.6 Parasitic adequate modules#

Section 46.6 of the Stacks Project, Tag 06ZK. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06ZM, a lemma

Tag 06ZM in the Stacks Project.

Stacks.Adequate.tfae_isZero_restrictModule_of_isAdequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/Parasitic.lean, line 475.

[Stacks, Tag 06ZM]. Let 𝓕 be an adequate 𝒪-module on a chosen big τ-site over S, for τ any of the five topologies Zar, étale, smooth, syntomic, fppf. The following are equivalent: 1. v𝓕 = 0, for the restriction v𝓕 = 𝓕|_{S_Zar} of 𝓕 to the small Zariski site of S (Stacks.Adequate.BigSite.zariskiRestrictModule, the functor v of [Stacks, Tag 06VN]); 2. 𝓕 is parasitic; 3. 𝓕 is parasitic for the τ-topology; 4. 𝓕(U) = 0 for every open U ⊆ S; 5. there is an affine open covering S = ⋃ Uᵢ such that 𝓕(Uᵢ) = 0 for all i.

(2)–(5) are Stacks.Adequate.tfae_isParasitic_of_isAdequate; (1) ⇔ (4) is the identification of the sections of v𝓕 over U with those of 𝓕 over U as an object of the site.

public theorem tfae_isZero_restrictModule_of_isAdequate (B : BigSite τ S)
    (F : SheafOfModules.{u} B.structureSheaf) (hF : IsAdequate B F) :
    List.TFAE
      [IsZero (B.zariskiRestrictModule.obj F),
        IsParasitic S B.toOver F.val,
        IsParasiticFor.{u, w} S B.toOver (isTauCovering.{u, w} B) F.val,
        ∀ U : S.Opens, Subsingleton (F.val.obj (op (B.opensToBig.obj U))),
        ∃ (I : Type u) (U : I → S.Opens), (∀ i, IsAffineOpen (U i)) ∧ (⨆ i, U i) = ⊤ ∧
          ∀ i, Subsingleton (F.val.obj (op (B.opensToBig.obj (U i))))]
Tag 06ZN, a lemma

Tag 06ZN in the Stacks Project.

Stacks.Adequate.BigSite.isSerreClass_parasiticAdequate, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/Parasitic.lean, line 525. The attribute's comment: “the subcategory of parasitic adequate modules is a Serre subcategory”.

[Stacks, Tag 06ZN], the Serre subcategory. The parasitic adequate 𝒪-modules form a Serre subcategory 𝒞 of Adeq(𝒪): it is the kernel of the exact functor v : Adeq(𝒪) ⥤ QCoh(𝒪_S) (Stacks.Adequate.BigSite.parasiticAdequate_eq_kernel, which is [Stacks, Tag 06ZM]), and the kernel of an exact functor is a Serre subcategory ([Stacks, Tag 02MQ]). v is exact by Stacks.Adequate.BigSite.preservesFiniteLimits_restrictModuleQCoh and Stacks.Adequate.BigSite.preservesFiniteColimits_restrictModuleQCoh. The abelian structure on Adeq(𝒪) is [Stacks, Tag 06VQ] (1), Stacks.Adequate.abelian_adequate.

public instance BigSite.isSerreClass_parasiticAdequate : B.parasiticAdequate.IsSerreClass

Stacks.Adequate.BigSite.isLocalization_restrictModuleQCoh, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/Parasitic.lean, line 554. The attribute's comment: “the functor v induces an equivalence Adeq(𝒪)/𝒞 = QCoh(𝒪_S): v is a localization functor for the isomorphisms modulo the Serre subcategory 𝒞”.

[Stacks, Tag 06ZN], the quotient equivalence. The functor v : Adeq(𝒪) ⥤ QCoh(𝒪_S) induces an equivalence Adeq(𝒪)/𝒞 ≌ QCoh(𝒪_S), where 𝒞 is the Serre subcategory of parasitic adequate modules and Adeq(𝒪)/𝒞 is the Serre quotient, the localization of Adeq(𝒪) at the morphisms which are isomorphisms modulo 𝒞 ([Stacks, Tag 02MS]): v is a localization functor for that class of morphisms.

The proof is the source's. v is exact, its kernel is 𝒞, so the morphisms inverted by v are those which are isomorphisms modulo 𝒞; and v has the fully faithful left adjoint u : QCoh(𝒪_S) ⥤ Adeq(𝒪) of [Stacks, Tag 06VN] (Stacks.Adequate.BigSite.adeqAdjunction, the unit 𝓕 → vu𝓕 being an isomorphism), which makes the induced functor v̄ essentially surjective and fully faithful (CategoryTheory.Adjunction.isLocalization').

public instance BigSite.isLocalization_restrictModuleQCoh :
    B.restrictModuleQCoh.IsLocalization B.parasiticAdequate.isoModSerre
Tag 06ZP, a lemma

Tag 06ZP in the Stacks Project.

Stacks.Adequate.isAdequate_and_isParasitic_directImage_ofAmbient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/ParasiticDirectImage.lean, line 367.

[Stacks, Tag 06ZP]. Let f : T ⟶ S be a quasi-compact and quasi-separated morphism of schemes and let 𝓕 be a parasitic adequate 𝒪_T-module on (Sch/T)_τ, for τ any of the five topologies Zar, étale, smooth, syntomic, fppf. Then the pushforward f_*𝓕 and every higher direct image R^i f_*𝓕 are parasitic adequate 𝒪_S-modules on (Sch/S)_τ.

(Sch/S)_τ and (Sch/T)_τ are the localizations at S and at T of one ambient big τ-site 𝒮, as they are in the source (Stacks.Adequate.BigSite.ofAmbient; by Stacks.Adequate.BigSite.exists_eq_ofAmbient every chosen big site is one). f_* is the direct image of [Stacks, Tag 06VR] along the base change V ↦ V ×_S T (Stacks.Adequate.ambientBaseChange) with its first projection, and R^i f_* is its i-th right derived functor; nothing is assumed about either, since Stacks.Adequate.isContinuous_ambientBaseChange and Stacks.Adequate.isBaseChangeAlong_ambientBaseChange supply what Tag 06VR needs. The proof is Stacks.Adequate.isAdequate_and_isParasitic_directImage.

public theorem isAdequate_and_isParasitic_directImage_ofAmbient
    (F : SheafOfModules.{u} (BigSite.ofAmbient 𝒮 T hT).structureSheaf)
    (hF : IsAdequate (BigSite.ofAmbient 𝒮 T hT) F)
    (hpar : IsParasitic T (BigSite.ofAmbient 𝒮 T hT).toOver F.val)
    (hqc : QuasiCompact f) (hqs : QuasiSeparated f) :
    (IsAdequate (BigSite.ofAmbient 𝒮 S hS)
        ((directImage.{u, u} (BigSite.ofAmbient 𝒮 S hS) (BigSite.ofAmbient 𝒮 T hT)
          (ambientBaseChange 𝒮 hS hT f) (ambientBaseChangeFst 𝒮 hS hT f)).obj F) ∧
      IsParasitic S (BigSite.ofAmbient 𝒮 S hS).toOver
        ((directImage.{u, u} (BigSite.ofAmbient 𝒮 S hS) (BigSite.ofAmbient 𝒮 T hT)
          (ambientBaseChange 𝒮 hS hT f) (ambientBaseChangeFst 𝒮 hS hT f)).obj F).val) ∧
      ∀ i : ℕ, IsAdequate (BigSite.ofAmbient 𝒮 S hS)
          ((higherDirectImage.{u, u} (BigSite.ofAmbient 𝒮 S hS) (BigSite.ofAmbient 𝒮 T hT)
            (ambientBaseChange 𝒮 hS hT f) (ambientBaseChangeFst 𝒮 hS hT f) i).obj F) ∧
        IsParasitic S (BigSite.ofAmbient 𝒮 S hS).toOver
          ((higherDirectImage.{u, u} (BigSite.ofAmbient 𝒮 S hS) (BigSite.ofAmbient 𝒮 T hT)
            (ambientBaseChange 𝒮 hS hT f) (ambientBaseChangeFst 𝒮 hS hT f) i).obj F).val
Sources
LeanStacks.Adequate.tfae_isZero_restrictModule_of_isAdequate · Stacks.Adequate.BigSite.isSerreClass_parasiticAdequate · Stacks.Adequate.BigSite.isLocalization_restrictModuleQCoh · Stacks.Adequate.isAdequate_and_isParasitic_directImage_ofAmbient

Section46.7 Derived categories of adequate modules, I#

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

Tag 06ZQ, a lemma

Tag 06ZQ in the Stacks Project.

Stacks.Adequate.BigSite.isLocalization_mapDerivedCategory_restrictModuleQCoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/Parasitic.lean, line 583. The attribute's comment: “the unbounded derived quotient D(Adeq(𝒪))/D_𝒞(Adeq(𝒪)) = D(QCoh(𝒪_S))”.

[Stacks, Tag 06ZQ]. D(Adeq(𝒪))/D_𝒞(Adeq(𝒪)) = D(QCoh(𝒪_S)): the functor D(v) : D(Adeq(𝒪)) ⥤ D(QCoh(𝒪_S)) is a localization functor for the morphisms whose cone has all its cohomology objects in the Serre subcategory 𝒞 of parasitic adequate modules. This is [Stacks, Tag 06XM] applied to v, which realises the Serre quotient by 𝒞 (Stacks.Adequate.BigSite.isLocalization_restrictModuleQCoh, [Stacks, Tag 06ZN]) and has the fully faithful left adjoint u of [Stacks, Tag 06VN].

public theorem BigSite.isLocalization_mapDerivedCategory_restrictModuleQCoh
    [HasDerivedCategory.{w₁} (adequate.{u, u} B).FullSubcategory]
    [HasDerivedCategory.{w₂} (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory] :
    B.restrictModuleQCoh.mapDerivedCategory.IsLocalization
      (ObjectProperty.trW (fun X : DerivedCategory (adequate.{u, u} B).FullSubcategory =>
        ∀ n : ℤ, B.parasiticAdequate
          ((DerivedCategory.homologyFunctor (adequate.{u, u} B).FullSubcategory n).obj X)))

Stacks.Adequate.BigSite.isLocalization_mapDerivedCategoryPlus_restrictModuleQCoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/ParasiticDerivedQuotient.lean, line 80. The attribute's comment: “bounded below version D⁺(Adeq(𝒪))/D⁺_𝒞(Adeq(𝒪)) = D⁺(QCoh(𝒪_S))”.

[Stacks, Tag 06ZQ], bounded below version. D⁺(Adeq(𝒪))/D⁺_𝒞(Adeq(𝒪)) = D⁺(QCoh(𝒪_S)): the functor D⁺(v) : D⁺(Adeq(𝒪)) ⥤ D⁺(QCoh(𝒪_S)) is a localization functor for the morphisms of D⁺(Adeq(𝒪)) whose cone has all its cohomology objects in the Serre subcategory 𝒞 of parasitic adequate modules.

public theorem BigSite.isLocalization_mapDerivedCategoryPlus_restrictModuleQCoh :
    B.restrictModuleQCoh.mapDerivedCategoryPlus.IsLocalization
      ((derivedCategoryB B.parasiticAdequate).inverseImage DerivedCategory.Plus.ι).trW

Stacks.Adequate.BigSite.isLocalization_mapDerivedCategoryMinus_restrictModuleQCoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/ParasiticDerivedQuotient.lean, line 92. The attribute's comment: “bounded above version D⁻(Adeq(𝒪))/D⁻_𝒞(Adeq(𝒪)) = D⁻(QCoh(𝒪_S))”.

[Stacks, Tag 06ZQ], bounded above version. D⁻(Adeq(𝒪))/D⁻_𝒞(Adeq(𝒪)) = D⁻(QCoh(𝒪_S)): the functor D⁻(v) : D⁻(Adeq(𝒪)) ⥤ D⁻(QCoh(𝒪_S)) is a localization functor for the morphisms of D⁻(Adeq(𝒪)) whose cone has all its cohomology objects in the Serre subcategory 𝒞 of parasitic adequate modules.

public theorem BigSite.isLocalization_mapDerivedCategoryMinus_restrictModuleQCoh :
    B.restrictModuleQCoh.mapDerivedCategoryMinus.IsLocalization
      ((derivedCategoryB B.parasiticAdequate).inverseImage DerivedCategory.Minus.ι).trW

Stacks.Adequate.BigSite.isLocalization_mapDerivedCategoryBounded_restrictModuleQCoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/ParasiticDerivedQuotient.lean, line 104. The attribute's comment: “bounded version Dᵇ(Adeq(𝒪))/Dᵇ_𝒞(Adeq(𝒪)) = Dᵇ(QCoh(𝒪_S))”.

[Stacks, Tag 06ZQ], bounded version. Dᵇ(Adeq(𝒪))/Dᵇ_𝒞(Adeq(𝒪)) = Dᵇ(QCoh(𝒪_S)): the functor Dᵇ(v) : Dᵇ(Adeq(𝒪)) ⥤ Dᵇ(QCoh(𝒪_S)) is a localization functor for the morphisms of Dᵇ(Adeq(𝒪)) whose cone has all its cohomology objects in the Serre subcategory 𝒞 of parasitic adequate modules.

public theorem BigSite.isLocalization_mapDerivedCategoryBounded_restrictModuleQCoh :
    B.restrictModuleQCoh.mapDerivedCategoryBounded.IsLocalization
      ((derivedCategoryB B.parasiticAdequate).inverseImage DerivedCategory.Bounded.ι).trW
Tag 06ZR, a lemma

Tag 06ZR in the Stacks Project.

Stacks.Adequate.BigSite.isLocalization_mapHomotopyCategoryPlus_associatedModuleAdeq_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedLocalizationAffineSections.lean, line 565. The attribute's comment: “over an affine base U = Spec A, with no hypothesis: D⁺(Adeq(𝒪)), taken as the source does as the localization of K⁺(Adeq(𝒪)) at the quasi-isomorphisms, is the localization of K⁺(QCoh(𝒪_U)) at the universal quasi-isomorphisms along u. (Sch/U)_fppf is rendered as a chosen big fppf site containing Spec A”.

[Stacks, Tag 06ZR] over an affine base, unconditionally. Over an affine scheme U = Spec A the bounded below derived category D⁺(Adeq(𝒪)) is the localization of K⁺(QCoh(𝒪_U)) at the universal quasi-isomorphisms.

This is BigSite.isLocalization_mapHomotopyCategoryPlus_associatedModuleAdeq_of_allAlgebras with its single hypothesis discharged by Stacks.Adequate.BigSite.universallyAcyclic_eq_inverseImage_qcohAllAlgebraSections.

public theorem BigSite.isLocalization_mapHomotopyCategoryPlus_associatedModuleAdeq_affine :
    (((BigSite.ofBigFppfSite B (Spec A) hS).associatedModuleAdeq).mapHomotopyCategoryPlus ⋙
        MorphismProperty.Q (HomotopyCategory.Plus.quasiIso
          (adequate.{u, u}
            (BigSite.ofBigFppfSite B (Spec A) hS)).FullSubcategory)).IsLocalization
      (universalQuasiIso (Spec A))
Tag 06ZS, a lemma

Tag 06ZS in the Stacks Project.

Stacks.Adequate.exists_adequator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/Adequator.lean, line 220.

[Stacks, Tag 06ZS]. Let U = Spec A be an affine scheme. The inclusion functor Adeq(𝒪) → Mod((Sch/U)_τ, 𝒪) has a right adjoint, and the adjunction mapping A(𝓕) → 𝓕 is an isomorphism for every adequate module 𝓕.

The right adjoint is Stacks.Adequate.affineAdequator, with adjunction Stacks.Adequate.affineAdequatorAdjunction.

public theorem exists_adequator :
    ∃ (R : SheafOfModules.{u} B.structureSheaf ⥤ (adequate.{u, u} B).FullSubcategory)
      (adjR : (adequate.{u, u} B).ι ⊣ R),
      ∀ F : SheafOfModules.{u} B.structureSheaf, IsAdequate B F → IsIso (adjR.counit.app F)
Tag 06ZT, an equation

Tag 06ZT in the Stacks Project.

Stacks.Adequate.adequateComparisonSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/Adequator.lean, line 150. The attribute's comment: “the commutativity of the square, with the comparison functor of Tag 06ZJ as its left vertical arrow; that it is an identification is Stacks.Adequate.isEquivalence_adequateComparison”.

[Stacks, Tag 06ZT], the commutative square in the proof of [Stacks, Tag 06ZS]: the inclusion of Adeq(𝒪) followed by the affine-section functor into the module-valued functors on the A-algebras of the site equals the comparison functor of [Stacks, Tag 06ZJ] followed by the inclusion of the adequate module-valued functors. It commutes by definitional unfolding, which is Stacks.Adequate.adequateComparison_ι.

public noncomputable def adequateComparisonSquare :
    adequateComparison.{u, m} B ⋙ (adequateOn.{u, max u m} A (schemeSizeBelow B.cutoff)).ι ≅
      (adequate.{u, max u m} B).ι ⋙ affineSectionsFunctor.{u, max u m} B A (𝟙 (Spec A))

Stacks.Adequate.adequateDiagramSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AdequatorDiagram.lean, line 96. The attribute's comment: “the commutativity of the diagram, with k, j and the right vertical arrow written out, at an arbitrary module universe”.

[Stacks, Tag 06ZT], the commutativity of the diagram, at an arbitrary module universe: k, then the inclusion j of sheaves into presheaves, then the right vertical arrow, is the left vertical arrow (the comparison functor of [Stacks, Tag 06ZJ]) followed by the inclusion i : 𝒜 → 𝒫. Both sides restrict sections to spectra and scalars along B ≅ 𝒪(Spec B).

public noncomputable def adequateDiagramSquare :
    adequateToAffineModules.{u, m} B ⋙ SheafOfModules.forget _ ⋙
        affinePresheafModulesToModuleValued.{u, m} B ≅
      adequateComparison.{u, m} B ⋙ (adequateOn.{u, max u m} A (schemeSizeBelow B.cutoff)).ι

Stacks.Adequate.adequateAffineDiagram, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AdequatorDiagram.lean, line 128. The attribute's comment: “the whole diagram: both vertical arrows are equivalences, it commutes, k and j are fully faithful, and its middle category is modules on the affine objects of the site”.

[Stacks, Tag 06ZT], the whole diagram. For U = Spec A affine, in the diagram Adeq(𝒪) --k--> Mod((Aff/U)_τ, 𝒪) --j--> PMod((Aff/U)_τ, 𝒪) over 𝒜 --i--> 𝒫:

  • the left vertical arrow Adeq(𝒪) → 𝒜 is an equivalence ([Stacks, Tag 06ZJ]);
  • the right vertical arrow PMod((Aff/U)_τ, 𝒪) → 𝒫 is an equivalence ([Stacks, Section 06US]);
  • the diagram commutes;
  • k and j are fully faithful;
  • the restriction Mod((Sch/U)_τ, 𝒪) → Mod((Aff/U)_τ, 𝒪) through which k factors is an equivalence ([Stacks, Tag 021V]);
  • the affine-spectrum functor from the A-algebras of the site is fully faithful, with essential image exactly the affine objects of the site, so that its source is (Aff/U)_τ.

The commutativity and full-faithfulness conjuncts are wrapped in Nonempty because an isomorphism of functors and a full-faithfulness witness are data while a conjunction needs a proposition; asserting the diagram commutes is asserting such an isomorphism exists.

public theorem adequateAffineDiagram :
    (adequateComparison.{u, u} B).IsEquivalence ∧
      (affinePresheafModulesToModuleValued.{u, u} B).IsEquivalence ∧
      Nonempty (adequateToAffineModules.{u, u} B ⋙ SheafOfModules.forget _ ⋙
          affinePresheafModulesToModuleValued.{u, u} B ≅
        adequateComparison.{u, u} B ⋙ (adequateOn.{u, u} A (schemeSizeBelow B.cutoff)).ι) ∧
      Nonempty (adequateToAffineModules.{u, u} B).FullyFaithful ∧
      Nonempty (SheafOfModules.forget.{u} (DenseSubsiteModules.ringRestriction
        (affineSubsiteTopology B) B.topology (affineSpecOver B A (𝟙 (Spec A)))
        B.structureSheaf)).FullyFaithful ∧
      (SheafOfModules.pushforward.{u} (𝟙 (DenseSubsiteModules.ringRestriction
        (affineSubsiteTopology B) B.topology (affineSpecOver B A (𝟙 (Spec A)))
        B.structureSheaf))).IsEquivalence ∧
      (affineSpecOver B A (𝟙 (Spec A))).Full ∧ (affineSpecOver B A (𝟙 (Spec A))).Faithful ∧
      ∀ X : B.category, IsAffine X.left.obj ↔ (affineSpecOver B A (𝟙 (Spec A))).essImage X

Declarations registered for the tag:

Tag 06ZU, a lemma

Tag 06ZU in the Stacks Project.

Stacks.Adequate.exactAt_mapHomologicalComplex_of_coreflection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AdequatorVanishing.lean, line 177. The attribute's comment: “the homological step of the proof: exactness in positive degrees of a right adjoint applied to an injective resolution, from the Ext vanishing along a separating family; stated for an arbitrary adjunction”.

The homological core of [Stacks, Tag 06ZU]. Let i ⊣ Q be an adjunction with i additive, let G be a fully faithful additive functor preserving injective objects which carries an injective resolution I of X to a resolution of G(X), and let P be a separating family in the domain of i whose objects have no degree-n extensions into G(X). Then Q(I^•) is exact in degree n > 0.

public theorem exactAt_mapHomologicalComplex_of_coreflection [HasExt.{w} E]
    (i : D ⥤ C) (Q : C ⥤ D) [i.Additive] [Q.Additive] (adj : i ⊣ Q)
    (G : C ⥤ E) [G.Additive] [G.Full] [G.Faithful] [G.PreservesInjectiveObjects]
    (P : ObjectProperty D) (hP : P.IsSeparating)
    {X : C} (I : InjectiveResolution X)
    [QuasiIso ((G.mapHomologicalComplex (ComplexShape.up ℕ)).map I.ι)]
    (n : ℕ) (hn : 0 < n)
    (hExt : ∀ L : D, P L → Subsingleton (Abelian.Ext.{w} (G.obj (i.obj L)) (G.obj X) n)) :
    ((Q.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).ExactAt n

Stacks.Adequate.isZero_rightDerived_of_coreflection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AdequatorVanishing.lean, line 234. The attribute's comment: “the same step read as the vanishing of the right derived functors of the right adjoint; stated for an arbitrary adjunction”.

The homological core of [Stacks, Tag 06ZU], read as the vanishing of a right derived functor of the right adjoint: under the hypotheses of Stacks.Adequate.exactAt_mapHomologicalComplex_of_coreflection, R^n Q(X) = 0.

public theorem isZero_rightDerived_of_coreflection [EnoughInjectives C] [HasExt.{w} E]
    (i : D ⥤ C) (Q : C ⥤ D) [i.Additive] [Q.Additive] (adj : i ⊣ Q)
    (G : C ⥤ E) [G.Additive] [G.Full] [G.Faithful] [G.PreservesInjectiveObjects]
    [PreservesFiniteLimits G]
    (P : ObjectProperty D) (hP : P.IsSeparating) (X : C)
    (hacyclic : ∀ k : ℕ, 0 < k → IsZero ((G.rightDerived k).obj X))
    (n : ℕ) (hn : 0 < n)
    (hExt : ∀ L : D, P L → Subsingleton (Abelian.Ext.{w} (G.obj (i.obj L)) (G.obj X) n)) :
    IsZero ((Q.rightDerived n).obj X)

Stacks.Adequate.isZero_rightDerived_adequator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AdequatorVanishing.lean, line 367. The attribute's comment: “the full statement, R^p A(F) = 0 for every p > 0 and every object of Adeq(O), for the named adequator of Tag 06ZS. Assumed: that adequator's own inputs (Q, E, adj from Tags 06Z6 and 06ZJ over the algebras of the site, hj and comm from Tag 06ZT), right acyclicity of the affine-section functor (hacyclic, Tags 06YK and 06VM), the positive-degree Ext vanishing along a separating family (hP and hExt, Tag 06ZI), the three closure properties of Tag 06VQ (1) and EnoughInjectives for the sheaves of modules on the site. Preservation of injective objects by the affine-section functor is proved, through Tag 03FB on the affine subsite”.

[Stacks, Tag 06ZU]. For U = Spec A affine, every object 𝓕 of Adeq(𝒪) and every p > 0, the p-th right derived functor of the adequator of [Stacks, Tag 06ZS] vanishes at 𝓕: the adequator of an injective resolution of 𝓕 is exact in positive degrees.

public theorem isZero_rightDerived_adequator
    (adj : (adequateOn.{u, max u m} A (schemeSizeBelow B.cutoff)).ι ⊣ Q)
    (hj : (affineSectionsFunctor.{u, max u m} B A (𝟙 (Spec A))).FullyFaithful)
    (comm : E.functor ⋙ (adequateOn.{u, max u m} A (schemeSizeBelow B.cutoff)).ι ≅
      (adequate.{u, max u m} B).ι ⋙ affineSectionsFunctor.{u, max u m} B A (𝟙 (Spec A)))
    (F : (adequate.{u, max u m} B).FullSubcategory) (p : ℕ) (hp : 0 < p)
    (hacyclic : AffineSectionsAcyclic.{u, m} B A (𝟙 (Spec A)) F.obj)
    (P : ObjectProperty (adequate.{u, max u m} B).FullSubcategory) (hP : P.IsSeparating)
    (hExt : AffineSectionsExtVanishing.{u, m, w} B P F.obj p) :
    letI : (adequator.{u, max u m} B Q E).Additive := additive_adequator B Q E adj hj comm
    IsZero (((adequator.{u, max u m} B Q E).rightDerived p).obj F.obj)

Stacks.Adequate.isZero_rightDerived_affineAdequator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AdequatorVanishingUnconditional.lean, line 60.

[Stacks, Tag 06ZU]. Let U = Spec A be an affine scheme. For every object 𝓕 of Adeq(𝒪) and every p > 0, R^p A(𝓕) = 0, where A is the adequator Stacks.Adequate.affineAdequator of [Stacks, Tag 06ZS], the right adjoint of the inclusion Adeq(𝒪) → Mod((Sch/U)_τ, 𝒪).

The letI preamble is not a list of hypotheses: it is the abelian structure of Adeq(𝒪) (Tag 06VQ (1)) and the additivity of the adequator, which is a right adjoint of an additive functor.

public theorem isZero_rightDerived_affineAdequator
    (F : (adequate.{u, u} B).FullSubcategory) (p : ℕ) (hp : 0 < p) :
    letI := adequate_isClosedUnderKernels.{u, u} B
    letI := adequate_isClosedUnderCokernels.{u, u} B
    letI := adequate_isClosedUnderFiniteProducts.{u, u} B
    letI : Abelian (adequate.{u, u} B).FullSubcategory := abelian_adequate B
    letI : (affineAdequator B).Additive :=
      (affineAdequatorAdjunction B).right_adjoint_additive
    IsZero (((affineAdequator B).rightDerived p).obj F.obj)
Tag 06ZV, a lemma

Tag 06ZV in the Stacks Project.

Stacks.Adequate.isEquivalence_adequateBoundedBelowComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedCategoryBoundedBelow.lean, line 94. The attribute's comment: “the full statement, that the canonical comparison functor D⁺(Adeq(𝒪)) ⥤ D⁺_Adeq(𝒪) of the equation (46.7.5.1) of Tag 06VV is an equivalence. Assumed: a right adjoint Ψ of the derived inclusion on bounded below objects together with its preservation of boundedness below (adj, hΨ), which is the source's RA, available because the adequator of Tag 06ZS is left exact and Mod(𝒪) has enough injectives; the source's key fact that the adjunction maps are quasi-isomorphisms on the SINGLE modules (hunit, hcounit), which is Tag 06ZU together with the moreover clause of Tag 06ZS; and the closure of adequacy under kernels, cokernels and finite products, Tag 06VQ (1), which makes Adeq(𝒪) abelian. The passage from the key fact on single modules to all of D⁺, which is the source's spectral sequence argument via Tag 015J, is proved”.

[Stacks, Tag 06ZV]. For U = Spec A affine, the canonical comparison functor D⁺(Adeq(𝒪)) ⥤ D⁺_{Adeq}(𝒪) — the inclusion Adeq(𝒪) ⥤ Mod(𝒪) applied degreewise to complexes — is an equivalence.

public theorem isEquivalence_adequateBoundedBelowComparison :
    (DerivedCategoryB.boundedBelowComparison (adequate.{u, m} B)).IsEquivalence

Stacks.Adequate.adequateBoundedBelowEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedCategoryBoundedBelow.lean, line 104. The attribute's comment: “the equivalence as data, D⁺(Adeq(𝒪)) ≌ D⁺_Adeq(𝒪), under the hypotheses of Stacks.Adequate.isEquivalence_adequateBoundedBelowComparison; its functor is the canonical comparison functor by Stacks.Adequate.adequateBoundedBelowEquivalence_functor”.

[Stacks, Tag 06ZV] as an equivalence of categories: D⁺(Adeq(𝒪)) ≌ D⁺_{Adeq}(𝒪) for U = Spec A affine.

public def adequateBoundedBelowEquivalence :
    DerivedCategory.Plus (adequate.{u, m} B).FullSubcategory ≌
      (DerivedCategoryB.derivedCategoryBPlus (adequate.{u, m} B)).FullSubcategory

Stacks.Adequate.isEquivalence_boundedBelowComparison_adequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedCategoryBoundedBelowUnconditional.lean, line 95.

[Stacks, Tag 06ZV]. Let U = Spec A be an affine scheme. The canonical functor D⁺(Adeq(𝒪)) ⥤ D⁺_{Adeq}(𝒪), the inclusion Adeq(𝒪) ⥤ Mod((Sch/U)_τ, 𝒪) applied degreewise to bounded below complexes, is an equivalence onto the bounded below objects of D(𝒪) whose cohomology sheaves are adequate.

public theorem isEquivalence_boundedBelowComparison_adequate
    [HasDerivedCategory.{w} (SheafOfModules.{u} B.structureSheaf)]
    [HasDerivedCategory.{w'} (adequate.{u, u} B).FullSubcategory] :
    (DerivedCategoryB.boundedBelowComparison (adequate.{u, u} B)).IsEquivalence
Tag 06ZW, a lemma

Tag 06ZW in the Stacks Project.

Stacks.Adequate.bijective_mapExtAddHom_ι_adequate_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AdequateExtComparison.lean, line 124. The attribute's comment: “degree 0, where the comparison is the map on Hom and the inclusion of the strictly full subcategory of adequate modules is fully faithful; every degree is bijective_mapExtAddHom_ι_adequate in HigherExtsAdequate/AdequateExtComparisonAll”.

For U = Spec A affine and adequate 𝒪-modules 𝓕, 𝓖, the natural map Ext^0_{Adeq(𝒪)}(𝓕, 𝓖) ⟶ Ext^0_{Mod((Sch/U)_τ, 𝒪)}(𝓕, 𝓖) is bijective.

public theorem bijective_mapExtAddHom_ι_adequate_zero :
    letI := adequate_isClosedUnderKernels.{u, u} B
    letI := adequate_isClosedUnderCokernels.{u, u} B
    letI := adequate_isClosedUnderFiniteProducts.{u, u} B
    letI : Abelian (adequate.{u, u} B).FullSubcategory := abelian_adequate B
    letI : PreservesFiniteLimits (adequate.{u, u} B).ι := (exact_ι_adequate B).1
    letI : PreservesFiniteColimits (adequate.{u, u} B).ι := (exact_ι_adequate B).2
    letI : HasDerivedCategory.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      HasDerivedCategory.standard _
    letI : HasDerivedCategory.{u + 1} (adequate.{u, u} B).FullSubcategory :=
      HasDerivedCategory.standard _
    letI : HasExt.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      hasExt_of_hasDerivedCategory _
    letI : HasExt.{u + 1} (adequate.{u, u} B).FullSubcategory :=
      hasExt_of_hasDerivedCategory _
    ∀ (F G : (adequate.{u, u} B).FullSubcategory),
      Function.Bijective ((adequate.{u, u} B).ι.mapExtAddHom.{u + 1, u + 1} F G 0)

Stacks.Adequate.bijective_mapExtAddHom_ι_adequate_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/AdequateExtComparison.lean, line 157. The attribute's comment: “degree 1, where the comparison is bijective because the adequate modules are closed under extensions, Tag 06VQ (3), and Ext^1 is the group of Yoneda extensions; every degree is bijective_mapExtAddHom_ι_adequate in HigherExtsAdequate/AdequateExtComparisonAll”.

For U = Spec A affine and adequate 𝒪-modules 𝓕, 𝓖, the natural map Ext^1_{Adeq(𝒪)}(𝓕, 𝓖) ⟶ Ext^1_{Mod((Sch/U)_τ, 𝒪)}(𝓕, 𝓖) is bijective.

public theorem bijective_mapExtAddHom_ι_adequate_one :
    letI := adequate_isClosedUnderKernels.{u, u} B
    letI := adequate_isClosedUnderCokernels.{u, u} B
    letI := adequate_isClosedUnderFiniteProducts.{u, u} B
    letI : Abelian (adequate.{u, u} B).FullSubcategory := abelian_adequate B
    letI : PreservesFiniteLimits (adequate.{u, u} B).ι := (exact_ι_adequate B).1
    letI : PreservesFiniteColimits (adequate.{u, u} B).ι := (exact_ι_adequate B).2
    letI : HasDerivedCategory.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      HasDerivedCategory.standard _
    letI : HasDerivedCategory.{u + 1} (adequate.{u, u} B).FullSubcategory :=
      HasDerivedCategory.standard _
    letI : HasExt.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      hasExt_of_hasDerivedCategory _
    letI : HasExt.{u + 1} (adequate.{u, u} B).FullSubcategory :=
      hasExt_of_hasDerivedCategory _
    ∀ (F G : (adequate.{u, u} B).FullSubcategory),
      Function.Bijective ((adequate.{u, u} B).ι.mapExtAddHom.{u + 1, u + 1} F G 1)

Stacks.Adequate.bijective_mapExtAddHom_ι_adequate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/AdequateExtComparisonAll.lean, line 50. The attribute's comment: “every degree i ≥ 0”.

Let U = Spec A be affine and 𝓕, 𝓖 adequate 𝒪-modules. For every i ≥ 0 the natural map Ext^i_{Adeq(𝒪)}(𝓕, 𝓖) ⟶ Ext^i_{Mod(𝒪)}(𝓕, 𝓖), induced by the exact inclusion of the adequate modules, is bijective.

The letI preamble is not a list of hypotheses: it is the abelian structure of Adeq(𝒪) (Tag 06VQ (1)), the exactness of its inclusion (Tag 06VQ (2)) and the standard derived-category and Ext choices, spelled exactly as in bijective_mapExtAddHom_ι_adequate_zero.

public theorem bijective_mapExtAddHom_ι_adequate :
    letI := adequate_isClosedUnderKernels.{u, u} B
    letI := adequate_isClosedUnderCokernels.{u, u} B
    letI := adequate_isClosedUnderFiniteProducts.{u, u} B
    letI : Abelian (adequate.{u, u} B).FullSubcategory := abelian_adequate B
    letI : PreservesFiniteLimits (adequate.{u, u} B).ι := (exact_ι_adequate B).1
    letI : PreservesFiniteColimits (adequate.{u, u} B).ι := (exact_ι_adequate B).2
    letI : HasDerivedCategory.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      HasDerivedCategory.standard _
    letI : HasDerivedCategory.{u + 1} (adequate.{u, u} B).FullSubcategory :=
      HasDerivedCategory.standard _
    letI : HasExt.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      hasExt_of_hasDerivedCategory _
    letI : HasExt.{u + 1} (adequate.{u, u} B).FullSubcategory :=
      hasExt_of_hasDerivedCategory _
    ∀ (F G : (adequate.{u, u} B).FullSubcategory) (n : ℕ),
      Function.Bijective ((adequate.{u, u} B).ι.mapExtAddHom.{u + 1, u + 1} F G n)
Sources
LeanStacks.Adequate.BigSite.isLocalization_mapDerivedCategory_restrictModuleQCoh · Stacks.Adequate.BigSite.isLocalization_mapDerivedCategoryPlus_restrictModuleQCoh · Stacks.Adequate.BigSite.isLocalization_mapDerivedCategoryMinus_restrictModuleQCoh · Stacks.Adequate.BigSite.isLocalization_mapDerivedCategoryBounded_restrictModuleQCoh · Stacks.Adequate.BigSite.isLocalization_mapHomotopyCategoryPlus_associatedModuleAdeq_affine · Stacks.Adequate.exists_adequator · Stacks.Adequate.adequateComparisonSquare · Stacks.Adequate.adequateDiagramSquare

Section46.8 Pure extensions#

Section 46.8 of the Stacks Project, Tag 06ZX. 9 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06ZY, a definition

Tag 06ZY in the Stacks Project.

Module.PureInjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Defs.lean, line 29. The attribute's comment: “pure_injective”.

An A-module I is pure injective if applying Hom_A(-, I) to every universally exact short exact sequence of A-modules gives a short exact sequence.

public abbrev PureInjective (A : Type u) [CommRing A] (I : Type v)
    [AddCommGroup I] [Module A I] : Prop

Module.PureProjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Defs.lean, line 51. The attribute's comment: “pure_projective”.

An A-module P is pure projective if applying Hom_A(P, -) to every universally exact short exact sequence of A-modules gives a short exact sequence.

public abbrev PureProjective (A : Type u) [CommRing A] (P : Type v)
    [AddCommGroup P] [Module A P] : Prop
Tag 06ZZ, a lemma

Tag 06ZZ in the Stacks Project.

Module.pureProjective_iff_directSum_finitelyPresented_retract, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Projective.lean, line 246. The attribute's comment: “pure_projective_characterization”.

An A-module is pure projective if and only if it is a retract of a direct sum of finitely presented A-modules.

public theorem pureProjective_iff_directSum_finitelyPresented_retract
    (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] :
    Module.PureProjective A M ↔
      ∃ (ι : Type (max u v)) (Q : ι → Type (max u v))
        (_ : (i : ι) → AddCommGroup (Q i))
        (_ : (i : ι) → Module A (Q i)),
        (∀ i, Module.FinitePresentation A (Q i)) ∧
          ∃ (s : M →ₗ[A] ⨁ i, Q i) (r : (⨁ i, Q i) →ₗ[A] M),
            r.comp s = LinearMap.id

Module.exists_pureProjective_universallyExact_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Projective.lean, line 296. The attribute's comment: “pure_projective_presentation”.

Every module is the quotient of a pure projective module in a universally exact short exact sequence.

public theorem exists_pureProjective_universallyExact_presentation
    (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] :
    ∃ (N P : Type (max u v))
      (_ : AddCommGroup N) (_ : Module A N)
      (_ : AddCommGroup P) (_ : Module A P)
      (f : N →ₗ[A] P) (g : P →ₗ[A] M),
      Function.Injective f ∧
        Function.Surjective g ∧
          LinearMap.range f = LinearMap.ker g ∧
            UniversallyInjective f ∧
              Module.PureProjective A P
Tag 0700, a lemma

Tag 0700 in the Stacks Project.

Module.characterModule_pureInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Injective.lean, line 76. The attribute's comment: “character_module_pure_injective”.

The character module Hom_ℤ(M, ℚ/ℤ) of any module M over a commutative ring is pure injective.

public theorem characterModule_pureInjective (A : Type u) [CommRing A]
    (M : Type v) [AddCommGroup M] [Module A M] :
    Module.PureInjective A (CharacterModule M)

Module.pureInjective_iff_evalₗ_splits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Injective.lean, line 131. The attribute's comment: “pure_injective_iff_double_dual_splits”.

A module is pure injective if and only if evaluation into its double character module has a linear retraction.

public theorem pureInjective_iff_evalₗ_splits (A : Type u) [CommRing A]
    (I : Type v) [AddCommGroup I] [Module A I] :
    Module.PureInjective A I ↔
      ∃ r : CharacterModule (CharacterModule I) →ₗ[A] I,
        r.comp (CharacterModule.evalₗ A I) = LinearMap.id

Module.exists_pureInjective_universallyExact_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Injective.lean, line 154. The attribute's comment: “exists_pure_injective_universally_exact_extension”.

Every module embeds universally injectively into a pure injective module, with a surjective cokernel map making the resulting sequence exact.

public theorem exists_pureInjective_universallyExact_extension
    (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] :
    ∃ (I N : Type v)
      (_ : AddCommGroup I) (_ : Module A I)
      (_ : AddCommGroup N) (_ : Module A N)
      (f : M →ₗ[A] I) (g : I →ₗ[A] N),
      Function.Injective f ∧
        Function.Surjective g ∧
          LinearMap.range f = LinearMap.ker g ∧
            UniversallyInjective f ∧ Module.PureInjective A I
Tag 0701, a lemma

Tag 0701 in the Stacks Project.

Module.universallyInjective_range_subtype, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Injective.lean, line 201. The attribute's comment: “part (1)”.

If L → M → N is exact and remains exact after every tensor product, then the inclusion of the image of M → N in N is universally injective.

theorem universallyInjective_range_subtype
    {L M N : Type v} [AddCommGroup L] [AddCommGroup M] [AddCommGroup N]
    [Module A L] [Module A M] [Module A N]
    (f : L →ₗ[A] M) (g : M →ₗ[A] N)
    (hexact : Function.Exact f g)
    (h : ∀ (Q : Type v) [AddCommGroup Q] [Module A Q],
      Function.Exact (f.rTensor Q) (g.rTensor Q)) :
    UniversallyInjective (LinearMap.range g).subtype

Module.kernel_universallyExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Injective.lean, line 216. The attribute's comment: “part (2)”.

The kernel-to-term-to-next-kernel sequences of a universally exact complex are universally exact short exact sequences.

theorem kernel_universallyExact
    {M : ℤ → Type u} [∀ i, AddCommGroup (M i)] [∀ i, Module A (M i)]
    (d : ∀ i, M i →ₗ[A] M (i + 1)) (h : UniversallyExactComplex M d) (i : ℤ) :
    UniversallyExact (LinearMap.ker (d i)).subtype (toNextKernel d h i)
Tag 0702, a definition

Tag 0702 in the Stacks Project.

Module.PureInjectiveResolution.IsPureInjectiveResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/InjectiveResolution.lean, line 37. The attribute's comment: “pure_injective_resolution”.

An augmentation M ⟶ I⁰ of a cochain complex is a pure injective resolution if 0 ⟶ M ⟶ I⁰ ⟶ I¹ ⟶ ⋯ is universally exact and every Iⁱ is pure injective.

public structure IsPureInjectiveResolution
    {M : Type v} [AddCommGroup M] [Module A M]
    (I : CochainComplex (ModuleCat.{v} A) ℕ) (augmentation : M →ₗ[A] I.X 0) : Prop

Module.PureProjectiveResolution.IsPureProjectiveResolution, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/ProjectiveResolution.lean, line 38. The attribute's comment: “pure_projective_resolution”.

An augmentation P₀ ⟶ M of a chain complex is a pure projective resolution if ⋯ ⟶ P₁ ⟶ P₀ ⟶ M ⟶ 0 is universally exact and every Pᵢ is pure projective.

public structure IsPureProjectiveResolution
    {M : Type v} [AddCommGroup M] [Module A M]
    (P : ChainComplex (ModuleCat.{w} A) ℕ) (augmentation : P.X 0 →ₗ[A] M) : Prop
Tag 0703, a lemma

Tag 0703 in the Stacks Project.

Module.PureProjectiveResolution.exists_comparison_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/ProjectiveResolution.lean, line 265. The attribute's comment: “comparison_map”.

A module map extends from a pure projective resolution to any universally exact resolution.

public theorem exists_comparison_map
    {M N : Type v} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
    (f : M →ₗ[A] N)
    (P C : ChainComplex (ModuleCat.{v} A) ℕ)
    (aP : P.X 0 →ₗ[A] M) (aC : C.X 0 →ₗ[A] N)
    (hP : Module.PureProjectiveResolution.IsPureProjectiveResolution P aP)
    (hC : IsUniversallyExactResolution C aC) :
    ∃ F : P ⟶ C, aC.comp (F.f 0).hom = f.comp aP

Module.PureProjectiveResolution.homotopy_of_same_augmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/ProjectiveResolution.lean, line 333. The attribute's comment: “homotopy_uniqueness”.

Two maps of resolutions inducing the same map of resolved modules are homotopic.

public theorem homotopy_of_same_augmentation
    {M N : Type v} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
    (P C : ChainComplex (ModuleCat.{v} A) ℕ)
    (augmentationP : P.X 0 →ₗ[A] M) (augmentationC : C.X 0 →ₗ[A] N)
    (hP : Module.PureProjectiveResolution.IsPureProjectiveResolution P augmentationP)
    (hC : Module.PureProjectiveResolution.IsUniversallyExactResolution C augmentationC)
    (f : M →ₗ[A] N) (α β : P ⟶ C)
    (hα : augmentationC.comp (α.f 0).hom = f.comp augmentationP)
    (hβ : augmentationC.comp (β.f 0).hom = f.comp augmentationP) :
    Nonempty (Homotopy α β)

Module.PureProjectiveResolution.exists_isPureProjectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/ResolutionExistence.lean, line 169. The attribute's comment: “existence”.

Every module admits a pure projective resolution.

public theorem exists_isPureProjectiveResolution :
    ∃ (P : ChainComplex (ModuleCat.{max u v} A) ℕ) (augmentation : P.X 0 →ₗ[A] M),
      IsPureProjectiveResolution P augmentation
Tag 0704, a lemma

Tag 0704 in the Stacks Project.

Module.PureInjectiveResolution.exists_comparison_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/InjectiveResolution.lean, line 225. The attribute's comment: “comparison_map”.

A map M → N extends to a map from any universally exact resolution of M to any pure injective resolution of N.

public theorem exists_comparison_map
    {M N : Type v} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
    (f : M →ₗ[A] N)
    (C I : CochainComplex (ModuleCat.{v} A) ℕ)
    (aC : M →ₗ[A] C.X 0) (aI : N →ₗ[A] I.X 0)
    (hC : IsUniversallyExactResolution C aC)
    (hI : Module.PureInjectiveResolution.IsPureInjectiveResolution I aI) :
    ∃ F : C ⟶ I, (F.f 0).hom.comp aC = aI.comp f

Module.PureInjectiveResolution.homotopy_of_same_augmentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/InjectiveResolution.lean, line 332. The attribute's comment: “comparison_homotopy”.

Comparison maps extending the same map between resolved modules are homotopic.

public theorem homotopy_of_same_augmentation
    {M N : Type v} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
    (C I : CochainComplex (ModuleCat.{v} A) ℕ)
    (augmentationC : M →ₗ[A] C.X 0) (augmentationI : N →ₗ[A] I.X 0)
    (hC : Module.PureInjectiveResolution.IsUniversallyExactResolution C augmentationC)
    (hI : Module.PureInjectiveResolution.IsPureInjectiveResolution I augmentationI)
    (f : M →ₗ[A] N) (α β : C ⟶ I)
    (hα : (α.f 0).hom.comp augmentationC = augmentationI.comp f)
    (hβ : (β.f 0).hom.comp augmentationC = augmentationI.comp f) :
    Nonempty (Homotopy α β)

Module.PureInjectiveResolution.exists_pureInjectiveResolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/InjectiveResolution.lean, line 447. The attribute's comment: “existence”.

Every module admits an augmented, universally exact cochain complex of pure injectives.

public theorem exists_pureInjectiveResolution
    (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] :
    ∃ (I : CochainComplex (ModuleCat.{v} A) ℕ) (augmentation : M →ₗ[A] I.X 0),
      Module.PureInjectiveResolution.IsPureInjectiveResolution I augmentation
Tag 0705, a definition

Tag 0705 in the Stacks Project.

Module.pureExt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Ext.lean, line 60.

The ith pure extension module of M by N.

public noncomputable def pureExt (M N : Type v) [AddCommGroup M] [Module A M]
    [AddCommGroup N] [Module A N] (i : ℕ) : ModuleCat.{v} A
Tag 0706, a lemma

Tag 0706 in the Stacks Project.

Module.pureExt_isZero_of_pureInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Ext.lean, line 381. The attribute's comment: “pure_injective_vanishing”.

Positive-degree pure extensions into a pure injective module vanish.

public theorem pureExt_isZero_of_pureInjective
    (M N : Type v) [AddCommGroup M] [Module A M]
    [AddCommGroup N] [Module A N]
    (hN : Module.PureInjective A N)
    (i : ℕ) (hi : 0 < i) :
    CategoryTheory.Limits.IsZero (Module.pureExt (A := A) M N i)

Module.pureExt_isZero_of_pureProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Ext.lean, line 463. The attribute's comment: “pure_projective_vanishing”.

Positive-degree pure extensions out of a pure projective module vanish.

public theorem pureExt_isZero_of_pureProjective
    (M N : Type (max u v)) [AddCommGroup M] [Module A M]
    [AddCommGroup N] [Module A N]
    (hM : Module.PureProjective A M)
    (i : ℕ) (hi : 0 < i) :
    CategoryTheory.Limits.IsZero (Module.pureExt (A := A) M N i)

Module.pureExt_isZero_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/Ext.lean, line 477. The attribute's comment: “finite_presentation_vanishing”.

Positive-degree pure extensions out of a module of finite presentation vanish.

public theorem pureExt_isZero_of_finitePresentation
    (M N : Type (max u v)) [AddCommGroup M] [Module A M]
    [AddCommGroup N] [Module A N] [Module.FinitePresentation A M]
    (i : ℕ) (hi : 0 < i) :
    CategoryTheory.Limits.IsZero (Module.pureExt (A := A) M N i)

Module.pureExtIsoHomologyOfPureProjectiveResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/Pure/ExtResolution.lean, line 664. The attribute's comment: “pure_projective_resolution”.

Pure extensions are computed by a pure projective resolution of the first variable: Pext^i_A(M, N) is the ith cohomology module of Hom_A(Pᐧ, N) for every pure projective resolution Pᐧ ⟶ M.

public noncomputable def pureExtIsoHomologyOfPureProjectiveResolution
    (M N : Type (max u v)) [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
    {P : ChainComplex (ModuleCat.{max u v} A) ℕ} {ε : P.X 0 →ₗ[A] M}
    (hP : Module.PureProjectiveResolution.IsPureProjectiveResolution P ε) (i : ℕ) :
    Module.pureExt (A := A) M N i ≅ (Module.homComplexOfChain P N).homology i
Sources
LeanModule.PureInjective · Module.PureProjective · Module.pureProjective_iff_directSum_finitelyPresented_retract · Module.exists_pureProjective_universallyExact_presentation · Module.characterModule_pureInjective · Module.pureInjective_iff_evalₗ_splits · Module.exists_pureInjective_universallyExact_extension · Module.universallyInjective_range_subtype

Section46.9 Higher exts of quasi-coherent sheaves on the big site#

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

Tag 0708, a lemma

Tag 0708 in the Stacks Project.

AdequateFunctor.injective_iff_moduleExtension_pureInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/InjectiveObjects.lean, line 244.

Stacks Project, Tag 0708. An adequate module-valued functor is injective exactly when it is naturally isomorphic to the extension of a pure injective module.

public theorem injective_iff_moduleExtension_pureInjective {A : Type u} [CommRing A]
    (F : (adequate.{u, v, max u v w} A).FullSubcategory) :
    Injective F ↔ ∃ I : ModuleCat.{max u v w} A, Module.PureInjective A I ∧
      Nonempty (F.obj ≅ moduleExtension.{max u v w, v} A I)
Tag 0709, a lemma

Tag 0709 in the Stacks Project.

Stacks.Adequate.pureExtToExt_bijective_and_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsAdequate/AdequateExtComparisonAll.lean, line 76. The attribute's comment: “every degree i: the canonical arrow is bijective and natural in M and N”.

Let U = Spec A be affine and M, N be A-modules. For every i, the canonical arrow Pext^i_A(M, N) ⟶ Ext^i_{Mod(𝒪)}(M^a, N^a) of pureExtToExt is bijective, and it is functorial in M and in N: precomposition with g : M' ⟶ M on Pext corresponds to composition with the class of g^a, and the action of g : N ⟶ N', through any map of the chosen pure injective resolutions lying over g, to composition with the class of g^a.

public theorem pureExtToExt_bijective_and_natural :
    letI := adequate_isClosedUnderKernels.{u, u} B
    letI := adequate_isClosedUnderCokernels.{u, u} B
    letI := adequate_isClosedUnderFiniteProducts.{u, u} B
    letI : Abelian (adequate.{u, u} B).FullSubcategory := abelian_adequate B
    letI : PreservesFiniteLimits (adequate.{u, u} B).ι := (exact_ι_adequate B).1
    letI : PreservesFiniteColimits (adequate.{u, u} B).ι := (exact_ι_adequate B).2
    letI : HasDerivedCategory.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      HasDerivedCategory.standard _
    letI : HasDerivedCategory.{u + 1} (adequate.{u, u} B).FullSubcategory :=
      HasDerivedCategory.standard _
    letI : HasExt.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      hasExt_of_hasDerivedCategory _
    letI : HasExt.{u + 1} (adequate.{u, u} B).FullSubcategory :=
      hasExt_of_hasDerivedCategory _
    (∀ (M N : ModuleCat.{u} A) (n : ℕ), Function.Bijective (pureExtToExt B M N n)) ∧
    (∀ {M M' : ModuleCat.{u} A} (N : ModuleCat.{u} A) (g : M' ⟶ M) (n : ℕ)
      (x : Module.pureExt (A := A) M N n),
      pureExtToExt B M' N n
          ((HomologicalComplex.homologyMap
            (Module.homComplexPrecomp g.hom (Module.pureExtResolution (A := A) N)) n).hom x) =
        (Ext.mk₀ ((associatedTilde B).map g)).comp (pureExtToExt B M N n x) (zero_add n)) ∧
    (∀ (M : ModuleCat.{u} A) {N N' : ModuleCat.{u} A} (g : N ⟶ N')
      (F : Module.pureExtResolution (A := A) N ⟶ Module.pureExtResolution (A := A) N')
      (_ : (F.f 0).hom.comp (Module.pureExtAugmentation N) =
        (Module.pureExtAugmentation N').comp g.hom)
      (n : ℕ) (x : Module.pureExt (A := A) M N n),
      pureExtToExt B M N' n
          ((HomologicalComplex.homologyMap (Module.homComplexPostcomp M F) n).hom x) =
        (pureExtToExt B M N n x).comp (Ext.mk₀ ((associatedTilde B).map g)) (add_zero n))

Stacks.Adequate.bijective_pureExtToExt_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/PureExtCanonicalArrow.lean, line 264. The attribute's comment: “degree 1: the canonical arrow pureExtToExt, natural in M and N by pureExtToExt_naturality_left/_right, is bijective in degree 1; every degree is pureExtToExt_bijective_and_natural in HigherExtsAdequate/AdequateExtComparisonAll”.

[Stacks, Tag 0709] in degree 1. For U = Spec A affine and A-modules M, N, the canonical arrow Pext¹_A(M, N) ⟶ Ext¹_{Mod((Sch/U)_τ, 𝒪)}(M^a, N^a) is bijective, with no hypothesis. It is the isomorphism Pext¹_A(M, N) ≅ Ext¹_{Adeq(𝒪)}(M^a, N^a) of Stacks.Adequate.pureExtAddEquivExtAdequate followed by the comparison of Tag 06ZW, which is bijective in degree 1 because the adequate modules are closed under extensions (Stacks.Adequate.bijective_mapExtAddHom_ι_adequate_one). The arrow is natural in M and N by Stacks.Adequate.pureExtToExt_naturality_left and _naturality_right.

public theorem bijective_pureExtToExt_one (M N : ModuleCat.{u} A) :
    letI : HasDerivedCategory.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      HasDerivedCategory.standard _
    letI : HasExt.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      hasExt_of_hasDerivedCategory _
    Function.Bijective (pureExtToExt B M N 1)

Stacks.Adequate.pureExtZeroAddEquivExtZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/HigherExtsBase/PureExtComparison.lean, line 179. The attribute's comment: “degree 0, where the canonical arrow is the action of M ↦ M^a on Hom composed with the computation of Pext in degree 0, and neither Tag 06ZW nor Tag 06ZG is needed; functorial in M and N by homAddEquivExtZero_naturality_left/_right together with Module.homComplexZeroHom_naturality_left/_right. Every degree is pureExtToExt_bijective_and_natural in HigherExtsAdequate/AdequateExtComparisonAll”.

[Stacks, Tag 0709] in degree 0. For U = Spec A affine and A-modules M, N, the canonical arrow

Pext⁰_A(M, N) ⟶ Ext⁰_{Mod((Sch/U)_τ, 𝒪)}(M^a, N^a)

is an isomorphism, with no hypothesis. It is the composite of two identifications: Pext⁰_A(M, N) = Hom_A(M, N), because the degree-0 cohomology of Hom_A(M, Iᐧ) is the kernel of its first differential and that kernel is the image of the augmentation (Module.pureExtZeroIsoHom); and Hom_A(M, N) = Ext⁰_{Mod(𝒪)}(M^a, N^a), because M ↦ M^a is fully faithful (Stacks.Adequate.homAddEquivExtZero). Neither Tag 06ZW nor Tag 06ZG enters: in degree 0 the comparison is a map on Hom, so no derived functor and no injective resolution in a category of functors is needed.

Functoriality in M and N is the naturality of the two halves, which is Stacks.Adequate.homAddEquivExtZero_naturality_left and _naturality_right for the Ext half and Module.homComplexZeroHom_naturality_left and Module.homComplexZeroHom_naturality_right for the Pext half; see the module documentation for why the latter two are stated at the Hom complex that computes Module.pureExt rather than at Module.pureExt itself.

The letI preamble is not a list of hypotheses: both entries are the standard derived-category and Ext choices for the sheaves of modules on the site, spelled out rather than registered because declaring them as instances in this chapter changes instance selection for files that do not import this one. It matches the preamble of Stacks.Adequate.bijective_mapExtAddHom_ι_adequate_zero, the degree-0 registration of Tag 06ZW, so the two share one spelling of each object.

public def pureExtZeroAddEquivExtZero (M N : ModuleCat.{u} A) :
    letI : HasDerivedCategory.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      HasDerivedCategory.standard _
    letI : HasExt.{u + 1} (SheafOfModules.{u} B.structureSheaf) :=
      hasExt_of_hasDerivedCategory _
    Module.pureExt (A := A) M N 0 ≃+
      Ext ((associatedTilde B).obj M) ((associatedTilde B).obj N) 0
Sources
LeanAdequateFunctor.injective_iff_moduleExtension_pureInjective · Stacks.Adequate.pureExtToExt_bijective_and_natural · Stacks.Adequate.bijective_pureExtToExt_one · Stacks.Adequate.pureExtZeroAddEquivExtZero

Section46.10 Derived categories of adequate modules, II#

Section 46.10 of the Stacks Project, Tag 070T. 4 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 070U, an equation

Tag 070U in the Stacks Project.

AlgebraicGeometry.BigFppfOver.baseToZariskiRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseRingedSite.lean, line 366.

The morphism of ringed sites f : ((Sch/S)_τ, 𝒪) ⟶ (S_Zar, 𝒪_S), for each τ ∈ {Zariski, étale, smooth, syntomic, fppf}: the continuous inclusion of the small Zariski site of S into the big site, with structure map the identification of the sections of 𝒪_S over an open with the functions on it.

public noncomputable def baseToZariskiRingedToposHom (τ : SiteKind) :
    RingedToposSiteHom (baseRingedTopos B S hS τ) S.zariskiRingedTopos
Tag 070V, a remark

Tag 070V in the Stacks Project.

Stacks.Adequate.BigSite.Coarsening.derivedAdequateCoarseningEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedTopologyIndependence.lean, line 249. The attribute's comment: “the canonical equivalence of D_Adeq(𝒪_τ) and D_Adeq(𝒪_τ'), for a coarsening of a chosen big site, at any models of the two derived categories”.

[Stacks, Tag 070V]. Let S be a scheme and let τ and τ' be two of the five topologies Zar, étale, smooth, syntomic, fppf, with τ stronger than τ', and denote 𝒪_τ and 𝒪_τ' the structure sheaf 𝒪 viewed as a sheaf on the big τ-site, resp. the big τ'-site, over S. Then D_Adeq(𝒪_τ) and D_Adeq(𝒪_τ') are canonically equivalent.

The equivalence is [Stacks, Tag 07A8] for the category of the site, the class of adequate 𝒪_τ-modules and the affine objects of the site (Stacks.Cohomology.CompareTopologies.derivedEquivalenceImageOfLEOfEssentiallySmall). Its assumption (1) is Stacks.Adequate.BigSite.Coarsening.adequateIsFineSheaf, (2) is Stacks.Adequate.adequate_isWeakSerreClass, (3) is Stacks.Adequate.BigSite.Coarsening.affineCoarseCovering and (4) is Stacks.Adequate.BigSite.isZero_rightDerived_sections_of_isAdequate, [Stacks, Tag 06VM] (3). Assumption (1) also identifies the image class of the adequate 𝒪_τ-modules with the adequate 𝒪_τ'-modules (Stacks.Adequate.BigSite.Coarsening.adequate_site_eq_imageOfLE).

def derivedAdequateCoarseningEquivalence
    [HasDerivedCategory.{d} (SheafOfModules.{u} B.structureSheaf)]
    [HasDerivedCategory.{d'} (SheafOfModules.{u} c.site.structureSheaf)] :
    (BigSite.derivedAdequate.{u, u, d} B).FullSubcategory ≌
      (BigSite.derivedAdequate.{u, u, d'} c.site).FullSubcategory

Stacks.Adequate.BigSite.derivedAdequateTopologyEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedTopologyIndependence.lean, line 312. The attribute's comment: “D_Adeq(𝒪_τ) ≌ D_Adeq(𝒪_τ') for any two of the five topologies, for big sites built on the same category of schemes over S, at any models of the two derived categories”.

[Stacks, Tag 070V]. Let S be a scheme and let τ, τ' be two of the five topologies Zar, étale, smooth, syntomic, fppf, and denote 𝒪_τ, resp. 𝒪_τ', the structure sheaf 𝒪 viewed as a sheaf on the big site (Sch/S)_τ, resp. (Sch/S)_τ', the two big sites being built on the same category of schemes over S (their cutoffs agree). Then D_Adeq(𝒪_τ) and D_Adeq(𝒪_τ') are canonically equivalent.

The five topologies are linearly ordered, Zar ≺ étale ≺ smooth ≺ syntomic ≺ fppf; if τ is finer than τ' this is Stacks.Adequate.BigSite.derivedAdequateEquivalenceOfIsFiner, and otherwise τ' is finer than τ and it is the inverse of that equivalence with the roles of the two sites exchanged. Both derived categories are taken at arbitrary models.

def BigSite.derivedAdequateTopologyEquivalence (B : BigSite τ S) (B' : BigSite τ' S)
    (hcut : B'.cutoff = B.cutoff)
    [HasDerivedCategory.{d} (SheafOfModules.{u} B.structureSheaf)]
    [HasDerivedCategory.{d'} (SheafOfModules.{u} B'.structureSheaf)] :
    (BigSite.derivedAdequate.{u, u, d} B).FullSubcategory ≌
      (BigSite.derivedAdequate.{u, u, d'} B').FullSubcategory

Stacks.Adequate.BigSite.Coarsening.derivedAdequateEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/TopologyIndependence.lean, line 353. The attribute's comment: “the canonical isomorphism of D_Adeq(𝒪_τ) and D_Adeq(𝒪_τ') as an equivalence of categories, for a coarsening of a chosen big site; the inputs it takes, and the one proved here, are listed in the docstring”.

[Stacks, Tag 070V]. Let S be a scheme and let τ and τ' be two of the five topologies Zar, étale, smooth, syntomic, fppf, with τ stronger than τ', and denote 𝒪_τ and 𝒪_τ' the structure sheaf 𝒪 viewed as a sheaf on the big τ-site, resp. the big τ'-site, over S. Then D_Adeq(𝒪_τ) and D_Adeq(𝒪_τ') are canonically isomorphic.

The equivalence is the second conclusion of [Stacks, Tag 07A8] applied to the class of adequate 𝒪_τ-modules and to the collection of affine objects of the site. Its assumption (2) is Stacks.Adequate.adequate_isWeakSerreClass and its assumption (4) is Stacks.Adequate.BigSite.isZero_rightDerived_sections_of_isAdequate, which is [Stacks, Tag 06VM] (3) and carries no hypothesis; assumptions (1) and (3) are hfine and hcover. That the two sides are the derived categories of the adequate modules for each topology, rather than of the adequate modules for τ and their image under ε_*, is Stacks.Adequate.BigSite.Coarsening.adequate_site_eq_imageOfLE.

The inputs this declaration takes are: comparison, the second conclusion of [Stacks, Tag 07A8] in the generality of its source, which this library does not prove; AdequateIsFineSheaf and AffineCoarseCovering, assumptions (1) and (3) of 07A8 for the adequate modules and the affine objects. Assumption (2) is discharged outright by [Stacks, Tag 06VQ], and assumption (4) by [Stacks, Tag 06VM] (3). The modules have values in the universe of the site, the universe at which [Stacks, Tag 06VQ] is available.

public def derivedAdequateEquivalence
    [HasSheafify c.topology AddCommGrpCat.{u}]
    [c.topology.WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasDerivedCategory.{d} (SheafOfModules.{u} B.structureSheaf)]
    [HasDerivedCategory.{d} (SheafOfModules.{u} c.site.structureSheaf)]
    (comparison : ∀ {C : Type (u + 1)} [Category.{u} C] {J J' : GrothendieckTopology C}
      (h : J' ≤ J) (R : Sheaf J RingCat.{u})
      [HasSheafify J AddCommGrpCat.{u}]
      [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
      [HasSheafify J' AddCommGrpCat.{u}]
      [J'.WEqualsLocallyBijective AddCommGrpCat.{u}]
      [EnoughInjectives (Sheaf J AddCommGrpCat.{u})]
      [HasDerivedCategory.{d} (SheafOfModules.{u} R)]
      [HasDerivedCategory.{d} (SheafOfModules.{u} (R.ofLE h))]
      (A : ObjectProperty (SheafOfModules.{u} R)) (ℬ : Set C), A.IsWeakSerreClass →
        (∀ U : C, ∃ 𝒰 : PreZeroHypercover.{u + 1} U, 𝒰.sieve₀ ∈ J' U ∧ ∀ i, ℬ (𝒰.X i)) →
        (∀ U ∈ ℬ, ∀ p : ℕ, 0 < p → ∀ F, A F →
          IsZero ((((sheafSections J AddCommGrpCat.{u}).obj (op U)).rightDerived p).obj
            ((SheafOfModules.toSheaf R).obj F))) →
        ((DerivedCategoryB.derivedCategoryB A).FullSubcategory ≌
          (DerivedCategoryB.derivedCategoryB
            (Stacks.Cohomology.CompareTopologies.imageOfLE.{u + 1, u, u, u} h R
              A)).FullSubcategory))
    (hfine : AdequateIsFineSheaf.{u, u} c) (hcover : AffineCoarseCovering.{u} c) :
    (BigSite.derivedAdequate.{u, u, d} B).FullSubcategory ≌
      (BigSite.derivedAdequate.{u, u, d} c.site).FullSubcategory
Tag 070W, a remark

Tag 070W in the Stacks Project.

Stacks.Adequate.BigSite.derivedRestrictAdequate, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedRestriction.lean, line 293. The attribute's comment: “the assertion that Rf_ carries D_Adeq(𝒪) into D_QCoh(S), in the source's own form Rf_ = f_ for the Zariski restriction of the morphism of Tag 070U, with right exactness of that restriction an instance argument. Lf^, adjointness and Rf_ Lf^ ≅ id are covered elsewhere”.

[Stacks, Tag 070W], the pushforward landing in the source's own form Rf_* = f_*. Restriction to the small Zariski site of S along the morphism of [Stacks, Tag 070U], assumed right exact, induces a functor D_Adeq(𝒪) ⥤ D_QCoh(S) on the chosen big fppf site over S; on modules it lands in the quasi-coherent sheaves by [Stacks, Tag 06VM] (1).

public def BigSite.derivedRestrictAdequate :
    (BigSite.derivedAdequate.{u, u, d} (BigSite.ofBigFppfSite B S hS)).FullSubcategory ⥤
      (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent S.ringCatSheaf)).FullSubcategory

Stacks.Adequate.BigSite.derivedAdequateAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedRestriction.lean, line 366. The attribute's comment: “the adjointness assertion only, for the subcategories D_Adeq(O) and D_QCoh(S); the ambient adjunction and the two landing assertions are inputs, listed in the docstring”.

[Stacks, Tag 070W], the adjointness assertion. Given the ambient derived adjunction Lf^* ⊣ Rf_* on all 𝒪-modules and the two landing assertions, the restricted functors Lf^* : D_QCoh(S) ⥤ D_Adeq(𝒪) and Rf_* : D_Adeq(𝒪) ⥤ D_QCoh(S) are adjoint.

The inputs are the ambient derived adjunction adj : L ⊣ R on all modules and both landing assertions — hL, that Lf^* carries D_QCoh(S) into D_Adeq(𝒪), and hR, that Rf_* carries D_Adeq(𝒪) into D_QCoh(S). Each carries its own content and none is proved here: the ambient adjunction of [Stacks, Tag 07A6] is not available for the morphism of [Stacks, Tag 070U] at the universes in which that morphism is stated. The isomorphism Rf_* Lf^* ≅ id is a separate declaration.

public def BigSite.derivedAdequateAdjunction (adj : L ⊣ R) :
    BigSite.derivedAdequatePullback B L hL ⊣
      BigSite.derivedAdequatePushforward B R hR

Stacks.Adequate.BigSite.derivedQuasicoherentAdequateAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedZariskiQuasicoherent.lean, line 97. The attribute's comment: “the adjunction Lf^ ⊣ Rf_ between D_QCoh(S) and D_Adeq(O), for the derived functors of the morphism of Tag 070U on a chosen big site, with no hypothesis”.

[Stacks, Tag 070W], the adjunction. The morphism f of [Stacks, Tag 070U] induces adjoint functors Lf^* : D_QCoh(S) ⥤ D_Adeq(𝒪) and Rf_* : D_Adeq(𝒪) ⥤ D_QCoh(S): the total derived functors of [Stacks, Tag 07A6] preserve the two subcategories, and their adjunction restricts.

def BigSite.derivedQuasicoherentAdequateAdjunction :
    B.derivedQuasicoherentPullback ⊣ B.derivedAdequateDirectImage

Stacks.Adequate.BigSite.derivedAdequateDirectImagePullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedZariskiQuasicoherent.lean, line 106. The attribute's comment: “Rf_ Lf^ ≅ id on D_QCoh(S), for the derived functors of the morphism of Tag 070U on a chosen big site”.

[Stacks, Tag 070W], Rf_* Lf^* ≅ id_{D_QCoh(S)}. The unit of the derived adjunction is invertible at every complex with quasi-coherent cohomology.

def BigSite.derivedAdequateDirectImagePullbackIso :
    B.derivedQuasicoherentPullback ⋙ B.derivedAdequateDirectImage ≅ 𝟭 _
Tag 070X, a remark

Tag 070X in the Stacks Project.

Stacks.Adequate.BigSite.isLocalization_derivedAdequatePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedQuotient.lean, line 223. The attribute's comment: “the equivalence D_Adeq(𝒪)/D_𝒞(𝒪) ⟶ D_QCoh(S), with the quotient described as the localization at the morphisms Rf_* inverts; the description by the subcategory D_𝒞(𝒪) = ker Rf_* is the companion BigSite.isLocalization_trW_kernel_derivedAdequatePushforward. The ambient derived adjunction adj, both landing assertions hL and hR, and the invertibility hunit of the ambient unit on D_QCoh(S) are hypotheses, exactly as for the Tag 070W declarations this consumes; none of them is proved here”.

[Stacks, Tag 070X]. Rf_* : D_Adeq(𝒪) ⥤ D_QCoh(S) is a localization functor for the morphisms of D_Adeq(𝒪) that it carries to isomorphisms of D_QCoh(S), so that D_Adeq(𝒪)/D_𝒞(𝒪) ⟶ D_QCoh(S) is an equivalence.

public theorem BigSite.isLocalization_derivedAdequatePushforward :
    (BigSite.derivedAdequatePushforward B R hR).IsLocalization
      ((MorphismProperty.isomorphisms _).inverseImage
        (BigSite.derivedAdequatePushforward B R hR))

Stacks.Adequate.BigSite.derivedAdequateQuotientEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedQuotient.lean, line 236. The attribute's comment: “the equivalence of categories itself, for the quotient described as the localization at the morphisms Rf_* inverts; the hypotheses are those of BigSite.isLocalization_derivedAdequatePushforward”.

[Stacks, Tag 070X], the equivalence. The localization of D_Adeq(𝒪) at the morphisms inverted by Rf_* is equivalent to D_QCoh(S).

public def BigSite.derivedAdequateQuotientEquivalence :
    ((MorphismProperty.isomorphisms _).inverseImage
        (BigSite.derivedAdequatePushforward B R hR)).Localization ≌
      (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent S.ringCatSheaf)).FullSubcategory

Stacks.Adequate.BigSite.isLocalization_trW_kernel_derivedAdequatePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedQuotient.lean, line 275. The attribute's comment: “the equivalence D_Adeq(𝒪)/D_𝒞(𝒪) ⟶ D_QCoh(S) with the quotient taken, as in the source, at the morphisms whose cone lies in the subcategory D_𝒞(𝒪), realised as the kernel of Rf_*, which is the source's own description of it. Beyond the hypotheses of BigSite.isLocalization_derivedAdequatePushforward, the pretriangulated structures of the two subcategories and the triangulatedness of the restricted Rf_* are instance arguments; the library does not construct them for the restricted functors”.

[Stacks, Tag 070X] in the source's own form. Rf_* : D_Adeq(𝒪) ⥤ D_QCoh(S) is a localization functor for the morphisms whose cone lies in D_𝒞(𝒪), the kernel of Rf_*.

public theorem BigSite.isLocalization_trW_kernel_derivedAdequatePushforward :
    (BigSite.derivedAdequatePushforward B R hR).IsLocalization
      (ObjectProperty.trW (BigSite.derivedAdequatePushforward B R hR).kernel)

Stacks.Adequate.BigSite.derivedParasiticQuotientEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedQuotient.lean, line 289. The attribute's comment: “the equivalence of categories itself, in the source's own form: the quotient of D_Adeq(𝒪) by D_𝒞(𝒪) = ker Rf_*. The hypotheses are those of BigSite.isLocalization_trW_kernel_derivedAdequatePushforward”.

[Stacks, Tag 070X], the equivalence D_Adeq(𝒪)/D_𝒞(𝒪) ≌ D_QCoh(S). The quotient of D_Adeq(𝒪) by the complexes with parasitic cohomology, the kernel of Rf_*, is equivalent to D_QCoh(S).

public def BigSite.derivedParasiticQuotientEquivalence :
    (ObjectProperty.trW
        (BigSite.derivedAdequatePushforward B R hR).kernel).Localization ≌
      (DerivedCategoryB.derivedCategoryB
        (SheafOfModules.isQuasicoherent S.ringCatSheaf)).FullSubcategory

Stacks.Adequate.BigSite.isLocalization_trW_derivedParasitic_derivedAdequateDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedQuotientUnconditional.lean, line 218. The attribute's comment: “the equivalence D_Adeq(O)/D_C(O) -> D_QCoh(S) induced by Rf_*, with the quotient the Verdier quotient by the complexes with parasitic adequate cohomology, for the derived functors of the morphism of Tag 070U on a chosen big site and each of the five topologies”.

[Stacks, Tag 070X]. Let S be a scheme and f : ((Sch/S)_τ, 𝒪) ⟶ (S_Zar, 𝒪_S) the morphism of [Stacks, Tag 070U], for a chosen big site and any of the five topologies. The derived direct image Rf_* : D_Adeq(𝒪) ⥤ D_QCoh(S) is the Verdier quotient of D_Adeq(𝒪) by D_𝒞(𝒪), the complexes whose cohomology modules are parasitic adequate: it is a localization functor for the morphisms whose cone lies in D_𝒞(𝒪), so that it induces an equivalence D_Adeq(𝒪)/D_𝒞(𝒪) ⟶ D_QCoh(S).

public theorem BigSite.isLocalization_trW_derivedParasitic_derivedAdequateDirectImage :
    B.derivedAdequateDirectImage.IsLocalization
      ((BigSite.derivedParasitic B).inverseImage
        (DerivedCategoryB.derivedCategoryB (adequate.{u, u} B : ObjectProperty (SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf B.ringedSite.toRingedTopos.O)))).ι).trW

Stacks.Adequate.BigSite.derivedAdequateParasiticQuotientEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Adequate/AdequateModules/DerivedQuotientUnconditional.lean, line 237. The attribute's comment: “the equivalence of categories D_Adeq(O)/D_C(O) ≌ D_QCoh(S) itself, for the derived functors of the morphism of Tag 070U on a chosen big site and each of the five topologies”.

[Stacks, Tag 070X], the equivalence D_Adeq(𝒪)/D_𝒞(𝒪) ≌ D_QCoh(S). The Verdier quotient of D_Adeq(𝒪) by the complexes with parasitic adequate cohomology is equivalent to D_QCoh(S), by the functor induced by Rf_*.

public def BigSite.derivedAdequateParasiticQuotientEquivalence :
    ((BigSite.derivedParasitic B).inverseImage
        (DerivedCategoryB.derivedCategoryB (adequate.{u, u} B : ObjectProperty (SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            B.ringedSite.toRingedTopos.O)))).ι).trW.Localization ≌
      (DerivedCategoryB.derivedCategoryB (SheafOfModules.isQuasicoherent S.ringCatSheaf :
        ObjectProperty (SheafOfModules.{u}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            S.zariskiRingedSite.toRingedTopos.O)))).FullSubcategory
Sources
LeanAlgebraicGeometry.BigFppfOver.baseToZariskiRingedToposHom · Stacks.Adequate.BigSite.Coarsening.derivedAdequateCoarseningEquivalence · Stacks.Adequate.BigSite.derivedAdequateTopologyEquivalence · Stacks.Adequate.BigSite.Coarsening.derivedAdequateEquivalence · Stacks.Adequate.BigSite.derivedRestrictAdequate · Stacks.Adequate.BigSite.derivedAdequateAdjunction · Stacks.Adequate.BigSite.derivedQuasicoherentAdequateAdjunction · Stacks.Adequate.BigSite.derivedAdequateDirectImagePullbackIso

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.