15.92 The Beauville-Laszlo… to 15.105 Tricks with double…
Section15.92 The Beauville-Laszlo theorem#
Section 15.92 of the Stacks Project, Tag 0BNI. 27 tags here are carried by 27 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BNJ, a lemma
Tag 0BNJ in the Stacks Project.
BeauvilleLaszlo.quotient_pow_equiv_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/Covering.lean, line 84.
The canonical map
R / f^n R → R^∧ / f^n R^∧is an isomorphism, whereR^∧is the(f)-adic completion.
public theorem quotient_pow_equiv_adicCompletion {R : Type*} [CommRing R]
(f : R) (n : ℕ) :
∃ e : (R ⧸ (Ideal.span {f}) ^ n) ≃+*
(AdicCompletion (Ideal.span {f}) R ⧸
(Ideal.span {(algebraMap R (AdicCompletion (Ideal.span {f}) R)) f}) ^ n),
∀ r : R,
e (Ideal.Quotient.mk _ r) =
Ideal.Quotient.mk _ ((algebraMap R (AdicCompletion (Ideal.span {f}) R)) r)
Tag 0BNL, a lemma
Tag 0BNL in the Stacks Project.
BeauvilleLaszlo.tensorProduct_prod_away_nontrivial_of_quotientMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/Covering.lean, line 177.
If
R → Sinduces isomorphisms modulo every positive power of(f), then tensoring withS ⊕ R_fdetects nonzero modules. In particular, tensoring withR^∧ ⊕ R_f, whereR^∧is the(f)-adic completion, detects nonzero modules.
public theorem tensorProduct_prod_away_nontrivial_of_quotientMap_bijective
(R : Type u) [CommRing R] (f : R) :
(∀ (S : Type v) [CommRing S] [Algebra R S],
(∀ n : ℕ, 0 < n →
Function.Bijective
(Ideal.quotientMap
(Ideal.map (algebraMap R S) ((Ideal.span {f}) ^ n))
(algebraMap R S) Ideal.le_comap_map)) →
∀ (M : Type w) [AddCommGroup M] [Module R M] [Nontrivial M],
Nontrivial (TensorProduct R M (S × Localization.Away f))) ∧
(∀ (M : Type w) [AddCommGroup M] [Module R M] [Nontrivial M],
Nontrivial
(TensorProduct R M
(AdicCompletion (Ideal.span {f}) R × Localization.Away f)))
Tag 0BNM, a lemma
Tag 0BNM in the Stacks Project.
BeauvilleLaszlo.primeSpectrum_cover_of_quotientMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/Covering.lean, line 273.
If
R → Sis an isomorphism modulof, thenSpec(S)andSpec(R_f)jointly coverSpec(R). The same cover holds with the(f)-adic completion in place ofS.
public theorem primeSpectrum_cover_of_quotientMap_bijective {R : Type*} [CommRing R] (f : R) :
(∀ {S : Type*} [CommRing S] (φ : R →+* S),
Function.Bijective
(Ideal.quotientMap (Ideal.map φ (Ideal.span {f})) φ Ideal.le_comap_map) →
Function.Surjective
(Sum.elim (PrimeSpectrum.comap φ)
(PrimeSpectrum.comap (algebraMap R (Localization.Away f))))) ∧
Function.Surjective
(Sum.elim
(PrimeSpectrum.comap
(algebraMap R (AdicCompletion (Ideal.span {f}) R)))
(PrimeSpectrum.comap (algebraMap R (Localization.Away f))))
Tag 0BNN, a lemma
Tag 0BNN in the Stacks Project.
BeauvilleLaszlo.finite_iff_tensorProduct_prod_away_of_quotientMap_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/Covering.lean, line 337.
Finite generation of a module is detected after extension of scalars to the product of an algebra inducing isomorphisms modulo every positive power of
(f)and the localization away fromf. In particular, it is detected by the product of the(f)-adic completion and that localization.
public theorem finite_iff_tensorProduct_prod_away_of_quotientMap_bijective
(R : Type u) [CommRing R] (f : R) :
(∀ (S : Type v) [CommRing S] [Algebra R S],
(∀ n : ℕ, 0 < n →
Function.Bijective
(Ideal.quotientMap
(Ideal.map (algebraMap R S) ((Ideal.span {f}) ^ n))
(algebraMap R S) Ideal.le_comap_map)) →
∀ (M : Type w) [AddCommGroup M] [Module R M],
Module.Finite R M ↔
Module.Finite (S × Localization.Away f)
(TensorProduct R (S × Localization.Away f) M)) ∧
(∀ (M : Type w) [AddCommGroup M] [Module R M],
Module.Finite
(AdicCompletion (Ideal.span {f}) R × Localization.Away f)
(TensorProduct R
(AdicCompletion (Ideal.span {f}) R × Localization.Away f) M) →
Module.Finite R M)
Tag 0BNP, a remark
Tag 0BNP in the Stacks Project.
BeauvilleLaszlo.exists_nonflat_adicCompletion_prod_localizationAway, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingPair.lean, line 1364.
Stacks 0BNP. Adic completion and localization do not in general form a flat cover: there is a commutative ring
Rand an elementfsuch that the product of the completion ofRat(f)andR_fis not flat overR.
public theorem exists_nonflat_adicCompletion_prod_localizationAway :
∃ (R : Type) (_ : CommRing R) (f : R),
¬ Module.Flat R
(AdicCompletion (Ideal.span ({f} : Set R)) R × Localization.Away f)
Tag 0F1Q, an equation
Tag 0F1Q in the Stacks Project.
BeauvilleLaszlo.beauvilleLaszloSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingPair.lean, line 142.
The canonical sequence
0 → R → S ⊕ Rₑ → Sₓ → 0, whose right-hand map is the difference of the two canonical localization maps.
public noncomputable def beauvilleLaszloSequence (f : R) (φ : R →+* S) :
ShortComplex AddCommGrpCat.{max u v}
Tag 0BNQ, an equation
Tag 0BNQ in the Stacks Project.
BeauvilleLaszlo.adicCompletionBeauvilleLaszloSequence, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingPair.lean, line 173.
The canonical sequence
0 → R → R̂ ⊕ Rₑ → R̂ₑ → 0, whereR̂is the completion ofRalong the principal ideal generated byf.
public noncomputable abbrev adicCompletionBeauvilleLaszloSequence
(R : Type u) [CommRing R] (f : R) : ShortComplex AddCommGrpCat.{u}
Tag 0BNR, a lemma
Tag 0BNR in the Stacks Project.
BeauvilleLaszlo.beauvilleLaszloSequence_exactness_iff_powerTorsionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingPair.lean, line 433.
If
R → Sis an isomorphism modulo every positive power off, the Beauville--Laszlo sequence is always exact on the right; its left and middle exactness are equivalent to injectivity and surjectivity onf-power torsion. Consequently it is short exact precisely when that map is bijective. The same criterion specializes to the(f)-adic completion ofR.
public theorem beauvilleLaszloSequence_exactness_iff_powerTorsionMap
(f : R) (φ : R →+* S)
(hφ : ∀ n : ℕ, 0 < n → Function.Bijective (quotientPowMap f n φ)) :
Epi (beauvilleLaszloSequence f φ).g ∧
(Mono (beauvilleLaszloSequence f φ).f ↔
Function.Injective (powerTorsionMap f φ)) ∧
((beauvilleLaszloSequence f φ).Exact ↔
Function.Surjective (powerTorsionMap f φ)) ∧
((beauvilleLaszloSequence f φ).ShortExact ↔
Function.Bijective (powerTorsionMap f φ)) ∧
((beauvilleLaszloSequence f
(algebraMap R (AdicCompletion (Ideal.span {f}) R))).ShortExact ↔
Function.Bijective (powerTorsionMap f
(algebraMap R (AdicCompletion (Ideal.span {f}) R))))
Tag 0BNS, a remark
Tag 0BNS in the Stacks Project.
BeauvilleLaszlo.adicCompletion_isRegular_and_isGlueingPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingPair.lean, line 520.
A nonzerodivisor
fremains a nonzerodivisor in the(f)-adic completion, and the canonical Beauville--Laszlo sequence is short exact; equivalently,(R, f)is a glueing pair.
public theorem adicCompletion_isRegular_and_isGlueingPair {R : Type*} [CommRing R] (f : R) (hf :
IsRegular f) :
IsRegular (algebraMap R (AdicCompletion (Ideal.span {f}) R) f) ∧
(beauvilleLaszloSequence f
(algebraMap R (AdicCompletion (Ideal.span {f}) R))).ShortExact
Tag 0BNT, a remark
Tag 0BNT in the Stacks Project.
BeauvilleLaszlo.adicCompletion_isGlueingPair_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingPair.lean, line 558.
If the
(f)-adic completion ofRis flat overR, then tensoring the exact sequence given by multiplication byf ^ nremains exact for every positiven, the canonical map onf ^ n-torsion is an isomorphism, and(R, f)is a glueing pair. These conclusions hold in particular whenRis Noetherian.
public theorem adicCompletion_isGlueingPair_of_flat {R : Type u} [CommRing R] (f : R) :
let P : Prop :=
(∀ n : ℕ, 0 < n →
let T := Submodule.torsionBy R R (f ^ n)
let a : T ⊗[R] AdicCompletion (Ideal.span {f}) R →ₗ[R]
AdicCompletion (Ideal.span {f}) R :=
(TensorProduct.lid R (AdicCompletion (Ideal.span {f}) R)).toLinearMap.comp
(TensorProduct.map T.subtype
(LinearMap.id (R := R) (M := AdicCompletion (Ideal.span {f}) R)))
let b : AdicCompletion (Ideal.span {f}) R →ₗ[R]
AdicCompletion (Ideal.span {f}) R :=
(LinearMap.lsmul R (AdicCompletion (Ideal.span {f}) R)) (f ^ n)
Function.Injective a ∧ Function.Exact a b ∧
Function.Injective
(fun x : T => algebraMap R (AdicCompletion (Ideal.span {f}) R) x.1) ∧
Set.range (fun x : T => algebraMap R (AdicCompletion (Ideal.span {f}) R) x.1) =
(Submodule.torsionBy (AdicCompletion (Ideal.span {f}) R)
(AdicCompletion (Ideal.span {f}) R)
((algebraMap R (AdicCompletion (Ideal.span {f}) R) f) ^ n) :
Set (AdicCompletion (Ideal.span {f}) R))) ∧
Function.Injective (fun r : R =>
(algebraMap R (AdicCompletion (Ideal.span {f}) R) r,
algebraMap R (Localization.Away f) r)) ∧
Function.Exact
(fun r : R => (algebraMap R (AdicCompletion (Ideal.span {f}) R) r,
algebraMap R (Localization.Away f) r))
(fun x : AdicCompletion (Ideal.span {f}) R × Localization.Away f =>
algebraMap (AdicCompletion (Ideal.span {f}) R)
(Localization.Away
(algebraMap R (AdicCompletion (Ideal.span {f}) R) f)) x.1 -
Localization.awayMap
(algebraMap R (AdicCompletion (Ideal.span {f}) R)) f x.2) ∧
Function.Surjective
(fun x : AdicCompletion (Ideal.span {f}) R × Localization.Away f =>
algebraMap (AdicCompletion (Ideal.span {f}) R)
(Localization.Away
(algebraMap R (AdicCompletion (Ideal.span {f}) R) f)) x.1 -
Localization.awayMap
(algebraMap R (AdicCompletion (Ideal.span {f}) R)) f x.2)
(Module.Flat R (AdicCompletion (Ideal.span {f}) R) → P) ∧
(∀ [IsNoetherianRing R], P)
Tag 0BNU, an example
Tag 0BNU in the Stacks Project.
BeauvilleLaszlo.adicCompletion_torsionMap_not_bijective_examples, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingPair.lean, line 1288.
Two quotients of
k[f, T₁, T₂, …]for which the canonical map onf-power torsion to the adic completion is respectively noninjective and nonsurjective. In the first exampleT₁is a nonzero kernel element whose image is divisible by every power off. In the second, the compatible residues ofT₁ + f T₂ + f² T₃ + ⋯define anf-torsion element outside the image. The two completion maps are not flat.
public theorem adicCompletion_torsionMap_not_bijective_examples (k : Type*) [Field k] :
let P := MvPolynomial (Option ℕ) k
let F : P := MvPolynomial.X none
let T : ℕ → P := fun n ↦ MvPolynomial.X (some n)
let I₁ : Ideal P := Ideal.span ({F * T 0} ∪ Set.range (fun n ↦ F * T (n + 1) - T n))
let R₁ := P ⧸ I₁
let f₁ : R₁ := Ideal.Quotient.mk I₁ F
let t₁ : ℕ → R₁ := fun n ↦ Ideal.Quotient.mk I₁ (T n)
let J₁ : Ideal R₁ := Ideal.span {f₁}
let c₁ := AdicCompletion.of J₁ R₁
let I₂ : Ideal P := Ideal.span (Set.range (fun n ↦ F ^ (n + 1) * T n))
let R₂ := P ⧸ I₂
let f₂ : R₂ := Ideal.Quotient.mk I₂ F
let t₂ : ℕ → R₂ := fun n ↦ Ideal.Quotient.mk I₂ (T n)
let J₂ : Ideal R₂ := Ideal.span {f₂}
let c₂ := AdicCompletion.of J₂ R₂
t₁ 0 ≠ 0 ∧ t₁ 0 ∈ Ideal.primaryComponent R₁ J₁ ∧ c₁ (t₁ 0) = 0 ∧
(∀ n : ℕ, f₁ ^ n • c₁ (t₁ n) = c₁ (t₁ 0)) ∧
(¬ Function.Injective (Ideal.primaryComponent.map J₁ c₁)) ∧
(¬ Module.Flat R₁ (AdicCompletion J₁ R₁)) ∧
(¬ Function.Surjective (Ideal.primaryComponent.map J₂ c₂)) ∧
(∃ x : Ideal.primaryComponent (AdicCompletion J₂ R₂) J₂,
(∀ n : ℕ, AdicCompletion.evalₐ J₂ n x.1 =
Ideal.Quotient.mk (J₂ ^ n) (∑ i ∈ Finset.range n, f₂ ^ i * t₂ i)) ∧
f₂ • x.1 = 0 ∧
x ∉ Set.range (Ideal.primaryComponent.map J₂ c₂)) ∧
(¬ Module.Flat R₂ (AdicCompletion J₂ R₂))
Tag 0F1R, an equation
Tag 0F1R in the Stacks Project.
BeauvilleLaszlo.beauvilleLaszloModuleSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueableModule/ModuleSequence.lean, line 148.
The canonical sequence
0 → M → (M ⊗[R] S) ⊕ (M ⊗[R] R_f) → M ⊗[R] S_f → 0. The right-hand map is the difference of the two maps induced by localization.
public noncomputable def beauvilleLaszloModuleSequence (f : R) :
ShortComplex AddCommGrpCat.{max u v w}
Tag 0BNV, an equation
Tag 0BNV in the Stacks Project.
BeauvilleLaszlo.isGlueable_iff_adicCompletion_beauvilleLaszloModuleSequence_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueableModule/ModuleSequence.lean, line 217.
An
R-module is glueable atfexactly when0 → M → (M ⊗[R] R̂) ⊕ (M ⊗[R] R_f) → M ⊗[R] R̂_f → 0is short exact, whereR̂is the(f)-adic completion.
public theorem isGlueable_iff_adicCompletion_beauvilleLaszloModuleSequence_shortExact {R : Type u}
[CommRing R] (M : Type w) [AddCommGroup M] [Module R M]
(f : R) :
IsGlueable M f ↔
(beauvilleLaszloModuleSequence
(S := AdicCompletion (Ideal.span {f}) R) M f).ShortExact
Tag 0BNW, a lemma
Tag 0BNW in the Stacks Project.
BeauvilleLaszlo.beauvilleLaszloModuleSequence_exactness_iff_powerTorsionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueableModule/ModuleSequence.lean, line 714.
If
R → Sis an isomorphism modulo every positive power off, the module Beauville--Laszlo sequence is surjective on the right; its left and middle exactness are equivalent to injectivity and surjectivity of the canonical map onf-power torsion. Thus the module is glueable exactly when this map is bijective. If the ring sequence is short exact, surjectivity on power torsion is automatic, so injectivity alone characterizes glueability. The latter criterion also applies to the(f)-adic completion.
public theorem beauvilleLaszloModuleSequence_exactness_iff_powerTorsionMap :
(∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
(M : Type w) [AddCommGroup M] [Module R M] (f : R),
(∀ n : ℕ, 0 < n → Function.Bijective
(quotientPowMap f n (algebraMap R S))) →
Epi (beauvilleLaszloModuleSequence (S := S) M f).g ∧
(Mono (beauvilleLaszloModuleSequence (S := S) M f).f ↔
Function.Injective (tensorProductPowerTorsionMap (S := S) M f)) ∧
((beauvilleLaszloModuleSequence (S := S) M f).Exact ↔
Function.Surjective (tensorProductPowerTorsionMap (S := S) M f)) ∧
((beauvilleLaszloModuleSequence (S := S) M f).ShortExact ↔
Function.Bijective (tensorProductPowerTorsionMap (S := S) M f)) ∧
((beauvilleLaszloSequence f (algebraMap R S)).ShortExact →
((beauvilleLaszloModuleSequence (S := S) M f).ShortExact ↔
Function.Injective (tensorProductPowerTorsionMap (S := S) M f)))) ∧
(∀ (R : Type u) [CommRing R] (M : Type w) [AddCommGroup M] [Module R M] (f : R),
(beauvilleLaszloSequence f
(algebraMap R (AdicCompletion (Ideal.span {f}) R))).ShortExact →
((beauvilleLaszloModuleSequence
(S := AdicCompletion (Ideal.span {f}) R) M f).ShortExact ↔
Function.Injective
(tensorProductPowerTorsionMap
(S := AdicCompletion (Ideal.span {f}) R) M f)))
Tag 0BNX, a remark
Tag 0BNX in the Stacks Project.
BeauvilleLaszlo.glueable_criteria, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueableModule/Criteria.lean, line 642.
Criteria ensuring that a module is glueable for a Beauville--Laszlo glueing pair.
For completion at
f, glueability is equivalent to injectivity onf-power torsion. Injectivity ofM[f] → M̂is equivalent toM[f] ∩ ⋂ n ≥ 1, f ^ n M = 0and implies glueability. For a general glueing pairR → S, vanishing ofTor₁(M, S_f)is sufficient and is equivalent toTor₁(M, S)beingf-power torsion. Consequently flat modules are glueable; ifSis flat overR, every module is glueable. The latter applies to completion over a Noetherian ring.
public theorem glueable_criteria :
(∀ (R : Type u) [CommRing R] (M : Type w) [AddCommGroup M] [Module R M]
(f : R),
(beauvilleLaszloSequence f
(algebraMap R (AdicCompletion (Ideal.span {f}) R))).ShortExact →
((IsGlueable M f ↔
Function.Injective
(tensorProductPowerTorsionMap
(S := AdicCompletion (Ideal.span {f}) R) M f)) ∧
(Function.Injective
(fun x : Submodule.torsionBy R M f ↦
AdicCompletion.of (Ideal.span {f}) M x.1) ↔
Submodule.torsionBy R M f ⊓
(⨅ n : ℕ, (Ideal.span {f}) ^ (n + 1) • ⊤) = ⊥) ∧
(Function.Injective
(fun x : Submodule.torsionBy R M f ↦
AdicCompletion.of (Ideal.span {f}) M x.1) →
IsGlueable M f))) ∧
(∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S]
(M : Type w) [AddCommGroup M] [Module R M] (f : R),
(beauvilleLaszloSequence f (algebraMap R S)).ShortExact →
((IsZero
(((Tor' (ModuleCat.{max u v w} (ULift.{max v w} R)) 1).obj
(ModuleCat.of (ULift.{max v w} R) (ULift.{max u v} M))).obj
(ModuleCat.of (ULift.{max v w} R)
(ULift.{max u w} (Localization.Away (algebraMap R S f))))) →
IsGlueableFor (S := S) M f) ∧
(IsZero
(((Tor' (ModuleCat.{max u v w} (ULift.{max v w} R)) 1).obj
(ModuleCat.of (ULift.{max v w} R) (ULift.{max u v} M))).obj
(ModuleCat.of (ULift.{max v w} R)
(ULift.{max u w} (Localization.Away (algebraMap R S f))))) ↔
modulePowerTorsion
(((Tor' (ModuleCat.{max u v w} (ULift.{max v w} R)) 1).obj
(ModuleCat.of (ULift.{max v w} R) (ULift.{max u v} M))).obj
(ModuleCat.of (ULift.{max v w} R) (ULift.{max u w} S)))
(ULift.up f) = ⊤) ∧
(Module.Flat R M → IsGlueableFor (S := S) M f) ∧
(Module.Flat R S → IsGlueableFor (S := S) M f))) ∧
(∀ (R : Type u) [CommRing R] [IsNoetherianRing R]
(M : Type w) [AddCommGroup M] [Module R M] (f : R),
IsGlueable M f)
Tag 0BNY, an example
Tag 0BNY in the Stacks Project.
BeauvilleLaszlo.exists_non_glueable_module_over_smooth_germ_ring, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueableModule/NonGlueableExample.lean, line 718.
The ring
Rof germs at zero of smooth functions onℝ, with coordinate germf, has completionℝ[[X]]. The flat germsφ(x) = exp (-1 / x²)andψ(x) = φ(x) / xvanish in the completion, while the class ofψinM = R / φRis nonzerof-torsion. It therefore lies in the kernel of the completion base-change map, soMis not glueable.
public theorem exists_non_glueable_module_over_smooth_germ_ring :
let S := smoothSheafCommRing (modelWithCornersSelf ℝ ℝ)
(modelWithCornersSelf ℝ ℝ) ℝ ℝ
let R := S.presheaf.stalk (0 : ℝ)
∃ (f₀ φ₀ ψ₀ : S.presheaf.obj (op ⊤)),
(∀ x : ℝ, f₀ ⟨x, Set.mem_univ x⟩ = x) ∧
(∀ x : ℝ, φ₀ ⟨x, Set.mem_univ x⟩ =
if x = 0 then 0 else Real.exp (-1 / x ^ 2)) ∧
(∀ x : ℝ, ψ₀ ⟨x, Set.mem_univ x⟩ =
if x = 0 then 0 else Real.exp (-1 / x ^ 2) / x) ∧
let f : R := S.presheaf.germ ⊤ 0 (Set.mem_univ 0) f₀
let φ : R := S.presheaf.germ ⊤ 0 (Set.mem_univ 0) φ₀
let ψ : R := S.presheaf.germ ⊤ 0 (Set.mem_univ 0) ψ₀
IsRegular f ∧ IsRegular φ ∧ f * ψ = φ ∧
∃ e : AdicCompletion (Ideal.span {f}) R ≃+* PowerSeries ℝ,
e (algebraMap R (AdicCompletion (Ideal.span {f}) R) f) = PowerSeries.X ∧
algebraMap R (AdicCompletion (Ideal.span {f}) R) φ = 0 ∧
algebraMap R (AdicCompletion (Ideal.span {f}) R) ψ = 0 ∧
(let M := R ⧸ Ideal.span {φ}
let m : M := Ideal.Quotient.mk (Ideal.span {φ}) ψ
let C := AdicCompletion (Ideal.span {f}) R
m ≠ 0 ∧ f • m = 0 ∧
TensorProduct.mk R M C m 1 = 0 ∧
(∃ q : TensorProduct R M C ≃ₗ[R] C,
∀ (r : R) (c : C),
q (TensorProduct.mk R M C (Ideal.Quotient.mk (Ideal.span {φ}) r) c) =
algebraMap R C r * c) ∧
¬ Function.Injective
(fun x : {x : M // ∃ n : ℕ, f ^ n • x = 0} ↦
TensorProduct.mk R M C x.1 1))
Tag 0BNZ, a lemma
Tag 0BNZ in the Stacks Project.
BeauvilleLaszlo.isZero_Tor_one_ideal_pow_of_beauvilleLaszlo_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/TorVanishing.lean, line 180.
If
(R → R', f)is a gluing pair, thenTor₁ʿ(R', f ^ n R) = 0for every positiven.
public theorem isZero_Tor_one_ideal_pow_of_beauvilleLaszlo_shortExact
{R S : Type u} [CommRing R] [CommRing S] (f : R) (φ : R →+* S)
(hφ : ∀ n : ℕ, 0 < n →
Function.Bijective (quotientPowMap f n φ))
(hglue : (beauvilleLaszloSequence f φ).ShortExact) :
∀ n : ℕ, 0 < n →
Limits.IsZero (((Tor (ModuleCat.{u} R) 1).obj
((ModuleCat.restrictScalars φ).obj (ModuleCat.of S S))).obj
(ModuleCat.of R ↑((Ideal.span {f}) ^ n)))
Tag 0BP0, a lemma
Tag 0BP0 in the Stacks Project.
BeauvilleLaszlo.isZero_Tor_one_quotient_powerTorsion_of_beauvilleLaszlo_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/TorVanishing.lean, line 449.
If
(R → R', f)is a glueing pair, thenTor₁ᴿ(R', R / R[f^∞]) = 0.
public theorem isZero_Tor_one_quotient_powerTorsion_of_beauvilleLaszlo_shortExact
{R S : Type u} [CommRing R] [CommRing S] (f : R) (φ : R →+* S)
(hφ : ∀ n : ℕ, 0 < n → Function.Bijective (quotientPowMap f n φ))
(hglue : (beauvilleLaszloSequence f φ).ShortExact) :
Limits.IsZero (((Tor (ModuleCat.{u} R) 1).obj
((ModuleCat.restrictScalars φ).obj (ModuleCat.of S S))).obj
(ModuleCat.of R (R ⧸ powerTorsion f)))
Tag 0BP1, a lemma
Tag 0BP1 in the Stacks Project.
BeauvilleLaszlo.isZero_Tor_one_coker_localizationMap_of_beauvilleLaszlo_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/TorVanishing.lean, line 637.
If
(R → R', f)is a Beauville--Laszlo glueing pair, then for everyR-moduleM,Tor₁ᴿ(R', coker(M → M_f)) = 0.
public theorem isZero_Tor_one_coker_localizationMap_of_beauvilleLaszlo_shortExact
{R : Type u} {S : Type v} {M : Type w}
[CommRing R] [CommRing S] [AddCommGroup M] [Module R M]
(f : R) (φ : R →+* S)
(hφ : ∀ n : ℕ, 0 < n → Function.Bijective (quotientPowMap f n φ))
(hglue : (beauvilleLaszloSequence f φ).ShortExact) :
Limits.IsZero (((Tor (ModuleCat.{max u v w}
(ULift.{max u v w} R)) 1).obj
((ModuleCat.restrictScalars (φ.ulift.{max u v w, max u v w})).obj
(ModuleCat.of (ULift.{max u v w} S) (ULift.{max u v w} S)))).obj
(ModuleCat.of (ULift.{max u v w} R)
(ULift.{max u v w}
(LocalizedModule (Submonoid.powers f) M ⧸
LinearMap.range (LocalizedModule.mkLinearMap (Submonoid.powers f) M)))))
Tag 0BP2, a theorem
Tag 0BP2 in the Stacks Project.
BeauvilleLaszlo.canonicalOnGlueableModules_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/ModuleEquivalence.lean, line 854.
Beauville--Laszlo glueing. For a glueing pair
(R → S, f), the canonical functor from glueableR-modules to module glueing data is an equivalence of categories. Compatible sections of every glueing datum are glueable, and the canonical map from any module to the sections of its canonical datum induces isomorphisms after extension of scalars toSand localization away fromf.
public theorem canonicalOnGlueableModules_isEquivalence
(hquot : ∀ n : ℕ, 0 < n →
Function.Bijective (quotientPowMap f n (algebraMap R S)))
(hglue : (beauvilleLaszloSequence f (algebraMap R S)).ShortExact) :
let C := moduleGlueingConstruction.{u, v, w} S (fun _ : Fin 1 ↦ f)
letI := C.category
(canonicalOnGlueableModules f C).IsEquivalence ∧
(∀ X : ModuleGlueingDatum.{u, v, w} S (fun _ : Fin 1 ↦ f) C.comparison,
glueableModules (S := S) f (C.sections.obj X)) ∧
(∀ M : ModuleCat.{max u v w} R,
Function.Bijective
(TensorProduct.map (LinearMap.id (R := R) (M := S))
(C.canonicalSectionsUnit.app M).hom) ∧
Function.Bijective
(LocalizedModule.map (Submonoid.powers f)
(C.canonicalSectionsUnit.app M).hom))
Tag 0BP3, an equation
Tag 0BP3 in the Stacks Project.
BeauvilleLaszlo.gluingDatum_difference_shortExact_of_quotientMap_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingData.lean, line 105.
The kernel of the difference map attached to a gluing datum fits into the short exact sequence
0 → ker(d) → M' × M₁ → M'ₑ → 0.Here the difference map sends
(x, y)tox / 1 - α⁻¹(1 ⊗ y). It is surjective as soon asR → Sis surjective modulo every positive power off; in particular the result applies to a Beauville--Laszlo gluing pair.
public theorem gluingDatum_difference_shortExact_of_quotientMap_surjective
(R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
(f : R)
(hmod : ∀ n : ℕ, 0 < n →
Function.Surjective
(Ideal.quotientMap
(Ideal.map (algebraMap R S) ((Ideal.span {f}) ^ n))
(algebraMap R S) Ideal.le_comap_map))
(M' : Type w) [AddCommGroup M'] [Module R M'] [Module S M']
[IsScalarTower R S M']
(M₁ : Type x) [AddCommGroup M₁] [Module R M₁]
[Module (Localization.Away f) M₁] [IsScalarTower R (Localization.Away f) M₁]
(α : LocalizedModule.Away (algebraMap R S f) M' ≃ₗ[S]
TensorProduct R S M₁) :
let localizationMap : M' →ₗ[R] LocalizedModule.Away (algebraMap R S f) M' :=
(LocalizedModule.mkLinearMap (Submonoid.powers (algebraMap R S f)) M').restrictScalars R
let tensorMap : M₁ →ₗ[R] TensorProduct R S M₁ := TensorProduct.mk R S M₁ 1
let d : (M' × M₁) →ₗ[R] LocalizedModule.Away (algebraMap R S f) M' :=
localizationMap.comp (LinearMap.fst R M' M₁) -
((α.symm.toLinearMap.restrictScalars R).comp tensorMap).comp
(LinearMap.snd R M' M₁)
Function.Injective (LinearMap.ker d).subtype ∧
Function.Exact (LinearMap.ker d).subtype d ∧
Function.Surjective d
Tag 0BP4, an equation
Tag 0BP4 in the Stacks Project.
BeauvilleLaszlo.exists_exact_quotient_powerTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingData.lean, line 220.
Suppose
A → Lis localization away fromf, the difference mapA × B → L,(a, b) ↦ g a - h b, is surjective, and multiplication byfis injective onB. IfMis the kernel of the difference map, projection toBinduces the canonical short exact sequence0 → M / M[f^∞] → B → L / range(g) → 0.The displayed compatibility uniquely specifies the induced left-hand map.
public theorem exists_exact_quotient_powerTorsion
(f : R) (g : A →ₗ[R] L) [IsLocalizedModule.Away f g] (h : B →ₗ[R] L)
(hd : Function.Surjective
(g.comp (LinearMap.fst R A B) - h.comp (LinearMap.snd R A B)))
(hf : Function.Injective (fun b : B ↦ f • b)) :
let d := g.comp (LinearMap.fst R A B) - h.comp (LinearMap.snd R A B)
let M := LinearMap.ker d
let T := Submodule.torsion' R M (Submonoid.powers f)
let q := (Submodule.mkQ (LinearMap.range g)).comp h
∃ i : (M ⧸ T) →ₗ[R] B,
(∀ m : M, i (Submodule.mkQ T m) = m.1.2) ∧
Function.Injective i ∧ LinearMap.range i = LinearMap.ker q ∧
Function.Surjective q
Tag 0BP5, an equation
Tag 0BP5 in the Stacks Project.
BeauvilleLaszlo.gluingDatum_baseChange_localizationQuotient_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/GlueingData.lean, line 478.
Let
(R → S, f)be a Beauville--Laszlo glueing pair and let(M', M₁, α)be a glueing datum. IfMis the kernel ofM' × M₁ → (M')_f,(x, y) ↦ x / 1 - α⁻¹(y ⊗ 1), projection toM₁induces a mapi : M / M[f^∞] → M₁. After extendingitoSand usingα, it is the left map of the canonical short exact sequence0 → (M / M[f^∞]) ⊗_R S → (M')_f → (M')_f / M' → 0.The first displayed condition characterizes the induced map
i; thus the assertion also records the canonical construction, rather than only the existence of some exact sequence with isomorphic terms.
public theorem gluingDatum_baseChange_localizationQuotient_shortExact
(R : Type uR) [CommRing R] (S : Type uS) [CommRing S] [Algebra R S]
(f : R)
(hmod : ∀ n : ℕ, 0 < n →
Function.Bijective
(Ideal.quotientMap
(Ideal.map (algebraMap R S) ((Ideal.span {f}) ^ n))
(algebraMap R S) Ideal.le_comap_map))
(hglue : (beauvilleLaszloSequence f (algebraMap R S)).ShortExact)
(M' : Type uM) [AddCommGroup M'] [Module R M'] [Module S M']
[IsScalarTower R S M']
(M₁ : Type uM₁) [AddCommGroup M₁] [Module R M₁]
[Module (Localization.Away f) M₁] [IsScalarTower R (Localization.Away f) M₁]
(α : LocalizedModule.Away (algebraMap R S f) M' ≃ₗ[S]
TensorProduct R S M₁) :
let localizationMap : M' →ₗ[R] LocalizedModule.Away (algebraMap R S f) M' :=
(LocalizedModule.mkLinearMap
(Submonoid.powers (algebraMap R S f)) M').restrictScalars R
let tensorMap : M₁ →ₗ[R] TensorProduct R S M₁ :=
TensorProduct.mk R S M₁ 1
let d : (M' × M₁) →ₗ[R] LocalizedModule.Away (algebraMap R S f) M' :=
localizationMap.comp (LinearMap.fst R M' M₁) -
((α.symm.toLinearMap.restrictScalars R).comp tensorMap).comp
(LinearMap.snd R M' M₁)
let M := LinearMap.ker d
let T := Submodule.torsion' R M (Submonoid.powers f)
let q : LocalizedModule.Away (algebraMap R S f) M' →ₗ[R]
AwayCokernel R S f M' :=
((LinearMap.range
(LocalizedModule.mkLinearMap
(Submonoid.powers (algebraMap R S f)) M')).mkQ).restrictScalars R
∃ i : (M ⧸ T) →ₗ[R] M₁,
(∀ m : M, i (Submodule.mkQ T m) = m.1.2) ∧
let iS :=
(TensorProduct.map (LinearMap.id (R := R) (M := S)) i).comp
(TensorProduct.comm R (M ⧸ T) S).toLinearMap
let a := (α.symm.toLinearMap.restrictScalars R).comp iS
Function.Injective a ∧ Function.Exact a q ∧ Function.Surjective q
Tag 0BP9, a remark
Tag 0BP9 in the Stacks Project.
BeauvilleLaszlo.canonicalToSections_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/ModuleEquivalence.lean, line 1064.
Let
(R → S, f)be a Beauville--Laszlo glueing pair and letMbe anyR-module. The canonical map fromMto the compatible sections of its canonical glueing datum is surjective. Its target is glueable, and the map becomes an isomorphism after extension of scalars toSand after localization away fromf.The equations on the generic and local coordinates characterize the canonical map.
public theorem canonicalToSections_surjective
(R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
(f : R)
(hquot : ∀ n : ℕ, 0 < n →
Function.Bijective (quotientPowMap f n (algebraMap R S)))
(hglue : (beauvilleLaszloSequence f (algebraMap R S)).ShortExact)
(M : Type w) [AddCommGroup M] [Module R M] :
let C := FormalGlueing.moduleGlueingConstruction.{u, v, w} S (fun _ : Fin 1 ↦ f)
letI := C.category
let X := C.canonical.obj (ModuleCat.of R (ULift.{max u v w} M))
let Mbar := C.sections.obj X
∃ g : M →ₗ[R] Mbar,
(∀ m : M,
let x := C.sectionsObj X (g m)
C.canonicalGeneric (ModuleCat.of R (ULift.{max u v w} M)) x.1.1 =
1 ⊗ₜ[R] ULift.up m ∧
C.canonicalLocal (ModuleCat.of R (ULift.{max u v w} M)) 0 (x.1.2 0) =
LocalizedModule.mkLinearMap (Submonoid.powers f) (ULift M) (ULift.up m)) ∧
glueableModules (S := S) f Mbar ∧
Function.Bijective
(TensorProduct.map (LinearMap.id (R := R) (M := S)) g) ∧
Function.Bijective (LocalizedModule.map (Submonoid.powers f) g) ∧
Function.Surjective g
Tag 0BP7, a lemma
Tag 0BP7 in the Stacks Project.
BeauvilleLaszlo.flat_iff_flat_baseChange_and_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/Descent.lean, line 677.
Let
(R → S, f)be a Beauville--Laszlo glueing pair. AnR-moduleMis flat if and only if its scalar extension toSis flat overSand its localization away fromfis flat overR_f.
public theorem flat_iff_flat_baseChange_and_localization
(R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
(f : R)
(hquot : ∀ n : ℕ, 0 < n →
Function.Bijective (quotientPowMap f n (algebraMap R S)))
(hglue : (beauvilleLaszloSequence f (algebraMap R S)).ShortExact)
(M : Type w) [AddCommGroup M] [Module R M] :
Module.Flat R M ↔
Module.Flat S (S ⊗[R] M) ∧
Module.Flat (Localization.Away f) (LocalizedModule.Away f M)
Tag 0BP6, a lemma
Tag 0BP6 in the Stacks Project.
BeauvilleLaszlo.finite_projective_iff_baseChange_and_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/Descent.lean, line 804.
Let
(R → S, f)be a Beauville--Laszlo glueing pair. AnR-moduleMis finite projective if and only if its scalar extension toSis finite projective overSand its localization away fromfis finite projective overR_f.
public theorem finite_projective_iff_baseChange_and_localization
(R : Type u) [CommRing R] (S : Type v) [CommRing S] [Algebra R S]
(f : R)
(hquot : ∀ n : ℕ, 0 < n →
Function.Bijective (quotientPowMap f n (algebraMap R S)))
(hglue : (beauvilleLaszloSequence f (algebraMap R S)).ShortExact)
(M : Type w) [AddCommGroup M] [Module R M] :
(Module.Finite R M ∧ Module.Projective R M) ↔
((Module.Finite S (S ⊗[R] M) ∧ Module.Projective S (S ⊗[R] M)) ∧
(Module.Finite (Localization.Away f) (LocalizedModule.Away f M) ∧
Module.Projective (Localization.Away f) (LocalizedModule.Away f M)))
Tag 0BP8, a remark
Tag 0BP8 in the Stacks Project.
BeauvilleLaszlo.beauvilleLaszlo_completion_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/BeauvilleLaszlo/CompletionComparison.lean, line 52.
For a nonzerodivisor
f : R, passage to the(f)-adic completion gives a Beauville--Laszlo glueing pair. Every module on whichfis a nonzerodivisor is glueable, the canonical functor identifies all glueable modules with glueing data, and finite projectivity can be checked after completion and localization for an arbitrary module, with no torsion-freeness or glueability assumption on that module.
public theorem beauvilleLaszlo_completion_comparison
(R : Type u) [CommRing R] (f : R) (hf : IsSMulRegular R f) :
let Rhat := AdicCompletion (Ideal.span {f}) R
(beauvilleLaszloSequence f (algebraMap R Rhat)).ShortExact ∧
(∀ (M : Type w) [AddCommGroup M] [Module R M], IsSMulRegular M f →
(beauvilleLaszloModuleSequence (S := Rhat) M f).ShortExact) ∧
(let C := FormalGlueing.moduleGlueingConstruction.{u, u, w} Rhat (fun _ : Fin 1 ↦ f);
let _ := C.category;
(canonicalOnGlueableModules f C).IsEquivalence) ∧
(∀ (M : Type w) [AddCommGroup M] [Module R M],
(Module.Finite R M ∧ Module.Projective R M) ↔
((Module.Finite Rhat (Rhat ⊗[R] M) ∧ Module.Projective Rhat (Rhat ⊗[R] M)) ∧
(Module.Finite (Localization.Away f) (LocalizedModule.Away f M) ∧
Module.Projective (Localization.Away f) (LocalizedModule.Away f M))))
Sources
Section15.93 Derived Completion#
Section 15.93 of the Stacks Project, Tag 091N. 25 tags here are carried by 26 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 091P, a lemma
Tag 091P in the Stacks Project.
DerivedHomAway.tfae_ext_localization_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/DerivedHomCompletionVanishing/VanishingCriteria.lean, line 599.
The cohomology of
RHom_A(A_f, K)isExt_A(A_f, K). Moreover, the following are equivalent: all those Ext groups vanish;Kis right orthogonal to every object ofD(A_f);T(K, f)vanishes; everyT(H^p(K), f)vanishes; bothHom_A(A_f, H^p(K))andExt^1_A(A_f, H^p(K))vanish for everyp;RHom_A(A_f, K)vanishes; and(x_n) ↦ (x_n - f x_{n+1})is an isomorphism on the product of countably many copies ofK.
public theorem tfae_ext_localization_vanishing (A : Type u) [CommRing A] (f : A)
(K : DerivedCategory (ModuleCat.{u} A)) :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
let Af : Type u := Localization.Away f
let AfA := ModuleCat.of A Af
let sAf := (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj AfA
let tower := Functor.ofOpSequence (X := fun _ : ℕ => K) (fun _ => f • 𝟙 K)
IsDerivedLimit tower (derivedHomFromAway A f K) ∧
Nonempty (∀ n : ℤ,
((DerivedCategory.homologyFunctor (ModuleCat.{u} A) n).obj
(derivedHomFromAway A f K)) ≃+
DerivedCategory.Ext sAf K n) ∧
List.TFAE
[ ∀ n : ℤ, Subsingleton (DerivedCategory.Ext sAf K n)
, ∀ E : DerivedCategory (ModuleCat.{u} Af),
Subsingleton
(((ModuleCat.restrictScalars.{u} (algebraMap A Af)).mapDerivedCategory.obj E) ⟶ K)
, ∃ L : DerivedCategory (ModuleCat.{u} A), IsDerivedLimit tower L ∧ IsZero L
, ∀ p : ℤ,
let Hp := (DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj K
let sHp := (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj Hp
let towerHp := Functor.ofOpSequence (X := fun _ : ℕ => sHp) (fun _ => f • 𝟙 sHp)
∃ L : DerivedCategory (ModuleCat.{u} A), IsDerivedLimit towerHp L ∧ IsZero L
, ∀ p : ℤ,
let Hp := (DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj K
Subsingleton (AfA ⟶ Hp) ∧ Subsingleton (Abelian.zExt AfA Hp 1)
, IsZero (derivedHomFromAway A f K)
, IsIso (Pi.lift fun n : ℕ =>
Pi.π (fun _ : ℕ => K) n - f • Pi.π (fun _ : ℕ => K) (n + 1)) ]
Tag 091Q, a lemma
Tag 091Q in the Stacks Project.
exists_isRadical_ideal_isDerivedCompleteAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompleteAdic.lean, line 174.
For
K ∈ D(A), the elementsf : Aat whichKis derived complete — equivalently, for which the derived limit of⋯ → K → K, with every transition map multiplication byf, is zero — are precisely the elements of a radical ideal ofA.
public theorem exists_isRadical_ideal_isDerivedCompleteAt (A : Type u) [CommRing A]
(K : DerivedCategory (ModuleCat.{v} A))
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A))] :
∃ I : Ideal A, I.IsRadical ∧ ∀ f : A, f ∈ I ↔ IsDerivedCompleteAt K f
Tag 091R, a lemma
Tag 091R in the Stacks Project.
isDerivedCompleteModule_of_isAdicComplete_and_adicCompletion_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompleteAdic.lean, line 418.
An
I-adically complete module is derived complete with respect toI. Conversely, for a finitely generated idealI, derived completeness makes the canonical map to theI-adic completion surjective.
public theorem isDerivedCompleteModule_of_isAdicComplete_and_adicCompletion_surjective
(A : Type u) [CommRing A] (I : Ideal A)
(M : Type v) [AddCommGroup M] [Module A M]
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A))] :
(IsAdicComplete I M → IsDerivedCompleteModule I (ModuleCat.of A M)) ∧
(I.FG → IsDerivedCompleteModule I (ModuleCat.of A M) →
Function.Surjective (AdicCompletion.of I M))
Tag 091S, a definition
Tag 091S in the Stacks Project.
IsDerivedComplete, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete.lean, line 172. The attribute's comment: “(1)”.
Kis derived complete with respect to the idealIifT(K,f) = 0for everyf ∈ I.
def IsDerivedComplete {C : Type*} [Category C] [Preadditive C] [Linear A C]
[HasProductsOfShape ℕ C] (I : Ideal A) (K : C) : Prop
IsDerivedCompleteModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete.lean, line 378. The attribute's comment: “(2)”.
An
A-module is derived complete with respect toIwhen the corresponding object ofD(A), concentrated in degree zero, is derived complete.
def IsDerivedCompleteModule (I : Ideal A) (M : ModuleCat.{v} A) : Prop
Tag 091T, a proposition
Tag 091T in the Stacks Project.
isAdicComplete_iff_isDerivedCompleteModule_and_iInf_pow_smul_top_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompleteAdic.lean, line 454.
For a finitely generated ideal
I, anA-moduleMisI-adically complete if and only if it is derived complete with respect toIand the intersection of the submodulesI ^ n Mis zero.
public theorem isAdicComplete_iff_isDerivedCompleteModule_and_iInf_pow_smul_top_eq_bot
(A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
(M : Type v) [AddCommGroup M] [Module A M]
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A))] :
IsAdicComplete I M ↔
IsDerivedCompleteModule I (ModuleCat.of A M) ∧
⨅ n : ℕ, I ^ n • (⊤ : Submodule A M) = ⊥
Tag 091U, a lemma
Tag 091U in the Stacks Project.
AdicWeakSerre.derivedCompleteModules_isWeakSerreClass_and_homology_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/AdicWeakSerreClass.lean, line 97.
Stacks 091U. The derived complete modules with respect to
Iform a weak Serre subcategory ofModuleCat A. Moreover, an object ofD(A)is derived complete exactly when all of its cohomology modules are derived complete.
public theorem derivedCompleteModules_isWeakSerreClass_and_homology_iff
(A : Type u) [CommRing A] (I : Ideal A) :
letI : HasExactLimitsOfShape (Discrete ℕ) (ModuleCat.{v} A) :=
moduleCat_hasExactLimitsOfShape_discrete.{v} A ℕ
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
let C : ObjectProperty (ModuleCat.{v} A) :=
fun M => IsDerivedCompleteModule I M
C.IsWeakSerreClass ∧
∀ K : DerivedCategory (ModuleCat.{v} A),
(∀ n : ℤ, C ((DerivedCategory.homologyFunctor (ModuleCat.{v} A) n).obj K)) ↔
IsDerivedComplete I K
Tag 09B9, a lemma
Tag 09B9 in the Stacks Project.
subsingleton_of_isDerivedCompleteModule_of_quotient_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/NakayamaModule.lean, line 256.
Stacks 09B9. A derived complete module with zero reduction modulo a finitely generated ideal is zero.
theorem subsingleton_of_isDerivedCompleteModule_of_quotient_smul
(A : Type u) [CommRing A]
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A))]
(I : Ideal A) (M : ModuleCat.{v} A) (hI : I.FG)
(hM : IsDerivedCompleteModule I M)
(hMI : Subsingleton (M ⧸ (I • ⊤ : Submodule A M))) : Subsingleton M
Tag 0A05, a lemma
Tag 0A05 in the Stacks Project.
isDerivedComplete_of_isPseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/PseudoCoherentComplete.lean, line 232.
Stacks 0A05. A pseudo-coherent object over a ring that is derived complete with respect to
Iis itself derived complete with respect toI. Pseudo-coherence is spelled out as in Stacks 064Q (2):Kis represented by a bounded-above complex of finite free modules.
theorem isDerivedComplete_of_isPseudoCoherent
(A : Type u) [CommRing A] (I : Ideal A)
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))] :
IsDerivedCompleteModule I (ModuleCat.of A A) →
∀ K : DerivedCategory (ModuleCat.{u} A),
(∃ E : CochainComplex (ModuleCat.{u} A) ℤ,
((∃ b : ℤ, E.IsStrictlyLE b) ∧
∀ i : ℤ, Module.Finite A (E.X i) ∧ Module.Free A (E.X i)) ∧
Nonempty (DerivedCategory.Q.obj E ≅ K)) →
IsDerivedComplete I K
Tag 0A6C, a lemma
Tag 0A6C in the Stacks Project.
DerivedHomLocalization.derivedHom_localization_comp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/DerivedHomCompletionLocalizationComp.lean, line 48.
Stacks 0A6C. For
f, g ∈ AandK ∈ D(A), there is a canonical isomorphismRHom_A(A_f, RHom_A(A_g, K)) ≅ RHom_A(A_{fg}, K).
public noncomputable def derivedHom_localization_comp {A : Type u} [CommRing A]
[HasDerivedCategory (ModuleCat A)] (f g : A) (K : DerivedCategory (ModuleCat A)) :
let D := StacksDraft.DerivedHom.derivedHomAdjunction (R := A)
let away (a : A) := DerivedCategory.Q.obj
((CochainComplex.singleFunctor (ModuleCat A) 0).obj
(ModuleCat.of A (Localization.Away a)))
D.hom.obj (Opposite.op (away f), D.hom.obj (Opposite.op (away g), K)) ≅
D.hom.obj (Opposite.op (away (f * g)), K)
Tag 091V, a lemma
Tag 091V in the Stacks Project.
CechCompletion.cechCompletion_isReflection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CechCompletion.lean, line 1129.
Derived completion with respect to the ideal generated by a finite family
fis computed functorially as derived Hom from its extended alternating Čech complex. It is derived complete, and the natural map from an object to its completion induces a bijection on morphisms into every derived-complete object.
public theorem cechCompletion_isReflection (A : Type u) [CommRing A] {r : ℕ}
(f : Fin r → A)
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))] :
∃ η : Functor.id (DerivedCategory (ModuleCat.{u} A)) ⟶ cechCompletionFunctor A f,
(∀ K, IsDerivedComplete (Ideal.span (Set.range f))
((cechCompletionFunctor A f).obj K)) ∧
∀ (K E : DerivedCategory (ModuleCat.{u} A)),
IsDerivedComplete (Ideal.span (Set.range f)) E →
Function.Bijective
(fun g : (cechCompletionFunctor A f).obj K ⟶ E ↦ η.app K ≫ g)
Tag 0G3E, a remark
Tag 0G3E in the Stacks Project.
DerivedCompletion.derivedCompletion_isReflection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CechReflection.lean, line 69.
Derived completion with respect to a finitely generated ideal is the reflection into the derived-complete objects: it takes derived-complete values, and its unit
K ⟶ K̂induces a bijection from maps out ofK̂to maps out ofKwhenever the target is derived complete.
public theorem derivedCompletion_isReflection (A : Type u) [CommRing A] {r : ℕ}
(f : Fin r → A)
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))] :
(∀ K, IsDerivedComplete (Ideal.span (Set.range f))
((derivedCompletionFunctor A f).obj K)) ∧
∀ (K E : DerivedCategory (ModuleCat.{u} A)),
IsDerivedComplete (Ideal.span (Set.range f)) E →
Function.Bijective
(fun g : (derivedCompletionFunctor A f).obj K ⟶ E ↦
(derivedCompletionUnit A f).app K ≫ g)
Tag 0A6D, a lemma
Tag 0A6D in the Stacks Project.
CechCompletion.isZero_cechCompletion_of_isIso_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CechCompletionVanishing.lean, line 129.
Stacks 0A6D. Let
Ibe the ideal generated by a finite familyg. If somex ∈ Iacts invertibly onK ∈ D(A), then the derived completion ofKwith respect toIis zero.
public theorem isZero_cechCompletion_of_isIso_smul (A : Type u) [CommRing A] {r : ℕ}
(g : Fin r → A) (K : DerivedCategory (ModuleCat.{u} A))
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))]
{x : A} (hx : x ∈ Ideal.span (Set.range g)) [IsIso (x • 𝟙 K)] :
IsZero ((cechCompletionFunctor A g).obj K)
Tag 0A6E, a lemma
Tag 0A6E in the Stacks Project.
DerivedHomCechCompletion.derivedHom_cechCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/DerivedHomCompletionHom.lean, line 276.
For a finite family
fgenerating an ideal ofA, derived completion commutes naturally with derived Hom in its target:RHom_A(K, L)^∧ ≅ RHom_A(K, L^∧). Ifη : K ⟶ K^∧is the reflection unit, then precomposition withηis the natural isomorphismRHom_A(K^∧, L^∧) ≅ RHom_A(K, L^∧).
public theorem derivedHom_cechCompletion (A : Type u) [CommRing A] {r : ℕ}
(f : Fin r → A)
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))] :
let C := DerivedCategory (ModuleCat.{u} A)
let D := StacksDraft.DerivedHom.derivedHomAdjunction (R := A)
let F := CechCompletion.cechCompletionFunctor A f
∃ η : Functor.id C ⟶ F,
(∀ K, IsDerivedComplete (Ideal.span (Set.range f)) (F.obj K)) ∧
(∀ (K E : C), IsDerivedComplete (Ideal.span (Set.range f)) E →
Function.Bijective (fun g : F.obj K ⟶ E ↦ η.app K ≫ g)) ∧
Nonempty
((D.hom ⋙ F) ≅
(((CategoryTheory.Prod.fst Cᵒᵖ C).prod'
(CategoryTheory.Prod.snd Cᵒᵖ C ⋙ F)) ⋙ D.hom)) ∧
∃ e :
((((CategoryTheory.Prod.fst Cᵒᵖ C ⋙ F.op).prod'
(CategoryTheory.Prod.snd Cᵒᵖ C ⋙ F)) ⋙ D.hom) ≅
(((CategoryTheory.Prod.fst Cᵒᵖ C).prod'
(CategoryTheory.Prod.snd Cᵒᵖ C ⋙ F)) ⋙ D.hom)),
∀ (K L : C), e.hom.app (Opposite.op K, L) =
D.hom.map
(show (Opposite.op (F.obj K), F.obj L) ⟶ (Opposite.op K, F.obj L) from
((η.app K).op, 𝟙 (F.obj L)))
Tag 091W, a lemma
Tag 091W in the Stacks Project.
isDerivedComplete_of_isMilnorTriangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete.lean, line 449.
Let
Abe a ring andI ⊂ Aan ideal. Let(Kₙ)be an inverse system of objects ofD(A)(objectsKsys n, transition mapsKt n : Ksys (n+1) ⟶ Ksys n) such that for everyf ∈ Iand everynthe scalarfacts nilpotently onKsys n. LetFbe an additiveA-linear endofunctor ofD(A), standing forK ⊗ᴸ (-). Then any derived limitK'of the tower(F.obj (Ksys n))is derived complete with respect toI.
theorem
isDerivedComplete_of_isMilnorTriangle (I : Ideal A) (Ksys : ℕ → DerivedCategory (ModuleCat A))
(Kt : ∀ n, Ksys (n + 1) ⟶ Ksys n) (hnil : ∀ f ∈ I, ∀ n, IsNilpotent (f • (1 : End (Ksys n))))
(F : DerivedCategory (ModuleCat A) ⥤ DerivedCategory (ModuleCat A)) [F.Additive] [F.Linear A]
(K' : DerivedCategory (ModuleCat A)) {ι : K' ⟶ ∏ᶜ fun n => F.obj (Ksys n)}
{δ : (∏ᶜ fun n => F.obj (Ksys n)) ⟶ K'⟦(1 : ℤ)⟧}
(hMilnor : IsMilnorTriangle (fun n => F.obj (Ksys n)) (fun n => F.map (Kt n)) K' ι δ) :
IsDerivedComplete I K'
Tag 0BKC, a situation
Tag 0BKC in the Stacks Project.
koszulPowerComplexes_form_inverseSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompleteKoszulPowers.lean, line 416. References: SGA 2 II (Lemma9), “partial”.
Stacks Project, Tag 0BKC. The Koszul complexes on the positive powers of a finite sequence form an inverse system. The displayed formula says that its transition maps are the maps of Koszul complexes induced by multiplying the
i-th basis vector by the appropriate power off i. The system is compatible both with its canonical maps fromAand, under the natural identifications in degree zero, with the inverse system of quotients by the ideals generated by the powered sequences.
public theorem koszulPowerComplexes_form_inverseSystem
{A : Type u} [CommRing A] {r : ℕ} (f : Fin r → A) :
let K : ℕ → ChainComplex (ModuleCat.{u} A) ℕ := fun n ↦
Koszul.seqComplex (fun i ↦ f i ^ (n + 1))
let Q : ℕ → ModuleCat.{u} A := fun n ↦
ModuleCat.of A (A ⧸ Ideal.span (Set.range fun i ↦ f i ^ (n + 1)))
∃ (τ : ∀ (m n : ℕ), n ≤ m → (K m ⟶ K n))
(σ : ∀ (m n : ℕ), n ≤ m → (Q m ⟶ Q n))
(e : ∀ n, (K n).homology 0 ≅ Q n)
(η : ∀ n, (ChainComplex.single₀ (ModuleCat.{u} A)).obj (ModuleCat.of A A) ⟶ K n),
(∀ n, τ n n (le_refl n) = 𝟙 (K n)) ∧
(∀ (k m n : ℕ) (hkm : m ≤ k) (hmn : n ≤ m),
τ k m hkm ≫ τ m n hmn = τ k n (hmn.trans hkm)) ∧
(∀ n, σ n n (le_refl n) = 𝟙 (Q n)) ∧
(∀ (k m n : ℕ) (hkm : m ≤ k) (hmn : n ≤ m),
σ k m hkm ≫ σ m n hmn = σ k n (hmn.trans hkm)) ∧
(∀ (m n : ℕ) (hmn : n ≤ m) (j : ℕ) (v : Fin j → Fin r → A),
(τ m n hmn).f j
⟨ExteriorAlgebra.ιMulti A j v, Koszul.ιMulti_mem j v⟩ =
⟨ExteriorAlgebra.ιMulti A j
(fun k i ↦ f i ^ (m - n) * v k i),
Koszul.ιMulti_mem j (fun k i ↦ f i ^ (m - n) * v k i)⟩) ∧
(∀ (n : ℕ) (a : A),
(η n).f 0 a =
a • ⟨ExteriorAlgebra.ιMulti A 0 (fun i ↦ Fin.elim0 i),
Koszul.ιMulti_mem 0 (fun i ↦ Fin.elim0 i)⟩) ∧
(∀ (m n : ℕ) (hmn : n ≤ m), η m ≫ τ m n hmn = η n) ∧
(∀ (m n : ℕ) (hmn : n ≤ m),
ModuleCat.ofHom
(Ideal.span (Set.range fun i ↦ f i ^ (m + 1))).mkQ ≫
σ m n hmn =
ModuleCat.ofHom
(Ideal.span (Set.range fun i ↦ f i ^ (n + 1))).mkQ) ∧
(∀ (m n : ℕ) (hmn : n ≤ m),
(e m).inv ≫ HomologicalComplex.homologyMap (τ m n hmn) 0 ≫ (e n).hom =
σ m n hmn) ∧
∀ n,
(HomologicalComplex.singleObjHomologySelfIso
(ComplexShape.down ℕ) 0 (ModuleCat.of A A)).inv ≫
HomologicalComplex.homologyMap (η n) 0 ≫ (e n).hom =
ModuleCat.ofHom
(Ideal.span (Set.range fun i ↦ f i ^ (n + 1))).mkQ
Tag 091Y, a lemma
Tag 091Y in the Stacks Project.
AdicKoszul.rlim_derivedTensor_koszulPowers_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/AdicKoszulTower.lean, line 244.
Stacks 091Y. Let
Ibe generated by a finite sequencef. For any inverse system whosen-th term is the Koszul complex onf i ^ (n + 1), the derived limit after derived tensoring withKis derived complete with respect toI.
theorem rlim_derivedTensor_koszulPowers_isDerivedComplete
{r : ℕ} (f : Fin r → A)
(τ : ∀ n : ℕ,
Koszul.seqComplex (fun i ↦ f i ^ (n + 2)) ⟶
Koszul.seqComplex (fun i ↦ f i ^ (n + 1)))
(T : DerivedTensorProduct A)
(K K' : DerivedCategory (ModuleCat.{u} A))
(hRlim : IsDerivedLimit (koszulPowerSystem f τ ⋙ T.tensor.obj K) K') :
IsDerivedComplete (Ideal.span (Set.range f)) K'
Tag 091Z, a lemma
Tag 091Z in the Stacks Project.
AdicKoszul.isDerivedComplete_iff_isIso_to_rlim_derivedTensor_koszulPowers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/AdicDerivedCompletionKoszul.lean, line 778.
The Koszul derived limit and its canonical natural map exist for every complex. A complex is derived complete for the ideal generated by
fif and only if the component of this map is an isomorphism. The ring and module universes are independent; only the tensor calculation is enlarged usingULift.
public theorem isDerivedComplete_iff_isIso_to_rlim_derivedTensor_koszulPowers
{r : ℕ} (f : Fin r → A)
(T : CochainComplex.DerivedTensor.DerivedTensorProduct (ULift.{v} A)) :
∃ C : KoszulPowerCompletion f T, ∀ K : DerivedCategory (ModuleCat.{v} A),
IsDerivedComplete (Ideal.span (Set.range f)) K ↔
IsIso (C.unit.app K)
Tag 0920, a lemma
Tag 0920 in the Stacks Project.
AdicKoszulAdjunction.koszulPowerDerivedLimit_isLeftAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/AdicDerivedCompletion/Adjunction.lean, line 226.
For a finite family
f, the functor whose value atKis the derived inverse limit ofK ⊗ᴸ Kₙ, whereKₙruns through the Koszul complexes on the positive powers off, is left adjoint to the inclusion of the derived-complete objects intoD(A).
public theorem koszulPowerDerivedLimit_isLeftAdjoint
(A : Type u) [CommRing A] {r : ℕ} (f : Fin r → A)
(T : CochainComplex.DerivedTensor.DerivedTensorProduct (ULift.{v} A))
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A))] :
letI : HasExactLimitsOfShape (Discrete ℕ) (ModuleCat.{max u v} (ULift.{v} A)) :=
moduleCat_hasExactLimitsOfShape_discrete.{max u v} (ULift.{v} A) ℕ
letI : HasProductsOfShape ℕ
(DerivedCategory (ModuleCat.{max u v} (ULift.{v} A))) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
let P : ObjectProperty (DerivedCategory (ModuleCat.{v} A)) :=
fun K ↦ IsDerivedComplete (Ideal.span (Set.range f)) K
∃ L : DerivedCategory (ModuleCat.{v} A) ⥤ P.FullSubcategory,
Nonempty (L ⊣ P.ι) ∧
∀ K, IsDerivedLimit (AdicKoszul.tensorKoszulPowerSystem f T K)
((AdicKoszul.derivedUniverseLift A).obj ((L ⋙ P.ι).obj K))
Tag 0H83, a lemma
Tag 0H83 in the Stacks Project.
KoszulTensorVanishing.positive_homology_isZero_iff_derivedTensorProduct_mod_ideal_iff_koszul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/KoszulTensorVanishing.lean, line 605.
Stacks Project, Tag 0H83. For a complex derived complete with respect to the ideal generated by a finite sequence, the following are equivalent: it has no positive cohomology, its derived reduction modulo that ideal has no positive cohomology, and its derived tensor product with the Koszul complex of the sequence has no positive cohomology.
theorem positive_homology_isZero_iff_derivedTensorProduct_mod_ideal_iff_koszul
{A : Type u} [CommRing A] {r : ℕ} (f : Fin r → A)
(K : DerivedCategory (ModuleCat.{u} A)) :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
IsDerivedComplete (Ideal.span (Set.range f)) K →
let I := Ideal.span (Set.range f)
let K₁ : DerivedCategory (ModuleCat.{u} A) :=
DerivedCategory.Q.obj
((ComplexShape.embeddingDownNat.extendFunctor (ModuleCat.{u} A)).obj
(Koszul.seqComplex f))
let p₁ := ∀ i : ℤ, 0 < i →
IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj K)
let p₂ := ∀ i : ℤ, 0 < i →
IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
(((canonicalDerivedTensorProductFunctor A).obj K).obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
(ModuleCat.of A (A ⧸ I)))))
let p₃ := ∀ i : ℤ, 0 < i →
IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj
(((canonicalDerivedTensorProductFunctor A).obj K).obj K₁))
(p₁ ↔ p₂) ∧ (p₂ ↔ p₃)
Tag 0G1U, a lemma
Tag 0G1U in the Stacks Project.
KoszulTensorVanishing.isZero_of_isDerivedComplete_of_derivedTensorProduct_mod_ideal_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/KoszulTensorVanishing.lean, line 659.
Derived Nakayama lemma, Stacks Project, Tag 0G1U. A derived-complete complex with respect to a finitely generated ideal is zero if its derived reduction modulo that ideal is zero.
theorem isZero_of_isDerivedComplete_of_derivedTensorProduct_mod_ideal_isZero
{A : Type u} [CommRing A] (I : Ideal A) (hI : I.FG)
(K : DerivedCategory (ModuleCat.{u} A)) :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
IsDerivedComplete I K →
IsZero
(((canonicalDerivedTensorProductFunctor A).obj K).obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
(ModuleCat.of A (A ⧸ I)))) →
IsZero K
Tag 0AAJ, a lemma
Tag 0AAJ in the Stacks Project.
CompletionAdjunction.derivedCompletion_finiteCohomologicalDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompletionAdjunction.lean, line 593.
Derived completion along an ideal generated by
relements has cohomological amplitude contained in[-r, 0]: it preserves isomorphisms in positive cohomological degrees and epimorphisms in degree zero, and it sends isomorphisms in negative degrees together with a monomorphism in degree zero to isomorphisms below degree-rand a monomorphism in degree-r.
public theorem derivedCompletion_finiteCohomologicalDimension
(A : Type u) [CommRing A]
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))]
{r : ℕ} (f : Fin r → A) :
let P : ObjectProperty (DerivedCategory (ModuleCat.{u} A)) :=
fun K ↦ IsDerivedComplete (Ideal.span (Set.range f)) K
∀ (C : DerivedCategory (ModuleCat.{u} A) ⥤ P.FullSubcategory),
(C ⊣ P.ι) →
∀ {K L : DerivedCategory (ModuleCat.{u} A)} (φ : K ⟶ L),
(((∀ i : ℤ, 1 ≤ i →
IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map φ)) ∧
Epi ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).map φ)) →
((∀ i : ℤ, 1 ≤ i →
IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
((C ⋙ P.ι).map φ))) ∧
Epi ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).map
((C ⋙ P.ι).map φ)))) ∧
(((∀ i : ℤ, i ≤ -1 →
IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map φ)) ∧
Mono ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).map φ)) →
((∀ i : ℤ, i ≤ -(r : ℤ) - 1 →
IsIso ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).map
((C ⋙ P.ι).map φ))) ∧
Mono ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-(r : ℤ))).map
((C ⋙ P.ι).map φ))))
Tag 0BKD, a lemma
Tag 0BKD in the Stacks Project.
AdicFilteredCompletion.exists_derivedCompletion_spectralSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/FilteredCompletionSpectralSequence.lean, line 184.
Stacks 0BKD. Let
Ibe a finitely generated ideal, and letK^•be a decreasingly filtered complex ofA-modules. There is a filtered representativeM^•of the derived completion ofK^•whose canonical spectral sequence consists of derived-complete modules from its first page onward and hasE₁^{p,q} ≅ H^{p+q}((gr^pK^•)^∧). If the filtration ofK^•is finite in each degree, the spectral sequence is bounded and converges canonically to the cohomology of(K^•)^∧.
theorem exists_derivedCompletion_spectralSequence
(A : Type u) [CommRing A]
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A))]
(I : Ideal A) (hI : I.FG)
(K : FilteredObject (CochainComplex (ModuleCat.{v} A) ℤ) ℤᵒᵖ) :
let P : ObjectProperty (DerivedCategory (ModuleCat.{v} A)) :=
fun L ↦ IsDerivedComplete I L
∀ (completion : DerivedCategory (ModuleCat.{v} A) ⥤ P.FullSubcategory),
(completion ⊣ P.ι) →
∃ (M : CochainComplex.Filtered (ModuleCat.{v} A))
(eTotal : DerivedCategory.Q.obj M.X ≅
(completion ⋙ P.ι).obj (DerivedCategory.Q.obj K.X))
(eCohomology : ∀ n : ℤ, M.X.homology n ≅
(DerivedCategory.homologyFunctor (ModuleCat.{v} A) n).obj
((completion ⋙ P.ι).obj (DerivedCategory.Q.obj K.X))),
let E := CochainComplex.Filtered.spectralSequenceFunctor.obj M
(∀ (r p q : ℤ) (hr : 1 ≤ r),
IsDerivedCompleteModule I ((E.page r (by omega)).X (p, q))) ∧
(∀ p q : ℤ, Nonempty
((E.page 1 (by omega)).X (p, q) ≅
(DerivedCategory.homologyFunctor (ModuleCat.{v} A) (p + q)).obj
((completion ⋙ P.ι).obj
(DerivedCategory.Q.obj ((FilteredObject.gr p).obj K))))) ∧
(K.filtration.IsDegreewiseFinite →
(∀ n : ℤ, {p : ℤ | ¬ IsZero ((E.page 1 (by omega)).X (p, n - p))}.Finite) ∧
(∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧
M.inducedFiltrationStep n a = ⊤ ∧ M.inducedFiltrationStep n b = ⊥) ∧
(∀ p q : ℤ, ∃ b : ℤ, ∀ (r : ℤ) (hr : 0 ≤ r), b ≤ r →
(E.page r hr).d (p, q) (p + r, q - r + 1) = 0) ∧
(∀ p n : ℤ,
IsGLB (Set.range fun r : ℕ ↦
CochainComplex.filtrationSubobject M p n ⊓
(Subobject.pullback (M.X.d n (n + 1))).obj
(CochainComplex.filtrationSubobject M (p + r) (n + 1)) ⊔
CochainComplex.filtrationSubobject M (p + 1) n)
(kernelSubobject (M.X.d n (n + 1)) ⊓ CochainComplex.filtrationSubobject M p n ⊔
CochainComplex.filtrationSubobject M (p + 1) n) ∧
IsLUB (Set.range fun r : ℕ ↦
CochainComplex.filtrationSubobject M p n ⊓
(Subobject.«exists» (M.X.d (n - 1) n)).obj
(CochainComplex.filtrationSubobject M (p - r) (n - 1)) ⊔
CochainComplex.filtrationSubobject M (p + 1) n)
(imageSubobject (M.X.d (n - 1) n) ⊓ CochainComplex.filtrationSubobject M p n ⊔
CochainComplex.filtrationSubobject M (p + 1) n)) ∧
(∀ p n : ℤ,
let C := (Subobject.pullback (M.X.iCycles n)).obj
(CochainComplex.filtrationSubobject M p n)
let N := kernelSubobject (M.X.d n (n + 1)) ⊓
CochainComplex.filtrationSubobject M p n ⊔
CochainComplex.filtrationSubobject M (p + 1) n
let B := imageSubobject (M.X.d (n - 1) n) ⊓
CochainComplex.filtrationSubobject M p n ⊔
CochainComplex.filtrationSubobject M (p + 1) n
∃ (a : (C : ModuleCat.{v} A) ⟶ (N : ModuleCat.{v} A))
(b : (C : ModuleCat.{v} A) ⟶ (M.inducedFiltrationStep n p : ModuleCat.{v} A))
(hFH : M.inducedFiltrationStep n (p + 1) ≤ M.inducedFiltrationStep n p)
(e : cokernel (Subobject.ofLE (B ⊓ N) N inf_le_right) ≅
cokernel (Subobject.ofLE _ _ hFH)),
C.arrow ≫ M.X.iCycles n = a ≫ N.arrow ∧
C.arrow ≫ M.X.homologyπ n =
b ≫ (M.inducedFiltrationStep n p).arrow ∧
a ≫ cokernel.π (Subobject.ofLE (B ⊓ N) N inf_le_right) ≫ e.hom =
b ≫ cokernel.π (Subobject.ofLE _ _ hFH)))
Tag 0BKE, an example
Tag 0BKE in the Stacks Project.
AdicFilteredCompletion.exists_spectralSequence_derivedCompletion_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/FilteredCompletionTruncation.lean, line 765.
Stacks 0BKE. For a finitely generated ideal
IandK ∈ D(A), the truncation filtration gives a bounded cohomological spectral sequenceS₁^{p,q} ≅ H^{2p+q}(H^{-p}(K)^∧)converging toH^{p+q}(K^∧). After the reindexingp = -j,q = i + 2jand a shift of the page number by one it is a bounded spectral sequence of derived-complete modules withE₂^{i,j} ≅ H^i(H^j(K)^∧)converging toH^{i+j}(K^∧).
theorem exists_spectralSequence_derivedCompletion_homology
(A : Type u) [CommRing A]
(I : Ideal A) (hI : I.FG) (K : DerivedCategory (ModuleCat.{v} A)) :
let P : ObjectProperty (DerivedCategory (ModuleCat.{v} A)) :=
fun L ↦ IsDerivedComplete I L
∃ (completion : DerivedCategory (ModuleCat.{v} A) ⥤ P.FullSubcategory)
(adj : completion ⊣ P.ι)
(C : CochainComplex (ModuleCat.{v} A) ℤ)
(eK : DerivedCategory.Q.obj C ≅ K)
(T : FilteredObject (CochainComplex (ModuleCat.{v} A) ℤ) ℤᵒᵖ)
(eUnderlying : T.X ≅ C)
(eStep : ∀ p : ℤ, T.filtration.obj (op p) ≅ C.truncLE (-p))
(eStep_ι : ∀ p : ℤ,
(eStep p).hom ≫ C.ιTruncLE (-p) =
T.filtration.ι.app (op p) ≫ eUnderlying.hom)
(hT : T.filtration.IsDegreewiseFinite)
(M : CochainComplex.Filtered (ModuleCat.{v} A))
(eTotal : DerivedCategory.Q.obj M.X ≅ (completion ⋙ P.ι).obj K)
(eCohomology : ∀ n : ℤ, M.X.homology n ≅
(DerivedCategory.homologyFunctor (ModuleCat.{v} A) n).obj
((completion ⋙ P.ι).obj K)),
let S := CochainComplex.Filtered.spectralSequenceFunctor.obj M
∃ (E : E₂CohomologicalSpectralSequence (ModuleCat.{v} A))
(eGr : ∀ p : ℤ,
DerivedCategory.Q.obj ((FilteredObject.gr p).obj T) ≅
((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).obj
((DerivedCategory.homologyFunctor (ModuleCat.{v} A) (-p)).obj K))⟦p⟧)
(e₁Filtered : ∀ p q : ℤ, (S.page 1 (by omega)).X (p, q) ≅
(DerivedCategory.homologyFunctor (ModuleCat.{v} A) (p + q)).obj
((completion ⋙ P.ι).obj
(DerivedCategory.Q.obj ((FilteredObject.gr p).obj T))))
(e₁ : ∀ p q : ℤ, (S.page 1 (by omega)).X (p, q) ≅
(DerivedCategory.homologyFunctor (ModuleCat.{v} A) (2 * p + q)).obj
((completion ⋙ P.ι).obj
((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).obj
((DerivedCategory.homologyFunctor (ModuleCat.{v} A) (-p)).obj K))))
(e₂ : ∀ i j : ℤ, (E.page 2).X (i, j) ≅
(DerivedCategory.homologyFunctor (ModuleCat.{v} A) i).obj
((completion ⋙ P.ι).obj
((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).obj
((DerivedCategory.homologyFunctor (ModuleCat.{v} A) j).obj K))))
(reindex : ∀ (r i j : ℤ) (hr : 2 ≤ r),
(E.page r hr).X (i, j) ≅ (S.page (r - 1) (by omega)).X (-j, i + 2 * j))
(hF : ∀ n : ℤ, Antitone (M.inducedFiltrationStep n)),
(∀ (r p q : ℤ) (hr : 1 ≤ r),
IsDerivedCompleteModule I ((S.page r (by omega)).X (p, q))) ∧
(∀ (r i j : ℤ) (hr : 2 ≤ r),
IsDerivedCompleteModule I ((E.page r hr).X (i, j))) ∧
(∀ (r i j : ℤ) (hr : 2 ≤ r),
(reindex r i j hr).hom ≫ (S.page (r - 1) (by omega)).d
(-j, i + 2 * j) (-(j - r + 1), (i + r) + 2 * (j - r + 1)) =
(E.page r hr).d (i, j) (i + r, j - r + 1) ≫
(reindex r (i + r) (j - r + 1) hr).hom) ∧
(∀ n : ℤ, {p : ℤ | ¬ IsZero ((S.page 1 (by omega)).X (p, n - p))}.Finite) ∧
(∀ n : ℤ, {i : ℤ | ¬ IsZero ((E.page 2).X (i, n - i))}.Finite) ∧
(∀ n : ℤ, ∃ a b : ℤ, a ≤ b ∧ M.inducedFiltrationStep n a = ⊤ ∧
M.inducedFiltrationStep n b = ⊥) ∧
(∀ p q : ℤ, ∃ (r₀ : ℤ) (hr₀ : 1 ≤ r₀), ∀ (r : ℤ) (hr : r₀ ≤ r),
(S.page r (by omega)).d (p, q) (p + r, q - r + 1) = 0 ∧
(S.page r (by omega)).d (p - r, q + r - 1) (p, q) = 0 ∧
Nonempty ((S.page r (by omega)).X (p, q) ≅
cokernel (Subobject.ofLE (M.inducedFiltrationStep (p + q) (p + 1))
(M.inducedFiltrationStep (p + q) p) (hF (p + q) (by omega))))) ∧
∀ i j : ℤ, ∃ (r₀ : ℤ) (hr₀ : 2 ≤ r₀), ∀ (r : ℤ) (hr : r₀ ≤ r),
(E.page r (by omega)).d (i, j) (i + r, j - r + 1) = 0 ∧
(E.page r (by omega)).d (i - r, j + r - 1) (i, j) = 0 ∧
Nonempty ((E.page r (by omega)).X (i, j) ≅
cokernel (Subobject.ofLE (M.inducedFiltrationStep (i + j) (-j + 1))
(M.inducedFiltrationStep (i + j) (-j)) (hF (i + j) (by omega))))
Tag 0924, a lemma
Tag 0924 in the Stacks Project.
isDerivedComplete_restrictScalars_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompleteRestrictScalars.lean, line 142.
A complex of
B-modules is derived complete for the extension ofItoBif and only if its restriction toAis derived complete forI. Equivalently, the inverse image ofD_comp(A, I)under restriction of scalars isD_comp(B, I B).
public theorem isDerivedComplete_restrictScalars_iff
(A : Type u) (B : Type v) [CommRing A] [CommRing B] (φ : A →+* B) (I : Ideal A)
(L : DerivedCategory (ModuleCat.{w} B)) :
IsDerivedComplete I ((ModuleCat.restrictScalars φ).mapDerivedCategory.obj L) ↔
IsDerivedComplete (I.map φ) L
Tag 0925, a lemma
Tag 0925 in the Stacks Project.
CompleteRestrictScalarsEquivalence.restrictScalars_equivalence_derivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompleteRestrictScalarsEquivalence/SmallQuotients.lean, line 694.
If
A → Bis flat and induces an isomorphism modulo a finitely generated idealI, then restriction of scalars induces an equivalence from the full subcategory ofI B-derived complete objects ofD(B)to the full subcategory ofI-derived complete objects ofD(A).
theorem restrictScalars_equivalence_derivedComplete
(A : Type u) (B : Type u) [CommRing A] [CommRing B] [Algebra A B]
(I : Ideal A) (hI : I.FG) (hflat : Module.Flat A B)
(hquot : Function.Bijective
(Ideal.quotientMap (I.map (algebraMap A B)) (algebraMap A B) Ideal.le_comap_map)) :
∃ hprodA : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)),
∃ hprodB : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} B)),
letI := hprodA
letI := hprodB
let completeA : ObjectProperty (DerivedCategory (ModuleCat.{u} A)) :=
fun K ↦ IsDerivedComplete I K
let completeB : ObjectProperty (DerivedCategory (ModuleCat.{u} B)) :=
fun K ↦ IsDerivedComplete (I.map (algebraMap A B)) K
let res := (ModuleCat.restrictScalars.{u} (algebraMap A B)).mapDerivedCategory
∃ hres : ∀ K : completeB.FullSubcategory, completeA (res.obj K.obj),
Functor.IsEquivalence
(completeA.lift (completeB.ι ⋙ res) (fun K ↦ hres K))
Sources
Section15.94 The category of derived complete modules#
Section 15.94 of the Stacks Project, Tag 0GLN. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GLP, a lemma
Tag 0GLP in the Stacks Project.
CompletionAdjunction.derivedCompleteModules_abelian_hasLimits_exact_hasColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompletionAdjunction.lean, line 854.
The full subcategory of modules derived complete with respect to an ideal is abelian and has all limits, and its inclusion into modules is exact and preserves limits. If the ideal is finitely generated, the subcategory has all colimits and the inclusion has a left adjoint.
public theorem derivedCompleteModules_abelian_hasLimits_exact_hasColimits
(A : Type u) [CommRing A] (I : Ideal A) :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
let P : ObjectProperty (ModuleCat.{u} A) :=
fun M => IsDerivedCompleteModule I M
let C := P.FullSubcategory
let F : C ⥤ ModuleCat.{u} A := P.ι
Nonempty (Abelian C) ∧
HasLimitsOfSize.{u, u} C ∧
PreservesLimitsOfSize.{u, u} F ∧
exactFunctor C (ModuleCat.{u} A) F ∧
(I.FG → HasColimitsOfSize.{u, u} C ∧ F.IsRightAdjoint)
Sources
Section15.95 Derived completion for a principal ideal#
Section 15.95 of the Stacks Project, Tag 0BKF. 12 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 091X, a lemma
Tag 091X in the Stacks Project.
ProTorsion.proIso_of_torsionBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/ProIsoBoundedTorsion.lean, line 1069.
Main statement. Let
Abe a commutative ring,f ∈ A, and assume thef-power torsion ofAis bounded, witnessed byc ≥ 1(soA[f^c] = A[f^m]for allm ≥ c). Then the explicit families of morphisms inD(A)
alpha n : K_n → A/(f^n)(the canonical map ontoH^0),beta c hc hstab n : A/(f^{n+c}) → K_n(built fromL_n = (A/A[f^c] →[f^{n+c}] A)and the quasi-isomorphismL_n ≃ A/(f^{n+c}), whose existence is derived fromhstab),defined above, induce an isomorphism of pro-objects between
{A/(f^n)}_{n ≥ 1}and{K_n}_{n ≥ 1}inD(A). Since Mathlib lacks a category of pro-objects, this is encoded by the two round-trip identities together with the compatibility of bothαandβwith the single-step transition maps:
- round trip through
{A/(f^•)}:β_n ≫ α_n = (A/(f^{n+c}) → A/(f^n));- round trip through
{K_•}:α_{n+c} ≫ β_n = (K_{n+c} → K_n);αcompatible with transitions:t_n ≫ α_n = α_{n+1} ≫ π_n;βcompatible with transitions:π_{(n+1)+c → n+c} ≫ β_n = β_{n+1} ≫ t_n.The hypotheses are exactly the boundedness data
c,1 ≤ c, andhstab; the existence ofβ(i.e. the relevant quasi-isomorphisms) is supplied internally byLqiCx_quasiIso.
theorem proIso_of_torsionBounded (c : ℕ)
(hstab : ∀ m : ℕ, c ≤ m → Submodule.torsionBy A A (f ^ c) = Submodule.torsionBy A A (f ^ m)) :
-- round trip through the system `{A/(f^•)}`
(∀ n : ℕ, beta A f c hstab n ≫ alpha A f n = Qtrans A f n c) ∧
-- round trip through the system `{K_•}`
(∀ n : ℕ, alpha A f (n + c) ≫ beta A f c hstab n = Ktrans A f n c) ∧
-- `α` is compatible with the single-step transition maps
(∀ n : ℕ, KtransOne A f n ≫ alpha A f n = alpha A f (n + 1) ≫ QtransOne A f n) ∧
-- `β` is compatible with the single-step transition maps
(∀ n : ℕ,
QtransOne A f (n + c) ≫ beta A f c hstab n
= eqToHom (by rw [Nat.add_right_comm]) ≫ beta A f c hstab (n +
1) ≫ KtransOne A f n)
Tag 0923, a lemma
Tag 0923 in the Stacks Project.
PrincipalNaiveCompletion.derivedCompletionToNaive_isIso_iff_torsionBounded, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/NoetherianCompletePrincipalIdeal.lean, line 4124.
Stacks 0923. For
f ∈ A, the canonical natural transformation from derived completion at(f)to the naive derived completion formed from the quotientsA/(f^(n+1))is an isomorphism if and only if thef-power torsion ofAis bounded.
public theorem derivedCompletionToNaive_isIso_iff_torsionBounded
(A : Type u) [CommRing A] (f : A)
(T : CochainComplex.DerivedTensor.DerivedTensorProduct A)
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))] :
let D := DerivedCategory (ModuleCat.{u} A)
let generators : Fin 1 → A := fun _ ↦ f
let P : ObjectProperty D :=
fun K ↦ IsDerivedComplete (Ideal.span (Set.range generators)) K
∃ (completion : D ⥤ P.FullSubcategory) (naiveCompletion : D ⥤ D)
(comparison : completion ⋙ P.ι ⟶ naiveCompletion),
Nonempty (completion ⊣ P.ι) ∧
(∀ K : D,
let koszulTower := NoetherianKoszulProIso.koszulPowerSystem generators ⋙ T.tensor.obj K
let quotientTower := NoetherianKoszulProIso.quotientPowerSystem generators ⋙ T.tensor.obj
K
∃ (p : (completion ⋙ P.ι).obj K ⟶
∏ᶜ fun n : ℕ ↦ koszulTower.obj (op n))
(δ : (∏ᶜ fun n : ℕ ↦ koszulTower.obj (op n)) ⟶
((completion ⋙ P.ι).obj K)⟦(1 : ℤ)⟧)
(q : naiveCompletion.obj K ⟶
∏ᶜ fun n : ℕ ↦ quotientTower.obj (op n))
(ε : (∏ᶜ fun n : ℕ ↦ quotientTower.obj (op n)) ⟶
(naiveCompletion.obj K)⟦(1 : ℤ)⟧),
Triangle.mk p
(Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ koszulTower.obj (op n)) n -
Pi.π (fun n : ℕ ↦ koszulTower.obj (op n)) (n + 1) ≫
koszulTower.map (homOfLE (Nat.le_succ n)).op)
δ ∈ distTriang D ∧
Triangle.mk q
(Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ quotientTower.obj (op n)) n -
Pi.π (fun n : ℕ ↦ quotientTower.obj (op n)) (n + 1) ≫
quotientTower.map (homOfLE (Nat.le_succ n)).op)
ε ∈ distTriang D ∧
∀ n : ℕ,
comparison.app K ≫ q ≫
Pi.π (fun n : ℕ ↦ quotientTower.obj (op n)) n =
p ≫ Pi.π (fun n : ℕ ↦ koszulTower.obj (op n)) n ≫
(T.tensor.obj K).map
((NoetherianKoszulProIso.koszulQuotientComparison generators).app (op n))) ∧
(IsIso comparison ↔ ProTorsion.TorsionBounded A f)
Tag 09AT, an example
Tag 09AT in the Stacks Project.
PrincipalAdicPresentation.isDerivedCompleteModule_iff_exists_shortExact_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/PrincipalAdicPresentation.lean, line 325.
Stacks 09AT. Let
fbe a nonzerodivisor in a commutative ringA. AnA-moduleMis derived complete with respect to(f)if and only if it occurs as the cokernel in a short exact sequence0 ⟶ K ⟶ L ⟶ M ⟶ 0, whereKandLaref-adically complete and multiplication byfis injective on both.
theorem isDerivedCompleteModule_iff_exists_shortExact_isAdicComplete
(A : Type u) [CommRing A] (f : A)
(hf : Function.Injective (LinearMap.lsmul A A f)) (M : ModuleCat.{u} A) :
letI : HasExactLimitsOfShape (Discrete ℕ) (ModuleCat.{u} A) :=
moduleCat_hasExactLimitsOfShape_discrete.{u} A ℕ
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
IsDerivedCompleteModule (Ideal.span {f}) M ↔
∃ (K L : ModuleCat.{u} A) (i : K ⟶ L) (p : L ⟶ M) (w : i ≫ p = 0),
(ShortComplex.mk i p w).ShortExact ∧
IsAdicComplete (Ideal.span {f}) K ∧
IsAdicComplete (Ideal.span {f}) L ∧
Function.Injective (LinearMap.lsmul A K f) ∧
Function.Injective (LinearMap.lsmul A L f)
Tag 0G3F, an example
Tag 0G3F in the Stacks Project.
PrincipalScaledVariable.scaledVariableCompletionCokernel_isDerivedComplete_not_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/PrincipalScaledVariable.lean, line 178.
Stacks 0G3F. Let
pbe prime. The cokernel of the map between thep-adic completions ofℤ_[p][X]induced byX ↦ pXis derived complete but not adically complete. The image of1 + pX + p²X² + ⋯is a nonzero element belonging to everyp^n M.
theorem scaledVariableCompletionCokernel_isDerivedComplete_not_isAdicComplete
(p : ℕ) [Fact p.Prime] :
let A := ℤ_[p]
let I : Ideal A := Ideal.span {(p : A)}
let φ : Polynomial A →ₗ[A] Polynomial A :=
(Polynomial.aeval ((p : A) • Polynomial.X)).toLinearMap
let φhat := AdicCompletion.map I φ
let M := HasQuotient.Quotient (AdicCompletion I (Polynomial A))
(LinearMap.range (φhat.restrictScalars A))
letI : HasExactLimitsOfShape (Discrete ℕ) (ModuleCat A) :=
moduleCat_hasExactLimitsOfShape_discrete A ℕ
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
IsDerivedCompleteModule I (ModuleCat.of A M) ∧
¬ IsAdicComplete I M ∧
∃ z : AdicCompletion I (Polynomial A),
(∀ n : ℕ, z.val n =
Submodule.Quotient.mk
(∑ i ∈ Finset.range n, (p : A) ^ i • (Polynomial.X : Polynomial A) ^ i)) ∧
Submodule.Quotient.mk z ≠ (0 : M) ∧
∀ n : ℕ, Submodule.Quotient.mk z ∈ I ^ n • (⊤ : Submodule A M)
Tag 0BKG, an example
Tag 0BKG in the Stacks Project.
CompletionSequences.derivedCompletion_principal_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompletionSequences/TruncationSequences.lean, line 456.
Stacks 0BKG. The two principal-completion short exact sequences, with their canonical maps.
Srecords the fixed mapping-cocone model, its comparison with the completion unit, and the normalized truncation maps. The remaining clauses retain all cohomology calculations, including both derived-limit realizations and the degree-one vanishing for the quotient system.
public theorem derivedCompletion_principal_homology
(A : Type u) [CommRing A]
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A))]
(f : A) :
let I : Ideal A := Ideal.span {f}
let P : ObjectProperty (DerivedCategory (ModuleCat.{v} A)) :=
fun L ↦ IsDerivedComplete I L
∀ (completion : DerivedCategory (ModuleCat.{v} A) ⥤ P.FullSubcategory)
(adj : completion ⊣ P.ι),
let completed := completion ⋙ P.ι
∃ S : PrincipalCompletionSequences A f completed adj.unit,
(∀ M : ModuleCat.{v} A,
let Mhat := completed.obj ((single A 0).obj M)
let torsionRlim := moduleDerivedLimit A (powerTorsionSystem A M f)
let quotientRlim := moduleDerivedLimit A (powerQuotientSystem A M f)
∃ (eT : FirstDerivedLimitComparison A (powerTorsionSystem A M f))
(eQ : FirstDerivedLimitComparison A (powerQuotientSystem A M f)),
IsDerivedLimit (powerTorsionSystem A M f ⋙ single A 0) torsionRlim ∧
IsDerivedLimit (powerQuotientSystem A M f ⋙ single A 0) quotientRlim ∧
Nonempty ((homology A (-1)).obj Mhat ≅ adicTateModule A M f) ∧
(ShortComplex.mk (eT.iso.hom ≫ (S.moduleSequence M).inclusion)
(S.moduleSequence M).projection
(by rw [Category.assoc, (S.moduleSequence M).zero, comp_zero])).ShortExact ∧
Nonempty ((homology A 1).obj Mhat ≅ (homology A 1).obj quotientRlim) ∧
IsZero ((homology A 1).obj quotientRlim) ∧
∀ n : ℤ, n ≠ -1 → n ≠ 0 → IsZero ((homology A n).obj Mhat)) ∧
∀ (K : DerivedCategory (ModuleCat.{v} A)) (p : ℤ),
(ShortComplex.mk ((S.truncation K p).inclusion S.shift)
((S.truncation K p).projection f S.shift
(S.moduleSequence ((homology A (p + 1)).obj K)).tateIso)
(S.truncation_zero K p)).ShortExact
Tag 0H32, a lemma
Tag 0H32 in the Stacks Project.
PrincipalCompletionDiagram.derivedCompletion_principal_homology_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/CompletionSequencesComparison/ComparisonDiagram.lean, line 760.
Stacks 0H32. For
K ∈ D(A), the ordinary completion ofHᵖ(K), the cohomology of the derived completion ofHᵖ(K), the cohomology of the derived completion ofK, and the inverse limits of the cohomology ofK ⊗ᴸ_A (A →[f^n] A)form the canonical commutative diagram of four short exact sequences from the source. Its bottom comparison is an isomorphism between the indicated first derived inverse limits.
public theorem derivedCompletion_principal_homology_comparison
(A : Type u) [CommRing A]
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A))]
(f : A) (K : DerivedCategory (ModuleCat.{v} A)) (p : ℤ) :
let I : Ideal A := Ideal.span {f}
let P : ObjectProperty (DerivedCategory (ModuleCat.{v} A)) :=
fun L ↦ IsDerivedComplete I L
∀ (completion : DerivedCategory (ModuleCat.{v} A) ⥤ P.FullSubcategory)
(adj : completion ⊣ P.ι),
let completed := completion ⋙ P.ι
∃ S : CompletionSequences.PrincipalCompletionSequences A f completed adj.unit,
let H (q : ℤ) := (homologyFunctor (ModuleCat.{v} A) q).obj K
let C := DerivedCategory.Q.objPreimage K
let eK := DerivedCategory.Q.objObjPreimageIso K
let E := PrincipalTorsionTower.principalComplexSystem A f C
let tensorSystem := principalDerivedTensorSystem A f K
let homologySystem (q : ℤ) := tensorSystem ⋙ homologyFunctor (ModuleCat.{v} A) q
let T := CompletionSequences.milnorTriangle A E
let completionIso := completed.mapIso eK.symm ≪≫ S.comparison.iso C
let coneTriangle (n : ℕ) := DerivedCategory.Q.mapTriangle.obj
(CochainComplex.mappingCone.triangle (f ^ (n + 1) • 𝟙 C))
let ordinaryCompletion := limit (CompletionSequences.powerQuotientSystem A (H p) f)
let limitHpTensor := limit (homologySystem p)
let tate := CompletionSequences.adicTateModule A (H (p + 1)) f
let H0CompletedHp := (homologyFunctor (ModuleCat.{v} A) 0).obj
(completed.obj ((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).obj (H p)))
let HpCompletedK := (homologyFunctor (ModuleCat.{v} A) p).obj (completed.obj K)
let R1Torsion := CompletionSequences.firstDerivedLimit A
(PrincipalTorsionTower.powerTorsionSystem A (H p) f)
let R1PreviousTensor := CompletionSequences.firstDerivedLimit A (homologySystem (p - 1))
let middleIn : H0CompletedHp ⟶ HpCompletedK := (S.truncation K p).inclusion S.shift
let middleOut : HpCompletedK ⟶ tate :=
(S.truncation K p).projection f S.shift (S.moduleSequence (H (p + 1))).tateIso
let leftIn : R1Torsion ⟶ H0CompletedHp := (S.moduleSequence (H p)).inclusion
let leftOut : H0CompletedHp ⟶ ordinaryCompletion := (S.moduleSequence (H p)).projection
∃ (termIn : CompletionSequences.powerQuotientSystem A (H p) f ⟶ homologySystem p)
(termOut : homologySystem p ⟶ PrincipalTorsionTower.powerTorsionSystem A (H (p + 1)) f)
(previousOut : homologySystem (p - 1) ⟶ PrincipalTorsionTower.powerTorsionSystem A (H p) f)
(productIso : (homologyFunctor (ModuleCat.{v} A) (p - 1)).obj T.obj₃ ≅
CompletionSequences.moduleProduct A (homologySystem (p - 1)))
(topIn : ordinaryCompletion ⟶ limitHpTensor)
(topOut : limitHpTensor ⟶ tate)
(htop : topIn ≫ topOut = 0)
(columnIn : R1PreviousTensor ⟶ HpCompletedK)
(columnOut : HpCompletedK ⟶ limitHpTensor)
(hcolumn : columnIn ≫ columnOut = 0)
(bottom : R1Torsion ≅ R1PreviousTensor),
(∀ n : ℕ,
cokernel.π (PrincipalTorsionTower.powerMultiplication A (H p) (f ^ (n + 1))) ≫
termIn.app ⟨n⟩ =
(homologyFunctor (ModuleCat.{v} A) p).map (eK.inv ≫ (coneTriangle n).mor₂)) ∧
(∀ n : ℕ,
termOut.app ⟨n⟩ ≫
kernel.ι (PrincipalTorsionTower.powerMultiplication A (H (p + 1)) (f ^ (n + 1))) =
(homologyFunctor (ModuleCat.{v} A) 0).homologySequenceδ
(coneTriangle n) p (p + 1) (by omega) ≫
(homologyFunctor (ModuleCat.{v} A) (p + 1)).map eK.hom) ∧
(∀ n : ℕ,
previousOut.app ⟨n⟩ ≫
kernel.ι (PrincipalTorsionTower.powerMultiplication A (H p) (f ^ (n + 1))) =
(homologyFunctor (ModuleCat.{v} A) 0).homologySequenceδ
(coneTriangle n) (p - 1) p (by omega) ≫
(homologyFunctor (ModuleCat.{v} A) p).map eK.hom) ∧
(∀ n : ℕ, topIn ≫ limit.π (homologySystem p) ⟨n⟩ =
limit.π (CompletionSequences.powerQuotientSystem A (H p) f) ⟨n⟩ ≫ termIn.app ⟨n⟩) ∧
(∀ n : ℕ, topOut ≫ limit.π (PrincipalTorsionTower.powerTorsionSystem A (H (p + 1)) f) ⟨n⟩ =
limit.π (homologySystem p) ⟨n⟩ ≫ termOut.app ⟨n⟩) ∧
(∀ n : ℕ, productIso.hom ≫
Pi.π (fun n : ℕ ↦ (homologySystem (p - 1)).obj ⟨n⟩) n =
(homologyFunctor (ModuleCat.{v} A) (p - 1)).map
(DerivedCategory.Q.map (Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) n))) ∧
(productIso.hom ≫ cokernel.π (CompletionSequences.moduleDifference A (homologySystem (p -
1))) ≫
columnIn = (homologyFunctor (ModuleCat.{v} A) 0).homologySequenceδ T (p - 1) p
(by omega) ≫ (homologyFunctor (ModuleCat.{v} A) p).map completionIso.inv) ∧
(cokernel.π (CompletionSequences.moduleDifference A (homologySystem (p - 1))) ≫ bottom.inv =
(Pi.lift fun n : ℕ ↦
Pi.π (fun n : ℕ ↦ (homologySystem (p - 1)).obj ⟨n⟩) n ≫
previousOut.app ⟨n⟩) ≫
cokernel.π (CompletionSequences.moduleDifference A
(PrincipalTorsionTower.powerTorsionSystem A (H p) f))) ∧
(∀ n : ℕ, columnOut ≫ limit.π (homologySystem p) ⟨n⟩ =
(homologyFunctor (ModuleCat.{v} A) p).map (completionIso.hom ≫ T.mor₁ ≫
DerivedCategory.Q.map (Pi.π (fun n : ℕ ↦ E.obj ⟨n⟩) n))) ∧
(ShortComplex.mk topIn topOut htop).ShortExact ∧
(ShortComplex.mk middleIn middleOut (S.truncation_zero K p)).ShortExact ∧
(ShortComplex.mk leftIn leftOut (S.moduleSequence (H p)).zero).ShortExact ∧
(ShortComplex.mk columnIn columnOut hcolumn).ShortExact ∧
middleIn ≫ columnOut = leftOut ≫ topIn ∧
middleOut = columnOut ≫ topOut ∧
bottom.hom ≫ columnIn = leftIn ≫ middleIn
Tag 0H33, a remark
Tag 0H33 in the Stacks Project.
PrincipalTorsionTower.isMittagLeffler_principalDerivedTensor_iff_powerTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/PrincipalTorsionTower.lean, line 213.
The cohomology tower of the derived reductions of
Kmodulo the positive powers offis Mittag--Leffler if and only if the tower of elements ofH^(p + 1)(K)killed by those powers is Mittag--Leffler.
theorem isMittagLeffler_principalDerivedTensor_iff_powerTorsion
(A : Type u) [CommRing A] (f : A)
(K : DerivedCategory (ModuleCat.{v} A)) (p : ℤ) :
((principalDerivedTensorSystem A f K ⋙
homologyFunctor (ModuleCat.{v} A) p) ⋙ forget (ModuleCat.{v} A)).IsMittagLeffler ↔
((powerTorsionSystem A ((homologyFunctor (ModuleCat.{v} A) (p + 1)).obj K) f) ⋙
forget (ModuleCat.{v} A)).IsMittagLeffler
Tag 0CQY, a lemma
Tag 0CQY in the Stacks Project.
DerivedCompleteTorsion.exists_pow_smul_top_eq_bot_of_isDerivedCompleteModule_of_isIPowerTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/TorsionAnnihilation.lean, line 420.
If
Iis finitely generated andMis both derived complete andI-power torsion, then a single power ofIannihilates all ofM.
theorem exists_pow_smul_top_eq_bot_of_isDerivedCompleteModule_of_isIPowerTorsion
(I : Ideal A) (M : ModuleCat.{v} A) (hI : I.FG)
(hM : IsDerivedCompleteModule I M)
(htors : IsIPowerTorsion A M I) :
∃ n : ℕ, I ^ n • (⊤ : Submodule A M) = ⊥
Tag 0G3G, a lemma
Tag 0G3G in the Stacks Project.
PrincipalCompletionKernel.iInf_principal_powers_annihilates_ker_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/PrincipalCompletionKernel.lean, line 180.
Stacks 0G3G. Let
Jbe the intersection of all powers of the principal ideal(f). IfMis derived complete with respect tof, thenJannihilates the kernel of the canonical map fromMto itsf-adic completion. In particular, ifAis derived complete with respect tof, thenJis square-zero.
public theorem iInf_principal_powers_annihilates_ker_adicCompletion
(A : Type u) [CommRing A] (f : A) (M : Type v) [AddCommGroup M] [Module A M] :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{v} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
let I := Ideal.span ({f} : Set A)
let J := ⨅ n : ℕ, I ^ n
(IsDerivedCompleteModule I (ModuleCat.of A M) →
J • (AdicCompletion.of I M).ker = ⊥) ∧
(IsDerivedCompleteModule I (ModuleCat.of A A) →
J ^ 2 = ⊥)
Tag 0G3H, a lemma
Tag 0G3H in the Stacks Project.
PrincipalHenselianPair.henselianPair_of_isDerivedCompleteModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/PrincipalHenselianPair.lean, line 149.
Stacks 0G3H. A commutative ring derived complete with respect to an ideal forms a henselian pair with that ideal.
theorem henselianPair_of_isDerivedCompleteModule
(A : Type u) [CommRing A] (I : Ideal A) :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_nat
IsDerivedCompleteModule I (ModuleCat.of A A) → HenselianPair A I
Tag 0G3I, a lemma
Tag 0G3I in the Stacks Project.
PrincipalCompletionNilpotent.iInf_powers_pow_two_pow_eq_bot_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/PrincipalCompletionNilpotent.lean, line 114.
Stacks 0G3I. If a commutative ring is derived complete with respect to an ideal
Igenerated byrelements, then the2 ^ r-th power of the intersection of all powers ofIis zero.
theorem iInf_powers_pow_two_pow_eq_bot_of_isDerivedComplete
(A : Type u) [CommRing A] (I : Ideal A) (r : ℕ) (f : Fin r → A)
(hI : I = Ideal.span (Set.range f)) :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_nat
IsDerivedCompleteModule I (ModuleCat.of A A) →
(⨅ n : ℕ, I ^ n) ^ (2 ^ r) = ⊥
Tag 0G5V, a lemma
Tag 0G5V in the Stacks Project.
PrincipalCompletionNilpotent.isAdicComplete_of_isReduced_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/PrincipalCompletionNilpotent.lean, line 183.
Stacks 0G5V. A reduced commutative ring which is derived complete with respect to a finitely generated ideal is adically complete with respect to that ideal.
theorem isAdicComplete_of_isReduced_of_isDerivedComplete
(A : Type u) [CommRing A] [IsReduced A] (I : Ideal A) (hI : I.FG) :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_nat
IsDerivedCompleteModule I (ModuleCat.of A A) → IsAdicComplete I A
Sources
Section15.96 Derived completion for Noetherian rings#
Section 15.96 of the Stacks Project, Tag 0BKH. 7 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0921, a lemma
Tag 0921 in the Stacks Project.
NoetherianKoszulProIso.koszulPowerSystem_proIso_quotientPowerSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/NoetherianKoszulProIso.lean, line 750.
Stacks Project, Tag 0921. Over a Noetherian ring, the inverse systems in the derived category formed by the Koszul complexes on the positive powers of a finite sequence and by the corresponding quotients are isomorphic as pro-objects. Concretely, the comparison is a natural transformation, and at every level it admits an inverse after passing to a later level. The first of the two displayed identities is precisely the factorization through the quotient asserted in the source.
public theorem koszulPowerSystem_proIso_quotientPowerSystem
{A : Type u} [CommRing A] [IsNoetherianRing A] {r : ℕ} (f : Fin r → A) :
∀ n : ℕ, ∃ (m : ℕ) (h : n ≤ m)
(s : (quotientPowerSystem f).obj (op m) ⟶
(koszulPowerSystem f).obj (op n)),
(koszulQuotientComparison f).app (op m) ≫ s =
(koszulPowerSystem f).map (homOfLE h).op ∧
s ≫ (koszulQuotientComparison f).app (op n) =
(quotientPowerSystem f).map (homOfLE h).op
Tag 0922, a proposition
Tag 0922 in the Stacks Project.
NoetherianAdicCompletion.idealPowerDerivedLimit_isLeftAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/NoetherianCompleteIdealPowers.lean, line 1146.
Stacks 0922. Over a Noetherian ring, derived completion is left adjoint to the inclusion of derived-complete objects and is computed by
R lim (K ⊗ᴸ[A] A/Iⁿ). The adjunction unit induces the canonical reduction map at every level of the tower. The projections are natural inKand are the actual projections of the derived limit.The reflector acts on
ModuleCat.{v} Afor an independent module universev. In the tensor formula only, the exact functorUlifts to modules overULift.{v} A;Jis the same ideal transported alongULift.ringEquiv.
public theorem idealPowerDerivedLimit_isLeftAdjoint
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(T : CochainComplex.DerivedTensor.DerivedTensorProduct (ULift.{v} A)) :
let P : ObjectProperty (DerivedCategory (ModuleCat.{v} A)) :=
fun K ↦ IsDerivedComplete I K
let U := AdicKoszul.derivedUniverseLift.{u, v} A
let J := I.comap ULift.ringEquiv.toRingHom
∃ L : DerivedCategory (ModuleCat.{v} A) ⥤ P.FullSubcategory,
∃ adj : L ⊣ P.ι,
∃ π : ∀ n : ℕ, (L ⋙ P.ι) ⋙ U ⟶
U ⋙ T.tensor.flip.obj ((idealPowerQuotientSystem J).obj ⟨n⟩),
(∀ K, IsDerivedLimitWithProjections
(idealPowerQuotientSystem J ⋙ T.tensor.obj (U.obj K))
(U.obj ((L ⋙ P.ι).obj K)) (fun n ↦ (π n).app K)) ∧
∀ K n, U.map (adj.unit.app K) ≫ (π n).app K =
(derivedReductionMap J T n).app (U.obj K)
Tag 0EET, a lemma
Tag 0EET in the Stacks Project.
AdicCompletionTor.derivedCompletion_homology_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/DerivedHomCompletionTorSequence.lean, line 1111.
Stacks 0EET. Over a Noetherian ring, derived completion has Milnor short exact sequences. For a module these read
0 ⟶ R¹ lim Tor_(i+1)(M, A/Iⁿ) ⟶ H^(-i)(M^∧) ⟶ lim Tor_i(M, A/Iⁿ) ⟶ 0. For a derived object, the Tor systems are replaced by the cohomology systems of its derived tensors withA/Iⁿ. The latter assertion is valid for every derived object, and in particular for every object ofD⁻(A).
public theorem derivedCompletion_homology_shortExact
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(T : CochainComplex.DerivedTensor.DerivedTensorProduct A)
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))] :
let P : ObjectProperty (DerivedCategory (ModuleCat.{u} A)) :=
fun K ↦ IsDerivedComplete I K
∃ L : DerivedCategory (ModuleCat.{u} A) ⥤ P.FullSubcategory,
Nonempty (L ⊣ P.ι) ∧
(∀ K, IsDerivedLimit
(NoetherianAdicCompletion.idealPowerQuotientSystem I ⋙ T.tensor.obj K)
((L ⋙ P.ι).obj K)) ∧
(∀ (M : ModuleCat.{u} A) (i : ℕ),
let M₀ := (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj M
let Mhat := (L ⋙ P.ι).obj M₀
let R1limTor := firstDerivedInverseLimit (torIdealPowerSystem I M (i + 1))
let HminusI := (DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-(i : ℤ))).obj Mhat
let limTor := limit (torIdealPowerSystem I M i)
∃ (a : R1limTor ⟶ HminusI) (b : HminusI ⟶ limTor) (w : a ≫ b = 0),
(ShortComplex.mk a b w).ShortExact) ∧
(∀ (K : DerivedCategory (ModuleCat.{u} A)) (p : ℤ),
let Khat := (L ⋙ P.ι).obj K
let H := derivedTensorHomologySystem T I K
let R1limH := firstDerivedInverseLimit (H (p - 1))
let Hp := (DerivedCategory.homologyFunctor (ModuleCat.{u} A) p).obj Khat
let limH := limit (H p)
∃ (a : R1limH ⟶ Hp) (b : Hp ⟶ limH) (w : a ≫ b = 0),
(ShortComplex.mk a b w).ShortExact)
Tag 0A06, a lemma
Tag 0A06 in the Stacks Project.
AdicCompletionCohomology.derivedCompletion_homology_iso_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/NoetherianCohomologyAdicCompletion.lean, line 290.
If every cohomology module of a complex over a Noetherian ring is finite, then the cohomology modules of its derived completion are the adic completions of the original cohomology modules.
public theorem derivedCompletion_homology_iso_adicCompletion
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(K : DerivedCategory (ModuleCat.{u} A))
(hK : ∀ n : ℤ,
Module.Finite A ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) n).obj K)) :
letI : HasExactLimitsOfShape (Discrete ℕ) (ModuleCat.{u} A) :=
moduleCat_hasExactLimitsOfShape_discrete.{u} A ℕ
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
let P : ObjectProperty (DerivedCategory (ModuleCat.{u} A)) :=
fun L ↦ IsDerivedComplete I L
∀ (C : DerivedCategory (ModuleCat.{u} A) ⥤ P.FullSubcategory),
(C ⊣ P.ι) → ∀ n : ℤ,
Nonempty
(((DerivedCategory.homologyFunctor (ModuleCat.{u} A) n).obj
((C ⋙ P.ι).obj K)) ≅
ModuleCat.of A
(AdicCompletion I
((DerivedCategory.homologyFunctor (ModuleCat.{u} A) n).obj K)))
Tag 09BA, a lemma
Tag 09BA in the Stacks Project.
FiniteDerivedComplete.exists_finite_adicCompletionModule_of_isDerivedCompleteModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/NoetherianExtFiniteComplete.lean, line 357.
Stacks 09BA. A derived-complete module over a Noetherian ring whose reduction modulo
Iis finite is canonically itsI-adic completion and is finite over the completed ring.
public theorem exists_finite_adicCompletionModule_of_isDerivedCompleteModule
(A : Type u) [CommRing A] [IsNoetherianRing A]
(I : Ideal A) (M : ModuleCat.{v} A)
(hM : IsDerivedCompleteModule I M)
(hfin : Module.Finite (A ⧸ I) (M ⧸ (I • ⊤ : Submodule A M))) :
∃ moduleM : Module (AdicCompletion I A) M,
letI := moduleM
IsScalarTower A (AdicCompletion I A) M ∧
Module.Finite (AdicCompletion I A) M ∧
∃ e : M ≃ₗ[AdicCompletion I A] AdicCompletion I M,
∀ m, e m = AdicCompletion.of I M m
Tag 0EEU, a lemma
Tag 0EEU in the Stacks Project.
AdicCompletionFlatTensor.derivedCompletion_iso_adicCompletion_of_finite_tensor_flat_and_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/NoetherianCompleteFlatTensor.lean, line 406.
Let
Ibe an ideal of a Noetherian ringA. DerivedI-adic completion agrees with ordinaryI-adic completion for the tensor product of a finite module with a flat module, and for the localization of a finite module at one element.
public theorem derivedCompletion_iso_adicCompletion_of_finite_tensor_flat_and_localization
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(T : CochainComplex.DerivedTensor.DerivedTensorProduct A)
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))] :
let P : ObjectProperty (DerivedCategory (ModuleCat.{u} A)) :=
fun K ↦ IsDerivedComplete I K
∀ (L : Functor (DerivedCategory (ModuleCat.{u} A)) P.FullSubcategory),
Nonempty (L ⊣ P.ι) →
(∀ K, IsDerivedLimit
(NoetherianAdicCompletion.idealPowerQuotientSystem I ⋙ T.tensor.obj K)
((L ⋙ P.ι).obj K)) →
let isUsual (Q : Type u) [AddCommGroup Q] [Module A Q] : Prop :=
Nonempty
((L ⋙ P.ι).obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
(ModuleCat.of A Q)) ≅
(DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
(ModuleCat.of A (AdicCompletion I Q)))
(∀ (M N : Type u) [AddCommGroup M] [Module A M] [Module.Finite A M]
[AddCommGroup N] [Module A N] [Module.Flat A N],
isUsual (TensorProduct A M N)) ∧
(∀ (M Mf : Type u) [AddCommGroup M] [Module A M] [Module.Finite A M]
[AddCommGroup Mf] [Module A Mf] (f : A) (φ : M →ₗ[A] Mf)
[IsLocalizedModule (Submonoid.powers f) φ],
isUsual Mf)
Tag 0EEV, a lemma
Tag 0EEV in the Stacks Project.
AdicCompletionPseudoCoherentTensor.derivedCompletion_tensor_iso_of_boundedAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedComplete/NoetherianTorPseudoCoherent.lean, line 918.
Stacks 0EEV. Derived completion of a bounded-above complex commutes with derived tensor product by a finite module, and more generally by a pseudo-coherent complex.
public theorem derivedCompletion_tensor_iso_of_boundedAbove
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(T : CochainComplex.DerivedTensor.DerivedTensorProduct A)
[HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{u} A))] :
let P : ObjectProperty (DerivedCategory (ModuleCat.{u} A)) :=
fun K ↦ IsDerivedComplete I K
∀ (C : Functor (DerivedCategory (ModuleCat.{u} A)) P.FullSubcategory),
Nonempty (C ⊣ P.ι) →
(∀ K, IsDerivedLimit
(NoetherianAdicCompletion.idealPowerQuotientSystem I ⋙ T.tensor.obj K)
((C ⋙ P.ι).obj K)) →
∀ (K : DerivedCategory (ModuleCat.{u} A)),
DerivedCategory.TStructure.t.minus K →
(∀ (M : Type u) [AddCommGroup M] [Module A M] [Module.Finite A M],
Nonempty
((C ⋙ P.ι).obj
((T.tensor.obj K).obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
(ModuleCat.of A M))) ≅
(T.tensor.obj ((C ⋙ P.ι).obj K)).obj
((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
(ModuleCat.of A M)))) ∧
(∀ L : DerivedCategory (ModuleCat.{u} A), StacksDraft.PseudoCoherence.IsPseudoCoherent L →
Nonempty
((C ⋙ P.ι).obj ((T.tensor.obj K).obj L) ≅
(T.tensor.obj ((C ⋙ P.ι).obj K)).obj L))
Sources
Section15.97 An operator introduced by Berthelot and Ogus#
Section 15.97 of the Stacks Project, Tag 0F7N. 12 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GSN, an example
Tag 0GSN in the Stacks Project.
Stacks.Eta.DerivedFunctor.eta_commutes_shift_but_not_triangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Derived.lean, line 908.
Stacks 0GSN. The cone triangle of multiplication by
fonAin degree one is distinguished. Its eta cone is homotopic to zero. Iffis not a unit, the first eta arrow is not invertible and the image triangle is not distinguished. The compatible shift comparison is the fixed multiplication-by-fmapetaShiftIso_one_hom_app_f_val.
theorem eta_commutes_shift_but_not_triangulated
(f : A) (hf : f ∈ nonZeroDivisors A) :
let g := etaCounterexampleMap.{u, v} f hf
let q := HomotopyCategory.quotient (FTorsionFreeModule.{u, v} f) (ComplexShape.up ℤ)
let T := CochainComplex.mappingCone.triangleh g
T ∈ distTriang (HomotopyCategory (FTorsionFreeModule.{u, v} f) (ComplexShape.up ℤ)) ∧
IsZero ((etaHomotopyFunctor f).obj (q.obj (CochainComplex.mappingCone g))) ∧
(¬ IsUnit f →
¬ IsIso ((etaHomotopyFunctor f).map (q.map g)) ∧
(etaHomotopyFunctor f).mapTriangle.obj T ∉
distTriang (HomotopyCategory (FTorsionFreeModule.{u, v} f) (ComplexShape.up ℤ)))
Tag 0F7P, a lemma
Tag 0F7P in the Stacks Project.
Stacks.Decalage.Cohomology.tag_0F7P_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Cohomology.lean, line 466.
Stacks Tag 0F7P (isomorphism form). Multiplication by
f^{j+1}descends to a canonical isomorphismH^{j+1}(M^•) / H^{j+1}(M^•)[f] ≅ H^{j+1}(η_f M^•).
theorem tag_0F7P_iso (C : FTFComplex A f) (j : ℤ) :
∃ (Φ : Hcohom C j →ₗ[A] Heta C j)
(e : (Hcohom C j ⧸ LinearMap.ker Φ) ≃ₗ[A] Heta C j),
(∀ ξ : Hcohom C j, ξ ∈ LinearMap.ker Φ ↔ f • ξ = 0) ∧
(∀ ξ : Hcohom C j, e (Submodule.Quotient.mk ξ) = Φ ξ)
Tag 0F7Q, a lemma
Tag 0F7Q in the Stacks Project.
Stacks.Eta.QuasiIsoPreservation.quasiIso_etaPow_of_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Derived.lean, line 1076.
Stacks 0F7Q. The Berthelot--Ogus décalage of a quasi-isomorphism of complexes of
f-torsion-free modules is a quasi-isomorphism.
theorem quasiIso_etaPow_of_quasiIso
{A : Type u} [CommRing A] {f : A} (_hf : f ∈ nonZeroDivisors A)
(E : EtaFunctor.{u, v} f)
{M N : CochainComplex (FTorsionFreeModule.{u, v} f) ℤ} (g : M ⟶ N)
(hg : QuasiIso ((underlyingComplex f).map g)) :
QuasiIso ((underlyingComplex f).map (E.functor.map g))
Stacks.Eta.GoodBaseChange.quasiIso_etaMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/GoodBaseChange.lean, line 318. The attribute's comment: “stated for EtaComplex.etaObject”.
The décalage
EtaComplex.etaMap f φof a quasi-isomorphismφbetween complexes off-torsion-freeA-modules is a quasi-isomorphism.
theorem quasiIso_etaMap (f : A) (hf : f ∈ nonZeroDivisors A)
{K L : CochainComplex (ModuleCat.{u} A) ℤ}
(hK : EtaComplex.IsTorsionFree f K) (hL : EtaComplex.IsTorsionFree f L)
(φ : K ⟶ L) (hφ : QuasiIso φ) :
QuasiIso (EtaComplex.etaMap f φ)
Tag 0F7R, a lemma
Tag 0F7R in the Stacks Project.
Stacks.Eta.DerivedDescent.exists_additive_derived_eta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Derived.lean, line 1385.
Stacks 0F7R. For a nonzerodivisor
f, the Berthelot--Ogus décalage descends to an additive endofunctor of the derived category. On every complex off-torsion-free modules it is naturally isomorphic, on objects and morphisms, to the chain-level décalage.
theorem exists_additive_derived_eta
{A : Type u} [CommRing A] [HasDerivedCategory.{w} (ModuleCat.{max u v} A)]
(f : A) (hf : f ∈ nonZeroDivisors A) :
∃ (Leta : DerivedCategory (ModuleCat.{max u v} A) ⥤
DerivedCategory (ModuleCat.{max u v} A)),
Leta.Additive ∧
∃ E : EtaFunctor.{u, v} f,
Nonempty (underlyingComplex f ⋙ DerivedCategory.Q ⋙ Leta ≅
E.functor ⋙ underlyingComplex f ⋙ DerivedCategory.Q)
Tag 0F7S, a remark
Tag 0F7S in the Stacks Project.
Stacks.Eta.Reduction.exists_boundary_subcomplex_of_etaQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Reduction.lean, line 688.
Stacks 0F7S. Modulo a nonzerodivisor
f, the eta complex has an acyclic subcomplex with degree-itermB^(i+1) ⊕ B^i, and the quotient complex has the cohomology modules ofM/fMas its terms, with the induced differential transported along the equivalencese. The final three clauses give the representative formulas for the mapst,s, ands'from the source.
theorem exists_boundary_subcomplex_of_etaQuotient
(f : A) (_hf : f ∈ nonZeroDivisors A)
(C : EtaComplex.Complex.{u, v} A) (hC : EtaComplex.IsTorsionFree f C) :
let barTerm : ℤ → Type (max u v) := fun i =>
(C.X i) ⧸ LinearMap.range (EtaComplex.scalarMap f (C.X i))
∃ barD : ∀ i j, barTerm i →ₗ[A] barTerm j,
(∀ i (x : C.X i),
barD i (i + 1) (Submodule.Quotient.mk x) =
Submodule.Quotient.mk ((C.d i (i + 1)).hom x)) ∧
(∀ i j, i + 1 ≠ j → barD i j = 0) ∧
(∀ i (x : barTerm i), barD (i + 1) (i + 1 + 1) (barD i (i + 1) x) = 0) ∧
let B : ∀ i, Submodule A (barTerm i) := fun i =>
LinearMap.range (barD (i - 1) i)
let Z : ∀ i, Submodule A (barTerm i) := fun i => LinearMap.ker (barD i (i + 1))
let H : ℤ → Type (max u v) := fun i =>
(Z i) ⧸ (B i).comap (Z i).subtype
let Q : ℤ → Type (max u v) := fun i => EtaComplex.QuotientTerm f C i
∃ (hBZ : ∀ i, B i ≤ Z i)
(s : ∀ i, B (i + 1) →ₗ[A] Q i)
(s' : ∀ i, B i →ₗ[A] Q i)
(t : ∀ i, Q i →ₗ[A] Z i)
(e : ∀ i,
(Q i ⧸ LinearMap.range (LinearMap.coprod (s i) (s' i))) ≃ₗ[A] H i),
(∀ i, Function.Injective (LinearMap.coprod (s i) (s' i))) ∧
(∀ i, Function.Injective (s i)) ∧
(∀ i, Function.Surjective (t i)) ∧
(∀ i, Function.Exact (s i) (t i)) ∧
(∀ i (bNext : B (i + 1)) (b : B i),
t i (s i bNext + s' i b) = ⟨b, hBZ i b.2⟩) ∧
(∀ i (bNext : B (i + 1)) (b : B i),
EtaComplex.quotientDifferential f C i (s i bNext + s' i b) =
s' (i + 1) bNext) ∧
(∀ i, Function.Exact
(fun p : B i × B (i - 1) => ((0 : B (i + 1)), p.1))
(fun p : B (i + 1) × B i => ((0 : B (i + 1 + 1)), p.1))) ∧
(∀ i (q : Q i),
e i (Submodule.Quotient.mk q) = Submodule.Quotient.mk (t i q)) ∧
(∃ dH : ∀ i, H i →ₗ[A] H (i + 1),
(∀ i (q : Q i),
e (i + 1) (Submodule.Quotient.mk
(EtaComplex.quotientDifferential f C i q)) =
dH i (e i (Submodule.Quotient.mk q))) ∧
(∀ i (h : H i), dH (i + 1) (dH i h) = 0)) ∧
(∀ i (x : C.X i)
(hx : EtaPow.fpowMap f (C.X i) i x ∈ EtaComplex.term f C i),
∃ hz : Submodule.Quotient.mk x ∈ Z i,
t i (Submodule.Quotient.mk
(⟨EtaPow.fpowMap f (C.X i) i x, hx⟩ : EtaComplex.term f C i)) =
⟨Submodule.Quotient.mk x, hz⟩) ∧
(∀ i (y : C.X (i + 1)) (hy : Submodule.Quotient.mk y ∈ B (i + 1))
(y' : C.X (i + 1)) (x : C.X i)
(_heq : y = f • y' + (C.d i (i + 1)).hom x),
∃ heta : EtaPow.fpowMap f (C.X i) (i + 1) x ∈ EtaComplex.term f C i,
s i ⟨Submodule.Quotient.mk y, hy⟩ =
Submodule.Quotient.mk
(⟨EtaPow.fpowMap f (C.X i) (i + 1) x, heta⟩ :
EtaComplex.term f C i)) ∧
(∀ i (x : C.X i) (hx : Submodule.Quotient.mk x ∈ B i)
(x' : C.X i) (z : C.X (i - 1))
(_heq : x = f • x' + (C.d (i - 1) i).hom z),
∃ heta : EtaPow.fpowMap f (C.X i) i ((C.d (i - 1) i).hom z) ∈
EtaComplex.term f C i,
s' i ⟨Submodule.Quotient.mk x, hx⟩ =
Submodule.Quotient.mk
(⟨EtaPow.fpowMap f (C.X i) i ((C.d (i - 1) i).hom z), heta⟩ :
EtaComplex.term f C i))
Tag 0GSP, an equation
Tag 0GSP in the Stacks Project.
Stacks.EtaComplex.FractionalPowerBockstein.powerBocksteinOperator_eq_connectingHom_comp_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Reduction.lean, line 1133.
Stacks 0GSP. For the actual fractional power ideals in
A[1/f], the Bockstein operator for the successive-quotient row equals the connecting morphism of the unquotiented row followed by cohomology of the canonical reductionfⁱ⁺¹A → fⁱ⁺¹A/fⁱ⁺²A, after tensoring both rows withM. The definitions above formally identify every object and map with the power-ideal diagram in the source.
theorem powerBocksteinOperator_eq_connectingHom_comp_reduction
(f : A) (hf : f ∈ nonZeroDivisors A)
(M : CochainComplex (ModuleCat.{u} A) ℤ) (hM : ∀ n, IsSMulRegular (M.X n) f)
(i n : ℤ) :
∃ (hUpper : (powerIdealShortComplex M f i).ShortExact)
(hLower : (successivePowerQuotientShortComplex M f i).ShortExact),
powerBocksteinOperator M f i n hLower =
hUpper.δ n (n + 1) (by simp [ComplexShape.up]) ≫
HomologicalComplex.homologyMap
((tensorWithCochainComplex M).map
(cokernel.π (fractionalPowerInclusion f (i + 1)))) (n + 1)
Tag 0GSQ, an equation
Tag 0GSQ in the Stacks Project.
EtaPow.Bockstein.bocksteinComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Reduction.lean, line 1239.
Stacks 0GSQ. The complex
Hᵇ(M/f)has termHⁱ(M ⊗ fⁱA/fⁱ⁺¹A)in degreeiand the canonical Bockstein map as its differential.
def bocksteinComplex (f : A) (hf : f ∈ nonZeroDivisors A)
(M : CochainComplex (ModuleCat.{u} A) ℤ)
(hM : ∀ n, IsSMulRegular (M.X n) f) :
CochainComplex (ModuleCat.{u} A) ℤ
Tag 0F7T, a lemma
Tag 0F7T in the Stacks Project.
Stacks.EtaComplex.ModNonzerodivisor.etaTensorMod_to_bockstein_quasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Reduction.lean, line 2099.
Stacks 0F7T. If
fis a nonzerodivisor and every term ofMisf-torsion-free, the canonical map fromη_f M ⊗_A A/fAto the Bockstein complex ofM/fis a quasi-isomorphism.
theorem etaTensorMod_to_bockstein_quasiIso
(f : A) (hf : f ∈ nonZeroDivisors A)
(M : CochainComplex (ModuleCat.{u} A) ℤ)
(hM : ∀ i, IsSMulRegular (M.X i) f) :
QuasiIso
((etaTensorQuotientIso f hf M hM).hom ≫ etaQuotientToBockstein f hf M hM)
Tag 0F7Y, a lemma
Tag 0F7Y in the Stacks Project.
Stacks.Eta.BocksteinVanishing.cyclesReduction_epi_iff_powerBocksteinOperator_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Reduction.lean, line 2471.
Stacks 0F7Y. For a complex of
f-torsion-free modules, reduction from cycles modulof²to cycles modulofis surjective if and only if the corresponding Bockstein operator is zero. Moreover, these equivalent conditions hold if multiplication byfis injective onHⁱ⁺¹(M).
theorem cyclesReduction_epi_iff_powerBocksteinOperator_eq_zero
(f : A) (hf : f ∈ nonZeroDivisors A)
(M : CochainComplex (ModuleCat.{v} A) ℤ) (hM : ∀ n, IsSMulRegular (M.X n) f)
(i : ℤ) :
let K := commonUniverseComplex M
let f' : ULift.{v} A := ULift.up f
let hf' := ulift_mem_nonZeroDivisors f hf
let hK := fun n => commonUniverseModules_regular (M.X n) f (hM n)
let hLower := (powerIdealRows_shortExact f' hf' K hK i).2
let cyclesReduction := HomologicalComplex.cyclesMap
(literalPowerQuotientShortComplex K f').g i
(Epi cyclesReduction ↔ powerBocksteinOperator K f' i i hLower = 0) ∧
(IsSMulRegular (M.homology (i + 1)) f → Epi cyclesReduction)
Tag 0F7Z, a lemma
Tag 0F7Z in the Stacks Project.
Stacks.Eta.ReductionDirectSum.etaQuotient_range_eq_prod_of_cyclesReduction_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Reduction.lean, line 2667.
Stacks 0F7Z. If cycles modulo
flift to cycles modulof², the canonical map(1, dⁱ)embeds the degree-ieta term modulofas a product of a submodule offⁱCⁱ/fⁱ⁺¹Cⁱand a submodule offⁱ⁺¹Cⁱ⁺¹/fⁱ⁺²Cⁱ⁺¹.
theorem etaQuotient_range_eq_prod_of_cyclesReduction_surjective
(f : A) (_hf : f ∈ nonZeroDivisors A)
(C : EtaComplex.Complex.{u, v} A) (hC : EtaComplex.IsTorsionFree f C)
(i : ℤ) :
let mul : ∀ _n : ℕ, ∀ j : ℤ, C.X j →ₗ[A] C.X j := fun n j =>
{ toFun := fun x => (f ^ n) • x
map_add' := fun x y => smul_add (f ^ n) x y
map_smul' := fun a x => by simp only [RingHom.id_apply, smul_comm a (f ^ n)] }
let modTerm : ℕ → ℤ → Type (max u v) := fun n j =>
(C.X j) ⧸ LinearMap.range (mul n j)
let dMod : ∀ n j, modTerm n j →ₗ[A] modTerm n (j + 1) := fun n j =>
Submodule.mapQ _ _ (C.d j (j + 1)).hom (by
rintro _ ⟨x, rfl⟩
exact ⟨(C.d j (j + 1)).hom x, by
exact (map_smul (C.d j (j + 1)).hom (f ^ n) x).symm⟩)
let reduction : ∀ j, modTerm 2 j →ₗ[A] modTerm 1 j := fun j =>
Submodule.mapQ _ _ LinearMap.id (by
rintro _ ⟨x, rfl⟩
refine ⟨f • x, ?_⟩
change f ^ 1 • (f • x) = f ^ 2 • x
simp only [pow_one, pow_two, mul_smul])
(∀ x : modTerm 1 i, dMod 1 i x = 0 →
∃ y : modTerm 2 i, dMod 2 i y = 0 ∧ reduction i y = x) →
let P₀ := EtaPow.fpowSub f (C.X i) i
let P₁ := EtaPow.fpowSub f (C.X i) (i + 1)
let Q₀ := EtaPow.fpowSub f (C.X (i + 1)) (i + 1)
let Q₁ := EtaPow.fpowSub f (C.X (i + 1)) (i + 2)
let leftPowerQuotient := P₀ ⧸ P₁.comap P₀.subtype
let rightPowerQuotient := Q₀ ⧸ Q₁.comap Q₀.subtype
∃ (canonical : EtaComplex.QuotientTerm f C i →ₗ[A]
leftPowerQuotient × rightPowerQuotient)
(Z : Submodule A leftPowerQuotient) (B : Submodule A rightPowerQuotient),
(∀ x : EtaComplex.term f C i,
canonical (Submodule.Quotient.mk x) =
(Submodule.Quotient.mk (⟨x.1, x.2.1⟩ : P₀),
Submodule.Quotient.mk
(⟨EtaPow.fLoc f (C.d i (i + 1)).hom x.1, x.2.2⟩ : Q₀))) ∧
Function.Injective canonical ∧ LinearMap.range canonical = Z.prod B
Tag 0F7U, a lemma
Tag 0F7U in the Stacks Project.
EtaDecalage.etaFetaG_eq_etaFG_cochainComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Composition.lean, line 295.
For a cochain complex
M^•ofA-modules, the cochain complexesη_f (η_g M^•)andη_{fg} M^•inCochainComplex (ModuleCat A) ℤare equal.
theorem etaFetaG_eq_etaFG_cochainComplex (hdd : ∀ i, (d (i + 1)).comp (d i) = 0)
(preserve : ∀ i, ((etaFetaG (f := f) (g := g) (d := d)) i).map (dLoc f g M d i)
≤ (etaFetaG (f := f) (g := g) (d := d)) (i + 1)) :
(etaFetaG (f := f) (g := g) (d := d)).toCochainComplex preserve hdd
= (etaFG (f := f) (g := g) (d := d)).toCochainComplex
(by rw [← etaFetaG_eq_etaFG hdd]; exact preserve) hdd
Tag 0GSR, a lemma
Tag 0GSR in the Stacks Project.
Stacks.Eta.BaseChange.algebraMap_mem_nonZeroDivisors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/BaseChange.lean, line 168. The attribute's comment: “g is a nonzerodivisor”.
Statement 1. If
fis a nonzerodivisor inAandA → Bis flat, then its imageg = algebraMap A B fis a nonzerodivisor inB.
theorem algebraMap_mem_nonZeroDivisors (f : A) [Module.Flat A B] (hf : f ∈ nonZeroDivisors A) :
(algebraMap A B f) ∈ nonZeroDivisors B
Stacks.Eta.BaseChange.isSMulRegular_baseChange_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/BaseChange.lean, line 176. The attribute's comment: “the base change is g-torsion free”.
Statement 2. For
A → Bflat andM^•a complex off-torsion freeA-modules, each base-changed termM^i ⊗_A Bisg-torsion free, whereg = algebraMap A B f.
theorem isSMulRegular_baseChange_X (f : A) [Module.Flat A B] (M : CochainComplex (ModuleCat A) ℤ)
(hM : ∀ i, IsSMulRegular (M.X i) f) (i : ℤ) :
IsSMulRegular (B ⊗[A] (M.X i : Type _)) (algebraMap A B f)
Stacks.Eta.BaseChange.etaBaseChangeTerm_eq_fetaTerm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/BaseChange.lean, line 706. The attribute's comment: “eta commutes with the base change”.
Statement 3. With the identification of Definition 4,
η_f M^• ⊗_A B = η_g (M^• ⊗_A B)as complexes ofg-torsion freeB-modules.This is the equality, for every
i ∈ ℤ, of twoB-submodules of the common ambient module(M^i ⊗_A B)_g = LocalizedModule (powers g) (B ⊗_A M^i):
- the base change
(η_f M)^i ⊗_A B(etaBaseChangeTerm f M i), and- the degree-
iterm(η_g (M^• ⊗_A B))^iof the décalage of the base-changed complex,fetaTerm g (d^i ⊗ id_B) i.The second conjunct records compatibility with the differentials: the localized base-changed differential
d^i ⊗ id_Bcarries the degree-iterm into the degree-(i+1)term, exhibiting the equality as an equality of subcomplexes.
theorem etaBaseChangeTerm_eq_fetaTerm (f : A) [Module.Flat A B] (M : CochainComplex (ModuleCat A) ℤ)
(i : ℤ) :
(etaBaseChangeTerm f M i
= fetaTerm (algebraMap A B f)
(LinearMap.baseChange B (M.d i (i + 1)).hom) i) ∧
Submodule.map (fLoc (algebraMap A B f) (LinearMap.baseChange B (M.d i (i + 1)).hom))
(fetaTerm (algebraMap A B f) (LinearMap.baseChange B (M.d i (i + 1)).hom) i)
≤ fetaTerm (algebraMap A B f) (LinearMap.baseChange B (M.d (i + 1) (i + 1 + 1)).hom) (i +
1)
Stacks.Eta.GoodBaseChange.isIso_etaBaseChangeMap_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/GoodBaseChangeFlat.lean, line 122. The attribute's comment: “the comparison B ⊗_A (η_f K) ⟶ η_g (B ⊗_A K) is an isomorphism of complexes, for a flat ring map and an arbitrary cochain complex”.
More on Algebra, Tag 0GSR as an isomorphism of complexes. Let
A → Bbe a flat map of commutative rings, letf ∈ Awith imageg = algebraMap A B f, and letKbe a cochain complex ofA-modules. Then the canonical comparison
B ⊗_A (η_f K) ⟶ η_g (B ⊗_A K)is an isomorphism of complexes of
B-modules: the décalage commutes with flat base change.The tag itself,
Stacks.Eta.BaseChange.etaBaseChangeTerm_eq_fetaTerm, states this as an equality ofB-submodules of one ambient localization in each degree; what is added here is that the comparison realizing that equality is a degreewise bijection, which isStacks.Eta.GoodBaseChange.bijective_psiTermMap_of_flat.
theorem isIso_etaBaseChangeMap_of_flat (f : A) [Module.Flat A B]
(K : CochainComplex (ModuleCat.{u} A) ℤ) :
IsIso (etaBaseChangeMap (B := B) f K)
Sources
Section15.98 Perfect complexes and the eta operator#
Section 15.98 of the Stacks Project, Tag 0F7V. 9 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0GSS, a lemma
Tag 0GSS in the Stacks Project.
Stacks.Eta.DeterminantalIdeal.pow_mul_idealI_eq_of_derived_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/DeterminantalIdeal.lean, line 1188.
Stacks 0GSS. Let
fbe a nonzerodivisor and letMandNbe bounded complexes of finite free modules representing isomorphic objects of the derived category. Ifmandnare nonnegative integers such thatm + ∑_{j ≥ i} (-1)^(j-i) rank(Mʲ) = n + ∑_{j ≥ i} (-1)^(j-i) rank(Nʲ), thenfᵐ I_i(M, f) = fⁿ I_i(N, f)as ideals.
public theorem pow_mul_idealI_eq_of_derived_iso
{A : Type*} [CommRing A] (f : A) (hf : f ∈ nonZeroDivisors A)
(M N : BoundedComplex A) (i : ℤ) (m n : ℕ)
(hMN : Nonempty ((DerivedCategory.Q).obj M.toCochainComplex ≅
(DerivedCategory.Q).obj N.toCochainComplex))
(hEuler : (m : ℤ) + M.tailEulerCharacteristic i =
(n : ℤ) + N.tailEulerCharacteristic i) :
Ideal.span {f ^ m} * idealI M f i = Ideal.span {f ^ n} * idealI N f i
Tag 0GST, a lemma
Tag 0GST in the Stacks Project.
idealI_unit_mul_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/BoundedComplex.lean, line 255.
Stacks Tag 0GST (Lemma 15.98.2). Let
Abe a commutative ring,f ∈ Aa nonzerodivisor, andu ∈ Aa unit. For a bounded complexM^•of finite freeA-modules and everyi ∈ ℤ,I_i(M^•, f) = I_i(M^•, u·f).
theorem idealI_unit_mul_eq (C : BoundedComplex A) (f : A) (u : Aˣ) (i : ℤ) :
idealI C f i = idealI C ((u : A) * f) i
Tag 0GSU, a lemma
Tag 0GSU in the Stacks Project.
map_idealI_eq_idealI_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/LinearAlgebra/Matrix/BoundedComplex.lean, line 130.
Stacks Tag 0GSU (Lemma 15.98.3). Let
φ : A → Bbe a ring map,fa nonzerodivisor inA,C = M^•a bounded complex of finite freeA-modules, and assumeg = φ(f)is a nonzerodivisor inB. Then for everyi ∈ ℤ, the extension ofI_i(M^•, f)alongφequalsI_i(M^• ⊗_A B, g).
theorem map_idealI_eq_idealI_baseChange {A B : Type*} [CommRing A] [CommRing B] (φ : A →+* B)
(f : A) (C : BoundedComplex A) (i : ℤ) :
Ideal.map φ (idealI C f i) = idealI (C.baseChange φ) (φ f) i
Tag 0GSV, a lemma
Tag 0GSV in the Stacks Project.
Stacks.DeterminantalIdeal.FreeHomology.localized_idealI_eq_span_pow_of_free_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/DeterminantalIdeal.lean, line 1437.
Stacks 0GSV. If the localization at
pof every cohomology module of a bounded complexMof finite free modules is free, then for every degree the localization ofI_i(M, f)is generated by a power of the nonzerodivisorf.
public theorem localized_idealI_eq_span_pow_of_free_homology
{A : Type*} [CommRing A] (p : Ideal A) [p.IsPrime]
(f : A) (hf : f ∈ nonZeroDivisors A) (M : BoundedComplex A)
(hfree : ∀ i : ℤ, Module.Free (Localization.AtPrime p)
(LocalizedModule p.primeCompl
((HomologicalComplex.homologyFunctor (ModuleCat A) (ComplexShape.up ℤ) i).obj
M.toCochainComplex))) :
∀ i : ℤ, ∃ n : ℕ,
Ideal.map (algebraMap A (Localization.AtPrime p)) (idealI M f i) =
Ideal.span {(algebraMap A (Localization.AtPrime p) f) ^ n}
Tag 0F7W, a lemma
Tag 0F7W in the Stacks Project.
EtaPow.LocallyFree.etaTerm_finite_projective_and_split_of_idealI_isPrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/LocallyFree.lean, line 443.
Stacks 0F7W. Let
fbe a nonzerodivisor and letCbe a bounded complex of finite free modules. If the ideal generated by the maximal minors of(f, dⁱ)is principal, then the degree-ieta term is finite locally free of rankrank C i. Its natural mapx ↦ (x, dⁱx)intofⁱ Cⁱ × fⁱ⁺¹ Cⁱ⁺¹admits a linear retraction, and hence includes it as a direct summand.
public theorem etaTerm_finite_projective_and_split_of_idealI_isPrincipal
{A : Type*} [CommRing A] (C : BoundedComplex A) (f : A) (hf : IsRegular f) (i : ℤ)
(hI : (idealI C f i).IsPrincipal) :
let d := (C.d i).mulVecLin
let E := fetaTerm f d i
let P := fpowSub f (Fin (C.rank i) → A) i
let Q := fpowSub f (Fin (C.rank (i + 1)) → A) (i + 1)
let inclusion : E →ₗ[A] P × Q := LinearMap.prod
(LinearMap.codRestrict P E.subtype (fun x => x.2.1))
(LinearMap.codRestrict Q ((fLoc f d).comp E.subtype) (fun x => x.2.2))
(∃ hfin : Module.Finite A E,
letI := hfin
∃ hproj : Module.Projective A E,
letI := hproj
Module.rankAtStalk (R := A) E = fun _ => C.rank i) ∧
∃ retraction : P × Q →ₗ[A] E,
retraction.comp inclusion = LinearMap.id
Tag 0F7X, a lemma
Tag 0F7X in the Stacks Project.
Stacks.Eta.GoodBaseChange.isIso_etaBaseChangeMap_toCochainComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/GoodBaseChange.lean, line 499. The attribute's comment: “the comparison chain map of this file is an isomorphism”.
For a bounded complex
Cof finite freeA-modules all of whose determinantal idealsI_i(C, f)are principal, the canonical base-change comparisonB ⊗_A (η_f C) ⟶ η_g (B ⊗_A C)is an isomorphism of complexes.
theorem isIso_etaBaseChangeMap_toCochainComplex (C : BoundedComplex A) (f : A) (hf : IsRegular f)
(hg : IsRegular (algebraMap A B f)) (hI : ∀ i : ℤ, (idealI C f i).IsPrincipal) :
IsIso (etaBaseChangeMap (B := B) f C.toCochainComplex)
Stacks.Eta.LocallyFreeTerms.eta_baseChange_of_idealI_isPrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/LocallyFree.lean, line 702.
Stacks 0F7X. Let
A → Bbe a ring map, letfbe a nonzerodivisor ofAwhose image is a nonzerodivisor ofB, and letCbe a bounded complex of finite freeA-modules. If every determinantal idealIᵢ(C, f)is principal, then base change of the eta construction agrees in every degree with the eta construction of the base-changed complex. The equality takes place inside the localization of the finite freeB-module after applying the canonical localization--base-change and finite-free base-change identifications.
public theorem eta_baseChange_of_idealI_isPrincipal
{A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
(C : BoundedComplex A) (f : A) (hf : IsRegular f)
(hg : IsRegular (algebraMap A B f))
(hI : ∀ i : ℤ, (idealI C f i).IsPrincipal) :
∀ i : ℤ,
let freeBaseChange := TensorProduct.piScalarRight A B B (Fin (C.rank i))
let ambientMap :=
((LocalizedModule.map (Submonoid.powers (algebraMap A B f))
freeBaseChange.toLinearMap).restrictScalars B).comp
(Stacks.Eta.BaseChange.psiEquiv f (Fin (C.rank i) → A)).toLinearMap
Submodule.map ambientMap
(Submodule.baseChange B (fetaTerm f (C.d i).mulVecLin i)) =
fetaTerm (algebraMap A B f)
((C.baseChange (algebraMap A B)).d i).mulVecLin i
Stacks.Eta.LocallyFreeTerms.etaTermBaseChangeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/LocallyFree.lean, line 1045. The attribute's comment: “the canonical isomorphism, degreewise: the comparison map etaTermBaseChangeMap, induced by the ambient comparison, is bijective in every degree. That these degreewise isomorphisms are compatible with the two differentials is ambientBaseChangeMap_comp_fLoc; they are not assembled into one isomorphism of cochain complexes here.”.
[Stacks, Tag 0F7X] in degree
i, as an isomorphism. For a ring mapA → Bunder which the nonzerodivisorfstays a nonzerodivisor, and a bounded complexM^•of finite freeA-modules all of whose determinantal idealsI_i(M^•, f)are principal, the canonical map(η_f M^•)^i ⊗_A B ⟶ (η_g (M^• ⊗_A B))^iofStacks.Eta.LocallyFreeTerms.etaTermBaseChangeMapis an isomorphism.
noncomputable def etaTermBaseChangeEquiv (C : BoundedComplex A) (f : A) (hf : IsRegular f)
(hg : IsRegular (algebraMap A B f)) (hI : ∀ i : ℤ, (idealI C f i).IsPrincipal) (i : ℤ) :
(B ⊗[A] (fetaTerm f (C.d i).mulVecLin i)) ≃ₗ[B]
fetaTerm (algebraMap A B f) ((C.d i).map (algebraMap A B)).mulVecLin i
Tag 0F80, a lemma
Tag 0F80 in the Stacks Project.
Stacks.SplitInjectionDirectSum.main_theorem_0f80, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Module/SplitInjection.lean, line 351.
Theorem (Stacks Tag 0F80, Lemma 15.98.7). Let
Abe a commutative ring, letM,N₁,N₂be finite projectiveA-modules, and lets : M → N₁ × N₂be a split injection. Then there exists a finitely generated idealJ ⊆ Asuch that, for every commutative ringBand every ring mapA → B, the mapA → Bfactors throughA/J(J ≤ ker(A → B)) if and only if the base-changed maps_BidentifiesM_Bwith a direct sum of submodules ofN_{1,B} ⊕ N_{2,B}(Definition 4).
theorem main_theorem_0f80
[Module.Finite A M] [Module.Projective A M]
[Module.Finite A N₁] [Module.Projective A N₁]
[Module.Finite A N₂] [Module.Projective A N₂]
(s : M →ₗ[A] (N₁ × N₂)) (hs : IsSplitInjective s) :
∃ J : Ideal A, J.FG ∧
∀ (B : Type v) [CommRing B] [Algebra A B],
(J ≤ RingHom.ker (algebraMap A B)) ↔ IdentifiesDirectSum s B
Tag 0GSW, a lemma
Tag 0GSW in the Stacks Project.
Stacks.Decalage.DirectSumIdeal.etaDirectSumIdeal_eq_of_derived_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/DirectSum.lean, line 438.
Stacks 0GSW. If
MandNare bounded complexes of finite free modules representing isomorphic objects in the derived category and everyI_i(M, f)is principal, then their direct-sum idealsJ_i(-, f)inA / fAagree in every degree.
public theorem etaDirectSumIdeal_eq_of_derived_iso
{A : Type u} [CommRing A] (f : A) (hf : IsRegular f)
(M N : BoundedComplex A)
(hMN : Nonempty ((DerivedCategory.Q).obj M.toCochainComplex ≅
(DerivedCategory.Q).obj N.toCochainComplex))
(_hI : ∀ i : ℤ, (idealI M f i).IsPrincipal) :
∀ i : ℤ, etaDirectSumIdeal M f i = etaDirectSumIdeal N f i
Tag 0F81, a lemma
Tag 0F81 in the Stacks Project.
Stacks.Decalage.ObstructionIdeal.exists_fg_obstructionIdeal_with_finiteProjective_etaHomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Eta/Perfect/DirectSum.lean, line 1612.
Stacks 0F81. The sum of the degreewise direct-sum obstruction ideals is finitely generated. Its quotient is a finitely presented closed immersion, the ideal vanishes at primes where cycles lift (equivalently, where the localized Bockstein operators vanish), primes where all localized cohomology modules are free belong to this locus, and after quotienting by the obstruction ideal all cohomology modules of the eta complex are finite projective.
public theorem exists_fg_obstructionIdeal_with_finiteProjective_etaHomology
{A : Type u} [CommRing A] (C : BoundedComplex A) (f : A) (hf : IsRegular f)
(hI : ∀ i : ℤ, (idealI C f i).IsPrincipal) :
let R := A ⧸ Ideal.span {f}
let M := associatedComplex C
∃ (Jᵢ : ℤ → Ideal R) (J : Ideal R),
(∀ i, (Jᵢ i).FG) ∧
(∀ i : ℤ, ∀ (B : Type v) [CommRing B] [Algebra R B],
Jᵢ i ≤ RingHom.ker (algebraMap R B) ↔
Stacks.SplitInjectionDirectSum.IdentifiesDirectSum (etaReductionMap C f i) B) ∧
(∀ i, C.rank i = 0 → C.rank (i + 1) = 0 → Jᵢ i = ⊥) ∧
(J = ⨆ i, Jᵢ i) ∧
J.FG ∧
Function.Surjective (Ideal.Quotient.mk J) ∧
RingHom.FinitePresentation (Ideal.Quotient.mk J) ∧
({p : Ideal A | ∃ hp : p.IsPrime, CyclesLiftAt C f p hp} =
{p : Ideal A | ∃ hp : p.IsPrime, BocksteinVanishesAt C f p hp}) ∧
(∀ (p : Ideal A) [hp : p.IsPrime], CyclesLiftAt C f p hp →
Subsingleton (LocalizedModule p.primeCompl J)) ∧
(∀ (p : Ideal A) [hp : p.IsPrime], f ∈ p →
(∀ i : ℤ, Module.Free (Localization.AtPrime p)
((associatedComplex (C.baseChange
(algebraMap A (Localization.AtPrime p)))).homology i)) →
CyclesLiftAt C f p hp) ∧
let S := R ⧸ J
let φ : A →+* S := (Ideal.Quotient.mk J).comp (Ideal.Quotient.mk (Ideal.span {f}))
let ηM := ((ModuleCat.extendScalars φ).mapHomologicalComplex
(ComplexShape.up ℤ)).obj (EtaComplex.etaObject f M)
∀ i : ℤ,
∃ hfin : Module.Finite S (ηM.homology i),
letI := hfin
Module.Projective S (ηM.homology i)
Sources
Section15.99 Taking limits of complexes#
Section 15.99 of the Stacks Project, Tag 09B6. 6 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0CQF, a lemma
Tag 0CQF in the Stacks Project.
StacksDraft.DerivedInverseLimit.derivedLimit_isPseudoCoherent_and_baseChange_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Limits/PseudoCoherent/DerivedLimit.lean, line 412.
Stacks 0CQF. Suppose a tower of rings has surjective transition maps with locally nilpotent kernels, and its derived module objects are preserved by the base-change maps induced by their transitions. If all terms are pseudo-coherent, or one term is pseudo-coherent and all subsequent kernels are nilpotent, then every derived inverse limit is pseudo-coherent and its canonical base-change map to each term is an isomorphism.
The limit ring is the vertex of the arbitrary limit cone
c. The distinguished triangle has the prescribed product difference map for the transitions restricted to that vertex.
public theorem derivedLimit_isPseudoCoherent_and_baseChange_iso
(A : ℕᵒᵖ ⥤ CommRingCat.{u}) (c : Cone A) (hc : IsLimit c)
(Kₙ : ∀ n : ℕ, DerivedCategory (ModuleCat.{max u v} (A.obj (op n))))
(φ : ∀ n : ℕ, Kₙ (n + 1) ⟶
(ModuleCat.restrictScalars (A.map (homOfLE (Nat.le_succ n)).op).hom).mapDerivedCategory.obj
(Kₙ n))
(hSurjective : ∀ n : ℕ,
Function.Surjective (A.map (homOfLE (Nat.le_succ n)).op).hom)
(hLocallyNilpotent : ∀ n : ℕ,
(RingHom.ker (A.map (homOfLE (Nat.le_succ n)).op).hom).IsLocallyNilpotent)
(hPseudoCoherent : (∀ n : ℕ, PseudoCoherence.IsPseudoCoherent (Kₙ n)) ∨
∃ n₀ : ℕ, PseudoCoherence.IsPseudoCoherent (Kₙ n₀) ∧
∀ n : ℕ, n₀ ≤ n →
IsNilpotent (RingHom.ker (A.map (homOfLE (Nat.le_succ n)).op).hom))
(hBaseChange : ∀ n : ℕ,
IsIso (derivedBaseChangeComparison (A.map (homOfLE (Nat.le_succ n)).op).hom (φ n))) :
let X : ℕ → DerivedCategory (ModuleCat.{max u v} c.pt) := fun n ↦
(ModuleCat.restrictScalars (c.π.app (op n)).hom).mapDerivedCategory.obj (Kₙ n)
let t : ∀ n : ℕ, X (n + 1) ⟶ X n := fun n ↦
(ModuleCat.restrictScalars (c.π.app (op (n + 1))).hom).mapDerivedCategory.map
(φ n) ≫
(derivedRestrictScalarsComp (c.π.app (op (n + 1))).hom
(A.map (homOfLE (Nat.le_succ n)).op).hom (c.π.app (op n)).hom
(congrArg CommRingCat.Hom.hom (c.w (homOfLE (Nat.le_succ n)).op)).symm).hom.app (Kₙ n)
∀ [HasProduct X] (K : DerivedCategory (ModuleCat.{max u v} c.pt))
(p : K ⟶ ∏ᶜ X) (δ : ∏ᶜ X ⟶ K⟦(1 : ℤ)⟧),
Pretriangulated.Triangle.mk p
(Pi.lift fun n : ℕ ↦ Pi.π X n - Pi.π X (n + 1) ≫ t n) δ ∈
distTriang (DerivedCategory (ModuleCat.{max u v} c.pt)) →
PseudoCoherence.IsPseudoCoherent K ∧ ∀ n : ℕ,
IsIso (derivedBaseChangeComparison (c.π.app (op n)).hom (p ≫ Pi.π X n))
Tag 09AV, a lemma
Tag 09AV in the Stacks Project.
StacksDraft.DerivedInverseLimit.derivedLimit_isPseudoCoherent_isDerivedComplete_and_baseChange_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Limits/PseudoCoherent/AdicallyComplete.lean, line 257.
Stacks 09AV. Let
AbeI-adically complete and letKₙ nbe a derived object overA ⧸ I ^ (n + 1). SupposeKₙ 0is pseudo-coherent and every transition map becomes an isomorphism after derived base change. Then a derived inverse limitKoverAis pseudo-coherent and derived complete, and its canonical derived base-change map to everyKₙ nis an isomorphism.
public theorem derivedLimit_isPseudoCoherent_isDerivedComplete_and_baseChange_iso
(A : Type u) [CommRing A] (I : Ideal A) [IsAdicComplete I A]
(Kₙ : ∀ n : ℕ, DerivedCategory (ModuleCat.{max u v} (A ⧸ I ^ (n + 1))))
(φ : ∀ n : ℕ, Kₙ (n + 1) ⟶
(ModuleCat.restrictScalars
(Ideal.Quotient.factorPow I (Nat.le_succ (n + 1)))).mapDerivedCategory.obj (Kₙ n))
(hPseudoCoherent : PseudoCoherence.IsPseudoCoherent (Kₙ 0))
(hBaseChange : ∀ n : ℕ, IsIso (derivedBaseChangeComparison
(Ideal.Quotient.factorPow I (Nat.le_succ (n + 1))) (φ n))) :
letI : HasExactLimitsOfShape (Discrete ℕ) (ModuleCat.{max u v} A) :=
moduleCat_hasExactLimitsOfShape_discrete A ℕ
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{max u v} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
let q : ∀ n : ℕ, A ⧸ I ^ (n + 2) →+* A ⧸ I ^ (n + 1) := fun n ↦
Ideal.Quotient.factorPow I (Nat.le_succ (n + 1))
let a : ∀ n : ℕ, A →+* A ⧸ I ^ (n + 1) := fun n ↦
Ideal.Quotient.mk (I ^ (n + 1))
let X : ℕ → DerivedCategory (ModuleCat.{max u v} A) := fun n ↦
(ModuleCat.restrictScalars (a n)).mapDerivedCategory.obj (Kₙ n)
let t : ∀ n : ℕ, X (n + 1) ⟶ X n := fun n ↦
(ModuleCat.restrictScalars (a (n + 1))).mapDerivedCategory.map (φ n) ≫
(derivedRestrictScalarsComp (a (n + 1)) (q n) (a n)
(by ext x; rfl)).hom.app (Kₙ n)
∀ (K : DerivedCategory (ModuleCat.{max u v} A))
(p : K ⟶ ∏ᶜ X) (δ : ∏ᶜ X ⟶ K⟦(1 : ℤ)⟧),
Triangle.mk p (Pi.lift fun n : ℕ ↦ Pi.π X n - Pi.π X (n + 1) ≫ t n) δ ∈
distTriang (DerivedCategory (ModuleCat.{max u v} A)) →
PseudoCoherence.IsPseudoCoherent K ∧ _root_.IsDerivedComplete I K ∧
∀ n : ℕ, IsIso (derivedBaseChangeComparison
(a n) (p ≫ Pi.π X n))
Tag 0CQG, a lemma
Tag 0CQG in the Stacks Project.
StacksDraft.DerivedInverseLimit.derivedLimit_isPerfect_and_baseChange_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Limits/Perfect.lean, line 269.
Suppose a tower of rings has surjective transition maps with locally nilpotent kernels, and its derived module objects are preserved by the base-change maps induced by their transitions. If all terms are perfect, or one term is perfect and every subsequent transition kernel is nilpotent, then every derived inverse limit over the vertex of the limit cone
cis perfect and its canonical base-change map to each term is an isomorphism.
public theorem derivedLimit_isPerfect_and_baseChange_iso
(A : ℕᵒᵖ ⥤ CommRingCat.{u}) (c : Cone A) (hc : IsLimit c)
(Kₙ : ∀ n : ℕ, DerivedCategory (ModuleCat.{max u v} (A.obj (op n))))
(φ : ∀ n : ℕ, Kₙ (n + 1) ⟶
(ModuleCat.restrictScalars (A.map (homOfLE (Nat.le_succ n)).op).hom).mapDerivedCategory.obj
(Kₙ n))
(hSurjective : ∀ n : ℕ,
Function.Surjective (A.map (homOfLE (Nat.le_succ n)).op).hom)
(hLocallyNilpotent : ∀ n : ℕ,
(RingHom.ker (A.map (homOfLE (Nat.le_succ n)).op).hom).IsLocallyNilpotent)
(hPerfect : (∀ n : ℕ, StacksDraft.Perfect.IsPerfect (Kₙ n)) ∨
∃ n₀ : ℕ, StacksDraft.Perfect.IsPerfect (Kₙ n₀) ∧
∀ n : ℕ, n₀ ≤ n →
IsNilpotent (RingHom.ker (A.map (homOfLE (Nat.le_succ n)).op).hom))
(hBaseChange : ∀ n : ℕ,
IsIso (StacksDraft.DerivedInverseLimit.derivedBaseChangeComparison
(A.map (homOfLE (Nat.le_succ n)).op).hom (φ n))) :
let X : ℕ → DerivedCategory (ModuleCat.{max u v} c.pt) := fun n ↦
(ModuleCat.restrictScalars (c.π.app (op n)).hom).mapDerivedCategory.obj (Kₙ n)
let t : ∀ n : ℕ, X (n + 1) ⟶ X n := fun n ↦
(ModuleCat.restrictScalars (c.π.app (op (n + 1))).hom).mapDerivedCategory.map
(φ n) ≫
(StacksDraft.DerivedInverseLimit.derivedRestrictScalarsComp (c.π.app (op (n + 1))).hom
(A.map (homOfLE (Nat.le_succ n)).op).hom (c.π.app (op n)).hom
(congrArg CommRingCat.Hom.hom (c.w (homOfLE (Nat.le_succ n)).op)).symm).hom.app (Kₙ n)
∀ [HasProduct X] (K : DerivedCategory (ModuleCat.{max u v} c.pt))
(p : K ⟶ ∏ᶜ X) (δ : ∏ᶜ X ⟶ K⟦(1 : ℤ)⟧),
Pretriangulated.Triangle.mk p
(Pi.lift fun n : ℕ ↦ Pi.π X n - Pi.π X (n + 1) ≫ t n) δ ∈
distTriang (DerivedCategory (ModuleCat.{max u v} c.pt)) →
StacksDraft.Perfect.IsPerfect K ∧ ∀ n : ℕ,
IsIso (StacksDraft.DerivedInverseLimit.derivedBaseChangeComparison
(c.π.app (op n)).hom (p ≫ Pi.π X n))
Tag 09AW, a lemma
Tag 09AW in the Stacks Project.
StacksDraft.DerivedInverseLimit.derivedLimit_isPerfect_isDerivedComplete_and_baseChange_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Limits/Perfect.lean, line 339.
Let
AbeI-adically complete and letKₙ nbe a derived object overA ⧸ I ^ (n + 1). SupposeKₙ 0is perfect and every transition map becomes an isomorphism after derived base change. Then a derived inverse limitKoverAis perfect and derived complete, and its canonical derived base-change map to everyKₙ nis an isomorphism.
public theorem derivedLimit_isPerfect_isDerivedComplete_and_baseChange_iso
(A : Type u) [CommRing A] (I : Ideal A) [IsAdicComplete I A]
(Kₙ : ∀ n : ℕ, DerivedCategory (ModuleCat.{max u v} (A ⧸ I ^ (n + 1))))
(φ : ∀ n : ℕ, Kₙ (n + 1) ⟶
(ModuleCat.restrictScalars
(Ideal.Quotient.factorPow I (Nat.le_succ (n + 1)))).mapDerivedCategory.obj (Kₙ n))
(hPerfect : StacksDraft.Perfect.IsPerfect (Kₙ 0))
(hBaseChange : ∀ n : ℕ, IsIso (StacksDraft.DerivedInverseLimit.derivedBaseChangeComparison
(Ideal.Quotient.factorPow I (Nat.le_succ (n + 1))) (φ n))) :
letI : HasExactLimitsOfShape (Discrete ℕ) (ModuleCat.{max u v} A) :=
moduleCat_hasExactLimitsOfShape_discrete.{max u v} A ℕ
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{max u v} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
let q : ∀ n : ℕ, A ⧸ I ^ (n + 2) →+* A ⧸ I ^ (n + 1) := fun n ↦
Ideal.Quotient.factorPow I (Nat.le_succ (n + 1))
let a : ∀ n : ℕ, A →+* A ⧸ I ^ (n + 1) := fun n ↦
Ideal.Quotient.mk (I ^ (n + 1))
let X : ℕ → DerivedCategory (ModuleCat.{max u v} A) := fun n ↦
(ModuleCat.restrictScalars (a n)).mapDerivedCategory.obj (Kₙ n)
let t : ∀ n : ℕ, X (n + 1) ⟶ X n := fun n ↦
(ModuleCat.restrictScalars (a (n + 1))).mapDerivedCategory.map (φ n) ≫
(StacksDraft.DerivedInverseLimit.derivedRestrictScalarsComp (a (n + 1)) (q n) (a n)
(by ext x; rfl)).hom.app (Kₙ n)
∀ (K : DerivedCategory (ModuleCat.{max u v} A))
(p : K ⟶ ∏ᶜ X) (δ : ∏ᶜ X ⟶ K⟦(1 : ℤ)⟧),
Triangle.mk p (Pi.lift fun n : ℕ ↦ Pi.π X n - Pi.π X (n + 1) ≫ t n) δ ∈
distTriang (DerivedCategory (ModuleCat.{max u v} A)) →
StacksDraft.Perfect.IsPerfect K ∧ _root_.IsDerivedComplete I K ∧
∀ n : ℕ, IsIso (StacksDraft.DerivedInverseLimit.derivedBaseChangeComparison
(a n) (p ≫ Pi.π X n))
Tag 09AU, a lemma
Tag 09AU in the Stacks Project.
Stacks.DerivedLimit.AdicSystem.isDerivedComplete_and_reduction_isIso_of_isDerivedLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Limits/AdicSystem.lean, line 1345.
Stacks 09AU. Let
Abe Noetherian andIan ideal. Suppose thatFis an inverse system inD(A)whosen-th member is the restriction of an objectKq nofD(A ⧸ I ^ (n + 1)). IfKq 0is bounded above and every transition induces an isomorphism after derived reduction to the preceding quotient, then a derived limitKis bounded above and derivedI-complete. Moreover, the canonical map from the derived reduction ofKtoKq nis an isomorphism for everyn.
public theorem isDerivedComplete_and_reduction_isIso_of_isDerivedLimit
{A : Type u} [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(F : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{max u v} A))
(Kq : ∀ n : ℕ, DerivedCategory (ModuleCat.{max u v} (A ⧸ I ^ (n + 1))))
(e : ∀ n : ℕ, F.obj (.op n) ≅
(ModuleCat.restrictScalars.{max u v} (Ideal.Quotient.mk (I ^ (n + 1)))).mapDerivedCategory.obj
(Kq n))
(adj : ∀ n : ℕ,
(CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars.{u, u, v}
(Ideal.Quotient.mk (I ^ (n + 1)))).functor ⊣
(ModuleCat.restrictScalars.{max u v}
(Ideal.Quotient.mk (I ^ (n + 1)))).mapDerivedCategory)
(hbounded : DerivedCategory.TStructure.t.minus (Kq 0))
(t : ∀ n : ℕ, Kq (n + 1) ⟶
(ModuleCat.restrictScalars.{max u v} (quotientTransition I n)).mapDerivedCategory.obj (Kq n))
(htransition : ∀ n : ℕ,
F.map (homOfLE (Nat.le_succ n)).op ≫ (e n).hom =
(e (n + 1)).hom ≫
(ModuleCat.restrictScalars.{max u v}
(Ideal.Quotient.mk (I ^ (n + 2)))).mapDerivedCategory.map
(t n) ≫ (restrictScalarsTransitionIso I n).hom.app (Kq n))
(hcompat : ∀ n : ℕ,
IsIso (StacksDraft.DerivedInverseLimit.derivedBaseChangeComparison.{u, v, u}
(quotientTransition I n) (t n))) :
letI : HasProductsOfShape ℕ (DerivedCategory (ModuleCat.{max u v} A)) :=
Stacks.DerivedProducts.hasProductsOfShape_derivedCategory
∀ (K : DerivedCategory (ModuleCat.{max u v} A))
(p : K ⟶ ∏ᶜ fun n : ℕ => F.obj (.op n))
(δ : (∏ᶜ fun n : ℕ => F.obj (.op n)) ⟶ K⟦(1 : ℤ)⟧),
Triangle.mk p
(Pi.lift fun n : ℕ => Pi.π (fun n : ℕ => F.obj (.op n)) n -
Pi.π (fun n : ℕ => F.obj (.op n)) (n + 1) ≫
F.map (homOfLE (Nat.le_succ n)).op) δ ∈
distTriang (DerivedCategory (ModuleCat.{max u v} A)) →
DerivedCategory.TStructure.t.minus K ∧
_root_.IsDerivedComplete I K ∧
∀ n : ℕ, IsIso (((adj n).homEquiv _ _).symm
(p ≫ Pi.π (fun n : ℕ => F.obj (.op n)) n ≫ (e n).hom))
Tag 0EGS, a lemma
Tag 0EGS in the Stacks Project.
Stacks.InverseSystem.AdicCompletionCohomology.adicCompletion_homology_iso_limit_derivedReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/Limits/AdicSystem.lean, line 207.
Stacks 0EGS (Kollár--Kovács). Let
Ibe an ideal of a Noetherian ringAandK ∈ D(A). Suppose that every cohomology module ofKis finite and, in every degree, the cohomology inverse system ofK ⊗ᴸ[A] A/Iⁿis Mittag--Leffler. Then the inverse limit ofHⁱ(K ⊗ᴸ[A] A/Iⁿ)is isomorphic to theI-adic completion ofHⁱ(K)for everyi.
public theorem adicCompletion_homology_iso_limit_derivedReduction
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(K : DerivedCategory (ModuleCat.{u} A))
(T : CochainComplex.DerivedTensor.DerivedTensorProduct A)
(hK : ∀ i : ℤ,
Module.Finite A ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj K))
(hML : ∀ i : ℤ,
(((NoetherianAdicCompletion.idealPowerQuotientSystem I ⋙ T.tensor.obj K) ⋙
DerivedCategory.homologyFunctor (ModuleCat.{u} A) i) ⋙
forget (ModuleCat.{u} A)).IsMittagLeffler) :
∀ i : ℤ,
Nonempty
(ModuleCat.of A
(AdicCompletion I
((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj K)) ≅
limit ((NoetherianAdicCompletion.idealPowerQuotientSystem I ⋙ T.tensor.obj K) ⋙
DerivedCategory.homologyFunctor (ModuleCat.{u} A) i))
Sources
Section15.100 Some evaluation maps#
Section 15.100 of the Stacks Project, Tag 0ATJ. 4 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0A68, a lemma
Tag 0A68 in the Stacks Project.
StacksDraft.DerivedHom.evaluationToIteratedDerivedHom_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/Evaluation/Iterated.lean, line 184.
Stacks 0A68. The canonical evaluation morphism
RHom_R(L, M) ⊗ᴸ_R K ⟶ RHom_R(RHom_R(K, L), M)is an isomorphism ifKis perfect, or ifKis pseudo-coherent,Lis cohomologically bounded below, andMhas finite injective dimension.
public theorem evaluationToIteratedDerivedHom_isIso
(K L M : DerivedCategory (ModuleCat R))
(h : StacksDraft.Perfect.IsPerfect K ∨
(StacksDraft.PseudoCoherence.IsPseudoCoherent K ∧
DerivedCategoryB.IsBoundedBelow L ∧
StacksDraft.InjectiveDimension.HasFiniteInjectiveDimension M)) :
let e := Classical.choose
(exists_evaluationToIteratedDerivedHom (R := R))
IsIso (e K L M)
Tag 0A69, a lemma
Tag 0A69 in the Stacks Project.
StacksDraft.DerivedHom.evaluationToIteratedDerivedHom_isIso_of_truncLE_pseudoCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/Evaluation/Iterated.lean, line 583.
Stacks 0A69. The canonical evaluation morphism
RHom_R(L, M) ⊗ᴸ_R K ⟶ RHom_R(RHom_R(K, L), M)is an isomorphism ifLandMhave finite injective dimension,RHom_R(L, M)has finite Tor dimension, and every truncationτ_{≤ n} Kis pseudo-coherent.
public theorem evaluationToIteratedDerivedHom_isIso_of_truncLE_pseudoCoherent
(K L M : DerivedCategory (ModuleCat R))
(hL : StacksDraft.InjectiveDimension.HasFiniteInjectiveDimension L)
(hM : StacksDraft.InjectiveDimension.HasFiniteInjectiveDimension M)
(hTor :
let D := derivedHomAdjunction (R := R)
∃ a b : ℤ, ∀ (N : ModuleCat R) (i : ℤ), i ∉ Set.Icc a b →
Limits.IsZero ((DerivedCategory.homologyFunctor (ModuleCat R) i).obj
(D.tensor.obj
(D.hom.obj (Opposite.op L, M),
(DerivedCategory.singleFunctor (ModuleCat R) 0).obj N))))
(hK : ∀ n : ℤ, StacksDraft.PseudoCoherence.IsPseudoCoherent
((DerivedCategory.TStructure.t.truncLE n).obj K)) :
let e := Classical.choose
(exists_evaluationToIteratedDerivedHom (R := R))
IsIso (e K L M)
Tag 0ATK, a lemma
Tag 0ATK in the Stacks Project.
Stacks.DerivedTensorHomDiagonal.isIso_derivedTensorHomDiagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/Evaluation/TensorHom/PerfectAndCurrying.lean, line 306. References: SGA 6 I (7.6), “affine case, E perfect”.
Stacks 0ATK. The canonical derived tensor--Hom diagonal
K ⊗ᴸ RHom(M, L) ⟶ RHom(M, K ⊗ᴸ L)is an isomorphism ifMis perfect, ifKis perfect, or ifMis pseudo-coherent,Lis bounded below andKhas Tor amplitude in[a, ∞].
public theorem isIso_derivedTensorHomDiagonal
{R : Type u} [CommRing R]
(K L M : DerivedCategory (ModuleCat.{u} R)) (a : ℤ)
(h : StacksDraft.Perfect.IsPerfect M ∨ StacksDraft.Perfect.IsPerfect K ∨
(StacksDraft.PseudoCoherence.IsPseudoCoherent M ∧
(∃ b : ℤ, DerivedCategory.IsGE L b) ∧
∀ (N : ModuleCat.{u} R) (i : ℤ), i < a →
IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) i).obj
((((CochainComplex.DerivedTensor.canonicalDerivedTensorProduct R).tensor.obj K).obj
((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj N)))))) :
IsIso (StacksDraft.DerivedHom.derivedTensorHomDiagonal K L M)
Tag 0BYQ, a lemma
Tag 0BYQ in the Stacks Project.
Stacks.DerivedHom.KFlatHomComplex.homComplex_kFlat_and_represents_RHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/Evaluation/KFlat.lean, line 395.
Stacks 0BYQ. Let
Pbe a bounded above cochain complex of projectiveR-modules which is perfect as an object of the derived categoryD(R), and letKbe a K-flat complex ofR-modules. ThenHom^•(P, K)is K-flat, and it representsRHom_R(P, K): for everyn, the map sending a degree-ncohomology class ofHom^•(P, K)to the corresponding morphismP ⟶ K⟦n⟧inD(R)is bijective.
theorem homComplex_kFlat_and_represents_RHom [HasDerivedCategory.{w} (ModuleCat.{u} R)]
(P K : CochainComplex (ModuleCat.{u} R) ℤ) (d : ℤ) [P.IsStrictlyLE d]
[∀ i, Module.Projective R (P.X i)]
(hP : StacksDraft.Perfect.IsPerfect (DerivedCategory.Q.obj P)) (hK : K.KFlat) :
(HomComplexR R P K).KFlat ∧
∀ n : ℤ, Function.Bijective
(fun (c : CohomologyClass P K n) =>
DerivedCategory.Qh.map (CohomologyClass.homAddEquiv c))
Sources
Section15.101 Base change for derived hom#
Section 15.101 of the Stacks Project, Tag 0E1V. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0E1V, the section
Tag 0E1V in the Stacks Project.
Stacks.DerivedHom.ExtensionOfScalars.derivedHomBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/RHom/BaseChange/BaseChangeMap.lean, line 247. The attribute's comment: “the derived base-change map for derived hom”.
Stacks 0E1X. The canonical derived-module base-change map
RHom_R(K, M) ⊗ᴸ_R A ⟶ RHom_A(K ⊗ᴸ_R A, M ⊗ᴸ_R A). It is the mate of the unit-induced map under the adjunction of Stacks 0GMT, using exactly the change-of-rings identification of Stacks 0E1W.
public def derivedHomBaseChange
{R : Type uR} {A : Type uA} [CommRing R] [CommRing A] (f : R →+* A) :
letI : (ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).IsLeftAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsRightAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isRightAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsLeftAdjoint :=
(ModuleCat.restrictCoextendScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
∀ (F : DerivedCategory (ModuleCat.{max uR uA uM} R) ⥤
DerivedCategory (ModuleCat.{max uR uA uM} A))
(comparison : DerivedCategory.Q ⋙ F ⟶
(ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
[F.IsLeftDerivedFunctor comparison
(HomologicalComplex.quasiIso (ModuleCat.{max uR uA uM} R) (ComplexShape.up ℤ))]
(K M : DerivedCategory (ModuleCat.{max uR uA uM} R)),
F.obj ((_root_.Stacks.DerivedHom.ScalarTransportedInternalHom.hom.{uR, max uR uA uM} R).obj
(Opposite.op K, M)) ⟶
(_root_.Stacks.DerivedHom.ScalarTransportedInternalHom.hom.{uA, max uR uA uM} A).obj
(Opposite.op (F.obj K), F.obj M)
Stacks.DerivedHom.BaseChangeIso.isIso_derivedHomBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/RHom/BaseChange/Invertibility.lean, line 617. The attribute's comment: “invertibility of the base-change map in each of the four cases”.
Stacks 0A6A. The canonical derived-Hom base-change morphism
RHom_R(K, M) ⊗ᴸ_R A ⟶ RHom_A(K ⊗ᴸ_R A, M ⊗ᴸ_R A)of Stacks 0E1X is an isomorphism in each of four cases:Kis perfect;Ais perfect as anR-module; the ring map is flat,Kis pseudo-coherent andMis bounded below; orAhas finite Tor dimension overR,Kis pseudo-coherent andMis bounded below.
public theorem isIso_derivedHomBaseChange
{R : Type uR} {A : Type uA} [CommRing R] [CommRing A] (f : R →+* A) :
letI : (ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).IsLeftAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsRightAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isRightAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsLeftAdjoint :=
(ModuleCat.restrictCoextendScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
∀ (F : Functor (DerivedCategory (ModuleCat.{max uR uA uM} R))
(DerivedCategory (ModuleCat.{max uR uA uM} A)))
(comparison : DerivedCategory.Q ⋙ F ⟶
(ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
[F.IsLeftDerivedFunctor comparison
(HomologicalComplex.quasiIso (ModuleCat.{max uR uA uM} R) (ComplexShape.up ℤ))]
(K M : DerivedCategory (ModuleCat.{max uR uA uM} R))
(h : StacksDraft.Perfect.IsPerfect K ∨
StacksDraft.Perfect.IsPerfect
((DerivedCategory.singleFunctor (ModuleCat.{max uR uA uM} R) 0).obj
((ModuleCat.restrictScalars f).obj (ModuleCat.of A (ULift.{max uR uM} A)))) ∨
(f.Flat ∧ StacksDraft.PseudoCoherence.IsPseudoCoherent K ∧
∃ b : ℤ, DerivedCategory.IsGE M b) ∨
((let e := moduleUniverseEquiv.{uR, max uA uM} R
letI : e.functor.Additive :=
inferInstanceAs (ModuleCat.restrictScalars.{max uR uA uM, max uR uA uM, uR}
(ULift.ringEquiv : ULift.{max uA uM} R ≃+* R).toRingHom).Additive
∃ a : ℤ, ∀ (N : ModuleCat.{max uR uA uM} R) (i : ℤ), i < a →
IsZero ((DerivedCategory.homologyFunctor
(ModuleCat.{max uR uA uM} (ULift.{max uA uM} R)) i).obj
((canonTensorMod
(e.functor.obj N)).obj
(e.functor.mapDerivedCategory.obj
((DerivedCategory.singleFunctor (ModuleCat.{max uR uA uM} R) 0).obj
((ModuleCat.restrictScalars f).obj
(ModuleCat.of A (ULift.{max uR uM} A)))))))) ∧
StacksDraft.PseudoCoherence.IsPseudoCoherent K ∧
∃ b : ℤ, DerivedCategory.IsGE M b)),
IsIso (Stacks.DerivedHom.ExtensionOfScalars.derivedHomBaseChange.{uR, uA, uM} f F comparison K
M)
Stacks.DerivedHom.BaseChange.derivedHomRestrictScalarsNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/RHom/BaseChange/ModelRestrictScalars.lean, line 736. The attribute's comment: “the change-of-rings isomorphism for derived hom”.
Stacks 0E1W. The canonical change-of-rings isomorphism for derived Hom, natural in the object of
D(R)in the contravariant variable and the object ofD(A)in the covariant variable. Its right-hand side uses any total left-derived extension-of-scalars functor; such a functor is left adjoint to derived restriction of scalars by Stacks 0GMT.
public noncomputable def derivedHomRestrictScalarsNatIso
{R : Type uR} {A : Type uA} [CommRing R] [CommRing A] (f : R →+* A) :
letI : (ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).IsLeftAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsRightAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isRightAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsLeftAdjoint :=
(ModuleCat.restrictCoextendScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
∀ (F : DerivedCategory (ModuleCat.{max uR uA uM} R) ⥤
DerivedCategory (ModuleCat.{max uR uA uM} A))
(comparison : DerivedCategory.Q ⋙ F ⟶
(ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
[F.IsLeftDerivedFunctor comparison
(HomologicalComplex.quasiIso (ModuleCat.{max uR uA uM} R) (ComplexShape.up ℤ))],
Functor.prod
(Functor.id (DerivedCategory (ModuleCat.{max uR uA uM} R))ᵒᵖ)
(ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).mapDerivedCategory ⋙
_root_.Stacks.DerivedHom.ScalarTransportedInternalHom.hom.{uR, max uR uA uM} R ≅
Functor.prod F.op (Functor.id (DerivedCategory (ModuleCat.{max uR uA uM} A))) ⋙
_root_.Stacks.DerivedHom.ScalarTransportedInternalHom.hom.{uA, max uR uA uM} A ⋙
(ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).mapDerivedCategory
Tag 0E1W, a lemma
Tag 0E1W in the Stacks Project.
Stacks.DerivedHom.BaseChange.derivedHomRestrictScalarsNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/RHom/BaseChange/ModelRestrictScalars.lean, line 736.
Stacks 0E1W. The canonical change-of-rings isomorphism for derived Hom, natural in the object of
D(R)in the contravariant variable and the object ofD(A)in the covariant variable. Its right-hand side uses any total left-derived extension-of-scalars functor; such a functor is left adjoint to derived restriction of scalars by Stacks 0GMT.
public noncomputable def derivedHomRestrictScalarsNatIso
{R : Type uR} {A : Type uA} [CommRing R] [CommRing A] (f : R →+* A) :
letI : (ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).IsLeftAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsRightAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isRightAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsLeftAdjoint :=
(ModuleCat.restrictCoextendScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
∀ (F : DerivedCategory (ModuleCat.{max uR uA uM} R) ⥤
DerivedCategory (ModuleCat.{max uR uA uM} A))
(comparison : DerivedCategory.Q ⋙ F ⟶
(ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
[F.IsLeftDerivedFunctor comparison
(HomologicalComplex.quasiIso (ModuleCat.{max uR uA uM} R) (ComplexShape.up ℤ))],
Functor.prod
(Functor.id (DerivedCategory (ModuleCat.{max uR uA uM} R))ᵒᵖ)
(ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).mapDerivedCategory ⋙
_root_.Stacks.DerivedHom.ScalarTransportedInternalHom.hom.{uR, max uR uA uM} R ≅
Functor.prod F.op (Functor.id (DerivedCategory (ModuleCat.{max uR uA uM} A))) ⋙
_root_.Stacks.DerivedHom.ScalarTransportedInternalHom.hom.{uA, max uR uA uM} A ⋙
(ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).mapDerivedCategory
Tag 0E1X, an equation
Tag 0E1X in the Stacks Project.
Stacks.DerivedHom.ExtensionOfScalars.derivedHomBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/RHom/BaseChange/BaseChangeMap.lean, line 247.
Stacks 0E1X. The canonical derived-module base-change map
RHom_R(K, M) ⊗ᴸ_R A ⟶ RHom_A(K ⊗ᴸ_R A, M ⊗ᴸ_R A). It is the mate of the unit-induced map under the adjunction of Stacks 0GMT, using exactly the change-of-rings identification of Stacks 0E1W.
public def derivedHomBaseChange
{R : Type uR} {A : Type uA} [CommRing R] [CommRing A] (f : R →+* A) :
letI : (ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).IsLeftAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsRightAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isRightAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsLeftAdjoint :=
(ModuleCat.restrictCoextendScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
∀ (F : DerivedCategory (ModuleCat.{max uR uA uM} R) ⥤
DerivedCategory (ModuleCat.{max uR uA uM} A))
(comparison : DerivedCategory.Q ⋙ F ⟶
(ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
[F.IsLeftDerivedFunctor comparison
(HomologicalComplex.quasiIso (ModuleCat.{max uR uA uM} R) (ComplexShape.up ℤ))]
(K M : DerivedCategory (ModuleCat.{max uR uA uM} R)),
F.obj ((_root_.Stacks.DerivedHom.ScalarTransportedInternalHom.hom.{uR, max uR uA uM} R).obj
(Opposite.op K, M)) ⟶
(_root_.Stacks.DerivedHom.ScalarTransportedInternalHom.hom.{uA, max uR uA uM} A).obj
(Opposite.op (F.obj K), F.obj M)
Tag 0A6A, a lemma
Tag 0A6A in the Stacks Project.
Stacks.DerivedHom.BaseChangeIso.isIso_derivedHomBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/HomComplex/RHom/BaseChange/Invertibility.lean, line 617.
Stacks 0A6A. The canonical derived-Hom base-change morphism
RHom_R(K, M) ⊗ᴸ_R A ⟶ RHom_A(K ⊗ᴸ_R A, M ⊗ᴸ_R A)of Stacks 0E1X is an isomorphism in each of four cases:Kis perfect;Ais perfect as anR-module; the ring map is flat,Kis pseudo-coherent andMis bounded below; orAhas finite Tor dimension overR,Kis pseudo-coherent andMis bounded below.
public theorem isIso_derivedHomBaseChange
{R : Type uR} {A : Type uA} [CommRing R] [CommRing A] (f : R →+* A) :
letI : (ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).IsLeftAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsRightAdjoint :=
(ModuleCat.extendRestrictScalarsAdj.{max uR uM, uR, uA} f).isRightAdjoint
letI : (ModuleCat.restrictScalars.{max uR uA uM, uR, uA} f).IsLeftAdjoint :=
(ModuleCat.restrictCoextendScalarsAdj.{max uR uM, uR, uA} f).isLeftAdjoint
∀ (F : Functor (DerivedCategory (ModuleCat.{max uR uA uM} R))
(DerivedCategory (ModuleCat.{max uR uA uM} A)))
(comparison : DerivedCategory.Q ⋙ F ⟶
(ModuleCat.extendScalars.{uR, uA, max uR uA uM} f).mapHomologicalComplex
(ComplexShape.up ℤ) ⋙ DerivedCategory.Q)
[F.IsLeftDerivedFunctor comparison
(HomologicalComplex.quasiIso (ModuleCat.{max uR uA uM} R) (ComplexShape.up ℤ))]
(K M : DerivedCategory (ModuleCat.{max uR uA uM} R))
(h : StacksDraft.Perfect.IsPerfect K ∨
StacksDraft.Perfect.IsPerfect
((DerivedCategory.singleFunctor (ModuleCat.{max uR uA uM} R) 0).obj
((ModuleCat.restrictScalars f).obj (ModuleCat.of A (ULift.{max uR uM} A)))) ∨
(f.Flat ∧ StacksDraft.PseudoCoherence.IsPseudoCoherent K ∧
∃ b : ℤ, DerivedCategory.IsGE M b) ∨
((let e := moduleUniverseEquiv.{uR, max uA uM} R
letI : e.functor.Additive :=
inferInstanceAs (ModuleCat.restrictScalars.{max uR uA uM, max uR uA uM, uR}
(ULift.ringEquiv : ULift.{max uA uM} R ≃+* R).toRingHom).Additive
∃ a : ℤ, ∀ (N : ModuleCat.{max uR uA uM} R) (i : ℤ), i < a →
IsZero ((DerivedCategory.homologyFunctor
(ModuleCat.{max uR uA uM} (ULift.{max uA uM} R)) i).obj
((canonTensorMod
(e.functor.obj N)).obj
(e.functor.mapDerivedCategory.obj
((DerivedCategory.singleFunctor (ModuleCat.{max uR uA uM} R) 0).obj
((ModuleCat.restrictScalars f).obj
(ModuleCat.of A (ULift.{max uR uM} A)))))))) ∧
StacksDraft.PseudoCoherence.IsPseudoCoherent K ∧
∃ b : ℤ, DerivedCategory.IsGE M b)),
IsIso (Stacks.DerivedHom.ExtensionOfScalars.derivedHomBaseChange.{uR, uA, uM} f F comparison K
M)
Sources
Section15.102 Systems of modules#
Section 15.102 of the Stacks Project, Tag 0EGT. 11 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0EGU, a lemma
Tag 0EGU in the Stacks Project.
Stacks.AdicSystem.ArtinReesHomology.exists_uniform_adic_homology_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Homology/QuotientComparison.lean, line 152.
Stacks 0EGU. For a complex of finite modules over a Noetherian ring, homology after reduction modulo
I ^ nand the quotients byI ^ nof the original homology are canonically pro-isomorphic. A single positive shift controls the inverse-system images, the comparison on ideal multiples, and the kernels and cokernels of all comparison maps.
theorem exists_uniform_adic_homology_comparison
{A K L M : Type*} [CommRing A]
[AddCommGroup K] [Module A K] [Module.Finite A K]
[AddCommGroup L] [Module A L] [Module.Finite A L]
[AddCommGroup M] [Module A M] [Module.Finite A M]
[IsNoetherianRing A]
(I : Ideal A) (α : K →ₗ[A] L) (β : L →ₗ[A] M) (hcomplex : β.comp α = 0) :
let H := (LinearMap.ker β) ⧸
(LinearMap.range α).comap (LinearMap.ker β).subtype
let cycles : ℕ → Submodule A L := fun n =>
(I ^ n • (⊤ : Submodule A M)).comap β
let boundaries : ℕ → Submodule A L := fun n =>
LinearMap.range α ⊔ I ^ n • (⊤ : Submodule A L)
let Hn : ℕ → Type _ := fun n =>
cycles n ⧸ (boundaries n).comap (cycles n).subtype
∃ (toLevel : ∀ n, H →ₗ[A] Hn n)
(transition : ∀ n, Hn (n + 1) →ₗ[A] Hn n)
(quotTransition : ∀ n,
(H ⧸ I ^ (n + 1) • (⊤ : Submodule A H)) →ₗ[A]
(H ⧸ I ^ n • (⊤ : Submodule A H)))
(fromQuotient : ∀ n,
(H ⧸ I ^ n • (⊤ : Submodule A H)) →ₗ[A] Hn n),
(∀ n (x : LinearMap.ker β) (y : cycles n), (y : L) = x →
toLevel n (Submodule.Quotient.mk x) = Submodule.Quotient.mk y) ∧
(∀ n (x : cycles (n + 1)) (y : cycles n), (y : L) = x →
transition n (Submodule.Quotient.mk x) = Submodule.Quotient.mk y) ∧
(∀ n (x : H),
quotTransition n (Submodule.Quotient.mk x) = Submodule.Quotient.mk x) ∧
(∀ n, transition n ∘ₗ toLevel (n + 1) = toLevel n) ∧
(∀ n, fromQuotient n ∘ₗ (I ^ n • (⊤ : Submodule A H)).mkQ = toLevel n) ∧
let Hsys : ℕᵒᵖ ⥤ ModuleCat A :=
Functor.ofOpSequence (X := fun n => ModuleCat.of A (Hn n))
(fun n => ModuleCat.ofHom (transition n))
let Qsys : ℕᵒᵖ ⥤ ModuleCat A :=
Functor.ofOpSequence
(X := fun n => ModuleCat.of A (H ⧸ I ^ n • (⊤ : Submodule A H)))
(fun n => ModuleCat.ofHom (quotTransition n))
∃ c : ℕ, 0 < c ∧
(∃ back : ∀ n, c ≤ n → Hn n →ₗ[A]
(H ⧸ I ^ (n - c) • (⊤ : Submodule A H)),
(∀ n (hn : c ≤ n),
(back n hn).comp (fromQuotient n) =
(tr Qsys (Nat.sub_le n c)).hom) ∧
(∀ n (hn : c ≤ n),
(fromQuotient (n - c)).comp (back n hn) =
(tr Hsys (Nat.sub_le n c)).hom) ∧
Nonempty (ProIso Hsys Qsys) ∧
Nonempty (limit Hsys ≅ limit Qsys) ∧
(Hsys ⋙ forget (ModuleCat A)).IsMittagLeffler ∧
(∀ n, LinearMap.range (tr Hsys (Nat.le_add_right n c)).hom =
LinearMap.range (toLevel n)) ∧
(∃ toLevelQuotient : ∀ n k,
(H ⧸ I ^ k • (⊤ : Submodule A H)) →ₗ[A]
(Hn n ⧸ I ^ k • (⊤ : Submodule A (Hn n))),
(∀ n k, (toLevelQuotient n k).comp
(I ^ k • (⊤ : Submodule A H)).mkQ =
(I ^ k • (⊤ : Submodule A (Hn n))).mkQ.comp (toLevel n)) ∧
(∀ n (hn : c ≤ n) (x : Hn n),
x ∈ I ^ c • (⊤ : Submodule A (Hn n)) →
toLevelQuotient n (n - c) (back n hn x) =
(I ^ (n - c) • (⊤ : Submodule A (Hn n))).mkQ x)) ∧
(∀ n,
I ^ c ≤ Module.annihilator A (LinearMap.ker (fromQuotient n)) ∧
I ^ c ≤ Module.annihilator A
(Hn n ⧸ LinearMap.range (fromQuotient n))))
Tag 0EGV, a lemma
Tag 0EGV in the Stacks Project.
Stacks.PseudoCoherent.AdicCompletion.pseudoCoherent_mittagLeffler_and_adicCompletion_iso_limit_derivedReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/PseudoCoherentHomology.lean, line 377.
Stacks 0EGV (Kollár--Kovács). If
Kis a pseudo-coherent object ofD(A)for a Noetherian ringA, then in every degree the cohomology of its reductions modulo the positive powers ofIis Mittag--Leffler, and its inverse limit is theI-adic completion of the cohomology ofK.
theorem pseudoCoherent_mittagLeffler_and_adicCompletion_iso_limit_derivedReduction
(A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
(K : DerivedCategory (ModuleCat.{u} A))
(T : CochainComplex.DerivedTensor.DerivedTensorProduct A)
(hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K) :
∀ i : ℤ,
(((NoetherianAdicCompletion.idealPowerQuotientSystem I ⋙ T.tensor.obj K) ⋙
DerivedCategory.homologyFunctor (ModuleCat.{u} A) i) ⋙
forget (ModuleCat.{u} A)).IsMittagLeffler ∧
Nonempty
(ModuleCat.of A
(AdicCompletion I
((DerivedCategory.homologyFunctor (ModuleCat.{u} A) i).obj K)) ≅
limit ((NoetherianAdicCompletion.idealPowerQuotientSystem I ⋙ T.tensor.obj K) ⋙
DerivedCategory.homologyFunctor (ModuleCat.{u} A) i))
Tag 0G9M, a lemma
Tag 0G9M in the Stacks Project.
Stacks.AdicSystem.DerivedReductionProIso.derivedReduction_proIsomorphic_adicReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/IdealPowerTensor.lean, line 2873.
Stacks Project, Tag 0G9M. Let
Ibe an ideal of a Noetherian ringAand letMbe a bounded complex of finiteA-modules. ThenMadmits a bounded-above resolutionp : P -> Mby finite free modules, and the canonical comparison from the derived reductions ofPmodulo the positive powers ofIto the degreewise reductions ofMis compatible with the transition maps and is an isomorphism of pro-objects in the derived category: each level acquires a two-sided inverse after passing to a later level.
public theorem derivedReduction_proIsomorphic_adicReduction
{A : Type u} [CommRing A] [IsNoetherianRing A]
(I : Ideal A) (M : CochainComplex (ModuleCat.{u} A) ℤ)
(hMbounded : ∃ a b : ℤ, M.IsStrictlyGE a ∧ M.IsStrictlyLE b)
(hMfinite : ∀ i : ℤ, Module.Finite A (M.X i)) :
∃ (P : CochainComplex (ModuleCat.{u} A) ℤ) (p : P ⟶ M),
(∃ b : ℤ, P.IsStrictlyLE b) ∧
(∀ i : ℤ, Module.Finite A (P.X i) ∧ Module.Free A (P.X i)) ∧
IsIso (DerivedCategory.Q.map p) ∧
(∀ n : ℕ,
adicReductionTransition I P (Nat.le_succ n) ≫ adicReductionComparison I p n =
adicReductionComparison I p (n + 1) ≫
adicReductionTransition I M (Nat.le_succ n)) ∧
∀ n : ℕ, ∃ (m : ℕ) (h : n ≤ m)
(s : DerivedCategory.Q.obj ((reduceComplex (I ^ (m + 1))).obj M) ⟶
DerivedCategory.Q.obj ((reduceComplex (I ^ (n + 1))).obj P)),
adicReductionComparison I p m ≫ s =
adicReductionTransition I P h ∧
s ≫ adicReductionComparison I p n =
adicReductionTransition I M h
Tag 09BB, a lemma
Tag 09BB in the Stacks Project.
Stacks.AdicSystem.HomComparison.hom_isom_quotient_systems_mittagLeffler_and_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Hom/MittagLeffler.lean, line 588. References: EGA 0 (7.3.4), “Hom^ ≅ Hom(M^,N^)”; EGA 0 (7.8.2), “canonical isomorphism”.
Stacks 09BB. Homomorphisms and isomorphisms between the adic quotients of two finite modules form Mittag--Leffler systems. The canonical comparison from the adic quotients of
Homhas uniformly bounded kernel and cokernel, and passage to the inverse limit identifies both homomorphisms and isomorphisms with those between the completed modules.
public theorem hom_isom_quotient_systems_mittagLeffler_and_completion
{A : Type u} {M : Type v} {N : Type w} [CommRing A] [IsNoetherianRing A]
[AddCommGroup M] [Module A M] [Module.Finite A M]
[AddCommGroup N] [Module A N] [Module.Finite A N]
(I : Ideal A) :
let Mq : ℕ → Type _ := fun n => M ⧸ I ^ n • (⊤ : Submodule A M)
let Nq : ℕ → Type _ := fun n => N ⧸ I ^ n • (⊤ : Submodule A N)
let H : ℕ → Type _ := fun n => Mq n →ₗ[A] Nq n
let E : ℕ → Type _ := fun n => Mq n ≃ₗ[A] Nq n
∃ (homTransition : ∀ n, H (n + 1) →ₗ[A] H n)
(isoTransition : ∀ n, E (n + 1) → E n)
(comparison : ∀ n,
((M →ₗ[A] N) ⧸ I ^ n • (⊤ : Submodule A (M →ₗ[A] N))) →ₗ[A] H n),
(∀ n (f : H (n + 1)) (m : M),
homTransition n f (Submodule.Quotient.mk m) =
AdicCompletion.transitionMap I N (Nat.le_succ n)
(f (Submodule.Quotient.mk m))) ∧
(∀ n (e : E (n + 1)) (m : M),
isoTransition n e (Submodule.Quotient.mk m) =
AdicCompletion.transitionMap I N (Nat.le_succ n)
(e (Submodule.Quotient.mk m))) ∧
(∀ n (f : M →ₗ[A] N) (m : M),
comparison n (Submodule.Quotient.mk f) (Submodule.Quotient.mk m) =
Submodule.Quotient.mk (f m)) ∧
let HomSys : ℕᵒᵖ ⥤ ModuleCat A :=
Functor.ofOpSequence (X := fun n => ModuleCat.of A (H n))
(fun n => ModuleCat.ofHom (homTransition n))
let IsoSys : ℕᵒᵖ ⥤ Type (max v w) :=
Functor.ofOpSequence (X := E) (fun n => TypeCat.ofHom (isoTransition n))
(HomSys ⋙ forget (ModuleCat A)).IsMittagLeffler ∧
IsoSys.IsMittagLeffler ∧
(∃ c : ℕ, ∀ n,
I ^ c ≤ Module.annihilator A (LinearMap.ker (comparison n)) ∧
I ^ c ≤ Module.annihilator A
(H n ⧸ LinearMap.range (comparison n))) ∧
(∃ homLimitIso :
limit HomSys ≅ ModuleCat.of A (AdicCompletion I (M →ₗ[A] N)),
∀ (f : ↥(limit HomSys)) n,
comparison n
(AdicCompletion.eval I (M →ₗ[A] N) n (homLimitIso.hom.hom f)) =
(limit.π HomSys (op n)).hom f) ∧
(∃ completedHomEquiv :
AdicCompletion I (M →ₗ[A] N) ≃ₗ[AdicCompletion I A]
(AdicCompletion I M →ₗ[AdicCompletion I A] AdicCompletion I N),
∀ (f : M →ₗ[A] N) (m : M),
completedHomEquiv (AdicCompletion.of I (M →ₗ[A] N) f)
(AdicCompletion.of I M m) =
AdicCompletion.of I N (f m)) ∧
∃ isoLimitEquiv :
{ e : ∀ n, E n // ∀ n, isoTransition n (e (n + 1)) = e n } ≃
(AdicCompletion I M ≃ₗ[AdicCompletion I A] AdicCompletion I N),
∀ (e : { e : ∀ n, E n // ∀ n, isoTransition n (e (n + 1)) = e n })
(n : ℕ) (m : M),
e.1 n (Submodule.Quotient.mk m) =
AdicCompletion.eval I N n
(isoLimitEquiv e (AdicCompletion.of I M m))
Tag 09BC, a lemma
Tag 09BC in the Stacks Project.
Stacks.AdicSystem.CompletionIsomorphism.adicCompletion_linearEquiv_of_quotient_linearEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Hom/MittagLeffler.lean, line 672.
Stacks 09BC. If all quotients of two finite modules by powers of an ideal are linearly equivalent, then their adic completions are linearly equivalent over the completed ring.
public theorem adicCompletion_linearEquiv_of_quotient_linearEquiv
{A : Type u} {M : Type v} {N : Type w} [CommRing A] [IsNoetherianRing A]
[AddCommGroup M] [Module A M] [Module.Finite A M]
[AddCommGroup N] [Module A N] [Module.Finite A N]
(I : Ideal A)
(h : ∀ n : ℕ,
Nonempty ((M ⧸ I ^ n • (⊤ : Submodule A M)) ≃ₗ[A]
(N ⧸ I ^ n • (⊤ : Submodule A N)))) :
Nonempty (AdicCompletion I M ≃ₗ[AdicCompletion I A] AdicCompletion I N)
Tag 0EGW, a remark
Tag 0EGW in the Stacks Project.
Stacks.Modules.AdicSystem.AdicModuleSystem.delayedCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Category.lean, line 991.
Stacks 0EGW. Systems of finite
A ⧸ I ^ n-modules, with morphisms represented by mapsI ^ c Eₙ → Fₙ / Fₙ[I ^ c]modulo increasingc, form a category. Composition is the induced composition at delayc + c'.
public noncomputable def delayedCategory : CategoryData (A := A) (I := I)
Tag 0EGX, a lemma
Tag 0EGX in the Stacks Project.
Stacks.AdicModuleSystem.IsomorphismCriterion.isIso_homOfRepresentative_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Category.lean, line 1415.
Stacks 0EGX. A delayed representative induces an isomorphism in the category of systems if and only if, eventually, the kernels and cokernels of all its component maps are annihilated by a single fixed power of the ideal.
public theorem isIso_homOfRepresentative_iff (r : HomRepresentative E F) :
letI := (AdicModuleSystem.delayedCategory (A := A) (I := I)).toCategory
IsIso (show E ⟶ F from homOfRepresentative r) ↔
∃ c' : ℕ, ∀ᶠ n : ℕ+ in atTop, ∀ h : r.delay ≤ (n : ℕ),
Module.IsTorsionBySet A (r.map n h).ker (↑(I ^ c') : Set A) ∧
Module.IsTorsionBySet A
((underlying F n ⧸ torsionPart F n r.delay) ⧸
LinearMap.range (r.map n h)) (↑(I ^ c') : Set A)
Tag 0EGY, a lemma
Tag 0EGY in the Stacks Project.
Stacks.AdicSystem.ExtDelayedIso.extAdicQuotientSystem_iso_extOfAdicQuotientsSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Ext/DelayedIso.lean, line 853.
Stacks 0EGY. For finite modules over a Noetherian ring, the system of adic quotients of
Extis isomorphic, in the category of delayed morphisms, to the system ofExtgroups over the corresponding quotient rings.
public theorem extAdicQuotientSystem_iso_extOfAdicQuotientsSystem
(I : Ideal A) (M N : Type v)
[AddCommGroup M] [Module A M] [Module.Finite A M]
[AddCommGroup N] [Module A N] [Module.Finite A N] (i : ℕ) :
letI := (AdicModuleSystem.delayedCategory (A := A) (I := I)).toCategory
Nonempty (extAdicQuotientSystem I M N i ≅ extOfAdicQuotientsSystem I M N i)
Tag 0EGZ, a remark
Tag 0EGZ in the Stacks Project.
Stacks.AdicSystem.ExtComparison.exists_eventually_extOfAdicQuotients_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Ext/Comparison.lean, line 473.
Stacks 0EGZ. There are powers
I ^ candI ^ dsuch that, form ≫ n ≫ 0, canonical maps fromI ^ c Ext_{A_m}^i(M_m,N_m) / I ^ n Ext_{A_m}^i(M_m,N_m)toExt_{A_n}^i(M_n,N_n) / Ext_{A_n}^i(M_n,N_n)[I ^ c]have kernel and cokernel annihilated byI ^ d. The displayed factorization characterizes these maps in terms of mutually inverse representatives of the isomorphism of Tag 0EGY.The source's single exponent is split: maps are defined on I^c-multiples, and their kernel/cokernel are annihilated by some possibly larger power I^d; with one exponent the claim fails, e.g. for A = k[x,y,z,w]/(xy), I = (x,y,z,w), M = N = A/(x), i = 2.
public theorem exists_eventually_extOfAdicQuotients_comparison (I : Ideal A) (M N : Type v)
[AddCommGroup M] [Module A M] [Module.Finite A M]
[AddCommGroup N] [Module A N] [Module.Finite A N] (i : ℕ) :
letI := (AdicModuleSystem.delayedCategory (A := A) (I := I)).toCategory
let E := extAdicQuotientSystem I M N i
let F := extOfAdicQuotientsSystem I M N i
∃ (e : E ≅ F) (r : AdicModuleSystem.HomRepresentative E F)
(s : AdicModuleSystem.HomRepresentative F E),
AdicModuleSystem.homOfRepresentative r = e.hom ∧
AdicModuleSystem.homOfRepresentative s = e.inv ∧
let c := s.delay + r.delay
∃ d : ℕ,
∃ comparison : ∀ (n m : ℕ+) (_ : c ≤ (n : ℕ)) (_ : n ≤ m),
(AdicModuleSystem.powerPart F m c ⧸
(AdicModuleSystem.powerPart F m (n : ℕ)).comap
(AdicModuleSystem.powerPart F m c).subtype) →ₗ[A]
AdicModuleSystem.underlying F n ⧸ AdicModuleSystem.torsionPart F n c,
∀ᶠ n : ℕ+ in atTop, ∀ᶠ m : ℕ+ in atTop,
∀ (hn : c ≤ (n : ℕ)) (hnm : n ≤ m),
(∀ z : AdicModuleSystem.powerPart F m c,
∃ (yₘ : AdicModuleSystem.powerPart E m r.delay)
(yₙ : AdicModuleSystem.powerPart E n r.delay),
s.map m (le_trans (Nat.le_add_right s.delay r.delay)
(le_trans hn (mod_cast hnm)))
⟨z, AdicModuleSystem.powerPart_add_le_left F m s.delay r.delay z.2⟩ =
(AdicModuleSystem.torsionPart E m s.delay).mkQ yₘ.1 ∧
extAdicQuotientTransition I M N i hnm yₘ = yₙ ∧
comparison n m hn hnm
(Quotient.mk _ z) =
AdicModuleSystem.quotientTransitionOfLE F n
(Nat.le_add_left r.delay s.delay)
(r.map n (le_trans (Nat.le_add_left r.delay s.delay) hn) yₙ)) ∧
Module.IsTorsionBySet A (comparison n m hn hnm).ker
(↑(I ^ d) : Set A) ∧
Module.IsTorsionBySet A
((AdicModuleSystem.underlying F n ⧸ AdicModuleSystem.torsionPart F n c) ⧸
LinearMap.range (comparison n m hn hnm)) (↑(I ^ d) : Set A)
Tag 0EH2, an example
Tag 0EH2 in the Stacks Project.
Stacks.AdicSystem.ExtCounterexample.extTwo_not_preserved_by_adicQuotients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Ext/Counterexample.lean, line 742.
Stacks 0EH2. For
A = k[[x, y]] / (xy)andM = A / (y), the periodic resolution computesExt_A^2(M, N)asN[y] / xN. At the finite level the numerator is the intersection of they-torsion and thex^(n - 1)-torsion. In particular, forN = M, the original Ext group is additively isomorphic tok, while every finite-level Ext group vanishes.
public theorem extTwo_not_preserved_by_adicQuotients (k : Type u) [Field k] :
let R := MvPowerSeries (Fin 2) k
let X : R := MvPowerSeries.X 0
let Y : R := MvPowerSeries.X 1
let A := R ⧸ Ideal.span {X * Y}
let x : A := Ideal.Quotient.mk _ X
let y : A := Ideal.Quotient.mk _ Y
let I : Ideal A := Ideal.span {x}
let M := A ⧸ Ideal.span {y}
Function.Exact (LinearMap.lsmul A A y) (LinearMap.lsmul A A x) ∧
Function.Exact (LinearMap.lsmul A A x) (LinearMap.lsmul A A y) ∧
Function.Exact (LinearMap.lsmul A A y) (Submodule.mkQ (Ideal.span {y})) ∧
Function.Surjective (Submodule.mkQ (Ideal.span {y})) ∧
(∀ (N : Type u) [AddCommGroup N] [Module A N],
let Ky := LinearMap.ker (LinearMap.lsmul A N y)
Nonempty (Ext (ModuleCat.of A M) (ModuleCat.of A N) 2 ≃ₗ[A]
(Ky ⧸ ((I • (⊤ : Submodule A N)).comap Ky.subtype)))) ∧
(∀ (n : ℕ+),
let An := A ⧸ I ^ (n : ℕ)
let xn : An := Ideal.Quotient.mk _ x
let yn : An := Ideal.Quotient.mk _ y
let Mn := M ⧸ (I ^ (n : ℕ) • (⊤ : Submodule A M))
∃ q : An →ₗ[An] Mn,
q 1 = Submodule.Quotient.mk (Ideal.Quotient.mk (Ideal.span {y}) 1) ∧
Function.Surjective q ∧
Function.Exact (LinearMap.lsmul An An yn) q ∧
Function.Exact (LinearMap.lsmul An An xn) (LinearMap.lsmul An An yn) ∧
Function.Exact
((LinearMap.lsmul An An yn).coprod
(LinearMap.lsmul An An (xn ^ ((n : ℕ) - 1))))
(LinearMap.lsmul An An xn)) ∧
(∀ (N : Type u) [AddCommGroup N] [Module A N] (n : ℕ+),
let An := A ⧸ I ^ (n : ℕ)
let anCommRing : CommRing An := Ideal.Quotient.commRing (I ^ (n : ℕ))
letI : Ring An := anCommRing.toRing
letI : CommSemiring An := anCommRing.toCommSemiring
letI : Semiring An := anCommRing.toSemiring
letI : Linear An (ModuleCat An) := ModuleCat.Algebra.instLinear
let xn : An := Ideal.Quotient.mk _ x
let yn : An := Ideal.Quotient.mk _ y
let Nn := N ⧸ (I ^ (n : ℕ) • (⊤ : Submodule A N))
let K := LinearMap.ker (LinearMap.lsmul An Nn yn) ⊓
LinearMap.ker (LinearMap.lsmul An Nn (xn ^ ((n : ℕ) - 1)))
let xNn : Submodule An Nn := Ideal.span {xn} • ⊤
let xK : Submodule An K := xNn.comap K.subtype
Nonempty (Ext (ModuleCat.of An
(M ⧸ (I ^ (n : ℕ) • (⊤ : Submodule A M))))
(ModuleCat.of An Nn) 2 ≃ₗ[An] (K ⧸ xK))) ∧
letI : Module k (Ext (ModuleCat.of A M) (ModuleCat.of A M) 2) :=
Module.compHom _ (algebraMap k A)
Nonempty (Ext (ModuleCat.of A M) (ModuleCat.of A M) 2 ≃ₗ[k] k) ∧
(∀ (n : ℕ+),
let An := A ⧸ I ^ (n : ℕ)
let xn : An := Ideal.Quotient.mk _ x
let Mn := M ⧸ (I ^ (n : ℕ) • (⊤ : Submodule A M))
Nonempty (Mn ≃ₗ[k] ((Polynomial k) ⧸
(Ideal.span {Polynomial.X ^ (n : ℕ)} : Ideal (Polynomial k)))) ∧
Function.Exact (LinearMap.lsmul An Mn xn)
(LinearMap.lsmul An Mn (xn ^ ((n : ℕ) - 1))) ∧
Subsingleton (Ext (ModuleCat.of An Mn) (ModuleCat.of An Mn) 2))
Tag 0EH0, a lemma
Tag 0EH0 in the Stacks Project.
Stacks.AdicSystem.ExtFlatBaseChange.limit_ext_quotient_iso_limit_ext_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Ext/FlatBaseChange.lean, line 687.
Stacks 0EH0. Let
A → Bbe a flat map of Noetherian rings, letIbe an ideal ofA, and letMandNbe finiteB-modules. IfMis flat overA, the canonical reduction maps from theI-adic quotients ofExt_B(M, N)to the Ext groups overB / I ^ n Bare compatible with all transition maps and induce an isomorphism on inverse limits.The maps are given simultaneously in every degree. Their identity, composition, reduction, and quotient-factorization laws record the canonical inverse-system structure. The induced map on limits is an isomorphism of
A-modules.
public theorem limit_ext_quotient_iso_limit_ext_baseChange
{A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN}
[CommRing A] [CommRing B] [Algebra A B]
[AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M]
[AddCommGroup N] [Module B N]
[IsNoetherianRing A] [IsNoetherianRing B] [Module.Flat A B]
[Module.Finite B M] [Module.Finite B N] [Module.Flat A M]
(I : Ideal A) :
let J := I.map (algebraMap A B)
let E : ℕ → Type (max uA uB uM uN) := fun i =>
Ext (ModuleCat.of B (ULift.{max uA uB uM uN} M))
(ModuleCat.of B (ULift.{max uA uB uM uN} N)) i
let _ : ∀ i, Module A (E i) := fun i =>
Module.compHom (E i) (algebraMap A B)
let Q : ℕ → ℕ → Type (max uA uB uM uN) := fun i n =>
E i ⧸ I ^ n • (⊤ : Submodule A (E i))
let Bn : ℕ → Type uB := fun n => B ⧸ J ^ n
let Mn : ℕ → Type uM := fun n =>
M ⧸ J ^ n • (⊤ : Submodule B M)
let Nn : ℕ → Type uN := fun n =>
N ⧸ J ^ n • (⊤ : Submodule B N)
let En : ℕ → ℕ → Type (max uA uB uM uN) := fun i n =>
Ext (ModuleCat.of (Bn n) (ULift.{max uA uB uM uN} (Mn n)))
(ModuleCat.of (Bn n) (ULift.{max uA uB uM uN} (Nn n))) i
let _ : ∀ i n, Module A (En i n) := fun i n =>
Module.compHom (En i n) (algebraMap A (Bn n))
∃ (extTransition : ∀ i m n, n ≤ m → En i m →ₗ[A] En i n)
(reduction : ∀ i n, E i →ₗ[A] En i n)
(comparison : ∀ i n, Q i n →ₗ[A] En i n),
(∀ i n, extTransition i n n le_rfl = LinearMap.id) ∧
(∀ i k m n (hkm : m ≤ k) (hmn : n ≤ m),
(extTransition i m n hmn).comp (extTransition i k m hkm) =
extTransition i k n (hmn.trans hkm)) ∧
(∀ i m n (hmn : n ≤ m),
(extTransition i m n hmn).comp (reduction i m) = reduction i n) ∧
(∀ i n,
(comparison i n).comp (I ^ n • (⊤ : Submodule A (E i))).mkQ = reduction i n) ∧
(∀ i m n (hmn : n ≤ m),
(extTransition i m n hmn).comp (comparison i m) =
(comparison i n).comp (Submodule.factorPow I (E i) hmn)) ∧
∀ i,
let Qsys : Functor ℕᵒᵖ (ModuleCat.{max uA uB uM uN} A) :=
Functor.ofOpSequence
(X := fun n => ModuleCat.of A (Q i n))
(fun n => ModuleCat.ofHom (Submodule.factorPowSucc I (E i) n))
let Esys : Functor ℕᵒᵖ (ModuleCat.{max uA uB uM uN} A) :=
Functor.ofOpSequence
(X := fun n => ModuleCat.of A (En i n))
(fun n => ModuleCat.ofHom
(extTransition i (n + 1) n n.le_succ))
∃ e : limit Qsys ≅ limit Esys,
∀ n, e.hom ≫ limit.π Esys (op n) =
limit.π Qsys (op n) ≫ ModuleCat.ofHom (comparison i n)
Sources
Section15.103 Systems of modules, bis#
Section 15.103 of the Stacks Project, Tag 0G3J. 7 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0G3K, a lemma
Tag 0G3K in the Stacks Project.
Stacks.AdicSystem.Homology.homologyIdealPowers_proIsomorphic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/Homology/IdealPowerComparison.lean, line 408.
Stacks 0G3K. The homology of the complex of ideal powers is canonically pro-isomorphic to the ideal powers of the homology.
public theorem homologyIdealPowers_proIsomorphic
{A : Type u} [CommRing A] [IsNoetherianRing A]
{K : Type v} {L : Type w} {M : Type x}
[AddCommGroup K] [AddCommGroup L] [AddCommGroup M]
[Module A K] [Module A L] [Module A M]
[Module.Finite A K] [Module.Finite A L] [Module.Finite A M]
(I : Ideal A) (α : K →ₗ[A] L) (β : L →ₗ[A] M)
(_hβα : β.comp α = 0) :
let P : ℕ → Submodule A L := fun n =>
LinearMap.ker β ⊓ (I ^ n • (⊤ : Submodule A L))
let D : (n : ℕ) → Submodule A (P n) := fun n =>
Submodule.comap (P n).subtype
(Submodule.map α (I ^ n • (⊤ : Submodule A K)))
let H : ℕ → Type _ := fun n => (P n) ⧸ D n
let Q : ℕ → Type _ := fun n =>
↥(I ^ n • (⊤ : Submodule A (H 0)))
∃ (τ : ∀ (m n : ℕ), n ≤ m → H m →ₗ[A] H n),
(∀ n, τ n n (le_refl n) = LinearMap.id) ∧
(∀ (k m n : ℕ) (hkm : m ≤ k) (hmn : n ≤ m),
(τ m n hmn).comp (τ k m hkm) = τ k n (hmn.trans hkm)) ∧
(∀ (m n : ℕ) (hmn : n ≤ m) (y : P m),
∃ z : P n, z.1 = y.1 ∧
τ m n hmn (Submodule.Quotient.mk y : H m) =
(Submodule.Quotient.mk z : H n)) ∧
∃ c : ℕ, 0 < c ∧
∃ (ρ : ∀ (n : ℕ), c ≤ n → H n →ₗ[A]
↥(I ^ (n - c) • (⊤ : Submodule A (H 0))))
(ψ : ∀ (n : ℕ), c ≤ n →
↥(I ^ n • (⊤ : Submodule A (H 0))) →ₗ[A] H (n - c)),
(∀ (n : ℕ) (hn : c ≤ n) (z : H n),
((ρ n hn z : ↥(I ^ (n - c) • (⊤ : Submodule A (H 0)))) : H 0) =
τ n 0 (Nat.zero_le n) z) ∧
(∀ (n : ℕ) (hn : c ≤ n)
(z : ↥(I ^ n • (⊤ : Submodule A (H 0)))) (y : P n),
y.1 ∈ I ^ n • LinearMap.ker β →
(z : H 0) = τ n 0 (Nat.zero_le n) (Submodule.Quotient.mk y : H n) →
ψ n hn z = τ n (n - c) (Nat.sub_le n c)
(Submodule.Quotient.mk y : H n)) ∧
(∀ (m n : ℕ) (hmn : n ≤ m) (hm : c ≤ m) (hn : c ≤ n)
(z : ↥(I ^ m • (⊤ : Submodule A (H 0))))
(z' : ↥(I ^ n • (⊤ : Submodule A (H 0)))),
(z' : H 0) = z →
τ (m - c) (n - c) (Nat.sub_le_sub_right hmn c) (ψ m hm z) =
ψ n hn z') ∧
(∀ (n : ℕ) (hn : 2 * c ≤ n)
(z : ↥(I ^ n • (⊤ : Submodule A (H 0)))),
(((ρ (n - c) (by omega) (ψ n (by omega) z) :
↥(I ^ ((n - c) - c) • (⊤ : Submodule A (H 0)))) : H 0) = z.1)) ∧
(∀ (n : ℕ) (hn : 2 * c ≤ n) (z : H n),
ψ (n - c) (by omega) (ρ n (by omega) z) =
τ n ((n - c) - c) (by omega) z) ∧
-- The standard explicit witness that the two inverse systems are
-- isomorphic as pro-objects, using the cofinal shift `n ↦ n + c`.
∃ (forward : ∀ m : ℕ, H (m + c) →ₗ[A] Q m)
(backward : ∀ m : ℕ, Q (m + c) →ₗ[A] H m),
(∀ (m m' : ℕ) (h : m ≤ m') (z : H (m' + c)),
((forward m (τ (m' + c) (m + c) (by omega) z) : Q m) : H 0) =
(forward m' z : H 0)) ∧
(∀ (m m' : ℕ) (h : m ≤ m') (z : Q (m' + c)) (z' : Q (m + c)),
(z' : H 0) = z →
backward m z' = τ m' m h (backward m' z)) ∧
(∀ (m : ℕ) (z : H ((m + c) + c)),
backward m (forward (m + c) z) =
τ ((m + c) + c) m (by omega) z) ∧
(∀ (m : ℕ) (z : Q ((m + c) + c)),
((forward m (backward (m + c) z) : Q m) : H 0) = z)
Tag 0G3L, a lemma
Tag 0G3L in the Stacks Project.
Stacks.AdicSystem.ExtIdealPowerRestriction.ext_ideal_power_restriction_factors, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/ExtRestriction.lean, line 527.
Stacks 0G3L. Restriction on positive-degree Ext from a finite module to a sufficiently high ideal power factors through Ext into a shifted ideal power of the second module.
public theorem ext_ideal_power_restriction_factors
{A : Type u} [CommRing A] [IsNoetherianRing A] [Small.{v} A]
{M N : Type v} [AddCommGroup M] [Module A M]
[AddCommGroup N] [Module A N] [Module.Finite A M]
(I : Ideal A) (p : ℕ) (_hp : 0 < p) :
∃ c : ℕ, ∀ n : ℕ, c ≤ n →
let P : Submodule A M := I ^ n • ⊤
let Q : Submodule A N := I ^ (n - c) • ⊤
∃ lift : Ext (ModuleCat.of A M) (ModuleCat.of A N) p →+
Ext (ModuleCat.of A P) (ModuleCat.of A Q) p,
((Ext.mk₀ (ModuleCat.ofHom Q.subtype)).postcomp
(ModuleCat.of A P) (add_zero p)).comp lift =
(Ext.mk₀ (ModuleCat.ofHom P.subtype)).precomp
(ModuleCat.of A N) (zero_add p)
Tag 0927, a lemma
Tag 0927 in the Stacks Project.
Stacks.AdicSystem.ExtRestrictionVanishing.ext_ideal_power_restriction_eq_zero_of_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/ExtRestriction.lean, line 560.
Stacks 0927. If a power of an ideal annihilates
N, then in every positive degree, restriction on Ext from a finite module to some ideal power is zero.
public theorem ext_ideal_power_restriction_eq_zero_of_annihilated
{A : Type u} [CommRing A] [IsNoetherianRing A] [Small.{v} A]
{M N : Type v} [AddCommGroup M] [Module A M]
[AddCommGroup N] [Module A N] [Module.Finite A M]
(I : Ideal A) (hN : ∃ m : ℕ, 0 < m ∧ I ^ m • (⊤ : Submodule A N) = ⊥)
(p : ℕ) (hp : 0 < p) :
∃ n : ℕ,
let P : Submodule A M := I ^ n • ⊤
(Ext.mk₀ (ModuleCat.ofHom P.subtype)).precomp
(ModuleCat.of A N) (zero_add p) = 0
Tag 0DYI, a lemma
Tag 0DYI in the Stacks Project.
Stacks.ExtIdealPowerImage.range_ext_map_ideal_pow_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/ExtRestriction.lean, line 847.
Stacks 0DYI. In each degree, the image in
Ext(K, M)of the Ext group with second argumentI ^ n Mis eventually contained inI ^ (n - c) Ext(K, M).
public theorem range_ext_map_ideal_pow_le
{A : Type u} [CommRing A] [IsNoetherianRing A]
(I : Ideal A) (K : DerivedCategory (ModuleCat.{v} A))
(hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K) (M : ModuleCat.{v} A)
[Module.Finite A M] (p : ℤ) :
∃ c : ℕ, ∀ n : ℕ, c ≤ n →
Set.range (fun x : DerivedCategory.Ext K
((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).obj
(ModuleCat.of A ↥(I ^ n • (⊤ : Submodule A M)))) p ↦
x ≫ ((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).map
(ModuleCat.ofHom (I ^ n • (⊤ : Submodule A M)).subtype))⟦p⟧') ⊆
((I ^ (n - c) • (⊤ : Submodule A
(DerivedCategory.Ext K
((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).obj M) p)) :
Submodule A _) : Set _)
Tag 0G3M, a lemma
Tag 0G3M in the Stacks Project.
Stacks.AdicSystem.KoszulIdealPower.idealPowerSystem_proIso_koszulIdealComplexSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/IdealPowerTensor.lean, line 929.
Stacks Project, Tag 0G3M. Over a Noetherian ring, the inverse system of positive powers of the ideal generated by a finite sequence and the inverse system of shifted, positive-degree Koszul complexes on its positive powers are pro-isomorphic in the derived category. The comparison is induced by the Koszul differential into the corresponding ideal power; the displayed identities express a two-sided inverse after cofinal refinement.
public theorem idealPowerSystem_proIso_koszulIdealComplexSystem
{A : Type u} [CommRing A] [IsNoetherianRing A] {r : ℕ} (f : Fin r → A) :
let I := Ideal.span (Set.range f)
∃ (ε : ∀ n : ℕ,
koszulIdealComplex (fun i ↦ f i ^ (n + 1)) ⟶
(ChainComplex.single₀ (ModuleCat.{u} A)).obj
(ModuleCat.of A ↥(I ^ (n + 1))))
(e : koszulIdealComplexSystem f ⟶ idealPowerSystem I),
(∀ n,
(ε n).f 0 ≫ ModuleCat.ofHom (I ^ (n + 1)).subtype =
(koszulIdealComplexXIso (fun i ↦ f i ^ (n + 1)) 0).hom ≫
(Koszul.seqComplex (fun i ↦ f i ^ (n + 1))).d 1 0 ≫
ModuleCat.ofHom
(exteriorPower.zeroEquiv A (Fin r → A)).toLinearMap) ∧
(∀ n,
e.app (op n) = DerivedCategory.Q.map
(HomologicalComplex.extendMap (ε n) ComplexShape.embeddingDownNat)) ∧
∀ n : ℕ, ∃ (m : ℕ) (h : n ≤ m)
(s : (idealPowerSystem I).obj (op m) ⟶
(koszulIdealComplexSystem f).obj (op n)),
e.app (op m) ≫ s =
(koszulIdealComplexSystem f).map (homOfLE h).op ∧
s ≫ e.app (op n) =
(idealPowerSystem I).map (homOfLE h).op
Tag 0G3N, a lemma
Tag 0G3N in the Stacks Project.
Stacks.AdicSystem.IdealPowerTensorComparison.derivedTensor_idealPowers_proIsomorphic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/CanonicalDerivedTensor.lean, line 100.
Stacks Project, Tag 0G3N. For a bounded complex of finite modules over a Noetherian ring, the inverse system of maps
Iⁿ ⊗ᴸ M → Iⁿ Mformed from the canonical derived tensor product is an isomorphism of pro-objects in the derived category. The displayed identities are the two-sided inverse identities after cofinal refinement.
public theorem derivedTensor_idealPowers_proIsomorphic {A : Type u} [CommRing A]
[IsNoetherianRing A] (I : Ideal A) (M : CochainComplex (ModuleCat.{u} A) ℤ)
(hbounded : ∃ a b : ℤ, a ≤ b ∧ ∀ i : ℤ, i < a ∨ b < i → IsZero (M.X i))
(hfinite : ∀ i : ℤ, Module.Finite A (M.X i)) :
∃ (t : ∀ n, idealPowerComplex M I (n + 1) ⟶ idealPowerComplex M I n)
(_ht : ∀ n, t n ≫ image.ι (idealPowerMultiplication M I n) =
image.ι (idealPowerMultiplication M I (n + 1)))
(α : derivedTensorIdealSystem (DerivedTensorData.canonicalDerivedTensorProduct A)
(DerivedTensorData.canonicalSymmetry A) M I ⟶ idealPowerSystem M I t),
(∀ n, α.app (op n) = derivedToIdealPowerMap
(DerivedTensorData.canonicalDerivedTensorProduct A)
(DerivedTensorData.canonicalSymmetry A) M I n) ∧
∀ n : ℕ, ∃ (m : ℕ) (h : n ≤ m)
(s : (idealPowerSystem M I t).obj (op m) ⟶
(derivedTensorIdealSystem (DerivedTensorData.canonicalDerivedTensorProduct A)
(DerivedTensorData.canonicalSymmetry A) M I).obj (op n)),
α.app (op m) ≫ s =
(derivedTensorIdealSystem (DerivedTensorData.canonicalDerivedTensorProduct A)
(DerivedTensorData.canonicalSymmetry A) M I).map (homOfLE h).op ∧
s ≫ α.app (op n) = (idealPowerSystem M I t).map (homOfLE h).op
Tag 0928, a lemma
Tag 0928 in the Stacks Project.
Stacks.AdicSystem.IdealPowerDerivedTensor.idealPowerInclusion_factors_through_derivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/CanonicalDerivedTensor.lean, line 134.
Stacks Project, Tag 0928. For a finite module over a Noetherian ring, the inclusion of some positive ideal power factors through the canonical map from the canonical derived tensor product with the ideal. The index
nrepresents the positive exponentn + 1.
public theorem idealPowerInclusion_factors_through_derivedTensor
{A : Type u} [CommRing A] [IsNoetherianRing A]
(I : Ideal A) (M : ModuleCat.{v} A) [Module.Finite A M] :
letI := Module.Finite.small.{u} A M
let K := (CochainComplex.singleFunctor (ModuleCat.{u} A) 0).obj
(ModuleCat.of A (Shrink.{u} M))
∃ n : ℕ,
∃ f : DerivedCategory.Q.obj
(Stacks.AdicSystem.IdealPowerTensorComparison.idealPowerComplex K I n) ⟶
(Stacks.AdicSystem.IdealPowerTensorComparison.derivedTensorIdealSystem
(DerivedTensorData.canonicalDerivedTensorProduct A)
(DerivedTensorData.canonicalSymmetry A) K I).obj (op 0),
f ≫
(Stacks.AdicSystem.IdealPowerTensorComparison.derivedToIdealPowerMap
(DerivedTensorData.canonicalDerivedTensorProduct A)
(DerivedTensorData.canonicalSymmetry A) K I 0 ≫
DerivedCategory.Q.map
(image.ι (Stacks.AdicSystem.IdealPowerTensorComparison.idealPowerMultiplication K I
0))) =
DerivedCategory.Q.map
(image.ι (Stacks.AdicSystem.IdealPowerTensorComparison.idealPowerMultiplication K I n))
Sources
Section15.104 Miscellany#
Section 15.104 of the Stacks Project, Tag 0926. 7 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0DYJ, a lemma
Tag 0DYJ in the Stacks Project.
Stacks.AdicSystem.ExtEssentiallyConstant.ext_quotient_ideal_pow_essentially_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/ExtRestriction.lean, line 1323.
Stacks 0DYJ. If high-degree Ext from a pseudo-coherent complex into every finite module is
I-power torsion, then the inverse systemExt^p(K, M / I ^ n M)is essentially constant with valueExt^p(K, M), which is also its limit.
public theorem ext_quotient_ideal_pow_essentially_constant
{A : Type u} [CommRing A] [IsNoetherianRing A]
(I : Ideal A) (K : DerivedCategory (ModuleCat.{v} A))
(hK : StacksDraft.PseudoCoherence.IsPseudoCoherent K) (a : ℤ)
(h : ∀ (N : ModuleCat.{v} A) [Module.Finite A N] (j : ℤ), a ≤ j →
IsIPowerTorsion A
(DerivedCategory.Ext K
((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).obj N) j) I)
(p : ℤ) (hp : a ≤ p) (M : ModuleCat.{v} A) [Module.Finite A M] :
let D : ℕᵒᵖ ⥤ DerivedCategory (ModuleCat.{v} A) :=
Functor.ofOpSequence
(X := fun n ↦ (DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).obj
(ModuleCat.of A (M ⧸ (I ^ n • ⊤ : Submodule A M)))) (fun n ↦
(DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).map
(ModuleCat.ofHom (Submodule.factorPowSucc I M n)))
let E : ℕᵒᵖ ⥤ ModuleCat.{max u (v + 1)} A :=
D ⋙ shiftFunctor (DerivedCategory (ModuleCat.{v} A)) p ⋙
(linearCoyoneda A (DerivedCategory (ModuleCat.{v} A))).obj (op K)
let X := ModuleCat.of A
(DerivedCategory.Ext K
((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).obj M) p)
∃ π : (Functor.const ℕᵒᵖ).obj X ⟶ E,
(∀ n : ℕ, π.app (op n) = ModuleCat.ofHom (Linear.rightComp A K
(((DerivedCategory.singleFunctor (ModuleCat.{v} A) 0).map
(ModuleCat.ofHom
((I ^ n • ⊤ : Submodule A M).mkQ)))⟦p⟧'))) ∧
(∃ (n : ℕᵒᵖ) (s : E.obj n ⟶ X),
EssentiallyConstantPro.IsEssentiallyConstantWith E (Cone.mk X π) n s) ∧
Nonempty (IsLimit (Cone.mk X π))
Tag 0FXN, a lemma
Tag 0FXN in the Stacks Project.
Stacks.TorIdealPowerVanishing.torMap_idealPowerInclusion_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Tor/IdealPower.lean, line 143.
Stacks Project, Tag 0FXN. If
Mis a finite module over a Noetherian ring andNis annihilated by an idealI, then for some positive power ofIthe inclusionIⁿM ⟶ Minduces zero onTor_p(-, N)for everyp ≥ 0. The indexndenotes the positive exponentn + 1.
public theorem torMap_idealPowerInclusion_eq_zero
{A : Type u} [CommRing A] [IsNoetherianRing A]
(I : Ideal A) (M N : ModuleCat.{u} A) [Module.Finite A M]
(hN : I ≤ Module.annihilator A N) :
let K := (CochainComplex.singleFunctor (ModuleCat.{u} A) 0).obj M
let N₀ := (DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj N
∃ n : ℕ, ∀ p : ℕ,
(DerivedCategory.homologyFunctor (ModuleCat.{u} A) (-(p : ℤ))).map
(((DerivedTensorData.canonicalDerivedTensorProduct A).tensor.flip.obj N₀).map
(DerivedCategory.Q.map
(image.ι (Stacks.AdicSystem.IdealPowerTensorComparison.idealPowerMultiplication K I
n)))) = 0
Tag 0D2L, a lemma
Tag 0D2L in the Stacks Project.
Stacks.PseudoCoherent.DerivedInverseLimit.derivedLimit_tensor_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/PseudoCoherent/InverseLimit.lean, line 179.
Stacks Project, Tag 0D2L. Let
Kbe pseudo-coherent and(Mₙ)an inverse system of modules. IfLandL'are derived inverse limits of(Mₙ)and(K ⊗ᴸ Mₙ), respectively, then the canonical comparisonL' ⟶ K ⊗ᴸ Lis an isomorphism. Its displayed equation characterizes it as the comparison induced by the two Milnor triangles.
theorem derivedLimit_tensor_iso
(T : DerivedTensorProduct.{u, v, w} R)
(P : DerivedProducts.{u, v, w} R)
(K : D.{u, v, w} R) (hK : IsPseudoCoherent K)
(M : ℕ → ModuleCat.{max v w} (SmallRing.{u, v, w} R))
(t : ∀ n, M (n + 1) ⟶ M n) :
letI := hasProductsOfShapeNat R P
let S := DerivedCategory.singleFunctor (ModuleCat.{max v w} (SmallRing.{u, v, w} R)) 0
∀ (L : D.{u, v, w} R) (ι : L ⟶ ∏ᶜ fun n => S.obj (M n))
(δ : (∏ᶜ fun n => S.obj (M n)) ⟶ L⟦(1 : ℤ)⟧)
(_ : IsMilnorTriangle (A := SmallRing.{u, v, w} R) (fun n => S.obj (M n))
(fun n => S.map (t n)) L ι δ)
(L' : D.{u, v, w} R)
(ι' : L' ⟶ ∏ᶜ fun n => (T.tensor.obj K).obj (S.obj (M n)))
(δ' : (∏ᶜ fun n => (T.tensor.obj K).obj (S.obj (M n))) ⟶ L'⟦(1 : ℤ)⟧)
(_ : IsMilnorTriangle (A := SmallRing.{u, v, w} R)
(fun n => (T.tensor.obj K).obj (S.obj (M n)))
(fun n => (T.tensor.obj K).map (S.map (t n))) L' ι' δ'),
∃ e : L' ≅ (T.tensor.obj K).obj L,
e.hom ≫ (T.tensor.obj K).map ι ≫
derivedTensorProductComparison R T K (fun n => S.obj (M n)) = ι'
Tag 0929, a lemma
Tag 0929 in the Stacks Project.
Stacks.ProjectiveDimension.Additivity.projectiveDimension_restrictScalars_quotient_eq_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/ProjectiveDimension/Quotient.lean, line 338.
Stacks 0929. Let
Rbe a Noetherian local ring,Ian ideal ofR, andEa nonzero finiteR ⧸ I-module. IfR ⧸ Ihas finite projective dimension overRandEhas finite projective dimension overR ⧸ I, then the restriction ofEtoRhas finite projective dimension, equal to the sum of the two given projective dimensions.
theorem projectiveDimension_restrictScalars_quotient_eq_add
{R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Small.{v} R]
(I : Ideal R) (E : Type v) [AddCommGroup E] [Module (R ⧸ I) E]
[Nontrivial E] [Module.Finite (R ⧸ I) E]
(hRI : Module.projectiveDimension R (R ⧸ I) ≠ ⊤)
(hE : Module.projectiveDimension (R ⧸ I) E ≠ ⊤) :
let E_R := (ModuleCat.restrictScalars.{v} (Ideal.Quotient.mk I)).obj
(ModuleCat.of (R ⧸ I) E)
Module.projectiveDimension R E_R ≠ ⊤ ∧
Module.projectiveDimension R E_R =
Module.projectiveDimension R (R ⧸ I) + Module.projectiveDimension (R ⧸ I) E
Tag 0GYI, a lemma
Tag 0GYI in the Stacks Project.
Stacks.SubcomplexEnlargement.exists_enlargements_killing_kernel_and_covering_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/SubcomplexEnlargement/CompatibleEnlargements.lean, line 370.
Compatible subcomplexes of quasi-isomorphic complexes after derived base change can be enlarged, with a bound depending only on the ring map, so that the kernel defect vanishes and the image defect is covered in every degree.
public theorem exists_enlargements_killing_kernel_and_covering_image
{A : Type u} {B : Type v} [CommRing A] [CommRing B] (f : A →+* B) :
∃ κ : Cardinal.{max u v},
letI : (ModuleCat.extendScalars.{u, v, max v (max u w)} f).IsLeftAdjoint :=
ModuleCat.instIsLeftAdjointExtendScalars.{u, v, max u w} f
let E : CochainComplex (ModuleCat.{max u v w} A) ℤ ⥤
CochainComplex (ModuleCat.{max u v w} B) ℤ :=
(ModuleCat.extendScalars.{u, v, max v (max u w)} f).mapHomologicalComplex
(ComplexShape.up ℤ)
let G : CochainComplex (ModuleCat.{max u v w} A) ℤ ⥤
DerivedCategory (ModuleCat.{max u v w} B) :=
E ⋙ DerivedCategory.Q (C := ModuleCat.{max u v w} B)
∀ (T : DerivedCategory (ModuleCat.{max u v w} A) ⥤
DerivedCategory (ModuleCat.{max u v w} B))
(α : DerivedCategory.Q (C := ModuleCat.{max u v w} A) ⋙ T ⟶ G)
[T.IsLeftDerivedFunctor α
(HomologicalComplex.quasiIso (ModuleCat.{max u v w} A) (ComplexShape.up ℤ))]
(M : CochainComplex (ModuleCat.{max u v w} A) ℤ)
(N : CochainComplex (ModuleCat.{max u v w} B) ℤ),
∀ (b : E.obj M ⟶ N),
IsIso (α.app M ≫
(DerivedCategory.Q (C := ModuleCat.{max u v w} B)).map b) →
∀ (M₁ : CochainComplex (ModuleCat.{max u v w} A) ℤ)
(N₁ : CochainComplex (ModuleCat.{max u v w} B) ℤ)
(m₁ : M₁ ⟶ M) (n₁ : N₁ ⟶ N) [Mono m₁] [Mono n₁]
(b₁ : E.obj M₁ ⟶ N₁),
E.map m₁ ≫ b = b₁ ≫ n₁ →
∃ (M₂ : CochainComplex (ModuleCat.{max u v w} A) ℤ)
(N₂ : CochainComplex (ModuleCat.{max u v w} B) ℤ)
(m₂ : M₂ ⟶ M) (n₂ : N₂ ⟶ N) (_ : Mono m₂) (_ : Mono n₂)
(m₁₂ : M₁ ⟶ M₂) (n₁₂ : N₁ ⟶ N₂) (_ : Mono m₁₂) (_ : Mono n₁₂)
(b₂ : E.obj M₂ ⟶ N₂),
m₁₂ ≫ m₂ = m₁ ∧ n₁₂ ≫ n₂ = n₁ ∧ E.map m₂ ≫ b = b₂ ≫ n₂ ∧
(∀ i : ℤ,
let H := DerivedCategory.homologyFunctor (ModuleCat.{max u v w} B) i
kernel.ι (H.map (α.app M₁ ≫
(DerivedCategory.Q (C := ModuleCat.{max u v w} B)).map b₁)) ≫
H.map (T.map
((DerivedCategory.Q (C := ModuleCat.{max u v w} A)).map m₁₂)) = 0) ∧
(∀ i : ℤ,
let H := DerivedCategory.homologyFunctor (ModuleCat.{max u v w} B) i
imageSubobject (H.map
((DerivedCategory.Q (C := ModuleCat.{max u v w} B)).map n₁₂)) ≤
imageSubobject (H.map (α.app M₂ ≫
(DerivedCategory.Q (C := ModuleCat.{max u v w} B)).map b₂))) ∧
Cardinal.mk ((Σ i : ℤ, M₂.X i) ⊕ (Σ i : ℤ, N₂.X i)) ≤
max (Cardinal.lift.{w} κ)
(Cardinal.mk ((Σ i : ℤ, M₁.X i) ⊕ (Σ i : ℤ, N₁.X i)))
Tag 0H84, a lemma
Tag 0H84 in the Stacks Project.
Stacks.DerivedCategory.MultiplicationCone.homology_isZero_of_localization_and_cone_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/ConeBoundedness.lean, line 94.
Let
Cbe a cone of multiplication byfonM. If every negative cohomology module ofMvanishes after localizing away fromf, and the cohomology ofCvanishes in degrees below-1, then every negative cohomology module ofMvanishes.
theorem homology_isZero_of_localization_and_cone_isZero
{R : Type u} [CommRing R]
(f : R) (M C : DerivedCategory (ModuleCat.{v} R))
(g : M ⟶ C) (h : C ⟶ M⟦1⟧)
(hC : Triangle.mk (f • 𝟙 M) g h ∈
distTriang (DerivedCategory (ModuleCat.{v} R)))
(hM : ∀ i : ℤ, i < 0 →
IsZero (ModuleCat.of R (LocalizedModule.Away f
((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj M))))
(hcone : ∀ i : ℤ, i < -1 →
IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj C)) :
∀ i : ℤ, i < 0 →
IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{v} R) i).obj M)
Tag 0H85, a lemma
Tag 0H85 in the Stacks Project.
Stacks.Flatness.LocalizationReduction.isomorphic_to_flat_module_of_localization_and_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Flat/LocalizationReduction.lean, line 506.
Let
M ∈ D(R)have no positive cohomology. If its derived base changes to the localizationR_fand the quotientR / fRare each isomorphic to a flat module placed in degree zero, thenMis isomorphic to a flatR-module placed in degree zero.
public theorem isomorphic_to_flat_module_of_localization_and_quotient
{R : Type u} [CommRing R] (f : R)
(M : DerivedCategory (ModuleCat.{max v u} R))
(hM : ∀ i : ℤ, 0 < i →
IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{max v u} R) i).obj M))
(hAway : ∃ F : ModuleCat.{max v u} (Localization.Away f),
Module.Flat (Localization.Away f) F ∧
Nonempty ((CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars
(algebraMap R (Localization.Away f))).functor.obj M ≅
(DerivedCategory.singleFunctor
(ModuleCat.{max v u} (Localization.Away f)) 0).obj F))
(hQuot : ∃ F : ModuleCat.{max v u} (R ⧸ Ideal.span {f}),
Module.Flat (R ⧸ Ideal.span {f}) F ∧
Nonempty ((CochainComplex.DerivedExtensionScalars.totalDerivedExtensionScalars
(Ideal.Quotient.mk (Ideal.span {f}))).functor.obj M ≅
(DerivedCategory.singleFunctor
(ModuleCat.{max v u} (R ⧸ Ideal.span {f})) 0).obj F)) :
∃ F : ModuleCat.{max v u} R, Module.Flat R F ∧
Nonempty (M ≅
(DerivedCategory.singleFunctor (ModuleCat.{max v u} R) 0).obj F)
Sources
Section15.105 Tricks with double complexes#
Section 15.105 of the Stacks Project, Tag 0EYW. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0H0Q, a lemma
Tag 0H0Q in the Stacks Project.
CplxCplx.total_H0_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/ProductTotalComplex.lean, line 386.
Stacks Tag 0H0Q (Lemma 15.105.1). Let
A_0^• → A_1^• → ⋯be a complex of complexes of abelian groups such thatH^{-p}(A_p^•) = 0for allp ≥ 0. ThenH^0(Tot_π(A^{•,•})) = 0, i.e. every degree-0cocycle of the product total complex is a coboundary: everyx ∈ Tot_π^0withD^0 x = 0isD^{-1} yfor somey ∈ Tot_π^{-1}. (Together withD ∘ D = 0, recorded intotalD_totalD_eq_zerobelow, this says exactly thatker(D^0) = im(D^{-1}), i.e.H^0(Tot_π) = 0.)Rigorous proof (recursion on
p; see the block comment above for the math). Build, byNat.rec, a dependent streamY : (p : ℕ) → Σ' (yp : c.A p (-1 - (p:ℤ))), c.StageInvariant x p ypsuch that the component equation ofD^{-1} (fun p => (Y p).fst) = xholds at everyp; sety p := (Y p).fst. * Base (Y 0).d_eq_zero_of_totalD_eq_zerosaysx 0is a0-cocycle, sohH 0(after reconciling0 - ↑0 = -↑0) yieldswwithd_2(w) = x_0; take(Y 0).fst := w.StageInvariant x 0 wreduces ((-1)^0 = 1) tof_0(d_2 w) = f_0(x_0), immediate fromd_2 w = x_0. * Step (Y (p+1)fromY p). Letyp := (Y p).fst,hinv := (Y p).snd.d_sub_eq_zero_of_stageInvariant c hx hinvshowsr_{p+1} = x_{p+1} - f_p(yp)is a(-(p+1))-cocycle, sohH (p+1)yieldsw'withd_2(w') = (-1)^{p+1} r_{p+1}(scale the witness by(-1)^{p+1}, valid since(-1)^{p+1}is a unit; or equivalently applyhHto(-1)^{p+1} r_{p+1}, which is also a cocycle). Take(Y (p+1)).fst := w'. ThenStageInvariant x (p+1) w'follows becausef\_\{p+1}(d\_2 w') = (-1)^\{p+1} f\_\{p+1}(r\_\{p+1}) = (-1)^\{p+1}(f\_\{p+1}(x\_\{p+1}) - f\_\{p+1}(f\_p yp)) = (-1)^\{p+1} f\_\{p+1}(x\_\{p+1})usingc.f_f p(f_{p+1}∘f_p = 0). Finallyc.totalD (-1) y = xbyfunext p,cases p, reading off the recorded construction equations (thep=0andp+1cases oftotalD_apply_zero/totalD_apply_succ,dPartHom_apply,fPartHom_apply).
theorem total_H0_eq_zero (c : CplxCplx)
(hH : ∀ p : ℕ, c.InternalCohomologyVanishes p)
(x : c.Tot 0) (hx : c.totalD 0 x = 0) :
∃ y : c.Tot (-1), c.totalD (-1) y = x
Tag 0EYX, a lemma
Tag 0EYX in the Stacks Project.
CplxCplx.Hom.isTotalQuasiIso_of_isInternalQuasiIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/ProductTotalComplex/Rowwise.lean, line 611.
A morphism between complexes of cochain complexes which is a quasi-isomorphism on every internal complex induces a quasi-isomorphism between their product total complexes.
theorem isTotalQuasiIso_of_isInternalQuasiIso {c c' : CplxCplx} (g : CplxCplx.Hom c c')
(hg : g.IsInternalQuasiIso) : g.IsTotalQuasiIso
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.