15.81 Strong generators and… to 15.91 Formal glueing of module…

Section15.81 Strong generators and regular rings#

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

Tag 0FXH, a lemma

Tag 0FXH in the Stacks Project.

StrongGeneration.comp_eq_zero_of_mem_triangEnvelopeIter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/StrongGenerator.lean, line 406.

Stacks 0FXH. If K belongs to ⟨R⟩ₙ in the derived category of a ring and a chain of n morphisms beginning at K induces the zero map on cohomology in every degree, then the composite of the chain is zero.

theorem comp_eq_zero_of_mem_triangEnvelopeIter
    {R : Type u} [Ring R] (n : ℕ) (hn : 0 < n)
    (F : ComposableArrows (DerivedCategory (ModuleCat.{u} R)) n)
    (hFleft :
      ObjectProperty.triangEnvelopeIter
        (ObjectProperty.singleton
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R)))
        (n - 1) F.left)
    (hF : ∀ (i : ℕ) (_ : i < n) (j : ℤ),
      (DerivedCategory.homologyFunctor (ModuleCat.{u} R) j).map (F.map' i (i + 1)) = 0) :
    F.hom = 0
Tag 0FXI, a lemma

Tag 0FXI in the Stacks Project.

StrongGeneration.isRegularRing_and_ringKrullDim_ne_top_of_isStrongGenerator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/StrongGenerator.lean, line 629.

Stacks 0FXI. A Noetherian ring for which R strongly generates its perfect derived category — that is, for which a single stage ⟨R⟩ₙ already exhausts ⟨R⟩ — is regular and has finite Krull dimension.

theorem isRegularRing_and_ringKrullDim_ne_top_of_isStrongGenerator
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    (h : ∃ n : ℕ,
      ObjectProperty.triangEnvelopeIter
        (ObjectProperty.singleton
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))) n =
      ObjectProperty.triangEnvelope
        (ObjectProperty.singleton
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R)))) :
    IsRegularRing R ∧ ringKrullDim R ≠ ⊤
Tag 0FXJ, a lemma

Tag 0FXJ in the Stacks Project.

StrongGeneration.subsingleton_hom_of_isGE_of_isLE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/StrongGenerator.lean, line 861.

Stacks 0FXJ. Let R be a regular Noetherian ring of finite dimension d. If K and L are bounded-above derived R-modules, the cohomology of K vanishes in degrees at most k, and the cohomology of L vanishes in degrees at least k - d + 1, then every morphism from K to L is zero.

theorem subsingleton_hom_of_isGE_of_isLE [IsRegularRing R]
    (d : ℕ) (hdim : ringKrullDim R = d)
    (K L : DerivedCategory.Minus (ModuleCat.{u} R)) (k : ℤ)
    (hK : K.obj.IsGE (k + 1)) (hL : L.obj.IsLE (k - d)) :
    Subsingleton (K.obj ⟶ L.obj)
Tag 0FXK, a lemma

Tag 0FXK in the Stacks Project.

StrongGeneration.iso_biproduct_truncations_of_cohomology_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/StrongGenerator.lean, line 879.

Stacks 0FXK. Let R be a regular Noetherian ring of finite positive dimension d. If a perfect derived R-module K has zero cohomology in every degree from k - d + 2 through k, then K is isomorphic to the biproduct of its truncations in degrees at most k - d + 1 and at least k + 1.

theorem iso_biproduct_truncations_of_cohomology_isZero [IsRegularRing R]
    (d : ℕ) (hdim : ringKrullDim R = d) (hd : 1 ≤ d)
    (K : DerivedCategory (ModuleCat.{u} R)) (hKperfect : StacksDraft.Perfect.IsPerfect K) (k : ℤ)
    (hK : ∀ i : ℤ, k - d + 2 ≤ i → i ≤ k →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj K)) :
    Nonempty
      (K ≅
        (DerivedCategory.TStructure.t.truncLE (k - d + 1)).obj K ⊞
          (DerivedCategory.TStructure.t.truncGE (k + 1)).obj K)
Tag 0FXL, a lemma

Tag 0FXL in the Stacks Project.

StrongGeneration.exists_triangEnvelopeIter_eq_isPerfect_of_isRegularRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/StrongGenerator.lean, line 1268.

Stacks 0FXL. Over a regular ring of finite Krull dimension, the regular module placed in degree zero is a strong generator of the perfect derived category: a single stage ⟨R⟩ₙ of the triangulated envelope of R[0] already contains every perfect complex. One may take for n the global dimension of R.

theorem exists_triangEnvelopeIter_eq_isPerfect_of_isRegularRing
    {R : Type u} [CommRing R] [IsRegularRing R] (hdim : ringKrullDim R ≠ ⊤) :
    ∃ n : ℕ,
      ObjectProperty.triangEnvelopeIter
          (ObjectProperty.singleton
            ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R))) n =
        (StacksDraft.Perfect.IsPerfect :
          ObjectProperty (DerivedCategory (ModuleCat.{u} R)))
Tag 0FXM, a proposition

Tag 0FXM in the Stacks Project.

StrongGeneration.isRegularRing_and_ringKrullDim_ne_top_iff_hasStrongGenerator_iff_regularModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/StrongGenerator.lean, line 1298.

Stacks 0FXM. For a Noetherian ring R the following are equivalent: R is regular of finite Krull dimension; the perfect derived category of R admits a strong generator; and the regular module placed in degree zero is such a strong generator. The implication from an arbitrary strong generator to the regular module uses that any object of the perfect derived category already lies in some finite stage of the envelope of R[0], so the stages of its own envelope are absorbed into those of R[0].

theorem isRegularRing_and_ringKrullDim_ne_top_iff_hasStrongGenerator_iff_regularModule
    {R : Type u} [CommRing R] [IsNoetherianRing R] :
    let D := DerivedCategory (ModuleCat.{u} R)
    let perfect := (StacksDraft.Perfect.IsPerfect : ObjectProperty D)
    let regularModule :=
      (DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj (ModuleCat.of R R)
    let regularFinite := IsRegularRing R ∧ ringKrullDim R ≠ ⊤
    let hasStrongGenerator := ∃ E : D, ∃ n : ℕ,
      ObjectProperty.triangEnvelopeIter (ObjectProperty.singleton E) n = perfect
    let regularModuleIsStrongGenerator := ∃ n : ℕ,
      ObjectProperty.triangEnvelopeIter (ObjectProperty.singleton regularModule) n = perfect
    (regularFinite ↔ hasStrongGenerator) ∧
      (hasStrongGenerator ↔ regularModuleIsStrongGenerator)
Sources

Section15.82 Relatively finitely presented modules#

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

Tag 05GY, a lemma

Tag 05GY in the Stacks Project.

Module.finitePresentationRel_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/Basic.lean, line 117.

Stacks 05GY: for an A-module M over a finite type ring map R → A, the three conditions "some presentation", "all presentations" and "all finitely presented covers" are equivalent.

theorem Module.finitePresentationRel_tfae [Algebra.FiniteType R A] :
    [Module.FinitePresentationRel R A M,
     Module.FinitePresentationRel.AllPresentations R A M,
     Module.FinitePresentationRel.AllFPCovers.{u} R A M].TFAE

Module.FinitePresentationRel.finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/Relative.lean, line 129. The attribute's comment: “the final conclusion, that a module finitely presented relative to R is a finitely presented A-module”.

A module finitely presented relative to R is a finitely presented A-module.

theorem Module.FinitePresentationRel.finitePresentation
    (h : Module.FinitePresentationRel R A M) : Module.FinitePresentation A M
Tag 05GZ, a definition

Tag 05GZ in the Stacks Project.

Module.FinitePresentationRel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/FinitePresentation/Relative.lean, line 40.

M is finitely presented relative to R: for some surjective R-algebra map α : R[x_1, …, x_n] → A, the module M viewed over R[x_1, …, x_n] via α is finitely presented.

def Module.FinitePresentationRel (R A : Type*) [CommRing R] [CommRing A] [Algebra R A]
    (M : Type*) [AddCommGroup M] [Module A M] : Prop
Tag 05H0, a lemma

Tag 05H0 in the Stacks Project.

Module.finitePresentationRel_iff_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/Finite.lean, line 297.

Stacks Tag 05H0 (Lemma 15.82.3). Let R be a ring, φ : A → B a finite map of R-algebras with both R → A and R → B of finite type, and M a B-module (hence an A-module via φ). Then M is finitely presented relative to R as an A-module iff it is finitely presented relative to R as a B-module.

The hypothesis [IsScalarTower R A B] encodes that A → B is a map of R-algebras; [IsScalarTower A B M] encodes that the A-module structure on M is the one obtained by restriction of scalars along φ : A → B.

theorem Module.finitePresentationRel_iff_of_finite
    (R A B : Type*) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
    [Algebra.FiniteType R A] [Algebra.FiniteType R B] [Module.Finite A B]
    (M : Type*) [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] :
    Module.FinitePresentationRel R A M ↔ Module.FinitePresentationRel R B M
Tag 065A, a lemma

Tag 065A in the Stacks Project.

Module.finitePresentationRel_away_of_away, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/Localization.lean, line 74.

Let A be a finite type algebra over a localization R_f, and let M be an A-module finitely presented relative to R_f. For g : A the localized module M_g over A_g is finitely presented relative to R. The composite R → R_f → A is given by an Algebra R A instance together with the scalar tower R → R_f → A.

theorem finitePresentationRel_away_of_away {R : Type u} [CommRing R] (f : R) {A : Type v}
    [CommRing A] [Algebra (Localization.Away f) A] [Algebra R A]
    [IsScalarTower R (Localization.Away f) A]
    [Algebra.FiniteType (Localization.Away f) A] (g : A) {M : Type w} [AddCommGroup M]
    [Module A M] (hM : Module.FinitePresentationRel (Localization.Away f) A M) :
    Module.FinitePresentationRel R (Localization.Away g) (LocalizedModule.Away g M)
Tag 065B, a lemma

Tag 065B in the Stacks Project.

finitePresentation_relative_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/BaseChange.lean, line 93. References: EGA IV (1.3.1); EGA IV (1.4.1), “more general”.

Let R → A be a finite type ring map and M an A-module finitely presented relative to R. For any ring map R → R', set A' := A ⊗[R] R' (an R'-algebra via the right factor and, canonically, an A-algebra via the left factor) and M' := A' ⊗[A] M (an A'-module via the left tensor factor A'). Then R' → A' is of finite type, and M' is finitely presented relative to R'.

theorem finitePresentation_relative_baseChange (R A R' M : Type*)
    [CommRing R] [CommRing A] [CommRing R'] [Algebra R A] [Algebra R R']
    [AddCommGroup M] [Module A M] [Algebra.FiniteType R A]
    (hM : Module.FinitePresentationRel R A M) :
    letI : Algebra R' (TensorProduct R A R') := Algebra.TensorProduct.rightAlgebra
    letI : Algebra A (TensorProduct R A R') := Algebra.TensorProduct.leftAlgebra
    Algebra.FiniteType R' (TensorProduct R A R') ∧
    Module.FinitePresentationRel R' (TensorProduct R A R')
      (TensorProduct A (TensorProduct R A R') M)
Tag 0670, a lemma

Tag 0670 in the Stacks Project.

finitelyPresentedRelative_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/BaseChange.lean, line 363. References: EGA IV (1.4.1), “more general”.

Let R → A be a ring map, M an A-module finitely presented relative to R, and A → A' a ring map of finite presentation. Then the A'-module A' ⊗[A] M (here TensorProduct A A' M, with its natural A'-module structure) is finitely presented relative to R.

The finite type hypothesis on R → A of the Stacks statement is not needed.

theorem finitelyPresentedRelative_baseChange
    (R A A' : Type*) [CommRing R] [CommRing A] [CommRing A']
    [Algebra R A] [Algebra A A'] [Algebra R A'] [IsScalarTower R A A']
    (M : Type*) [AddCommGroup M] [Module A M]
    (hM : Module.FinitePresentationRel R A M)
    [Algebra.FinitePresentation A A'] :
    Module.FinitePresentationRel R A' (TensorProduct A A' M)
Tag 065C, a lemma

Tag 065C in the Stacks Project.

Module.finitePresentationRel_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/Basic.lean, line 156.

Stacks 065C, Lemma 15.82.7. Given finite type ring maps R → A and A → B and a B-module M, if M is finitely presented relative to A and A is of finite presentation over R, then M is finitely presented relative to R.

theorem Module.finitePresentationRel_comp {R A B : Type*} [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    [Algebra.FinitePresentation R A] {M : Type*} [AddCommGroup M] [Module B M]
    (hM : Module.FinitePresentationRel A B M) : Module.FinitePresentationRel R B M
Tag 065D, a lemma

Tag 065D in the Stacks Project.

Module.finitePresentationRel_iff_of_span_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/Localization.lean, line 175.

Relative finite presentation of a module over a finite type algebra can be checked on a finite family of principal opens covering the spectrum: if f : ι → A generates the unit ideal, then M is finitely presented relative to R exactly when each M_{f i} is finitely presented relative to R over A_{f i}.

theorem finitePresentationRel_iff_of_span_eq_top {R : Type u} [CommRing R] {A : Type v}
    [CommRing A] [Algebra R A] [Algebra.FiniteType R A] {M : Type w} [AddCommGroup M]
    [Module A M] {ι : Type x} [Finite ι] (f : ι → A) (hf : Ideal.span (Set.range f) = ⊤) :
    (∀ i, Module.FinitePresentationRel R (Localization.Away (f i))
      (LocalizedModule.Away (f i) M)) ↔ Module.FinitePresentationRel R A M
Tag 0671, a lemma

Tag 0671 in the Stacks Project.

Module.finitePresentationRel_two_of_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/Basic.lean, line 230. The attribute's comment: “(1)”.

Stacks 0671, part (1). Given a short exact sequence of A-modules 0 → M' →[i] M →[p] M'' → 0 (so i is injective, p is surjective and range i = ker p), if M' and M'' are finitely presented relative to R, then M is finitely presented relative to R.

By Stacks 05GY, M' and M'' are finitely presented over R[x_1, …, x_n] for every presentation α, so one may pick a single presentation and apply two-out-of-three over the polynomial ring R[x_1, …, x_n].

theorem Module.finitePresentationRel_two_of_three (i : M' →ₗ[A] M) (p : M →ₗ[A] M'')
    (hi : Function.Injective i) (hp : Function.Surjective p)
    (hex : LinearMap.range i = LinearMap.ker p)
    (hM' : Module.FinitePresentationRel R A M')
    (hM'' : Module.FinitePresentationRel R A M'') :
    Module.FinitePresentationRel R A M

Module.finitePresentationRel_of_surjective_of_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/Basic.lean, line 261. The attribute's comment: “(2)”.

Stacks 0671, part (2). Given a short exact sequence of A-modules 0 → M' →[i] M →[p] M'' → 0, if M' is a finite type (finitely generated) A-module and M is finitely presented relative to R, then M'' is finitely presented relative to R.

theorem Module.finitePresentationRel_of_surjective_of_finite {R A : Type*} [CommRing R]
    [CommRing A] [Algebra R A] {M' M M'' : Type*} [AddCommGroup M'] [Module A M']
    [AddCommGroup M] [Module A M] [AddCommGroup M''] [Module A M'']
    (i : M' →ₗ[A] M) (p : M →ₗ[A] M'')
    (hp : Function.Surjective p)
    (hex : LinearMap.range i = LinearMap.ker p)
    (hM' : Module.Finite A M') (hM : Module.FinitePresentationRel R A M) :
    Module.FinitePresentationRel R A M''
Tag 0672, a lemma

Tag 0672 in the Stacks Project.

Module.finitePresentationRel_of_prod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/FinitePresentationRel/Basic.lean, line 305.

Stacks 0672 (Lemma 15.82.10).

Let R → A be a ring map (in Stacks, of finite type — the hypothesis is not needed here) and let M, M' be A-modules. If the direct sum M × M' is finitely presented relative to R, then both M and M' are finitely presented relative to R.

theorem Module.finitePresentationRel_of_prod {R A : Type*} [CommRing R] [CommRing A]
    [Algebra R A] {M M' : Type*} [AddCommGroup M] [Module A M] [AddCommGroup M'] [Module A M']
    (h : Module.FinitePresentationRel R A (M × M')) :
    Module.FinitePresentationRel R A M ∧ Module.FinitePresentationRel R A M'
Sources

Section15.83 Relatively pseudo-coherent modules#

Section 15.83 of the Stacks Project, Tag 065E. 17 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 065F, a lemma

Tag 065F in the Stacks Project.

PseudoCoherence.derivedTensorPolynomialEvalZeroIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/PolynomialRetract.lean, line 330.

Stacks 065F. If R[X] → R evaluates X at zero, then for every K ∈ D(R), the derived tensor product of K, regarded as an R[X]-complex, with R is isomorphic in D(R) to K ⊞ K[1].

public theorem derivedTensorPolynomialEvalZeroIso
    {R : Type u} [CommRing R]
    (D : KFlatDerivedTensoringDatum (Polynomial R))
    (K : DerivedCategory (ModuleCat.{u} R)) :
    let ev : Polynomial R →+* R := Polynomial.eval₂RingHom (RingHom.id R) 0
    letI : Module (Polynomial R) R := ev.toAlgebra.toModule
    Nonempty
      ((ModuleCat.restrictScalars
          (Polynomial.C : R →+* Polynomial R)).mapDerivedCategory.obj
            ((D.tensor.obj ((ModuleCat.restrictScalars ev).mapDerivedCategory.obj K)).obj
              ((DerivedCategory.singleFunctor (ModuleCat.{u} (Polynomial R)) 0).obj
                (ModuleCat.of (Polynomial R) R))) ≅
        Limits.biprod K
          ((shiftFunctor (DerivedCategory (ModuleCat.{u} R)) (1 : ℤ)).obj K))
Tag 065G, a lemma

Tag 065G in the Stacks Project.

PseudoCoherence.isPseudoCoherentFrom_iff_restrictScalars_polynomial_evalZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Polynomial.lean, line 208.

Stacks 065G. An object of D(R) is m-pseudo-coherent over R if and only if, after letting X act by zero, it is m-pseudo-coherent over R[X].

For an object represented by a complex, Functor.mapDerivedCategoryFactors identifies the right-hand object with the localization of that complex after restriction of scalars.

public theorem isPseudoCoherentFrom_iff_restrictScalars_polynomial_evalZero
    {R : Type u} [CommRing R]
    (K : DerivedCategory (ModuleCat.{max u v} R)) (m : ℤ) :
    let ev : Polynomial R →+* R := Polynomial.eval₂RingHom (RingHom.id R) (0 : R)
    IsPseudoCoherentFrom K m ↔
      IsPseudoCoherentFrom
        ((ModuleCat.restrictScalars.{max u v} ev).mapDerivedCategory.obj K) m
Tag 065H, a lemma

Tag 065H in the Stacks Project.

PseudoCoherence.isPseudoCoherentFrom_polynomialPresentation_independent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Presentation.lean, line 224.

Stacks 065H. For a finite-type R-algebra A, m-pseudo-coherence of an object of D(A) after restriction to a finite polynomial presentation is independent of the presentation. The same is true of pseudo-coherence. For an object represented by a complex, Functor.mapDerivedCategoryFactors identifies each restricted object below with the localization of the representing complex after degreewise restriction of scalars.

public theorem isPseudoCoherentFrom_polynomialPresentation_independent
    {R : Type u} {A : Type w} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (K : DerivedCategory (ModuleCat.{max u v} A)) (m : ℤ) :
    ((∃ (n : ℕ) (α : MvPolynomial (Fin n) R →ₐ[R] A), Function.Surjective α ∧
        IsPseudoCoherentFrom
          ((ModuleCat.restrictScalars.{max u v} α.toRingHom).mapDerivedCategory.obj K) m) ↔
      ∀ (n : ℕ) (α : MvPolynomial (Fin n) R →ₐ[R] A), Function.Surjective α →
        IsPseudoCoherentFrom
          ((ModuleCat.restrictScalars.{max u v} α.toRingHom).mapDerivedCategory.obj K) m) ∧
    ((∃ (n : ℕ) (α : MvPolynomial (Fin n) R →ₐ[R] A), Function.Surjective α ∧
        IsPseudoCoherent
          ((ModuleCat.restrictScalars.{max u v} α.toRingHom).mapDerivedCategory.obj K)) ↔
      ∀ (n : ℕ) (α : MvPolynomial (Fin n) R →ₐ[R] A), Function.Surjective α →
        IsPseudoCoherent
          ((ModuleCat.restrictScalars.{max u v} α.toRingHom).mapDerivedCategory.obj K))
Tag 065I, a definition

Tag 065I in the Stacks Project.

PseudoCoherence.IsRelativelyPseudoCoherentFrom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Defs.lean, line 84. The attribute's comment: “(1)”.

Stacks 065I (1). An object of D(A) is m-pseudo-coherent relative to R if its restriction of scalars along every finite polynomial presentation of A over R is m-pseudo-coherent. By Stacks 065H it is equivalent to require this of one presentation.

public def IsRelativelyPseudoCoherentFrom
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (K : DerivedCategory (ModuleCat.{u} A)) (m : ℤ) : Prop

PseudoCoherence.IsRelativelyPseudoCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Defs.lean, line 94. The attribute's comment: “(2)”.

Stacks 065I (2). An object of D(A) is pseudo-coherent relative to R if it is m-pseudo-coherent relative to R for every integer m.

public def IsRelativelyPseudoCoherent
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (K : DerivedCategory (ModuleCat.{u} A)) : Prop

PseudoCoherence.IsModuleRelativelyPseudoCoherentFrom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Defs.lean, line 102. The attribute's comment: “(3)”.

Stacks 065I (3). An A-module is m-pseudo-coherent relative to R if the object concentrated in degree zero that it determines has that property.

public def IsModuleRelativelyPseudoCoherentFrom
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (M : Type u) [AddCommGroup M] [Module A M] (m : ℤ) : Prop

PseudoCoherence.IsModuleRelativelyPseudoCoherent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Defs.lean, line 111. The attribute's comment: “(4)”.

Stacks 065I (4). An A-module is pseudo-coherent relative to R if the object concentrated in degree zero that it determines has that property.

public def IsModuleRelativelyPseudoCoherent
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (M : Type u) [AddCommGroup M] [Module A M] : Prop
Tag 0673, a lemma

Tag 0673 in the Stacks Project.

PseudoCoherence.isRelativelyPseudoCoherentFrom_and_isRelativelyPseudoCoherent_iff_restrictScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Finite.lean, line 237.

Stacks 0673. Restriction of scalars along a finite map of finite-type R-algebras preserves and reflects relative m-pseudo-coherence and relative pseudo-coherence.

public theorem isRelativelyPseudoCoherentFrom_and_isRelativelyPseudoCoherent_iff_restrictScalars
    {R : Type u} {A : Type u} {B : Type u} [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
    [Algebra.FiniteType R A] [Module.Finite A B]
    (K : DerivedCategory (ModuleCat.{u} B)) (m : ℤ) :
    letI : Algebra.FiniteType R B :=
      Algebra.FiniteType.trans (inferInstance : Algebra.FiniteType R A)
        (Module.Finite.finiteType B)
    let Kₐ := (ModuleCat.restrictScalars.{u} (algebraMap A B)).mapDerivedCategory.obj K
    (IsRelativelyPseudoCoherentFrom (R := R) K m ↔
      IsRelativelyPseudoCoherentFrom (R := R) Kₐ m) ∧
    (IsRelativelyPseudoCoherent (R := R) K ↔
      IsRelativelyPseudoCoherent (R := R) Kₐ)
Tag 0674, a lemma

Tag 0674 in the Stacks Project.

PseudoCoherence.isRelativelyPseudoCoherent_of_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Triangle.lean, line 47.

Stacks 0674. Relative pseudo-coherence is preserved around a distinguished triangle, with the indicated shift in the degree bound. Without a degree bound it is a two-out-of-three property.

public theorem isRelativelyPseudoCoherent_of_distinguished
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (m : ℤ)
    (T : Triangle (DerivedCategory (ModuleCat.{u} A)))
    (hT : T ∈ distinguishedTriangles) :
    ((IsRelativelyPseudoCoherentFrom (R := R) T.obj₁ (m + 1) →
        IsRelativelyPseudoCoherentFrom (R := R) T.obj₂ m →
        IsRelativelyPseudoCoherentFrom (R := R) T.obj₃ m) ∧
      (IsRelativelyPseudoCoherentFrom (R := R) T.obj₁ m →
        IsRelativelyPseudoCoherentFrom (R := R) T.obj₃ m →
        IsRelativelyPseudoCoherentFrom (R := R) T.obj₂ m) ∧
      (IsRelativelyPseudoCoherentFrom (R := R) T.obj₂ (m + 1) →
        IsRelativelyPseudoCoherentFrom (R := R) T.obj₃ m →
        IsRelativelyPseudoCoherentFrom (R := R) T.obj₁ (m + 1))) ∧
    ((IsRelativelyPseudoCoherent (R := R) T.obj₁ →
        IsRelativelyPseudoCoherent (R := R) T.obj₂ →
        IsRelativelyPseudoCoherent (R := R) T.obj₃) ∧
      (IsRelativelyPseudoCoherent (R := R) T.obj₁ →
        IsRelativelyPseudoCoherent (R := R) T.obj₃ →
        IsRelativelyPseudoCoherent (R := R) T.obj₂) ∧
      (IsRelativelyPseudoCoherent (R := R) T.obj₂ →
        IsRelativelyPseudoCoherent (R := R) T.obj₃ →
        IsRelativelyPseudoCoherent (R := R) T.obj₁))
Tag 0675, a lemma

Tag 0675 in the Stacks Project.

PseudoCoherence.moduleRelativelyPseudoCoherent_iff_finiteness_and_resolutions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Module.lean, line 197.

Stacks 0675. For a module over a finite-type R-algebra, relative pseudo-coherence in degrees 0, -1, and -d is equivalent respectively to finite generation, relative finite presentation, and the existence over every polynomial presentation of a finite free resolution through degree d. Relative pseudo-coherence is equivalent to the existence over every polynomial presentation of an infinite finite free resolution.

public theorem moduleRelativelyPseudoCoherent_iff_finiteness_and_resolutions
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (M : Type u) [AddCommGroup M] [Module A M] :
    (IsModuleRelativelyPseudoCoherentFrom (R := R) (A := A) M 0 ↔
      Module.Finite A M) ∧
    (IsModuleRelativelyPseudoCoherentFrom (R := R) (A := A) M (-1) ↔
      Module.FinitePresentationRel R A M) ∧
    (∀ d : ℕ, IsModuleRelativelyPseudoCoherentFrom (R := R) (A := A)
      M (-(d : ℤ)) ↔
      ∀ (n : ℕ) (α : MvPolynomial (Fin n) R →ₐ[R] A), Function.Surjective α →
        @HasFiniteFreeResolutionOfLength _ _ M _
          (Module.compHom M α.toRingHom) d) ∧
    (IsModuleRelativelyPseudoCoherent (R := R) (A := A) M ↔
      ∀ (n : ℕ) (α : MvPolynomial (Fin n) R →ₐ[R] A), Function.Surjective α →
        Nonempty (@FiniteFreeModuleResolution _ _ M _
          (Module.compHom M α.toRingHom)))
Tag 0676, a lemma

Tag 0676 in the Stacks Project.

PseudoCoherence.isRelativelyPseudoCoherentFrom_and_isRelativelyPseudoCoherent_of_biproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Summand.lean, line 42.

Each summand of a relatively m-pseudo-coherent binary biproduct is relatively m-pseudo-coherent, and each summand of a relatively pseudo-coherent binary biproduct is relatively pseudo-coherent.

public theorem isRelativelyPseudoCoherentFrom_and_isRelativelyPseudoCoherent_of_biproduct
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (K L : DerivedCategory (ModuleCat.{u} A)) (m : ℤ) :
    (IsRelativelyPseudoCoherentFrom (R := R) (K ⊞ L) m →
      IsRelativelyPseudoCoherentFrom (R := R) K m ∧
        IsRelativelyPseudoCoherentFrom (R := R) L m) ∧
    (IsRelativelyPseudoCoherent (R := R) (K ⊞ L) →
      IsRelativelyPseudoCoherent (R := R) K ∧
        IsRelativelyPseudoCoherent (R := R) L)
Tag 0677, a lemma

Tag 0677 in the Stacks Project.

PseudoCoherence.relativelyPseudoCoherentFrom_and_relativelyPseudoCoherent_of_boundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/BoundedAbove.lean, line 49.

Stacks 0677. A bounded-above complex with suitably relatively pseudo-coherent terms is relatively pseudo-coherent in the corresponding degrees. In particular, relative pseudo-coherence of every term implies relative pseudo-coherence of the complex.

public theorem relativelyPseudoCoherentFrom_and_relativelyPseudoCoherent_of_boundedAbove
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (K : CochainComplex (ModuleCat.{u} A) ℤ)
    (hK : ∃ b : ℤ, K.IsStrictlyLE b) :
    (∀ m : ℤ,
      (∀ i : ℤ, IsModuleRelativelyPseudoCoherentFrom (R := R) (A := A) (K.X i) (m - i)) →
        IsRelativelyPseudoCoherentFrom (R := R) (DerivedCategory.Q.obj K) m) ∧
    ((∀ i : ℤ, IsModuleRelativelyPseudoCoherent (R := R) (A := A) (K.X i)) →
      IsRelativelyPseudoCoherent (R := R) (DerivedCategory.Q.obj K))
Tag 0678, a lemma

Tag 0678 in the Stacks Project.

PseudoCoherence.relativelyPseudoCoherent_of_boundedAbove_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/BoundedAboveCohomology.lean, line 91.

Stacks 0678. A cohomologically bounded-above derived object whose cohomology modules are relatively pseudo-coherent in the corresponding degrees is relatively pseudo-coherent.

public theorem relativelyPseudoCoherent_of_boundedAbove_cohomology
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Algebra.FiniteType R A] (K : DerivedCategory (ModuleCat.{u} A)) (m : ℤ)
    (hK : ∃ b : ℤ, ∀ i : ℤ, b < i →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj K)) :
    ((∀ i : ℤ, IsModuleRelativelyPseudoCoherentFrom (R := R) (A := A)
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj K) (m - i)) →
      IsRelativelyPseudoCoherentFrom (R := R) K m) ∧
    ((∀ i : ℤ, IsModuleRelativelyPseudoCoherent (R := R) (A := A)
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj K)) →
      IsRelativelyPseudoCoherent (R := R) K)
Tag 0679, a lemma

Tag 0679 in the Stacks Project.

PseudoCoherence.localization_preserves_relativePseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Localization.lean, line 510.

Stacks 0679. Localizing a complex that is relatively m-pseudo-coherent, respectively pseudo-coherent, over R_f produces a complex with the corresponding property relative to R.

public theorem localization_preserves_relativePseudoCoherent
    {R : Type u} {Rf : Type u} {A : Type u} {Ag : Type u}
    [CommRing R] [CommRing Rf] [CommRing A] [CommRing Ag]
    [Algebra R Rf] (f : R) [IsLocalization.Away f Rf]
    [Algebra Rf A] [Algebra.FiniteType Rf A]
    [Algebra R A] [IsScalarTower R Rf A]
    (g : A) [Algebra A Ag] [IsLocalization.Away g Ag]
    [Algebra R Ag] [IsScalarTower R A Ag]
    (K : DerivedCategory (ModuleCat.{u} A)) (m : ℤ) :
    letI : Algebra.FiniteType R Rf :=
      IsLocalization.finiteType_of_monoid_fg (Submonoid.powers f) Rf
    letI : Algebra.FiniteType R A := Algebra.FiniteType.trans
      (inferInstance : Algebra.FiniteType R Rf) (inferInstance : Algebra.FiniteType Rf A)
    letI : Algebra.FiniteType A Ag :=
      IsLocalization.finiteType_of_monoid_fg (Submonoid.powers g) Ag
    letI : Algebra.FiniteType R Ag := Algebra.FiniteType.trans
      (inferInstance : Algebra.FiniteType R A) (inferInstance : Algebra.FiniteType A Ag)
    (IsRelativelyPseudoCoherentFrom (R := Rf) K m →
      IsRelativelyPseudoCoherentFrom (R := R)
        ((derivedExtensionScalarsGeneral.{u, u, u} (algebraMap A Ag)).functor.obj K) m) ∧
    (IsRelativelyPseudoCoherent (R := Rf) K →
      IsRelativelyPseudoCoherent (R := R)
        ((derivedExtensionScalarsGeneral.{u, u, u} (algebraMap A Ag)).functor.obj
          K))
Tag 067A, a lemma

Tag 067A in the Stacks Project.

PseudoCoherence.derivedExtensionScalars_preserves_relativelyPseudoCoherent_of_torIndependent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/TorIndependentBaseChange.lean, line 271. References: SGA 6 III (1.10), “a), affine case”; SGA 6 III (1.8), “affine, E₂ = O”; SGA 6 III (4.7), “(a), special case”.

A Tor-independent base change preserves relative m-pseudo-coherence for every integer m, as well as relative pseudo-coherence.

The chosen R'-algebra R' ⊗[R] A is identified with the source's A ⊗[R] R' by Algebra.TensorProduct.commRight R R' A.

public theorem derivedExtensionScalars_preserves_relativelyPseudoCoherent_of_torIndependent
    {R : Type u} {A : Type u} {R' : Type u}
    [CommRing R] [CommRing A] [CommRing R']
    [Algebra R A] [Algebra R R'] [Algebra.FiniteType R A]
    (K : DerivedCategory (ModuleCat.{u} A))
    (hTor : TorIndependent R A R') :
    let A' := R' ⊗[R] A
    letI : Algebra R' A' := Algebra.TensorProduct.leftAlgebra
    let f : A →+* A' := Algebra.TensorProduct.includeRight.toRingHom
    (∀ m : ℤ, IsRelativelyPseudoCoherentFrom (R := R) K m →
      IsRelativelyPseudoCoherentFrom (R := R')
        ((derivedExtensionScalarsGeneral.{u, u, u} f).functor.obj K)
          m) ∧
      (IsRelativelyPseudoCoherent (R := R) K →
        IsRelativelyPseudoCoherent (R := R')
          ((derivedExtensionScalarsGeneral.{u, u, u} f).functor.obj
            K))
Tag 067B, a lemma

Tag 067B in the Stacks Project.

PseudoCoherence.derivedExtensionScalars_preserves_relativelyPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Tower.lean, line 944.

If B is pseudo-coherent relative to A, derived extension of scalars from A to B preserves relative m-pseudo-coherence and relative pseudo-coherence over the base ring R.

public theorem derivedExtensionScalars_preserves_relativelyPseudoCoherent
    {R : Type u} {A : Type u} {B : Type u}
    [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    [Algebra.FiniteType R A] [Algebra.FiniteType A B]
    (K : DerivedCategory (ModuleCat.{u} A)) (m : ℤ)
    (hB : IsModuleRelativelyPseudoCoherent.{u}
      (R := A) (A := B) B) :
    letI : Algebra.FiniteType R B :=
      Algebra.FiniteType.trans (R := R) (S := A) (A := B) inferInstance inferInstance
    (IsRelativelyPseudoCoherentFrom (R := R) K m →
      IsRelativelyPseudoCoherentFrom (R := R)
        ((derivedExtensionScalars hB).obj K) m) ∧
    (IsRelativelyPseudoCoherent (R := R) K →
      IsRelativelyPseudoCoherent (R := R)
        ((derivedExtensionScalars hB).obj K))
Tag 067C, a lemma

Tag 067C in the Stacks Project.

PseudoCoherence.tensorProduct_preserves_relativelyPseudoCoherent_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/TowerModule.lean, line 128.

Flat extension of scalars preserves relative m-pseudo-coherence and relative pseudo-coherence for modules.

public theorem tensorProduct_preserves_relativelyPseudoCoherent_of_flat
    {R : Type u} {A : Type u} {B : Type u}
    [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    [Algebra.FiniteType R A] [Algebra.FiniteType A B]
    (M : Type u) [AddCommGroup M] [Module A M] [Module.Flat A B] (m : ℤ)
    (hB : IsModuleRelativelyPseudoCoherent (R := A) (A := B) B) :
    letI : Algebra.FiniteType R B :=
      Algebra.FiniteType.trans (R := R) (S := A) (A := B) inferInstance inferInstance
    (IsModuleRelativelyPseudoCoherentFrom (R := R) (A := A) M m →
      IsModuleRelativelyPseudoCoherentFrom (R := R) (A := B)
        (TensorProduct A B M) m) ∧
    (IsModuleRelativelyPseudoCoherent (R := R) (A := A) M →
      IsModuleRelativelyPseudoCoherent (R := R) (A := B)
        (TensorProduct A B M))
Tag 067D, a lemma

Tag 067D in the Stacks Project.

PseudoCoherence.relativelyPseudoCoherent_iff_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Composition.lean, line 258. References: SGA 6 I (2.14), “(ii), affine case”.

Stacks 067D. Relative pseudo-coherence is invariant under composition with a relatively pseudo-coherent finite-type algebra, for every object of the derived category.

public theorem relativelyPseudoCoherent_iff_of_comp
    {R : Type u} {A : Type u} {B : Type u}
    [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    [Algebra.FiniteType R A] [Algebra.FiniteType A B]
    (hA : IsModuleRelativelyPseudoCoherent (R := R) (A := A) A)
    (K : DerivedCategory (ModuleCat.{u} B)) (m : ℤ) :
    letI : Algebra.FiniteType R B :=
      Algebra.FiniteType.trans (R := R) (S := A) (A := B) inferInstance inferInstance
    (IsRelativelyPseudoCoherentFrom (R := A) K m ↔
      IsRelativelyPseudoCoherentFrom (R := R) K m) ∧
    (IsRelativelyPseudoCoherent (R := A) K ↔
      IsRelativelyPseudoCoherent (R := R) K)
Tag 067E, a lemma

Tag 067E in the Stacks Project.

PseudoCoherence.relativelyPseudoCoherent_iff_localizationAway_of_span_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Locality.lean, line 563.

Stacks 067E. Relative m-pseudo-coherence and relative pseudo-coherence are local on a finite principal cover of a finite-type algebra.

public theorem relativelyPseudoCoherent_iff_localizationAway_of_span_eq_top
    {R : Type u} {A : Type u} [CommRing R] [CommRing A]
    [Algebra R A] [Algebra.FiniteType R A]
    {ι : Type*} [Finite ι] (f : ι → A) (hf : Ideal.span (Set.range f) = ⊤)
    (K : DerivedCategory (ModuleCat.{u} A)) (m : ℤ) :
    ((∀ i,
      letI : Algebra.FiniteType A (Localization.Away (f i)) :=
        IsLocalization.finiteType_of_monoid_fg (Submonoid.powers (f i)) _
      letI : Algebra.FiniteType R (Localization.Away (f i)) :=
        Algebra.FiniteType.trans (R := R) (S := A)
          (A := Localization.Away (f i)) inferInstance inferInstance
      IsRelativelyPseudoCoherentFrom (R := R)
        ((localizationAwayFunctorAux.{u, u} (f i)).obj K) m) ↔
      IsRelativelyPseudoCoherentFrom (R := R) K m) ∧
    ((∀ i,
      letI : Algebra.FiniteType A (Localization.Away (f i)) :=
        IsLocalization.finiteType_of_monoid_fg (Submonoid.powers (f i)) _
      letI : Algebra.FiniteType R (Localization.Away (f i)) :=
        Algebra.FiniteType.trans (R := R) (S := A)
          (A := Localization.Away (f i)) inferInstance inferInstance
      IsRelativelyPseudoCoherent (R := R)
        ((localizationAwayFunctorAux.{u, u} (f i)).obj K)) ↔
      IsRelativelyPseudoCoherent (R := R) K)
Tag 067F, a lemma

Tag 067F in the Stacks Project.

PseudoCoherence.relativePseudoCoherent_iff_boundedAbove_finite_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/Relative/Noetherian.lean, line 147.

Stacks 067F. For a finite-type algebra over a Noetherian ring, relative pseudo-coherence from degree m means bounded-above finite homology in degrees at least m; relative pseudo-coherence means bounded-above finite homology in every degree; and relative pseudo-coherence of a module is equivalent to its finiteness.

public theorem relativePseudoCoherent_iff_boundedAbove_finite_homology
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [IsNoetherianRing R] [Algebra.FiniteType R A]
    (K : DerivedCategory (ModuleCat.{u} A)) (m : ℤ)
    (M : Type u) [AddCommGroup M] [Module A M] :
    (IsRelativelyPseudoCoherentFrom (R := R) K m ↔
      (∃ b : ℤ, ∀ i : ℤ, b < i →
        IsZero ((DerivedCategory.homologyFunctor
          (ModuleCat.{u} A) i).obj K)) ∧
      ∀ i : ℤ, m ≤ i →
        Module.Finite A ((DerivedCategory.homologyFunctor
          (ModuleCat.{u} A) i).obj K)) ∧
    (IsRelativelyPseudoCoherent (R := R) K ↔
      (∃ b : ℤ, ∀ i : ℤ, b < i →
        IsZero ((DerivedCategory.homologyFunctor
          (ModuleCat.{u} A) i).obj K)) ∧
      ∀ i : ℤ,
        Module.Finite A ((DerivedCategory.homologyFunctor
          (ModuleCat.{u} A) i).obj K)) ∧
    (IsModuleRelativelyPseudoCoherent (R := R) (A := A) M ↔
      Module.Finite A M)
Sources

Section15.84 Pseudo-coherent and perfect ring maps#

Section 15.84 of the Stacks Project, Tag 067G. 8 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 067H, a definition

Tag 067H in the Stacks Project.

Algebra.PseudoCoherent, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/Defs.lean, line 88. The attribute's comment: “(1)”.

An A-algebra B is pseudo-coherent if B is a quotient A[x₁, …, xₙ] ⧸ I of a polynomial algebra such that the A[x₁, …, xₙ]-module A[x₁, …, xₙ] ⧸ I has a resolution by finite free modules.

This is Stacks 067H (1) in the form of the remark that follows it, with B replaced by the isomorphic A[x₁, …, xₙ]-module A[x₁, …, xₙ] ⧸ I, which lives in the universe of A. By Stacks 0675 it says that A → B is of finite type and that B, as a module over itself, is pseudo-coherent relative to A (for A and B in one universe, Algebra.pseudoCoherent_iff_exists_isModuleRelativelyPseudoCoherent). The resolution then exists over every finite polynomial presentation (Algebra.PseudoCoherent.nonempty_finiteFreeModuleResolution). When A and B live in one universe, the condition is the same for B itself, made an A[x₁, …, xₙ]-module through the presentation (Algebra.PseudoCoherent.nonempty_finiteFreeModuleResolution_quotient_iff_compHom).

public class Algebra.PseudoCoherent (A : Type u) (B : Type v) [CommRing A] [CommRing B]
    [Algebra A B] : Prop

RingHom.IsPerfectRingMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/Defs.lean, line 114. The attribute's comment: “(2)”. References: SGA 6 III (4.1), “affine case”.

A ring map A → B is perfect if it is pseudo-coherent and B, regarded as an A-module, has finite Tor dimension, read off the certified derived tensor product derivedTensor on a model of D(A). Neither the model nor the certificate matters (RingHom.isPerfectRingMap_iff_exists_flat_roof).

public def IsPerfectRingMap
    (A : Type u) (B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    [HasDerivedCategory.{w} (ModuleCat.{u} A)]
    (derivedTensor :
      DerivedCategory (ModuleCat.{u} A) ⥤
        DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} A))
    (comparison : ∀ N : ModuleCat.{u} A,
      DerivedCategory.Q ⋙
          derivedTensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N) ⟶
        (StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerived : ∀ N : ModuleCat.{u} A,
      (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N)).IsLeftDerivedFunctor
        (comparison N)
        (HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))) : Prop
Tag 068Y, a lemma

Tag 068Y in the Stacks Project.

RingHom.isPerfectRingMap_iff_exists_finite_projective_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/PerfectPresentation.lean, line 276.

Stacks 068Y. A ring map A → B is perfect if and only if there is a presentation B = A[x_1, …, x_n]/I for which B, as a module over A[x_1, …, x_n], admits a finite resolution by finite projective A[x_1, …, x_n]-modules.

public theorem isPerfectRingMap_iff_exists_finite_projective_resolution
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    (derivedTensor :
      DerivedCategory (ModuleCat.{u} A) ⥤
        DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} A))
    (comparison : ∀ N : ModuleCat.{u} A,
      DerivedCategory.Q ⋙
          derivedTensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N) ⟶
        (StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerived : ∀ N : ModuleCat.{u} A,
      (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N)).IsLeftDerivedFunctor
        (comparison N)
        (HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))) :
    IsPerfectRingMap A B derivedTensor comparison isLeftDerived ↔
      ∃ (n : ℕ) (α : MvPolynomial (Fin n) A →ₐ[A] B), Function.Surjective α ∧
        let : Module (MvPolynomial (Fin n) A) B := Module.compHom B α.toRingHom
        ∃ (d : ℕ) (F : ModuleResolution (MvPolynomial (Fin n) A) B),
          (∀ i : ℕ, Module.Finite (MvPolynomial (Fin n) A) (F.complex.X i) ∧
            Module.Projective (MvPolynomial (Fin n) A) (F.complex.X i)) ∧
          ∀ i : ℕ, d < i → IsZero (F.complex.X i)
Tag 067I, a lemma

Tag 067I in the Stacks Project.

Algebra.PseudoCoherent.of_finiteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/Noetherian.lean, line 38. References: SGA 6 III (1.3), “third example, affine”.

Stacks 067I. A finite-type ring map whose source is Noetherian is pseudo-coherent.

public theorem of_finiteType
    (A : Type u) (B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    [IsNoetherianRing A] [Algebra.FiniteType A B] :
    Algebra.PseudoCoherent A B
Tag 067J, a lemma

Tag 067J in the Stacks Project.

RingHom.isPerfectRingMap_of_flat_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/Flat.lean, line 320.

Stacks 067J. A flat ring map of finite presentation is perfect: it is pseudo-coherent, and its target has finite Tor dimension over its source for every certified derived tensor product.

public theorem isPerfectRingMap_of_flat_of_finitePresentation
    (A : Type u) (B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    [Module.Flat A B] [Algebra.FinitePresentation A B] :
    Algebra.PseudoCoherent A B ∧
    ∀ (derivedTensor : DerivedCategory (ModuleCat.{u} A) ⥤
        DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} A))
      (comparison : ∀ N : ModuleCat.{u} A,
        DerivedCategory.Q ⋙ derivedTensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N) ⟶
          (StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
      (isLeftDerived : ∀ N : ModuleCat.{u} A,
        (derivedTensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N)).IsLeftDerivedFunctor
          (comparison N)
          (HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))),
      IsPerfectRingMap A B derivedTensor comparison isLeftDerived
Tag 067K, a lemma

Tag 067K in the Stacks Project.

RingHom.isPerfectRingMap_of_finiteType_of_isRegularRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/Regular.lean, line 75.

Stacks 067K. A finite-type ring map out of a regular ring is perfect: it is pseudo-coherent, and its target has finite Tor dimension as a module over its source, for every certified derived tensor product.

The source assumes in addition that the regular ring has finite Krull dimension; that hypothesis is not needed, because the bound on the length of the resolution is produced from quasi-compactness of the prime spectrum of the polynomial ring rather than from a bound on its global dimension.

public theorem isPerfectRingMap_of_finiteType_of_isRegularRing
    (A : Type u) (B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    [IsRegularRing A] [Algebra.FiniteType A B]
    (derivedTensor : DerivedCategory (ModuleCat.{u} A) ⥤
      DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} A))
    (comparison : ∀ N : ModuleCat.{u} A,
      DerivedCategory.Q ⋙ derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N) ⟶
        (StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
          (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerived : ∀ N : ModuleCat.{u} A,
      (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N)).IsLeftDerivedFunctor
        (comparison N)
        (HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))) :
    IsPerfectRingMap A B derivedTensor comparison isLeftDerived
Tag 07EN, a lemma

Tag 07EN in the Stacks Project.

RingHom.IsLocalCompleteIntersection.isPerfectRingMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/CompleteIntersection.lean, line 273. References: SGA 6 III (4.1.1), “second part, affine”; SGA 6 VIII (1.7), “affine case”.

Stacks 07EN. A local complete intersection homomorphism is perfect.

public theorem IsLocalCompleteIntersection.isPerfectRingMap
    {A : Type u} {B : Type u} [CommRing A] [CommRing B] (f : A →+* B)
    (h : IsLocalCompleteIntersection f)
    (derivedTensor :
      DerivedCategory (ModuleCat.{u} A) ⥤
        DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} A))
    (comparison : ∀ N : ModuleCat.{u} A,
      DerivedCategory.Q ⋙
          derivedTensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N) ⟶
        (StacksDraft.TorAmplitude.tensorModuleRight N).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerived : ∀ N : ModuleCat.{u} A,
      (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N)).IsLeftDerivedFunctor
        (comparison N)
        (HomologicalComplex.quasiIso (ModuleCat.{u} A) (ComplexShape.up ℤ))) :
    letI := f.toAlgebra
    IsPerfectRingMap A B derivedTensor comparison isLeftDerived
Tag 0DHQ, a lemma

Tag 0DHQ in the Stacks Project.

PseudoCoherence.relativelyPseudoCoherent_iff_pseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/Absolute.lean, line 132.

Stacks 0DHQ. Let R → A be a pseudo-coherent ring map. An object of D(A) is m-pseudo-coherent relative to R exactly when it is m-pseudo-coherent, and it is pseudo-coherent relative to R exactly when it is pseudo-coherent.

public theorem relativelyPseudoCoherent_iff_pseudoCoherent
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    (hRA : Algebra.PseudoCoherent R A)
    (K : DerivedCategory (ModuleCat.{u} A)) (m : ℤ) :
    (IsRelativelyPseudoCoherentFrom (R := R) K m ↔ IsPseudoCoherentFrom K m) ∧
    (IsRelativelyPseudoCoherent (R := R) K ↔ IsPseudoCoherent K)
Tag 0E1T, a lemma

Tag 0E1T in the Stacks Project.

PseudoCoherence.pseudoCoherent_tfae_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/PseudoCoherentMap/Surjection.lean, line 51.

For a surjection B → A of flat, finitely presented R-algebras, absolute pseudo-coherence in D(A), relative pseudo-coherence over R and over A, and the two analogous conditions after restriction of scalars to B are equivalent; the same holds for m-pseudo-coherence.

public theorem pseudoCoherent_tfae_of_surjective
    {R : Type u} {B : Type u} {A : Type u}
    [CommRing R] [CommRing B] [CommRing A]
    [Algebra R B] [Algebra B A] [Algebra R A] [IsScalarTower R B A]
    [Module.Flat R B] [Algebra.FinitePresentation R B]
    [Module.Flat R A] [Algebra.FinitePresentation R A]
    (hsurj : Function.Surjective (algebraMap B A))
    (K : DerivedCategory (ModuleCat.{u} A)) (m : ℤ) :
    let Kₑ := (ModuleCat.restrictScalars.{u} (algebraMap B A)).mapDerivedCategory.obj K
    List.TFAE [
      IsPseudoCoherent K,
      IsRelativelyPseudoCoherent (R := R) K,
      IsRelativelyPseudoCoherent (R := A) K,
      IsPseudoCoherent Kₑ,
      IsRelativelyPseudoCoherent (R := R) Kₑ] ∧
    List.TFAE [
      IsPseudoCoherentFrom K m,
      IsRelativelyPseudoCoherentFrom (R := R) K m,
      IsRelativelyPseudoCoherentFrom (R := A) K m,
      IsPseudoCoherentFrom Kₑ m,
      IsRelativelyPseudoCoherentFrom (R := R) Kₑ m]
Sources

Section15.85 Relatively perfect modules#

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

Tag 0DHS, a definition

Tag 0DHS in the Stacks Project.

PseudoCoherence.IsRelativelyPerfect, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/RelativelyPerfect.lean, line 59. References: SGA 6 III (4.1), “affine, flat f.p. case”.

Stacks 0DHS. For a flat, finitely presented ring map R → A, an object K of D(A) is perfect relative to R if it is pseudo-coherent over A and its restriction of scalars has finite Tor dimension over R.

public def IsRelativelyPerfect
    {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A]
    [Module.Flat R A] [Algebra.FinitePresentation R A]
    (derivedTensor :
      DerivedCategory (ModuleCat.{max u v w} R) ⥤
        DerivedCategory (ModuleCat.{max u v w} R) ⥤ DerivedCategory (ModuleCat.{max u v w} R))
    (comparison : ∀ M : ModuleCat.{max u v w} R,
      DerivedCategory.Q ⋙
          derivedTensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{max u v w} R) 0).obj M) ⟶
        (StacksDraft.TorAmplitude.tensorModuleRight M).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerived : ∀ M : ModuleCat.{max u v w} R,
      (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor
            (ModuleCat.{max u v w} R) 0).obj M)).IsLeftDerivedFunctor
        (comparison M)
        (HomologicalComplex.quasiIso (ModuleCat.{max u v w} R) (ComplexShape.up ℤ)))
    (K : DerivedCategory (ModuleCat.{max u v w} A)) : Prop
Tag 0DHT, a lemma

Tag 0DHT in the Stacks Project.

PseudoCoherence.isClosedUnderIsomorphisms_relativelyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Triangulated.lean, line 267.

For a flat, finitely presented ring map R → A, the objects of D(A) perfect relative to R form a strictly full subcategory: relative perfectness is invariant under isomorphism in D(A).

theorem isClosedUnderIsomorphisms_relativelyPerfect :
    (relativelyPerfect.{u, v, w} (A := A) derivedTensor comparison
      isLeftDerived).IsClosedUnderIsomorphisms

PseudoCoherence.isTriangulated_relativelyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Triangulated.lean, line 299. References: SGA 6 III (4.2), “affine case, flat f.p.”.

For a flat, finitely presented ring map R → A, the objects of D(A) perfect relative to R form a triangulated subcategory: the property contains the zero object, is stable under all shifts, and is closed under extensions.

theorem isTriangulated_relativelyPerfect :
    (relativelyPerfect.{u, v, w} (A := A) derivedTensor comparison
      isLeftDerived).IsTriangulated

PseudoCoherence.isSaturated_relativelyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Triangulated.lean, line 325.

For a flat, finitely presented ring map R → A, the objects of D(A) perfect relative to R form a saturated (thick) subcategory: a direct summand of a relatively perfect object is relatively perfect.

theorem isSaturated_relativelyPerfect :
    (relativelyPerfect.{u, v, w} (A := A) derivedTensor comparison
      isLeftDerived).IsSaturated
Tag 0DHU, a lemma

Tag 0DHU in the Stacks Project.

PseudoCoherence.isRelativelyPerfect_of_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Tensor.lean, line 631.

Stacks 0DHU. For a flat, finitely presented ring map R → A, a perfect object of D(A) is perfect relative to R: a bounded complex of finite projective A-modules representing it is pseudo-coherent by Stacks 064U, and its terms are flat over R by transitivity of flatness, so its restriction to R has finite Tor dimension.

theorem isRelativelyPerfect_of_isPerfect (K : DerivedCategory (ModuleCat.{max u v w} A))
    (hK : StacksDraft.Perfect.IsPerfect K) :
    IsRelativelyPerfect.{u, v, w} derivedTensor comparison isLeftDerived K

PseudoCoherence.isRelativelyPerfect_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Tensor.lean, line 696.

Stacks 0DHU. For a flat, finitely presented ring map R → A, the derived tensor product over A of a perfect object of D(A) with an R-perfect object is R-perfect.

Pseudo-coherence: a bounded-above finite free representative of the perfect object is K-flat, so the derived tensor product is computed by the total tensor product with a bounded-above finite free representative of the R-perfect object, and that has bounded-above finite free terms.

Finite Tor dimension: a bounded finite projective representative of the perfect object is also K-flat, and the R-perfect object has a bounded representative whose terms are flat over R (Stacks 0653); the total tensor product of the two is bounded with terms flat over R.

theorem isRelativelyPerfect_derivedTensor
    (K M : DerivedCategory (ModuleCat.{max u v w} A))
    (hK : StacksDraft.Perfect.IsPerfect K)
    (hM : IsRelativelyPerfect.{u, v, w} derivedTensor comparison isLeftDerived M) :
    IsRelativelyPerfect.{u, v, w} derivedTensor comparison isLeftDerived
      ((derivedTensorA.obj K).obj M)
Tag 0DHV, a lemma

Tag 0DHV in the Stacks Project.

PseudoCoherence.isRelativelyPerfect_iff_exists_bounded_flat_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/FlatComplex.lean, line 356.

Stacks 0DHV. For a flat, finitely presented ring map R → A, an object of D(A) is perfect relative to R if and only if it is isomorphic to a finite complex of A-modules that are flat over R and finitely presented over A.

theorem isRelativelyPerfect_iff_exists_bounded_flat_finitePresentation
    (K : DerivedCategory (ModuleCat.{max u v w} A)) :
    IsRelativelyPerfect.{u, v, w} derivedTensor comparison isLeftDerived K ↔
      ∃ (P : CochainComplex (ModuleCat.{max u v w} A) ℤ) (a b : ℤ),
        P.IsStrictlyGE a ∧ P.IsStrictlyLE b ∧
        (∀ i : ℤ, Module.Flat R
          ((ModuleCat.restrictScalars (algebraMap R A)).obj (P.X i))) ∧
        (∀ i : ℤ, Module.FinitePresentation A (P.X i)) ∧
        Nonempty (K ≅ DerivedCategory.Q.obj P)
Tag 0DHW, a lemma

Tag 0DHW in the Stacks Project.

PseudoCoherence.derivedExtensionScalars_isRelativelyPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/BaseChange.lean, line 121.

Stacks 0DHW. If A is flat and finitely presented over R, then arbitrary base change R → R' sends an R-perfect object of D(A) to an R'-perfect object of D(A ⊗[R] R').

theorem derivedExtensionScalars_isRelativelyPerfect
    {R A R' : Type u} [CommRing R] [CommRing A] [CommRing R']
    [Algebra R A] [Algebra R R'] [Module.Flat R A] [Algebra.FinitePresentation R A]
    (derivedTensorR :
      DerivedCategory (ModuleCat.{u} R) ⥤
        DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
    (comparisonR : ∀ M : ModuleCat.{u} R,
      DerivedCategory.Q ⋙
          derivedTensorR.flip.obj ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj M) ⟶
        (tensorModuleRight M).mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerivedR : ∀ M : ModuleCat.{u} R,
      (derivedTensorR.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj M)).IsLeftDerivedFunctor
        (comparisonR M)
        (HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
    (derivedTensorR' :
      DerivedCategory (ModuleCat.{u} R') ⥤
        DerivedCategory (ModuleCat.{u} R') ⥤ DerivedCategory (ModuleCat.{u} R'))
    (comparisonR' : ∀ M : ModuleCat.{u} R',
      DerivedCategory.Q ⋙
          derivedTensorR'.flip.obj ((DerivedCategory.singleFunctor (ModuleCat.{u} R') 0).obj M) ⟶
        (tensorModuleRight M).mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerivedR' : ∀ M : ModuleCat.{u} R',
      (derivedTensorR'.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R') 0).obj M)).IsLeftDerivedFunctor
        (comparisonR' M)
        (HomologicalComplex.quasiIso (ModuleCat.{u} R') (ComplexShape.up ℤ)))
    (K : DerivedCategory (ModuleCat.{u} A))
    (hK : IsRelativelyPerfect.{u, u, u} derivedTensorR comparisonR isLeftDerivedR K) :
    let A' := A ⊗[R] R'
    letI : Algebra R' A' := Algebra.TensorProduct.rightAlgebra
    let e : (R' ⊗[R] A) ≃ₐ[R'] A' :=
      AlgEquiv.ofRingEquiv (f := (Algebra.TensorProduct.comm R R' A).toRingEquiv)
        (fun r' => by
          change (Algebra.TensorProduct.comm R R' A)
            (algebraMap R' (R' ⊗[R] A) r') = _
          rw [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self_apply,
            Algebra.TensorProduct.comm_tmul]
          rfl)
    letI : Module.Flat R' A' := Module.Flat.of_linearEquiv e.symm.toLinearEquiv
    letI : Algebra.FinitePresentation R' A' := Algebra.FinitePresentation.equiv e
    let f : A →+* A' := Algebra.TensorProduct.includeLeftRingHom
    IsRelativelyPerfect.{u, u, u} derivedTensorR' comparisonR' isLeftDerivedR'
      ((totalDerivedExtensionScalars.{u, u, u} f).functor.obj K)
Tag 0E1U, a lemma

Tag 0E1U in the Stacks Project.

StacksDraft.RelativelyPerfect.exists_homComplex_representation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Representative.lean, line 576.

Stacks 0E1U. For a flat map R → A, a pseudo-coherent complex K and a complex L of finite Tor-dimension over R admit representatives P and F for which Homᴬ(P, F) is a bounded-below complex of R-flat A-modules computing derived Hom. The construction commutes with every base change R → R'. If A is finitely presented over R and L is perfect relative to R, the terms of F and of the Hom complex may moreover be chosen finitely presented over A.

public theorem exists_homComplex_representation
    (R : Type uR) (A : Type uA) [CommRing R] [CommRing A] [Algebra R A] [Module.Flat R A]
    (K L : CochainComplex (ModuleCat.{max uR uA uM} A) ℤ) :
    letI : HasDerivedCategory (ModuleCat.{max uR uA uM} R) :=
      HasDerivedCategory.standard (ModuleCat.{max uR uA uM} R)
    letI : HasDerivedCategory (ModuleCat.{max uR uA uM} A) :=
      HasDerivedCategory.standard (ModuleCat.{max uR uA uM} A)
    (∀ m : ℤ, IsPseudoCoherentFrom ((DerivedCategory.Q).obj K) m) →
    (∃ a b : ℤ,
      StacksDraft.TorAmplitude.FaithfullyFlat.HasTorAmplitude
        (((ModuleCat.restrictScalars
          ((algebraMap R A).comp
            (ULift.ringEquiv : ULift.{max uA uM} R ≃+* R).toRingHom)).mapHomologicalComplex
              (.up ℤ)).obj L)
        a b) →
    ∃ (P F : CochainComplex (ModuleCat.{max uR uA uM} A) ℤ)
      (_eP : (DerivedCategory.Q).obj P ≅ (DerivedCategory.Q).obj K)
      (_eF : (DerivedCategory.Q).obj F ≅ (DerivedCategory.Q).obj L),
      (∃ d : ℤ, P.IsStrictlyLE d) ∧
      (∀ i : ℤ, Module.Finite A (P.X i) ∧ Module.Free A (P.X i)) ∧
      (∃ a b : ℤ, F.IsStrictlyGE a ∧ F.IsStrictlyLE b) ∧
      (∀ i : ℤ, Module.Flat R
        ((ModuleCat.restrictScalars (algebraMap R A)).obj (F.X i))) ∧
      (∃ c : ℤ, (CochainComplex.HomComplexR A P F).IsStrictlyGE c) ∧
      (∀ i : ℤ, Module.Flat R
        ((ModuleCat.restrictScalars (algebraMap R A)).obj
          ((CochainComplex.HomComplexR A P F).X i))) ∧
      (∀ n : ℤ, Function.Bijective
        (fun (z : CochainComplex.HomComplex.CohomologyClass P F n) ↦
          DerivedCategory.Qh.map
            (CochainComplex.HomComplex.CohomologyClass.homAddEquiv z))) ∧
      (∀ (R' : Type uB) [CommRing R'] [Algebra R R'],
        let A' := A ⊗[R] R'
        let f : A →+* A' := Algebra.TensorProduct.includeLeftRingHom
        let Ext := (ModuleCat.extendScalars.{uA, max uA uB, max uR uA uM} f).mapHomologicalComplex
          (ComplexShape.up ℤ)
        let P' := Ext.obj P
        let F' := Ext.obj F
        let E' := Ext.obj (CochainComplex.HomComplexR A P F)
        letI : HasDerivedCategory (ModuleCat.{max uR uA uM uB} A') :=
          HasDerivedCategory.standard (ModuleCat.{max uR uA uM uB} A')
        ∃! e : E' ≅ CochainComplex.HomComplexR A' P' F',
          IsCanonicalHomComplexBaseChangeIso f P F e ∧
            ∀ n : ℤ,
              IsIso (HomologicalComplex.homologyMap e.hom n) ∧
                Function.Bijective
                  (fun (z : CochainComplex.HomComplex.CohomologyClass P' F' n) ↦
                    DerivedCategory.Qh.map
                      (CochainComplex.HomComplex.CohomologyClass.homAddEquiv z))) ∧
      (Algebra.FinitePresentation R A →
        (∀ m : ℤ, IsPseudoCoherentFrom (DerivedCategory.Q.obj L) m) →
        (∀ i : ℤ, Module.FinitePresentation A (F.X i)) ∧
          ∀ n : ℤ,
            Module.FinitePresentation A ((CochainComplex.HomComplexR A P F).X n))
Tag 0DHX, a lemma

Tag 0DHX in the Stacks Project.

PseudoCoherence.relativelyPerfectComplexes_filteredColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Colimit/FilteredColimit.lean, line 439.

Relatively perfect complexes descend through filtered colimits, derived Hom from a pseudo-coherent complex to a complex of finite Tor-dimension commutes with such a colimit, and the category of relatively perfect complexes over the limit is the categorical colimit of the categories at the stages.

public theorem relativelyPerfectComplexes_filteredColimit
    {R₀ : Type uR} [CommRing R₀]
    {I : Type uI} [Category.{uJ} I] [IsFiltered I]
    (F : I ⥤ CommAlgCat.{uR} R₀) (c : Cocone F)
    (hc : IsColimit ((CommAlgCat.uliftFunctor.{max uI uJ, uR, uR} R₀).mapCocone c))
    (A₀ : Type uA) [CommRing A₀] [Algebra R₀ A₀]
    [Module.Flat R₀ A₀] [Algebra.FinitePresentation R₀ A₀]
    (D₀ : DerivedTensoringDatum.{uR, max uR uA uM} R₀)
    (D : ∀ i : I, DerivedTensoringDatum.{uR, max uR uA uM} (F.obj i))
    (Dlim : DerivedTensoringDatum.{uR, max uR uA uM} c.pt) :
    let E := fun {A B : Type (max uR uA)} [CommRing A] [CommRing B] (f : A →+* B) ↦
      totalDerivedExtensionScalars.{max uR uA, max uR uA, uM} f
    let liftBase : ULift.{uR} A₀ →+* A₀ := ULift.ringEquiv.toRingHom
    let W := (ModuleCat.restrictScalars.{max uR uA uM} liftBase).mapDerivedCategory
    let b := fun i : I ↦ (baseToStageMap F A₀ i).comp liftBase
    let blim := (baseToLimitMap c A₀).comp liftBase
    let B := fun i : I ↦ W ⋙ (E (b i)).functor
    let Blim := W ⋙ (E blim).functor
    let S := fun (i : I) ↦ E (stageToLimitMap c A₀ i)
    let P : ∀ i : I, ObjectProperty
        (DerivedCategory (ModuleCat.{max uR uA uM} (stageAlgebra F A₀ i))) := fun i K ↦
      IsRelativelyPerfect.{uR, max uR uA, uM}
        (D i).tensor (D i).comparison (D i).isLeftDerived K
    let Plim : ObjectProperty
        (DerivedCategory (ModuleCat.{max uR uA uM} (c.pt ⊗[R₀] A₀))) := fun K ↦
      IsRelativelyPerfect.{uR, max uR uA, uM}
        Dlim.tensor Dlim.comparison Dlim.isLeftDerived K
    ∃ (comp : ∀ {A B C : Type (max uR uA)} [CommRing A] [CommRing B] [CommRing C]
          (f : A →+* B) (g : B →+* C),
          (E f).functor ⋙ (E g).functor ≅ (E (g.comp f)).functor)
      (unit : ∀ (A : Type (max uR uA)) [CommRing A],
        𝟭 (DerivedCategory (ModuleCat.{max uR uA uM} A)) ≅ (E (RingHom.id A)).functor),
      (∀ {A B C : Type (max uR uA)} [CommRing A] [CommRing B] [CommRing C]
          (f : A →+* B) (g : B →+* C)
          (Q : CochainComplex (ModuleCat.{max uR uA uM} A) ℤ),
        letI : (ModuleCat.extendScalars.{max uR uA, max uR uA, max uR uA uM} f).IsLeftAdjoint :=
          (ModuleCat.extendRestrictScalarsAdj.{max uR uA uM, max uR uA, max uR uA}
            f).isLeftAdjoint
        (E g).functor.map ((E f).comparison.app Q) ≫
            (E g).comparison.app
              (((ModuleCat.extendScalars.{max uR uA, max uR uA, max uR uA uM}
                f).mapHomologicalComplex
                (ComplexShape.up ℤ)).obj Q) ≫
            (extensionOfScalarsComplexComp.{max uR uA, uM} f g).inv.app Q =
          (comp f g).hom.app (DerivedCategory.Q.obj Q) ≫
            (E (g.comp f)).comparison.app Q) ∧
      (∀ {A B C D' : Type (max uR uA)} [CommRing A] [CommRing B] [CommRing C] [CommRing D']
          (f : A →+* B) (g : B →+* C) (h : C →+* D')
          (X : DerivedCategory (ModuleCat.{max uR uA uM} A)),
        (E h).functor.map ((comp f g).hom.app X) ≫ (comp (g.comp f) h).hom.app X =
          (comp g h).hom.app ((E f).functor.obj X) ≫
            (comp f (h.comp g)).hom.app X) ∧
      (∀ {A B : Type (max uR uA)} [CommRing A] [CommRing B] (f : A →+* B)
          (X : DerivedCategory (ModuleCat.{max uR uA uM} A)),
        (E f).functor.map ((unit A).hom.app X) ≫
            (comp (RingHom.id A) f).hom.app X = 𝟙 _) ∧
      (∀ {A B : Type (max uR uA)} [CommRing A] [CommRing B] (f : A →+* B)
          (X : DerivedCategory (ModuleCat.{max uR uA uM} A)),
        (unit B).hom.app ((E f).functor.obj X) ≫
            (comp f (RingHom.id B)).hom.app X = 𝟙 _) ∧
      (∀ (K : DerivedCategory (ModuleCat.{max uR uA uM} (c.pt ⊗[R₀] A₀))), Plim K →
        ∃ (i : I) (Kᵢ : DerivedCategory (ModuleCat.{max uR uA uM} (stageAlgebra F A₀ i))),
          P i Kᵢ ∧ Nonempty ((S i).functor.obj Kᵢ ≅ K)) ∧
      (∀ (K₀ L₀ : DerivedCategory (ModuleCat.{max uR uA uM} A₀)),
        StacksDraft.PseudoCoherence.IsPseudoCoherent K₀ →
        HasFiniteTorDimension D₀.tensor D₀.comparison D₀.isLeftDerived
            ((ModuleCat.restrictScalars (algebraMap R₀ A₀)).mapDerivedCategory.obj L₀) →
        ∃ (H : I ⥤ Type (max uI uJ (max uR uA uM + 1)))
          (eH : ∀ i : I, H.obj i ≃ ((B i).obj K₀ ⟶ (B i).obj L₀))
          (s : Cocone H)
          (eTarget : s.pt ≃ (Blim.obj K₀ ⟶ Blim.obj L₀))
          (_hs : IsColimit s),
          (∀ {i j : I} (f : i ⟶ j) (x : H.obj i),
            let h : (stageMap F A₀ f).comp (b i) =
                b j := by
              ext a
              simp [b, liftBase, stageMap, baseToStageMap, Algebra.TensorProduct.includeRight_apply,
                Algebra.TensorProduct.map_tmul]
            let stageComp := comp (b i) (stageMap F A₀ f) ≪≫
              derivedExtensionScalarsCongr.{max uR uA, uM} h
            eH j (H.map f x) =
              stageComp.inv.app (W.obj K₀) ≫ (E (stageMap F A₀ f)).functor.map (eH i x) ≫
                stageComp.hom.app (W.obj L₀)) ∧
          (∀ (i : I) (g : (B i).obj K₀ ⟶ (B i).obj L₀),
            let h : (stageToLimitMap c A₀ i).comp (b i) =
                blim := by
              ext a
              simp [b, blim, liftBase, stageToLimitMap, baseToStageMap, baseToLimitMap,
                Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.map_tmul]
            let limitComp := comp (b i) (stageToLimitMap c A₀ i) ≪≫
              derivedExtensionScalarsCongr.{max uR uA, uM} h
            eTarget (s.ι.app i ((eH i).symm g)) =
              limitComp.inv.app (W.obj K₀) ≫ (S i).functor.map g ≫ limitComp.hom.app (W.obj L₀))) ∧
      (∀ i : I, (P i).IsTriangulated) ∧ Plim.IsTriangulated ∧
      ∃ (G : I ⥤ Cat.{max uI uJ (max uR uA uM + 1), max uI uJ (max uR uA uM + 1)})
        (eG : ∀ i : I, G.obj i ≌ (P i).FullSubcategory)
        (transition : ∀ {i j : I} (f : i ⟶ j),
          (eG i).inverse ⋙ (G.map f).toFunctor ⋙ (eG j).functor ⋙
              ObjectProperty.ι (P j) ≅
            ObjectProperty.ι (P i) ⋙ (E (stageMap F A₀ f)).functor)
        (_transition_id : ∀ (i : I) (X : (P i).FullSubcategory),
          let mapIdIso : (G.map (𝟙 i)).toFunctor ≅ 𝟭 (G.obj i) :=
            eqToIso (congrArg Cat.Hom.toFunctor (G.map_id i))
          let h : RingHom.id (stageAlgebra F A₀ i) = stageMap F A₀ (𝟙 i) := by
            ext <;> simp [stageMap]
          ((eG i).functor ⋙ ObjectProperty.ι (P i)).map
                (mapIdIso.hom.app ((eG i).inverse.obj X)) ≫
              (ObjectProperty.ι (P i)).map ((eG i).counitIso.hom.app X) ≫
              (unit (stageAlgebra F A₀ i)).hom.app ((ObjectProperty.ι (P i)).obj X) ≫
              (derivedExtensionScalarsCongr.{max uR uA, uM} h).hom.app
                ((ObjectProperty.ι (P i)).obj X) =
            (transition (𝟙 i)).hom.app X)
        (_transition_comp : ∀ {i j k : I} (f : i ⟶ j) (g : j ⟶ k)
            (X : (P i).FullSubcategory),
          let mapCompIso : (G.map (f ≫ g)).toFunctor ≅
              (G.map f).toFunctor ⋙ (G.map g).toFunctor :=
            eqToIso (congrArg Cat.Hom.toFunctor (G.map_comp f g))
          let h : (stageMap F A₀ g).comp (stageMap F A₀ f) =
              stageMap F A₀ (f ≫ g) := by
            ext <;> simp [stageMap, Algebra.TensorProduct.map_tmul]
          let Z := (eG i).inverse.obj X
          let Y := (eG j).functor.obj ((G.map f).toFunctor.obj Z)
          ((eG k).functor ⋙ ObjectProperty.ι (P k)).map (mapCompIso.hom.app Z) ≫
              ((eG k).functor ⋙ ObjectProperty.ι (P k)).map
                ((G.map g).toFunctor.map
                  ((eG j).unitIso.hom.app ((G.map f).toFunctor.obj Z))) ≫
              (transition g).hom.app Y ≫
              (E (stageMap F A₀ g)).functor.map ((transition f).hom.app X) ≫
              (comp (stageMap F A₀ f) (stageMap F A₀ g)).hom.app
                ((ObjectProperty.ι (P i)).obj X) ≫
              (derivedExtensionScalarsCongr.{max uR uA, uM} h).hom.app
                ((ObjectProperty.ι (P i)).obj X) =
            (transition (f ≫ g)).hom.app X)
        (sG : Cocone G) (_hsG : IsColimit sG)
        (eLimit : sG.pt ≌ Plim.FullSubcategory)
        (leg : ∀ i : I,
          (eG i).inverse ⋙ (sG.ι.app i).toFunctor ⋙ eLimit.functor ⋙
                ObjectProperty.ι Plim ≅
            ObjectProperty.ι (P i) ⋙ (S i).functor),
        ∀ {i j : I} (f : i ⟶ j) (X : (P i).FullSubcategory),
          let mapCoconeIso : (G.map f).toFunctor ⋙ (sG.ι.app j).toFunctor ≅
              (sG.ι.app i).toFunctor :=
            eqToIso (congrArg Cat.Hom.toFunctor (sG.w f))
          let h : (stageToLimitMap c A₀ j).comp (stageMap F A₀ f) =
              stageToLimitMap c A₀ i := by
            ext x
            · simp [stageToLimitMap, stageMap]
            · simp [stageToLimitMap, stageMap]
          let limitComp := comp (stageMap F A₀ f) (stageToLimitMap c A₀ j) ≪≫
            derivedExtensionScalarsCongr.{max uR uA, uM} h
          let Z := (eG i).inverse.obj X
          let Y := (eG j).functor.obj ((G.map f).toFunctor.obj Z)
          ((eLimit.functor ⋙ ObjectProperty.ι Plim).map (mapCoconeIso.hom.app Z)) ≫
                (leg i).hom.app X =
            (((sG.ι.app j).toFunctor ⋙ eLimit.functor ⋙ ObjectProperty.ι Plim).map
                ((eG j).unitIso.hom.app ((G.map f).toFunctor.obj Z))) ≫
              (leg j).hom.app Y ≫
              (S j).functor.map ((transition f).hom.app X) ≫
              limitComp.hom.app ((ObjectProperty.ι (P i)).obj X)
Tag 0DJG, a lemma

Tag 0DJG in the Stacks Project.

PseudoCoherence.isRelativelyPerfect_of_derivedExtensionScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Nilpotent.lean, line 206.

Stacks 0DJG. Let R' → A' be a flat ring map of finite presentation, let R' → R be a surjective ring map whose kernel is a nilpotent ideal and set A = A' ⊗[R'] R. If the derived extension of scalars of K' ∈ D(A') to A is perfect relative to R, then K' is perfect relative to R'.

theorem isRelativelyPerfect_of_derivedExtensionScalars
    {R' A' R : Type u} [CommRing R'] [CommRing A'] [CommRing R]
    [Algebra R' A'] [Algebra R' R] [Module.Flat R' A']
    [Algebra.FinitePresentation R' A']
    (hsurj : Function.Surjective (algebraMap R' R))
    (hnil : IsNilpotent (RingHom.ker (algebraMap R' R)))
    (derivedTensorR' :
      DerivedCategory (ModuleCat.{u} R') ⥤
        DerivedCategory (ModuleCat.{u} R') ⥤ DerivedCategory (ModuleCat.{u} R'))
    (comparisonR' : ∀ M : ModuleCat.{u} R',
      DerivedCategory.Q ⋙
          derivedTensorR'.flip.obj ((DerivedCategory.singleFunctor (ModuleCat.{u} R') 0).obj M) ⟶
        (tensorModuleRight M).mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerivedR' : ∀ M : ModuleCat.{u} R',
      (derivedTensorR'.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R') 0).obj M)).IsLeftDerivedFunctor
        (comparisonR' M)
        (HomologicalComplex.quasiIso (ModuleCat.{u} R') (ComplexShape.up ℤ)))
    (derivedTensorR :
      DerivedCategory (ModuleCat.{u} R) ⥤
        DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
    (comparisonR : ∀ M : ModuleCat.{u} R,
      DerivedCategory.Q ⋙
          derivedTensorR.flip.obj ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj M) ⟶
        (tensorModuleRight M).mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerivedR : ∀ M : ModuleCat.{u} R,
      (derivedTensorR.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj M)).IsLeftDerivedFunctor
        (comparisonR M)
        (HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
    (K' : DerivedCategory (ModuleCat.{u} A')) :
    let A := A' ⊗[R'] R
    let e : (R ⊗[R'] A') ≃ₐ[R] A :=
      AlgEquiv.ofRingEquiv (f := (Algebra.TensorProduct.comm R' R A').toRingEquiv)
        (fun r => by
          change (Algebra.TensorProduct.comm R' R A')
            (algebraMap R (R ⊗[R'] A') r) = _
          rw [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self_apply,
            Algebra.TensorProduct.comm_tmul]
          rfl)
    letI : Module.Flat R A := Module.Flat.of_linearEquiv e.symm.toLinearEquiv
    letI : Algebra.FinitePresentation R A := Algebra.FinitePresentation.equiv e
    let f : A' →+* A := Algebra.TensorProduct.includeLeftRingHom
    IsRelativelyPerfect.{u, u, u} derivedTensorR comparisonR isLeftDerivedR
        ((totalDerivedExtensionScalars.{u, u, u} f).functor.obj K') →
      IsRelativelyPerfect.{u, u, u} derivedTensorR' comparisonR' isLeftDerivedR' K'
Tag 0DJH, a lemma

Tag 0DJH in the Stacks Project.

PseudoCoherence.hasTorAmplitude_localization_of_isZero_homology_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Fibrewise.lean, line 334.

Stacks 0DJH. Let A be flat and of finite presentation over R, presented by d variables, let q ⊂ A be a prime lying over p ⊂ R and let K ∈ D(A) be pseudo-coherent. If the cohomology of K_q ⊗ᴸ_{R_p} κ(p) vanishes outside [a, b], then K_q has Tor amplitude in [a - d, b] over R.

theorem hasTorAmplitude_localization_of_isZero_homology_fibre
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Module.Flat R A] [Algebra.FinitePresentation R A]
    (d : ℕ) (presentation : MvPolynomial (Fin d) R →ₐ[R] A)
    (hpresentation : Function.Surjective presentation)
    (q : Ideal A) [q.IsPrime]
    (derivedTensor :
      DerivedCategory (ModuleCat.{u} R) ⥤
        DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
    (comparison : ∀ N : ModuleCat.{u} R,
      DerivedCategory.Q ⋙
          derivedTensor.flip.obj ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N) ⟶
        (tensorModuleRight N).mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerived : ∀ N : ModuleCat.{u} R,
      (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)).IsLeftDerivedFunctor
        (comparison N) (HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
    (fibreTensor :
      DerivedCategory (ModuleCat.{u} (Localization.AtPrime (q.under R))) ⥤
        DerivedCategory (ModuleCat.{u} (Localization.AtPrime (q.under R))) ⥤
          DerivedCategory (ModuleCat.{u} (Localization.AtPrime (q.under R))))
    (fibreComparison : ∀ N : ModuleCat.{u} (Localization.AtPrime (q.under R)),
      DerivedCategory.Q ⋙
          fibreTensor.flip.obj
            ((DerivedCategory.singleFunctor
              (ModuleCat.{u} (Localization.AtPrime (q.under R))) 0).obj N) ⟶
        (tensorModuleRight N).mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (fibreIsLeftDerived : ∀ N : ModuleCat.{u} (Localization.AtPrime (q.under R)),
      (fibreTensor.flip.obj
          ((DerivedCategory.singleFunctor
            (ModuleCat.{u} (Localization.AtPrime (q.under R))) 0).obj N)).IsLeftDerivedFunctor
        (fibreComparison N)
        (HomologicalComplex.quasiIso
          (ModuleCat.{u} (Localization.AtPrime (q.under R))) (ComplexShape.up ℤ)))
    (K : DerivedCategory (ModuleCat.{u} A))
    (hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K) (a b : ℤ)
    (hfibre : ∀ i : ℤ, i < a ∨ b < i →
      IsZero ((DerivedCategory.homologyFunctor
        (ModuleCat.{u} (Localization.AtPrime (q.under R))) i).obj
        ((fibreTensor.obj
          ((ModuleCat.restrictScalars
            (algebraMap (Localization.AtPrime (q.under R))
              (Localization.AtPrime q))).mapDerivedCategory.obj
            ((totalDerivedExtensionScalars
              (algebraMap A (Localization.AtPrime q))).functor.obj K))).obj
          ((DerivedCategory.singleFunctor
            (ModuleCat.{u} (Localization.AtPrime (q.under R))) 0).obj
              (ModuleCat.of (Localization.AtPrime (q.under R))
                (q.under R).ResidueField))))) :
    HasTorAmplitude derivedTensor comparison isLeftDerived
      ((ModuleCat.restrictScalars
        ((algebraMap A (Localization.AtPrime q)).comp
          (algebraMap R A))).mapDerivedCategory.obj
        ((totalDerivedExtensionScalars
          (algebraMap A (Localization.AtPrime q))).functor.obj K))
      (a - (d : ℤ)) b
Tag 0GHJ, a lemma

Tag 0GHJ in the Stacks Project.

PseudoCoherence.isRelativelyPerfect_iff_isBoundedBelow_and_fibres_isBoundedBelow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/RelativelyPerfect/Criterion.lean, line 606.

Stacks 0GHJ. Let R → A be a flat ring map of finite presentation and let K be a pseudo-coherent object of D(A). Then K is perfect relative to R if and only if K is bounded below and, for every prime p of R, the derived fibre K ⊗_R^L κ(p) is bounded below.

theorem isRelativelyPerfect_iff_isBoundedBelow_and_fibres_isBoundedBelow
    {R : Type u} {A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [Module.Flat R A] [Algebra.FinitePresentation R A]
    (derivedTensor :
      DerivedCategory (ModuleCat.{u} R) ⥤
        DerivedCategory (ModuleCat.{u} R) ⥤ DerivedCategory (ModuleCat.{u} R))
    (comparison : ∀ M : ModuleCat.{u} R,
      DerivedCategory.Q ⋙
          derivedTensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj M) ⟶
        (StacksDraft.TorAmplitude.tensorModuleRight M).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerived : ∀ M : ModuleCat.{u} R,
      (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj M)).IsLeftDerivedFunctor
        (comparison M)
        (HomologicalComplex.quasiIso (ModuleCat.{u} R) (ComplexShape.up ℤ)))
    (K : DerivedCategory (ModuleCat.{u} A))
    (hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K) :
    IsRelativelyPerfect.{u, u, u} derivedTensor comparison isLeftDerived K ↔
      (∃ a : ℤ, K.IsGE a) ∧
        ∀ p : PrimeSpectrum R, ∃ a : ℤ,
          ((CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, u}
              (algebraMap R p.asIdeal.ResidueField)).functor.obj
            ((ModuleCat.restrictScalars (algebraMap R A)).mapDerivedCategory.obj K)).IsGE a
Sources

Section15.86 Two term complexes#

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

Tag 0G9C, a lemma

Tag 0G9C in the Stacks Project.

TwoTermComplex.projective_homology_iff_ext_one_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/ProjectiveCohomology.lean, line 155.

Stacks 0G9C. For a derived object with cohomology concentrated in degrees -1 and 0, vanishing of degree-one Ext against every module is equivalent to vanishing of degree-minus-one cohomology and projectivity of zero-th cohomology. If the ring is Noetherian and these two cohomology modules are finite, the same condition can be tested on finite modules.

public theorem projective_homology_iff_ext_one_vanishing
    {R : Type u} [CommRing R] [Small.{v} R]
    (K : DerivedCategory (ModuleCat.{v} R))
    (hK : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj K)) :
    let moduleObject := fun N : ModuleCat.{v} R ↦
      (DerivedCategory.singleFunctor (ModuleCat.{v} R) 0).obj N
    let projectiveHomology :=
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) (-1)).obj K) ∧
        Module.Projective R
          ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) 0).obj K)
    let extVanishes := ∀ N : ModuleCat.{v} R,
      Subsingleton (DerivedCategory.Ext K (moduleObject N) 1)
    let finiteExtVanishes := ∀ N : ModuleCat.{v} R, Module.Finite R N →
      Subsingleton (DerivedCategory.Ext K (moduleObject N) 1)
    (projectiveHomology ↔ extVanishes) ∧
      (IsNoetherianRing R →
        Module.Finite R
          ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) (-1)).obj K) →
        Module.Finite R
          ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) 0).obj K) →
        (projectiveHomology ↔ finiteExtVanishes))
Tag 0G9D, a remark

Tag 0G9D in the Stacks Project.

TwoTermComplex.smooth_and_formallySmooth_iff_ext_one_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/ProjectiveCohomology.lean, line 358.

Stacks 0G9D. A ring map is smooth if and only if it is of finite presentation and degree-one Ext from its naive cotangent complex to every module vanishes. It is formally smooth if and only if the same Ext groups vanish, without a finite-presentation condition.

public theorem smooth_and_formallySmooth_iff_ext_one_vanishing
    {R : Type u'} {S : Type v'} [CommRing R] [CommRing S] (f : R →+* S) :
    letI := f.toAlgebra
    let naiveCotangentObject : DerivedCategory (ModuleCat.{max u' v'} S) :=
      DerivedCategory.Q.obj
        (HomologicalComplex.double
          (ModuleCat.ofHom (Algebra.Generators.self R S).toExtension.cotangentComplex)
          (show (ComplexShape.up ℤ).Rel (-1) 0 from rfl))
    let extOneVanishes := ∀ N : ModuleCat.{max u' v'} S,
      Subsingleton
        (DerivedCategory.Ext naiveCotangentObject
          ((DerivedCategory.singleFunctor (ModuleCat.{max u' v'} S) 0).obj N) 1)
    (f.Smooth ↔ f.FinitePresentation ∧ extOneVanishes) ∧
      (f.FormallySmooth ↔ extOneVanishes)
Tag 0G9E, a lemma

Tag 0G9E in the Stacks Project.

TwoTermComplex.exists_twoTerm_representative_free_zero_and_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/Representative.lean, line 111.

Stacks 0G9E. A derived object with cohomology only in degrees -1 and 0 has a two-term representative whose degree-zero term is free. If the ring is Noetherian and both cohomology modules are finite, it also has such a representative with finite degree-minus-one term and finite free degree-zero term.

public theorem exists_twoTerm_representative_free_zero_and_finite
    {R : Type u} [Ring R] [Small.{v} R]
    (K : DerivedCategory (ModuleCat.{v} R))
    (hK : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj K)) :
    (∃ L : CochainComplex (ModuleCat.{v} R) ℤ,
      L.IsStrictlyGE (-1) ∧ L.IsStrictlyLE 0 ∧
        Module.Free R (L.X 0) ∧ Nonempty (DerivedCategory.Q.obj L ≅ K)) ∧
    (IsNoetherianRing R →
      Module.Finite R
          ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) (-1)).obj K) →
      Module.Finite R
          ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) 0).obj K) →
      ∃ L : CochainComplex (ModuleCat.{v} R) ℤ,
        L.IsStrictlyGE (-1) ∧ L.IsStrictlyLE 0 ∧
          Module.Finite R (L.X (-1)) ∧ Module.Finite R (L.X 0) ∧
            Module.Free R (L.X 0) ∧ Nonempty (DerivedCategory.Q.obj L ≅ K))
Tag 0ALN, a lemma

Tag 0ALN in the Stacks Project.

TwoTermComplexExt.exists_hom_Q_map_eq_of_comp_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/Ext/ChainRepresentative.lean, line 441. The attribute's comment: “(3)”.

(3) Assume K^i = 0 for i ≤ -3. Let α ∈ Hom_{D(R)}(M, K). Suppose the composite of α with the canonical map K → K^{-2}[2], viewed in Hom_{D(R)}(M, K^{-2}[2]) = Ext^2(M, K^{-2}), comes from an R-module homomorphism a : M^{-2} → K^{-2} with a ∘ d_M^{-3} = 0 (i.e. equals the D(R)-morphism induced by the chain map M → (single (-2)).obj (K^{-2}) determined by a). Then α is represented by a morphism of complexes a^• : M → K with a^{-2} = a.

PROOF SKETCH (Stacks 0ALN, proof of (3)): take P := exists_projRes, lift α to b : F → K with b^{-2} = a ∘ p^{-2} (exists_hom_from_projRes_Q_map_eq), descend b through p to ab : M → K with p ≫ ab = b and ab^{-2} = a (exists_hom_comp_projRes_eq). Then Q.map p ≫ Q.map ab = Q.map b = Q.map p ≫ α, and Q.map p is an iso, so Q.map ab = α. This ab is the required representative.

theorem exists_hom_Q_map_eq_of_comp_canonical
    (hM_pos : ∀ i, 0 < i → IsZero (M.X i)) (hM0 : Projective (M.X 0))
    (hK : ∀ i ≤ (-3 : ℤ), IsZero (K.X i))
    (α : HomD M K)
    (a : M.X (-2) ⟶ K.X (-2))
    (ha : M.d (-3) (-2) ≫ a = 0)
    (hα : α ≫ DerivedCategory.Q.map (canonicalToSingleNegTwo K hK)
        = DerivedCategory.Q.map (HomologicalComplex.mkHomToSingle a (by
            intro i hi
            simp only [ComplexShape.up_Rel] at hi
            have hi3 : i = -3 := by omega
            subst hi3
            exact ha))) :
    ∃ (ab : M ⟶ K),
      DerivedCategory.Q.map ab = α ∧ HomologicalComplex.Hom.f ab (-2) = a

TwoTermComplexExt.toHomD_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/Ext/HomotopyComparison.lean, line 385. The attribute's comment: “(1)”.

(1) Assume K^i = 0 for i ≤ -2. Then the canonical map Hom_{K(R)}(M, K) → Hom_{D(R)}(M, K) is an isomorphism (bijective).

PROOF SKETCH (Stacks 0ALN, proof of (1)): Pick a termwise-surjective projective resolution p : F → M (exists_projRes); then F is K-projective. By CochainComplex.IsKProjective.Qh_map_bijective, the localization map Qh.map : Hom_{K(R)}(F, K) → Hom_{D(R)}(F, K) is bijective. Since Q.map p is an isomorphism in D(R) (p a quasi-iso), postcomposition identifies Hom_{D(R)}(F, K) ≅ Hom_{D(R)}(M, K). By precomp_quotient_map_projRes_bijective, precomposition with [p] is a bijection Hom_{K(R)}(M, K) → Hom_{K(R)}(F, K). Chasing the square (Qh.map is natural and toHomD = Qh.map), toHomD : Hom\_\{K(R)}(M, K) → Hom\_\{D(R)}(M, K) is the composite of these three bijections, hence bijective.

theorem toHomD_bijective
    (hM_pos : ∀ i, 0 < i → IsZero (M.X i)) (hM0 : Projective (M.X 0))
    (hK : ∀ i ≤ (-2 : ℤ), IsZero (K.X i)) :
    Function.Bijective (fun f : HomK M K => (toHomD f : HomD M K))

TwoTermComplexExt.forall_Q_map_comp_eq_zero_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/Ext/HomotopyComparison.lean, line 638. The attribute's comment: “(2)”.

(2) Assume K^i = 0 for i ∉ {-1, 0} and that K^0 is projective. For a morphism of complexes a : M → K, condition (2a) — that for every module N the induced map Ext^1(a, N) : Ext^1(K, N) → Ext^1(M, N), given by pre-composition with Q.map a, is the zero map — is equivalent to (2b) — the existence of an R-module homomorphism h^0 : M^0 → K^{-1} with a^{-1} + h^0 ∘ d_M^{-1} = 0.

PROOF SKETCH: the two implications are Q_map_comp_eq_zero_of_nullHomotopy ((2b)⇒(2a)) and exists_nullHomotopy_of_Q_map_comp_eq_zero ((2a)⇒(2b)); assemble with Iff.intro.

theorem forall_Q_map_comp_eq_zero_iff
    (hM_pos : ∀ i, 0 < i → IsZero (M.X i)) (hM0 : Projective (M.X 0))
    (hK : ∀ i, i ≠ -1 → i ≠ 0 → IsZero (K.X i)) (hK0 : Projective (K.X 0))
    (a : M ⟶ K) :
    (∀ (N : ModuleCat.{v} R) (ξ : ExtMod K N 1),
        DerivedCategory.Q.map a ≫ ξ = 0)
      ↔
    (∃ h0 : M.X 0 ⟶ K.X (-1),
        HomologicalComplex.Hom.f a (-1) + M.d (-1) 0 ≫ h0 = 0)

TwoTermComplexExt.exists_homotopy_components_of_Q_map_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/Ext/RepresentativeHomotopy.lean, line 441. The attribute's comment: “(4)”.

(4) In the situation of (3): given α and a representing morphism of complexes a^• with a^{-2} = a (as produced in (3)), for any second representing morphism of complexes (a')^• with (a')^{-2} = a, there exist R-module homomorphisms h^0 : M^0 → K^{-1} and h^{-1} : M^{-1} → K^{-2} such that h^{-1} ∘ d_M^{-2} = 0, (a')^{-1} = a^{-1} + d_K^{-2} ∘ h^{-1} + h^0 ∘ d_M^{-1}, and (a')^0 = a^0 + d_K^{-1} ∘ h^0.

PROOF SKETCH (Stacks 0ALN, proof of (4)): ab and ab' both represent α, so by nonempty_homotopy_of_Q_map_eq they are chain-homotopic; pick a homotopy H. Feed H (and the degree--2 agreement) to exists_homotopy_components_of_homotopy to obtain h^0, h^{-1} and the three relations.

theorem exists_homotopy_components_of_Q_map_eq
    (hM_pos : ∀ i, 0 < i → IsZero (M.X i)) (hM0 : Projective (M.X 0))
    (hK : ∀ i ≤ (-3 : ℤ), IsZero (K.X i))
    (α : HomD M K)
    (a : M.X (-2) ⟶ K.X (-2))
    (ab ab' : M ⟶ K)
    (hab : DerivedCategory.Q.map ab = α) (hab' : DerivedCategory.Q.map ab' = α)
    (hab_2 : HomologicalComplex.Hom.f ab (-2) = a)
    (hab'_2 : HomologicalComplex.Hom.f ab' (-2) = a) :
    ∃ (h0 : M.X 0 ⟶ K.X (-1)) (hm1 : M.X (-1) ⟶ K.X (-2)),
      M.d (-2) (-1) ≫ hm1 = 0 ∧
      HomologicalComplex.Hom.f ab' (-1) =
        HomologicalComplex.Hom.f ab (-1) + hm1 ≫ K.d (-2) (-1) + M.d (-1) 0 ≫ h0 ∧
      HomologicalComplex.Hom.f ab' 0 =
        HomologicalComplex.Hom.f ab 0 + h0 ≫ K.d (-1) 0
Tag 0G9F, a lemma

Tag 0G9F in the Stacks Project.

TwoTermComplex.ext_one_annihilated_iff_twoTerm_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/Representative.lean, line 356.

Stacks 0G9F. For a derived object with cohomology concentrated in degrees -1 and 0, the first Ext groups are annihilated by an ideal exactly when multiplication by every element of the ideal factors through the differential of a suitable free two-term representative, or of every projective two-term representative. Under Noetherian and finiteness hypotheses these are also equivalent to testing only finite modules and to the existence of a finite representative.

public theorem ext_one_annihilated_iff_twoTerm_factorization
    {R : Type u} [CommRing R] [Small.{v} R] (I : Ideal R)
    (K : DerivedCategory (ModuleCat.{v} R))
    (hK : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj K)) :
    let moduleObject := fun N : ModuleCat.{v} R ↦
      (DerivedCategory.singleFunctor (ModuleCat.{v} R) 0).obj N
    let extAnnihilated := ∀ (N : ModuleCat.{v} R) (a : R), a ∈ I →
      ∀ ξ : DerivedCategory.Ext K (moduleObject N) 1, a • ξ = 0
    let hasFreeRepresentative := ∃ L : CochainComplex (ModuleCat.{v} R) ℤ,
      L.IsStrictlyGE (-1) ∧ L.IsStrictlyLE 0 ∧ Module.Free R (L.X 0) ∧
        Nonempty (DerivedCategory.Q.obj L ≅ K) ∧
        ∀ (a : R), a ∈ I → ∃ h : L.X 0 ⟶ L.X (-1),
          L.d (-1) 0 ≫ h = a • 𝟙 (L.X (-1))
    let everyProjectiveRepresentative := ∀ L : CochainComplex (ModuleCat.{v} R) ℤ,
      L.IsStrictlyGE (-1) → L.IsStrictlyLE 0 → Module.Projective R (L.X 0) →
        Nonempty (DerivedCategory.Q.obj L ≅ K) →
        ∀ (a : R), a ∈ I → ∃ h : L.X 0 ⟶ L.X (-1),
          L.d (-1) 0 ≫ h = a • 𝟙 (L.X (-1))
    let finiteExtAnnihilated := ∀ (N : ModuleCat.{v} R), Module.Finite R N →
      ∀ (a : R), a ∈ I → ∀ ξ : DerivedCategory.Ext K (moduleObject N) 1, a • ξ = 0
    let hasFiniteFreeRepresentative := ∃ L : CochainComplex (ModuleCat.{v} R) ℤ,
      L.IsStrictlyGE (-1) ∧ L.IsStrictlyLE 0 ∧ Module.Finite R (L.X (-1)) ∧
        Module.Finite R (L.X 0) ∧ Module.Free R (L.X 0) ∧
        Nonempty (DerivedCategory.Q.obj L ≅ K) ∧
        ∀ (a : R), a ∈ I → ∃ h : L.X 0 ⟶ L.X (-1),
          L.d (-1) 0 ≫ h = a • 𝟙 (L.X (-1))
    (extAnnihilated ↔ hasFreeRepresentative) ∧
      (hasFreeRepresentative ↔ everyProjectiveRepresentative) ∧
      (IsNoetherianRing R →
        Module.Finite R
          ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) (-1)).obj K) →
        Module.Finite R
          ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) 0).obj K) →
        (extAnnihilated ↔ finiteExtAnnihilated) ∧
          (finiteExtAnnihilated ↔ hasFiniteFreeRepresentative))
Tag 0G9G, a lemma

Tag 0G9G in the Stacks Project.

TwoTermComplex.twoTermBaseChange_iso_truncGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/BaseChange.lean, line 344.

Stacks 0G9G. Termwise base change of a two-term representative whose degree-zero term is flat represents the truncation in degrees at least -1 of the derived base change: the canonical comparison, transported along the representative isomorphism e, factors through truncGEπ (-1) by an isomorphism.

public theorem twoTermBaseChange_iso_truncGE
    {R : Type u} {R' : Type v} [CommRing R] [CommRing R']
    (φ : R →+* R') :
    letI : (ModuleCat.extendScalars.{u, v, max v (max u w)} φ).IsLeftAdjoint :=
      ModuleCat.instIsLeftAdjointExtendScalars.{u, v, max u w} φ
    ∀ (K : DerivedCategory (ModuleCat.{max u v w} R))
      (L : CochainComplex (ModuleCat.{max u v w} R) ℤ)
      (e : DerivedCategory.Q.obj L ≅ K)
      (_hK : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
        Limits.IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{max u v w} R) i).obj K))
      (_hL : ∀ i : ℤ, i ≠ -1 → i ≠ 0 → Limits.IsZero (L.X i))
      (_hflat : Module.Flat R (L.X 0))
      (derivedBaseChange : DerivedCategory (ModuleCat.{max u v w} R) ⥤
        DerivedCategory (ModuleCat.{max u v w} R'))
      (comparison : DerivedCategory.Q ⋙ derivedBaseChange ⟶
        (ModuleCat.extendScalars.{u, v, max v (max u w)} φ).mapHomologicalComplex
          (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
      [derivedBaseChange.IsLeftDerivedFunctor comparison
        (HomologicalComplex.quasiIso (ModuleCat.{max u v w} R) (ComplexShape.up ℤ))],
      ∃ f : ((DerivedCategory.TStructure.t (C := ModuleCat.{max u v w} R')).truncGE (-1)).obj
          (derivedBaseChange.obj K) ⟶
        DerivedCategory.Q.obj
          (((ModuleCat.extendScalars.{u, v, max v (max u w)} φ).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj L),
        ((DerivedCategory.TStructure.t (C := ModuleCat.{max u v w} R')).truncGEπ (-1)).app
          (derivedBaseChange.obj K) ≫ f = derivedBaseChange.map e.inv ≫ comparison.app L ∧
        IsIso f
Tag 0G9H, a lemma

Tag 0G9H in the Stacks Project.

TwoTermComplex.ext_one_annihilated_truncGE_derivedBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/ExtAnnihilationCriteria.lean, line 51.

Stacks 0G9H. If an ideal annihilates every degree-one Ext group from a two-term derived object, then the extended ideal has the same property for its derived base change truncated in degrees at least -1.

public theorem ext_one_annihilated_truncGE_derivedBaseChange
    {R : Type u} {R' : Type v} [CommRing R] [CommRing R']
    (I : Ideal R) (K : DerivedCategory (ModuleCat.{max u v} R))
    (hK : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{max u v} R) i).obj K))
    (φ : R →+* R')
    (hI : ∀ (N : ModuleCat.{max u v} R) (a : R), a ∈ I →
      ∀ ξ : DerivedCategory.Ext K
        ((DerivedCategory.singleFunctor (ModuleCat.{max u v} R) 0).obj N) 1,
        a • ξ = 0)
    (derivedBaseChange : DerivedCategory (ModuleCat.{max u v} R) ⥤
      DerivedCategory (ModuleCat.{max u v} R'))
    (comparison : DerivedCategory.Q ⋙ derivedBaseChange ⟶
      (ModuleCat.extendScalars φ).mapHomologicalComplex (ComplexShape.up ℤ) ⋙
        DerivedCategory.Q)
    [derivedBaseChange.IsLeftDerivedFunctor comparison
      (HomologicalComplex.quasiIso (ModuleCat.{max u v} R) (ComplexShape.up ℤ))] :
    let K' := ((DerivedCategory.TStructure.t (C := ModuleCat.{max u v} R')).truncGE (-1)).obj
      (derivedBaseChange.obj K)
    ∀ (N : ModuleCat.{max u v} R') (a : R'), a ∈ Ideal.map φ I →
      ∀ ξ : DerivedCategory.Ext K'
        ((DerivedCategory.singleFunctor (ModuleCat.{max u v} R') 0).obj N) 1,
        a • ξ = 0
Tag 0G9I, a lemma

Tag 0G9I in the Stacks Project.

TwoTermComplex.smul_id_eq_zero_of_two_term_homology_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/Morphisms.lean, line 103.

Stacks 0G9I. Let α : K ⟶ K' be a morphism of D(R) between objects with cohomology in degrees -1 and 0 such that H⁰(α) is an isomorphism and H⁻¹(α) is surjective. If multiplication by f : R is zero on K, then it is zero on K'.

public theorem smul_id_eq_zero_of_two_term_homology_map
    {R : Type u} [CommRing R]
    {K K' : DerivedCategory (ModuleCat.{v} R)} (α : K ⟶ K')
    (hK : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      Limits.IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj K))
    (hK' : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      Limits.IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj K'))
    (hα0 : IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) 0).map α))
    (hαneg : Epi ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) (-1)).map α))
    (f : R) (hf : f • 𝟙 K = 0) :
    f • 𝟙 K' = 0
Tag 0G9J, a lemma

Tag 0G9J in the Stacks Project.

TwoTermComplexExt.ext_one_annihilated_of_homology_iso_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/ExtAnnihilation.lean, line 53.

Stacks 0G9J. Let K ⟶ K' be a morphism of derived objects whose cohomology is concentrated in degrees -1 and 0. If it induces an isomorphism in degree 0 and an epimorphism in degree -1, then ideal annihilation of every first Ext group for K implies the same ideal annihilation for K'.

public theorem ext_one_annihilated_of_homology_iso_epi
    {R : Type u} [CommRing R] (I : Ideal R)
    {K K' : DerivedCategory (ModuleCat.{v} R)}
    (α : K ⟶ K')
    (hK : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj K))
    (hK' : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj K'))
    [IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) 0).map α)]
    [Epi ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) (-1)).map α)]
    (h : ∀ (N : ModuleCat.{v} R) (a : R), a ∈ I →
      ∀ ξ : DerivedCategory.Ext K
        ((DerivedCategory.singleFunctor (ModuleCat.{v} R) 0).obj N) 1,
        a • ξ = 0) :
    ∀ (N : ModuleCat.{v} R) (a : R), a ∈ I →
      ∀ ξ : DerivedCategory.Ext K'
        ((DerivedCategory.singleFunctor (ModuleCat.{v} R) 0).obj N) 1,
        a • ξ = 0
Tag 0G9K, a lemma

Tag 0G9K in the Stacks Project.

TwoTermComplex.exists_power_ext_one_annihilated_iff_cohomology_conditions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/IdealPower.lean, line 362.

Stacks 0G9K. For a two-term derived object, some power of an ideal annihilates all first Ext groups if and only if some power annihilates degree-minus-one cohomology and makes degree-zero cohomology relatively projective. Under Noetherian and finiteness hypotheses these are also equivalent to the corresponding finite-module Ext condition and to projectivity of degree-zero cohomology after localization on a finite cover of the complement of the ideal's vanishing locus.

public theorem exists_power_ext_one_annihilated_iff_cohomology_conditions
    {R : Type u} [CommRing R] [Small.{v} R] (I : Ideal R)
    (K : DerivedCategory (ModuleCat.{v} R))
    (hK : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj K)) :
    let Hneg := (DerivedCategory.homologyFunctor (ModuleCat.{v} R) (-1)).obj K
    let Hzero := (DerivedCategory.homologyFunctor (ModuleCat.{v} R) 0).obj K
    let moduleObject := fun N : ModuleCat.{v} R ↦
      (DerivedCategory.singleFunctor (ModuleCat.{v} R) 0).obj N
    let extAnnihilatedBySomePower := ∃ c : ℕ, ∀ (N : ModuleCat.{v} R) (a : R),
      a ∈ I ^ c → ∀ ξ : DerivedCategory.Ext K (moduleObject N) 1, a • ξ = 0
    let cohomologyCondition := ∃ c : ℕ,
      (∀ (a : R), a ∈ I ^ c → ∀ x : Hneg, a • x = 0) ∧
        Module.IsIProjective R (I ^ c) Hzero
    let finiteExtAnnihilatedBySomePower := ∃ c : ℕ, ∀ (N : ModuleCat.{v} R),
      Module.Finite R N → ∀ (a : R), a ∈ I ^ c →
        ∀ ξ : DerivedCategory.Ext K (moduleObject N) 1, a • ξ = 0
    let localizedProjectiveOnNeighborhood :=
      IsIPowerTorsion R Hneg I ∧ ∃ (n : ℕ) (f : Fin n → R),
        I.radical ≤ (Ideal.span (Set.range f)).radical ∧
          ∀ i, Module.Projective (Localization.Away (f i))
            (LocalizedModule (Submonoid.powers (f i)) Hzero)
    let localizedProjectiveOnCover :=
      IsIPowerTorsion R Hneg I ∧ ∃ (n : ℕ) (f : Fin n → R),
        (∀ i, f i ∈ I) ∧ (Ideal.span (Set.range f)).radical = I.radical ∧
          ∀ i, Module.Projective (Localization.Away (f i))
            (LocalizedModule (Submonoid.powers (f i)) Hzero)
    let localizedProjectiveOnEveryCover :=
      IsIPowerTorsion R Hneg I ∧ ∀ (n : ℕ) (f : Fin n → R),
        (∀ i, f i ∈ I) → (Ideal.span (Set.range f)).radical = I.radical →
          ∀ i, Module.Projective (Localization.Away (f i))
            (LocalizedModule (Submonoid.powers (f i)) Hzero)
    (extAnnihilatedBySomePower ↔ cohomologyCondition) ∧
      (IsNoetherianRing R → Module.Finite R Hneg → Module.Finite R Hzero →
        (extAnnihilatedBySomePower ↔ finiteExtAnnihilatedBySomePower) ∧
        (finiteExtAnnihilatedBySomePower ↔ localizedProjectiveOnNeighborhood) ∧
        (localizedProjectiveOnNeighborhood ↔ localizedProjectiveOnCover) ∧
        (localizedProjectiveOnCover ↔ localizedProjectiveOnEveryCover))
Tag 0AJT, a lemma

Tag 0AJT in the Stacks Project.

TwoTermComplex.comp_eq_zero_of_two_term_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/Morphisms.lean, line 55.

Stacks 0AJT. Let K₁, K₂, K₃ be objects of D(R) with cohomology in degrees -1 and 0, and let φ : K₁ ⟶ K₂, ψ : K₂ ⟶ K₃. If H⁰(φ) = 0 and H⁻¹(ψ) = 0, then φ ≫ ψ = 0.

public theorem comp_eq_zero_of_two_term_homology
    {R : Type u} [Ring R]
    (K₁ K₂ K₃ : DerivedCategory (ModuleCat.{u} R))
    (hK₁ : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      Limits.IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj K₁))
    (_hK₂ : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      Limits.IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj K₂))
    (hK₃ : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      Limits.IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj K₃))
    (φ : K₁ ⟶ K₂) (ψ : K₂ ⟶ K₃)
    (hφ : (DerivedCategory.homologyFunctor (ModuleCat.{u} R) 0).map φ = 0)
    (hψ : (DerivedCategory.homologyFunctor (ModuleCat.{u} R) (-1)).map ψ = 0) :
    φ ≫ ψ = 0
Tag 0G9L, a lemma

Tag 0G9L in the Stacks Project.

Matrix.Q_map_detSmul_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/TwoTermComplex/Determinant.lean, line 208.

Stacks 0G9L. The morphism det(A) : K → K is the zero morphism in the derived category D(R).

theorem Q_map_detSmul_eq_zero :
    (DerivedCategory.Q (C := ModuleCat R)).map (detSmul A) = 0
Sources

Section15.87 The naive cotangent complex#

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

Tag 0FUY, a lemma

Tag 0FUY in the Stacks Project.

NaiveCotangent.naiveCotangent_baseChange_truncGE_comparison_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/DerivedBaseChange.lean, line 561.

Stacks 0FUY. For R → S → S', the canonical comparison from derived to termwise base change of the naive cotangent complex induces an isomorphism after truncation in degrees at least -1. This holds for the canonical presentation and for every polynomial presentation of S over R.

public theorem naiveCotangent_baseChange_truncGE_comparison_isIso
    {R : Type uR} {S : Type uS} {S' : Type uS'}
    [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra S S'] :
    letI : Functor.IsLeftAdjoint
        (ModuleCat.extendScalars.{uS, uS', max uS' (max uR uS w)} (algebraMap S S')) :=
      ModuleCat.instIsLeftAdjointExtendScalars.{uS, uS', max uR uS w} (algebraMap S S')
    ∀ (derivedBaseChange : DerivedCategory (ModuleCat.{max uS' (max uR uS w)} S) ⥤
        DerivedCategory (ModuleCat.{max uS' (max uR uS w)} S'))
      (comparison : DerivedCategory.Q ⋙ derivedBaseChange ⟶
        (ModuleCat.extendScalars.{uS, uS', max uS' (max uR uS w)}
          (algebraMap S S')).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
      [derivedBaseChange.IsLeftDerivedFunctor comparison
        (HomologicalComplex.quasiIso (ModuleCat.{max uS' (max uR uS w)} S)
          (ComplexShape.up ℤ))],
    let canonicalMapInducesIso
        (L : CochainComplex (ModuleCat.{max uS' (max uR uS w)} S) ℤ) : Prop :=
      ∃ f : ((DerivedCategory.TStructure.t
                (C := ModuleCat.{max uS' (max uR uS w)} S')).truncGE (-1)).obj
              (derivedBaseChange.obj (DerivedCategory.Q.obj L)) ⟶
            DerivedCategory.Q.obj
              (((ModuleCat.extendScalars.{uS, uS', max uS' (max uR uS w)}
                  (algebraMap S S')).mapHomologicalComplex
                (ComplexShape.up ℤ)).obj L),
        comparison.app L =
          ((DerivedCategory.TStructure.t
              (C := ModuleCat.{max uS' (max uR uS w)} S')).truncGEπ (-1)).app
            (derivedBaseChange.obj (DerivedCategory.Q.obj L)) ≫ f ∧
          IsIso f
    canonicalMapInducesIso
        (CochainComplex.mappingCone
          ((CochainComplex.singleFunctor (ModuleCat.{max uS' (max uR uS w)} S) 0).map
            (ModuleCat.ofHom
              (ULift.moduleEquiv.{uS, max uR uS,
                  max uS' (max uR uS w)}.symm.toLinearMap.comp
                ((NaiveCotangent.NL (NaiveCotangent.canonicalGenerators R S)).d.comp
                  ULift.moduleEquiv.{uS, max uR uS,
                    max uS' (max uR uS w)}.toLinearMap))))) ∧
      ∀ (ι : Type w) (P : Algebra.Generators R S ι),
        canonicalMapInducesIso
          (CochainComplex.mappingCone
            ((CochainComplex.singleFunctor (ModuleCat.{max uS' (max uR uS w)} S) 0).map
              (ModuleCat.ofHom
                (ULift.moduleEquiv.{uS, max (max uR uS) w,
                    max uS' (max uR uS w)}.symm.toLinearMap.comp
                  ((NaiveCotangent.NL P).d.comp
                    ULift.moduleEquiv.{uS, max uR w,
                      max uS' (max uR uS w)}.toLinearMap)))))
Tag 0FUZ, a lemma

Tag 0FUZ in the Stacks Project.

NaiveCotangent.naiveCotangentComplex_baseChange_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/DerivedBaseChange.lean, line 486.

Stacks 0FUZ. Formation of the naive cotangent complex commutes with arbitrary base change on H⁰ and is surjective on H⁻¹, both for a chosen polynomial presentation and for the canonical one.

public theorem naiveCotangentComplex_baseChange_homology
    {R : Type u} {S : Type v} {T : Type w} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T] {ι : Type t} (P : Algebra.Generators R S ι) :
    let S' := T ⊗[R] S
    letI : Algebra S S' := Algebra.TensorProduct.rightAlgebra
    let P' := P.baseChange T
    let h := (P.baseChangeFromBaseChange T).comp (P.toExtension.toBaseChange T)
    let d := AlgebraTensorModule.lTensor S' S' P.toExtension.cotangentComplex
    let f₁ := (Algebra.Extension.Cotangent.map h).liftBaseChange S'
    let f₀ := (Algebra.Extension.CotangentSpace.map h).liftBaseChange S'
    P'.toExtension.cotangentComplex ∘ₗ f₁ = f₀ ∘ₗ d ∧
      (∀ y, ∃ x, y - f₀ x ∈ LinearMap.range P'.toExtension.cotangentComplex) ∧
      (∀ x, f₀ x ∈ LinearMap.range P'.toExtension.cotangentComplex ↔
        x ∈ LinearMap.range d) ∧
      (∀ y, P'.toExtension.cotangentComplex y = 0 →
        ∃ x, d x = 0 ∧ f₁ x = y) ∧
      let Pc := Algebra.Generators.self R S
      let Pc' := Algebra.Generators.self T S'
      let hc := (Pc.defaultHom Pc').toExtensionHom
      let dc := AlgebraTensorModule.lTensor S' S' Pc.toExtension.cotangentComplex
      let fc₁ := (Algebra.Extension.Cotangent.map hc).liftBaseChange S'
      let fc₀ := (Algebra.Extension.CotangentSpace.map hc).liftBaseChange S'
      Pc'.toExtension.cotangentComplex ∘ₗ fc₁ = fc₀ ∘ₗ dc ∧
        (∀ y, ∃ x, y - fc₀ x ∈ LinearMap.range Pc'.toExtension.cotangentComplex) ∧
        (∀ x, fc₀ x ∈ LinearMap.range Pc'.toExtension.cotangentComplex ↔
          x ∈ LinearMap.range dc) ∧
        ∀ y, Pc'.toExtension.cotangentComplex y = 0 →
          ∃ x, dc x = 0 ∧ fc₁ x = y
Tag 0FJU, a lemma

Tag 0FJU in the Stacks Project.

NaiveCotangent.naiveCotangentComplex_quasiIso_baseChange_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/Cocartesian.lean, line 830.

Stacks 0FJU. Let A → B be flat, let A → A' be arbitrary and let B' = A' ⊗[A] B be the pushout, so that the square with corners A, A', B, B' is cocartesian. Then the canonical map NL_{B/A} ⊗_B B' → NL_{B'/A'} is a quasi-isomorphism, and if in addition NL_{B/A} has Tor amplitude in [-1, 0] then the derived base-change map NL_{B/A} ⊗_B^L B' → NL_{B'/A'} is a quasi-isomorphism too.

The naive cotangent complexes are the two-term complexes HomologicalComplex.double of the canonical presentations, in cohomological degrees -1 and 0, with their modules and rings lifted to one universe. The map of the first assertion is the displayed chain map g; the map of the second is that chain map composed with the comparison from derived to ordinary extension of scalars, which is what makes the composite the derived base-change map.

public theorem naiveCotangentComplex_quasiIso_baseChange_of_flat
    {A : Type uA} {B : Type uB} {A' : Type uC}
    [CommRing A] [CommRing B] [CommRing A'] [Algebra A B] [Algebra A A'] [Module.Flat A B] :
    let B' := A' ⊗[A] B
    letI : Algebra B B' := Algebra.TensorProduct.rightAlgebra
    let P := Algebra.Generators.self A B
    let P' := Algebra.Generators.self A' B'
    let h := (P.defaultHom P').toExtensionHom
    let X₁ : ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B) :=
      ModuleCat.of (ULift.{max uA uB uC} B)
        (ULift.{max uA uB uC} P.toExtension.Cotangent)
    let X₀ : ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B) :=
      ModuleCat.of (ULift.{max uA uB uC} B)
        (ULift.{max uA uB uC} P.toExtension.CotangentSpace)
    let X₁' : ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B') :=
      ModuleCat.of (ULift.{max uA uB uC} B')
        (ULift.{max uA uB uC} P'.toExtension.Cotangent)
    let X₀' : ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B') :=
      ModuleCat.of (ULift.{max uA uB uC} B')
        (ULift.{max uA uB uC} P'.toExtension.CotangentSpace)
    let d : X₁ ⟶ X₀ := ModuleCat.ofHom {
      toFun := fun x => ULift.up (P.toExtension.cotangentComplex x.down)
      map_add' := by
        intro x y
        exact congrArg ULift.up (P.toExtension.cotangentComplex.map_add x.down y.down)
      map_smul' := by
        intro r x
        exact congrArg ULift.up (P.toExtension.cotangentComplex.map_smul r.down x.down) }
    let d' : X₁' ⟶ X₀' := ModuleCat.ofHom {
      toFun := fun x => ULift.up (P'.toExtension.cotangentComplex x.down)
      map_add' := by
        intro x y
        exact congrArg ULift.up (P'.toExtension.cotangentComplex.map_add x.down y.down)
      map_smul' := by
        intro r x
        exact congrArg ULift.up (P'.toExtension.cotangentComplex.map_smul r.down x.down) }
    let hd : (ComplexShape.up ℤ).Rel (-1) 0 := by decide
    let hne : (-1 : ℤ) ≠ 0 := by decide
    let K : CochainComplex (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)) ℤ :=
      HomologicalComplex.double d hd
    let K' : CochainComplex (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B')) ℤ :=
      HomologicalComplex.double d' hd
    let E : ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B) ⥤
        ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B') :=
      ModuleCat.extendScalars.{max uA uB uC, max uA uB uC, max uA uB uC}
        ((algebraMap B B').ulift)
    let f₁ : E.obj X₁ ⟶ X₁' :=
      ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars ((algebraMap B B').ulift)
        (ModuleCat.ofHom (Y := (ModuleCat.restrictScalars ((algebraMap B B').ulift)).obj X₁')
          { toFun := fun x => ULift.up (Algebra.Extension.Cotangent.map h x.down)
            map_add' := by
              intro x y
              exact congrArg ULift.up ((Algebra.Extension.Cotangent.map h).map_add x.down y.down)
            map_smul' := by
              intro r x
              change ULift.up _ = ULift.up _
              congr 1
              change (Algebra.Extension.Cotangent.map h) (r.down • x.down) =
                (algebraMap B B' r.down) • (Algebra.Extension.Cotangent.map h x.down)
              exact (Algebra.Extension.Cotangent.map h).map_smul r.down x.down })
    let f₀ : E.obj X₀ ⟶ X₀' :=
      ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars ((algebraMap B B').ulift)
        (ModuleCat.ofHom (Y := (ModuleCat.restrictScalars ((algebraMap B B').ulift)).obj X₀')
          { toFun := fun x => ULift.up (Algebra.Extension.CotangentSpace.map h x.down)
            map_add' := by
              intro x y
              exact congrArg ULift.up
                ((Algebra.Extension.CotangentSpace.map h).map_add x.down y.down)
            map_smul' := by
              intro r x
              change ULift.up _ = ULift.up _
              congr 1
              change (Algebra.Extension.CotangentSpace.map h) (r.down • x.down) =
                (algebraMap B B' r.down) • (Algebra.Extension.CotangentSpace.map h x.down)
              rw [IsScalarTower.algebraMap_smul]
              exact (Algebra.Extension.CotangentSpace.map h).map_smul r.down x.down })
    ∀ (derivedTensor :
        DerivedCategory (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)) ⥤
          DerivedCategory (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)) ⥤
            DerivedCategory (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)))
      (tensorComparison : ∀ M : ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B),
        DerivedCategory.Q ⋙ derivedTensor.flip.obj
            ((DerivedCategory.singleFunctor
              (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)) 0).obj M) ⟶
          (StacksDraft.TorAmplitude.tensorModuleRight M).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
      (tensorIsLeftDerived : ∀ M : ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B),
        (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor
            (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B))
            0).obj M)).IsLeftDerivedFunctor
          (tensorComparison M)
          (HomologicalComplex.quasiIso
            (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)) (ComplexShape.up ℤ)))
      (tensorCommShift : ∀ M : ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B),
        (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor
            (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)) 0).obj M)).CommShift ℤ)
      (tensorTriangulated : ∀ M : ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B),
        letI := tensorCommShift M
        (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor
            (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)) 0).obj M)).IsTriangulated)
      (derivedExtension :
        DerivedCategory (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)) ⥤
          DerivedCategory (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B')))
      (extensionComparison :
        DerivedCategory.Q ⋙ derivedExtension ⟶
          E.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
      (_extensionIsLeftDerived : derivedExtension.IsLeftDerivedFunctor extensionComparison
        (HomologicalComplex.quasiIso
          (ModuleCat.{max uA uB uC} (ULift.{max uA uB uC} B)) (ComplexShape.up ℤ))),
    ∃ g : (E.mapHomologicalComplex (ComplexShape.up ℤ)).obj K ⟶ K',
      g.f (-1) =
          E.map (HomologicalComplex.doubleXIso₀ d hd).hom ≫ f₁ ≫
            (HomologicalComplex.doubleXIso₀ d' hd).inv ∧
        g.f 0 =
          E.map (HomologicalComplex.doubleXIso₁ d hd hne).hom ≫ f₀ ≫
            (HomologicalComplex.doubleXIso₁ d' hd hne).inv ∧
        QuasiIso g ∧
        (StacksDraft.TorAmplitude.HasTorAmplitude derivedTensor tensorComparison
            tensorIsLeftDerived (DerivedCategory.Q.obj K) (-1) 0 →
          IsIso (extensionComparison.app K ≫ DerivedCategory.Q.map g))
Tag 0FV0, a lemma

Tag 0FV0 in the Stacks Project.

NaiveCotangent.naiveCotangentComplex_isPerfect_and_hasTorAmplitude, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/CompleteIntersection/NaiveCotangentPerfect.lean, line 414. References: SGA 6 0 (4.4), “affine case”.

The naive cotangent complex of a local complete intersection is perfect and has Tor-amplitude in [-1, 0].

public theorem naiveCotangentComplex_isPerfect_and_hasTorAmplitude
    {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B]
    (h : RingHom.IsLocalCompleteIntersection (algebraMap A B))
    (derivedTensor :
      DerivedCategory (ModuleCat.{max u v} B) ⥤
        DerivedCategory (ModuleCat.{max u v} B) ⥤
          DerivedCategory (ModuleCat.{max u v} B))
    (comparison : ∀ M : ModuleCat.{max u v} B,
      DerivedCategory.Q ⋙
          derivedTensor.flip.obj
            ((DerivedCategory.singleFunctor (ModuleCat.{max u v} B) 0).obj M) ⟶
        (tensorModuleRight M).mapHomologicalComplex
            (ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
    (isLeftDerived : ∀ M : ModuleCat.{max u v} B,
      (derivedTensor.flip.obj
          ((DerivedCategory.singleFunctor (ModuleCat.{max u v} B) 0).obj M)).IsLeftDerivedFunctor
        (comparison M)
        (HomologicalComplex.quasiIso (ModuleCat.{max u v} B) (ComplexShape.up ℤ))) :
    StacksDraft.Perfect.IsPerfect (naiveCotangentObject A B) ∧
      HasTorAmplitude derivedTensor comparison isLeftDerived
        (naiveCotangentObject A B) (-1) 0
Tag 0FV1, a lemma

Tag 0FV1 in the Stacks Project.

NaiveCotangent.finite_projective_ker_naiveCotangent_baseChange_homology_negOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/NaiveCotangent/CocartesianKernel.lean, line 294.

Stacks 0FV1. In a pushout square of rings, if both parallel maps are local complete intersections, then the kernel of the base-change map on degree -1 homology of the naive cotangent complex is a finite projective module over the pushout.

public theorem finite_projective_ker_naiveCotangent_baseChange_homology_negOne
    {A : Type u} {B : Type v} {A' : Type w}
    [CommRing A] [CommRing B] [CommRing A'] [Algebra A B] [Algebra A A']
    (h : RingHom.IsLocalCompleteIntersection (algebraMap A B)) :
    let B' := A' ⊗[A] B
    letI : Algebra B B' := Algebra.TensorProduct.rightAlgebra
    RingHom.IsLocalCompleteIntersection (algebraMap A' B') →
      let P := Algebra.Generators.self A B
      let P' := Algebra.Generators.self A' B'
      let comparison := (P.defaultHom P').toExtensionHom
      let d := AlgebraTensorModule.lTensor B' B' P.toExtension.cotangentComplex
      let f := (Algebra.Extension.Cotangent.map comparison).liftBaseChange B'
      Module.Finite B' (LinearMap.ker (f.domRestrict (LinearMap.ker d))) ∧
        Module.Projective B' (LinearMap.ker (f.domRestrict (LinearMap.ker d)))
Sources

Section15.88 Rlim of abelian groups#

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

Tag 07KW, a lemma

Tag 07KW in the Stacks Project.

Rlim.lim_hasRightDerivedFunctor_and_computations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Rlim.lean, line 1770.

Stacks 07KW. The inverse-limit functor on inverse systems of abelian groups has a right derived functor on the unbounded derived category. Higher derived limits vanish above degree one; the derived limit of a system is represented by the two-term product complex with differential (x_n) ↦ (x_n - f_{n+1}(x_{n+1})); Mittag--Leffler systems have vanishing first derived limit; every complex has a quasi-isomorphic complex of right-acyclic terms; and on such a complex the derived limit is represented by the termwise inverse-limit complex. Its shift structure and natural degree-zero comparison give an exact functor on the derived categories. The ordinary limit is the kernel of the product differential, its first derived limit is the cokernel, and the latter identification holds for any right-derived functor.

public theorem lim_hasRightDerivedFunctor_and_computations :
    let F : Rlim.InvSystemAb.{u} ⥤ Ab.{u} := lim
    let P := Rlim.product.{u}
    let δ := Rlim.delta.{u}
    ∃ (RF : DerivedCategory Rlim.InvSystemAb.{u} ⥤ DerivedCategory Ab.{u})
      (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
        DerivedCategory.Qh ⋙ RF),
      RF.IsRightDerivedFunctor α (HomotopyCategory.quasiIso Rlim.InvSystemAb.{u} (ComplexShape.up
        ℤ)) ∧
      (∀ (A : Rlim.InvSystemAb.{u}) (p : ℤ), 1 < p →
        IsZero ((DerivedCategory.homologyFunctor Ab.{u} p).obj
          (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj A)))) ∧
      (∀ A : Rlim.InvSystemAb.{u}, ∃ (K : CochainComplex Ab.{u} ℤ)
          (e₀ : K.X 0 ≅ P A) (e₁ : K.X 1 ≅ P A),
        (∀ i : ℤ, i ≠ 0 → i ≠ 1 → IsZero (K.X i)) ∧
        e₀.inv ≫ K.d 0 1 ≫ e₁.hom = δ A ∧
        Nonempty (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj A) ≅
          DerivedCategory.Q.obj K)) ∧
      (∀ A : Rlim.InvSystemAb.{u}, (A ⋙ forget Ab).IsMittagLeffler →
        IsZero ((DerivedCategory.homologyFunctor Ab.{u} 1).obj
          (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj A)))) ∧
      (∀ K : CochainComplex Rlim.InvSystemAb.{u} ℤ,
        ∃ (L : CochainComplex Rlim.InvSystemAb.{u} ℤ) (f : K ⟶ L) (_ : QuasiIso f),
          ∀ p : ℤ, IsZero ((DerivedCategory.homologyFunctor Ab.{u} 1).obj
            (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj (L.X p))))) ∧
      (∀ K : CochainComplex Rlim.InvSystemAb.{u} ℤ,
        (∀ p : ℤ, IsZero ((DerivedCategory.homologyFunctor Ab.{u} 1).obj
          (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj (K.X p))))) →
        Nonempty (RF.obj (DerivedCategory.Q.obj K) ≅
          DerivedCategory.Q.obj ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K))) ∧
      (∀ A : Rlim.InvSystemAb.{u},
        ∃ e : limit A ≅ kernel (δ A),
          ∀ n : ℕ, e.hom ≫ kernel.ι (δ A) ≫
            Pi.π (fun n : ℕ ↦ A.obj (Opposite.op n)) n =
              limit.π A (Opposite.op n)) ∧
      (∀ A : Rlim.InvSystemAb.{u},
        Nonempty (((DerivedCategory.homologyFunctor Ab.{u} 1).obj
          (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj A))) ≅
            cokernel (δ A))) ∧
      (∀ A : Rlim.InvSystemAb.{u},
        IsZero ((DerivedCategory.homologyFunctor Ab.{u} 1).obj
          (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj A))) →
        ∃ w : Rlim.limitToProduct A ≫ δ A = 0,
          (ShortComplex.mk (Rlim.limitToProduct A) (δ A) w).ShortExact) ∧
      (∀ (RF' : DerivedCategory Rlim.InvSystemAb.{u} ⥤ DerivedCategory Ab.{u})
        (α' : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
          DerivedCategory.Qh ⋙ RF'),
        RF'.IsRightDerivedFunctor α'
          (HomotopyCategory.quasiIso Rlim.InvSystemAb.{u} (ComplexShape.up ℤ)) →
        ∀ A : Rlim.InvSystemAb.{u},
          Nonempty (((DerivedCategory.homologyFunctor Ab.{u} 1).obj
            (RF'.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj A))) ≅
              cokernel (δ A))) ∧
      ∃ (commShift : RF.CommShift ℤ),
        letI : RF.CommShift ℤ := commShift
        NatTrans.CommShift α ℤ ∧ RF.IsTriangulated ∧
          Nonempty (F ≅ DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0 ⋙ RF ⋙
            DerivedCategory.homologyFunctor Ab.{u} 0)
Tag 08U4, an equation

Tag 08U4 in the Stacks Project.

Rlim.lim_hasRightDerivedFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Rlim.lean, line 1981.

Stacks 08U4. The inverse-limit functor on inverse systems of abelian groups has a right derived functor from D(Ab(N)) to D(Ab).

public theorem lim_hasRightDerivedFunctor :
    let F : Rlim.InvSystemAb ⥤ Ab.{0} := lim
    ∃ (RF : DerivedCategory Rlim.InvSystemAb ⥤ DerivedCategory Ab.{0})
      (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
        DerivedCategory.Qh ⋙ RF),
      RF.IsRightDerivedFunctor α
        (HomotopyCategory.quasiIso Rlim.InvSystemAb (ComplexShape.up ℤ))
Tag 0H31, a lemma

Tag 0H31 in the Stacks Project.

Rlim.exists_sixTerm_exact_sequence_lim_rightDerived_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Rlim.lean, line 2025.

Stacks 0H31. A short exact sequence of inverse systems of abelian groups induces the exact sequence 0 ⟶ lim A ⟶ lim B ⟶ lim C ⟶ R¹lim A ⟶ R¹lim B ⟶ R¹lim C ⟶ 0. The maps other than the connecting morphism are the functorial maps of lim and R¹lim. The connecting morphism is canonically obtained from the distinguished triangle of the short exact sequence and is natural in morphisms of short exact sequences.

public theorem exists_sixTerm_exact_sequence_lim_rightDerived_one
    {S : ShortComplex Rlim.InvSystemAb.{u}} (hS : S.ShortExact) :
    let F : Rlim.InvSystemAb.{u} ⥤ Ab.{u} := lim
    ∃ (RF : DerivedCategory Rlim.InvSystemAb.{u} ⥤ DerivedCategory Ab.{u})
      (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
        DerivedCategory.Qh ⋙ RF) (commShift : RF.CommShift ℤ),
      letI : RF.CommShift ℤ := commShift
      RF.IsRightDerivedFunctor α
          (HomotopyCategory.quasiIso Rlim.InvSystemAb.{u} (ComplexShape.up ℤ)) ∧
        RF.IsTriangulated ∧
        let R (n : ℤ) : Rlim.InvSystemAb.{u} ⥤ Ab.{u} :=
          DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0 ⋙ RF ⋙
            DerivedCategory.homologyFunctor Ab.{u} n
        ∃ e : F ≅ R 0,
          let δ : ∀ {T : ShortComplex Rlim.InvSystemAb.{u}}, T.ShortExact →
              (F.obj T.X₃ ⟶ (R 1).obj T.X₁) := fun {T} (hT : T.ShortExact) ↦ by
            change F.obj T.X₃ ⟶
              (DerivedCategory.homologyFunctor Ab.{u} 1).obj
                (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj T.X₁))
            exact e.hom.app T.X₃ ≫
              DerivedCategory.HomologySequence.δ
                (RF.mapTriangle.obj hT.singleTriangle) 0 1 rfl
          (ComposableArrows.mk₅ (F.map S.f) (F.map S.g) (δ hS)
              ((R 1).map S.f) ((R 1).map S.g)).Exact ∧
            Mono (F.map S.f) ∧ Epi ((R 1).map S.g) ∧
            ∀ {T₁ T₂ : ShortComplex Rlim.InvSystemAb.{u}}
              (h₁ : T₁.ShortExact) (h₂ : T₂.ShortExact) (f : T₁ ⟶ T₂),
              δ h₁ ≫ (R 1).map f.τ₁ = F.map f.τ₃ ≫ δ h₂
Tag 0918, a lemma

Tag 0918 in the Stacks Project.

Rlim.comparisonHomologyLimit_isIso_of_isZero_rightDerivedLim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Rlim.lean, line 2389.

Stacks 0918. Let A⁻² ⟶ A⁻¹ ⟶ A⁰ ⟶ A¹ be an inverse system of four-term complexes of abelian groups. If R¹ lim vanishes on A⁻², on A⁻¹, and on the inverse system of degree -1 cohomologies, then the canonical morphism from the degree-zero cohomology of the termwise inverse limit to the inverse limit of the degree-zero cohomologies is an isomorphism.

public theorem comparisonHomologyLimit_isIso_of_isZero_rightDerivedLim
    (A_neg2 A_neg1 A_0 A_1 : Rlim.InvSystemAb)
    (d_neg2 : A_neg2 ⟶ A_neg1) (d_neg1 : A_neg1 ⟶ A_0) (d_0 : A_0 ⟶ A_1)
    (h_neg1 : ∀ i, d_neg2.app i ≫ d_neg1.app i = 0)
    (h_0 : ∀ i, d_neg1.app i ≫ d_0.app i = 0)
    (RF : DerivedCategory Rlim.InvSystemAb ⥤ DerivedCategory Ab.{0})
    (α : (lim : Rlim.InvSystemAb ⥤ Ab.{0}).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RF)
    (hRF : RF.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso Rlim.InvSystemAb (ComplexShape.up ℤ)))
    (hA_neg2 : IsZero ((DerivedCategory.homologyFunctor Ab.{0} 1).obj
      (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb 0).obj A_neg2))))
    (hA_neg1 : IsZero ((DerivedCategory.homologyFunctor Ab.{0} 1).obj
      (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb 0).obj A_neg1))))
    (hH_neg1 : IsZero ((DerivedCategory.homologyFunctor Ab.{0} 1).obj
      (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb 0).obj
        (homologyInvSystem d_neg2 d_neg1 h_neg1))))) :
    IsIso (comparisonHomologyLimit d_neg1 d_0 h_0)
Tag 0H9K, a lemma

Tag 0H9K in the Stacks Project.

Rlim.Pro.exists_map_lim_and_cokernel_delta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ProIsomorphism/LimAndRlimOne.lean, line 657.

Stacks 0H9K. Morphisms of pro-systems of abelian groups induce maps on inverse limits and first derived inverse limits. The maps are functorial in the pro-morphism, and both are isomorphisms when the pro-morphism is an isomorphism.

public theorem exists_map_lim_and_cokernel_delta :
    let Rlim.InvSystemAb := ℕᵒᵖ ⥤ Ab.{w}
    let proYoneda (A : Rlim.InvSystemAb) : Ab.{w} ⥤ Type w := colimit (A.op ⋙ coyoneda)
    let P (A : Rlim.InvSystemAb) : Ab.{w} := ∏ᶜ fun n : ℕ ↦ A.obj (op n)
    let shift (A : Rlim.InvSystemAb) : P A ⟶ P A := Pi.lift fun n ↦
      Pi.π (fun n : ℕ ↦ A.obj (op n)) (n + 1) ≫
        A.map (homOfLE (Nat.le_succ n)).op
    let δ (A : Rlim.InvSystemAb) : P A ⟶ P A := 𝟙 (P A) - shift A
    ∃ (mapLim : ∀ A B : Rlim.InvSystemAb,
          (proYoneda B ⟶ proYoneda A) → (limit A ⟶ limit B))
      (mapR1lim : ∀ A B : Rlim.InvSystemAb,
          (proYoneda B ⟶ proYoneda A) →
            (cokernel (δ A) ⟶ cokernel (δ B))),
      (∀ A : Rlim.InvSystemAb, mapLim A A (𝟙 _) = 𝟙 _) ∧
      (∀ A : Rlim.InvSystemAb, mapR1lim A A (𝟙 _) = 𝟙 _) ∧
      (∀ (A B C : Rlim.InvSystemAb) (φ : proYoneda B ⟶ proYoneda A)
          (ψ : proYoneda C ⟶ proYoneda B),
        mapLim A C (ψ ≫ φ) = mapLim A B φ ≫ mapLim B C ψ) ∧
      (∀ (A B C : Rlim.InvSystemAb) (φ : proYoneda B ⟶ proYoneda A)
          (ψ : proYoneda C ⟶ proYoneda B),
        mapR1lim A C (ψ ≫ φ) = mapR1lim A B φ ≫ mapR1lim B C ψ) ∧
      (∀ (A B : Rlim.InvSystemAb) (φ : proYoneda B ⟶ proYoneda A),
        IsIso φ → IsIso (mapLim A B φ) ∧ IsIso (mapR1lim A B φ)) ∧
      (∀ (A B : Rlim.InvSystemAb) (r : SequentialRep A B),
        Rlim.delta A ≫ r.productSecond = r.productFirst ≫ Rlim.delta B) ∧
      (∀ (A : Rlim.InvSystemAb),
        (SequentialRep.id A).productFirst = 𝟙 _ ∧
        (SequentialRep.id A).productSecond = 𝟙 _) ∧
      (∀ (A B C : Rlim.InvSystemAb) (r : SequentialRep A B) (s : SequentialRep B C),
        (r.comp s).productFirst = r.productFirst ≫ s.productFirst ∧
        (r.comp s).productSecond = r.productSecond ≫ s.productSecond) ∧
      (∀ (A B : Rlim.InvSystemAb) (r s : SequentialRep A B),
        r.Refines s → r.mapLim = s.mapLim ∧
          r.productSecond ≫ cokernel.π (Rlim.delta B) =
            s.productSecond ≫ cokernel.π (Rlim.delta B)) ∧
      (∀ (A B : Rlim.InvSystemAb) (φ : proYoneda B ⟶ proYoneda A),
        ∃ r : SequentialRep A B, r.Represents φ) ∧
      (∀ (A B : Rlim.InvSystemAb) (φ : proYoneda B ⟶ proYoneda A)
        (r : SequentialRep A B), r.Represents φ →
        ∃ hδ : Rlim.delta A ≫ r.productSecond =
            r.productFirst ≫ Rlim.delta B,
          mapLim A B φ = r.mapLim ∧
          mapR1lim A B φ = r.mapR1lim hδ ∧
          Rlim.limitToProduct A ≫ r.productFirst =
            mapLim A B φ ≫ Rlim.limitToProduct B ∧
          cokernel.π (Rlim.delta A) ≫ mapR1lim A B φ =
            r.productSecond ≫ cokernel.π (Rlim.delta B)) ∧
      (∀ (A B : Rlim.InvSystemAb) (a : InverseSequence.ProIso A B),
        ∃ (φ : proYoneda B ⟶ proYoneda A),
          proIsoRepresents a φ ∧ IsIso φ ∧
          IsIso (mapLim A B φ) ∧ IsIso (mapR1lim A B φ)) ∧
      (∀ {D : Type u} [Category.{w} D] [HasZeroObject D] [HasShift D ℤ]
          [Preadditive D] [∀ n : ℤ, (shiftFunctor D n).Additive]
          [Pretriangulated D]
          (F G : ℕᵒᵖ ⥤ D)
          [HasProduct fun n : ℕ => F.obj (op n)]
          [HasProduct fun n : ℕ => G.obj (op n)] (L : D)
          (f₁ f₂ : Rlim.Hom.systemProduct F ⟶ Rlim.Hom.systemProduct G)
          (φ₀ : proYoneda (Rlim.Hom.homSystem L G) ⟶
            proYoneda (Rlim.Hom.homSystem L F))
          (φ₁ : proYoneda (Rlim.Hom.shiftedHomSystem L G) ⟶
            proYoneda (Rlim.Hom.shiftedHomSystem L F))
          (r₀ : SequentialRep (Rlim.Hom.homSystem L F)
            (Rlim.Hom.homSystem L G))
          (r₁ : SequentialRep (Rlim.Hom.shiftedHomSystem L F)
            (Rlim.Hom.shiftedHomSystem L G)),
          r₀.Represents φ₀ → r₁.Represents φ₁ →
          r₀.productFirst = Rlim.Hom.homProductMap L F G f₁ →
          r₁.productFirst = Rlim.Hom.shiftedHomProductMap L F G f₁ →
          r₁.productSecond = Rlim.Hom.shiftedHomProductMap L F G f₂ →
          ∃ hδ : Rlim.delta (Rlim.Hom.shiftedHomSystem L F) ≫
              Rlim.Hom.shiftedHomProductMap L F G f₂ =
            Rlim.Hom.shiftedHomProductMap L F G f₁ ≫
              Rlim.delta (Rlim.Hom.shiftedHomSystem L G),
            Rlim.limitToProduct (Rlim.Hom.homSystem L F) ≫
                Rlim.Hom.homProductMap L F G f₁ =
              mapLim _ _ φ₀ ≫
                Rlim.limitToProduct (Rlim.Hom.homSystem L G) ∧
            mapR1lim _ _ φ₁ =
              cokernel.map (Rlim.delta (Rlim.Hom.shiftedHomSystem L F))
                (Rlim.delta (Rlim.Hom.shiftedHomSystem L G))
                (Rlim.Hom.shiftedHomProductMap L F G f₁)
                (Rlim.Hom.shiftedHomProductMap L F G f₂) hδ)
Tag 0919, a lemma

Tag 0919 in the Stacks Project.

Rlim.Hom.hom_into_isDerivedLimit_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/RlimHom.lean, line 419.

Stacks 0919. If K is a derived limit of an inverse system F in a triangulated category, then for every object L there is a short exact sequence 0 ⟶ R¹ lim Hom(L, Fₙ[-1]) ⟶ Hom(L, K) ⟶ lim Hom(L, Fₙ) ⟶ 0.

Here R¹ lim is the cokernel of the 1 - shift endomorphism of the product of the shifted Hom-groups. The arrows are characterized by the connecting map and the triangle inclusion. For a morphism of defining triangles, the resulting Milnor sequences form a commutative diagram with the induced maps on the cokernel and inverse limit.

public theorem hom_into_isDerivedLimit_shortExact
    {D : Type u} [Category.{v} D] [HasZeroObject D] [HasShift D ℤ] [Preadditive D]
    [∀ n : ℤ, (shiftFunctor D n).Additive] [Pretriangulated D]
    (F : ℕᵒᵖ ⥤ D) [HasProduct fun n : ℕ => F.obj (op n)] (K L : D)
    (hK : Pretriangulated.IsDerivedLimit F K) :
    ∃ (t : DerivedLimitTriangle F K) (S : MilnorSequence L F K t),
      ∀ (G : ℕᵒᵖ ⥤ D) [HasProduct fun n : ℕ => G.obj (op n)] (M : D)
        (tG : DerivedLimitTriangle G M) (a : t.triangle ⟶ tG.triangle)
        (b : limit (homSystem L F) ⟶ limit (homSystem L G))
        (_hb : Rlim.limitToProduct (homSystem L F) ≫ homProductMap L F G a.hom₂ =
          b ≫ Rlim.limitToProduct (homSystem L G)),
        ∃ (SG : MilnorSequence L G M tG)
          (hδ : Rlim.delta (shiftedHomSystem L F) ≫
              shiftedHomProductMap L F G a.hom₃ =
            shiftedHomProductMap L F G a.hom₂ ≫ Rlim.delta (shiftedHomSystem L G)),
          (cokernel.map (Rlim.delta (shiftedHomSystem L F))
              (Rlim.delta (shiftedHomSystem L G))
              (shiftedHomProductMap L F G a.hom₂)
              (shiftedHomProductMap L F G a.hom₃) hδ) ≫ SG.inclusion =
            S.inclusion ≫ (preadditiveCoyoneda.obj (op L)).map a.hom₁ ∧
          S.projection ≫ b =
            (preadditiveCoyoneda.obj (op L)).map a.hom₁ ≫ SG.projection
Tag 0H9L, a lemma

Tag 0H9L in the Stacks Project.

Rlim.Pro.nonempty_iso_of_isDerivedLimit_of_pro_isomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ProIsomorphism/DerivedLimit.lean, line 251.

Stacks 0H9L. Derived limits of pro-isomorphic inverse systems in a pretriangulated category are non-canonically isomorphic.

public theorem nonempty_iso_of_isDerivedLimit_of_pro_isomorphism
    {D : Type u} [Category.{v} D] [HasZeroObject D] [HasShift D ℤ] [Preadditive D]
    [∀ n : ℤ, (shiftFunctor D n).Additive] [Pretriangulated D]
    (F G : CategoryTheory.Functor ℕᵒᵖ D) [HasProduct fun n : ℕ => F.obj (op n)]
    [HasProduct fun n : ℕ => G.obj (op n)] (K M : D)
    (hK : Pretriangulated.IsDerivedLimit F K) (hM : Pretriangulated.IsDerivedLimit G M)
    (a : InverseSequence.ProIso F G) : Nonempty (K ≅ M)
Tag 0CQX, a lemma

Tag 0CQX in the Stacks Project.

Rlim.Hom.exists_shortExact_map_from_isHomotopyColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/RlimHom.lean, line 581.

Let F : ℕ ⥤ D be a system in a pretriangulated category and let K be a derived colimit of F. For every L, there is a short exact sequence 0 → R¹ lim Hom(F n, L[-1]) → Hom(K, L) → lim Hom(F n, L) → 0.

Here R¹ lim is written as the cokernel of 1 - shift on the product of the inverse system Hom(F n, L[-1]), using the explicit description of derived inverse limits from Tag 07KW.

public theorem exists_shortExact_map_from_isHomotopyColimit
    {D : Type u} [Category.{v} D] [Preadditive D] [HasZeroObject D] [HasShift D ℤ]
    [∀ n : ℤ, (shiftFunctor D n).Additive] [Pretriangulated D]
    (F : ℕ ⥤ D) [HasCoproduct F.obj] (K L : D) (hK : IsHomotopyColimit F K) :
    let A₀ : ℕᵒᵖ ⥤ AddCommGrpCat.{v} := F.op ⋙ preadditiveYoneda.obj L
    let A₁ : ℕᵒᵖ ⥤ AddCommGrpCat.{v} := F.op ⋙ preadditiveYoneda.obj (L⟦(-1 : ℤ)⟧)
    let P₁ : AddCommGrpCat.{v} := ∏ᶜ fun n : ℕ ↦ A₁.obj (Opposite.op n)
    let shift₁ : P₁ ⟶ P₁ := Pi.lift fun n ↦
      Pi.π (fun n : ℕ ↦ A₁.obj (Opposite.op n)) (n + 1) ≫
        A₁.map (homOfLE (Nat.le_succ n)).op
    let δ₁ : P₁ ⟶ P₁ := 𝟙 P₁ - shift₁
    let H : AddCommGrpCat.{v} := (preadditiveYoneda.obj L).obj (Opposite.op K)
    ∃ (i : cokernel δ₁ ⟶ H) (p : H ⟶ limit A₀) (z : i ≫ p = 0),
      (ShortComplex.mk i p z).ShortExact
Tag 091A, a remark

Tag 091A in the Stacks Project.

Rlim.ChaoticSite.diagramLimitAndRightDerivedIsoSiteCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/RlimSiteCohomology.lean, line 76.

On the chaotic site on a small category, abelian sheaves are diagrams of abelian groups on its opposite category. Under the canonical equivalence, global sections are naturally isomorphic to the limit functor, and for every p the site-cohomology functor is naturally isomorphic to R^p lim.

public noncomputable def diagramLimitAndRightDerivedIsoSiteCohomology
    {C : Type u} [SmallCategory C] :
    let J : GrothendieckTopology C := ⊥
    let e := sheafBotEquivalence (C := C) Ab.{u}
    (e.functor ⋙ (lim : (Cᵒᵖ ⥤ Ab.{u}) ⥤ Ab.{u}) ≅
      Stacks.Cohomology.CompositeRightDerived.siteSections J) ×
      (∀ p : ℕ,
        e.functor ⋙ (lim : (Cᵒᵖ ⥤ Ab.{u}) ⥤ Ab.{u}).rightDerived p ≅
          Stacks.Cohomology.CompositeRightDerived.siteCohomology J p)
Tag 07KX, a lemma

Tag 07KX in the Stacks Project.

Rlim.lim_hasRightDerivedFunctor_and_isDerivedLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/RlimTriangle.lean, line 357.

Stacks 07KX. The right-derived inverse-limit functor on inverse systems of abelian groups is, on every object, a derived limit of the associated inverse system in D(Ab). Equivalently, its value fits in the canonical distinguished triangle R lim K ⟶ ∏ Kₙ ⟶ ∏ Kₙ ⟶ (R lim K)⟦1⟧, where the middle map is 1 - shift.

public theorem lim_hasRightDerivedFunctor_and_isDerivedLimit :
    let F : Rlim.InvSystemAb.{u} ⥤ Ab.{u} := lim
    ∃ (RF : DerivedCategory Rlim.InvSystemAb.{u} ⥤ DerivedCategory Ab.{u})
      (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
        DerivedCategory.Qh ⋙ RF),
      RF.IsRightDerivedFunctor α
        (HomotopyCategory.quasiIso Rlim.InvSystemAb.{u} (ComplexShape.up ℤ)) ∧
      ∀ K : DerivedCategory Rlim.InvSystemAb.{u},
        ∃ _ : HasProduct fun n : ℕ => (derivedEvaluationSystem K).obj (Opposite.op n),
          Pretriangulated.IsDerivedLimit (derivedEvaluationSystem K) (RF.obj K)
Tag 07KY, a lemma

Tag 07KY in the Stacks Project.

DerivedCategory.isDerivedLimit_homology_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/MilnorShortExact.lean, line 273.

The canonical Milnor short exact sequence of a derived limit. The inclusion descends the connecting morphism through the cokernel of 1 - shift in degree r - 1, and the projection to the inverse limit is characterized by the maps to the degree-r cohomologies of the terms.

This is the direct long-exact-sequence argument of Stacks 07KY and 07KZ. It applies to every IsDerivedLimit, independently of any choice of right-derived inverse-limit functor.

public theorem isDerivedLimit_homology_shortExact
    (F : ℕᵒᵖ ⥤ DerivedCategory A) [HasProduct fun n : ℕ => F.obj ⟨n⟩]
    (K : DerivedCategory A) (hK : IsDerivedLimit F K) :
    let X : ℕ → DerivedCategory A := fun n ↦ F.obj (Opposite.op n)
    let d : (∏ᶜ X) ⟶ ∏ᶜ X := Pi.lift fun n : ℕ ↦
      Pi.π X n - Pi.π X (n + 1) ≫ F.map (homOfLE (Nat.le_succ n)).op
    ∃ (a : K ⟶ ∏ᶜ X) (b : (∏ᶜ X) ⟶ K⟦(1 : ℤ)⟧),
      let T := Pretriangulated.Triangle.mk a d b
      T ∈ distTriang (DerivedCategory A) ∧
        ∀ r : ℤ,
          let H := DerivedCategory.homologyFunctor A r
          let H₁ := DerivedCategory.homologyFunctor A (r - 1)
          let homologySystem : ℕᵒᵖ ⥤ A := F ⋙ H
          let shiftedHomologySystem : ℕᵒᵖ ⥤ A := F ⋙ H₁
          let P : A :=
            ∏ᶜ fun n : ℕ ↦ shiftedHomologySystem.obj (Opposite.op n)
          let δ : P ⟶ P := Pi.lift fun n : ℕ ↦
            Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (Opposite.op n)) n -
              Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (Opposite.op n)) (n + 1) ≫
                shiftedHomologySystem.map (homOfLE (Nat.le_succ n)).op
          ∃ (e : H₁.obj (∏ᶜ X) ≅ P)
            (i : cokernel δ ⟶ H.obj K) (q : H.obj K ⟶ limit homologySystem)
            (w : i ≫ q = 0),
            e.hom = piComparison H₁ X ∧
              cokernel.π δ ≫ i = e.inv ≫
                DerivedCategory.HomologySequence.δ T (r - 1) r ∧
              (∀ n : ℕ, q ≫ limit.π homologySystem (Opposite.op n) =
                H.map a ≫ H.map (Pi.π X n)) ∧
              (ShortComplex.mk i q w).ShortExact
Tag 0CQ9, a lemma

Tag 0CQ9 in the Stacks Project.

Stacks.InverseSystem.AbelianGroupDerivedLift.exists_lift_of_inverseSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Ab.lean, line 393.

Stacks Tag 0CQ9 / Lemma 15.88.11. Every inverse system K : Nᵒᵖ ⥤ D(Ab) of objects of the derived category D(Ab) lifts to an object M of D(Ab(N)): there exist an object M of D(Ab(N)) and, for every index n, an isomorphism ψ n : ev_n(M) ≅ K_n in D(Ab), such that for every morphism f : a ⟶ b of Nᵒᵖ the square ev_a(M) → ev_b(M) → K_b and ev_a(M) → K_a → K_b commutes, i.e. the isomorphisms ψ are compatible with the transition maps (the induced transition maps evTrans f of M on the source, the given transition maps K.map f of the system on the target).

theorem exists_lift_of_inverseSystem (K : ℕᵒᵖ ⥤ DerivedCategory Ab.{u}) :
    ∃ (M : DerivedCategory AbN.{u}) (ψ : ∀ n, (evD n).obj M ≅ K.obj n),
      ∀ ⦃a b : ℕᵒᵖ⦄ (f : a ⟶ b),
        (evTrans f).app M ≫ (ψ b).hom = (ψ a).hom ≫ K.map f
Tag 08U5, a remark

Tag 08U5 in the Stacks Project.

Rlim.derivedLimit_iso_rightDerivedLimit_and_homology_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/RlimTriangle.lean, line 514.

Stacks 08U5. Let E be an inverse system in D(Ab) and let K be a derived limit of E. The system has a lift to D(Ab(N)), and the value on every lift of a right-derived inverse-limit functor is isomorphic to K. In particular this value is independent, up to isomorphism, of the chosen lift.

For every p, the defining product triangle of K induces the canonical short exact sequence 0 ⟶ R¹ lim H^(p-1)(Eₙ) ⟶ H^p(K) ⟶ lim H^p(Eₙ) ⟶ 0. The two maps are specified by the connecting morphism and the map from K to the product, respectively.

public theorem derivedLimit_iso_rightDerivedLimit_and_homology_shortExact
(E : Functor ℕᵒᵖ (DerivedCategory Ab.{0})) :
    let F : Functor Rlim.InvSystemAb Ab.{0} := lim
    ∃ (RF : Functor (DerivedCategory Rlim.InvSystemAb) (DerivedCategory Ab.{0}))
      (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
        DerivedCategory.Qh ⋙ RF),
      RF.IsRightDerivedFunctor α
          (HomotopyCategory.quasiIso Rlim.InvSystemAb (ComplexShape.up ℤ)) ∧
        (∃ K : DerivedCategory Ab.{0}, Pretriangulated.IsDerivedLimit E K) ∧
        (∃ (M : DerivedCategory Stacks.InverseSystem.AbelianGroupDerivedLift.AbN)
          (ψ : ∀ n, (Stacks.InverseSystem.AbelianGroupDerivedLift.evD n).obj M ≅ E.obj n),
          ∀ ⦃a b : ℕᵒᵖ⦄ (f : a ⟶ b),
            (Stacks.InverseSystem.AbelianGroupDerivedLift.evTrans f).app M ≫ (ψ b).hom = (ψ a).hom ≫
              E.map f) ∧
        ∀ (K : DerivedCategory Ab.{0}), Pretriangulated.IsDerivedLimit E K →
        (∀ (M : DerivedCategory Stacks.InverseSystem.AbelianGroupDerivedLift.AbN)
            (ψ : ∀ n, (Stacks.InverseSystem.AbelianGroupDerivedLift.evD n).obj M ≅ E.obj n),
            (∀ ⦃a b : ℕᵒᵖ⦄ (f : a ⟶ b),
              (Stacks.InverseSystem.AbelianGroupDerivedLift.evTrans f).app M ≫ (ψ b).hom = (ψ a).hom
                ≫ E.map f) →
            Nonempty (K ≅ RF.obj M)) ∧
        let P := ∏ᶜ fun n : ℕ => E.obj (Opposite.op n)
        let d : P ⟶ P := Pi.lift fun n : ℕ =>
          Pi.π (fun n : ℕ => E.obj (Opposite.op n)) n -
            Pi.π (fun n : ℕ => E.obj (Opposite.op n)) (n + 1) ≫
              E.map (homOfLE (Nat.le_succ n)).op
        ∃ (a : K ⟶ P) (b : P ⟶ K⟦(1 : ℤ)⟧),
          Pretriangulated.Triangle.mk a d b ∈ distTriang (DerivedCategory Ab.{0}) ∧
          ∀ p : ℤ,
            let H : ℤ → Rlim.InvSystemAb := fun q =>
              E ⋙ DerivedCategory.homologyFunctor Ab.{0} q
            let HP : ℤ → Ab.{0} := fun q =>
              (DerivedCategory.homologyFunctor Ab.{0} q).obj P
            let PH : ℤ → Ab.{0} := fun q =>
              ∏ᶜ fun n : ℕ => (H q).obj (Opposite.op n)
            let δH : (q : ℤ) → (PH q ⟶ PH q) := fun q => Rlim.delta (H q)
            let R1lim := Rlim.firstDerivedLimit (H (p - 1))
            let HpK := (DerivedCategory.homologyFunctor Ab.{0} p).obj K
            let limHp := lim.obj (H p)
            let T := Pretriangulated.Triangle.mk a d b
            let connecting : HP (p - 1) ⟶ HpK :=
              (DerivedCategory.homologyFunctor Ab.{0} 0).homologySequenceδ
                T (p - 1) p (by omega)
            ∃ (ePrev : HP (p - 1) ≅ PH (p - 1)) (eCurr : HP p ≅ PH p),
              (∀ n : ℕ, ePrev.hom ≫ Pi.π
                  (fun n : ℕ => (H (p - 1)).obj (Opposite.op n)) n =
                (DerivedCategory.homologyFunctor Ab.{0} (p - 1)).map
                  (Pi.π (fun n : ℕ => E.obj (Opposite.op n)) n)) ∧
              (∀ n : ℕ, eCurr.hom ≫ Pi.π
                  (fun n : ℕ => (H p).obj (Opposite.op n)) n =
                (DerivedCategory.homologyFunctor Ab.{0} p).map
                  (Pi.π (fun n : ℕ => E.obj (Opposite.op n)) n)) ∧
              (DerivedCategory.homologyFunctor Ab.{0} (p - 1)).map d ≫ ePrev.hom =
                ePrev.hom ≫ δH (p - 1) ∧
              (DerivedCategory.homologyFunctor Ab.{0} p).map d ≫ eCurr.hom =
                eCurr.hom ≫ δH p ∧
              ∃ (eLim : limHp ≅ kernel (δH p))
                (hConnecting : δH (p - 1) ≫ ePrev.inv ≫ connecting = 0)
                (hKernel : (DerivedCategory.homologyFunctor Ab.{0} p).map a ≫
                  eCurr.hom ≫ δH p = 0),
                (∀ n : ℕ, eLim.hom ≫ kernel.ι (δH p) ≫
                    Pi.π (fun n : ℕ => (H p).obj (Opposite.op n)) n =
                  limit.π (H p) (Opposite.op n)) ∧
                let i : R1lim ⟶ HpK :=
                  cokernel.desc (δH (p - 1)) (ePrev.inv ≫ connecting) hConnecting
                let q : HpK ⟶ limHp :=
                  kernel.lift (δH p)
                    ((DerivedCategory.homologyFunctor Ab.{0} p).map a ≫ eCurr.hom)
                    hKernel ≫ eLim.inv
                ∃ w : i ≫ q = 0, (ShortComplex.mk i q w).ShortExact
Tag 091B, a lemma

Tag 091B in the Stacks Project.

Rlim.Pro.lim_hasRightDerivedFunctor_and_maps_proIsomorphisms_to_isomorphisms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ProIsomorphism/RightDerivedLimit.lean, line 477.

Stacks 091B. The right-derived inverse-limit functor sends a morphism of derived inverse systems to an isomorphism if the induced morphism between their associated systems in D(Ab) is an isomorphism of pro-objects. Such a pro-isomorphism induces pro-isomorphisms between the cohomology inverse systems in every degree; the displayed degreewise criterion then gives the result.

public theorem lim_hasRightDerivedFunctor_and_maps_proIsomorphisms_to_isomorphisms :
    let F : Functor Rlim.InvSystemAb.{v} Ab.{v} := lim
    ∃ (RF : Functor (DerivedCategory Rlim.InvSystemAb.{v}) (DerivedCategory Ab.{v}))
      (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
        DerivedCategory.Qh ⋙ RF),
      RF.IsRightDerivedFunctor α
          (HomotopyCategory.quasiIso Rlim.InvSystemAb.{v} (ComplexShape.up ℤ)) ∧
        MapsHomologyProIsomorphismsToIsomorphisms RF ∧
        ∀ {E D : DerivedCategory Rlim.InvSystemAb.{v}} (f : E ⟶ D),
          IsProIsomorphismOnDerivedEvaluationSystems f →
            (∀ p : ℤ,
              let H := DerivedCategory.homologyFunctor Rlim.InvSystemAb.{v} p
              IsIso (colim.map
                (Functor.whiskerRight (NatTrans.op (H.map f)) coyoneda))) ∧
            IsIso (RF.map f)
Tag 0CQA, a lemma

Tag 0CQA in the Stacks Project.

Rlim.isMittagLeffler_iff_isZero_rightDerivedLim_one_and_countable_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/MittagLeffler.lean, line 322.

Stacks 0CQA (Emmanouil). An inverse system of abelian groups is Mittag--Leffler if and only if the first derived inverse limit vanishes for it and for the countable direct sum of copies of it.

public theorem isMittagLeffler_iff_isZero_rightDerivedLim_one_and_countable_coproduct
    (A : Rlim.InvSystemAb.{v}) :
    let F : Rlim.InvSystemAb.{v} ⥤ Ab.{v} := lim
    ∀ (RF : DerivedCategory Rlim.InvSystemAb.{v} ⥤ DerivedCategory Ab.{v})
      (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
        DerivedCategory.Qh ⋙ RF),
      RF.IsRightDerivedFunctor α
          (HomotopyCategory.quasiIso Rlim.InvSystemAb.{v} (ComplexShape.up ℤ)) →
        ((A ⋙ forget Ab).IsMittagLeffler ↔
          (IsZero ((DerivedCategory.homologyFunctor Ab.{v} 1).obj
            (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{v} 0).obj A))) ∧
          IsZero ((DerivedCategory.homologyFunctor Ab.{v} 1).obj
            (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{v} 0).obj
              (∐ fun _ : Discrete ℕ => A))))))
Tag 0CQB, a lemma

Tag 0CQB in the Stacks Project.

Declarations registered for the tag:

Tag 091C, a lemma

Tag 091C in the Stacks Project.

Rlim.Pro.isProZero_iff_isZero_lim_and_rightDerivedLim_one_and_countable_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ProIsomorphism/RightDerivedLimit.lean, line 613.

Stacks 091C. An inverse system of abelian groups is zero as a pro-object if and only if its inverse limit and first derived inverse limit vanish, and the same two vanishings hold for the countable direct sum of copies of the system.

public theorem isProZero_iff_isZero_lim_and_rightDerivedLim_one_and_countable_coproduct
    (A : Rlim.InvSystemAb.{u}) :
    let F : Rlim.InvSystemAb.{u} ⥤ Ab.{u} := lim
    ∀ (RF : DerivedCategory Rlim.InvSystemAb.{u} ⥤ DerivedCategory Ab.{u})
      (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
        DerivedCategory.Qh ⋙ RF),
      RF.IsRightDerivedFunctor α
          (HomotopyCategory.quasiIso Rlim.InvSystemAb.{u} (ComplexShape.up ℤ)) →
        ((∀ n : ℕ, ∃ (m : ℕ) (h : n ≤ m), A.map (homOfLE h).op = 0) ↔
          IsZero (limit A) ∧
          IsZero ((DerivedCategory.homologyFunctor Ab.{u} 1).obj
            (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj A))) ∧
          IsZero (limit (∐ fun _ : Discrete ℕ => A)) ∧
          IsZero ((DerivedCategory.homologyFunctor Ab.{u} 1).obj
            (RF.obj ((DerivedCategory.singleFunctor Rlim.InvSystemAb.{u} 0).obj
              (∐ fun _ : Discrete ℕ => A)))))
Sources

Section15.89 Rlim of modules#

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

Tag 091D, a lemma

Tag 091D in the Stacks Project.

ModuleInverseLimit.inverseLimit_hasRightDerivedFunctor_and_computations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleInverseLimitFunctor/TermwiseComputation.lean, line 425.

Stacks 091D. For modules over an inverse system of rings, the inverse-limit functor has a right derived functor on the unbounded derived category. Higher derived limits vanish above degree one; the derived limit of a module system is represented by the two-term product complex with differential (x_n) ↦ (x_n - f_{n+1}(x_{n+1})); Mittag--Leffler systems are right acyclic; every complex has a quasi-isomorphic complex of right-acyclic terms; and a termwise right-acyclic complex computes its derived limit by taking inverse limits termwise. For each right-acyclic system, the canonical limit cone and product differential form a natural short exact sequence.

public theorem inverseLimit_hasRightDerivedFunctor_and_computations
    (rings : ℕᵒᵖ ⥤ RingCat.{u}) :
    let baseRing := limit rings
    let functor : PresheafOfModules.{v} rings ⥤ ModuleCat.{v} baseRing := inverseLimit rings
    let productFamily (system : PresheafOfModules.{v} rings) : ModuleCat.{v} baseRing :=
      ∏ᶜ fun n : ℕ ↦ (moduleDiagram rings system).obj (Opposite.op n)
    let shift (system : PresheafOfModules.{v} rings) : productFamily system ⟶ productFamily system
      := Pi.lift fun n ↦
      Pi.π (fun n : ℕ ↦ (moduleDiagram rings system).obj (Opposite.op n)) (n + 1) ≫
        (moduleDiagram rings system).map (homOfLE (Nat.le_succ n)).op
    let delta (system : PresheafOfModules.{v} rings) : productFamily system ⟶ productFamily system
      := 𝟙 (productFamily system) - shift system
    ∃ (additive : functor.Additive),
      letI := additive
      ∃ (derivedFunctor : DerivedCategory (PresheafOfModules.{v} rings) ⥤
            DerivedCategory (ModuleCat.{v} baseRing))
          (unit : functor.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
            DerivedCategory.Qh ⋙ derivedFunctor),
          derivedFunctor.IsRightDerivedFunctor unit
              (HomotopyCategory.quasiIso (PresheafOfModules.{v} rings) (ComplexShape.up ℤ)) ∧
          (∀ (system : PresheafOfModules.{v} rings) (degree : ℤ), 1 < degree →
            IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} baseRing) degree).obj
              (derivedFunctor.obj ((DerivedCategory.singleFunctor (PresheafOfModules.{v} rings)
                0).obj system)))) ∧
          (∀ system : PresheafOfModules.{v} rings, ∃ (complex : CochainComplex (ModuleCat.{v}
            baseRing) ℤ)
              (zeroIso : complex.X 0 ≅ productFamily system) (oneIso : complex.X 1 ≅ productFamily
                system),
            (∀ index : ℤ, index ≠ 0 → index ≠ 1 → IsZero (complex.X index)) ∧
            zeroIso.inv ≫ complex.d 0 1 ≫ oneIso.hom = delta system ∧
            Nonempty (derivedFunctor.obj
              ((DerivedCategory.singleFunctor (PresheafOfModules.{v} rings) 0).obj system) ≅
                DerivedCategory.Q.obj complex)) ∧
          (∀ system : PresheafOfModules.{v} rings, (system.presheaf ⋙ forget Ab).IsMittagLeffler →
            IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} baseRing) 1).obj
              (derivedFunctor.obj ((DerivedCategory.singleFunctor (PresheafOfModules.{v} rings)
                0).obj system)))) ∧
          (∀ system : PresheafOfModules.{v} rings,
            IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} baseRing) 1).obj
              (derivedFunctor.obj ((DerivedCategory.singleFunctor (PresheafOfModules.{v} rings)
                0).obj system))) →
            ∃ zeroComposition : inverseLimitToProduct rings system ≫ delta system = 0,
              (ShortComplex.mk (inverseLimitToProduct rings system) (delta system)
                zeroComposition).ShortExact) ∧
          (∀ {system targetSystem : PresheafOfModules.{v} rings} (morphism : system ⟶ targetSystem),
            inverseLimitToProduct rings system ≫ productMap rings morphism =
              functor.map morphism ≫ inverseLimitToProduct rings targetSystem ∧
            delta system ≫ productMap rings morphism = productMap rings morphism ≫ delta
              targetSystem) ∧
          (∀ complex : CochainComplex (PresheafOfModules.{v} rings) ℤ,
            ∃ (replacement : CochainComplex (PresheafOfModules.{v} rings) ℤ) (morphism : complex ⟶
              replacement) (_ : QuasiIso morphism),
              ∀ degree : ℤ, IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} baseRing) 1).obj
                (derivedFunctor.obj
                  ((DerivedCategory.singleFunctor (PresheafOfModules.{v} rings) 0).obj
                    (replacement.X degree))))) ∧
          ∀ complex : CochainComplex (PresheafOfModules.{v} rings) ℤ,
            (∀ degree : ℤ, IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} baseRing) 1).obj
              (derivedFunctor.obj
                ((DerivedCategory.singleFunctor (PresheafOfModules.{v} rings) 0).obj (complex.X
                  degree))))) →
            Nonempty (derivedFunctor.obj (DerivedCategory.Q.obj complex) ≅
              DerivedCategory.Q.obj
                ((functor.mapHomologicalComplex (ComplexShape.up ℤ)).obj complex))
Tag 091E, a remark

Tag 091E in the Stacks Project.

ModuleInverseLimitGlobalSections.derivedInverseLimitIsoDerivedGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleInverseLimitGlobalSections.lean, line 667.

On the site ℕ with its bottom topology, module sheaves over an inverse system of rings are compatible inverse systems of modules. Under this equivalence, the right derived inverse-limit functor is canonically the right-derived global-sections functor. After forgetting the module structure, it is canonically the right-derived global-sections functor of the underlying sheaf of abelian groups. The two comparison isomorphisms commute with the respective derived-functor structure transformations.

public theorem derivedInverseLimitIsoDerivedGlobalSections (A : ℕᵒᵖ ⥤ RingCat.{u}) :
    let R := inverseSystemRingSheaf A
    let e : SheafOfModules.{v} R ≌ PresheafOfModules.{v} A := moduleSheafBotEquivalence A
    let B : RingCat.{u} := limit A
    let limMod : PresheafOfModules.{v} A ⥤ ModuleCat.{v} B := ModuleInverseLimit.inverseLimit A
    let Γ : SheafOfModules.{v} R ⥤ ModuleCat.{v} B := e.functor ⋙ limMod
    let ΓAb : Sheaf (⊥ : GrothendieckTopology ℕ) Ab.{v} ⥤ Ab.{v} :=
      sheafToPresheaf (⊥ : GrothendieckTopology ℕ) Ab.{v} ⋙ lim
    ∃ (hE : e.functor.Additive),
      letI := hE
      ∃ (hLim : limMod.Additive),
      letI := hLim
      ∃ (Rlim : DerivedCategory (PresheafOfModules.{v} A) ⥤
            DerivedCategory (ModuleCat.{v} B))
          (α : limMod.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
            DerivedCategory.Qh ⋙ Rlim)
          (hΓ : Γ.Additive),
        letI := hΓ
        ∃ (hΓAb : ΓAb.Additive),
        letI := hΓAb
        ∃ (hToSheafAdd : (SheafOfModules.toSheaf.{v} R).Additive),
        letI := hToSheafAdd
        ∃ (hForgetFiniteColimits :
            PreservesFiniteColimits (forget₂ (ModuleCat.{v} B) Ab.{v})),
        letI := hForgetFiniteColimits
        ∃ (RΓ : DerivedCategory (SheafOfModules.{v} R) ⥤
              DerivedCategory (ModuleCat.{v} B))
            (β : Γ.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
              DerivedCategory.Qh ⋙ RΓ)
          (RΓAb : DerivedCategory (Sheaf (⊥ : GrothendieckTopology ℕ) Ab.{v}) ⥤
              DerivedCategory Ab.{v})
            (γ : ΓAb.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
              DerivedCategory.Qh ⋙ RΓAb)
            (hToSheaf : PreservesFiniteColimits (SheafOfModules.toSheaf.{v} R)),
          letI := hToSheaf
          Rlim.IsRightDerivedFunctor α
              (HomotopyCategory.quasiIso (PresheafOfModules.{v} A) (ComplexShape.up ℤ)) ∧
          RΓ.IsRightDerivedFunctor β
              (HomotopyCategory.quasiIso (SheafOfModules.{v} R) (ComplexShape.up ℤ)) ∧
          RΓAb.IsRightDerivedFunctor γ
              (HomotopyCategory.quasiIso
                (Sheaf (⊥ : GrothendieckTopology ℕ) Ab.{v}) (ComplexShape.up ℤ)) ∧
          ∃ (η : e.functor.mapDerivedCategory ⋙ Rlim ≅ RΓ)
              (θ : Γ ⋙ forget₂ (ModuleCat.{v} B) Ab.{v} ≅
                SheafOfModules.toSheaf.{v} R ⋙ ΓAb)
              (ζ : RΓ ⋙ (forget₂ (ModuleCat.{v} B) Ab.{v}).mapDerivedCategory ≅
                (SheafOfModules.toSheaf.{v} R).mapDerivedCategory ⋙ RΓAb),
            (∀ K,
              β.app K ≫ η.inv.app (DerivedCategory.Qh.obj K) =
                DerivedCategory.Qh.map
                    ((Functor.mapHomotopyCategoryCompIso (Iso.refl Γ)
                      (ComplexShape.up ℤ)).inv.app K) ≫
                  α.app ((e.functor.mapHomotopyCategory (ComplexShape.up ℤ)).obj K) ≫
                  Rlim.map (e.functor.mapDerivedCategoryFactorsh.inv.app K)) ∧
            ∀ K,
              (forget₂ (ModuleCat.{v} B) Ab.{v}).mapDerivedCategoryFactorsh.inv.app
                    ((Γ.mapHomotopyCategory (ComplexShape.up ℤ)).obj K) ≫
                  (forget₂ (ModuleCat.{v} B) Ab.{v}).mapDerivedCategory.map (β.app K) ≫
                  ζ.hom.app (DerivedCategory.Qh.obj K) =
                DerivedCategory.Qh.map
                    ((NatTrans.mapHomotopyCategory θ.hom (ComplexShape.up ℤ)).app K) ≫
                  γ.app (((SheafOfModules.toSheaf.{v} R).mapHomotopyCategory
                    (ComplexShape.up ℤ)).obj K) ≫
                  RΓAb.map
                    ((SheafOfModules.toSheaf.{v} R).mapDerivedCategoryFactorsh.inv.app K)
Tag 0CQD, a lemma

Tag 0CQD in the Stacks Project.

ModuleRightDerivedLimit.rightDerivedInverseLimit_isDerivedLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleRightDerivedLimit.lean, line 405.

Stacks 0CQD. The right-derived inverse-limit functor for compatible modules over an inverse system of rings is, on every object, a derived limit of the associated inverse system in the derived category of modules over the inverse-limit ring. Equivalently, its value fits in the canonical distinguished triangle R lim K ⟶ ∏ Kₙ ⟶ ∏ Kₙ ⟶ (R lim K)⟦1⟧, whose middle map is 1 - shift.

public theorem rightDerivedInverseLimit_isDerivedLimit
    (A : ℕᵒᵖ ⥤ RingCat.{u}) :
    let B := limit A
    let F : PresheafOfModules.{v} A ⥤ ModuleCat.{v} B := ModuleInverseLimit.inverseLimit A
    ∀ (hF : F.Additive),
      letI := hF
      ∀ (RF : DerivedCategory (PresheafOfModules.{v} A) ⥤
            DerivedCategory (ModuleCat.{v} B))
          (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
            DerivedCategory.Qh ⋙ RF),
        RF.IsRightDerivedFunctor α
            (HomotopyCategory.quasiIso (PresheafOfModules.{v} A) (ComplexShape.up ℤ)) →
        ∀ K : DerivedCategory (PresheafOfModules.{v} A),
          ∃ _ : HasProduct fun n : ℕ => (derivedModuleDiagram A K).obj (Opposite.op n),
            Pretriangulated.IsDerivedLimit (derivedModuleDiagram A K) (RF.obj K)
Tag 0CQE, a lemma

Tag 0CQE in the Stacks Project.

ModuleRightDerivedLimit.inverseLimit_hasRightDerivedFunctor_and_homology_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleRightDerivedLimit.lean, line 581.

Stacks 0CQE. For a complex of compatible modules over an inverse system of rings, the long exact cohomology sequence of its canonical derived-limit triangle breaks into short exact sequences 0 ⟶ R¹ lim H^(p-1)(Kₙ) ⟶ H^p(R lim K) ⟶ lim H^p(Kₙ) ⟶ 0.

The displayed maps are the cokernel descent of the connecting morphism and the kernel lift of the following morphism in the long exact sequence.

public theorem inverseLimit_hasRightDerivedFunctor_and_homology_shortExact
    (A : ℕᵒᵖ ⥤ RingCat.{u}) :
    let B := limit A
    let F : PresheafOfModules.{v} A ⥤ ModuleCat.{v} B := ModuleInverseLimit.inverseLimit A
    ∃ (hF : F.Additive),
      letI := hF
      ∃ (RF : DerivedCategory (PresheafOfModules.{v} A) ⥤
            DerivedCategory (ModuleCat.{v} B))
          (α : F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
            DerivedCategory.Qh ⋙ RF),
        RF.IsRightDerivedFunctor α
            (HomotopyCategory.quasiIso (PresheafOfModules.{v} A) (ComplexShape.up ℤ)) ∧
        ∀ K : DerivedCategory (PresheafOfModules.{v} A),
          ∃ _ : HasProduct fun n : ℕ ↦
              (ModuleRightDerivedLimit.derivedModuleDiagram A K).obj (Opposite.op n),
            let E := ModuleRightDerivedLimit.derivedModuleDiagram A K
            let P := ∏ᶜ fun n : ℕ ↦ E.obj (Opposite.op n)
            let d : P ⟶ P := Pi.lift fun n : ℕ ↦
              Pi.π (fun n : ℕ ↦ E.obj (Opposite.op n)) n -
                Pi.π (fun n : ℕ ↦ E.obj (Opposite.op n)) (n + 1) ≫
                  E.map (homOfLE (Nat.le_succ n)).op
            ∃ (a : RF.obj K ⟶ P) (b : P ⟶ (RF.obj K)⟦(1 : ℤ)⟧),
              Pretriangulated.Triangle.mk a d b ∈
                  distTriang (DerivedCategory (ModuleCat.{v} B)) ∧
              ∀ p : ℤ,
                let H : ℤ → PresheafOfModules.{v} A := fun q ↦
                  (DerivedCategory.homologyFunctor (PresheafOfModules.{v} A) q).obj K
                let EH : ℤ → (ℕᵒᵖ ⥤ ModuleCat.{v} B) := fun q ↦
                  E ⋙ DerivedCategory.homologyFunctor (ModuleCat.{v} B) q
                let MH : ℤ → (ℕᵒᵖ ⥤ ModuleCat.{v} B) := fun q ↦
                  ModuleInverseLimit.moduleDiagram A (H q)
                let HP : ℤ → ModuleCat.{v} B := fun q ↦
                  (DerivedCategory.homologyFunctor (ModuleCat.{v} B) q).obj P
                let PH : ℤ → ModuleCat.{v} B := fun q ↦
                  ∏ᶜ fun n : ℕ ↦ (MH q).obj (Opposite.op n)
                let δH : (q : ℤ) → (PH q ⟶ PH q) := fun q ↦ Pi.lift fun n : ℕ ↦
                  Pi.π (fun n : ℕ ↦ (MH q).obj (Opposite.op n)) n -
                    Pi.π (fun n : ℕ ↦ (MH q).obj (Opposite.op n)) (n + 1) ≫
                      (MH q).map (homOfLE (Nat.le_succ n)).op
                let R1lim := (DerivedCategory.homologyFunctor (ModuleCat.{v} B) 1).obj
                  (RF.obj ((DerivedCategory.singleFunctor (PresheafOfModules.{v} A) 0).obj
                    (H (p - 1))))
                let HpRlim :=
                  (DerivedCategory.homologyFunctor (ModuleCat.{v} B) p).obj (RF.obj K)
                let limHp := F.obj (H p)
                let T := Pretriangulated.Triangle.mk a d b
                let connecting : HP (p - 1) ⟶ HpRlim :=
                  (DerivedCategory.homologyFunctor (ModuleCat.{v} B) 0).homologySequenceδ
                    T (p - 1) p (by omega)
                ∃ (eHPrev : EH (p - 1) ≅ MH (p - 1)) (eHCurr : EH p ≅ MH p)
                    (ePrev : HP (p - 1) ≅ PH (p - 1)) (eCurr : HP p ≅ PH p),
                  (∀ n : ℕ, ePrev.hom ≫
                      Pi.π (fun n : ℕ ↦ (MH (p - 1)).obj (Opposite.op n)) n =
                    (DerivedCategory.homologyFunctor (ModuleCat.{v} B) (p - 1)).map
                        (Pi.π (fun n : ℕ ↦ E.obj (Opposite.op n)) n) ≫
                      eHPrev.hom.app (Opposite.op n)) ∧
                  (∀ n : ℕ, eCurr.hom ≫
                      Pi.π (fun n : ℕ ↦ (MH p).obj (Opposite.op n)) n =
                    (DerivedCategory.homologyFunctor (ModuleCat.{v} B) p).map
                        (Pi.π (fun n : ℕ ↦ E.obj (Opposite.op n)) n) ≫
                      eHCurr.hom.app (Opposite.op n)) ∧
                  (DerivedCategory.homologyFunctor (ModuleCat.{v} B) (p - 1)).map d ≫
                      ePrev.hom = ePrev.hom ≫ δH (p - 1) ∧
                  (DerivedCategory.homologyFunctor (ModuleCat.{v} B) p).map d ≫
                      eCurr.hom = eCurr.hom ≫ δH p ∧
                  ∃ (eR1 : R1lim ≅ cokernel (δH (p - 1)))
                    (eLim : limHp ≅ kernel (δH p))
                    (hConnecting : δH (p - 1) ≫ ePrev.inv ≫ connecting = 0)
                    (hKernel : (DerivedCategory.homologyFunctor (ModuleCat.{v} B) p).map a ≫
                      eCurr.hom ≫ δH p = 0),
                    (∀ n : ℕ, eLim.hom ≫ kernel.ι (δH p) ≫
                        Pi.π (fun n : ℕ ↦ (MH p).obj (Opposite.op n)) n =
                      limit.π (MH p) (Opposite.op n)) ∧
                    let i : R1lim ⟶ HpRlim := eR1.hom ≫
                      cokernel.desc (δH (p - 1)) (ePrev.inv ≫ connecting) hConnecting
                    let q : HpRlim ⟶ limHp :=
                      kernel.lift (δH p)
                        ((DerivedCategory.homologyFunctor (ModuleCat.{v} B) p).map a ≫
                          eCurr.hom)
                        hKernel ≫ eLim.inv
                    ∃ w : i ≫ q = 0, (ShortComplex.mk i q w).ShortExact
Tag 091I, a lemma

Tag 091I in the Stacks Project.

Stacks.InverseSystem.ModuleDerivedLift.exists_derivedObject_of_inverseSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Modules.lean, line 1035.

Stacks 091I. Let (A_n) be an inverse system of commutative rings with transition maps f n : A_{n+1} → A_n, let K n be objects of D(A_n), and let φ n : K (n+1) ⟶ (Drestr n).obj (K n) be morphisms in D(A_{n+1}). Then there are an object M of D(Mod(ℕ, (A_n))) and isomorphisms ψ n : (Dcomp n).obj M ≅ K n in D(A_n) such that (transitionNT n).app M ≫ (Drestr n).map (ψ n).hom = (ψ (n+1)).hom ≫ φ n.

theorem exists_derivedObject_of_inverseSystem
    (K : ∀ n, DerivedCategory (ModuleCat.{max u v} (A n)))
    (φ : ∀ n, K (n + 1) ⟶ (Drestr A f n).obj (K n)) :
    ∃ (M : DerivedCategory (PresheafOfModules.{max u v} (Rfun A f)))
      (ψ : ∀ n, (Dcomp A f n).obj M ≅ K n),
      ∀ n, (transitionNT A f n).app M ≫ (Drestr A f n).map (ψ n).hom
        = (ψ (n + 1)).hom ≫ φ n
Tag 07KZ, a remark

Tag 07KZ in the Stacks Project.

ModuleDerivedLimitTriangle.derivedLimit_iso_and_homology_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleDerivedLimitTriangle.lean, line 68.

Stacks 07KZ. Any two derived limits of the same countable inverse system of complexes of modules are isomorphic. Moreover, after exhibiting a derived limit by its defining distinguished triangle, for every r : ℤ there is a canonical short exact sequence 0 ⟶ R¹ lim H⁽ʳ⁻¹⁾(Fₙ) ⟶ Hʳ(K) ⟶ lim Hʳ(Fₙ) ⟶ 0.

Here R¹ lim is the cokernel of 1 - shift. The left map is characterized as the factorization of the connecting map of the defining triangle through that cokernel (using the canonical comparison between the homology of a product and the product of the homologies), and the right map is characterized by all its composites with the limit projections.

public theorem derivedLimit_iso_and_homology_shortExact
    (R : Type u) [Ring R] [HasDerivedCategory.{w} (ModuleCat.{max v u} R)]
    (F : CategoryTheory.Functor ℕᵒᵖ (DerivedCategory (ModuleCat.{max v u} R)))
    [HasProduct fun n : ℕ => F.obj (op n)] :
    (∀ (K K' : DerivedCategory (ModuleCat.{max v u} R)),
      Pretriangulated.IsDerivedLimit F K →
        Pretriangulated.IsDerivedLimit F K' → Nonempty (K ≅ K')) ∧
      ∀ (K : DerivedCategory (ModuleCat.{max v u} R)),
        Pretriangulated.IsDerivedLimit F K →
          let X : ℕ → DerivedCategory (ModuleCat.{max v u} R) := fun n ↦ F.obj (op n)
          let d : (∏ᶜ X) ⟶ ∏ᶜ X := Pi.lift fun n : ℕ ↦
            Pi.π X n - Pi.π X (n + 1) ≫ F.map (homOfLE (Nat.le_succ n)).op
          ∃ (a : K ⟶ ∏ᶜ X) (b : (∏ᶜ X) ⟶ K⟦(1 : ℤ)⟧),
            let T := Pretriangulated.Triangle.mk a d b
            T ∈ distTriang (DerivedCategory (ModuleCat.{max v u} R)) ∧
              ∀ r : ℤ,
                let H := DerivedCategory.homologyFunctor (ModuleCat.{max v u} R) r
                let H₁ := DerivedCategory.homologyFunctor (ModuleCat.{max v u} R) (r - 1)
                let homologySystem : ℕᵒᵖ ⥤ ModuleCat.{max v u} R := F ⋙ H
                let shiftedHomologySystem : ℕᵒᵖ ⥤ ModuleCat.{max v u} R := F ⋙ H₁
                let P : ModuleCat.{max v u} R :=
                  ∏ᶜ fun n : ℕ ↦ shiftedHomologySystem.obj (op n)
                let δ : P ⟶ P := Pi.lift fun n : ℕ ↦
                  Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (op n)) n -
                    Pi.π (fun n : ℕ ↦ shiftedHomologySystem.obj (op n)) (n + 1) ≫
                      shiftedHomologySystem.map (homOfLE (Nat.le_succ n)).op
                ∃ (e : H₁.obj (∏ᶜ X) ≅ P)
                  (i : cokernel δ ⟶ H.obj K) (q : H.obj K ⟶ limit homologySystem)
                  (w : i ≫ q = 0),
                  e.hom = piComparison H₁ X ∧
                    cokernel.π δ ≫ i = e.inv ≫
                      DerivedCategory.HomologySequence.δ T (r - 1) r ∧
                    (∀ n : ℕ, q ≫ limit.π homologySystem (op n) =
                      H.map a ≫ H.map (Pi.π X n)) ∧
                    (ShortComplex.mk i q w).ShortExact
Tag 091F, a lemma

Tag 091F in the Stacks Project.

ModuleSystemRepresentative.exists_representative_with_surjective_transition_maps, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleRepresentatives.lean, line 312.

Stacks 091F. Every object of the derived category of inverse systems of modules over an inverse system of rings is represented by a complex whose transition maps are surjective in every degree.

public theorem exists_representative_with_surjective_transition_maps
    {A : ℕᵒᵖ ⥤ RingCat.{u}}
    [HasDerivedCategory.{w} (PresheafOfModules.{v} A)]
    (K : DerivedCategory (PresheafOfModules.{v} A)) :
    ∃ (M : CochainComplex (PresheafOfModules.{v} A) ℤ)
      (_ : DerivedCategory.Q.obj M ≅ K),
      ∀ (n : ℕ) (i : ℤ),
        Function.Surjective
          ((M.X i).map ((homOfLE (Nat.le_succ n)).op))
Tag 091G, a lemma

Tag 091G in the Stacks Project.

ModuleSystemKFlat.exists_representative_with_kFlat_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleRlimDerived.lean, line 138.

Stacks 091G. Every object of the derived category of inverse systems of modules over an inverse system of commutative rings has a representative whose complex at every index is K-flat.

public theorem exists_representative_with_kFlat_components
    {A : Functor ℕᵒᵖ CommRingCat.{u}}
    [HasDerivedCategory.{w}
      (PresheafOfModules.{u} (A ⋙ forget₂ CommRingCat RingCat))]
    (K : DerivedCategory
      (PresheafOfModules.{u} (A ⋙ forget₂ CommRingCat RingCat))) :
    ∃ (M : CochainComplex
        (PresheafOfModules.{u} (A ⋙ forget₂ CommRingCat RingCat)) ℤ)
      (_ : DerivedCategory.Q.obj M ≅ K),
      ∀ n : ℕ,
        CochainComplex.KFlat
          (show CochainComplex (ModuleCat (A.obj (op n))) ℤ from
            ((PresheafOfModules.evaluation
              (A ⋙ forget₂ CommRingCat RingCat) (op n)).mapHomologicalComplex
                (ComplexShape.up ℤ)).obj M)
Tag 091H, a lemma

Tag 091H in the Stacks Project.

ModuleSystemKFlatComparison.derivedTensorProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleKFlatComparison/DerivedTensor.lean, line 710.

Stacks 091H. The derived category of compatible module systems over an inverse system of commutative rings has a canonical symmetric derived tensor product. A componentwise K-flat representative computes the whole system by pointwise total tensor, compatibly with evaluation at every index. The bifunctor is exact in each variable.

public noncomputable def derivedTensorProduct
    (A : Functor ℕᵒᵖ CommRingCat.{u})
    [HasDerivedCategory.{w}
      (PresheafOfModules.{max u v} (A ⋙ forget₂ CommRingCat RingCat))] :
    DerivedTensorProduct A
Tag 091J, a remark

Tag 091J in the Stacks Project.

ModuleSystemRlimTensor.exists_exactFunctor_isDerivedLimit_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleRlimTensorLimit.lean, line 936.

Stacks 091J. The construction is the composite of the constant-system functor, derived tensor product with a lift of E in the derived category of compatible systems, and derived inverse limit. Its value at K is a derived limit of K ⊗ᴸ[A] Eₙ.

public theorem exists_exactFunctor_isDerivedLimit_tensor
    (A : Type u) [CommRing A]
    (E : ℕᵒᵖ ⥤ CochainComplex.DerivedTensor.DObj A) :
    let AR : ℕᵒᵖ ⥤ CommRingCat.{u} := (Functor.const ℕᵒᵖ).obj (CommRingCat.of A)
    let R : ℕᵒᵖ ⥤ RingCat.{u} := AR ⋙ forget₂ CommRingCat RingCat
    let C := PresheafOfModules.{u} R
    let DA := CochainComplex.DerivedTensor.DObj A
    let DN := DerivedCategory C
    let DB := DerivedCategory (ModuleCat.{u} (limit R : RingCat.{u}))
    let T := CochainComplex.DerivedTensor.canonicalDerivedTensorProduct A
    let S := ModuleSystemKFlatComparison.derivedTensorProduct.{u, u} AR
    let L : C ⥤ ModuleCat.{u} (limit R : RingCat.{u}) := ModuleInverseLimit.inverseLimit R
    ∃ (ρ : (limit R : RingCat.{u}) ≅ RingCat.of A),
      letI : (ModuleCat.restrictScalars.{u} ρ.inv.hom).IsEquivalence :=
        ModuleCat.restrictScalars_isEquivalence_of_ringEquiv
          ρ.symm.ringCatIsoToRingEquiv
      let U : DB ⥤ DA := (ModuleCat.restrictScalars.{u} ρ.inv.hom).mapDerivedCategory
      ∃ (hL : L.Additive),
      letI := hL
      ∃ (Δ : DA ⥤ DN)
        (_ : ∀ n : ℕᵒᵖ,
          Δ ⋙ (PresheafOfModules.evaluation R n).mapDerivedCategory ≅ 𝟭 DA)
        (_ : ∀ K : DA,
          ModuleRightDerivedLimit.derivedModuleDiagram R (Δ.obj K) ⋙ U ≅
            (Functor.const ℕᵒᵖ).obj K)
        (Etilde : DN)
        (_ : ModuleRightDerivedLimit.derivedModuleDiagram R Etilde ⋙ U ≅ E)
        (RF : DN ⥤ DB)
        (α : L.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
          DerivedCategory.Qh ⋙ RF)
        (hRFShift : RF.CommShift ℤ),
        letI := hRFShift
        RF.IsRightDerivedFunctor α
          (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) ∧
        RF.IsTriangulated ∧
        (∀ X : DN, ∃ _ : HasProduct fun n : ℕ ↦
            (ModuleRightDerivedLimit.derivedModuleDiagram R X).obj ⟨n⟩,
          IsDerivedLimit (ModuleRightDerivedLimit.derivedModuleDiagram R X) (RF.obj X)) ∧
        let tensorE := S.tensor.flip.obj Etilde
        ∃ (_ : ∀ n : ℕᵒᵖ,
          tensorE ⋙ (PresheafOfModules.evaluation R n).mapDerivedCategory ≅
            (PresheafOfModules.evaluation R n).mapDerivedCategory ⋙
              T.tensor.flip.obj (E.obj n))
          (_ : ∀ K : DA,
            ModuleRightDerivedLimit.derivedModuleDiagram R (tensorE.obj (Δ.obj K)) ⋙ U ≅
              E ⋙ T.tensor.obj K),
        let F := (Δ ⋙ tensorE) ⋙ RF ⋙ U
        ∃ (hF : F.CommShift ℤ),
          letI := hF
          F.IsTriangulated ∧
            ∀ K, ∃ (_ : HasProduct fun n : ℕ ↦
              (E ⋙ T.tensor.obj K).obj ⟨n⟩),
              IsDerivedLimit (E ⋙ T.tensor.obj K) (F.obj K)
Tag 091K, a lemma

Tag 091K in the Stacks Project.

ModuleSystemRlimTensor.derivedLimit_tensor_mapTriangle_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleRlimTensorLimit.lean, line 1066.

Stacks 091K. The canonical composite Rlim ∘ (ΔK ⊗ᴸ[A] -) from D(ℕ, A) to D(A) is exact. Equivalently, its canonical image of every distinguished triangle is distinguished.

public theorem derivedLimit_tensor_mapTriangle_distinguished
    (A : Type u) [CommRing A]
    (K : CochainComplex.DerivedTensor.DObj A) :
    let AR : ℕᵒᵖ ⥤ CommRingCat.{u} := (Functor.const ℕᵒᵖ).obj (CommRingCat.of A)
    let R : ℕᵒᵖ ⥤ RingCat.{u} := AR ⋙ forget₂ CommRingCat RingCat
    let C := PresheafOfModules.{u} R
    let DA := CochainComplex.DerivedTensor.DObj A
    let DN := DerivedCategory C
    let S := ModuleSystemKFlatComparison.derivedTensorProduct.{u, u} AR
    let L : C ⥤ ModuleCat.{u} (limit R : RingCat.{u}) := ModuleInverseLimit.inverseLimit R
    ∃ (ρ : (limit R : RingCat.{u}) ≅ RingCat.of A),
      letI : (ModuleCat.restrictScalars.{u} ρ.inv.hom).IsEquivalence :=
        ModuleCat.restrictScalars_isEquivalence_of_ringEquiv
          ρ.symm.ringCatIsoToRingEquiv
      let U : DerivedCategory (ModuleCat.{u} (limit R : RingCat.{u})) ⥤ DA :=
        (ModuleCat.restrictScalars.{u} ρ.inv.hom).mapDerivedCategory
      ∃ (hL : L.Additive),
        letI := hL
        ∃ (Δ : DA ⥤ DN)
          (_ : ∀ n : ℕᵒᵖ,
            Δ ⋙ (PresheafOfModules.evaluation R n).mapDerivedCategory ≅ 𝟭 DA)
          (_ : ModuleRightDerivedLimit.derivedModuleDiagram R (Δ.obj K) ⋙ U ≅
            (Functor.const ℕᵒᵖ).obj K)
          (RF : DN ⥤ DerivedCategory (ModuleCat.{u} (limit R : RingCat.{u})))
          (α : L.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
            DerivedCategory.Qh ⋙ RF)
          (hRFShift : RF.CommShift ℤ),
          letI := hRFShift
          RF.IsRightDerivedFunctor α
              (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) ∧
            RF.IsTriangulated ∧
            let tensorK := S.tensor.obj (Δ.obj K)
            let hTensorShift : tensorK.CommShift ℤ := S.commShift_right (Δ.obj K)
            letI := hTensorShift
            let G := tensorK ⋙ RF ⋙ U
            let hGShift : G.CommShift ℤ := inferInstance
            letI := hGShift
            G.IsTriangulated
Tag 091L, a lemma

Tag 091L in the Stacks Project.

ModuleSystemRlimProTensor.derivedLimit_tensor_map_isIso_of_proIsomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/ModuleRlimProTensor.lean, line 622.

If the morphism between the systems in D(A) associated to a morphism in D(ℕ, A) is an isomorphism of pro-objects, then for every K ∈ D(A) the corresponding map between the derived limits of the pointwise derived tensor products is an isomorphism.

public theorem derivedLimit_tensor_map_isIso_of_proIsomorphism
    (A : Type u) [CommRing A]
    {E D : DerivedCategory
      (PresheafOfModules.{u} ((Functor.const ℕᵒᵖ).obj (RingCat.of A)))} (f : E ⟶ D)
    (hf : IsIso (colim.map (Functor.whiskerRight
      (NatTrans.op ((derivedEvaluationFunctor A).map f)) coyoneda)))
    (K : CochainComplex.DerivedTensor.DObj A) :
    let AR : ℕᵒᵖ ⥤ CommRingCat.{u} := (Functor.const ℕᵒᵖ).obj (CommRingCat.of A)
    let R : ℕᵒᵖ ⥤ RingCat.{u} := (Functor.const ℕᵒᵖ).obj (RingCat.of A)
    let C := PresheafOfModules.{u} R
    let DA := CochainComplex.DerivedTensor.DObj A
    let DN := DerivedCategory C
    let S := ModuleSystemKFlatComparison.derivedTensorProduct AR
    let L : C ⥤ ModuleCat.{u} (limit R : RingCat.{u}) := ModuleInverseLimit.inverseLimit R
    ∃ (ρ : (limit R : RingCat.{u}) ≅ RingCat.of A),
      letI : (ModuleCat.restrictScalars.{u} ρ.inv.hom).IsEquivalence :=
        ModuleCat.restrictScalars_isEquivalence_of_ringEquiv
          ρ.symm.ringCatIsoToRingEquiv
      let U : DerivedCategory (ModuleCat.{u} (limit R : RingCat.{u})) ⥤ DA :=
        (ModuleCat.restrictScalars.{u} ρ.inv.hom).mapDerivedCategory
      ∃ (hL : L.Additive),
      letI := hL
      ∃ (Δ : DA ⥤ DN)
        (_ : ModuleRightDerivedLimit.derivedModuleDiagram R (Δ.obj K) ⋙ U ≅
          (Functor.const ℕᵒᵖ).obj K)
        (Rlim : DN ⥤ DerivedCategory (ModuleCat.{u} (limit R : RingCat.{u})))
        (α : L.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh ⟶
          DerivedCategory.Qh ⋙ Rlim),
      Rlim.IsRightDerivedFunctor α
          (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)) ∧
        IsIso ((S.tensor.obj (Δ.obj K) ⋙ Rlim ⋙ U).map f)
Sources

Section15.90 Torsion modules#

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

Tag 05E6, a definition

Tag 05E6 in the Stacks Project.

IsIPowerTorsion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/IPowerTorsion.lean, line 58.

An R-module M is I-power torsion if for every m ∈ M there exists an integer n > 0 such that Iⁿ m = 0, i.e. a • m = 0 for every a ∈ Iⁿ.

def IsIPowerTorsion (R : Type*) [CommSemiring R] (M : Type*) [AddCommMonoid M]
    [Module R M] (I : Ideal R) : Prop

IsElementPowerTorsion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/IPowerTorsion.lean, line 65.

An R-module M is f-power torsion if every element is annihilated by some strictly positive power of f.

def IsElementPowerTorsion (R : Type*) [CommSemiring R] (M : Type*) [AddCommMonoid M]
    [Module R M] (f : R) : Prop
Tag 05E8, a lemma

Tag 05E8 in the Stacks Project.

exists_directSum_quotient_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/IPowerTorsion/Resolution.lean, line 151.

Stacks 05E8. An I-power torsion module admits an exact resolution whose terms are direct sums of quotients of the ring by positive powers of I.

public theorem exists_directSum_quotient_resolution
    (R : Type u) [CommRing R] (I : Ideal R)
    (M : Type v) [AddCommGroup M] [Module R M]
    (hM : IsIPowerTorsion R M I) :
    ∃ (α : ℕ → Type (max u v)) (n : ∀ i, α i → ℕ),
      (∀ i a, 0 < n i a) ∧
        ∃ (d : ∀ i,
            DirectSum (α (i + 1)) (fun a ↦ R ⧸ I ^ n (i + 1) a) →ₗ[R]
              DirectSum (α i) (fun a ↦ R ⧸ I ^ n i a))
          (ε : DirectSum (α 0) (fun a ↦ R ⧸ I ^ n 0 a) →ₗ[R] M),
          Function.Surjective ε ∧ Function.Exact (d 0) ε ∧
            ∀ i, Function.Exact (d (i + 1)) (d i)
Tag 05EA, a lemma

Tag 05EA in the Stacks Project.

torsionBySet_eq_bot_iff_powers_eq_bot_iff_bigLambda_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/IPowerTorsion.lean, line 170.

For a finitely generated ideal I, the following are equivalent: no nonzero element of M is annihilated by I; the same holds for every positive power of I; and, for every finite generating family of I, the canonical map from M to the direct sum of the localizations at those generators is injective.

theorem torsionBySet_eq_bot_iff_powers_eq_bot_iff_bigLambda_injective
    {R : Type u} [CommRing R] (I : Ideal R)
    {M : Type v} [AddCommGroup M] [Module R M] (hI : I.FG) :
    (Submodule.torsionBySet R M (I : Set R) = ⊥ ↔
      ∀ n : ℕ, 1 ≤ n → Submodule.torsionBySet R M ((I ^ n : Ideal R) : Set R) = ⊥) ∧
    ((∀ n : ℕ, 1 ≤ n → Submodule.torsionBySet R M ((I ^ n : Ideal R) : Set R) = ⊥) ↔
      ∀ (t : ℕ) (f : Fin t → R), I = Ideal.span (Set.range f) →
        Function.Injective (bigLambda (M := M) t f))
Tag 05EB, a lemma

Tag 05EB in the Stacks Project.

torsionBySet_quotient_primaryComponent_eq_bot_and_isIPowerTorsion_of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/IPowerTorsion.lean, line 232.

For a finitely generated ideal I, the quotient of any module by its I-primary component has no nonzero elements annihilated by I. Moreover, in a short exact sequence, if the first and third modules are I-power torsion, then so is the middle module.

theorem torsionBySet_quotient_primaryComponent_eq_bot_and_isIPowerTorsion_of_exact
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) :
    (∀ (M : Type v) [AddCommGroup M] [Module R M],
      Submodule.torsionBySet R (M ⧸ (Ideal.primaryComponent M I)) (I : Set R) = ⊥) ∧
    ∀ (M₁ : Type v₁) (M₂ : Type v₂) (M₃ : Type v₃)
      [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂]
      [AddCommGroup M₃] [Module R M₃]
      (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃),
      Function.Injective f → Function.Exact f g → Function.Surjective g →
        IsIPowerTorsion R M₁ I →
        IsIPowerTorsion R M₃ I →
        IsIPowerTorsion R M₂ I
Tag 0A6K, a lemma

Tag 0A6K in the Stacks Project.

isSerreClass_isIPowerTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/IPowerTorsion/SerreClass.lean, line 43.

Stacks 0A6K. The modules annihilated elementwise by positive powers of a finitely generated ideal form a Serre subcategory of the category of modules.

public theorem isSerreClass_isIPowerTorsion
    {R : Type u} [CommRing R] (I : Ideal R) (hI : I.FG) :
    CategoryTheory.ObjectProperty.IsSerreClass
      ((fun M : ModuleCat.{v} R => IsIPowerTorsion R M I) :
        CategoryTheory.ObjectProperty (ModuleCat.{v} R))
Tag 0953, a lemma

Tag 0953 in the Stacks Project.

isIPowerTorsion_iff_support_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/IPowerTorsion.lean, line 108.

Let R be a commutative ring and let I ⊆ R be a finitely generated ideal. Then for every R-module M, M is I-power torsion if and only if Supp(M) ⊆ V(I).

theorem isIPowerTorsion_iff_support_subset
    (R : Type*) [CommRing R] (M : Type*) [AddCommGroup M] [Module R M]
    (I : Ideal R) (hI : I.FG) :
    IsIPowerTorsion R M I ↔
      Module.support R M ⊆ PrimeSpectrum.zeroLocus (I : Set R)
Tag 0H82, a lemma

Tag 0H82 in the Stacks Project.

StacksDraft.PowerTorsionVanishing.positive_homology_derivedTensorProduct_isZero_of_mod_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/TorsionAmplitude.lean, line 672.

Stacks 0H82. If K ⊗ᴸ[R] R / I has no positive cohomology, then positive cohomology also vanishes after derived tensoring K with every positive-power quotient of R, with every I-power-torsion module, and with every bounded, nonpositively concentrated object of D(R) whose cohomology is I-power torsion.

public theorem positive_homology_derivedTensorProduct_isZero_of_mod_ideal
    {R : Type u} [CommRing R] (I : Ideal R)
    (K : DerivedCategory (ModuleCat.{u} R))
    (hK : ∀ i : ℤ, 0 < i →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj
        (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K).obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
            (ModuleCat.of R (R ⧸ I)))))) :
    (∀ (n : ℕ), 0 < n → ∀ i : ℤ, 0 < i →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj
        (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K).obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
            (ModuleCat.of R (R ⧸ I ^ n)))))) ∧
    (∀ (N : ModuleCat.{u} R), IsIPowerTorsion R N I → ∀ i : ℤ, 0 < i →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj
        (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K).obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)))) ∧
    (∀ (M : DerivedCategory.Bounded (ModuleCat.{u} R)),
      (∀ i : ℤ, IsIPowerTorsion R
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj M.obj) I) →
      (∀ i : ℤ, 0 < i →
        IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj M.obj)) →
      ∀ i : ℤ, 0 < i →
        IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj
          (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K).obj
            M.obj)))
Tag 0G1T, a lemma

Tag 0G1T in the Stacks Project.

IPowerTorsionDerivedTensor.derivedTensorProduct_isZero_of_mod_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/IPowerTorsion/TorAmplitude.lean, line 138.

Stacks 0G1T. If K ⊗ᴸ[R] R / I vanishes, then so does the derived tensor product of K with every positive-power quotient of R, every I-power-torsion module, and every bounded derived object with I-power-torsion cohomology.

public theorem derivedTensorProduct_isZero_of_mod_ideal
    {R : Type u} [CommRing R] (I : Ideal R)
    (K : DerivedCategory (ModuleCat.{u} R))
    (hK : IsZero
      (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K).obj
        ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
          (ModuleCat.of R (R ⧸ I))))) :
    (∀ (n : ℕ), 0 < n →
      IsZero
        (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K).obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj
            (ModuleCat.of R (R ⧸ I ^ n))))) ∧
    (∀ (N : ModuleCat.{u} R), IsIPowerTorsion R N I →
      IsZero
        (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K).obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N))) ∧
    (∀ (M : DerivedCategory.Bounded (ModuleCat.{u} R)),
      (∀ i : ℤ, IsIPowerTorsion R
        ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj M.obj) I) →
      IsZero
        (((CochainComplex.DerivedTensor.canonicalDerivedTensorProductFunctor R).obj K).obj
          M.obj))
Tag 0BNK, a lemma

Tag 0BNK in the Stacks Project.

tensorProduct_mk_bijective_of_ideal_power_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/IPowerTorsion/ScalarExtension.lean, line 281. References: SGA 2 IV (4.5), “more general”; SGA 2 IV (4.6), “more general”.

The canonical map from an ideal-power torsion module to its scalar extension is an isomorphism when the scalar extension is unchanged modulo every positive power of the ideal. In particular this holds for the adic completion of a finitely generated ideal; this is a slight generalization of Beauville--Laszlo, Lemme 1.

public theorem tensorProduct_mk_bijective_of_ideal_power_torsion
    (R : Type u) [CommRing R] (I : Ideal R)
    (M : Type w) [AddCommGroup M] [Module R M]
    (hM : ∀ m : M, ∃ n : ℕ, ∀ r ∈ I ^ n, r • m = 0) :
    (∀ (S : Type v) [CommRing S] [Algebra R S],
      (∀ n : ℕ, 0 < n →
        Function.Bijective
          (Ideal.quotientMap (Ideal.map (algebraMap R S) (I ^ n))
            (algebraMap R S) Ideal.le_comap_map)) →
      Function.Bijective (fun m : M => TensorProduct.mk R M S m (1 : S))) ∧
    (I.FG →
      Function.Bijective
        (fun m : M => TensorProduct.mk R M (AdicCompletion I R) m 1))
Sources

Section15.91 Formal glueing of module categories#

Section 15.91 of the Stacks Project, Tag 05E5. 22 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05E7, a lemma

Tag 05E7 in the Stacks Project.

FormalGlueing.flat_and_faithful_on_ideal_torsion_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingFlatIsomorphism.lean, line 269.

Let R → S be a ring map and I an ideal of R. The following are equivalent:

  1. S is flat over R and R/I → S/IS is faithfully flat;
  2. S is flat over R and Spec(S/IS) → Spec(R/I) is surjective;
  3. S is flat over R and tensoring with S is faithful on modules annihilated by I;
  4. S is flat over R and tensoring with S is faithful on I-power torsion modules.
public theorem flat_and_faithful_on_ideal_torsion_tfae
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (I : Ideal R) :
    let q : R ⧸ I →+* S ⧸ I.map (algebraMap R S) :=
      Ideal.quotientMap (I.map (algebraMap R S)) (algebraMap R S) Ideal.le_comap_map
    List.TFAE
      [ Module.Flat R S ∧ RingHom.FaithfullyFlat q,
        Module.Flat R S ∧ Function.Surjective (PrimeSpectrum.comap q),
        Module.Flat R S ∧
          ∀ (M N : Type (max u v)) [AddCommGroup M] [Module R M]
            [AddCommGroup N] [Module R N],
            I ≤ Module.annihilator R M → I ≤ Module.annihilator R N →
              Function.Injective fun f : M →ₗ[R] N ↦ LinearMap.rTensor S f,
        Module.Flat R S ∧
          ∀ (M N : Type (max u v)) [AddCommGroup M] [Module R M]
            [AddCommGroup N] [Module R N],
            IsIPowerTorsion R M I → IsIPowerTorsion R N I →
              Function.Injective fun f : M →ₗ[R] N ↦ LinearMap.rTensor S f ]
Tag 05E9, a lemma

Tag 05E9 in the Stacks Project.

Declarations registered for the tag:

Tag 05EC, a lemma

Tag 05EC in the Stacks Project.

Declarations registered for the tag:

Tag 091M, a lemma

Tag 091M in the Stacks Project.

FormalGlueing.quasiIso_koszulSeq_and_cechComplex_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingKoszulBaseChange.lean, line 431.

If a flat map R → S is an isomorphism modulo a finitely generated ideal I, then for every finite sequence defining the same closed subset as I, the canonical base-change maps on the Koszul complex and on the extended alternating Čech complex are quasi-isomorphisms.

public theorem quasiIso_koszulSeq_and_cechComplex_baseChange
    (R : Type uR) (S : Type uS) [CommRing R] [CommRing S] [Algebra R S]
    (I : Ideal R) (hI : I.FG) (hflat : Module.Flat R S)
    (hquot : Function.Bijective
      (Ideal.quotientMap (I.map (algebraMap R S)) (algebraMap R S) Ideal.le_comap_map))
    {r : ℕ} (f : Fin r → R)
    (hV : PrimeSpectrum.zeroLocus (Ideal.span (Set.range f) : Set R) =
      PrimeSpectrum.zeroLocus (I : Set R)) :
    let liftR := (ModuleCat.uliftFunctor.{uS, uR} R)
    let liftS := (ModuleCat.uliftFunctor.{uR, uS} S)
    let koszulR := (liftR.mapHomologicalComplex (ComplexShape.down ℕ)).obj
      (Koszul.seqComplex f)
    let koszulS := (liftS.mapHomologicalComplex (ComplexShape.down ℕ)).obj
      (Koszul.seqComplex (fun i => algebraMap R S (f i)))
    let cechR := (liftR.mapHomologicalComplex (ComplexShape.up ℕ)).obj
      (Cech.cechComplex f R)
    let cechS := (liftS.mapHomologicalComplex (ComplexShape.up ℕ)).obj
      (Cech.cechComplex (fun i => algebraMap R S (f i)) S)
    ∃ k : koszulR ⟶
          ((ModuleCat.restrictScalars.{max uR uS} (algebraMap R S)).mapHomologicalComplex
            (ComplexShape.down ℕ)).obj koszulS,
      (∀ (n : ℕ) (v : Fin n → (Fin r → R)),
          k.f n (ULift.up (exteriorPower.ιMulti R n v)) =
            ULift.up (exteriorPower.ιMulti S n (fun i j => algebraMap R S (v i j)))) ∧
      QuasiIso k ∧
      ∃ c : cechR ⟶
          ((ModuleCat.restrictScalars.{max uR uS} (algebraMap R S)).mapHomologicalComplex
            (ComplexShape.up ℕ)).obj cechS,
        (∀ (p : ℕ) (s : {t : Finset (Fin r) // t.card = p}) (x : R)
            (y : Cech.cechSub f s.1),
            c.f p
                (ULift.up (DirectSum.lof R {t : Finset (Fin r) // t.card = p}
                  (fun t => Cech.cechMod f R t.1) s
                  (LocalizedModule.mk x y))) =
              ULift.up (DirectSum.lof S {t : Finset (Fin r) // t.card = p}
                (fun t => Cech.cechMod (fun i => algebraMap R S (f i)) S t.1) s
                (LocalizedModule.mk (algebraMap R S x)
                  ⟨algebraMap R S y, by
                    obtain ⟨n, hn⟩ := y.2
                    exact ⟨n, by rw [← hn, map_pow, map_prod]⟩⟩))) ∧
        QuasiIso c
Tag 05ED, a lemma

Tag 05ED in the Stacks Project.

Stacks.RelationsOfSequence.short_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RelationsOfSequence.lean, line 106.

The sequence 0 → K → M → I → 0 is exact: the inclusion K ↪ M and φ are exact at M, and the range of φ is the ideal I = (f_1, …, f_n).

theorem short_exact :
    Function.Exact (K f).subtype (phi f) ∧
      LinearMap.range (phi f) = (idealI f).restrictScalars R

Stacks.RelationsOfSequence.K_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Ideal/RelationsOfSequence.lean, line 142.

The kernel K = ker φ is annihilated by the ideal I = (f_1, …, f_n).

theorem K_annihilated : ∀ a ∈ idealI f, ∀ k ∈ K f, a • k = 0
Tag 05EE, a lemma

Tag 05EE in the Stacks Project.

FormalGlueing.extOne_exact_firstRelationHomology_to_kernelHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingKoszulRelations.lean, line 438.

There is a canonical exact sequence 0 → Ext¹_R(R / (f), N) → H₁(N, f) → Hom_R(K, N), where K is the kernel from Stacks 05ED.

public theorem extOne_exact_firstRelationHomology_to_kernelHom
    (N : Type v) [AddCommGroup N] [Module R N] :
    ∃ i : CategoryTheory.Abelian.Ext
        (ModuleCat.of R (ULift.{max u v} (R ⧸ Stacks.RelationsOfSequence.idealI f)))
        (ModuleCat.of R (ULift.{max u v} N)) 1 →ₗ[R] firstRelationHomology f N,
      (∀ g : Stacks.RelationsOfSequence.idealI f →ₗ[R] N,
          i (idealHomToExtOne f N g) = idealHomToFirstRelationHomology f N g) ∧
        Function.Injective i ∧ Function.Exact i (firstRelationHomologyToKernelHom f N) ∧
        ∀ j : CategoryTheory.Abelian.Ext
            (ModuleCat.of R (ULift.{max u v} (R ⧸ Stacks.RelationsOfSequence.idealI f)))
            (ModuleCat.of R (ULift.{max u v} N)) 1 →ₗ[R] firstRelationHomology f N,
          (∀ g : Stacks.RelationsOfSequence.idealI f →ₗ[R] N,
            j (idealHomToExtOne f N g) = idealHomToFirstRelationHomology f N g) → j = i
Tag 05EF, a lemma

Tag 05EF in the Stacks Project.

FormalGlueing.idealI_le_annihilator_firstRelationHomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingKoszulRelations.lean, line 498.

The ideal generated by a finite family annihilates its first relation homology with coefficients in any module.

public theorem idealI_le_annihilator_firstRelationHomology
    {R : Type u} [CommRing R] {n : ℕ} (f : Fin n → R)
    (N : Type v) [AddCommGroup N] [Module R N] :
    Stacks.RelationsOfSequence.idealI f ≤ Module.annihilator R (FormalGlueing.firstRelationHomology
      f N)
Tag 05EG, a lemma

Tag 05EG in the Stacks Project.

FormalGlueing.exists_shortExactSequence_lift_of_flat_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingFlatIsomorphism.lean, line 1312.

A short exact sequence over S ending in the base change of an I-power torsion module fits below a short exact sequence over R, provided R → S is flat and induces an isomorphism modulo the finitely generated ideal I.

public theorem exists_shortExactSequence_lift_of_flat_baseChange
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    (I : Ideal R) (hI : I.FG) (hflat : Module.Flat R S)
    (hq : Function.Bijective
      (Ideal.quotientMap (I.map (algebraMap R S)) (algebraMap R S) Ideal.le_comap_map))
    (M : Type w) [AddCommGroup M] [Module R M]
    (N : Type x) [AddCommGroup N] [Module R N]
    (hM : IsIPowerTorsion R M I)
    (E' : Type y) [AddCommGroup E'] [Module R E'] [Module S E'] [IsScalarTower R S E']
    (i : TensorProduct R S N →ₗ[S] E')
    (p : E' →ₗ[S] TensorProduct R S M)
    (hi : Function.Injective i) (hp : Function.Surjective p)
    (hexact : Function.Exact i p) :
    ∃ (E : Type (max x (max w y))) (_ : AddCommGroup E) (_ : Module R E)
      (a : N →ₗ[R] E) (b : E →ₗ[R] M) (c : E →ₗ[R] E'),
      Function.Injective a ∧ Function.Exact a b ∧ Function.Surjective b ∧
        c.comp a = (i.restrictScalars R).comp ((TensorProduct.mk R S N) 1) ∧
        ((TensorProduct.mk R S M) 1).comp b = (p.restrictScalars R).comp c
Tag 05EJ, an equation

Tag 05EJ in the Stacks Project.

FormalGlueing.glueingBeta_comp_glueingAlpha, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingComplex/Basic.lean, line 157.

The maps glueingAlpha and glueingBeta form the glueing complex of Stacks Project, Tag 05EJ.

public theorem glueingBeta_comp_glueingAlpha :
    (glueingBeta S f M).comp (glueingAlpha S f M) = 0
Tag 05EK, a lemma

Tag 05EK in the Stacks Project.

FormalGlueing.glueingComplex_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingComplex/Exact.lean, line 429.

If R → S is flat and induces an isomorphism modulo the ideal generated by f, then the glueing complex of every R-module is exact, including at its initial term.

public theorem glueingComplex_exact
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    {r : ℕ} (f : Fin r → R) (M : Type w) [AddCommGroup M] [Module R M]
    (hflat : Module.Flat R S)
    (hq : Function.Bijective
      (Ideal.quotientMap
        ((Ideal.span (Set.range f)).map (algebraMap R S))
        (algebraMap R S) Ideal.le_comap_map)) :
    Function.Injective (glueingAlpha S f M) ∧
      Function.Exact (glueingAlpha S f M) (glueingBeta S f M)
Tag 05EL, a remark

Tag 05EL in the Stacks Project.

FormalGlueing.moduleGlueingConstruction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingCategory/Adjunction.lean, line 166.

The category Glue(R → S, f₁, …, fₜ), its canonical functor from R-modules, and its compatible-sections functor H⁰.

public noncomputable def moduleGlueingConstruction : ModuleGlueingConstruction S f
Tag 0H77, a lemma

Tag 0H77 in the Stacks Project.

FormalGlueing.canonicalSectionsAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingCategory/Adjunction.lean, line 572.

The compatible-sections functor H⁰ on module glueing data is right adjoint to the canonical glueing-data functor.

public noncomputable def canonicalSectionsAdjunction
    {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
    {r : ℕ} (f : Fin r → R)
    (C : FormalGlueing.ModuleGlueingConstruction.{u, v, w} S f) :
    letI := C.category
    C.canonical ⊣ C.sections
Tag 05EM, a lemma

Tag 05EM in the Stacks Project.

FormalGlueing.canonicalSectionsUnit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingEquivalence/LeftQuasiInverse.lean, line 261.

If a flat ring map is an isomorphism modulo the ideal generated by f, then compatible sections are a left quasi-inverse to the canonical module glueing functor.

public theorem canonicalSectionsUnit_isIso
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    {r : ℕ} (f : Fin r → R) (hflat : Module.Flat R S)
    (hq : Function.Bijective
      (Ideal.quotientMap
        ((Ideal.span (Set.range f)).map (algebraMap R S))
        (algebraMap R S) Ideal.le_comap_map)) :
    let c := moduleGlueingConstruction.{u, v, w} S f
    letI := c.category
    IsIso c.canonicalSectionsUnit
Tag 05EN, a lemma

Tag 05EN in the Stacks Project.

FormalGlueing.moduleGlueingConstruction_abelian_exact_preservesColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingCategory/Abelian.lean, line 735.

For a flat ring map, the category of module glueing data is abelian, and the canonical functor from modules is exact and preserves arbitrary colimits.

public theorem moduleGlueingConstruction_abelian_exact_preservesColimits
    {R : Type u} [CommRing R] (S : Type v) [CommRing S] [Algebra R S] [Module.Flat R S]
    {r : ℕ} (f : Fin r → R) :
    let c := moduleGlueingConstruction.{u, v, w} S f
    letI := c.category
    Nonempty (Abelian (ModuleGlueingDatum.{u, v, w} S f c.comparison)) ∧
      exactFunctor (ModuleCat.{max u v w} R)
        (ModuleGlueingDatum.{u, v, w} S f c.comparison) c.canonical ∧
      PreservesColimits c.canonical
Tag 05EP, a lemma

Tag 05EP in the Stacks Project.

FormalGlueing.canonicalFunctor_sections_areQuasiInverse_of_span_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingEquivalence/UnitIdeal.lean, line 303.

If a finite family generates the unit ideal and R → S is flat, then the canonical module glueing functor and compatible sections are quasi-inverse equivalences of categories.

public theorem canonicalFunctor_sections_areQuasiInverse_of_span_eq_top
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    {r : ℕ} (f : Fin r → R) (hflat : Module.Flat R S)
    (hf : Ideal.span (Set.range f) = ⊤) :
    let c := moduleGlueingConstruction.{u, v, w} S f
    letI := c.category
    ∃ e : ModuleCat.{max u v w} R ≌ ModuleGlueingDatum.{u, v, w} S f c.comparison,
      e.functor = c.canonical ∧ e.inverse = c.sections
Tag 05EQ, a lemma

Tag 05EQ in the Stacks Project.

FormalGlueing.exists_baseChange_commuting_with_canonical_and_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingEquivalence/BaseChange.lean, line 544.

Stacks 05EQ. Flat base change defines a functor on module glueing data which commutes, up to natural isomorphism, with the canonical glueing-data functor and compatible global sections. Its generic and local components, including their action on morphisms, are the corresponding scalar-extension functors.

public theorem exists_baseChange_commuting_with_canonical_and_sections
    (R : Type u) (S : Type v) (R' : Type x)
    [CommRing R] [CommRing S] [CommRing R'] [Algebra R S] [Algebra R R']
    {r : ℕ} (f : Fin r → R) (I : Ideal R) (hI : I = Ideal.span (Set.range f))
    (hS : Module.Flat R S) (hR' : Module.Flat R R') :
    let upper := FormalGlueing.moduleGlueingConstruction.{u, v, max u v x w} S f
    let lower := FormalGlueing.moduleGlueingConstruction.{x, max v x, max u v x w}
      (TensorProduct R S R') (fun i ↦ algebraMap R R' (f i))
    letI := upper.category
    letI := lower.category
    let genericMap : S →+* TensorProduct R S R' :=
      Algebra.TensorProduct.includeLeftRingHom
    let localMap : ∀ i, Localization.Away (f i) →+*
        Localization.Away (algebraMap R R' (f i)) := fun i ↦
      IsLocalization.Away.map (Localization.Away (f i))
        (Localization.Away (algebraMap R R' (f i))) (algebraMap R R') (f i)
    ∃ (baseChange :
        FormalGlueing.ModuleGlueingDatum S f upper.comparison ⥤
          FormalGlueing.ModuleGlueingDatum (TensorProduct R S R')
            (fun i ↦ algebraMap R R' (f i)) lower.comparison)
      (genericIso : ∀ X, (baseChange.obj X).generic ≅
        (ModuleCat.extendScalars genericMap).obj X.generic)
      (localIso : ∀ X i, (baseChange.obj X).localPiece i ≅
        (ModuleCat.extendScalars (localMap i)).obj (X.localPiece i))
      (genericLocalizationIso : ∀ X i,
        LocalizedModule.Away
            (algebraMap R' (TensorProduct R S R') (algebraMap R R' (f i)))
            (baseChange.obj X).generic ≃ₗ[TensorProduct R S R']
          TensorProduct S (TensorProduct R S R')
            (LocalizedModule.Away (algebraMap R S (f i)) X.generic))
      (genericLocalTensorIso : ∀ X i,
        TensorProduct R' (TensorProduct R S R')
            (FormalGlueing.restrictFromAway
              (R := R') (fun i ↦ algebraMap R R' (f i)) i
              ((baseChange.obj X).localPiece i)) ≃ₗ[TensorProduct R S R']
          TensorProduct S (TensorProduct R S R')
            (TensorProduct R S
              (FormalGlueing.restrictFromAway (R := R) f i (X.localPiece i))))
      (localOverlapIso : ∀ X i j,
        Cech.cechMod (fun i ↦ algebraMap R R' (f i))
            (FormalGlueing.restrictFromAway
              (R := R') (fun i ↦ algebraMap R R' (f i)) i
              ((baseChange.obj X).localPiece i)) {j} ≃ₗ[R']
          TensorProduct R R'
            (Cech.cechMod f
              (FormalGlueing.restrictFromAway (R := R) f i (X.localPiece i)) {j})),
      (∀ {X Y} (g : X ⟶ Y),
        (lower.homEquiv (baseChange.obj X) (baseChange.obj Y)
              (baseChange.map g)).generic ≫ (genericIso Y).hom =
          (genericIso X).hom ≫
            (ModuleCat.extendScalars genericMap).map
              (upper.homEquiv X Y g).generic) ∧
        (∀ {X Y} (g : X ⟶ Y) i,
          (lower.homEquiv (baseChange.obj X) (baseChange.obj Y)
                (baseChange.map g)).localPiece i ≫ (localIso Y i).hom =
            (localIso X i).hom ≫
              (ModuleCat.extendScalars (localMap i)).map
                ((upper.homEquiv X Y g).localPiece i)) ∧
        (∀ X i (m : X.generic) (t : TensorProduct R S R'),
          genericLocalizationIso X i
              (LocalizedModule.mkLinearMap
                (Submonoid.powers
                  (algebraMap R' (TensorProduct R S R') (algebraMap R R' (f i)))) _
                ((genericIso X).inv (t ⊗ₜ[S] m))) =
            t ⊗ₜ[S]
              LocalizedModule.mkLinearMap
                (Submonoid.powers (algebraMap R S (f i))) _ m) ∧
        (∀ (X : FormalGlueing.ModuleGlueingDatum S f upper.comparison) i,
          letI : Module R (X.localPiece i) :=
            Module.compHom _ (algebraMap R (Localization.Away (f i)))
          ∀ (m : X.localPiece i) (t : TensorProduct R S R'),
          genericLocalTensorIso X i
              (t ⊗ₜ[R'] (localIso X i).inv
                ((1 : Localization.Away (algebraMap R R' (f i)))
                  ⊗ₜ[Localization.Away (f i)] m)) =
            t ⊗ₜ[S] (1 ⊗ₜ[R] m)) ∧
        (∀ (X : FormalGlueing.ModuleGlueingDatum S f upper.comparison) i j,
          letI : Module R (X.localPiece i) :=
            Module.compHom _ (algebraMap R (Localization.Away (f i)))
          ∀ (m : X.localPiece i),
          localOverlapIso X i j
              (LocalizedModule.mkLinearMap
                (Cech.cechSub (fun i ↦ algebraMap R R' (f i)) {j}) _
                ((localIso X i).inv
                  ((1 : Localization.Away (algebraMap R R' (f i)))
                    ⊗ₜ[Localization.Away (f i)] m))) =
            1 ⊗ₜ[R]
              LocalizedModule.mkLinearMap (Cech.cechSub f {j}) _ m) ∧
        (∀ X i d,
          genericLocalTensorIso X i ((baseChange.obj X).alpha i d) =
            TensorProduct.map LinearMap.id (X.alpha i).toLinearMap
              (genericLocalizationIso X i d)) ∧
        (∀ X i j d,
          localOverlapIso X j i ((baseChange.obj X).alphaIJ i j d) =
            TensorProduct.map LinearMap.id (X.alphaIJ i j).toLinearMap
              (localOverlapIso X i j d)) ∧
        Nonempty
          (upper.canonical ⋙ baseChange ≅
            ModuleCat.extendScalars (algebraMap R R') ⋙ lower.canonical) ∧
        Nonempty
          (upper.sections ⋙ ModuleCat.extendScalars (algebraMap R R') ≅
            baseChange ⋙ lower.sections)
Tag 05ER, a proposition

Tag 05ER in the Stacks Project.

FormalGlueing.canonicalFunctor_sections_areQuasiInverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingEquivalence/MainTheorem.lean, line 281.

Stacks 05ER. For a flat ring map inducing an isomorphism modulo the ideal generated by f, the canonical module glueing functor and compatible sections are quasi-inverse equivalences of categories.

public theorem canonicalFunctor_sections_areQuasiInverse
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    {r : ℕ} (f : Fin r → R) (hflat : Module.Flat R S)
    (hq : Function.Bijective
      (Ideal.quotientMap
        ((Ideal.span (Set.range f)).map (algebraMap R S))
        (algebraMap R S) Ideal.le_comap_map)) :
    let c := moduleGlueingConstruction.{u, v, w} S f
    letI := c.category
    ∃ e : ModuleCat.{max u v w} R ≌ ModuleGlueingDatum.{u, v, w} S f c.comparison,
      e.functor = c.canonical ∧ e.inverse = c.sections
Tag 0ALK, a lemma

Tag 0ALK in the Stacks Project.

FormalGlueing.exists_descent_of_idealPowerTorsion_kernel_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingEquivalence/MainTheorem.lean, line 747.

Stacks 0ALK. A map to or from an extended module whose kernel and cokernel are ideal-power torsion descends at the level of its source or target module, with the given map recovered by extension of scalars and with the same kernel and cokernel after restriction of scalars.

public theorem exists_descent_of_idealPowerTorsion_kernel_cokernel
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    (I : Ideal R) (hI : I.FG) (hflat : Module.Flat R S)
    (hq : Function.Bijective
      (Ideal.quotientMap (I.map (algebraMap R S)) (algebraMap R S) Ideal.le_comap_map)) :
    let E := ModuleCat.extendScalars.{u, v, max u v w} (algebraMap R S)
    let U := ModuleCat.restrictScalars.{max u v w} (algebraMap R S)
    (∀ (N : ModuleCat.{max u v w} R) (M' : ModuleCat.{max u v w} S)
      (φ : M' ⟶ E.obj N),
      IsIPowerTorsion S
        (↥(kernel φ : ModuleCat.{max u v w} S)) (I.map (algebraMap R S)) →
      IsIPowerTorsion S
        (↥(cokernel φ : ModuleCat.{max u v w} S)) (I.map (algebraMap R S)) →
      ∃ (M : ModuleCat.{max u v w} R) (ψ : M ⟶ N) (e : E.obj M ≅ M')
          (_eKer : U.obj (kernel φ) ≅ kernel ψ)
          (_eCoker : U.obj (cokernel φ) ≅ cokernel ψ),
        e.hom ≫ φ = E.map ψ) ∧
    (∀ (M : ModuleCat.{max u v w} R) (N' : ModuleCat.{max u v w} S)
      (φ : E.obj M ⟶ N'),
      IsIPowerTorsion S
        (↥(kernel φ : ModuleCat.{max u v w} S)) (I.map (algebraMap R S)) →
      IsIPowerTorsion S
        (↥(cokernel φ : ModuleCat.{max u v w} S)) (I.map (algebraMap R S)) →
      ∃ (N : ModuleCat.{max u v w} R) (ψ : M ⟶ N) (e : E.obj N ≅ N')
          (_eKer : U.obj (kernel φ) ≅ kernel ψ)
          (_eCoker : U.obj (cokernel φ) ≅ cokernel ψ),
        E.map ψ ≫ e.hom = φ)
Tag 05ES, a theorem

Tag 05ES in the Stacks Project.

FormalGlueing.exists_canonicalModuleGlueingEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingModuleProperties/PrincipalLocalization.lean, line 523.

Stacks 05ES. For a flat ring map inducing an isomorphism modulo (f), the canonical functor from modules over the source to pairs of modules identified after localization is an equivalence of categories.

public theorem exists_canonicalModuleGlueingEquivalence
    (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
    (f : R) (hflat : Module.Flat R S)
    (hq : Function.Bijective
      (Ideal.quotientMap
        ((Ideal.span {f}).map (algebraMap R S))
        (algebraMap R S) Ideal.le_comap_map)) :
    let Rf := Localization.Away f
    let Sf := Localization.Away (algebraMap R S f)
    let ρ := principalLocalizationMap R S f
    letI : Algebra Rf Sf := ρ.toAlgebra
    let generic := ModuleCat.extendScalars.{u, v, max u v w} (algebraMap R S)
    let localPiece := ModuleCat.extendScalars.{u, u, max u v w} (algebraMap R Rf)
    let genericOverlap := ModuleCat.extendScalars.{v, v, max u v w} (algebraMap S Sf)
    let localOverlap := ModuleCat.extendScalars.{u, v, max u v w} (algebraMap Rf Sf)
    ∃ comparison : generic ⋙ genericOverlap ≅ localPiece ⋙ localOverlap,
      (∀ (M : ModuleCat.{max u v w} R) (m : M),
        comparison.hom.app M
            ((ModuleCat.extendRestrictScalarsAdj.{max u v w, v, v}
              (algebraMap S Sf)).unit.app
              (generic.obj M)
              ((ModuleCat.extendRestrictScalarsAdj.{max u v w, u, v}
                (algebraMap R S)).unit.app M m)) =
          (ModuleCat.extendRestrictScalarsAdj.{max u v w, u, v}
            (algebraMap Rf Sf)).unit.app
            (localPiece.obj M)
            ((ModuleCat.extendRestrictScalarsAdj.{max u v w, u, u}
              (algebraMap R Rf)).unit.app M m)) ∧
      ((CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback
        genericOverlap localOverlap (ModuleCat.{max u v w} R)).obj
        { fst := generic
          snd := localPiece
          iso := comparison }).IsEquivalence
Tag 05ET, a proposition

Tag 05ET in the Stacks Project.

FormalGlueing.exists_adicCompletionGlueingEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingModuleProperties/AdicCompletion.lean, line 327.

Stacks 05ET. Over a Noetherian ring, finitely generated modules are equivalent to finitely generated modules on the adic completion and on the complementary principal open, identified over their common localization.

public theorem exists_adicCompletionGlueingEquivalence
    (R : Type u) [CommRing R] [IsNoetherianRing R] (f : R) :
    let I := Ideal.span {f}
    let Rhat := AdicCompletion I R
    let Rf := Localization.Away f
    let Sf := Localization.Away (algebraMap R Rhat f)
    let ρ := FormalGlueing.principalLocalizationMap R Rhat f
    letI : Algebra Rf Sf := ρ.toAlgebra
    let completion := finiteAdicCompletion R I
    let localPiece := finiteExtensionOfScalars R Rf
    let completionOverlap := finiteExtensionOfScalars Rhat Sf
    let localOverlap := finiteExtensionOfScalars Rf Sf
    ∃ comparison : completion ⋙ completionOverlap ≅ localPiece ⋙ localOverlap,
      (∀ (M : FGModuleCat.{u} R) (m : M) (s : Sf),
        comparison.hom.app M
            (s ⊗ₜ[Rhat] AdicCompletion.of I M m) =
          s ⊗ₜ[Rf] ((1 : Rf) ⊗ₜ[R] m)) ∧
      ((CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback
        completionOverlap localOverlap (FGModuleCat.{u} R)).obj
        { fst := completion
          snd := localPiece
          iso := comparison }).IsEquivalence
Tag 05EU, a remark

Tag 05EU in the Stacks Project.

FormalGlueing.formalGlueing_preserves_moduleProperties_tensor_and_algebras, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingModuleProperties/Properties.lean, line 608.

Stacks 05EU. Formal glueing detects the standard finiteness and flatness properties, is pointwise symmetric monoidal, and hence induces an equivalence on commutative algebra objects. The final two clauses state property detection, pointwise symmetry, and the canonical commutative algebra equivalence for the principal-localization and adic-completion functors of Tags 05ES and 05ET.

public theorem formalGlueing_preserves_moduleProperties_tensor_and_algebras :
    (∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
      (r : ℕ) (f : Fin r → R) (hflat : Module.Flat R S)
      (hq : Function.Bijective
        (Ideal.quotientMap
          ((Ideal.span (Set.range f)).map (algebraMap R S))
          (algebraMap R S) Ideal.le_comap_map)),
      let c := moduleGlueingConstruction.{u, v, w} S f
      letI := c.category
      let G := ModuleGlueingDatum.{u, v, w} S f c.comparison
      ∃ (sourceTensor : LargeModuleMonoidalStructure.{u, max u v w} R)
          (genericTensor : LargeModuleMonoidalStructure.{v, max u v w} S)
          (localTensor : ∀ i, LargeModuleMonoidalStructure.{u, max u v w}
            (Localization.Away (f i)))
          (glueingTensor : MonoidalCategory G)
          (e : ModuleCat.{max u v w} R ≌ G),
        letI := sourceTensor.monoidal
        letI := genericTensor.monoidal
        letI (i : Fin r) := (localTensor i).monoidal
        letI := sourceTensor.symmetric
        letI := genericTensor.symmetric
        letI (i : Fin r) := (localTensor i).symmetric
        letI := glueingTensor
        ∃ (_ : SymmetricCategory G)
            (_ : (genericProjection S f c).Braided)
            (_ : ∀ i, (localProjection S f c i).Braided)
            (_ : c.canonical.Braided) (_ : c.sections.Braided)
            (_ : e.functor.Braided) (_ : e.inverse.Braided) (_ : e.IsMonoidal),
          e.functor = c.canonical ∧ e.inverse = c.sections ∧
          (∀ M : ModuleCat.{max u v w} R,
            (Module.Finite R M ↔
              Module.Finite S (e.functor.obj M).generic ∧
                ∀ i, Module.Finite (Localization.Away (f i))
                  ((e.functor.obj M).localPiece i)) ∧
            (Module.FinitePresentation R M ↔
              Module.FinitePresentation S (e.functor.obj M).generic ∧
                ∀ i, Module.FinitePresentation (Localization.Away (f i))
                  ((e.functor.obj M).localPiece i)) ∧
            (Module.Flat R M ↔
              Module.Flat S (e.functor.obj M).generic ∧
                ∀ i, Module.Flat (Localization.Away (f i))
                  ((e.functor.obj M).localPiece i)) ∧
            (Module.Projective R M ↔
              Module.Projective S (e.functor.obj M).generic ∧
                ∀ i, Module.Projective (Localization.Away (f i))
                  ((e.functor.obj M).localPiece i))) ∧
          ∃ algebraEquivalence : CommMon (ModuleCat.{max u v w} R) ≌ CommMon G,
            algebraEquivalence = e.mapCommMon) ∧
    (∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
      (f : R) (hflat : Module.Flat R S)
      (hq : Function.Bijective
        (Ideal.quotientMap ((Ideal.span {f}).map (algebraMap R S))
          (algebraMap R S) Ideal.le_comap_map)),
      let Rf := Localization.Away f
      let Sf := Localization.Away (algebraMap R S f)
      let ρ := FormalGlueing.principalLocalizationMap R S f
      letI : Algebra Rf Sf := ρ.toAlgebra
      let generic := ModuleCat.extendScalars.{u, v, max u v w} (algebraMap R S)
      let localPiece := ModuleCat.extendScalars.{u, u, max u v w} (algebraMap R Rf)
      let genericOverlap := ModuleCat.extendScalars.{v, v, max u v w} (algebraMap S Sf)
      let localOverlap := ModuleCat.extendScalars.{u, v, max u v w} (algebraMap Rf Sf)
      ∃ comparison : generic ⋙ genericOverlap ≅ localPiece ⋙ localOverlap,
        (∀ (M : ModuleCat.{max u v w} R) (m : M),
          comparison.hom.app M
              ((ModuleCat.extendRestrictScalarsAdj.{max u v w, v, v}
                (algebraMap S Sf)).unit.app
                (generic.obj M)
                ((ModuleCat.extendRestrictScalarsAdj.{max u v w, u, v}
                  (algebraMap R S)).unit.app M m)) =
            (ModuleCat.extendRestrictScalarsAdj.{max u v w, u, v}
              (algebraMap Rf Sf)).unit.app
              (localPiece.obj M)
              ((ModuleCat.extendRestrictScalarsAdj.{max u v w, u, u}
                (algebraMap R Rf)).unit.app M m)) ∧
        let F := (CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback
          genericOverlap localOverlap (ModuleCat.{max u v w} R)).obj
          { fst := generic, snd := localPiece, iso := comparison }
        ∃ (sourceTensor : LargeModuleMonoidalStructure.{u, max u v w} R)
            (genericTensor : LargeModuleMonoidalStructure.{v, max u v w} S)
            (localTensor : LargeModuleMonoidalStructure.{u, max u v w} Rf)
            (overlapTensor : LargeModuleMonoidalStructure.{v, max u v w} Sf)
            (glueingTensor : MonoidalCategory
              (CategoricalPullback genericOverlap localOverlap))
            (e : ModuleCat.{max u v w} R ≌
              CategoricalPullback genericOverlap localOverlap),
          letI := sourceTensor.monoidal
          letI := genericTensor.monoidal
          letI := localTensor.monoidal
          letI := overlapTensor.monoidal
          letI := sourceTensor.symmetric
          letI := genericTensor.symmetric
          letI := localTensor.symmetric
          letI := overlapTensor.symmetric
          letI := glueingTensor
          ∃ (_ : SymmetricCategory (CategoricalPullback genericOverlap localOverlap))
              (_ : generic.Braided) (_ : localPiece.Braided)
              (_ : genericOverlap.Braided) (_ : localOverlap.Braided)
              (_ : comparison.hom.IsMonoidal)
              (_ : (CategoricalPullback.π₁ genericOverlap localOverlap).Braided)
              (_ : (CategoricalPullback.π₂ genericOverlap localOverlap).Braided)
              (_ : F.Braided) (_ : e.functor.Braided) (_ : e.inverse.Braided)
              (_ : e.IsMonoidal),
            e.functor = F ∧
            (∀ M : ModuleCat.{max u v w} R,
              (Module.Finite R M ↔ Module.Finite S (F.obj M).fst ∧
                Module.Finite Rf (F.obj M).snd) ∧
              (Module.FinitePresentation R M ↔
                Module.FinitePresentation S (F.obj M).fst ∧
                  Module.FinitePresentation Rf (F.obj M).snd) ∧
              (Module.Flat R M ↔ Module.Flat S (F.obj M).fst ∧
                Module.Flat Rf (F.obj M).snd) ∧
              (Module.Projective R M ↔ Module.Projective S (F.obj M).fst ∧
                Module.Projective Rf (F.obj M).snd)) ∧
            ∃ algebraEquivalence : CommMon (ModuleCat.{max u v w} R) ≌
                CommMon (CategoricalPullback genericOverlap localOverlap),
              algebraEquivalence = e.mapCommMon) ∧
    (∀ (R : Type u) [CommRing R] [IsNoetherianRing R] (f : R),
      let I := Ideal.span {f}
      let Rhat := AdicCompletion I R
      let Rf := Localization.Away f
      let Sf := Localization.Away (algebraMap R Rhat f)
      let ρ := FormalGlueing.principalLocalizationMap R Rhat f
      letI : Algebra Rf Sf := ρ.toAlgebra
      let completion := FormalGlueing.finiteAdicCompletion R I
      let localPiece := FormalGlueing.finiteExtensionOfScalars R Rf
      let completionOverlap := FormalGlueing.finiteExtensionOfScalars Rhat Sf
      let localOverlap := FormalGlueing.finiteExtensionOfScalars Rf Sf
      ∃ comparison : completion ⋙ completionOverlap ≅ localPiece ⋙ localOverlap,
        (∀ (M : FGModuleCat.{u} R) (m : M) (s : Sf),
          comparison.hom.app M (s ⊗ₜ[Rhat] AdicCompletion.of I M m) =
            s ⊗ₜ[Rf] ((1 : Rf) ⊗ₜ[R] m)) ∧
        let F := (CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback
          completionOverlap localOverlap (FGModuleCat.{u} R)).obj
          { fst := completion, snd := localPiece, iso := comparison }
        ∃ (glueingTensor : MonoidalCategory
              (CategoricalPullback completionOverlap localOverlap))
            (e : FGModuleCat.{u} R ≌
              CategoricalPullback completionOverlap localOverlap),
          letI := glueingTensor
          ∃ (_ : SymmetricCategory (CategoricalPullback completionOverlap localOverlap))
              (_ : completion.Braided) (_ : localPiece.Braided)
              (_ : completionOverlap.Braided) (_ : localOverlap.Braided)
              (_ : comparison.hom.IsMonoidal)
              (_ : (CategoricalPullback.π₁ completionOverlap localOverlap).Braided)
              (_ : (CategoricalPullback.π₂ completionOverlap localOverlap).Braided)
              (_ : F.Braided) (_ : e.functor.Braided) (_ : e.inverse.Braided)
              (_ : e.IsMonoidal),
            e.functor = F ∧
            (∀ M : FGModuleCat.{u} R,
              (Module.Finite R M ↔ Module.Finite Rhat (F.obj M).fst ∧
                Module.Finite Rf (F.obj M).snd) ∧
              (Module.FinitePresentation R M ↔
                Module.FinitePresentation Rhat (F.obj M).fst ∧
                  Module.FinitePresentation Rf (F.obj M).snd) ∧
              (Module.Flat R M ↔ Module.Flat Rhat (F.obj M).fst ∧
                Module.Flat Rf (F.obj M).snd) ∧
              (Module.Projective R M ↔ Module.Projective Rhat (F.obj M).fst ∧
                Module.Projective Rf (F.obj M).snd)) ∧
            ∃ algebraEquivalence : CommMon (FGModuleCat.{u} R) ≌
                CommMon (CategoricalPullback completionOverlap localOverlap),
              algebraEquivalence = e.mapCommMon)
Tag 05EV, a remark

Tag 05EV in the Stacks Project.

Declarations registered for the tag:

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.