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
Kbelongs to⟨R⟩ₙin the derived category of a ring and a chain ofnmorphisms beginning atKinduces 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
Rstrongly 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
Rbe a regular Noetherian ring of finite dimensiond. IfKandLare bounded-above derivedR-modules, the cohomology ofKvanishes in degrees at mostk, and the cohomology ofLvanishes in degrees at leastk - d + 1, then every morphism fromKtoLis 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
Rbe a regular Noetherian ring of finite positive dimensiond. If a perfect derivedR-moduleKhas zero cohomology in every degree fromk - d + 2throughk, thenKis isomorphic to the biproduct of its truncations in degrees at mostk - d + 1and at leastk + 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 ofR[0]already contains every perfect complex. One may take fornthe global dimension ofR.
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
Rthe following are equivalent:Ris regular of finite Krull dimension; the perfect derived category ofRadmits 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 ofR[0], so the stages of its own envelope are absorbed into those ofR[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-moduleMover a finite type ring mapR → 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
Ris a finitely presentedA-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.
Mis finitely presented relative toR: for some surjectiveR-algebra mapα : R[x_1, …, x_n] → A, the moduleMviewed overR[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
Rbe a ring,φ : A → Ba finite map ofR-algebras with bothR → AandR → Bof finite type, andMaB-module (hence anA-module viaφ). ThenMis finitely presented relative toRas anA-module iff it is finitely presented relative toRas aB-module.The hypothesis
[IsScalarTower R A B]encodes thatA → Bis a map ofR-algebras;[IsScalarTower A B M]encodes that theA-module structure onMis 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
Abe a finite type algebra over a localizationR_f, and letMbe anA-module finitely presented relative toR_f. Forg : Athe localized moduleM_goverA_gis finitely presented relative toR. The compositeR → R_f → Ais given by anAlgebra R Ainstance together with the scalar towerR → 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 → Abe a finite type ring map andManA-module finitely presented relative toR. For any ring mapR → R', setA' := A ⊗[R] R'(anR'-algebra via the right factor and, canonically, anA-algebra via the left factor) andM' := A' ⊗[A] M(anA'-module via the left tensor factorA'). ThenR' → A'is of finite type, andM'is finitely presented relative toR'.
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 → Abe a ring map,ManA-module finitely presented relative toR, andA → A'a ring map of finite presentation. Then theA'-moduleA' ⊗[A] M(hereTensorProduct A A' M, with its naturalA'-module structure) is finitely presented relative toR.The finite type hypothesis on
R → Aof 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 → AandA → Band aB-moduleM, ifMis finitely presented relative toAandAis of finite presentation overR, thenMis finitely presented relative toR.
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 : ι → Agenerates the unit ideal, thenMis finitely presented relative toRexactly when eachM_{f i}is finitely presented relative toRoverA_{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-modules0 → M' →[i] M →[p] M'' → 0(soiis injective,pis surjective andrange i = ker p), ifM'andM''are finitely presented relative toR, thenMis finitely presented relative toR.By Stacks 05GY,
M'andM''are finitely presented overR[x_1, …, x_n]for every presentationα, so one may pick a single presentation and apply two-out-of-three over the polynomial ringR[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-modules0 → M' →[i] M →[p] M'' → 0, ifM'is a finite type (finitely generated)A-module andMis finitely presented relative toR, thenM''is finitely presented relative toR.
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 → Abe a ring map (in Stacks, of finite type — the hypothesis is not needed here) and letM,M'beA-modules. If the direct sumM × M'is finitely presented relative toR, then bothMandM'are finitely presented relative toR.
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] → RevaluatesXat zero, then for everyK ∈ D(R), the derived tensor product ofK, regarded as anR[X]-complex, withRis isomorphic inD(R)toK ⊞ 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)ism-pseudo-coherent overRif and only if, after lettingXact by zero, it ism-pseudo-coherent overR[X].For an object represented by a complex,
Functor.mapDerivedCategoryFactorsidentifies 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-algebraA,m-pseudo-coherence of an object ofD(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.mapDerivedCategoryFactorsidentifies 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)ism-pseudo-coherent relative toRif its restriction of scalars along every finite polynomial presentation ofAoverRism-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 toRif it ism-pseudo-coherent relative toRfor every integerm.
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 ism-pseudo-coherent relative toRif 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 toRif 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 relativem-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 degrees0,-1, and-dis equivalent respectively to finite generation, relative finite presentation, and the existence over every polynomial presentation of a finite free resolution through degreed. 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 relativelym-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, overR_fproduces a complex with the corresponding property relative toR.
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 integerm, as well as relative pseudo-coherence.The chosen
R'-algebraR' ⊗[R] Ais identified with the source'sA ⊗[R] R'byAlgebra.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
Bis pseudo-coherent relative toA, derived extension of scalars fromAtoBpreserves relativem-pseudo-coherence and relative pseudo-coherence over the base ringR.
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
mmeans bounded-above finite homology in degrees at leastm; 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-algebraBis pseudo-coherent ifBis a quotientA[x₁, …, xₙ] ⧸ Iof a polynomial algebra such that theA[x₁, …, xₙ]-moduleA[x₁, …, xₙ] ⧸ Ihas a resolution by finite free modules.This is Stacks 067H (1) in the form of the remark that follows it, with
Breplaced by the isomorphicA[x₁, …, xₙ]-moduleA[x₁, …, xₙ] ⧸ I, which lives in the universe ofA. By Stacks 0675 it says thatA → Bis of finite type and thatB, as a module over itself, is pseudo-coherent relative toA(forAandBin one universe,Algebra.pseudoCoherent_iff_exists_isModuleRelativelyPseudoCoherent). The resolution then exists over every finite polynomial presentation (Algebra.PseudoCoherent.nonempty_finiteFreeModuleResolution). WhenAandBlive in one universe, the condition is the same forBitself, made anA[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 → Bis perfect if it is pseudo-coherent andB, regarded as anA-module, has finite Tor dimension, read off the certified derived tensor productderivedTensoron a model ofD(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 → Bis perfect if and only if there is a presentationB = A[x_1, …, x_n]/Ifor whichB, as a module overA[x_1, …, x_n], admits a finite resolution by finite projectiveA[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 → Abe a pseudo-coherent ring map. An object ofD(A)ism-pseudo-coherent relative toRexactly when it ism-pseudo-coherent, and it is pseudo-coherent relative toRexactly 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 → Aof flat, finitely presentedR-algebras, absolute pseudo-coherence inD(A), relative pseudo-coherence overRand overA, and the two analogous conditions after restriction of scalars toBare equivalent; the same holds form-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 objectKofD(A)is perfect relative toRif it is pseudo-coherent overAand its restriction of scalars has finite Tor dimension overR.
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 ofD(A)perfect relative toRform a strictly full subcategory: relative perfectness is invariant under isomorphism inD(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 ofD(A)perfect relative toRform 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 ofD(A)perfect relative toRform 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 ofD(A)is perfect relative toR: a bounded complex of finite projectiveA-modules representing it is pseudo-coherent by Stacks 064U, and its terms are flat overRby transitivity of flatness, so its restriction toRhas 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 overAof a perfect object ofD(A)with anR-perfect object isR-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 overR(Stacks 0653); the total tensor product of the two is bounded with terms flat overR.
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 ofD(A)is perfect relative toRif and only if it is isomorphic to a finite complex ofA-modules that are flat overRand finitely presented overA.
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
Ais flat and finitely presented overR, then arbitrary base changeR → R'sends anR-perfect object ofD(A)to anR'-perfect object ofD(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 complexKand a complexLof finite Tor-dimension overRadmit representativesPandFfor whichHomᴬ(P, F)is a bounded-below complex ofR-flatA-modules computing derived Hom. The construction commutes with every base changeR → R'. IfAis finitely presented overRandLis perfect relative toR, the terms ofFand of the Hom complex may moreover be chosen finitely presented overA.
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, letR' → Rbe a surjective ring map whose kernel is a nilpotent ideal and setA = A' ⊗[R'] R. If the derived extension of scalars ofK' ∈ D(A')toAis perfect relative toR, thenK'is perfect relative toR'.
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
Abe flat and of finite presentation overR, presented bydvariables, letq ⊂ Abe a prime lying overp ⊂ Rand letK ∈ D(A)be pseudo-coherent. If the cohomology ofK_q ⊗ᴸ_{R_p} κ(p)vanishes outside[a, b], thenK_qhas Tor amplitude in[a - d, b]overR.
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 → Abe a flat ring map of finite presentation and letKbe a pseudo-coherent object ofD(A). ThenKis perfect relative toRif and only ifKis bounded below and, for every primepofR, the derived fibreK ⊗_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
-1and0, 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
-1and0has 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 = 0fori ≤ -3. Letα ∈ Hom_{D(R)}(M, K). Suppose the composite ofαwith the canonical mapK → K^{-2}[2], viewed inHom_{D(R)}(M, K^{-2}[2]) = Ext^2(M, K^{-2}), comes from anR-module homomorphisma : M^{-2} → K^{-2}witha ∘ d_M^{-3} = 0(i.e. equals theD(R)-morphism induced by the chain mapM → (single (-2)).obj (K^{-2})determined bya). Thenαis represented by a morphism of complexesa^• : M → Kwitha^{-2} = a.PROOF SKETCH (Stacks 0ALN, proof of (3)): take
P := exists_projRes, liftαtob : F → Kwithb^{-2} = a ∘ p^{-2}(exists_hom_from_projRes_Q_map_eq), descendbthroughptoab : M → Kwithp ≫ ab = bandab^{-2} = a(exists_hom_comp_projRes_eq). ThenQ.map p ≫ Q.map ab = Q.map b = Q.map p ≫ α, andQ.map pis an iso, soQ.map ab = α. Thisabis 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 = 0fori ≤ -2. Then the canonical mapHom_{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); thenFis K-projective. ByCochainComplex.IsKProjective.Qh_map_bijective, the localization mapQh.map : Hom_{K(R)}(F, K) → Hom_{D(R)}(F, K)is bijective. SinceQ.map pis an isomorphism inD(R)(pa quasi-iso), postcomposition identifiesHom_{D(R)}(F, K) ≅ Hom_{D(R)}(M, K). Byprecomp_quotient_map_projRes_bijective, precomposition with[p]is a bijectionHom_{K(R)}(M, K) → Hom_{K(R)}(F, K). Chasing the square (Qh.mapis natural andtoHomD = 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 = 0fori ∉ {-1, 0}and thatK^0is projective. For a morphism of complexesa : M → K, condition (2a) — that for every moduleNthe induced mapExt^1(a, N) : Ext^1(K, N) → Ext^1(M, N), given by pre-composition withQ.map a, is the zero map — is equivalent to (2b) — the existence of anR-module homomorphismh^0 : M^0 → K^{-1}witha^{-1} + h^0 ∘ d_M^{-1} = 0.PROOF SKETCH: the two implications are
Q_map_comp_eq_zero_of_nullHomotopy((2b)⇒(2a)) andexists_nullHomotopy_of_Q_map_comp_eq_zero((2a)⇒(2b)); assemble withIff.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 complexesa^•witha^{-2} = a(as produced in (3)), for any second representing morphism of complexes(a')^•with(a')^{-2} = a, there existR-module homomorphismsh^0 : M^0 → K^{-1}andh^{-1} : M^{-1} → K^{-2}such thath^{-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)):
abandab'both representα, so bynonempty_homotopy_of_Q_map_eqthey are chain-homotopic; pick a homotopyH. FeedH(and the degree--2agreement) toexists_homotopy_components_of_homotopyto obtainh^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
-1and0, 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
-1of the derived base change: the canonical comparison, transported along the representative isomorphisme, factors throughtruncGEπ (-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 ofD(R)between objects with cohomology in degrees-1and0such thatH⁰(α)is an isomorphism andH⁻¹(α)is surjective. If multiplication byf : Ris zero onK, then it is zero onK'.
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-1and0. If it induces an isomorphism in degree0and an epimorphism in degree-1, then ideal annihilation of every first Ext group forKimplies the same ideal annihilation forK'.
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 ofD(R)with cohomology in degrees-1and0, and letφ : K₁ ⟶ K₂,ψ : K₂ ⟶ K₃. IfH⁰(φ) = 0andH⁻¹(ψ) = 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 → Kis the zero morphism in the derived categoryD(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 ofSoverR.
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 onH⁻¹, 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 → Bbe flat, letA → A'be arbitrary and letB' = A' ⊗[A] Bbe the pushout, so that the square with cornersA, A', B, B'is cocartesian. Then the canonical mapNL_{B/A} ⊗_B B' → NL_{B'/A'}is a quasi-isomorphism, and if in additionNL_{B/A}has Tor amplitude in[-1, 0]then the derived base-change mapNL_{B/A} ⊗_B^L B' → NL_{B'/A'}is a quasi-isomorphism too.The naive cotangent complexes are the two-term complexes
HomologicalComplex.doubleof the canonical presentations, in cohomological degrees-1and0, with their modules and rings lifted to one universe. The map of the first assertion is the displayed chain mapg; 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
-1homology 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))toD(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 oflimandR¹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. IfR¹ limvanishes onA⁻², onA⁻¹, and on the inverse system of degree-1cohomologies, 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
Kis a derived limit of an inverse systemFin a triangulated category, then for every objectLthere is a short exact sequence0 ⟶ R¹ lim Hom(L, Fₙ[-1]) ⟶ Hom(L, K) ⟶ lim Hom(L, Fₙ) ⟶ 0.Here
R¹ limis the cokernel of the1 - shiftendomorphism 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 : ℕ ⥤ Dbe a system in a pretriangulated category and letKbe a derived colimit ofF. For everyL, there is a short exact sequence0 → R¹ lim Hom(F n, L[-1]) → Hom(K, L) → lim Hom(F n, L) → 0.Here
R¹ limis written as the cokernel of1 - shifton the product of the inverse systemHom(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
pthe site-cohomology functor is naturally isomorphic toR^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 triangleR lim K ⟶ ∏ Kₙ ⟶ ∏ Kₙ ⟶ (R lim K)⟦1⟧, where the middle map is1 - 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 - shiftin degreer - 1, and the projection to the inverse limit is characterized by the maps to the degree-rcohomologies 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 categoryD(Ab)lifts to an objectMofD(Ab(N)): there exist an objectMofD(Ab(N))and, for every indexn, an isomorphismψ n : ev_n(M) ≅ K_ninD(Ab), such that for every morphismf : a ⟶ bofNᵒᵖthe squareev_a(M) → ev_b(M) → K_bandev_a(M) → K_a → K_bcommutes, i.e. the isomorphismsψare compatible with the transition maps (the induced transition mapsevTrans fofMon the source, the given transition mapsK.map fof 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
Ebe an inverse system inD(Ab)and letKbe a derived limit ofE. The system has a lift toD(Ab(N)), and the value on every lift of a right-derived inverse-limit functor is isomorphic toK. In particular this value is independent, up to isomorphism, of the chosen lift.For every
p, the defining product triangle ofKinduces the canonical short exact sequence0 ⟶ 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 fromKto 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:
isMittagLeffler_of_shortExact, declared in the repository, registered withadd_to_stacksin StacksFrontier/Homology/DerivedCategory/InverseSystem/MittagLeffler.lean, line 52 (StacksFrontier): “In a short exact sequence of inverse systems of abelian groups indexed by the natural numbers, if the outer two systems are Mittag-Leffler, then the middle system is Mittag-Leffler.”.
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 is1 - 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 mapsf n : A_{n+1} → A_n, letK nbe objects ofD(A_n), and letφ n : K (n+1) ⟶ (Drestr n).obj (K n)be morphisms inD(A_{n+1}). Then there are an objectMofD(Mod(ℕ, (A_n)))and isomorphismsψ n : (Dcomp n).obj M ≅ K ninD(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 sequence0 ⟶ R¹ lim H⁽ʳ⁻¹⁾(Fₙ) ⟶ Hʳ(K) ⟶ lim Hʳ(Fₙ) ⟶ 0.Here
R¹ limis the cokernel of1 - 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
Ein the derived category of compatible systems, and derived inverse limit. Its value atKis a derived limit ofK ⊗ᴸ[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] -)fromD(ℕ, A)toD(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 inD(ℕ, A)is an isomorphism of pro-objects, then for everyK ∈ 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-moduleMisI-power torsion if for everym ∈ Mthere exists an integern > 0such thatIⁿ m = 0, i.e.a • m = 0for everya ∈ 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-moduleMisf-power torsion if every element is annihilated by some strictly positive power off.
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 ofI.
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 ofMis annihilated byI; the same holds for every positive power ofI; and, for every finite generating family ofI, the canonical map fromMto 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 itsI-primary component has no nonzero elements annihilated byI. Moreover, in a short exact sequence, if the first and third modules areI-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
Rbe a commutative ring and letI ⊆ Rbe a finitely generated ideal. Then for everyR-moduleM,MisI-power torsion if and only ifSupp(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 / Ihas no positive cohomology, then positive cohomology also vanishes after derived tensoringKwith every positive-power quotient ofR, with everyI-power-torsion module, and with every bounded, nonpositively concentrated object ofD(R)whose cohomology isI-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 / Ivanishes, then so does the derived tensor product ofKwith every positive-power quotient ofR, everyI-power-torsion module, and every bounded derived object withI-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 → Sbe a ring map andIan ideal ofR. The following are equivalent:
Sis flat overRandR/I → S/ISis faithfully flat;Sis flat overRandSpec(S/IS) → Spec(R/I)is surjective;Sis flat overRand tensoring withSis faithful on modules annihilated byI;Sis flat overRand tensoring withSis faithful onI-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:
IPowerTorsion.baseChange_bijective_iff_quotientMap_bijective, declared in the repository, registered withadd_to_stacksin StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingFlatIsomorphism.lean, line 351 (StacksFrontier): “the base-change criterion on ideal-power torsion modules”.
Tag 05EC, a lemma
Tag 05EC in the Stacks Project.
Declarations registered for the tag:
IPowerTorsion.baseChange_equiv_of_quotientMap_bijective, declared in the repository, registered withadd_to_stacksin StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingFlatIsomorphism.lean, line 377 (StacksFrontier): “the torsion-submodule isomorphism and the equivalence of subcategories”.
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 → Sis an isomorphism modulo a finitely generated idealI, then for every finite sequence defining the same closed subset asI, 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 → 0is exact: the inclusionK ↪ Mandφare exact atM, and the range ofφis the idealI = (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 idealI = (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), whereKis 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
Sending in the base change of anI-power torsion module fits below a short exact sequence overR, providedR → Sis flat and induces an isomorphism modulo the finitely generated idealI.
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
glueingAlphaandglueingBetaform 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 → Sis flat and induces an isomorphism modulo the ideal generated byf, then the glueing complex of everyR-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 fromR-modules, and its compatible-sections functorH⁰.
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 → Sis 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:
TopCat.Sheaf.sheafEquivGlueData, declared in the repository, registered withadd_to_stacksin StacksFrontier/RingTheory/Localization/Glueing/FormalGlueingEquivalence/MainTheorem.lean, line 811 (StacksFrontier).
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.