22.27 Obtaining triangulated… to 22.36 Characterizing compact…
Section22.27 Obtaining triangulated categories#
Section 22.27 of the Stacks Project, Tag 09P5. 17 tags here are carried by 43 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09P6, a lemma
Tag 09P6 in the Stacks Project.
DifferentialGradedModule.connectingHom_gradedSplit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/GradedSplitAdmissible.lean, line 143. The attribute's comment: “the connecting morphism of a graded splitting is the connecting homomorphism”.
The connecting homomorphism of the admissible sequence is the connecting morphism of the graded splitting. Both are
π d(s): the Hom differential of the differential graded category is the graded commutatord ∘ s - s ∘ d, and its second term is killed byπ ∘ s = 0.
theorem connectingHom_gradedSplit (z : Z.M) :
(connectingHom (homOfCocycle A E.a) (homOfCocycle A E.b)
(isAdmissibleShortExact_gradedSplit A E)
(gradedSplitS A E) (gradedSplitPi A E)
(gradedSplit_b_s A E) (gradedSplit_pi_a A E)
(compatibleSplittings_gradedSplit A E).hker).val.toFun z =
(DGCategory.GradedSplitShortExact.connectingHom E).1 z
CochainComplex.gradedSplitOfDegreewiseSplit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/CochainComplexGradedSplit.lean, line 102. The attribute's comment: “a degreewise split short exact sequence of complexes”.
A degreewise split short complex of cochain complexes is a graded-split short exact sequence of the differential graded category of complexes.
def gradedSplitOfDegreewiseSplit :
DGCategory.GradedSplitShortExact (A := dgCategory B) S.X₁ S.X₂ S.X₃
CochainComplex.connectingHom_gradedSplitOfDegreewiseSplit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/CochainComplexGradedSplit.lean, line 163. The attribute's comment: “the connecting morphism of a degreewise split sequence of complexes”.
The connecting morphism of a degreewise split sequence of complexes is Mathlib's
CochainComplex.cocycleOfDegreewiseSplit. The Hom differential ofsis the graded commutators ≫ d - d ≫ s, and its second term dies againstπbecauseπ ∘ s = 0, leaving(σ p).s ≫ d ≫ (σ q).r.
theorem connectingHom_gradedSplitOfDegreewiseSplit :
DGCategory.GradedSplitShortExact.connectingHom (gradedSplitOfDegreewiseSplit S σ) =
(cocycleOfDegreewiseSplit S σ).1
CochainComplex.dgShiftComparisonData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/CochainComplexShiftComparison.lean, line 111. The attribute's comment: “axiom (B)'s identification of Hom complexes, for complexes”.
Mathlib's shift supplies axiom (B)'s identification of Hom modules for the differential graded category of complexes. A degree
k + ncochainX ⟶ Yis a degreekcochainX ⟶ Y[n]; the identification multiplies the Hom differential by(-1)^nand leaves composition on the right alone.
noncomputable def dgShiftComparisonData :
DGCategory.ShiftComparisonData (dgCategory B)
DGCategory.GradedSplitShortExact.connectingHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 165. The attribute's comment: “the connecting morphism”.
The connecting morphism
π d(s), as a homogeneous morphism of degree one.
public def connectingHom {x y z : A.Obj} (E : GradedSplitShortExact (A := A) x y z) :
A.Hom z x 1
DGCategory.GradedSplitShortExact.connectingHom_eq_neg_d_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 282. The attribute's comment: “alternative formula for the connecting morphism”.
The alternative formula
δ = -d(π)sfor the connecting morphism.
public theorem connectingHom_eq_neg_d_comp {x y z : A.Obj}
(E : GradedSplitShortExact (A := A) x y z) :
connectingHom E =
-A.comp (by omega : (0 + 1 : ℤ) + 0 = 1) (A.d E.π) E.s
DGCategory.GradedSplitShortExact.connectingHom_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 290. The attribute's comment: “the connecting morphism is closed”.
The connecting morphism is a cocycle.
public theorem connectingHom_closed {x y z : A.Obj}
(E : GradedSplitShortExact (A := A) x y z) : A.d (connectingHom E) = 0
DGCategory.GradedSplitShortExact.comp_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 300. The attribute's comment: “the first consecutive composite”.
The composite
x ⟶ y ⟶ zis zero.
public theorem comp_zero {x y z : A.Obj}
(E : GradedSplitShortExact (A := A) x y z) :
A.comp (by omega : (0 : ℤ) + 0 = 0) E.b.1 E.a.1 = 0
DGCategory.GradedSplitShortExact.comp_connectingHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 338. The attribute's comment: “the third consecutive composite”.
The composite
z ⟶ x[1] ⟶ y[1]is the boundaryd(s)before shifting.
public theorem comp_connectingHom {x y z : A.Obj}
(E : GradedSplitShortExact (A := A) x y z) :
A.comp (by omega : (0 : ℤ) + 1 = 1) E.a.1 (connectingHom E) = A.d E.s
DGCategory.GradedSplitShortExact.connectingHom_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 345. The attribute's comment: “the second consecutive composite”.
The composite
y ⟶ z ⟶ x[1]is the boundaryd(-π)before shifting.
public theorem connectingHom_comp {x y z : A.Obj}
(E : GradedSplitShortExact (A := A) x y z) :
A.comp (by omega : (1 : ℤ) + 0 = 1) (connectingHom E) E.b.1 = A.d (-E.π)
DGCategory.GradedSplitShortExact.connecting_shift_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 353. The attribute's comment: “closed connecting map into the shift”.
The degree-one connecting cocycle remains closed after conversion to a map into the shifted object.
public theorem connecting_shift_closed {x y z : A.Obj}
(S : ShiftAxiomB A) (E : GradedSplitShortExact (A := A) x y z) :
A.d ((S.toShift 1 z x 0) (connectingHom E)) = 0
DGCategory.GradedSplitShortExact.connectingCocycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 366. The attribute's comment: “the triangle's connecting arrow”.
The actual connecting arrow
z ⟶ x[1]inComp(A).
public def connectingCocycle {x y z : A.Obj}
(S : ShiftAxiomB A) (E : GradedSplitShortExact (A := A) x y z) :
A.Cocycle z ((S.shiftFunctor 1).obj x)
DGCategory.GradedSplitShortExact.associatedCompTriangle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 384. The attribute's comment: “the associated triangle in the category of complexes”.
The associated triangle in the category of complexes, with the arrow
z ⟶ x[1]given byπ d(s).
public def associatedCompTriangle {x y z : A.Obj}
(S : ShiftAxiomB A) (E : GradedSplitShortExact (A := A) x y z) :
letI : HasShift A.Comp ℤ := S.compShift
Pretriangulated.Triangle A.Comp
DGCategory.GradedSplitShortExact.associatedKTriangle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 397. The attribute's comment: “the associated triangle in the homotopy category”.
The same triangle, regarded in the homotopy category.
public def associatedKTriangle {x y z : A.Obj}
(S : ShiftAxiomB A) (E : GradedSplitShortExact (A := A) x y z) :
letI : HasShift A.K ℤ := S.kShift
Pretriangulated.Triangle A.K
DGCategory.GradedSplitShortExact.first_comp_zero_in_K, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 413. The attribute's comment: “first composite vanishes in the homotopy category”.
The first two arrows compose to zero in the homotopy category.
public theorem first_comp_zero_in_K {x y z : A.Obj}
(E : GradedSplitShortExact (A := A) x y z) :
A.compK (Quotient.mk (A.homotopySetoid y z) E.b)
(Quotient.mk (A.homotopySetoid x y) E.a) =
Quotient.mk (A.homotopySetoid x z)
(⟨0, A.d_zero⟩ : A.Cocycle x z)
DGCategory.GradedSplitShortExact.connecting_comp_zero_in_K, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 436. The attribute's comment: “second composite vanishes in the homotopy category”.
The composite
y ⟶ z ⟶ x[1]is zero inK(A).
public theorem connecting_comp_zero_in_K {x y z : A.Obj}
(S : ShiftAxiomB A)
(E : GradedSplitShortExact (A := A) x y z) :
A.compK (Quotient.mk (A.homotopySetoid z ((S.shiftFunctor 1).obj x))
(connectingCocycle S E))
(Quotient.mk (A.homotopySetoid y z) E.b) =
Quotient.mk (A.homotopySetoid y ((S.shiftFunctor 1).obj x))
(⟨0, A.d_zero⟩ : A.Cocycle y ((S.shiftFunctor 1).obj x))
DGCategory.GradedSplitShortExact.comp_connecting_zero_in_K, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 465. The attribute's comment: “third composite vanishes in the homotopy category”.
The composite
z ⟶ x[1] ⟶ y[1]is zero inK(A).
public theorem comp_connecting_zero_in_K {x y z : A.Obj}
(S : ShiftAxiomB A)
(E : GradedSplitShortExact (A := A) x y z) :
A.compK (Quotient.mk (A.homotopySetoid ((S.shiftFunctor 1).obj x)
((S.shiftFunctor 1).obj y)) ((S.shiftFunctor 1).mapCocycle E.a))
(Quotient.mk (A.homotopySetoid z ((S.shiftFunctor 1).obj x))
(connectingCocycle S E)) =
Quotient.mk (A.homotopySetoid z ((S.shiftFunctor 1).obj y))
(⟨0, A.d_zero⟩ : A.Cocycle z ((S.shiftFunctor 1).obj y))
DGCategory.GradedSplitShortExact.shifted_connecting_comp_zero_in_K, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Triangulated.lean, line 527. The attribute's comment: “rotated composite vanishes in the homotopy category”.
The rotated composite
z[-1] ⟶ x ⟶ yis zero inK(A).
public theorem shifted_connecting_comp_zero_in_K {x y z : A.Obj}
(S : ShiftAxiomB A)
(E : GradedSplitShortExact (A := A) x y z) :
A.compK (Quotient.mk (A.homotopySetoid x y) E.a)
(Quotient.mk (A.homotopySetoid ((S.shiftFunctor (-1)).obj z) x)
(shiftedConnecting S E)) =
Quotient.mk (A.homotopySetoid ((S.shiftFunctor (-1)).obj z) y)
(⟨0, A.d_zero⟩ : A.Cocycle ((S.shiftFunctor (-1)).obj z) y)
Tag 09QJ, a situation
Tag 09QJ in the Stacks Project.
DGCategory.ConeSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ConeSituation.lean, line 37.
Axioms (A), (B), and (C) for a differential graded category. For every closed degree-zero arrow
f : x ⟶ y, the sequencey ⟶ c(f) ⟶ x[1]is admissible and its connecting arrowx[1] ⟶ y[1]isf[1].
structure ConeSituation {R : Type w} [CommRing R] (A : DGCategory.{v, u} R)
Tag 09P7, a lemma
Tag 09P7 in the Stacks Project.
DGCategory.exists_coneTriangleMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ConeMorphism.lean, line 254.
A homotopy-commutative square of complexes induces a morphism of their cone triangles, whose cone component has a representative in the category of complexes.
theorem exists_coneTriangleMorphism (S : ConeSituation A)
{x₁ y₁ x₂ y₂ : A.Obj}
(f₁ : A.Cocycle x₁ y₁) (f₂ : A.Cocycle x₂ y₂)
(a : A.Cocycle x₁ x₂) (b : A.Cocycle y₁ y₂)
(hcomm : A.compK (Quotient.mk (A.homotopySetoid y₁ y₂) b)
(Quotient.mk (A.homotopySetoid x₁ y₁) f₁) =
A.compK (Quotient.mk (A.homotopySetoid x₂ y₂) f₂)
(Quotient.mk (A.homotopySetoid x₁ x₂) a)) :
∃ c : A.Cocycle (S.cone f₁) (S.cone f₂),
(A.compK
(Quotient.mk (A.homotopySetoid (S.cone f₁) (S.cone f₂)) c)
(Quotient.mk (A.homotopySetoid y₁ (S.cone f₁)) (S.coneSequence f₁).a) =
A.compK
(Quotient.mk (A.homotopySetoid y₂ (S.cone f₂)) (S.coneSequence f₂).a)
(Quotient.mk (A.homotopySetoid y₁ y₂) b)) ∧
(A.compK
(Quotient.mk (A.homotopySetoid (S.cone f₂)
((S.shift.shiftFunctor 1).obj x₂)) (S.coneSequence f₂).b)
(Quotient.mk (A.homotopySetoid (S.cone f₁) (S.cone f₂)) c) =
A.compK
(Quotient.mk (A.homotopySetoid ((S.shift.shiftFunctor 1).obj x₁)
((S.shift.shiftFunctor 1).obj x₂))
((S.shift.shiftFunctor 1).mapCocycle a))
(Quotient.mk (A.homotopySetoid (S.cone f₁)
((S.shift.shiftFunctor 1).obj x₁)) (S.coneSequence f₁).b))
Tag 09QK, a lemma
Tag 09QK in the Stacks Project.
DGCategory.id_cone_homotopic_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ConeMorphism.lean, line 404.
The identity of the cone of an identity morphism is homotopic to zero.
theorem id_cone_homotopic_zero (S : ConeSituation A) (x : A.Obj) :
let c := S.cone (⟨A.id x, A.d_id x⟩ : A.Cocycle x x)
A.Homotopic (⟨A.id c, A.d_id c⟩ : A.Cocycle c c) (⟨0, A.d_zero⟩ : A.Cocycle c c)
Tag 09QL, a lemma
Tag 09QL in the Stacks Project.
DGCategory.exists_rectification_of_isAdmissibleMono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Rectification.lean, line 66. The attribute's comment: “adjust_right”.
Rectify the right arrow of a homotopy-commutative square along an admissible monomorphism.
theorem exists_rectification_of_isAdmissibleMono {x y z w : A.Obj}
(f : A.Cocycle x y) (a : A.Cocycle x z) (b : A.Cocycle y w) (g : A.Cocycle z w)
(hcomm : A.Homotopic (A.compCocycle b f) (A.compCocycle g a))
(hf : IsAdmissibleMono f) :
∃ b' : A.Cocycle y w,
A.Homotopic b b' ∧ A.compCocycle b' f = A.compCocycle g a
DGCategory.exists_rectification_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Rectification.lean, line 87. The attribute's comment: “adjust_left”.
Rectify the left arrow of a homotopy-commutative square along an admissible epimorphism, presented by a degree-zero section of its lower horizontal arrow.
theorem exists_rectification_left (C : ConeSituation A) (S : HomotopyCommutativeSquare C)
(hg : ∃ s : A.Hom S.w S.z 0,
A.comp (show (0 : ℤ) + 0 = 0 by omega) S.g.1 s = A.id S.w) :
∃ a' : A.Cocycle S.x S.z,
A.Homotopic S.a a' ∧ A.compCocycle S.g a' = A.compCocycle S.b S.f
Tag 09QM, a lemma
Tag 09QM in the Stacks Project.
DGCategory.exists_admissibleMono_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/AdmissibleMonoFactorization.lean, line 351.
Every morphism in the category of complexes factors through an admissible monomorphism followed by a retraction admitting a strict section and a homotopy inverse.
public theorem exists_admissibleMono_factorization
{R : Type w} [CommRing R] {A : DGCategory.{v, u} R}
(S : ConeSituation A) {x y : A.Obj} (α : A.Cocycle x y) :
∃ (y' z : A.Obj) (E : GradedSplitShortExact (A := A) x y' z)
(π : A.Cocycle y' y) (s : A.Cocycle y y'),
(A.compCocycle π E.a = α) ∧
(A.compCocycle π s = (⟨A.id y, A.d_id y⟩ : A.Cocycle y y)) ∧
A.Homotopic (A.compCocycle s π)
(⟨A.id y', A.d_id y'⟩ : A.Cocycle y' y')
Tag 09QN, a lemma
Tag 09QN in the Stacks Project.
DGCategory.exists_admissibleMono_sequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/AdmissibleMonoFactorization.lean, line 515.
A finite chain of maps in the category of complexes has a commuting replacement by admissible monomorphisms, with a homotopy equivalence at every vertex.
public theorem exists_admissibleMono_sequence {R : Type w} [CommRing R]
(A : DGCategory.{v, u} R) (S : ConeSituation A) (n : ℕ)
(x : Fin (n + 1) → A.Comp)
(f : ∀ i : Fin n, x i.castSucc ⟶ x i.succ) :
∃ (y : Fin (n + 1) → A.Comp)
(g : ∀ i : Fin n, y i.castSucc ⟶ y i.succ)
(p : ∀ i : Fin (n + 1), y i ⟶ x i),
(∀ i : Fin n,
∃ z : A.Obj, ∃ E : GradedSplitShortExact (A := A)
(y i.castSucc) (y i.succ) z, E.a = g i) ∧
(∀ i : Fin (n + 1), IsIso ((A.compToK).map (p i))) ∧
(∀ i : Fin n, g i ≫ p i.succ = p i.castSucc ≫ f i)
Tag 09QP, a lemma
Tag 09QP in the Stacks Project.
DGCategory.comp_homotopic_zero_of_gradedSplitShortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/AdmissibleNullHomotopy.lean, line 109.
Two morphisms whose composites with opposite sides of an admissible short exact sequence vanish up to homotopy have null-homotopic composite.
theorem comp_homotopic_zero_of_gradedSplitShortExact {x y z y₁ y₃ : A.Obj}
(E : GradedSplitShortExact (A := A) x y z)
(b : A.Cocycle y₁ y) (b' : A.Cocycle y y₃)
(hb : A.Homotopic (A.compCocycle E.b b) ⟨0, A.d_zero⟩)
(hb' : A.Homotopic (A.compCocycle b' E.a) ⟨0, A.d_zero⟩) :
A.Homotopic (A.compCocycle b' b) ⟨0, A.d_zero⟩
Tag 09QQ, a lemma
Tag 09QQ in the Stacks Project.
DGCategory.associatedKTriangle_eq_of_same_sequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/TriangleIndependence.lean, line 139.
Changing the graded splitting of an admissible short exact sequence does not change its associated triangle in the homotopy category.
theorem associatedKTriangle_eq_of_same_sequence {x y z : A.Obj} (S : ShiftAxiomB A)
(E E' : GradedSplitShortExact (A := A) x y z) (ha : E.a = E'.a) (hb : E.b = E'.b) :
GradedSplitShortExact.associatedKTriangle S E =
GradedSplitShortExact.associatedKTriangle S E'
Tag 09QR, a lemma
Tag 09QR in the Stacks Project.
DGCategory.associatedCompTriangle_coneSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/RotatedConeTriangle.lean, line 60. The attribute's comment: “the statement in Comp(A): the triangle associated to the cone sequence of f is the triangle on y, c(f), x[1] whose first two arrows are that sequence's inclusion and projection and whose connecting arrow is f[1]. The homotopy-category form is associatedKTriangle_coneSequence; neither covers the comparison with the cone triangle of f (Tag 09QU) nor the rotation of this triangle (Tag 09QS)”.
Let
f : x ⟶ ybe a morphism inComp(𝒜). The triangle(y, c(f), x[1], i, p, f[1])is the triangle associated to the admissible short exact sequencey ⟶ c(f) ⟶ x[1].
theorem associatedCompTriangle_coneSequence (C : ConeSituation A) {x y : A.Obj}
(f : A.Cocycle x y) :
letI : HasShift A.Comp ℤ := C.shift.compShift
GradedSplitShortExact.associatedCompTriangle C.shift (C.coneSequence f) =
Pretriangulated.Triangle.mk
((C.coneSequence f).a : (show A.Comp from y) ⟶ (show A.Comp from C.cone f))
((C.coneSequence f).b :
(show A.Comp from C.cone f) ⟶
(show A.Comp from (C.shift.shiftFunctor 1).obj x))
(((C.shift.shiftFunctor 1).mapCocycle f :
(show A.Comp from (C.shift.shiftFunctor 1).obj x) ⟶
(show A.Comp from (C.shift.shiftFunctor 1).obj y)) ≫
eqToHom (congrArg (fun F : A.Comp ⥤ A.Comp => F.obj y)
(C.shift.compShift_functor 1)).symm)
DGCategory.associatedKTriangle_coneSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/RotatedConeTriangle.lean, line 86. The attribute's comment: “the statement in K(A): the triangle associated to the cone sequence of f is the triangle on y, c(f), x[1] whose first two arrows are the homotopy classes of that sequence's inclusion and projection and whose connecting arrow is the class of f[1]. The form in Comp(A) is associatedCompTriangle_coneSequence; neither covers the comparison with the cone triangle of f (Tag 09QU) nor the rotation of this triangle (Tag 09QS)”.
The same identification in the homotopy category: the triangle
(y, c(f), x[1], i, p, f[1])is the triangle associated to the admissible short exact sequencey ⟶ c(f) ⟶ x[1].
theorem associatedKTriangle_coneSequence (C : ConeSituation A) {x y : A.Obj}
(f : A.Cocycle x y) :
letI : HasShift A.K ℤ := C.shift.kShift
GradedSplitShortExact.associatedKTriangle C.shift (C.coneSequence f) =
Pretriangulated.Triangle.mk
(Quotient.mk (A.homotopySetoid y (C.cone f)) (C.coneSequence f).a)
(Quotient.mk (A.homotopySetoid (C.cone f) ((C.shift.shiftFunctor 1).obj x))
(C.coneSequence f).b)
((Quotient.mk (A.homotopySetoid ((C.shift.shiftFunctor 1).obj x)
((C.shift.shiftFunctor 1).obj y))
((C.shift.shiftFunctor 1).mapCocycle f)) ≫
eqToHom (congrArg (fun F : A.K ⥤ A.K => F.obj y)
(C.shift.kShift_functor 1)).symm)
Tag 09QS, a lemma
Tag 09QS in the Stacks Project.
DGCategory.rotatedAssociatedTriangle_iso_connectingConeTriangle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/RotatedConeTriangle.lean, line 308.
The rotated triangle of an admissible sequence is isomorphic to the cone triangle of its desuspended connecting map.
theorem rotatedAssociatedTriangle_iso_connectingConeTriangle
(C : ConeSituation A) {x y z : A.Obj}
(E : GradedSplitShortExact (A := A) x y z) :
letI : HasShift A.K ℤ := C.shift.kShift
Nonempty (rotatedAssociatedTriangle C E ≅ connectingConeTriangle C E)
Tag 09QT, a lemma
Tag 09QT in the Stacks Project.
DGCategory.isIso_cone_of_isIso_source_target, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ConeHomotopyEquivalence.lean, line 293.
In a morphism of cone triangles, homotopy equivalences on the source and target induce a homotopy equivalence on the cones.
public theorem isIso_cone_of_isIso_source_target
(S : ConeSituation A)
{x₁ y₁ x₂ y₂ : A.Obj} (f₁ : A.Cocycle x₁ y₁) (f₂ : A.Cocycle x₂ y₂)
(φ :
letI : HasShift A.K ℤ := S.shift.kShift
coneTriangle S f₁ ⟶ coneTriangle S f₂) :
letI : HasShift A.K ℤ := S.shift.kShift
IsIso φ.hom₁ → IsIso φ.hom₂ → IsIso φ.hom₃
Tag 09QU, a lemma
Tag 09QU in the Stacks Project.
DGCategory.coneTriangleIsoOfShortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ConeTriangleComparison.lean, line 713. The attribute's comment: “part (1)”. References: SGA 4 XVII (1.1.1), “DG category setting”.
An admissible short exact sequence identifies its quotient with the cone of its first arrow, compatibly with the two triangles and the identity on their first two terms.
public theorem coneTriangleIsoOfShortExact (S : ConeSituation A)
{x y z : A.Obj} (E : GradedSplitShortExact (A := A) x y z) :
letI : HasShift A.K ℤ := S.shift.kShift
∃ φ : negativeConeTriangle S E.a ⟶ GradedSplitShortExact.associatedKTriangle S.shift E,
φ.hom₁ = 𝟙 _ ∧ φ.hom₂ = 𝟙 _ ∧ IsIso φ.hom₃
DGCategory.shortExactTriangleIsoOfFactorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ConeTriangleComparison.lean, line 864. The attribute's comment: “part (2)”. References: SGA 4 XVII (1.1.1), “DG cat. with cone situat”.
The admissible sequence in a factorization of a closed arrow gives a triangle isomorphic to the cone triangle of that arrow, by the identity on the source and the factorization's homotopy equivalence on the target.
public theorem shortExactTriangleIsoOfFactorization (S : ConeSituation A)
{x y y' z : A.Obj} (α : A.Cocycle x y)
(E : GradedSplitShortExact (A := A) x y' z)
(π : A.Cocycle y' y) (hπα : A.compCocycle π E.a = α)
(s : A.Cocycle y y')
(hπs : A.compCocycle π s = (⟨A.id y, A.d_id y⟩ : A.Cocycle y y))
(hsπ : A.Homotopic (A.compCocycle s π)
(⟨A.id y', A.d_id y'⟩ : A.Cocycle y' y')) :
letI : HasShift A.K ℤ := S.shift.kShift
∃ φ : GradedSplitShortExact.associatedKTriangle S.shift E ⟶ negativeConeTriangle S α,
φ.hom₁ = 𝟙 _ ∧
φ.hom₂ = Quotient.mk (A.homotopySetoid y' y) π ∧
IsIso φ.hom₃
Tag 09QW, a lemma
Tag 09QW in the Stacks Project.
DGCategory.homotopyPretriangulated, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/HomotopyCategoryTriangulated.lean, line 1406. The attribute's comment: “the pre-triangulated structure”. References: SGA 4½ Etat 0 (1.2.2), “TR1, TR2, TR3”.
The homotopy category with the triangles of admissible short exact sequences as its distinguished triangles is pretriangulated.
public noncomputable def homotopyPretriangulated :
letI : Preadditive A.K := homotopyPreadditive A
letI : HasZeroObject A.K := homotopyHasZeroObject A T
letI : HasShift A.K ℤ := T.shift.kShift
letI : ∀ n : ℤ, (shiftFunctor A.K n).Additive := fun n => homotopyShiftAdditive A T n
Pretriangulated A.K
DGCategory.distinguishedTriangles_homotopyPretriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/HomotopyCategoryTriangulated.lean, line 1417. The attribute's comment: “its distinguished triangles”. References: SGA 4½ Etat 0 (1.2.2), “more general”.
The distinguished triangles of the pretriangulated structure on
K(A)are exactly the triangles isomorphic to that of an admissible short exact sequence.
public theorem distinguishedTriangles_homotopyPretriangulated :
letI : Preadditive A.K := homotopyPreadditive A
letI : HasZeroObject A.K := homotopyHasZeroObject A T
letI : HasShift A.K ℤ := T.shift.kShift
letI : ∀ n : ℤ, (shiftFunctor A.K n).Additive := fun n => homotopyShiftAdditive A T n
(homotopyPretriangulated A T).distinguishedTriangles =
{U | IsDistinguishedTriangle A T U}
Tag 09QX, a lemma
Tag 09QX in the Stacks Project.
DGCategory.admissibleMonomorphisms_octahedron, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/Octahedron.lean, line 761.
The octahedral diagram associated to two composable admissible monomorphisms. The input exact sequences witness admissibility and fix the two quotient objects.
theorem admissibleMonomorphisms_octahedron
(S : ConeSituation A)
{x y z q₁ q₃ : A.Obj}
(E₁ : GradedSplitShortExact (A := A) x y q₁)
(E₃ : GradedSplitShortExact (A := A) y z q₃) :
letI : HasShift A.K ℤ := S.shift.kShift
let T₁ := GradedSplitShortExact.associatedKTriangle S.shift E₁
let T₃ := GradedSplitShortExact.associatedKTriangle S.shift E₃
∃ (q₂ : A.Obj)
(E₂ : GradedSplitShortExact (A := A) x z q₂)
(E₄ : GradedSplitShortExact (A := A) q₁ q₂ q₃),
let T₂ := GradedSplitShortExact.associatedKTriangle S.shift E₂
let T₄ := GradedSplitShortExact.associatedKTriangle S.shift E₄
(E₂.a.1 = A.comp (by rfl : (0 : ℤ) + 0 = 0) E₃.a.1 E₁.a.1) ∧
(T₁.mor₁ ≫ T₃.mor₁ = T₂.mor₁) ∧
(T₁.mor₂ ≫ T₄.mor₁ = T₃.mor₁ ≫ T₂.mor₂) ∧
(T₄.mor₁ ≫ T₂.mor₃ = T₁.mor₃) ∧
(T₂.mor₂ ≫ T₄.mor₂ = T₃.mor₂) ∧
(T₂.mor₃ ≫ T₁.mor₁⟦1⟧' = T₄.mor₂ ≫ T₃.mor₃) ∧
(T₄.mor₃ = T₃.mor₃ ≫ T₁.mor₂⟦1⟧')
Tag 09QY, a proposition
Tag 09QY in the Stacks Project.
DGCategory.homotopyCategory_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/HomotopyCategoryTriangulated.lean, line 1431. References: SGA 4½ Etat 0 (1.2.2); SGA 4 Vbis (2.5.1), “more general”.
The homotopy category of a differential graded category satisfying axioms (A), (B) and (C), with the translation functors of axiom (B) and the triangles of admissible short exact sequences as distinguished triangles, is a triangulated category.
public theorem homotopyCategory_isTriangulated :
letI : Preadditive A.K := homotopyPreadditive A
letI : HasZeroObject A.K := homotopyHasZeroObject A T
letI : HasShift A.K ℤ := T.shift.kShift
letI : ∀ n : ℤ, (shiftFunctor A.K n).Additive := fun n => homotopyShiftAdditive A T n
letI : Pretriangulated A.K := homotopyPretriangulated A T
IsTriangulated A.K
Tag 0FQF, a lemma
Tag 0FQF in the Stacks Project.
SheafOfModules.DifferentialGradedModule.isTriangulated_onK, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/DifferentialGradedCrossSiteExact.lean, line 149. The attribute's comment: “the induced functor on homotopy categories is exact, across two ringed sites”.
A differential graded functor across two ringed sites commuting with the shift is exact on the homotopy categories, which is [Stacks, Tag 0FQF] in the generality the derived pullback and the derived pushforward of a sheaf of differential graded modules need. The triangulated structures are the ones of [Stacks, Tag 0FS7]: restriction of scalars to
ℤchanges neither the homotopy categories, nor their cones, nor their admissible short exact sequences, so the cone situation here is the one that puts the triangulated structure onK(Mod(A, d)).
theorem isTriangulated_onK
{F : DGCategory.DGFunctor (dgCategoryOverInt.{u, v, w} A) (dgCategoryOverInt.{u, v, w} B)}
(hF : F.CommShiftB (coneSituationOverInt.{u, v, w} A).shift
(coneSituationOverInt.{u, v, w} B).shift) :
letI : Preadditive (dgCategoryOverInt.{u, v, w} A).K :=
DGCategory.homotopyPreadditive _
letI : HasZeroObject (dgCategoryOverInt.{u, v, w} A).K :=
DGCategory.homotopyHasZeroObject _ (coneSituationOverInt.{u, v, w} A)
letI : HasShift (dgCategoryOverInt.{u, v, w} A).K ℤ :=
(coneSituationOverInt.{u, v, w} A).shift.kShift
letI : ∀ n : ℤ, (shiftFunctor (dgCategoryOverInt.{u, v, w} A).K n).Additive := fun n =>
DGCategory.homotopyShiftAdditive _ (coneSituationOverInt.{u, v, w} A) n
letI : Pretriangulated (dgCategoryOverInt.{u, v, w} A).K :=
DGCategory.homotopyPretriangulated _ (coneSituationOverInt.{u, v, w} A)
letI : Preadditive (dgCategoryOverInt.{u, v, w} B).K :=
DGCategory.homotopyPreadditive _
letI : HasZeroObject (dgCategoryOverInt.{u, v, w} B).K :=
DGCategory.homotopyHasZeroObject _ (coneSituationOverInt.{u, v, w} B)
letI : HasShift (dgCategoryOverInt.{u, v, w} B).K ℤ :=
(coneSituationOverInt.{u, v, w} B).shift.kShift
letI : ∀ n : ℤ, (shiftFunctor (dgCategoryOverInt.{u, v, w} B).K n).Additive := fun n =>
DGCategory.homotopyShiftAdditive _ (coneSituationOverInt.{u, v, w} B) n
letI : Pretriangulated (dgCategoryOverInt.{u, v, w} B).K :=
DGCategory.homotopyPretriangulated _ (coneSituationOverInt.{u, v, w} B)
letI : F.onK.CommShift ℤ := commShift_onK A B hF
F.onK.IsTriangulated
DGCategory.DGFunctor.CommShiftB.isDistinguishedTriangle_mapTriangleK, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ExactFunctor.lean, line 427. The attribute's comment: “distinguished triangles are carried to distinguished triangles”.
Tag 0FQF. The functor induced by
Fon homotopy categories carries the distinguished triangles ofK(A)to the distinguished triangles ofK(B), the third arrow of the image triangle being formed with the comparison isomorphismF(x[1]) = F(x)[1].
theorem isDistinguishedTriangle_mapTriangleK (CA : ConeSituation A) (CB : ConeSituation B)
(hF : F.CommShiftB CA.shift CB.shift) :
letI : HasShift A.K ℤ := CA.shift.kShift
letI : HasShift B.K ℤ := CB.shift.kShift
∀ T : Pretriangulated.Triangle A.K, IsDistinguishedTriangle A CA T →
IsDistinguishedTriangle B CB (hF.mapTriangleK.obj T)
DGCategory.DGFunctor.CommShiftK.commShift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ExactFunctor.lean, line 523. The attribute's comment: “the induced functor commutes with the translations”.
Tag 0FQF. The induced functor
K(A) ⥤ K(B)commutes with the translation functors.
def commShift (hF : F.CommShiftK SA SB) :
letI : HasShift A.K ℤ := SA.kShift
letI : HasShift B.K ℤ := SB.kShift
F.onK.CommShift ℤ
DGCategory.DGFunctor.CommShiftK.isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ExactFunctor.lean, line 544. The attribute's comment: “the induced functor on homotopy categories is exact, from the translation coherences as data”. References: SGA 4 Vbis (2.5.1), “more general”.
Tag 0FQF. A functor
F : A ⥤ Bof differential graded categories overRbetween categories satisfying axioms (A), (B) and (C), which commutes with the shift, induces an exact functorK(A) ⥤ K(B)of triangulated categories.The commutation is asked for here as a
CommShiftK, that is, together with the two coherences of the comparison isomorphisms with theℤ-action data of the translations. Under the source's hypothesisF(x[1]) = F(x)[1]alone those two areDGCategory.DGFunctor.CommShiftK.ofCommShiftBaway, as soon as the translations of the homotopy categories are strict;DGCategory.DGFunctor.CommShiftB.isTriangulatedis that form.
theorem isTriangulated (CA : ConeSituation A) (CB : ConeSituation B)
(hF : F.CommShiftK CA.shift CB.shift) :
letI : Preadditive A.K := homotopyPreadditive A
letI : HasZeroObject A.K := homotopyHasZeroObject A CA
letI : HasShift A.K ℤ := CA.shift.kShift
letI : ∀ n : ℤ, (shiftFunctor A.K n).Additive := fun n => homotopyShiftAdditive A CA n
letI : Pretriangulated A.K := homotopyPretriangulated A CA
letI : Preadditive B.K := homotopyPreadditive B
letI : HasZeroObject B.K := homotopyHasZeroObject B CB
letI : HasShift B.K ℤ := CB.shift.kShift
letI : ∀ n : ℤ, (shiftFunctor B.K n).Additive := fun n => homotopyShiftAdditive B CB n
letI : Pretriangulated B.K := homotopyPretriangulated B CB
letI : F.onK.CommShift ℤ := hF.commShift
F.onK.IsTriangulated
DGCategory.DGFunctor.CommShiftB.isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ExactFunctor.lean, line 580. The attribute's comment: “the induced functor on homotopy categories is exact, from F(x[1]) = F(x)[1]”. References: SGA 4 Vbis (2.5.1), “more general”.
Tag 0FQF. A functor
F : A ⥤ Bof differential graded categories overRbetween categories satisfying axioms (A), (B) and (C) and such thatF(x[1]) = F(x)[1]induces an exact functorK(A) ⥤ K(B)of triangulated categories.The hypothesis on
Fis exactly the source's, namelyCommShiftB; what is assumed besides is not aboutFbut about the two axiom (B) data, namely that the translations they put on the homotopy categories are the strict ones of the source (DGCategory.ShiftAxiomB.IsStrictKShift). That is what makes the two coherences ofDGCategory.DGFunctor.CommShiftK— the agreement of the comparison isomorphisms withshiftFunctorZeroandshiftFunctorAdd, which Mathlib'sFunctor.CommShiftdemands and whichF(x[1]) = F(x)[1]does not imply for an arbitrary translation — available, byDGCategory.DGFunctor.CommShiftK.ofCommShiftB.
theorem isTriangulated (CA : ConeSituation A) (CB : ConeSituation B)
(hA : CA.shift.IsStrictKShift) (hB : CB.shift.IsStrictKShift)
(hF : F.CommShiftB CA.shift CB.shift) :
letI : Preadditive A.K := homotopyPreadditive A
letI : HasZeroObject A.K := homotopyHasZeroObject A CA
letI : HasShift A.K ℤ := CA.shift.kShift
letI : ∀ n : ℤ, (shiftFunctor A.K n).Additive := fun n => homotopyShiftAdditive A CA n
letI : Pretriangulated A.K := homotopyPretriangulated A CA
letI : Preadditive B.K := homotopyPreadditive B
letI : HasZeroObject B.K := homotopyHasZeroObject B CB
letI : HasShift B.K ℤ := CB.shift.kShift
letI : ∀ n : ℤ, (shiftFunctor B.K n).Additive := fun n => homotopyShiftAdditive B CB n
letI : Pretriangulated B.K := homotopyPretriangulated B CB
letI : F.onK.CommShift ℤ := (CommShiftK.ofCommShiftB hF hA hB).commShift
F.onK.IsTriangulated
DGCategory.DGFunctor.CommShiftB.isTriangulated_strictify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/ExactFunctor.lean, line 637. The attribute's comment: “the induced functor on homotopy categories is exact, from F(x[1]) = F(x)[1] alone”. References: SGA 4 Vbis (2.5.1), “more general”.
Tag 0FQF, with nothing assumed but the source's hypothesis. A functor
F : A ⥤ Bof differential graded categories overRbetween categories satisfying axioms (A), (B) and (C) and such thatF(x[1]) = F(x)[1]induces an exact functorK(A) ⥤ K(B)of triangulated categories, for the triangulated structures attached to the strictifications of the two axiom bundles.Passing to the strictifications changes nothing about the differential graded categories, their shifts, their cones or the distinguished triangles of Tag 09QW: it only replaces the
HasShiftfield of axiom (B), whose functorskShift_functoralready pins down, by the one whose coherence isomorphisms are the canonical ones. So this is Tag 0FQF with no hypothesis beyond the source'sF(x[1]) = F(x)[1], andDGCategory.DGFunctor.CommShiftB.isTriangulatedis the form in which the strictness is left as a hypothesis, for a caller who already knows it of the translations in hand.
theorem isTriangulated_strictify (CA : ConeSituation A) (CB : ConeSituation B)
(hF : F.CommShiftB CA.shift CB.shift) :
letI : Preadditive A.K := homotopyPreadditive A
letI : HasZeroObject A.K := homotopyHasZeroObject A CA.strictify
letI : HasShift A.K ℤ := CA.strictify.shift.kShift
letI : ∀ n : ℤ, (shiftFunctor A.K n).Additive := fun n =>
homotopyShiftAdditive A CA.strictify n
letI : Pretriangulated A.K := homotopyPretriangulated A CA.strictify
letI : Preadditive B.K := homotopyPreadditive B
letI : HasZeroObject B.K := homotopyHasZeroObject B CB.strictify
letI : HasShift B.K ℤ := CB.strictify.shift.kShift
letI : ∀ n : ℤ, (shiftFunctor B.K n).Additive := fun n =>
homotopyShiftAdditive B CB.strictify n
letI : Pretriangulated B.K := homotopyPretriangulated B CB.strictify
letI : F.onK.CommShift ℤ := (CommShiftK.ofCommShiftB hF.strictify
CA.isStrictKShift_strictify CB.isStrictKShift_strictify).commShift
F.onK.IsTriangulated
Sources
Section22.28 Bimodules#
Section 22.28 of the Stacks Project, Tag 0FQG. 5 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0FQH, a definition
Tag 0FQH in the Stacks Project.
DifferentialGraded.Bimodule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Endomorphism/BimoduleDefs.lean, line 51. The attribute's comment: “(3): a differential graded (A, B)-bimodule, presented as in Tag 0FQI by a right differential graded B-module together with a left differential graded A-action on its underlying complex whose homogeneous multiplications are right B-linear; the grading, the differential and the two Leibniz rules are those of the right module and of the left action. Its underlying graded bimodule, part (2), is DifferentialGraded.Bimodule.toGradedBimodule”.
A differential graded
(A, B)-bimodule, presented as a right differential gradedB-module with a compatible left differential gradedA-action.
structure Bimodule
AlgebraBimodule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/GradedBimodule.lean, line 99. The attribute's comment: “(1): an (A, B)-bimodule, bundled as a carrier together with the Mathlib classes that discharge the source's clauses — Module A M and Module Bᵐᵒᵖ M (clause (a) by mul_smul, clause (c) by one_smul), SMulCommClass A Bᵐᵒᵖ M (clause (b)), and Module R M with the two IsScalarTowers (R-bilinearity of the two actions)”.
An
(A, B)-bimodule over a commutative ringR, forR-algebrasAandB: anR-moduleMwith anR-bilinear leftA-action and anR-bilinear rightB-action which commute.All of the source's clauses are discharged by the Mathlib classes listed as fields, so the only data is the carrier:
mul_smulof the two module structures is clause (a),SMulCommClassis clause (b),one_smulis clause (c), and the twoIsScalarTowerfields together with theR-module structure are theR-bilinearity of the two actions.
structure AlgebraBimodule (R : Type u) [CommRing R] (A : Type u) [Ring A] [Algebra R A]
(B : Type u) [Ring B] [Algebra R B]
GradedBimodule, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/GradedBimodule.lean, line 133. The attribute's comment: “(2): a graded (A, B)-bimodule, an AlgebraBimodule (part (1), the parent projection toAlgebraBimodule) together with a grading by R-submodules which decomposes the module and satisfies Aⁿ Mᵐ ⊆ Mⁿ⁺ᵐ and Mⁿ Bᵐ ⊆ Mⁿ⁺ᵐ”.
A graded
(A, B)-bimodule over a commutative ringR, forℤ-gradedR-algebras𝒜andℬ: an(A, B)-bimoduleMwith a gradingM = ⨁ Mⁿsuch thatAⁿ Mᵐ ⊆ Mⁿ⁺ᵐandMⁿ Bᵐ ⊆ Mⁿ⁺ᵐ.The underlying
(A, B)-bimodule of part (1) is the parent projectionGradedBimodule.toAlgebraBimodule.
structure GradedBimodule {R : Type u} [CommRing R] {A : Type u} [Ring A] [Algebra R A]
(𝒜 : ℤ → Submodule R A) [GradedAlgebra 𝒜] {B : Type u} [Ring B] [Algebra R B]
(ℬ : ℤ → Submodule R B) [GradedAlgebra ℬ] extends AlgebraBimodule R A B
DifferentialGraded.Bimodule.toGradedBimodule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/GradedBimodule.lean, line 176. The attribute's comment: “the graded (A, B)-bimodule underlying a differential graded one, which is what makes part (3) a refinement of part (2); the three parts themselves are tagged with stacks_fixed, which plain @[stacks] cannot carry on a structure”.
The graded
(A, B)-bimodule underlying a differential graded(A, B)-bimodule: the right differential gradedB-module with its grading, the leftA-action totalized from the left differential graded action, and the differential forgotten.This is what makes the three parts of [Stacks, Tag 0FQH] one definition rather than three unrelated ones: part (3),
DifferentialGraded.Bimodule, refines part (2),GradedBimodule, which in turn extends part (1),AlgebraBimodule.
noncomputable def Bimodule.toGradedBimodule (M : Bimodule.{u, u} A B) :
GradedBimodule A.grading B.grading
Tag 0FQI, a lemma
Tag 0FQI in the Stacks Project.
DifferentialGradedModule.bimoduleStructureEquivRightLinearEndomorphismHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Endomorphism/Bimodule.lean, line 82.
Compatible left differential graded actions on a fixed right differential graded
B-module correspond bijectively to homomorphisms into its rightB-linear endomorphism differential graded algebra. The specified equation makes the correspondence canonical on every homogeneous element.
noncomputable def bimoduleStructureEquivRightLinearEndomorphismHom :
{ e : BimoduleStructure A B M ≃ RightLinearEndomorphismHom A B M //
∀ (L : BimoduleStructure A B M) (n : ℤ) (a : A.grading n),
(endomorphismDGA M.toCochainComplex).cochainEquiv n
⟨(e L).1.toAlgebraHom a, (e L).1.map_grading n a a.property⟩ = L.1.action n a }
Tag 0FQJ, a lemma
Tag 0FQJ in the Stacks Project.
DifferentialGraded.Bimodule.tensorEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Endomorphism/BimoduleTensorEquivalence.lean, line 466.
A differential graded
(A, B)-bimodule is canonically a right differential graded module over the graded tensor product of the graded opposite ofAwithB, and this is an equivalence of categories.
noncomputable def tensorEquivalence : TensorEquivalence A B
Tag 0FQK, a lemma
Tag 0FQK in the Stacks Project.
DifferentialGraded.Bimodule.exists_propertyP_resolution, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Endomorphism/BimodulePropertyP.lean, line 110.
Stacks 0FQK. "Let
Rbe a ring. Let(A, d)and(B, d)be differential gradedR-algebras. LetMbe a differential graded(A, B)-bimodule. There exists a homomorphismP → Mof differential graded(A, B)-bimodules which is a quasi-isomorphism such thatPhas property (P)."Property (P) of the resolving bimodule is recorded as a property-(P) filtration of the right differential graded
Aᵒᵖ ⊗_R B-module it is by Tag 0FQJ, and being a quasi-isomorphism is Mathlib'sQuasiIsoon the cochain complex underlying the homomorphism of rightB-modules.
theorem exists_propertyP_resolution (A B : DifferentialGradedAlgebra.{u, u} R)
(M : Bimodule A B) :
∃ (P : Bimodule A B) (f : P ⟶ M),
QuasiIso ((DifferentialGradedModule.forgetToCochainComplex B).map f.rightHom) ∧
Nonempty (DifferentialGradedModule.PropertyPFiltration (toTensorModule A B P))
Tag 0FQL, a lemma
Tag 0FQL in the Stacks Project.
DifferentialGraded.Bimodule.exists_admissible_telescope, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Endomorphism/BimoduleTelescope.lean, line 117.
Stacks 0FQL. "Let
Rbe a ring. Let(A, d)and(B, d)be differential gradedR-algebras. LetPbe a differential graded(A, B)-bimodule having property (P) with corresponding filtrationF_•, then we obtain a short exact sequence0 → ⨁ F_iP → ⨁ F_iP → P → 0of differential graded(A, B)-bimodules which is split as a sequence of graded(A, B)-bimodules."Property (P) is read on the right differential graded
Aᵒᵖ ⊗_R B-module of Tag 0FQJ, and the stages of the filtration are brought back to bimodules through the same construction. The direct sum is recorded by its universal property, the second map is the sum of the inclusionsF_iP → P, and the first map is, on the summandF_iP, the identity minus the inclusionF_iP → F_{i+1}P.
theorem exists_admissible_telescope (P : Bimodule A B)
(F : DifferentialGradedModule.PropertyPFiltration (toTensorModule A B P)) :
∃ (S : Bimodule A B) (ι : ∀ i : ℕ, ofTensorModule A B (F.F i) ⟶ S) (α : S ⟶ S) (β : S ⟶ P),
(∀ (T : Bimodule A B) (g : ∀ i : ℕ, ofTensorModule A B (F.F i) ⟶ T),
∃! h : S ⟶ T, ∀ i : ℕ, ι i ≫ h = g i) ∧
(∀ (i : ℕ) (x : (F.F i).M),
β.rightHom.toFun ((ι i).rightHom.toFun x) = (F.ι i).toFun x) ∧
(∀ (i : ℕ) (x : (F.F i).M), α.rightHom.toFun ((ι i).rightHom.toFun x) =
(ι i).rightHom.toFun x - (ι (i + 1)).rightHom.toFun ((F.incl i).toFun x)) ∧
IsAdmissibleShortExact A B α β
Sources
Section22.29 Bimodules and tensor product#
Section 22.29 of the Stacks Project, Tag 0FQM. 2 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09LM, a lemma
Tag 09LM in the Stacks Project.
DifferentialGraded.Bimodule.tensorDGFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensor.lean, line 1264. The attribute's comment: “the DG functor”.
Stacks 09LM. Tensoring with a differential graded
(A, B)-bimodule is a functor of differential graded categories.
noncomputable def tensorDGFunctor (N : Bimodule A B) : TensorDGFunctorData N
DifferentialGraded.Bimodule.tensorCompFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensor.lean, line 1270. The attribute's comment: “the ordinary functor”.
Stacks 09LM. The induced functor on the categories of differential graded modules.
noncomputable abbrev tensorCompFunctor (N : Bimodule A B) :
DifferentialGradedModule A ⥤ DifferentialGradedModule B
DifferentialGraded.Bimodule.tensorHomotopyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensor.lean, line 1277. The attribute's comment: “the homotopy functor”.
Stacks 09LM. The induced functor on the homotopy categories.
noncomputable def tensorHomotopyFunctor (N : Bimodule A B) :
HomotopyCategory A ⥤ HomotopyCategory B
DifferentialGraded.Bimodule.tensorCompFunctor_quotient, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensor.lean, line 1298. The attribute's comment: “compatibility with the quotient”.
Stacks 09LM. Passing the ordinary tensor functor to homotopy classes yields the tensor functor on the homotopy categories.
noncomputable def tensorCompFunctor_quotient (N : Bimodule A B) :
(tensorCompFunctor N ⋙ toHomotopyCategory B) ≅
(toHomotopyCategory A ⋙ tensorHomotopyFunctor N)
Tag 0FQN, a remark
Tag 0FQN in the Stacks Project.
DifferentialGraded.Bimodule.tensorShiftIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensorShift.lean, line 229.
Stacks 0FQN. The canonical, sign-free identification
(M ⊗_A N)[k] ≅ M[k] ⊗_A N: it sends each pure tensor to the same pure tensor.
noncomputable def tensorShiftIso (N : Bimodule A B) (M : DifferentialGradedModule A) (k : ℤ) :
{ e : shift ((tensorDGFunctor N).functor.obj M) k ≅
(tensorDGFunctor N).functor.obj (shift M k) //
∀ (x : M.M) (y : N.rightModule.M),
e.hom.toFun (((tensorDGFunctor N).pure M).toLinearMap x y) =
((tensorDGFunctor N).pure (shift M k)).toLinearMap x y }
Sources
Section22.30 Bimodules and internal hom#
Section 22.30 of the Stacks Project, Tag 0FQP. 3 tags here are carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0FQQ, a lemma
Tag 0FQQ in the Stacks Project.
DifferentialGradedModule.homHomotopyDescent, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 561. The attribute's comment: “descent of the functor on DG modules”.
The internal hom functor on homotopy categories is the descent of the internal hom functor on differential graded modules: both send
Pto the chosen presentation ofHom^•_B(N, P)and a homotopy class to the class of the postcomposition.
def homHomotopyDescent (N : DifferentialGradedModule B) (L : BimoduleStructure A B N) :
toHomotopyCategory B ⋙ homHomotopyCategoryFunctor A B N L ≅
homModuleFunctor A B N L ⋙ toHomotopyCategory A
DifferentialGradedModule.homDGFunctorData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/InternalHomFunctor.lean, line 315. The attribute's comment: “the DG functor”.
Stacks 0FQQ. The internal hom functor of a differential graded bimodule, as a functor of differential graded categories.
noncomputable def homDGFunctorData : HomDGFunctorData A B N L
DifferentialGradedModule.homModuleFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/InternalHomFunctor.lean, line 477. The attribute's comment: “the functor on DG modules”.
Stacks 0FQQ. The internal hom functor on the categories of differential graded modules.
noncomputable def homModuleFunctor :
DifferentialGradedModule B ⥤ DifferentialGradedModule A
DifferentialGradedModule.homHomotopyCategoryFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/InternalHomFunctor.lean, line 485. The attribute's comment: “the functor on homotopy categories”.
Stacks 0FQQ. The internal hom functor on the homotopy categories of differential graded modules.
noncomputable def homHomotopyCategoryFunctor :
HomotopyCategory B ⥤ HomotopyCategory A
Tag 0FQR, a remark
Tag 0FQR in the Stacks Project.
DifferentialGradedModule.shiftHomIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/BimoduleHomShift.lean, line 1116.
The canonical, sign-free isomorphism
Hom_B^gr(N,P)[k] ≅ Hom_B^gr(N,P[k])of right DGA-modules. The equality says that the associated homogeneous maps have the same value on each homogeneous element ofN.
public theorem shiftHomIso (k : ℤ) :
∃ (H : HomDGModulePresentation A B N P L)
(Hk : HomDGModulePresentation A B N (DifferentialGradedModule.shift P k) L)
(e : DifferentialGradedModule.shift H.module k ≅ Hk.module),
∀ (n p : ℤ) (f : (DifferentialGradedModule.shift H.module k).grading n)
(x : N.grading p),
((Hk.homogeneousEquiv n (e.hom.gradedMap n f)).1 x : P.M) =
(H.homogeneousEquiv (n + k)
⟨(f.1 : H.module.M), by
simpa only [DifferentialGradedModule.shift_grading] using f.property⟩).1 x
DifferentialGradedModule.shiftHomModuleIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/InternalHom.lean, line 515.
Stacks 0FQR. The canonical, sign-free isomorphism
Hom^•_B(N, P)[k] ≅ Hom^•_B(N, P[k])of right differential gradedA-modules. The displayed equation says that the homogeneous maps associated with corresponding elements take the same value on every homogeneous element ofN.
theorem shiftHomModuleIso (k : ℤ) :
∃ (H : HomModuleData A B N P L)
(Hk : HomModuleData A B N (shift P k) L)
(e : shift H.module k ≅ Hk.module),
∀ (n p : ℤ) (f : (shift H.module k).grading n) (x : N.grading p),
((Hk.homogeneousEquiv n (e.hom.gradedMap n f)).1 x : P.M) =
(H.homogeneousEquiv (n + k)
⟨(f.1 : H.module.M), by
simpa only [shift_grading] using f.property⟩).1 x
Tag 09LN, a lemma
Tag 09LN in the Stacks Project.
Bimod.tensorHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Bimod/TensorHom.lean, line 132. The attribute's comment: “ordinary_tensor_hom”. References: SGA 4 IV (12.14), “punctual topos”.
Stacks 09LN, ordinary tensor--hom. For a right
A-moduleM, an(A,B)-bimoduleN, and a rightB-moduleP,B-linear maps fromM ⊗_A NtoPare canonically the same asA-balanced maps fromMinto theB-linear maps fromNtoP.
public noncomputable def tensorHomEquiv {A B : Mon (ModuleCat.{u} R)}
(M : Bimod (𝟙_ (Mon (ModuleCat.{u} R))) A) (N : Bimod A B)
(P : Bimod (𝟙_ (Mon (ModuleCat.{u} R))) B) :
rightLinearMaps (M.tensorBimod N) P ≃ₗ[R] balancedRightLinearMaps M N P
Bimod.tensorHomEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Bimod/TensorHom.lean, line 254. The attribute's comment: “ordinary_tensor_hom”.
The forward tensor-hom correspondence is evaluation on pure tensors.
public theorem tensorHomEquiv_apply {A B : Mon (ModuleCat.{u} R)}
(M : Bimod (𝟙_ (Mon (ModuleCat.{u} R))) A) (N : Bimod A B)
(P : Bimod (𝟙_ (Mon (ModuleCat.{u} R))) B)
(f : rightLinearMaps (M.tensorBimod N) P) (m : M.X) (n : N.X) :
(tensorHomEquiv M N P f).1 m n =
f.1 (CategoryTheory.Limits.coequalizer.π
(M.actRight ▷ N.X) ((α_ M.X A.X N.X).hom ≫ (M.X ◁ N.actLeft)) |>.hom
(m ⊗ₜ[R] n))
DifferentialGraded.Bimodule.tensorCompFunctor_adj_homModuleFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensorHom.lean, line 535. The attribute's comment: “the differential graded case in degree zero”.
Stacks 09LN, the differential graded case. Tensoring with a differential graded
(A, B)-bimoduleNis left adjoint to the internal hom out ofN, as functors between the categories of differential graded modules:Hom_{Mod^{dg}_{(B,d)}}(M ⊗_A N, P) = Hom_{Mod^{dg}_{(A,d)}}(M, Hom^•_B(N, P)), naturally inMandP.This is the degree-zero part of the source's isomorphism of Hom complexes — the bijection of the morphism groups of the two categories of differential graded modules — which is why the tag is part-qualified.
def tensorCompFunctor_adj_homModuleFunctor (N : Bimodule A B) :
tensorCompFunctor N ⊣ homModuleFunctor A B N.rightModule N.leftAction
DifferentialGraded.Bimodule.tensorHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensorHom.lean, line 550. The attribute's comment: “the differential graded case in degree zero, as a bijection”.
Stacks 09LN, the differential graded case, as the bijection of morphism groups
Hom_{Mod^{dg}_{(B,d)}}(M ⊗_A N, P) = Hom_{Mod^{dg}_{(A,d)}}(M, Hom^•_B(N, P)). It is natural inMandP, being the hom-set bijection ofDifferentialGraded.Bimodule.tensorCompFunctor_adj_homModuleFunctor.
def tensorHomEquiv (N : Bimodule A B) (M : DifferentialGradedModule A)
(P : DifferentialGradedModule B) :
((tensorCompFunctor N).obj M ⟶ P) ≃
(M ⟶ (homModuleFunctor A B N.rightModule N.leftAction).obj P)
DifferentialGraded.Bimodule.tensorHomotopyFunctor_adj_homHomotopyCategoryFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensorHom.lean, line 569. The attribute's comment: “the differential graded case in degree zero, on the homotopy categories”. References: SGA 5 IIIB (5.2), “partial”.
Stacks 09LN for differential graded modules, on the homotopy categories. Tensoring with a differential graded
(A, B)-bimoduleNis left adjoint to the internal hom out ofNas functorsK(A, d) ⥤ K(B, d)andK(B, d) ⥤ K(A, d).This is the adjunction on the categories of differential graded modules, descended along the passage to homotopy classes: both functors are compatible with it, by Tag 09LM (
DifferentialGraded.Bimodule.tensorCompFunctor_quotient) and Tag 0FQQ (DifferentialGradedModule.homHomotopyDescent), and an adjunction descends to a quotient category byCategoryTheory.Quotient.adjunctionOfSquares.
def tensorHomotopyFunctor_adj_homHomotopyCategoryFunctor (N : Bimodule A B) :
tensorHomotopyFunctor N ⊣ homHomotopyCategoryFunctor A B N.rightModule N.leftAction
DifferentialGraded.Bimodule.exists_tensorHomComplexIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensorHom.lean, line 981. The attribute's comment: “the differential graded case in every degree, as an isomorphism of Hom complexes”.
Stacks 09LN, in every degree. For a right differential graded
A-moduleM, a differential graded(A, B)-bimoduleNand a right differential gradedB-modulePthe two Hom complexes
Hom^•_{Mod^{dg}_{(B, d)}}(M ⊗_A N, P)andHom^•_{Mod^{dg}_{(A, d)}}(M, Hom^•_B(N, P))are isomorphic as complexes of
R-modules: in each degreenthe homogeneous right-B-linear mapsM ⊗_A N → Pof degreencorrespondR-linearly to the homogeneous right-A-linear mapsM → Hom^•_B(N, P)of degreen, by restriction to the pure tensors, and the correspondence commutes with the differentials of the two Hom complexes.The correspondence is pinned by its value on pure tensors, which is what the first displayed property says: the homogeneous map that the image of
ψat a homogeneousxpresents sendsytoψ (x ⊗ y). That property determines it, since the pure tensors generateM ⊗_A N.The degree-zero part is
DifferentialGraded.Bimodule.tensorHomEquiv, which is the bijection of morphism groups of the two categories of differential graded modules; the statement here is the isomorphism of Hom complexes that the source asserts, of which that bijection is the part given by the closed elements of degree zero.
theorem exists_tensorHomComplexIso (N : Bimodule A B) (M : DifferentialGradedModule A)
(P : DifferentialGradedModule B) :
∃ e : ∀ n : ℤ, HomogeneousMap B (tensorObj N M) P n ≃ₗ[R]
HomogeneousMap A M (homPresentation N P).module n,
(∀ (n p : ℤ) (ψ : HomogeneousMap B (tensorObj N M) P n) (x : M.M)
(hx : x ∈ M.grading p) (y : N.rightModule.M),
((homPresentation N P).homogeneousEquiv (p + n)
⟨(e n ψ).1 x, (e n ψ).2.1 p x hx⟩).1 y =
ψ.1 (((tensorDGFunctor N).pure M).toLinearMap x y)) ∧
∀ (n : ℤ) (ψ : HomogeneousMap B (tensorObj N M) P n),
e (n + 1) (homogeneousMapDifferential B ψ) =
homogeneousMapDifferential A (e n ψ)
Sources
Section22.31 Derived Hom#
Section 22.31 of the Stacks Project, Tag 09LF. 6 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09LG, an equation
Tag 09LG in the Stacks Project.
DifferentialGradedModule.homModuleFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/InternalHomFunctor.lean, line 477. The attribute's comment: “the induced functor Mod_(B,d) → Mod_(A,d)”.
Stacks 0FQQ. The internal hom functor on the categories of differential graded modules.
noncomputable def homModuleFunctor :
DifferentialGradedModule B ⥤ DifferentialGradedModule A
Tag 09LH, a lemma
Tag 09LH in the Stacks Project.
DifferentialGradedModule.homHomotopyCategoryFunctor_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/InternalHomCommShift.lean, line 577.
Stacks 09LH. The internal hom functor out of a differential graded bimodule is an exact functor of the homotopy categories, for the commutation with the translation of Tag 0FQR.
instance homHomotopyCategoryFunctor_isTriangulated :
(homHomotopyCategoryFunctor A B N L).IsTriangulated
Tag 09LI, a lemma
Tag 09LI in the Stacks Project.
DifferentialGradedModule.derivedHomData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomFunctor.lean, line 223.
Stacks 09LI. The right derived functor of
Fexists; we denote itRHom(N, -) : D(B, d) ⥤ D(A, d). HereFis internal Hom out of the differential graded(A, B)-bimoduleNread on homotopy categories and followed by localization (DifferentialGradedModule.homToDerivedCategory), and a right derived functor of it, with its comparison map and the everywhere-definedness of Tag 05SV, is exactly aDifferentialGradedModule.DerivedHomData; so the source's assertion that the derived functor exists is the construction of one such datum, which this is.It is
DifferentialGradedModule.DerivedHomData.ofPropertyIResolutions— the Stacks proof, Tag 06XN applied to the modules with property (I), whose orthogonality to the acyclic modules is Tag 09KS — fed the existence of the resolutions, Tag 09KU (DifferentialGradedModule.exists_propertyI_resolution). Nothing is assumed.The functor is determined by this up to the canonical isomorphism
DifferentialGradedModule.DerivedHomData.functorIso, so a consumer that only needs someRHom(N, -)should take an arbitrary datum rather than this one.
def derivedHomData (A B : DifferentialGradedAlgebra R) (N : DifferentialGradedModule B)
(L : BimoduleStructure A B N) : DerivedHomData A B N L
Tag 0BYV, a lemma
Tag 0BYV in the Stacks Project.
DifferentialGraded.Bimodule.derivedPrecomp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomPrecomposition.lean, line 114. The attribute's comment: “the natural transformation”.
Precomposition with a homomorphism
f : M ⟶ Nof differential graded(A, B)-bimodules induces a natural transformationRHom(N, -) ⟹ RHom(M, -)of derived Hom functorsD(B, d) ⥤ D(A, d).
def derivedPrecomp (f : M ⟶ N) : DN.functor ⟶ DM.functor
DifferentialGraded.Bimodule.derivedPrecomp_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomPrecomposition.lean, line 122. The attribute's comment: “compatibility with the comparison maps”.
The derived transformation is compatible with the canonical comparison maps from ordinary internal hom to derived Hom.
theorem derivedPrecomp_comparison (f : M ⟶ N) :
DN.comparison ≫
Functor.whiskerLeft (quasiIsomorphisms' B).Q (derivedPrecomp DN DM f) =
precompToDerivedNatTrans f ≫ DM.comparison
DifferentialGraded.Bimodule.derivedPrecomp_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomPrecompositionIso.lean, line 141. The attribute's comment: “quasi-isomorphisms induce natural isomorphisms”.
Stacks 0BYV, the last assertion. If a homomorphism
f : M ⟶ Nof differential graded(A, B)-bimodules is a quasi-isomorphism of the underlying right differential gradedB-modules, then the induced transformationRHom(N, -) ⟹ RHom(M, -)of derived Hom functors is an isomorphism.Nothing is assumed:
DNandDMrange over all right derived functors of internal Hom out of the two bimodules, of which the ones of Tag 09LI (DifferentialGradedModule.derivedHomData) are instances.
theorem derivedPrecomp_isIso
(DN : DerivedHomData A B N.rightModule N.leftAction)
(DM : DerivedHomData A B M.rightModule M.leftAction)
(f : M ⟶ N) (hf : QuasiIso ((forgetToCochainComplex B).map f.rightHom)) :
IsIso (derivedPrecomp DN DM f)
Tag 0CS5, a lemma
Tag 0CS5 in the Stacks Project.
DifferentialGradedModule.extIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomExtIso.lean, line 161. The attribute's comment: “the identification of the cohomology of derived Hom with Ext”.
Degree-
ncohomology of derived Hom out ofNisExt^n_{D(B,d)}(N, -) = Hom_{D(B,d)}(N, (-)[n]), as functors onD(B, d).
def extIso (D : DerivedHomData A B N L) (n : ℤ) :
D.functor ⋙ extCohomologyFunctor A n ≅ extFunctor B N n
DifferentialGradedModule.extLinearEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomExtIso.lean, line 225. The attribute's comment: “the identification is natural in the target”.
The identification
DifferentialGradedModule.extLinearEquivis natural in the target: a cohomology class of derived Hom pushed forward alonggis sent to theExt-class followed by then-shift ofg.
theorem extLinearEquiv_naturality (D : DerivedHomData A B N L) (n : ℤ)
{M M' : derivedCategory' B} (g : M ⟶ M')
(x : (degreeZeroCohomologyOnLocalization' A).obj ((D.functor.obj M)⟦n⟧)) :
extLinearEquiv A B N L D n M'
((degreeZeroCohomologyOnLocalization' A).map ((D.functor.map g)⟦n⟧') x) =
extLinearEquiv A B N L D n M x ≫ g⟦n⟧'
DifferentialGraded.Bimodule.extLinearEquiv_derivedPrecomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomExtIsoPrecomp.lean, line 374. The attribute's comment: “the identification is natural in the bimodule, with respect to Tag 0BYV”.
Stacks 0CS5, the clause asserting compatibility with Tag 0BYV. For a homomorphism
f : M ⟶ Nof differential graded(A, B)-bimodules, the identification of Tag 0CS5 carries the pullback alongfof a degree-ncohomology class of derived Hom out ofN— the transformation of Tag 0BYV,DifferentialGraded.Bimodule.derivedPrecomp— to theExt-class ofNcomposed with the image offinD(B, d).Together with
DifferentialGradedModule.extIsoandDifferentialGradedModule.extLinearEquiv_naturalitythis completes Tag 0CS5.
theorem extLinearEquiv_derivedPrecomp (DN : DerivedHomData A B N.rightModule N.leftAction)
(DM : DerivedHomData A B M.rightModule M.leftAction) (f : M ⟶ N) (n : ℤ)
(P : derivedCategory' B)
(x : (degreeZeroCohomologyOnLocalization' A).obj ((DN.functor.obj P)⟦n⟧)) :
extLinearEquiv A B M.rightModule M.leftAction DM n P
((degreeZeroCohomologyOnLocalization' A).map
(((derivedPrecomp DN DM f).app P)⟦n⟧') x) =
(quasiIsomorphisms' B).Q.map ((toHomotopyCategory B).map f.rightHom) ≫
extLinearEquiv A B N.rightModule N.leftAction DN n P x
DifferentialGradedModule.General.homComplexExtEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/HomComplexExtGeneral.lean, line 437. The attribute's comment: “the cohomology of ordinary differential graded Hom is Ext out of a module orthogonal to the acyclics, at independent universes”.
H^n(Hom^•_{(A, d)}(L, M)) = Ext^n_{D(A, d)}(L, M), at independent universes, forLorthogonal on the left to the acyclic modules.This is the content that Tag 0CS5 and Tag 0BYW together provide, in the form Tag 0CS6 asks for: Tag 09LC identifies the cohomology of the Hom complex with the morphism groups of
K(A, d)(DifferentialGradedModule.General.homComplexHomologyEquiv), and the localization functor is bijective on the morphisms out of a left-orthogonal object (DifferentialGradedModule.General.bijective_q_map_of_leftOrthogonal), which is the mechanism of Tag 09KY; the shift is moved across the localization by its commutation with the translation.With
Ext^n_{D(A, d)}(L, M) = Hom_{D(A, d)}(L, M[n]), as everywhere in Tag 0CS6, the right-hand side is thatExt-group.
def homComplexExtEquiv (n : ℤ)
(hL : (acyclic.{u, v, w} A).leftOrthogonal ((toHomotopyCategory A).obj L)) :
↥((homComplex A L M).homology n) ≃+
((quasiIsomorphisms.{u, v, w} A).Q.obj ((toHomotopyCategory A).obj L) ⟶
((quasiIsomorphisms.{u, v, w} A).Q.obj ((toHomotopyCategory A).obj M))⟦n⟧)
Tag 0BYW, a lemma
Tag 0BYW in the Stacks Project.
DifferentialGradedModule.DerivedHomData.isIso_comparison_of_bijective_q_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomLeftOrthogonal.lean, line 217. The attribute's comment: “the comparison under the Hom hypothesis”.
If
Hom_{D(B,d)}(N, N') = Hom_{K(Mod_{(B,d)})}(N, N')for allN' ∈ K(B, d), thenRHom(N, M) = Hom_{Mod^{dg}_{(B,d)}}(N, M)functorially inMinD(B, d).The equality of morphism modules is the hypothesis
hN, that the localizationQ : K(B, d) ⥤ D(B, d)is bijective on the morphisms out ofN. The functorial equality of the conclusion is the invertibility of the comparison natural transformation of Tag 09LI, from ordinary differential graded Hom out ofNread inD(A, d)to derived Hom precomposed with the localization;DifferentialGradedModule.DerivedHomData.comparisonNatIsois the resulting isomorphism of functors.Under the hypothesis the functor being derived already inverts the quasi-isomorphisms (
DifferentialGradedModule.isInvertedBy_homToDerivedCategory_of_bijective_q_map), and the comparison of any right derived functor of a functor that inverts them is invertible.
theorem isIso_comparison_of_bijective_q_map (D : DerivedHomData A B N L)
(hN : ∀ P : HomotopyCategory B, Function.Bijective
((quasiIsomorphisms' B).Q.map : ((toHomotopyCategory B).obj N ⟶ P) → _)) :
IsIso D.comparison
DifferentialGradedModule.DerivedHomData.isIso_comparison_of_propertyP, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomLeftOrthogonal.lean, line 232. The attribute's comment: “the property-(P) sufficient condition”.
A differential graded
(A, B)-bimodule whose underlyingB-module has property (P) computes derived Hom by ordinary differential graded Hom, canonically and naturally in the second argument.A module with property (P) is orthogonal on the left to the acyclic modules, which is Tag 09KM, and the localization is bijective on the morphisms out of such a module, which is the mechanism of Tag 09KY; so the hypothesis of the previous statement holds.
theorem isIso_comparison_of_propertyP (D : DerivedHomData A B N L)
(hN : Nonempty (PropertyPFiltration N)) :
IsIso D.comparison
DifferentialGradedModule.DerivedHomData.comparisonNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomLeftOrthogonal.lean, line 242. The attribute's comment: “as an identification of functors”.
RHom(N, -) = Hom_{Mod^{dg}_{(B,d)}}(N, -)as functors. Ordinary differential graded Hom out ofN, read inD(A, d), is derived Hom out ofNprecomposed with the localization, by the comparison map of Tag 09LI and naturally in the second argument.
def comparisonNatIso (D : DerivedHomData A B N L)
(hN : ∀ P : HomotopyCategory B, Function.Bijective
((quasiIsomorphisms' B).Q.map : ((toHomotopyCategory B).obj N ⟶ P) → _)) :
homToDerivedCategory A B N L ≅ (quasiIsomorphisms' B).Q ⋙ D.functor
DifferentialGradedModule.General.homComplexExtEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/HomComplexExtGeneral.lean, line 437. The attribute's comment: “ordinary differential graded Hom out of a left-orthogonal module computes derived Hom, read on cohomology, at independent universes”.
H^n(Hom^•_{(A, d)}(L, M)) = Ext^n_{D(A, d)}(L, M), at independent universes, forLorthogonal on the left to the acyclic modules.This is the content that Tag 0CS5 and Tag 0BYW together provide, in the form Tag 0CS6 asks for: Tag 09LC identifies the cohomology of the Hom complex with the morphism groups of
K(A, d)(DifferentialGradedModule.General.homComplexHomologyEquiv), and the localization functor is bijective on the morphisms out of a left-orthogonal object (DifferentialGradedModule.General.bijective_q_map_of_leftOrthogonal), which is the mechanism of Tag 09KY; the shift is moved across the localization by its commutation with the translation.With
Ext^n_{D(A, d)}(L, M) = Hom_{D(A, d)}(L, M[n]), as everywhere in Tag 0CS6, the right-hand side is thatExt-group.
def homComplexExtEquiv (n : ℤ)
(hL : (acyclic.{u, v, w} A).leftOrthogonal ((toHomotopyCategory A).obj L)) :
↥((homComplex A L M).homology n) ≃+
((quasiIsomorphisms.{u, v, w} A).Q.obj ((toHomotopyCategory A).obj L) ⟶
((quasiIsomorphisms.{u, v, w} A).Q.obj ((toHomotopyCategory A).obj M))⟦n⟧)
DifferentialGradedModule.General.homComplexExtEquivOfPropertyP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/HomComplexExtGeneral.lean, line 457. The attribute's comment: “the property-(P) sufficient condition, read on cohomology, at independent universes”.
H^n(Hom^•_{(A, d)}(L, M)) = Ext^n_{D(A, d)}(L, M)forLwith property (P), at independent universes.A differential graded module with property (P) is orthogonal on the left to the acyclic modules, which is Tag 09KM at independent universes (
DifferentialGradedModule.General.leftOrthogonal_acyclic_of_propertyP), so the previous identification applies. This is the source's own sufficient condition in Tag 0BYW.
def homComplexExtEquivOfPropertyP {L M : DifferentialGradedModule.{u, v, max v w} A} (n : ℤ)
(hL : Nonempty (PropertyPFiltration L)) :
↥((homComplex A L M).homology n) ≃+
((quasiIsomorphisms.{u, v, max v w} A).Q.obj ((toHomotopyCategory A).obj L) ⟶
((quasiIsomorphisms.{u, v, max v w} A).Q.obj ((toHomotopyCategory A).obj M))⟦n⟧)
DifferentialGradedModule.propertyPModelExtEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/PropertyPDerivedModel.lean, line 173. The attribute's comment: “the cohomology of the differential graded Hom complex of chosen property-(P) representatives is Ext between the objects they represent, at independent universes”.
H^n(Hom^•_{(A, d)}(P_M, P_N)) = Ext^n_{D(A, d)}(M, N)for arbitraryM,NinD(A, d), whereP_MandP_Nare the chosen property-(P) representatives.This is the content of Tag 0BYW with no hypothesis on
MorN: the property-(P) reduction is performed by the choice of representative rather than assumed. On the representatives it isDifferentialGradedModule.General.homComplexExtEquivOfPropertyP, and the two isomorphismsDifferentialGradedModule.propertyPModelIsotransport theExt-group from the representatives to the objects, the shift being moved across by the commutation of the shift functor with an isomorphism.
def propertyPModelExtEquiv (M N : derivedCategory.{u, v, max v w} A) (n : ℤ) :
↥((General.homComplex A (propertyPModel.{u, v, w} A M)
(propertyPModel.{u, v, w} A N)).homology n) ≃+ (M ⟶ N⟦n⟧)
Sources
Section22.32 Variant of derived Hom#
Section 22.32 of the Stacks Project, Tag 09LJ. 1 tag here is carried by 12 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09LK, a lemma
Tag 09LK in the Stacks Project.
CochainComplex.homComplexesFunctorCommShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomCommShift.lean, line 88. The attribute's comment: “the functor Hom(K, -) being derived commutes with the translation: the shift comparisons Hom(K, X[n]) = Hom(K, X)[n] are natural in X and compatible with shiftFunctorZero and shiftFunctorAdd, which is the coherence Functor.mapTriangle is formed with”.
Hom(K, -)commutes with the translation. The shift comparisonsHom(K, X[n]) ≅ Hom(K, X)[n]of Tag 09LE are natural inXand compatible withCategoryTheory.shiftFunctorZeroandCategoryTheory.shiftFunctorAdd, so they makeHom(K, -) : CochainComplex B ℤ ⥤ Mod_{(E, d)}a functor commuting with the shift byℤ.
noncomputable instance homComplexesFunctorCommShift :
(homComplexesFunctor B K).CommShift ℤ
DifferentialGradedModule.derivedForgetData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomData.lean, line 136. The attribute's comment: “the forgetful functor D(E, d) ⥤ D(Ab) of the conclusion, together with the identification of its value on an ordinary differential graded module with the underlying complex of that module, which is the phrase on taking associated complexes”.
The forgetful functor datum of Tag 09LK exists, with no hypothesis beyond a differential graded algebra over a commutative ring and a chosen derived category of complexes of modules over that ring.
The functor is
DifferentialGradedModule.derivedForget, the underlying-complex functor descended through the quotient by homotopy and then through the localization at the quasi-isomorphisms, and the identification is the composite of those two descents,DifferentialGradedModule.derivedForgetFactorizationandDifferentialGradedModule.forgetHomotopyToDerivedCategoryIso.
def derivedForgetData : DerivedForgetData A
CochainComplex.homHomotopyFunctor_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomExactness.lean, line 219. The attribute's comment: “the differential graded Hom functor Hom(K, -) : K(B) ⥤ K(E, d) is exact as a functor of triangulated categories -- it commutes with the translation and carries distinguished triangles to distinguished triangles, which is the exactness of the functor being derived read on the homotopy categories”.
Stacks 09LK, the exactness of
Hom(K, -)on the homotopy categories. The differential graded Hom functorHom(K, -) : K(B) ⥤ K(E, d)of Tag 09LE is exact as a functor of triangulated categories: it commutes with the translation, which isCochainComplex.homHomotopyFunctorCommShift, and it carries distinguished triangles to distinguished triangles.This is the exactness asserted by Tag 09LK of the functor being derived, read on the homotopy categories. It is obtained from the exactness of the descent of
Hom(K, -)along the quotient by homotopy, transported alongCochainComplex.homHomotopyFunctorLiftIso.
noncomputable instance homHomotopyFunctor_isTriangulated :
(homHomotopyFunctor B K).IsTriangulated
CochainComplex.homToDerivedCategory_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomExactness.lean, line 231. The attribute's comment: “the functor Hom(K, -) : K(B) ⥤ D(E, d) being right derived is exact as a functor of triangulated categories”.
Stacks 09LK, the exactness of the functor being right derived. The functor
Hom(K, -) : K(B) ⥤ D(E, d)of Tag 09LK — the differential graded Hom functor followed by the localization of the differential gradedE-modules at the quasi-isomorphisms — is exact as a functor of triangulated categories, the localization functor being exact.
noncomputable instance homToDerivedCategory_isTriangulated :
(homToDerivedCategory B K).IsTriangulated
CochainComplex.derivedHomReflectorFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomFunctorAssembly.lean, line 232. The attribute's comment: “the functor itself: R Hom(K, -) : D(A) ⥤ D(E, d), for E the endomorphism differential graded category of K”.
The functor
R Hom(K, -) : D(A) ⥤ D(E, d)of [Stacks, Tag 09LK], forE = C(K, K)the endomorphism differential graded category ofKinComp^dg(A): the reflector-and-descend functorDGCategory.phiReflectorof steps 1 and 2, taken at the chosen witnessesCochainComplex.derivedHomReflectorLandCochainComplex.derivedHomReflector_isZero.Deliberately an
abbrev: the exactness and shift compatibility ofDGCategory.phiReflector(DGCategory.phiReflectorCommShift,DGCategory.phiReflector_isTriangulated) and the identification(*)and step 3 at an arbitrary reflector all apply to it after reduction, so nothing has to be re-registered or restated at the chosen witnesses — and in particular no secondCommShiftterm competes with the canonical one.
abbrev derivedHomReflectorFunctor : DerivedCategory A ⥤
DGCategory.RightModule.derivedCategory
(DGCategory.endDGCategory (CochainComplex.dgCategory A) K)
CochainComplex.homHomotopyFunctorCommShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomHomotopyCommShift.lean, line 195. The attribute's comment: “the differential graded Hom functor Hom(K, -) : K(B) ⥤ K(E, d) commutes with the translation, the shift comparisons of 09LE descending along the quotient by homotopy”.
Hom(K, -) : K(B) ⥤ K(E, d)commutes with the translation.
noncomputable instance homHomotopyFunctorCommShift :
(homHomotopyFunctor B K).CommShift ℤ
CochainComplex.homToDerivedCategoryCommShift, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomHomotopyCommShift.lean, line 202. The attribute's comment: “the functor Hom(K, -) : K(B) ⥤ D(E, d) being right derived commutes with the translation”.
The functor being right derived in Tag 09LK commutes with the translation.
noncomputable instance homToDerivedCategoryCommShift :
(homToDerivedCategory B K).CommShift ℤ
CochainComplex.isDistinguishedTriangle_homComplexesFunctor_triangleOfDegreewiseSplit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomTriangles.lean, line 213. The attribute's comment: “the functor Hom(K, -) carries the triangle of a degreewise split short exact sequence of complexes to a distinguished triangle of K(E, d) -- preservation of distinguished triangles for the functor being derived”.
Hom(K, -)carries the triangle of a degreewise split short exact sequence of complexes to a distinguished triangle ofK(E, d). This is the triangle half of the exactness clause of Tag 09LK for the functor being derived.
theorem isDistinguishedTriangle_homComplexesFunctor_triangleOfDegreewiseSplit :
IsDistinguishedTriangle (DGCategory.endAlgebra (dgCategory B) K)
(Pretriangulated.Triangle.mk
((toHomotopyCategory _).map ((homComplexesFunctor B K).map S.f))
((toHomotopyCategory _).map ((homComplexesFunctor B K).map S.g))
((toHomotopyCategory _).map (homComplexesConnecting B K S σ) ≫
eqToHom (CategoryTheory.Quotient.functor_obj_shift
(homotopyRel (DGCategory.endAlgebra (dgCategory B) K)) ℤ
(DGCategory.representableModule (dgCategory B) K S.X₁) 1).symm))
CochainComplex.exists_isDistinguishedTriangle_homComplexesFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomTriangles.lean, line 242. The attribute's comment: “the functor Hom(K, -) being derived preserves distinguished triangles: every distinguished triangle of K(B) is the triangle of a degreewise split short exact sequence of complexes, and its image, with the third arrow read through the shift comparison Hom(K, X[1]) = Hom(K, X)[1], is a distinguished triangle of K(E, d)”. References: SGA 4½ Etat 0 (1.2.4).
Hom(K, -)preserves distinguished triangles. Every distinguished triangle ofK(B)is isomorphic to the triangle of a degreewise split short exact sequence of complexes, and the image of that triangle underHom(K, -)— with its third arrow corrected by the shift comparisonHom(K, X[1]) ≅ Hom(K, X)[1]— is a distinguished triangle ofK(E, d).This is the preservation of distinguished triangles asserted by Tag 09LK of the functor being derived. It is stated for a presentation of the triangle by a degreewise split sequence rather than as
CategoryTheory.Functor.IsTriangulated; theCategoryTheory.Functor.CommShift ℤthat the latter also requires isCochainComplex.homComplexesFunctorCommShift, whose degree-one component is the comparison appearing here.
theorem exists_isDistinguishedTriangle_homComplexesFunctor [HasZeroObject B]
[HasBinaryBiproducts B]
(T : Pretriangulated.Triangle (HomotopyCategory B (ComplexShape.up ℤ)))
(hT : T ∈ Pretriangulated.distinguishedTriangles
(C := HomotopyCategory B (ComplexShape.up ℤ))) :
∃ (S : ShortComplex (CochainComplex B ℤ))
(σ : ∀ n, (S.map (eval B (ComplexShape.up ℤ) n)).Splitting),
Nonempty (T ≅ trianglehOfDegreewiseSplit S σ) ∧
IsDistinguishedTriangle (DGCategory.endAlgebra (dgCategory B) K)
(Pretriangulated.Triangle.mk
((toHomotopyCategory _).map ((homComplexesFunctor B K).map S.f))
((toHomotopyCategory _).map ((homComplexesFunctor B K).map S.g))
((toHomotopyCategory _).map (homComplexesConnecting B K S σ) ≫
eqToHom (CategoryTheory.Quotient.functor_obj_shift
(homotopyRel (DGCategory.endAlgebra (dgCategory B) K)) ℤ
(DGCategory.representableModule (dgCategory B) K S.X₁) 1).symm))
DGCategory.derivedHomForgetPhiReflectorBetaIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomUnitAppIdCore.lean, line 593. The attribute's comment: “the reduction clause: the functor REDUCES TO THE USUAL R Hom(K, -) on taking associated complexes of abelian groups, under the source's own hypothesis h and the reflector data of steps 1 and 2”.
R Hom(K, -) ≅ R̃ ⋙ U, with nothing owed.
def derivedHomForgetPhiReflectorBetaIso :
CochainComplex.derivedHomForgetFunctor A K h ≅ phiReflectorForget A K L hΦ
DGCategory.phiReflectorCommShift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/RightModule/DerivedHomPhiReflectorExact.lean, line 98. The attribute's comment: “half of exactness as a functor of TRIANGULATED categories: the translation compatibility of R Hom(K, -) : D(A) ⥤ D(E, d), relative to which the exactness below is stated”.
R̃ : D(A) ⥤ D(E)commutes with the translations. The comparison isomorphisms are those of the compositeJ ⋙ ev_K: on the first factor they come fromCategoryTheory.Functor.commShiftOfLocalizationat the localizationDGCategory.phiComparisonLocalization, on the second from the derived evaluation functor.This names the term global instance search already produces for this goal; it is deliberately not itself registered as an instance, since
CategoryTheory.Functor.CommShiftis data and a second registration would be a diamond.
def phiReflectorCommShift : (phiReflector A K L hΦ).CommShift ℤ
DGCategory.phiReflector_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/DifferentialGraded/RightModule/DerivedHomPhiReflectorExact.lean, line 106. The attribute's comment: “the other half: R Hom(K, -) : D(A) ⥤ D(E, d) is EXACT -- it carries distinguished triangles to distinguished triangles, for the translation compatibility above”.
R̃ : D(A) ⥤ D(E)is exact. It is the composite of the descentJof step 1 through the localizationqofK(Comp^dg(A))at the complexesΦ⁻¹ N, which is exact byDGCategory.isTriangulated_derivedReflectorDescent, with evaluation atKon the derived categories; both factors are exact, hence so isR̃.
instance phiReflector_isTriangulated : (phiReflector A K L hΦ).IsTriangulated
Sources
Section22.33 Derived tensor product#
Section 22.33 of the Stacks Project, Tag 09LP. 10 tags here are carried by 50 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09LQ, an equation
Tag 09LQ in the Stacks Project.
DifferentialGraded.Bimodule.tensorCompFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensor.lean, line 1270. The attribute's comment: “the functor Mod_(A,d) -> Mod_(B,d), M |-> M (x)_A N”.
Stacks 09LM. The induced functor on the categories of differential graded modules.
noncomputable abbrev tensorCompFunctor (N : Bimodule A B) :
DifferentialGradedModule A ⥤ DifferentialGradedModule B
Tag 09LR, a lemma
Tag 09LR in the Stacks Project.
DifferentialGraded.Bimodule.tensorHomotopyFunctor_isTriangulated', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensorTriangulated.lean, line 660.
Stacks 09LR. Tensoring with a differential graded
(A, B)-bimodule is an exact functor from the homotopy category of differential gradedA-modules to that of differential gradedB-modules: it commutes with translation and carries distinguished triangles to distinguished triangles.
theorem tensorHomotopyFunctor_isTriangulated' (N : Bimodule A B) :
∃ h : (tensorHomotopyFunctor N).CommShift ℤ,
letI := h
(tensorHomotopyFunctor N).IsTriangulated
Tag 09LS, a lemma
Tag 09LS in the Stacks Project.
DifferentialGraded.Bimodule.tensorFunctorToDerivedCategory_isLeftDerivable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorFunctor.lean, line 110. The attribute's comment: “existence in the pro-object sense”.
Stacks Tag 09LS, in the source's own sense. Tensoring with the bimodule
N, followed by localization of the target, is left derivable with respect to the quasi-isomorphisms: its left derived functor is defined at every object ofK(A, d), meaning that the pro-objectQis(A)/X ⥤ D(B, d)is essentially constant (Tag 05SV).
theorem tensorFunctorToDerivedCategory_isLeftDerivable (N : Bimodule A B) :
(tensorFunctorToDerivedCategory N).IsLeftDerivable (quasiIsomorphisms' A)
DifferentialGraded.Bimodule.tensorFunctorToDerivedCategory_hasLeftDerivedFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorFunctor.lean, line 120. The attribute's comment: “existence of the total left derived functor”.
Stacks Tag 09LS, in Mathlib's Kan extension sense. Tensoring with the bimodule
N, followed by localization of the target, has a total left derived functor: a right Kan extension along the localization ofK(A, d)at the quasi-isomorphisms. This is what names- ⊗_A^𝐋 Nas a functor onD(A, d).
theorem tensorFunctorToDerivedCategory_hasLeftDerivedFunctor (N : Bimodule A B) :
(tensorFunctorToDerivedCategory N).HasLeftDerivedFunctor (quasiIsomorphisms' A)
DifferentialGraded.Bimodule.derivedTensorFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorFunctor.lean, line 128. The attribute's comment: “the derived tensor functor”.
The derived tensor product
- ⊗_A^𝐋 N : D(A, d) ⥤ D(B, d)of Stacks Tag 09LS: the total left derived functor of tensoring withNfollowed by localization.
def derivedTensorFunctor (N : Bimodule A B) : derivedCategory' A ⥤ derivedCategory' B
DifferentialGraded.Bimodule.derivedTensorFunctor_isLeftDerivedFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorFunctor.lean, line 149. The attribute's comment: “universal property”.
The universal property of Stacks Tag 09LS: the comparison
DifferentialGraded.Bimodule.derivedTensorFunctorCounitexhibits- ⊗_A^𝐋 Nas the left derived functor of tensoring withNfollowed by localization, with respect to the quasi-isomorphisms.
instance derivedTensorFunctor_isLeftDerivedFunctor (N : Bimodule A B) :
(derivedTensorFunctor N).IsLeftDerivedFunctor
(derivedTensorFunctorCounit N) (quasiIsomorphisms' A)
Tag 09S3, a lemma
Tag 09S3 in the Stacks Project.
DifferentialGraded.Bimodule.derivedTensorNatTrans, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorBimoduleMap.lean, line 299. The attribute's comment: “the natural transformation 1 (x) f”.
Stacks 09S3, the morphism of functors. A homomorphism
f : N ⟶ N'of differential graded(A, B)-bimodules induces1 ⊗ f : - ⊗_A^𝐋 N ⟶ - ⊗_A^𝐋 N', a natural transformation of the derived tensor functors of Tag 09LS onD(A, d).It is the descent of
DifferentialGraded.Bimodule.ordinaryTensorNatTransalong the localization:- ⊗_A^𝐋 N'is a right Kan extension of ordinary tensoring withN', so the transformation is the unique one compatible with the two comparisons of Tag 09LS (DifferentialGraded.Bimodule.derivedTensorNatTrans_counit).
def derivedTensorNatTrans {N N' : Bimodule A B} (f : N ⟶ N') :
derivedTensorFunctor N ⟶ derivedTensorFunctor N'
DifferentialGraded.Bimodule.isIso_derivedTensorNatTrans_app_shift_regularModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorQuasiIsoDevissage.lean, line 198. The attribute's comment: “the second assertion at the shifts A[k] of the algebra, where the quasi-isomorphism hypothesis enters”.
Clause (3) of the dévissage of Stacks 0FQE for
1 ⊗ f: for a homomorphismf : N ⟶ N'of differential graded(A, B)-bimodules which is a quasi-isomorphism of right differential gradedB-modules, the transformation1 ⊗ f : - ⊗_A^𝐋 N ⟶ - ⊗_A^𝐋 N'is invertible at the class of every shiftA[k]of the regular module.The shift
A[k]is orthogonal on the left to the acyclic modules by Tag 09K1, so both comparisons of Tag 09LS are invertible there and1 ⊗ fbecomes the ordinary mapA[k] ⊗_A N ⟶ A[k] ⊗_A N', which is the quasi-isomorphismf[k].
theorem isIso_derivedTensorNatTrans_app_shift_regularModule {N N' : Bimodule A B} (f : N ⟶ N')
(hf : QuasiIso ((forgetToCochainComplex B).map f.rightHom)) (k : ℤ) :
IsIso ((derivedTensorNatTrans f).app
(((toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).obj (regularModule A))⟦k⟧))
DifferentialGraded.Bimodule.isIso_derivedTensorNatTrans_app_sigma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorQuasiIsoDevissage.lean, line 237. The attribute's comment: “the second assertion at a direct sum, from the summands”.
Clause (1) of the dévissage of Stacks 0FQE for
1 ⊗ f: the transformation1 ⊗ f : - ⊗_A^𝐋 N ⟶ - ⊗_A^𝐋 N'is invertible at a direct sum of objects ofD(A, d)at which it is invertible.Both functors are left adjoints by Tag 09LT, hence preserve direct sums, so the component of
1 ⊗ fat⨁ᵢ Kᵢis the comparison of the two colimit cocones induced by its components at theKᵢ.
theorem isIso_derivedTensorNatTrans_app_sigma {N N' : Bimodule A B} (f : N ⟶ N')
{ι : Type u} (K : ι → derivedCategory' A)
(h : ∀ i, IsIso ((derivedTensorNatTrans f).app (K i))) :
IsIso ((derivedTensorNatTrans f).app (∐ K))
DifferentialGraded.Bimodule.derivedTensorTwoOutOfThree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorQuasiIsoDevissage.lean, line 268. The attribute's comment: “the second assertion along a distinguished triangle, two out of three”.
Clause (2) of the dévissage of Stacks 0FQE for the transformations
1 ⊗ f. The derived tensor functors are exact and1 ⊗ fcommutes with the translation, so its components form a morphism of distinguished triangles, to which the five lemma of Tag 014A applies.
theorem derivedTensorTwoOutOfThree (A B : DifferentialGradedAlgebra.{u, u} R) :
DerivedTensorTwoOutOfThree A B
DifferentialGraded.Bimodule.quasiIsoInvertsDerivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorQuasiIsoDevissage.lean, line 299. The attribute's comment: “the second assertion”.
The second assertion of Stacks 09S3. A homomorphism
f : N ⟶ N'of differential graded(A, B)-bimodules that is a quasi-isomorphism of right differential gradedB-modules induces an isomorphism1 ⊗ f : - ⊗_A^𝐋 N ⟶ - ⊗_A^𝐋 N'of functorsD(A, d) ⥤ D(B, d).
theorem quasiIsoInvertsDerivedTensor (A B : DifferentialGradedAlgebra.{u, u} R) :
QuasiIsoInvertsDerivedTensor A B
Tag 0GZ2, a lemma
Tag 0GZ2 in the Stacks Project.
DifferentialGraded.Bimodule.LeftPropertyP, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorLeftPropertyP.lean, line 104. The attribute's comment: “the hypothesis: property (P) as a left differential graded A-module”.
The differential graded
(A, B)-bimoduleNhas property (P) as a left differential gradedA-module: the left differential gradedA-module underlying it, read as a right differential gradedA^{opp}-module through the equivalence of Tag 0FQ0, carries a property-(P) filtration in the sense of Tag 09KK.
def LeftPropertyP (N : Bimodule A B) : Prop
DifferentialGraded.Bimodule.isIso_derivedTensorFunctorCounit_app_of_leftPropertyP', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorLeftPropertyPProof.lean, line 156.
For a differential graded
(A, B)-bimoduleNwith property (P) as a left differential gradedA-module and every differential gradedA-moduleM, the comparisonM ⊗_A^𝐋 N ⟶ M ⊗_A Nof Tag 09LS is an isomorphism inD(B, d).
theorem isIso_derivedTensorFunctorCounit_app_of_leftPropertyP' (N : Bimodule A B)
(hP : LeftPropertyP N) (M : DifferentialGradedModule A) :
IsIso ((derivedTensorFunctorCounit N).app ((toHomotopyCategory A).obj M))
DifferentialGraded.Bimodule.derivedTensorIsoOfLeftPropertyP', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorLeftPropertyPProof.lean, line 165. The attribute's comment: “as an isomorphism of functors”.
For a differential graded
(A, B)-bimoduleNwith property (P) as a left differential gradedA-module, the isomorphism- ⊗_A^𝐋 N ≅ - ⊗_A Nof functorsD(A, d) ⥤ D(B, d).
def derivedTensorIsoOfLeftPropertyP' (N : Bimodule A B) (hP : LeftPropertyP N) :
(quasiIsomorphisms' A).Q ⋙ derivedTensorFunctor N ≅ tensorFunctorToDerivedCategory N
Tag 09LT, a lemma
Tag 09LT in the Stacks Project.
DifferentialGraded.Bimodule.derivedTensorFunctor_adj_derivedHomFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorHomAdjunction.lean, line 240. References: SGA 5 IIIB (5.2), “5.2.3”.
Stacks 09LT. The derived tensor product
- ⊗_A^𝐋 N : D(A, d) ⥤ D(B, d)of Tag 09LS is a left adjoint to derived HomRHom(N, -) : D(B, d) ⥤ D(A, d)of Tag 09LI, for a differential graded(A, B)-bimoduleN. Nothing is assumed.This is
DifferentialGraded.Bimodule.derivedTensorFunctor_adj_derivedHomwith both of its hypotheses supplied: Tag 09LN byDifferentialGraded.Bimodule.tensorHomotopyFunctor_adj_homHomotopyCategoryFunctor, and Tag 09KU byDifferentialGradedModule.exists_propertyI_resolution, which also pins the derived Hom functor to that ofDifferentialGradedModule.derivedHomData.The degree-zero scope of the Tag 09LN input does not limit this. What is proved of Tag 09LN for differential graded modules is the bijection of the morphism groups of the two categories, not the isomorphism of Hom complexes in all degrees that the source also states there. But Tag 09LT asserts an adjunction of functors between the derived categories — a bijection of morphism groups, natural in both variables — and it is deduced from an adjunction of functors between the homotopy categories, which is again a bijection of morphism groups. The all-degrees half of Tag 09LN is neither used nor needed, so this is Tag 09LT in full and the tag is bare.
def derivedTensorFunctor_adj_derivedHomFunctor (N : Bimodule A B) :
derivedTensorFunctor N ⊣ (derivedHomData A B N.rightModule N.leftAction).functor
DifferentialGraded.Bimodule.derivedTensorFunctor_adj_derivedHomFunctor_homEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorHomAdjunction.lean, line 250. The attribute's comment: “as a bijection of morphism groups”.
Stacks 09LT, as the bifunctorial identification of morphism groups
Hom_{D(B,d)}(M ⊗_A^𝐋 N, P) ≃ Hom_{D(A,d)}(M, RHom(N, P))that Stacks 0BYX, Example 22.33.2 uses. Nothing is assumed: it is the hom-set bijection ofDifferentialGraded.Bimodule.derivedTensorFunctor_adj_derivedHomFunctor.
def derivedTensorFunctor_adj_derivedHomFunctor_homEquiv (N : Bimodule A B)
(M : derivedCategory' A) (P : derivedCategory' B) :
((derivedTensorFunctor N).obj M ⟶ P) ≃
(M ⟶ (derivedHomData A B N.rightModule N.leftAction).functor.obj P)
Tag 0BYX, an example
Tag 0BYX in the Stacks Project.
DifferentialGraded.Bimodule.tensorRegularRightNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensorRegularRight.lean, line 255. The attribute's comment: “restriction of scalars is tensoring with the regular bimodule, on differential graded modules”.
Stacks 0BYX, the tensor half, on differential graded modules. Restriction of scalars along
ψ : C → Bis tensoring with the regular(B, C)-bimodule, naturally in the module.Naturality is an equality of two homomorphisms out of a tensor product, so it is checked on pure tensors, where both sides send
x ⊗ btof(x) b.
def tensorRegularRightNatIso (ψ : C.Hom B) :
tensorCompFunctor (regularRight ψ) ≅ restrictScalarsFunctor ψ
DifferentialGraded.Bimodule.derivedTensorRegularRightIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensorRegularRight.lean, line 300. The attribute's comment: “restriction of scalars is tensoring with the regular bimodule, on derived categories”.
Stacks 0BYX, the tensor half, on derived categories. Derived restriction of scalars along
ψ : C → Bis the derived tensor product with the regular(B, C)-bimodule.Tensoring with the regular bimodule already inverts the quasi-isomorphisms, so by the construction of the derived tensor product in the proof of Tag 09LS it computes the derived tensor product; and it descends to derived restriction of scalars through the localizations.
def derivedTensorRegularRightIso (ψ : C.Hom B) :
derivedTensorFunctor (regularRight ψ) ≅ derivedRestriction ψ
DifferentialGradedModule.regularHomFactorization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomFunctor.lean, line 242. The attribute's comment: “the factorization of derived Hom out of the regular bimodule”.
Stacks 0BYX. Internal Hom out of the regular differential graded
(A, B)-bimodule, followed by localization of the target, factors through the derived category ofBas derived restriction of scalars alongφ.This is the composite of the identification of internal Hom out of the regular bimodule with restriction of scalars (
DifferentialGradedModule.homHomotopyFunctorRegularIso) and the defining factorisation of derived restriction (DifferentialGradedModule.derivedRestrictionFactorization).
def regularHomFactorization (φ : A.Hom B) :
(quasiIsomorphisms' B).Q ⋙ derivedRestriction φ ≅
homToDerivedCategory A B (regularModule B) (regularBimoduleStructure φ)
DifferentialGradedModule.DerivedHomData.regular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomFunctor.lean, line 261. The attribute's comment: “derived Hom out of the regular bimodule, as a right derived functor”.
Stacks 0BYX, and Stacks 09LI for the regular bimodule. Derived Hom out of the regular differential graded
(A, B)-bimodule of a homomorphismφ : A → B, as a right derived functor of internal Hom — unconditionally, with the derived functor being the already-constructedDifferentialGradedModule.derivedRestriction.No resolutions are used: the hypothesis of
DifferentialGradedModule.DerivedHomData.ofResolutions— the existence of property (I) resolutions, Tag 09KU — does not appear, because internal Hom out of the regular bimodule is restriction of scalars, which does not change the underlying complex and therefore already inverts the quasi-isomorphisms.
def regular (φ : A.Hom B) :
DerivedHomData A B (regularModule B) (regularBimoduleStructure φ)
DifferentialGradedModule.DerivedHomData.functorIsoDerivedRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedHomFunctor.lean, line 273. The attribute's comment: “RHom(B, -) is restriction of scalars, for any derived Hom datum”.
Stacks 0BYX, Example 22.33.2.
RHom(B, -) = (-)_A: the functor of any right derived functor of Hom out of the regular differential graded(A, B)-bimodule is canonically derived restriction of scalars alongφ.
def functorIsoDerivedRestriction (φ : A.Hom B)
(D : DerivedHomData A B (regularModule B) (regularBimoduleStructure φ)) :
D.functor ≅ derivedRestriction φ
DifferentialGradedModule.regularBimoduleStructure, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 203. The attribute's comment: “the regular bimodule structure”.
A homomorphism
φ : A → Bof differential graded algebras makes the regular right differential gradedB-module into a differential graded(A, B)-bimodule:Aacts on the left by multiplication throughφ, and that action is rightB-linear by associativity.
def regularBimoduleStructure (φ : A.Hom B) : BimoduleStructure A B (regularModule B)
DifferentialGradedModule.regularHomogeneousEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 271. The attribute's comment: “evaluation at one, degreewise”.
Evaluation at one. The degree-
nhomogeneous rightB-linear maps out of the regular differential gradedB-module are the degree-nelements of the target, by evaluation at the unit. This is the degreewise half of Example 22.33.2.
def regularHomogeneousEquiv (P : DifferentialGradedModule B) (n : ℤ) :
P.grading n ≃ₗ[R] HomogeneousMap B (regularModule B) P n
DifferentialGradedModule.restrictScalarsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 309. The attribute's comment: “restriction of scalars as a functor”. References: EGA II (2.8.6), “more general”.
Restriction of scalars along
φ, as a functor between the categories of differential graded modules. A homomorphism is unchanged: aB-linear map isA-linear throughφ.
def restrictScalarsFunctor (φ : A.Hom B) :
DifferentialGradedModule B ⥤ DifferentialGradedModule A
DifferentialGradedModule.restrictScalarsHomotopyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 369. The attribute's comment: “restriction of scalars on homotopy categories”.
Restriction of scalars along
φon the homotopy categories: it descends through the homotopy quotient because it preserves homotopies.
def restrictScalarsHomotopyFunctor (φ : A.Hom B) : HomotopyCategory B ⥤ HomotopyCategory A
DifferentialGradedModule.derivedRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 416. The attribute's comment: “restriction of scalars on derived categories”.
Restriction of scalars along
φon the derived categories, obtained by descending restriction on the homotopy categories through the localization at the quasi-isomorphisms. This is the functorR Hom(B, -) : D(B, d) ⥤ D(A, d)of Example 22.33.2, whose identification with derived Hom out of the regular bimodule is the content of that example.
def derivedRestriction (φ : A.Hom B) : derivedCategory' B ⥤ derivedCategory' A
DifferentialGradedModule.derivedRestrictionFactorization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 423. The attribute's comment: “the factorization of derived restriction”.
Derived restriction of scalars is restriction of scalars read through the localizations: the square of homotopy and derived categories commutes up to this canonical isomorphism.
def derivedRestrictionFactorization (φ : A.Hom B) :
(quasiIsomorphisms' B).Q ⋙ derivedRestriction φ ≅
restrictScalarsHomotopyFunctor φ ⋙ (quasiIsomorphisms' A).Q
DifferentialGradedModule.regularHomModuleData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 465. The attribute's comment: “restriction of scalars presents the internal hom”. References: EGA III (7.2.2), “more general”.
Restriction of scalars along
φpresents the internal hom out of the regular differential graded(A, B)-bimodule: its degree-npart is the degree-nhomogeneous rightB-linear mapsB → P, by evaluation at the unit, and the rightA-action matches precomposition with multiplication throughφ.
def regularHomModuleData (φ : A.Hom B) (P : DifferentialGradedModule B) :
HomModuleData A B (regularModule B) P (regularBimoduleStructure φ)
DifferentialGradedModule.homModuleRegularIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 491. The attribute's comment: “evaluation at one”.
Evaluation at the unit identifies the internal hom out of the regular differential graded
(A, B)-bimodule with restriction of scalars alongφ.
def homModuleRegularIso (φ : A.Hom B) (P : DifferentialGradedModule B) :
(regularHomFunctor φ).obj P ≅ (restrictScalarsFunctor φ).obj P
DifferentialGradedModule.homModuleFunctorRegularIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 532. The attribute's comment: “evaluation at one is natural”.
Evaluation at one is natural: the internal hom functor out of the regular differential graded
(A, B)-bimodule is restriction of scalars alongφ.
def homModuleFunctorRegularIso (φ : A.Hom B) :
regularHomFunctor φ ≅ restrictScalarsFunctor φ
DifferentialGradedModule.homHomotopyFunctorRegularIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 586. The attribute's comment: “evaluation at one on homotopy categories”.
Evaluation at one on homotopy categories: the internal hom functor out of the regular differential graded
(A, B)-bimodule is restriction of scalars alongφ. This is the identificationR Hom(B, -) = (-)_Aof Example 22.33.2, before localizing.
def homHomotopyFunctorRegularIso (φ : A.Hom B) :
homHomotopyCategoryFunctor A B (regularModule B) (regularBimoduleStructure φ) ≅
restrictScalarsHomotopyFunctor φ
DifferentialGradedModule.quasiIsomorphisms_isInvertedBy_homToDerivedCategory_regular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 598. The attribute's comment: “derived Hom out of the regular bimodule needs no resolutions”.
The functor whose right derived functor is derived Hom out of the regular differential graded
(A, B)-bimodule already inverts the quasi-isomorphisms: it is restriction of scalars followed by localization, and restriction does not change the underlying complex.
theorem quasiIsomorphisms_isInvertedBy_homToDerivedCategory_regular (φ : A.Hom B) :
(quasiIsomorphisms' B).IsInvertedBy
(homToDerivedCategory A B (regularModule B) (regularBimoduleStructure φ))
DifferentialGraded.Bimodule.regular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestriction.lean, line 618. The attribute's comment: “the regular bimodule”.
The regular differential graded
(A, B)-bimodule of a homomorphismφ : A → Bof differential graded algebras:Bitself, withBacting on the right by multiplication andAacting on the left throughφ. Tensoring with it is the extension of scalars- ⊗_A B : D(A, d) ⥤ D(B, d)of Example 22.33.2.
def regular (φ : A.Hom B) : Bimodule A B
DifferentialGradedModule.derivedHom_comparison_eq_evaluationAtOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedRestrictionEvaluation.lean, line 143. The attribute's comment: “the comparison of derived Hom out of the regular bimodule is evaluation at one”.
Stacks 0BYX, Example 22.33.2. The identification of derived Hom out of the regular differential graded
(A, B)-bimodule with derived restriction of scalars is pinned by evaluation at the unit: on the class of a differential gradedB-moduleN, the canonical comparison of the derived functor with internal Hom, followed by the identification with derived restriction and the factorisation of derived restriction, is the localisation of the evaluation morphismHom^•_B(B, N) → N_A, f ↦ f(1), transported along the identificationDifferentialGradedModule.homHomotopyFunctorRegularIsoof the two source objects.The transport is not optional: internal Hom out of the regular bimodule is isomorphic to restriction of scalars and not equal to it, so the two morphisms have different sources.
theorem derivedHom_comparison_eq_evaluationAtOne (φ : A.Hom B)
(D : DerivedHomData A B (regularModule B) (regularBimoduleStructure φ))
(N : DifferentialGradedModule B) :
D.comparison.app ((toHomotopyCategory B).obj N) ≫
(DerivedHomData.functorIsoDerivedRestriction φ D).hom.app
((quasiIsomorphisms' B).Q.obj ((toHomotopyCategory B).obj N)) ≫
(derivedRestrictionFactorization φ).hom.app ((toHomotopyCategory B).obj N) =
(quasiIsomorphisms' A).Q.map
((homHomotopyFunctorRegularIso φ).hom.app ((toHomotopyCategory B).obj N)) ≫
(quasiIsomorphisms' A).Q.map
((toHomotopyCategory A).map ((evaluationAtOne φ).evaluation N))
DifferentialGraded.Bimodule.derivedTensorFunctor_adj_derivedRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorHomAdjunction.lean, line 279. The attribute's comment: “the adjunction Hom_{D(A,d)}(M, N_A) = Hom_{D(B,d)}(M ⊗_A^𝐋 B, N), bifunctorially”. References: SGA 5 IIIB (5.2), “5.2.3 for F = B”.
Stacks 0BYX, Example 22.33.2. For a homomorphism
φ : (A, d) → (B, d)of differential graded algebras, derived extension of scalars- ⊗_A^𝐋 B : D(A, d) ⥤ D(B, d)— tensoring with the regular bimodule,DifferentialGraded.Bimodule.regular— is left adjoint to derived restriction of scalars(-)_A : D(B, d) ⥤ D(A, d). Nothing is assumed.This is the displayed formula of the example,
Hom_{D(A,d)}(M, N_A) = Hom_{D(B,d)}(M ⊗_A^𝐋 B, N), bifunctorially inMandN: anCategoryTheory.Adjunctionis exactly a bijection of the two morphism groups together with its naturality in both variables, so the bifunctoriality the source asserts is carried by this statement and needs no separate lemma. The bijection on its own isDifferentialGraded.Bimodule.derivedTensorFunctor_adj_derivedRestriction_homEquiv.The two inputs are the two steps the example takes. The adjunction with derived Hom out of the regular bimodule on the right is Tag 09LT,
DifferentialGraded.Bimodule.derivedTensorFunctor_adj_derivedHomFunctor; andDifferentialGradedModule.DerivedHomData.functorIsoDerivedRestrictionis the example's identificationRHom(B, -) = (-)_A, which comes fromHom_{Mod^{dg}_B}(B, N) ≅ N_A,f ↦ f(1), naturally inN. Transporting the right adjoint along that isomorphism replacesRHom(B, -)by restriction of scalars, which is the example's conclusion.
def derivedTensorFunctor_adj_derivedRestriction (φ : A.Hom B) :
derivedTensorFunctor (Bimodule.regular φ) ⊣ derivedRestriction φ
DifferentialGraded.Bimodule.derivedTensorFunctor_adj_derivedRestriction_homEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorHomAdjunction.lean, line 293. The attribute's comment: “the displayed formula Hom_{D(A,d)}(M, N_A) = Hom_{D(B,d)}(M ⊗_A^𝐋 B, N)”.
Stacks 0BYX, Example 22.33.2, the displayed formula itself:
Hom_{D(A,d)}(M, N_A) = Hom_{D(B,d)}(M ⊗_A^𝐋 B, N).It is the hom-set bijection of
DifferentialGraded.Bimodule.derivedTensorFunctor_adj_derivedRestriction, so the bifunctoriality inMandNthat the source asserts is the naturality carried by that adjunction; it is not restated here.
def derivedTensorFunctor_adj_derivedRestriction_homEquiv (φ : A.Hom B)
(M : derivedCategory' A) (N : derivedCategory' B) :
(M ⟶ (derivedRestriction φ).obj N) ≃
((derivedTensorFunctor (Bimodule.regular φ)).obj M ⟶ N)
DifferentialGradedModule.evaluationAtOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/EvaluationAtOne.lean, line 95. The attribute's comment: “evaluation_at_one”.
Evaluation at the unit identifies the graded Hom from
Bwith restriction toA, naturally in the differential gradedB-module.
public noncomputable def evaluationAtOne (φ : A.Hom B) :
EvaluationAtOneData φ
DifferentialGradedModule.restrictScalars, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/Restriction.lean, line 60. The attribute's comment: “restriction_notation”. References: EGA II (2.8.6), “more general”.
Restrict a right differential graded
B-module toAalong a homomorphism of differential graded algebras.
def restrictScalars (φ : A.Hom B) (N : DifferentialGradedModule B) :
DifferentialGradedModule A
Dualizing.derivedExtensionToDGA_adj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolutionExtension.lean, line 87. The attribute's comment: “extension of scalars along R -> E is left adjoint to forgetting the action”.
Stacks 0BYX for the structure homomorphism of
E, read onD(R). Derived extension of scalars- ⊗_R^𝐋 E : D(R) ⥤ D(E, d)is left adjoint to the forgetful functorD(E, d) ⥤ D(R).The adjunction of Tag 0BYX is between derived extension and derived restriction of scalars along
R → E; transporting its right adjoint alongDualizing.derivedRestrictBaseForgetIso, which identifies derived restriction read onD(R)with the forgetful functor, gives the statement in the form Situation 0BZB uses.
def derivedExtensionToDGA_adj (E : DifferentialGradedAlgebra.{u, u} R) :
derivedExtensionToDGA E ⊣ derivedForget E
Dualizing.derivedTensorResolvingBimoduleForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolutionForget.lean, line 150. The attribute's comment: “forgetting the action is derived tensoring with the regular (E, R)-bimodule”.
The tensor half of Stacks 0BYX for the structure homomorphism of
E. Derived tensoring with the resolving bimoduleE, read in the derived category ofR-modules through the degree-zero equivalence, is the forgetful functorD(E, d) ⥤ D(R): forgetting theE-action is restriction of scalars alongR → E, which is tensoring with the regular(E, R)-bimodule.
def derivedTensorResolvingBimoduleForgetIso (E : DifferentialGradedAlgebra.{u, u} R) :
Bimodule.derivedTensorFunctor (resolvingBimodule E) ⋙
(degreeZeroDerivedEquivalence (R := R) (A := R)).functor ≅ derivedForget E
Dualizing.DGAResolution.derivedTensorResolvingBimoduleIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/DifferentialGradedResolutionForget.lean, line 166. The attribute's comment: “forgetting the action of the resolving algebra is derived tensoring with its regular (E, R)-bimodule”.
The tensor half of Stacks 0BYX at the resolving algebra of Situation 0BZB. Derived tensoring with the resolving bimodule of
E, read in the derived category ofR-modules, is the forgetful functorD(E, d) ⥤ D(R).
def derivedTensorResolvingBimoduleIso (S : Dualizing.DGAResolution R A) :
Bimodule.derivedTensorFunctor (Dualizing.resolvingBimodule S.E) ⋙
(degreeZeroDerivedEquivalence (R := R) (A := R)).functor ≅
DifferentialGradedModule.derivedForget S.E
Tag 09R9, a lemma
Tag 09R9 in the Stacks Project.
DifferentialGraded.Bimodule.derivedTensorFunctor_fullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorFullyFaithful.lean, line 431.
Stacks 09R9. Let
(A, d)and(B, d)be differential graded algebras over a commutative ringRand letNbe a differential graded(A, B)-bimodule. Assume
- the class of
NinD(B, d)is a compact object, and- the canonical map
H^k(A) → Hom_{D(B,d)}(N, N[k])ofDifferentialGraded.Bimodule.cohomologyEndomorphismComparisonis bijective for everyk : ℤ.Then the derived tensor product
- ⊗_A^𝐋 N : D(A, d) ⥤ D(B, d)of Tag 09LS is fully faithful.Full faithfulness is data — a chosen inverse to the action on morphism groups — so this is a definition. It is Tag 07RB applied to the adjunction of Tag 09LT, whose unit is invertible by
DifferentialGraded.Bimodule.isIso_unit_derivedTensorFunctor_adj_derivedHomFunctor.
def derivedTensorFunctor_fullyFaithful (N : Bimodule A B)
[IsCompactObject.{u} ((toHomotopyCategory B ⋙ (quasiIsomorphisms' B).Q).obj N.rightModule)]
(h2 : ∀ k : ℤ, Function.Bijective (N.cohomologyEndomorphismComparison k)) :
(derivedTensorFunctor N).FullyFaithful
Tag 0BYZ, a lemma
Tag 0BYZ in the Stacks Project.
DifferentialGraded.Bimodule.derivedBaseChangeFunctor_isLeftDerivedFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BaseChange.lean, line 224. The attribute's comment: “part (1) only, with the functor being derived presented as M |-> M (x)_A A': the identification c_M with the source's M |-> M (x)_R R' is baseChangeTensorIso over R' and baseChangeTensorAlgebraIso over A'. Corrected: the source says "right derived functor", but base change is a tensor product and so is LEFT derived, as Tag 09LS has it. Parts (2) and (3) are elsewhere, per the docstrings; nothing of Tag 0BYZ remains uncovered”.
Stacks 0BYZ, part (1). The derived tensor product
- ⊗_A^𝐋 A'with the base changeA' = A ⊗_R R'is the total left derived functor of base changeK(A, d) → K(A', d),M ↦ M ⊗_R R', followed by localization.The functor derived here is
M ↦ M ⊗_A A'; it is base changeM ↦ M ⊗_R R'by the canonical mapc_Mof the source's proof, which isDifferentialGraded.Bimodule.baseChangeTensorIsoas an isomorphism of differential gradedR'-modules andDifferentialGraded.Bimodule.baseChangeTensorAlgebraIsoas one of differential gradedA'-modules. Part (3) isDifferentialGraded.Bimodule.isIso_derivedBaseChangeCounit_app_of_kFlatofStacksFrontier/Algebra/DifferentialGraded/Module/BaseChangeRepresents.leanand part (2) isDifferentialGraded.Bimodule.derivedBaseChangeRestrictionSquareofStacksFrontier/Algebra/DifferentialGraded/Module/BaseChangeRestrictionSquare.lean.
theorem derivedBaseChangeFunctor_isLeftDerivedFunctor :
(derivedBaseChangeFunctor A R').IsLeftDerivedFunctor
(derivedBaseChangeCounit A R') (quasiIsomorphisms' A)
DifferentialGraded.Bimodule.baseChangeTensorAlgebraIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BaseChangeAbsoluteTensor.lean, line 559. The attribute's comment: “the A'-linearity of the canonical map c_M of the PROOF, NOT any of parts (1), (2), (3): M (x)_A A' is M (x)_R R' as differential graded A'-modules, the right action on M (x)_R R' being (m (x) t)(a (x) s) = (m a) (x) (t s). With this nothing of Tag 0BYZ is left unformalized; the module docstring says where the three parts and the R'-only form baseChangeTensorIso are, and how this A'-module restricts to that R'-module”.
The
A'-linearity of the canonical mapc_Min the proof of Stacks 0BYZ. LetR → R'be a map of commutative rings, let(A, d)be a differential gradedR-algebra and letA' = A ⊗_R R'be its base change. For a differential gradedA-moduleMthe base changeM ⊗_A A'isM ⊗_R R'as a differential gradedA'-module, the right action ofa ⊗ sonM ⊗_R R'being(m ⊗ t) · (a ⊗ s) = (m · a) ⊗ (t s)(DifferentialGradedModule.baseChange_smul_tmul).The isomorphism is the source's
c_M, read in the direction out of the relative tensor product: it sends the pure tensorx ⊗ (a ⊗ s)to(x · a) ⊗ s(DifferentialGraded.Bimodule.baseChangeTensorForward_pure), and its inverse — the source'sc_Mitself — sendsx ⊗ stox ⊗ (1 ⊗ s).
def baseChangeTensorAlgebraIso :
baseChangeRelativeTensor A R' M ≅ baseChangeAbsoluteTensor M R'
DifferentialGraded.Bimodule.isIso_derivedBaseChangeCounit_app_of_kFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BaseChangeRepresents.lean, line 138. The attribute's comment: “part (3): M K-flat as a complex of R-modules implies that the ordinary base change represents M (x)_A^L A'. The representing object is spelled M (x)_A A'; it is the source's differential graded A'-module M (x)_R R' by baseChangeTensorIso over R' and by baseChangeTensorAlgebraIso of BaseChangeAbsoluteTensor.lean over A'. Part (2) is derivedBaseChangeRestrictionSquare of BaseChangeRestrictionSquare.lean”.
Let
R → R'be a ring map,(A, d)a differential gradedR-algebra which is K-flat as a complex ofR-modules, andA' = A ⊗_R R'. For a differential gradedA-moduleMwhich is K-flat as a complex ofR-modules, the comparison from the derived base changeM ⊗_A^𝐋 A'to the ordinary base changeM ⊗_A A'is an isomorphism atM, soM ⊗_A A'representsM ⊗_A^𝐋 A'. Nothing is asked ofR'.
theorem isIso_derivedBaseChangeCounit_app_of_kFlat
(hA : CochainComplex.KFlat.{u, u} (regularModule A).toCochainComplex)
(M : DifferentialGradedModule.{u, u, u} A)
(hM : CochainComplex.KFlat.{u, u} M.toCochainComplex) :
IsIso ((derivedBaseChangeCounit A R').app ((toHomotopyCategory A).obj M))
DifferentialGraded.Bimodule.derivedBaseChangeRestrictionSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BaseChangeRestrictionSquare.lean, line 395. The attribute's comment: “part (2): the square of restriction and derived base change commutes. The left column is restriction along the structure homomorphism R -> A, the right column restriction along r' |-> 1 (x) r', and the bottom edge derived base change of R in degree zero read in D(R', d) through the unitor R (x)_R R' = R' of degreeZeroBaseChangeUnitor. Parts (1) and (3) are derivedBaseChangeFunctor_isLeftDerivedFunctor and isIso_derivedBaseChangeCounit_app_of_kFlat”.
Stacks 0BYZ, part (2). "Let
R → R'be a ring map, let(A, d)be a differential gradedR-algebra, let(A', d)be the base changeA ⊗_R R'. IfAis K-flat as a complex ofR-modules, then the diagramcommutes."D(A, d) --- - ⊗_A^𝐋 A' ---> D(A', d) | | restriction restriction v v D(R) --- - ⊗_R^𝐋 R' ---> D(R')The two columns are restriction of scalars along the structure homomorphism
R → AofDifferentialGradedAlgebra.baseHomand alongr' ↦ 1 ⊗ r'; the bottom edge is derived base change of the base ring in degree zero, read inD(R', d)throughDifferentialGradedAlgebra.degreeZeroBaseChangeUnitor, whose derived restriction is the equivalenceDifferentialGradedModule.degreeZeroBaseChangeEquivalence.Both composites are left derived functors of the same functor
K(A, d) ⥤ D(R', d),M ↦ M ⊗_R R': the comparisonc_Mof the plain functors is an isomorphism for everyM(DifferentialGraded.Bimodule.isIso_baseChangeStructureTensorTrans_app), and the left-hand composite's own comparison is invertible at the modules with property (P) — which is where the K-flatness ofAis used, throughDifferentialGradedModule.kFlat_toCochainComplex_of_propertyPFiltrationand part (3) in the formDifferentialGraded.Bimodule.isIso_derivedTensorBimoduleCounit_app_of_kFlat. So the square commutes by the uniqueness of a left derived functor.
def derivedBaseChangeRestrictionSquare
(hA : CochainComplex.KFlat.{u, u} (regularModule A).toCochainComplex) :
derivedBaseChangeFunctor A R' ⋙
derivedRestriction (tensorIncludeRightHom A (degreeZero R R')) ≅
derivedRestriction (baseHom A) ⋙
derivedBaseChangeFunctor (degreeZero R R) R' ⋙
derivedRestriction (tensorIncludeRightHom (degreeZero R R) (degreeZero R R'))
DifferentialGraded.Bimodule.baseChangeTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleTensorRestrictRight.lean, line 232. The attribute's comment: “the canonical map c_M of the PROOF, over R' — NOT any of parts (1), (2), (3). It is what identifies the functor derived in part (1), derivedBaseChangeFunctor_isLeftDerivedFunctor of BaseChange.lean, with the source's M |-> M (x)_R R'. Part (2) is derivedBaseChangeRestrictionSquare, part (3) isIso_derivedBaseChangeCounit_app_of_kFlat. The A'-linear form of this map, which is what the source states, is baseChangeTensorAlgebraIso”.
The canonical map
c_Min the proof of Stacks 0BYZ, overR'. LetR → R'be a ring map, let(A, d)be a differential gradedR-algebra and letA' = A ⊗_R R'be its base change. For a differential gradedA-moduleMthe differential gradedR'-module underlying the base changeM ⊗_A A'isM ⊗_R R'.The source's
c_M : M ⊗_R R' → M ⊗_A A'is a map of differential gradedA'-modules; this is that map after restricting the right action fromA'toR', which is where its content lies: restricting the right action does not change the relative tensor product (DifferentialGraded.Bimodule.tensorCompFunctorRestrictRightIso), and overR'the base-change bimodule is the one for whichM ⊗_A (A ⊗_R R') = M ⊗_R R'is already proved (DifferentialGraded.absBalanceIso). TheA'-linear statement, which needsM ⊗_R R'built as a differential gradedA ⊗_R R'-module and is proved by the universal property rather than by this transfer, isDifferentialGraded.Bimodule.baseChangeTensorAlgebraIsoinStacksFrontier/Algebra/DifferentialGraded/Module/BaseChangeAbsoluteTensor.lean.
def baseChangeTensorIso (M : DifferentialGradedModule.{u, u, u} A) :
(restrictScalarsFunctor (tensorIncludeRightHom A (degreeZero R R'))).obj
((tensorCompFunctor (baseChange A R')).obj M) ≅
M.absoluteTensor (degreeZero R R')
DifferentialGradedModule.kFlat_toCochainComplex_of_propertyPFiltration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/PropertyPKFlat.lean, line 95. The attribute's comment: “the K-flatness half of the claim in the PROOF — a differential graded A-module with property (P) is K-flat as a complex of R-modules. Not any of parts (1), (2), (3); part (1) is DifferentialGraded.Bimodule.derivedBaseChangeFunctor_isLeftDerivedFunctor”.
A differential graded module with property (P) over a differential graded algebra which is K-flat as a complex of
R-modules is itself K-flat as a complex ofR-modules. This is the K-flatness half of the claim in the proof of Stacks 0BYZ.The induction is
DifferentialGradedModule.propertyPFiltration_induction; its five obligations are, in order, that K-flatness is invariant under isomorphism, that it holds on a direct sum of shifts ofA, that it is stable under countable direct sums, and the two directions of two-out-of-three along an admissible short exact sequence. The hypothesis onAenters only in the second.
theorem kFlat_toCochainComplex_of_propertyPFiltration
(hA : CochainComplex.KFlat.{u, u} (regularModule A).toCochainComplex)
{P : DifferentialGradedModule A} (F : PropertyPFiltration P) :
CochainComplex.KFlat.{u, u} P.toCochainComplex
Tag 0BZ0, a lemma
Tag 0BZ0 in the Stacks Project.
DifferentialGraded.Bimodule.homDualBimodule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/InternalHomBimodule.lean, line 254. The attribute's comment: “the (B, A)-bimodule structure on S = Hom(T, B)”.
Stacks 0BZ0, first assertion. For a differential graded
(A, B)-bimoduleT, the internal homS = Hom_{Mod^{dg}_{(B, d)}}(T, B)is a differential graded(B, A)-bimodule: the rightA-action is precomposition with the left action ofAonT, and the leftB-action is postcomposition with left multiplication onB.
def homDualBimodule (T : Bimodule A B) : Bimodule B A
DifferentialGraded.Bimodule.derivedTensorHomDualFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/InternalHomTensorIso.lean, line 402. The attribute's comment: “the second assertion: the functorial isomorphism N ⊗_B^L S ≅ RHom(T, N)”.
Stacks 0BZ0, second assertion. Let
Rbe a ring, let(A, d)and(B, d)be differential gradedR-algebras and letTbe a differential graded(A, B)-bimodule. Assume
Tdefines a compact object ofD(B, d), andS = Hom_{Mod^{dg}_{(B, d)}}(T, B)representsR Hom(T, B)inD(A, d), that is, the comparison of Tag 09LI is invertible at the regular module.Then there is an isomorphism
N ⊗_B^𝐋 S ⟶ R Hom(T, N)functorial inNinD(B, d): the differential graded(B, A)-bimodule structure onSisDifferentialGraded.Bimodule.homDualBimodule, and the functorial isomorphism is an isomorphism of the two functorsD(B, d) ⥤ D(A, d)of Tag 09LS and Tag 09LI.The map itself is
DifferentialGraded.Bimodule.derivedEvalNatTrans: the composition pairing of Tag 09LC, read on differential graded modules and descended to the derived category, lifted along the localizationK(B, d) ⥤ D(B, d).
def derivedTensorHomDualFunctorIso (T : Bimodule A B)
(h1 : IsCompactObject.{u}
((toHomotopyCategory B ⋙ (quasiIsomorphisms' B).Q).obj T.rightModule))
(h2 : IsIso ((derivedHomData A B T.rightModule T.leftAction).comparison.app
((toHomotopyCategory B).obj (regularModule B)))) :
derivedTensorFunctor (homDualBimodule T) ≅
(derivedHomData A B T.rightModule T.leftAction).functor
Sources
Section22.34 Composition of derived tensor products#
Section 22.34 of the Stacks Project, Tag 0BZ1. 5 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0BZ2, an equation
Tag 0BZ2 in the Stacks Project.
DifferentialGraded.Bimodule.derivedTensorFunctorCounit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorFunctor.lean, line 138. The attribute's comment: “the canonical map from the derived to the plain tensor product”.
The canonical comparison from the derived tensor product to ordinary tensoring: the counit of the Kan extension defining
- ⊗_A^𝐋 N. Its components are the mapsP ⊗_A^𝐋 N → P ⊗_A NinD(B, d), which are isomorphisms exactly on the objects at which ordinary tensoring already computes the derived functor.
def derivedTensorFunctorCounit (N : Bimodule A B) :
(quasiIsomorphisms' A).Q ⋙ derivedTensorFunctor N ⟶ tensorFunctorToDerivedCategory N
Tag 0BZ3, a lemma
Tag 0BZ3 in the Stacks Project.
DifferentialGraded.Bimodule.compTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleComposition.lean, line 362. The attribute's comment: “the composite bimodule N'' = N (x)_B N' as an (A, C)-bimodule”.
Stacks Tag 0BZ3. The composite of a differential graded
(A, B)-bimoduleNwith a differential graded(B, C)-bimoduleN': the relative tensor productN ⊗_B N'of the rightB-module underlyingNwithN', carrying the leftA-action inherited fromN. This is the bimoduleN''of Tag 0BZ3.
def compTensor (N : Bimodule A B) (N' : Bimodule B C) : Bimodule A C
DifferentialGraded.Bimodule.derivedTensorFunctorCompTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorComposition.lean, line 291. The attribute's comment: “composition of the derived tensor functors”.
Stacks Tag 0BZ3. "Let
Rbe a ring. Let(A, d),(B, d), and(C, d)be differential gradedR-algebras. LetNbe a differential graded(A, B)-bimodule. LetN'be a differential graded(B, C)-bimodule. Assume that (0BZ2)N_B ⊗_B^𝐋 N' ⟶ (N ⊗_B N')_Cis an isomorphism. Then the compositionD(A, d) → D(B, d) → D(C, d)of- ⊗_A^𝐋 Nand- ⊗_B^𝐋 N'is isomorphic to- ⊗_A^𝐋 N''whereN'' = N ⊗_B N'."The bimodule
N''isDifferentialGraded.Bimodule.compTensor N N', the relative tensor product with the leftA-action inherited fromN, exactly as in the source; the isomorphism isDifferentialGraded.Bimodule.derivedTensorCompNatTrans, the transformation attached to the associativity isomorphism of the plain tensor functors by the universal property of Tag 09LS.
def derivedTensorFunctorCompTensorIso (N : Bimodule A B) (N' : Bimodule B C)
(hiso : IsIso ((derivedTensorFunctorCounit N').app
((toHomotopyCategory B).obj N.rightModule))) :
derivedTensorFunctor N ⋙ derivedTensorFunctor N' ≅
derivedTensorFunctor (compTensor N N')
Tag 0BZ4, an equation
Tag 0BZ4 in the Stacks Project.
DifferentialGraded.isIso_derivedTensorBaseChangeComparison_degreeZeroBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BaseChangeUnitBaseAlgebra.lean, line 246. The attribute's comment: “the canonical map is an isomorphism when the first algebra is the base ring in degree zero”.
The canonical map of Stacks 0BZ4 is an isomorphism when the first algebra is the base ring in degree zero. For differential graded
R-algebras(B, d)and(C, d), the map(R ⊗_R B)_B ⊗_B^𝐋 {}_B(B ⊗_R C)_C ⟶ (R ⊗_R B ⊗_R C)_CofD(C, d)is invertible, with nothing assumed aboutBorC.By
DifferentialGraded.Bimodule.isIso_derivedTensorBaseChangeComparison_iffthe assertion is that the comparison of Tag 09LS from the derived to the plain tensor product with{}_B(B ⊗_R C)_Cis invertible at the right differential gradedB-module(R ⊗_R B)_B. That module is the regular module, byDifferentialGraded.unitBaseChangeIso, and the regular module is orthogonal on the left to the acyclic modules by Tag 09K1, where the plain tensor product already computes the derived one.This is the hypothesis that Stacks 0BZ5 assumes and that Stacks 09S4 discharges from K-flatness of
C; over the base ring no K-flatness is needed.
theorem isIso_derivedTensorBaseChangeComparison_degreeZeroBase
(C : DifferentialGradedAlgebra.{u, u} R) :
IsIso (derivedTensorBaseChangeComparison (degreeZero R R) B C)
DifferentialGraded.tripleTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorAlgebraComparison.lean, line 574. The attribute's comment: “the identification of the plain tensor products”.
The identification
(A ⊗_R B)_B ⊗_B {}_B(B ⊗_R C)_C = (A ⊗_R B ⊗_R C)_C: the plain relative tensor product of the two base-change bimodules is the triple tensor product, as right differential gradedC-modules.
def tripleTensorIso : plainTensorObj A B C ≅ baseChangeModule (tensorProduct A B) C
DifferentialGraded.derivedTensorBaseChangeComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorAlgebraComparison.lean, line 600. The attribute's comment: “the canonical map in D(C, d)”.
The canonical map
(A ⊗_R B)_B ⊗_B^𝐋 {}_B(B ⊗_R C)_C ⟶ (A ⊗_R B ⊗_R C)_CinD(C, d). It is the comparison of the derived with the plain tensor product at the right differential gradedB-moduleA ⊗_R B, followed by the identification of the plain tensor product(A ⊗_R B)_B ⊗_B {}_B(B ⊗_R C)_CwithA ⊗_R B ⊗_R C.
def derivedTensorBaseChangeComparison :
(Bimodule.derivedTensorFunctor (baseChangeBimodule B C)).obj
((quasiIsomorphisms' B).Q.obj ((toHomotopyCategory B).obj (baseChangeModule A B))) ⟶
(quasiIsomorphisms' C).Q.obj
((toHomotopyCategory C).obj (baseChangeModule (tensorProduct A B) C))
Tag 0BZ5, a lemma
Tag 0BZ5 in the Stacks Project.
DifferentialGraded.Bimodule.derivedTensorFunctorCompIsoDegreeZeroBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BaseChangeUnitBaseAlgebra.lean, line 271. The attribute's comment: “unconditionally when the first algebra is the base ring in degree zero”.
Stacks 0BZ5 when the first algebra is the base ring in degree zero, with nothing assumed. For a differential graded
R-algebra(C, d), a differential graded(R, B)-bimoduleNand a differential graded(B, C)-bimoduleN', the composite of- ⊗_R^𝐋 N : D(R) ⥤ D(B, d)and- ⊗_B^𝐋 N' : D(B, d) ⥤ D(C, d)is the derived tensor functor of the differential graded(R, C)-bimoduleN'' = Ñ ⊗_B Ñ'of Stacks 0BZ3.This is
DifferentialGraded.Bimodule.derivedTensorFunctorCompIsoOfBaseChangewith its only hypothesis — the map of Tag 0BZ4, which Stacks 0BZ5 assumes to be an isomorphism — supplied byDifferentialGraded.isIso_derivedTensorBaseChangeComparison_degreeZeroBase. HereD(R)is the derived category of the base ring viewed as a differential graded algebra concentrated in degree zero, which is the derived category ofR-modules byDifferentialGradedModule.degreeZeroDerivedEquivalence.
def derivedTensorFunctorCompIsoDegreeZeroBase
(C : DifferentialGradedAlgebra.{u, u} R)
(N : Bimodule (degreeZero R R) B) (N' : Bimodule B C) :
derivedTensorFunctor N ⋙ derivedTensorFunctor N' ≅
derivedTensorFunctor (compTensorResolution N N')
DifferentialGraded.Bimodule.compTensorResolution, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BimoduleComposition.lean, line 415. The attribute's comment: “the bimodule N'' described in the proof”.
The bimodule
N''of Stacks Tag 0BZ5. Given a differential graded(A, B)-bimoduleNand a differential graded(B, C)-bimoduleN', it is the compositeÑ ⊗_B Ñ'of their property-(P) replacements, viewed as a differential graded(A, C)-bimodule.
def compTensorResolution (N : Bimodule A B) (N' : Bimodule B C) : Bimodule A C
DifferentialGraded.Bimodule.derivedTensorFunctorCompIsoOfBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorBaseChangeSecondVariable.lean, line 318. The attribute's comment: “the composite of the two derived tensor functors is the derived tensor functor of the composite bimodule, under the Tag 0BZ4 isomorphism that the source itself assumes”.
Stacks 0BZ5 with Tag 0BZ4 as its only hypothesis. For differential graded algebras
(A, d),(B, d)and(C, d)overRsuch that the canonical map(A ⊗_R B)_B ⊗_B^𝐋 {}_B(B ⊗_R C)_C ⟶ (A ⊗_R B ⊗_R C)_Cof Tag 0BZ4 is an isomorphism, the composite of- ⊗_A^𝐋 Nand- ⊗_B^𝐋 N'is isomorphic to- ⊗_A^𝐋 N''for the differential graded(A, C)-bimoduleN'' = Ñ ⊗_B Ñ'of the source.This is
DifferentialGraded.Bimodule.derivedTensorFunctorCompIsowith all four of its remaining inputs supplied: the second assertion of Tag 09S3 twice, Tag 0BZ3, and the dévissage of the present proof.
def derivedTensorFunctorCompIsoOfBaseChange
(hiso : IsIso (derivedTensorBaseChangeComparison A B C))
(N : Bimodule A B) (N' : Bimodule B C) :
derivedTensorFunctor N ⋙ derivedTensorFunctor N' ≅
derivedTensorFunctor (compTensorResolution N N')
Tag 09S4, a lemma
Tag 09S4 in the Stacks Project.
DifferentialGraded.Bimodule.isIso_derivedTensorBaseChangeComparison_of_kFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/BaseChangeTensorKFlat.lean, line 1032. The attribute's comment: “the canonical map (0BZ4) is an isomorphism”.
Stacks Tag 09S4, first conclusion. "Let
Rbe a ring. Let(A, d),(B, d), and(C, d)be differential gradedR-algebras. IfCis K-flat as a complex ofR-modules, then (0BZ4) is an isomorphism."The map of Tag 0BZ4 is
DifferentialGraded.derivedTensorBaseChangeComparison, the canonical map(A ⊗_R B)_B ⊗_B^𝐋 {}_B(B ⊗_R C)_C ⟶ (A ⊗_R B ⊗_R C)_CinD(C, d), and K-flatness isCochainComplex.KFlat(Tag 06XZ) of the complex ofR-modules underlyingC.The source's argument is followed: on underlying complexes, tensoring over
Bwith{}_B(B ⊗_R C)_Cis tensoring overRwithC, so by Tag 06Y0 it carries quasi-isomorphisms to quasi-isomorphisms; hence the plain tensor functor already computes the derived one and the comparison of Tag 09LS is invertible everywhere, in particular at(A ⊗_R B)_B, which byDifferentialGraded.Bimodule.isIso_derivedTensorBaseChangeComparison_iffis the assertion.
theorem isIso_derivedTensorBaseChangeComparison_of_kFlat
(A B C : DifferentialGradedAlgebra.{u, u} R)
(hC : CochainComplex.KFlat.{u, u} (regularModule C).toCochainComplex) :
IsIso (derivedTensorBaseChangeComparison A B C)
DifferentialGraded.Bimodule.derivedTensorFunctorCompIsoOfKFlatAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/DerivedTensorBaseChangeSecondVariable.lean, line 344. The attribute's comment: “the conclusion of Stacks 0BZ5 is valid when C is K-flat as a complex of R-modules”.
Stacks Tag 09S4, second conclusion. "Let
Rbe a ring. Let(A, d),(B, d),(C, d)be differential gradedR-algebras. IfCis K-flat as a complex ofR-modules, then (0BZ4) is an isomorphism and the conclusion of Lemma 0BZ5 is valid." This is the second half: ifCis K-flat as a complex ofR-modules, then for every differential graded(A, B)-bimoduleNand every differential graded(B, C)-bimoduleN'the composite of- ⊗_A^𝐋 Nand- ⊗_B^𝐋 N'is isomorphic to- ⊗_A^𝐋 N''for the differential graded(A, C)-bimoduleN'' = Ñ ⊗_B Ñ'ofDifferentialGraded.Bimodule.compTensorResolution, which is the conclusion of Tag 0BZ5.K-flatness of
Cis the only hypothesis, exactly as in the source. The first half of the tag,DifferentialGraded.Bimodule.isIso_derivedTensorBaseChangeComparison_of_kFlat, supplies the sole hypothesis of Tag 0BZ5 in the formDifferentialGraded.Bimodule.derivedTensorFunctorCompIsoOfBaseChange, whose own four inputs are discharged there by the second assertion of Tag 09S3 twice, Tag 0BZ3 and the dévissage above.
def derivedTensorFunctorCompIsoOfKFlatAlgebra
(hC : CochainComplex.KFlat.{u, u} (regularModule C).toCochainComplex)
(N : Bimodule A B) (N' : Bimodule B C) :
derivedTensorFunctor N ⋙ derivedTensorFunctor N' ≅
derivedTensorFunctor (compTensorResolution N N')
Sources
Section22.35 Variant of derived tensor product#
Section 22.35 of the Stacks Project, Tag 09LU. 6 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09LV, a lemma
Tag 09LV in the Stacks Project.
AlgebraicGeometry.RingedSite.tensorWithComplexDG, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplex/TensorHomAdjunction.lean, line 998. The attribute's comment: “the differential graded tensor functor”.
Tensoring with
K, as the DG left adjoint to the representable DG functorHom(K, -).
public noncomputable def tensorWithComplexDG
(K : CochainComplex (ModO.{u, v, w, t} X) ℤ) : TensorWithComplexData.{u, v, w, t, s, o} X R K
AlgebraicGeometry.RingedSite.tensorWithComplexDG_regular, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplex/TensorHomAdjunction.lean, line 1039. The attribute's comment: “the image of the regular module”.
Tensoring the regular endomorphism module with
KreturnsK.
public noncomputable def tensorWithComplexDG_regular
(K : CochainComplex (ModO.{u, v, w, t} X) ℤ) :
letI : Category (CompDG.{u, v, w, t, s, o} X R).Obj := (CompDG.{u, v, w, t, s, o} X
R).instCategoryComp
(((tensorWithComplexDG.{u, v, w, t, s, o} X R K).functor.obj
((Rep.{u, v, w, t, s, o} X R K).functor.obj (liftComplex.{u, v, w, t, s} X K)) :
(CompDG.{u, v, w, t, s, o} X R).Comp) ≅
(liftComplex.{u, v, w, t, s} X K : (CompDG.{u, v, w, t, s, o} X R).Comp))
AlgebraicGeometry.RingedSite.tensorWithComplexDG_preservesCoproducts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplex/TensorHomAdjunction.lean, line 1066. The attribute's comment: “preservation of direct sums”.
Tensoring with
Kcommutes with all small direct sums.
public theorem tensorWithComplexDG_preservesCoproducts
(K : CochainComplex (ModO.{u, v, w, t} X) ℤ) (I : Type i) :
PreservesColimitsOfShape (Discrete I)
(tensorWithComplexDG.{u, v, w, t, s, o} X R K).functor.onComp
Tag 09LW, a lemma
Tag 09LW in the Stacks Project.
AlgebraicGeometry.RingedSite.tensorWithComplexToDerivedCategory_negMor₃_distinguished, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexConeExactness.lean, line 50. The attribute's comment: “exactness against the cone triangles, up to the sign of the third arrow”.
The image in
D(O)of a triangle isomorphic to a cone triangle ofK(Mod_(E, d))is distinguished once its third arrow is negated: that negation turns a cone triangle into the triangle of an admissible short exact sequence, which tensoring withKkeeps distinguished.
theorem tensorWithComplexToDerivedCategory_negMor₃_distinguished
(T : Triangle (DifferentialGradedModule.HomotopyCategory.{0, max u v w t s, max u v w t s}
(Rep.{u, v, w, t, s, 0} X ℤ K).algebra))
(hT : T ∈ distinguishedConeTriangles.{0, max u v w t s, max u v w t s}
(A := (Rep.{u, v, w, t, s, 0} X ℤ K).algebra)) :
(tensorWithComplexToDerivedCategory.{u, v, w, t, s, 0} X ℤ K).mapTriangle.obj
(Triangle.mk T.mor₁ T.mor₂ (-T.mor₃)) ∈
distTriang (DerivedCategory (TensorModO.{u, v, w, t, s} X))
AlgebraicGeometry.RingedSite.tensorWithComplexHomotopy, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexHomotopy.lean, line 102. The attribute's comment: “the induced functor on homotopy categories”.
Stacks 09LW. The functor
K(Mod_(E, d)) ⥤ K(O)induced on homotopy categories by tensoring differential graded modules over the endomorphism differential graded algebra ofKwithK.
public noncomputable def tensorWithComplexHomotopy
(K : CochainComplex (ModO.{u, v, w, t} X) ℤ) :
DifferentialGradedModule.HomotopyCategory (Rep.{u, v, w, t, s, o} X R K).algebra ⥤
_root_.HomotopyCategory (TensorModO.{u, v, w, t, s} X) (ComplexShape.up ℤ)
AlgebraicGeometry.RingedSite.tensorWithComplexHomotopy_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexHomotopy.lean, line 118. The attribute's comment: “compatibility with the differential graded functor”.
The induced functor on homotopy categories is the lift, along the two quotient functors, of the ordinary functor on complexes attached to the differential graded tensor functor.
public theorem tensorWithComplexHomotopy_spec
(K : CochainComplex (ModO.{u, v, w, t} X) ℤ) :
DifferentialGradedModule.toHomotopyCategory (Rep.{u, v, w, t, s, o} X R K).algebra ⋙
tensorWithComplexHomotopy.{u, v, w, t, s, o} X R K =
DifferentialGradedModule.dgFunctorToComplexes
(tensorWithComplexDG.{u, v, w, t, s, o} X R K).functor ⋙
HomotopyCategory.quotient (TensorModO.{u, v, w, t, s} X) (ComplexShape.up ℤ)
AlgebraicGeometry.RingedSite.tensorWithComplexHomotopy_isTriangulated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexHomotopy.lean, line 154. The attribute's comment: “exactness of the induced functor”.
Stacks 09LW. Tensoring with
Kis an exact functor of triangulated categoriesK(Mod_(E, d)) ⥤ K(O): it commutes with the translation and carries distinguished triangles to distinguished triangles.
public theorem tensorWithComplexHomotopy_isTriangulated
(K : CochainComplex (ModO.{u, v, w, t} X) ℤ) :
(tensorWithComplexHomotopy.{u, v, w, t, s, o} X R K).IsTriangulated
Tag 09LX, a lemma
Tag 09LX in the Stacks Project.
AlgebraicGeometry.RingedSite.tensorWithComplexToDerivedCategory_isLeftDerivable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerived.lean, line 146. The attribute's comment: “existence in the pro-object sense”.
Stacks 09LX, in the source's own sense. The left derived functor of tensoring with
K, followed by localization of the target, is defined at every object ofK(Mod_(E, d)): the pro-object of its values along the quasi-isomorphisms into an object is essentially constant.
theorem tensorWithComplexToDerivedCategory_isLeftDerivable :
(tensorWithComplexToDerivedCategory.{u, v, w, t, s, o} X R K).IsLeftDerivable
(quasiIsomorphisms (Rep.{u, v, w, t, s, o} X R K).algebra)
AlgebraicGeometry.RingedSite.tensorWithComplexToDerivedCategory_hasLeftDerivedFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerived.lean, line 159. The attribute's comment: “existence of the total left derived functor”.
Stacks 09LX, in the Kan extension sense. Tensoring with
K, followed by localization of the target, has a total left derived functor onD(E, d).
theorem tensorWithComplexToDerivedCategory_hasLeftDerivedFunctor :
(tensorWithComplexToDerivedCategory.{u, v, w, t, s, o} X R K).HasLeftDerivedFunctor
(quasiIsomorphisms (Rep.{u, v, w, t, s, o} X R K).algebra)
AlgebraicGeometry.RingedSite.tensorWithComplexDerived, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerived.lean, line 170. The attribute's comment: “the derived tensor functor”.
Stacks 09LX. The derived tensor product
- ⊗_E^𝐋 K : D(E, d) ⥤ D(O): the total left derived functor of tensoring withKfollowed by localization of the target.
def tensorWithComplexDerived :
DifferentialGradedModule.derivedCategory (Rep.{u, v, w, t, s, o} X R K).algebra ⥤
DerivedCategory (TensorModO.{u, v, w, t, s} X)
AlgebraicGeometry.RingedSite.tensorWithComplexDerived_isLeftDerivedFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerived.lean, line 192. The attribute's comment: “universal property”.
The universal property of Stacks 09LX: the comparison exhibits
- ⊗_E^𝐋 Kas the left derived functor of tensoring withKfollowed by localization of the target.
instance tensorWithComplexDerived_isLeftDerivedFunctor :
(tensorWithComplexDerived.{u, v, w, t, s, o} X R K).IsLeftDerivedFunctor
(tensorWithComplexDerivedCounit.{u, v, w, t, s, o} X R K)
(quasiIsomorphisms (Rep.{u, v, w, t, s, o} X R K).algebra)
Tag 0CS6, a lemma
Tag 0CS6 in the Stacks Project.
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedExtMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerived.lean, line 343. The attribute's comment: “the induced maps on Ext”.
Stacks 0CS6. The maps
Ext^n_{D(E, d)}(M, N) → Ext^n_{D(𝒪)}(M ⊗_E^𝐋 K^•, N ⊗_E^𝐋 K^•)induced by the functor- ⊗_E^𝐋 K^•. WithExt^n_{D(C)}(X, Y) = Hom_{D(C)}(X, Y[n]), the map induced by a functor is its action on morphisms followed by its commutation with the translation, here that ofAlgebraicGeometry.RingedSite.tensorWithComplexDerivedCommShift.
def tensorWithComplexDerivedExtMap
{M N : DifferentialGradedModule.derivedCategory (Rep.{u, v, w, t, s, o} X R K).algebra} (n : ℤ)
(f : M ⟶ N⟦n⟧) :
(tensorWithComplexDerived.{u, v, w, t, s, o} X R K).obj M ⟶
((tensorWithComplexDerived.{u, v, w, t, s, o} X R K).obj N)⟦n⟧
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedExtMap_q, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerived.lean, line 378. The attribute's comment: “the maps on Ext are those induced by tensoring with K”.
Stacks 0CS6, the maps on
Extare those induced by tensoring withK. On a class coming fromK(Mod_(E, d)), the map induced by- ⊗_E^𝐋 Kagrees, through the comparison- ⊗_E^𝐋 K → - ⊗_E Kof Tag 09LX, with the map induced by the differential graded tensor functor of Tag 09LV read on homotopy categories. This is the compatibility of that comparison with the translation.
theorem tensorWithComplexDerivedExtMap_q
{P Y : DifferentialGradedModule.HomotopyCategory.{o, max u v w t s, max u v w t s}
(Rep.{u, v, w, t, s, o} X R K).algebra} (n : ℤ) (f : P ⟶ Y⟦n⟧) :
(tensorWithComplexDerivedCounit.{u, v, w, t, s, o} X R K).app P ≫
tensorWithComplexToDerivedCategoryExtMap.{u, v, w, t, s, o} X R K n f =
tensorWithComplexDerivedExtMap.{u, v, w, t, s, o} X R K n
((quasiIsomorphisms (Rep.{u, v, w, t, s, o} X R K).algebra).Q.map f ≫
(((quasiIsomorphisms (Rep.{u, v, w, t, s, o} X R K).algebra).Q).commShiftIso n).hom.app
Y) ≫
((tensorWithComplexDerivedCounit.{u, v, w, t, s, o} X R K).app Y)⟦n⟧'
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomSourceExtEquivOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerivedExtClauseOver.lean, line 230. The attribute's comment: “the source of the canonical map in D(R) is RHom(M, N), read on cohomology, for every M, N in D(E, d)”.
Stacks 0CS6, the source of the canonical map in
D(R), read on cohomology and for everyM,NinD(E, d). The degree-ncohomology of the source ofAlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomMapDerivedModulesOveris theExt-group
Ext^n_{D(E, d)}(M, N) = Hom_{D(E, d)}(M, N[n]),so that source really is
RHom(M, N)read on cohomology. It isAlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomSourceExtEquivread throughAlgebraicGeometry.RingedSite.homologyForgetEquivandAlgebraicGeometry.RingedSite.dgHomComplexModulesDerivedForgetIso, which say that forgetting theR-action changes neither the cohomology group nor the complex it is taken of. There is no hypothesis onMorN.
def tensorWithComplexDerivedHomSourceExtEquivOver
(M N : DifferentialGradedModule.derivedCategory (Rep.{u, u, u, u, u, o} X R K).algebra)
(n : ℤ) :
↥((DerivedCategory.homologyFunctor (ModuleCat.{u} R) n).obj
(DerivedCategory.Q.obj ((DifferentialGradedModule.dgCategory.{_, _, u}
(Rep.{u, u, u, u, u, o} X R K).algebra).homComplexModules
(DifferentialGradedModule.propertyPModel.{o, u, 0}
(Rep.{u, u, u, u, u, o} X R K).algebra M)
(DifferentialGradedModule.propertyPModel.{o, u, 0}
(Rep.{u, u, u, u, u, o} X R K).algebra N)))) ≃+ (M ⟶ N⟦n⟧)
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomTargetExtEquivOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerivedExtClauseOver.lean, line 263. The attribute's comment: “the target of the canonical map in D(R) read on cohomology: its degree-n cohomology is Ext^n_{D(O)}(M ⊗_E^𝐋 K, N ⊗_E^𝐋 K), for every M, N in D(E, d)”.
Stacks 0CS6, the target of the canonical map in
D(R), read on cohomology and for everyM,NinD(E, d). The degree-ncohomology of the target ofAlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomMapDerivedModulesOveris theExt-group
Ext^n_{D(O)}(M ⊗_E^𝐋 K^•, N ⊗_E^𝐋 K^•) = Hom_{D(O)}(M ⊗_E^𝐋 K^•, (N ⊗_E^𝐋 K^•)[n]).It is
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomTargetExtEquivread throughAlgebraicGeometry.RingedSite.homologyForgetEquivandAlgebraicGeometry.RingedSite.globalDerivedHomForgetAppOver. Together withAlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomSourceExtEquivOverit exhibits both cohomology modules of the clause as theExt-groups the clause compares; that the map between them is the one induced by- ⊗_E^𝐋 K^•isAlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomMapDerivedModulesOver_homology.There is no hypothesis on
MorN, and none on the site.
def tensorWithComplexDerivedHomTargetExtEquivOver
(M N : DifferentialGradedModule.derivedCategory (Rep.{u, u, u, u, u, o} X R K).algebra)
(n : ℤ) :
↥((DerivedCategory.homologyFunctor (ModuleCat.{u} R) n).obj
((scalarRestriction X R).mapDerivedCategory.obj
(((globalDerivedHomModules X).obj
(op ((tensorWithComplexDerived.{u, u, u, u, u, o} X R K).obj M))).obj
((tensorWithComplexDerived.{u, u, u, u, u, o} X R K).obj N)))) ≃+
((tensorWithComplexDerived.{u, u, u, u, u, o} X R K).obj M ⟶
((tensorWithComplexDerived.{u, u, u, u, u, o} X R K).obj N)⟦n⟧)
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomMapDerivedModulesOver_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerivedExtClauseOver.lean, line 299. The attribute's comment: “H^n of the canonical map is the Ext map induced by - ⊗_E^𝐋 K, for every M, N in D(E, d) and every n, in the source's D(R)”.
Stacks 0CS6, the central clause, in the source's
D(R). The degree-ncohomology of the canonical map
RHom(M, N) ⟶ RHom_O(M ⊗_E^𝐋 K^•, N ⊗_E^𝐋 K^•)of
D(R)is the map onExtinduced by the derived tensor product withK, for everyM,NinD(E, d)and everyn, with both sides read as theExt-groups they are byAlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomSourceExtEquivOverandAlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomTargetExtEquivOver.There is no hypothesis on
MorN: the statement is quantified over every object ofD(E, d), as the source's is, and the property-(P) reduction of the source's proof is performed by the choice of representativeDifferentialGradedModule.propertyPModel. Nor is anything assumed about the site.This is
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomMapDerived_homologyread over the source's base ring: the canonical map inD(R)forgets to theD(ℤ)-valued one byAlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomMapDerivedModulesOver_forget, and forgetting the scalars changes neither the cohomology groups nor the map between them.
theorem tensorWithComplexDerivedHomMapDerivedModulesOver_homology
(M N : DifferentialGradedModule.derivedCategory (Rep.{u, u, u, u, u, o} X R K).algebra)
(n : ℤ)
(η : ↥((DerivedCategory.homologyFunctor (ModuleCat.{u} R) n).obj
(DerivedCategory.Q.obj ((DifferentialGradedModule.dgCategory.{_, _, u}
(Rep.{u, u, u, u, u, o} X R K).algebra).homComplexModules
(DifferentialGradedModule.propertyPModel.{o, u, 0}
(Rep.{u, u, u, u, u, o} X R K).algebra M)
(DifferentialGradedModule.propertyPModel.{o, u, 0}
(Rep.{u, u, u, u, u, o} X R K).algebra N))))) :
tensorWithComplexDerivedHomTargetExtEquivOver X R K M N n
(ModuleCat.Hom.hom ((DerivedCategory.homologyFunctor (ModuleCat.{u} R) n).map
(tensorWithComplexDerivedHomMapDerivedModulesOver X R K M N)) η) =
tensorWithComplexDerivedExtMap.{u, u, u, u, u, o} X R K n
(tensorWithComplexDerivedHomSourceExtEquivOver X R K M N n η)
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomMapModulesOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerivedHomModulesOver.lean, line 213. The attribute's comment: “the canonical map out of the differential graded Hom complex, into RHom_O(M ⊗_E K, N ⊗_E K), in the source's D(R)”.
The canonical map in
D(R). The differential graded functor of Tag 09LV acts on theR-module-valued differential graded Hom complexes, and the Hom complex of two complexes ofO-modules overRmaps canonically to their global derived hom of Tag 0B6E read overR(AlgebraicGeometry.RingedSite.homComplexToGlobalDerivedHomModulesOver); the composite is this morphism ofD(R).Its source is the differential graded Hom complex of two differential graded modules, and its target is the global derived hom of the ordinary tensor products.
def tensorWithComplexDerivedHomMapModulesOver
(M N : (DifferentialGradedModule.dgCategory.{_, _, u}
(Rep.{u, u, u, u, u, o} X R K).algebra).Obj) :
DerivedCategory.Q.obj ((DifferentialGradedModule.dgCategory.{_, _, u}
(Rep.{u, u, u, u, u, o} X R K).algebra).homComplexModules M N) ⟶
(scalarRestriction X R).mapDerivedCategory.obj
(((globalDerivedHomModules X).obj (op (DerivedCategory.Q.obj
((tensorWithComplexDG.{u, u, u, u, u, o} X R K).functor.obj M)))).obj
(DerivedCategory.Q.obj
((tensorWithComplexDG.{u, u, u, u, u, o} X R K).functor.obj N)))
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomMapDerivedModulesOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerivedHomModulesOver.lean, line 330. The attribute's comment: “the canonical map RHom(M, N) ⟶ RHom_O(M ⊗_E^𝐋 K, N ⊗_E^𝐋 K) in the source's D(R), for every M, N in D(E, d)”.
The canonical map
RHom(M, N) ⟶ RHom_O(M ⊗_E^𝐋 K^•, N ⊗_E^𝐋 K^•)inD(R), for everyM,NinD(E, d). The canonical map ofAlgebraicGeometry.RingedSite.tensorWithComplexDerivedHomMapModulesOver, taken at the chosen property-(P) representatives ofMandN, is read into the global derived hom of the derived tensor products,
RHom(M, N) ⟶ RHom_O(M ⊗_E^𝐋 K^•, N ⊗_E^𝐋 K^•),by transporting both arguments along
AlgebraicGeometry.RingedSite.tensorWithComplexDerivedRepIso: in the contravariant argument the isomorphism is used as it stands, and in the covariant one it is inverted.There is no hypothesis on
MorN.
def tensorWithComplexDerivedHomMapDerivedModulesOver
(M N : DifferentialGradedModule.derivedCategory (Rep.{u, u, u, u, u, o} X R K).algebra) :
DerivedCategory.Q.obj
((DifferentialGradedModule.dgCategory.{_, _, u}
(Rep.{u, u, u, u, u, o} X R K).algebra).homComplexModules
(DifferentialGradedModule.propertyPModel.{o, u, 0}
(Rep.{u, u, u, u, u, o} X R K).algebra M)
(DifferentialGradedModule.propertyPModel.{o, u, 0}
(Rep.{u, u, u, u, u, o} X R K).algebra N)) ⟶
(scalarRestriction X R).mapDerivedCategory.obj
(((globalDerivedHomModules X).obj
(op ((tensorWithComplexDerived.{u, u, u, u, u, o} X R K).obj M))).obj
((tensorWithComplexDerived.{u, u, u, u, u, o} X R K).obj N))
Tag 09LY, a lemma
Tag 09LY in the Stacks Project.
AlgebraicGeometry.RingedSite.tensorWithComplexDerived_adj_derivedHomWithComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerivedAdjunction.lean, line 286.
The derived tensor--Hom adjunction: the derived tensor product
- ⊗_E^𝐋 K^• : D(E, d) ⥤ D(O)of Tag 09LX is left adjoint to derived HomRHom(K^•, -) : D(O) ⥤ D(E, d).
def tensorWithComplexDerived_adj_derivedHomWithComplex :
tensorWithComplexDerived.{u, v, w, t, s, 0} X ℤ K ⊣
derivedHomWithComplex.{u, v, w, t, s} X K
Tag 09LZ, a lemma
Tag 09LZ in the Stacks Project.
AlgebraicGeometry.RingedSite.tensorWithComplexDerived_fullyFaithful_of_ext, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorWithComplexDerivedFullyFaithfulDerivedHom.lean, line 192. The attribute's comment: “exactly the source's two hypotheses and nothing else: (1) is compactness of K in D(O), stated as such, and (2) is bijectivity of the functor on Hom(E, E[n]). The adjunction of Tag 09LY, the dévissage of Tag 0FQE, the direct sums and the weak generation of D(E, d), the commutation of RHom(K, -) with direct sums and the exactness of both functors (Tag 09LW, read through the sign-twisted identity of D(O)) are supplied by carriers of this library”.
Stacks 09LZ. "Let
(C, O)be a ringed site. LetKbe a complex ofO-modules. Assume (1)Krepresents a compact object ofD(O), and (2)E = Hom_{Comp^dg(O)}(K, K)computes the ext groups ofKinD(O). Then the functor- ⊗_E^𝐋 K : D(E, d) ⥤ D(O)of Lemma 09LX is fully faithful."The functor is the one Tag 09LX constructs,
AlgebraicGeometry.RingedSite.tensorWithComplexDerived, and the right adjoint through which the source's proof runs is the derived HomRHom(K, -)of Tag 09LK, the adjunction between them being the unconditionalAlgebraicGeometry.RingedSite.tensorWithComplexDerived_adj_derivedHomWithComplexof Tag 09LY.The source's two hypotheses are its two hypotheses here:
hcompactis (1), thatKrepresents a compact object ofD(O), andhExtis (2), read as the bijectivity of the functor on the morphism groupsHom_{D(E, d)}(E, E[n]). The source's proof uses (1) only through the commutation of the right adjoint with direct sums, and that commutation is derived here rather than assumed: the regular moduleEis a compact weak generator ofD(E, d)and- ⊗_E^𝐋 Ksends it toK, soCategoryTheory.Pretriangulated.preservesCoproducts_of_isCompactObject_mapapplies.Exactness of neither functor is assumed. The exactness of
- ⊗_E^𝐋 Kin the pretriangulated structure in force onD(E, d)is false, by a sign; what holds, unconditionally, is the exactness of its composite with the sign-twisted identity ofD(O)(AlgebraicGeometry.RingedSite.tensorWithComplexDerived_signTwist_isTriangulated), and the adjunction read between the twisted composites carries that to the right adjoint. SinceCategoryTheory.signTwistis the identity on objects and on morphisms, the full faithfulness obtained is full faithfulness of- ⊗_E^𝐋 Kitself. See the module's implementation notes.Everything else that
AlgebraicGeometry.RingedSite.tensorWithComplexDerived_fullyFaithfultakes as an argument is supplied here — the adjunction of Tag 09LY and its commutation with the translation, the dévissage of Tag 0FQE, the direct sums ofD(E, d)and the weak generation ofD(E, d)by the regular module. See the module's implementation notes.Full faithfulness is data, a chosen inverse to the action on morphism groups, so this is a definition.
def tensorWithComplexDerived_fullyFaithful_of_ext
(hcompact : IsCompactObject.{max u v w t s}
(DerivedCategory.Q.obj (liftComplex.{u, v, w, t, s} X K)))
(hExt : ∀ n : ℤ, Function.Bijective
(fun f : repRegularDerived.{u, v, w, t, s} X K ⟶
(repRegularDerived.{u, v, w, t, s} X K)⟦n⟧ =>
(tensorWithComplexDerived.{u, v, w, t, s, 0} X ℤ K).map f)) :
(tensorWithComplexDerived.{u, v, w, t, s, 0} X ℤ K).FullyFaithful
Sources
Section22.36 Characterizing compact objects#
Section 22.36 of the Stacks Project, Tag 09QZ. 6 tags here are carried by 23 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 09R0, a remark
Tag 09R0 in the Stacks Project.
Stacks.DifferentialGradedModule.SourceProjective.sourceProjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjective.lean, line 74. The attribute's comment: “source_projective_dg_modules”.
The source-projective objects of the homotopy category of right differential graded
A-modules: those from which morphisms are unchanged by passage to the derived category.
abbrev sourceProjective :
ObjectProperty (DifferentialGradedModule.HomotopyCategory.{u, v, w} A)
Stacks.DifferentialGradedModule.SourceProjective.sourceProjective_isClosedUnderIsomorphisms, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjective.lean, line 189. The attribute's comment: “triangulated_saturated”.
Stacks Project, Tag 09R0. Source-projectivity is invariant under isomorphism in the homotopy category.
instance sourceProjective_isClosedUnderIsomorphisms :
ObjectProperty.IsClosedUnderIsomorphisms (sourceProjective.{u, v, w} A)
Stacks.DifferentialGradedModule.SourceProjective.sourceProjective_isTriangulated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjective.lean, line 196. The attribute's comment: “triangulated_saturated”.
Stacks Project, Tag 09R0. The source-projective objects form a triangulated subcategory of the homotopy category.
instance sourceProjective_isTriangulated :
(sourceProjective.{u, v, w} A).IsTriangulated
Stacks.DifferentialGradedModule.SourceProjective.sourceProjective_isSaturated, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjective.lean, line 204. The attribute's comment: “triangulated_saturated”.
Stacks Project, Tag 09R0. The triangulated subcategory of source-projective objects is saturated.
instance sourceProjective_isSaturated :
(sourceProjective.{u, v, w} A).IsSaturated
Stacks.DifferentialGradedModule.SourceProjective.dualNumberAlgebra, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 143. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The dual-number algebra, as a differential graded algebra concentrated in degree zero.
noncomputable def dualNumberAlgebra :
DifferentialGradedAlgebra.{u, u} (DualNumber k)
Stacks.DifferentialGradedModule.SourceProjective.dualNumberAlgebra_carrier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 169. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The differential graded algebra has exactly the dual-number ring as its underlying algebra.
theorem dualNumberAlgebra_carrier : (dualNumberAlgebra k).A = DualNumber k
Stacks.DifferentialGradedModule.SourceProjective.dualNumberAlgebra_algebraMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 174. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The scalar structure on the concentrated algebra is the regular one.
theorem dualNumberAlgebra_algebraMap (r : DualNumber k) :
cast (dualNumberAlgebra_carrier k)
(algebraMap (DualNumber k) (dualNumberAlgebra k).A r) = r
Stacks.DifferentialGradedModule.SourceProjective.dualNumberAlgebra_grading, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 181. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The differential graded algebra is concentrated in degree zero.
theorem dualNumberAlgebra_grading (n : ℤ) :
(dualNumberAlgebra k).grading n = if n = 0 then ⊤ else ⊥
Stacks.DifferentialGradedModule.SourceProjective.dualNumberAlgebra_differential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 186. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The differential graded algebra has zero differential.
theorem dualNumberAlgebra_differential : (dualNumberAlgebra k).d = 0
Stacks.DifferentialGradedModule.SourceProjective.dualNumberModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 287. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The doubly infinite complex of free rank-one dual-number modules.
noncomputable def dualNumberModule :
DifferentialGradedModule.{u, u, u} (dualNumberAlgebra k)
Stacks.DifferentialGradedModule.SourceProjective.gradedFreeEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 357. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. An isomorphism from the graded module to a direct sum of shifted copies of its regular module.
noncomputable def gradedFreeEquiv :
(dualNumberModule k).M ≃ₗ[MulOpposite (dualNumberAlgebra k).A]
(⨁ _ : ℤ, MulOpposite (dualNumberAlgebra k).A)
Stacks.DifferentialGradedModule.SourceProjective.gradedFreeEquiv_mem_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 366. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The direct-sum coordinates identify each homogeneous piece with its corresponding shifted copy of the regular module.
theorem gradedFreeEquiv_mem_iff (n : ℤ) (x : (dualNumberModule k).M) :
x ∈ (dualNumberModule k).grading n ↔
∃ a : MulOpposite (dualNumberAlgebra k).A,
gradedFreeEquiv k x =
DirectSum.lof (MulOpposite (dualNumberAlgebra k).A) ℤ
(fun _ => MulOpposite (dualNumberAlgebra k).A) n a
Stacks.DifferentialGradedModule.SourceProjective.gradedPieceEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 385. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The chosen regular-module coordinates on a homogeneous component.
noncomputable def gradedPieceEquiv (n : ℤ) :
((dualNumberModule k).grading n) ≃ₗ[DualNumber k] DualNumber k
Stacks.DifferentialGradedModule.SourceProjective.dualNumberModule_differential, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 414. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. In the regular coordinates, the differential is multiplication by
ε.
theorem dualNumberModule_differential (n : ℤ) (x : (dualNumberModule k).grading n) :
gradedPieceEquiv k (n + 1) ((dualNumberModule k).gradedDifferential n x) =
DualNumber.eps * gradedPieceEquiv k n x
Stacks.DifferentialGradedModule.SourceProjective.dualNumberModule_acyclic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 459. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The doubly infinite complex is acyclic.
theorem dualNumberModule_acyclic :
DifferentialGradedModule.acyclic (dualNumberAlgebra k)
((DifferentialGradedModule.toHomotopyCategory (dualNumberAlgebra k)).obj
(dualNumberModule k))
Stacks.DifferentialGradedModule.SourceProjective.dualNumberModule_homotopy_id_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 531. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. The identity of the complex survives passage to the homotopy category.
theorem dualNumberModule_homotopy_id_ne_zero :
(𝟙 ((DifferentialGradedModule.toHomotopyCategory (dualNumberAlgebra k)).obj
(dualNumberModule k))) ≠ 0
Stacks.DifferentialGradedModule.SourceProjective.dualNumberModule_not_sourceProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DGA/SourceProjectiveCounterexample.lean, line 543. The attribute's comment: “dual_number_counterexample”.
Stacks Project, Tag 09R0. Graded freeness does not imply source-projectivity: the acyclic graded-free module above is not source-projective.
theorem dualNumberModule_not_sourceProjective :
¬ sourceProjective (dualNumberAlgebra k)
((DifferentialGradedModule.toHomotopyCategory (dualNumberAlgebra k)).obj
(dualNumberModule k))
Declarations registered for the tag:
Stacks.DifferentialGradedModule.SourceProjective.sourceProjective_iff_hom_acyclic_subsingleton, declared in the repository, registered withadd_to_stacksin StacksFrontier/Algebra/DGA/SourceProjective.lean, line 168 (StacksFrontier): “acyclic_target_criterion”.
Tag 09R1, a remark
Tag 09R1 in the Stacks Project.
DifferentialGradedModule.IsFinite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/Finite.lean, line 37. The attribute's comment: “finite_differential_graded_module”.
A differential graded module that is finitely generated as a right module over its differential graded algebra.
public abbrev IsFinite {R : Type u} [CommRing R] {A : DifferentialGradedAlgebra R}
(M : DifferentialGradedModule A) : Prop
Tag 09R2, a lemma
Tag 09R2 in the Stacks Project.
DifferentialGradedModule.exists_factorThrough_finiteSubfiltration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/CompactFiniteCellFiltration/FiniteSubfiltration.lean, line 707.
Stacks Tag 09R2. Let
(A, d)be a differential graded algebra, letEbe a compact object ofD(A, d)and letPbe a differential gradedA-module carrying a finite filtration0 = F₋₁P ⊆ F₀P ⊆ ⋯ ⊆ FₙP = Pby differential graded submodules whose graded pieces are direct sumsF_{i+1}P/FᵢP ≅ ⨁_{j ∈ Jᵢ} A[k_{i,j}]of shifts of the algebra. Then every morphismE ⟶ PofD(A, d)factors through a differential graded submoduleP' ⊆ Pwhose intersections with the filtration have graded pieces the finite subsums⨁_{j ∈ J'ᵢ} A[k_{i,j}], for finite subsetsJ'ᵢ ⊆ Jᵢ.The filtration of
P'is produced as the pullback of that ofP, and the identification of its graded pieces with the finite subsums is compatible with the given identification of the graded pieces ofP, through the inclusion of the subsum.
theorem exists_factorThrough_finiteSubfiltration (A : DifferentialGradedAlgebra.{u, u} R)
(n : ℕ) (P : DifferentialGradedModule.{u, u, u} A) (F : Filtration P ℕ)
(_hzero : IsZero (F.obj 0)) (htop : IsIso (F.ι.app (n + 1)))
(J : Fin (n + 1) → Type u) (k : ∀ i, J i → ℤ)
(e : ∀ i : Fin (n + 1), cokernel (F.diagram.map (homOfLE (Nat.le_succ i.val))) ≅
∐ fun j : J i => shift (regularModule A) (k i j))
(E : derivedCategory' A) [IsCompactObject.{u} E]
(f : E ⟶ (toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).obj P) :
∃ (P' : DifferentialGradedModule.{u, u, u} A) (p : P' ⟶ P),
Mono p ∧
∃ (F' : Filtration P' ℕ) (β : ∀ i : ℕ, F'.obj i ⟶ F.obj i),
(∀ i : ℕ, IsPullback (F'.ι.app i) (β i) p (F.ι.app i)) ∧
(∃ (J' : ∀ i : Fin (n + 1), Finset (J i))
(e' : ∀ i : Fin (n + 1),
cokernel (F'.diagram.map (homOfLE (Nat.le_succ i.val))) ≅
∐ fun j : ↑(J' i) => shift (regularModule A) (k i j.val))
(q : ∀ i : Fin (n + 1),
cokernel (F'.diagram.map (homOfLE (Nat.le_succ i.val))) ⟶
cokernel (F.diagram.map (homOfLE (Nat.le_succ i.val)))),
(∀ i : Fin (n + 1),
cokernel.π (F'.diagram.map (homOfLE (Nat.le_succ i.val))) ≫ q i =
β (i.val + 1) ≫ cokernel.π (F.diagram.map (homOfLE (Nat.le_succ i.val)))) ∧
(∀ i : Fin (n + 1),
(e' i).hom ≫ Sigma.map' (fun j : ↑(J' i) => j.val) (fun _ => 𝟙 _) =
q i ≫ (e i).hom)) ∧
∃ g : E ⟶ (toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).obj P',
g ≫ (toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).map p = f
Tag 09R3, a proposition
Tag 09R3 in the Stacks Project.
DifferentialGradedModule.isCompactObject_iff_exists_retract_hasFiniteCellFiltration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/CompactFiniteCellFiltration/CompactObjects.lean, line 777.
Stacks Tag 09R3. "Let
(A, d)be a differential graded algebra. LetEbe an object ofD(A, d). The following are equivalent: (1)Eis a compact object, and (2)Eis a direct summand of an object which is represented by a differential graded modulePwhich has a finite filtrationF_•by differential graded submodules such thatF_iP/F_{i-1}Pare finite direct sums of shifts ofA."Condition (2) is read as:
Eis a retract of the image of a module with a finite cell filtration,DifferentialGradedModule.HasFiniteCellFiltration. A retract is the same thing as a direct summand here, the derived category of a differential graded algebra being idempotent complete ([Stacks, Tag 05QW]); the retract formulation is the one both implications produce and consume.
theorem isCompactObject_iff_exists_retract_hasFiniteCellFiltration
(A : DifferentialGradedAlgebra.{u, u} R) (E : derivedCategory' A) :
IsCompactObject.{u} E ↔
∃ P : DifferentialGradedModule.{u, u, u} A, HasFiniteCellFiltration P ∧
∃ (i : E ⟶ (toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).obj P)
(r : (toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).obj P ⟶ E), i ≫ r = 𝟙 E
Tag 09RA, a lemma
Tag 09RA in the Stacks Project.
DifferentialGradedModule.exists_subsingleton_hom_of_isZero_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/CompactCohomologyWindow.lean, line 315.
Stacks Tag 09RA. For every compact object
Eof the derived category of a differential graded algebra there are integersa ≤ bsuch thatHom_{D(A, d)}(E, M) = 0for every objectMwhose cohomologyHⁱ(M)vanishes for alli ∈ [a, b].If no such interval existed, then for each
nthere would be an objectMₙwith vanishing cohomology on[-n, n]and a nonzero morphismE ⟶ Mₙ. In each fixed degree only finitely many of theMₙhave nonvanishing cohomology, soDifferentialGradedModule.finite_setOf_ne_zero_of_isCompactObjectapplies to the family and contradicts the fact that all of the chosen morphisms are nonzero.
theorem exists_subsingleton_hom_of_isZero_homology (A : DifferentialGradedAlgebra.{u, u} R)
(E : derivedCategory' A) [IsCompactObject.{u} E] :
∃ a b : ℤ, a ≤ b ∧ ∀ M : derivedCategory' A,
(∀ i : ℤ, a ≤ i → i ≤ b → IsZero (M.as.obj.as.toCochainComplex.homology i)) →
Subsingleton (E ⟶ M)
Tag 09RB, a lemma
Tag 09RB in the Stacks Project.
DifferentialGradedModule.exists_retract_isFiniteFreeAsGradedModule_of_isCompactObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/CompactFiniteFree.lean, line 634. The attribute's comment: “(1) ⟹ (2), corrected: a compact object is a DIRECT SUMMAND of (the image of) a differential graded module which is finite FREE as a graded module and satisfies Hom_K = Hom_D; the literal statement, with 'represented by' and 'finite projective', is a mistake in the source — see the refutation in Examples/Algebra/CompactObjectNoFiniteProjectiveModel.lean”.
[Stacks, Tag 09RB], the implication (1) ⟹ (2), in the corrected form that the source's own proof establishes. A compact object
EofD(A, d)is a direct summand inD(A, d)of the image of a differential gradedA-modulePwhich is finite free as a gradedA-module and satisfiesHom_{K(A, d)}(P, M) = Hom_{D(A, d)}(P, M)for every differential gradedA-moduleM.The literal statement of the source — that
Ecan be represented by such aP, with finite projective in place of finite free — is false, and is a mistake in the Stacks Project, pending review: it is contradicted by the source's own [Stacks, Tag 09R5], whose compact object over the bounded algebraA = k[x, y]/(y²)of Tag 09R4 has no finite graded-projective representative at all. That refutation isStacks.Examples.not_forall_exists_finite_gradedProjective_of_isCompactObject, inStacksFrontier/Examples/Algebra/CompactObjectNoFiniteProjectiveModel.lean. The two differences below are exactly what the argument of Tag 09R3 delivers, and the counterexample is consistent with them: thereE = Ker(x)is a direct summand of the regular module, which is finite free.The statement is unconditional: the boundedness hypothesis "
A^n = 0for|n| ≫ 0" of the source is not assumed and is not used anywhere in the proof, which is part of why the literal statement cannot be rescued by it.The proof composes the two implications the chapter already has. [Stacks, Tag 09R3],
DifferentialGradedModule.isCompactObject_iff_exists_retract_hasFiniteCellFiltration, makesEa retract of the image of a modulePwith a finite cell filtration; such aPis finite free as a graded module, because its filtration is built out of finitely many finite direct sums of shifts of the algebra and splits as a filtration of graded modules (DifferentialGradedModule.isFiniteFreeAsGradedModule_of_hasFiniteCellFiltration); and it is orthogonal on the left to the acyclic modules, so morphisms out of it are not changed by localization (DifferentialGradedModule.bijective_q_map_of_hasFiniteCellFiltration, Tag 09KY), which is the condition of [Stacks, Tag 09R0].The converse holds too, as
DifferentialGradedModule.isCompactObject_of_retract_isFiniteFreeAsGradedModule, so the tag's equivalence is restored by the correction; the registration of (2) ⟹ (1) stays on the source's own spelling of condition (2), namelyDifferentialGradedModule.isCompactObject_of_exists_finite_projective_representative.
theorem exists_retract_isFiniteFreeAsGradedModule_of_isCompactObject
(A : DifferentialGradedAlgebra.{u, u} R) (E : derivedCategory' A)
(hE : IsCompactObject.{u} E) :
∃ P : DifferentialGradedModule.{u, u, u} A, IsFiniteFreeAsGradedModule P ∧
(∀ M : DifferentialGradedModule.{u, u, u} A, Function.Bijective
(((quasiIsomorphisms' A).Q).map :
((toHomotopyCategory A).obj P ⟶ (toHomotopyCategory A).obj M) → _)) ∧
∃ (i : E ⟶ (toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).obj P)
(r : (toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).obj P ⟶ E), i ≫ r = 𝟙 E
DifferentialGradedModule.isCompactObject_of_exists_finite_projective_representative, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/DifferentialGraded/Module/CompactFiniteProjective.lean, line 293. The attribute's comment: “(2) ⟹ (1)”.
[Stacks, Tag 09RB], the implication (2) ⟹ (1). "Let
(A, d)be a differential graded algebra. Assume thatA^n = 0for|n| ≫ 0. LetEbe an object ofD(A, d). The following are equivalent: (1)Eis a compact object, and (2)Ecan be represented by a differential gradedA-modulePwhich is finite projective as a gradedA-module and satisfiesHom_{K(A, d)}(P, M) = Hom_{D(A, d)}(P, M)for every differential gradedA-moduleM."Condition (2) is read as the conjunction of:
Pis finite, that is finitely generated as a rightA-module (DifferentialGradedModule.IsFinite, Tag 09R1);Pis projective as a graded module (Stacks.DifferentialGraded.DGModule.IsProjectiveAsGradedModule, Tag 09K0); the localization functor is bijective on morphisms out of the class ofPinto the class of every differential graded module (Tag 09R0); andEis isomorphic inD(A, d)to the class ofP.The boundedness of
Aand the graded projectivity ofPare hypotheses of the source statement and are recorded here, but this implication uses neither: finiteness together with the comparison of morphism groups already gives compactness.
theorem isCompactObject_of_exists_finite_projective_representative
(A : DifferentialGradedAlgebra.{u, u} R) (c : ℤ)
(_hA : ∀ n : ℤ, c ≤ |n| → A.grading n = ⊥) (E : derivedCategory' A)
(hE : ∃ P : DifferentialGradedModule.{u, u, u} A, IsFinite P ∧
Stacks.DifferentialGraded.DGModule.IsProjectiveAsGradedModule.{u, u, u, u}
(Unbundled.module P) ∧
(∀ M : DifferentialGradedModule.{u, u, u} A, Function.Bijective
(((quasiIsomorphisms' A).Q).map :
((toHomotopyCategory A).obj P ⟶ (toHomotopyCategory A).obj M) → _)) ∧
Nonempty (E ≅ (toHomotopyCategory A ⋙ (quasiIsomorphisms' A).Q).obj P)) :
IsCompactObject.{u} E
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.