Transporting homogeneous morphisms across chosen shifts

IsShiftBy.mapShift moves a closed degree-zero morphism across two chosen shifts. A shift functor has to move morphisms of every degree, and this file does that.

One characterising square, and everything else follows

shiftMap is written down as s.inv ≫ f ≫ s'.hom, but nothing below unfolds that formula. What is used is that it is the unique degree-p morphism c with

s.hom ≫ c = f ≫ s'.hom,

uniqueness holding because s.inv ≫ s.hom = 𝟙 makes left composition with s.hom injective. Identity, composition and the differential are then three short verifications of that square rather than three associativity chains.

The differential is where the sign appears

s.hom and s'.hom are closed, so differentiating the square leaves one Leibniz term, and with the repository's convention δ(a ≫ b) = a ≫ δb + (-1)^|b| δa ≫ b and |s'.hom| = -n that term carries (-1)^n. So

δ (shiftMap p f) = (-1)^n • shiftMap (p+1) (δ f),

and not shiftMap (p+1) (δ f). A shift functor must therefore multiply shiftMap by a sign depending on the degree; (-1)^(n * p) is the unique solution, and Pretriangulated/FunctorCategory.lean uses it. This is the reason the naive formula does not define a dg functor.

theorem CategoryTheory.dgComp_units_smul_left {C : Type u} [DGCategory C] {W X Y : C} (p q r : ℤ) (h : p + q = r) (c : ℤˣ) (f : ↑((DGCategoryStruct.dgHom W X).X p)) (g : ↑((DGCategoryStruct.dgHom X Y).X q)) : ((DGCategoryStruct.dgComp p q r h) (c • f)) g = c • ((DGCategoryStruct.dgComp p q r h) f) g

dgComp commutes with the sign action in its first argument.

theorem CategoryTheory.dgComp_units_smul_right {C : Type u} [DGCategory C] {W X Y : C} (p q r : ℤ) (h : p + q = r) (c : ℤˣ) (f : ↑((DGCategoryStruct.dgHom W X).X p)) (g : ↑((DGCategoryStruct.dgHom X Y).X q)) : ((DGCategoryStruct.dgComp p q r h) f) (c • g) = c • ((DGCategoryStruct.dgComp p q r h) f) g

dgComp commutes with the sign action in its second argument.

noncomputable def CategoryTheory.IsShiftBy.shiftMap {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (p : ℤ) (f : ↑((DGCategoryStruct.dgHom A B).X p)) : ↑((DGCategoryStruct.dgHom A' B').X p)

Transport a homogeneous morphism across chosen shifts of its source and target: go back along the source's shift, across, and out along the target's.

mapShift is this at degree zero. The sign that makes the construction a dg functor is not included here; see the module docstring.

Equations

• s.shiftMap s' p f = ((CategoryTheory.DGCategoryStruct.dgComp (n + p) (-n) p ⋯) (((CategoryTheory.DGCategoryStruct.dgComp n p (n + p) ⋯) s.inv) f)) s'.hom

theorem CategoryTheory.IsShiftBy.hom_comp_shiftMap {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (p m : ℤ) (hm : -n + p = m) (hm' : p + -n = m) (f : ↑((DGCategoryStruct.dgHom A B).X p)) : ((DGCategoryStruct.dgComp (-n) p m hm) s.hom) (s.shiftMap s' p f) = ((DGCategoryStruct.dgComp p (-n) m hm') f) s'.hom

The characterising square. s.hom followed by the transported morphism is the morphism followed by s'.hom.

theorem CategoryTheory.IsShiftBy.shiftMap_unique {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (p m : ℤ) (hm : -n + p = m) (hm' : p + -n = m) (f : ↑((DGCategoryStruct.dgHom A B).X p)) (c : ↑((DGCategoryStruct.dgHom A' B').X p)) (h : ((DGCategoryStruct.dgComp (-n) p m hm) s.hom) c = ((DGCategoryStruct.dgComp p (-n) m hm') f) s'.hom) : s.shiftMap s' p f = c

The transported morphism is the only one making that square commute.

Left composition with s.hom is injective because s.inv is a left inverse for it, so the square determines c. Every property of shiftMap below is proved by checking the square for a candidate.

theorem CategoryTheory.IsShiftBy.shiftMap_add {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (p : ℤ) (f g : ↑((DGCategoryStruct.dgHom A B).X p)) : s.shiftMap s' p (f + g) = s.shiftMap s' p f + s.shiftMap s' p g

Transport is additive in the morphism.

@[simp]

theorem CategoryTheory.IsShiftBy.shiftMap_zero {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (p : ℤ) : s.shiftMap s' p 0 = 0

theorem CategoryTheory.IsShiftBy.shiftMap_units_smul {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (p : ℤ) (c : ℤˣ) (f : ↑((DGCategoryStruct.dgHom A B).X p)) : s.shiftMap s' p (c • f) = c • s.shiftMap s' p f

Transport commutes with the sign action.

theorem CategoryTheory.IsShiftBy.shiftMap_id {C : Type u} [DGCategory C] {A A' : C} {n : ℤ} (s : IsShiftBy A n A') : s.shiftMap s 0 (DGCategoryStruct.dgId A) = DGCategoryStruct.dgId A'

Transport takes the identity to the identity.

theorem CategoryTheory.IsShiftBy.shiftMap_comp {C : Type u} [DGCategory C] {A A' B B' E E' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (s'' : IsShiftBy E n E') (p q r : ℤ) (h : p + q = r) (f : ↑((DGCategoryStruct.dgHom A B).X p)) (g : ↑((DGCategoryStruct.dgHom B E).X q)) : s.shiftMap s'' r (((DGCategoryStruct.dgComp p q r h) f) g) = ((DGCategoryStruct.dgComp p q r h) (s.shiftMap s' p f)) (s'.shiftMap s'' q g)

Transport preserves the graded composition.

theorem CategoryTheory.IsShiftBy.shiftMap_comp_inv {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (p m : ℤ) (hm : p + n = m) (hm' : n + p = m) (f : ↑((DGCategoryStruct.dgHom A B).X p)) : ((DGCategoryStruct.dgComp p n m hm) (s.shiftMap s' p f)) s'.inv = ((DGCategoryStruct.dgComp n p m hm') s.inv) f

Transport followed by the target's inverse is the source's inverse followed by the morphism. The two hom/inv factors in the middle cancel, and this is the form the shift witness's surjectivity argument needs.

theorem CategoryTheory.IsShiftBy.shiftMap_d {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (p : ℤ) (f : ↑((DGCategoryStruct.dgHom A B).X p)) : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom A' B').d p (p + 1))) (s.shiftMap s' p f) = n.negOnePow • s.shiftMap s' (p + 1) ((AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom A B).d p (p + 1))) f)

Transport does not commute with the differential; it anticommutes by (-1)^n.

Both s.hom and s'.hom are closed, so differentiating the characterising square leaves the single Leibniz term carrying (-1)^{-n} = (-1)^n. This is the identity that forces a shift functor's sign, and it is why the naive formula does not define a dg functor.

theorem CategoryTheory.IsShiftBy.comp_inv_naturality {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (t : IsShiftBy B n B') {V V' : C} (q p r m rq : ℤ) (hp : q + n = p) (hrq : r + q = rq) (hm : r + p = m) (hm' : p + r = m) (w : ↑((DGCategoryStruct.dgHom V V').X r)) (α : ↑((DGCategoryStruct.dgHom V A').X q)) (β : ↑((DGCategoryStruct.dgHom V' B').X q)) (g : ↑((DGCategoryStruct.dgHom A B).X r)) (hnat : ((DGCategoryStruct.dgComp r q rq hrq) w) β = (q * r).negOnePow • ((DGCategoryStruct.dgComp q r rq ⋯) α) ((n * r).negOnePow • s.shiftMap t r g)) : ((DGCategoryStruct.dgComp r p m hm) w) (((DGCategoryStruct.dgComp q n p hp) β) t.inv) = (p * r).negOnePow • ((DGCategoryStruct.dgComp p r m hm') (((DGCategoryStruct.dgComp q n p hp) α) s.inv)) g

Naturality transports back along the inverses.

Suppose a degree-q family is natural for the transported morphism s.shiftMap t r g (with the shift functor's sign (-1)^(n r) in place). Then the family composed with the inverses is natural for g itself, at degree p = q + n, and the sign becomes (-1)^(p r).

This is the step that makes right composition with a shift element surjective on natural transformations, and it is stated here, with every object a variable, on purpose: in the dg category of dg functors the same identity has (F.shiftedFunctor n).obj X and F.shiftObj n X in the two arguments, which are definitionally but not syntactically equal, and rw cannot build a motive over such a goal.

theorem CategoryTheory.IsShiftBy.comp_inv_comp_hom {C : Type u} [DGCategory C] {A A' : C} {n : ℤ} (s : IsShiftBy A n A') {V : C} (q p : ℤ) (hp : q + n = p) (hq : p + -n = q) (α : ↑((DGCategoryStruct.dgHom V A').X q)) : ((DGCategoryStruct.dgComp p (-n) q hq) (((DGCategoryStruct.dgComp q n p hp) α) s.inv)) s.hom = α

Composing with the inverse and then with the shift element again is the identity. Stated with the ambient object a variable for the same reason as comp_inv_naturality.

Comparing two chosen shifts, and composing shifts

Everything above fixes one shift of the source and one of the target. A shift functor needs two more things: that the shifts of one object by n form a contractible groupoid, which IsShiftBy.compare already says, and that shifting by n and then by m agrees with shifting by n + m. The lemmas here make both statements natural in the morphism rather than true only at each object.

theorem CategoryTheory.IsShiftBy.hom_comp_compare {C : Type u} [DGCategory C] {A A' : C} {n : ℤ} {A'' : C} (s : IsShiftBy A n A') (t : IsShiftBy A n A'') : ((DGCategoryStruct.dgComp (-n) 0 (-n) ⋯) s.hom) (s.compare t) = t.hom

The characterising property of compare. Composing the first shift element with the comparison gives the second; this is s.hom ≫ s.inv = 𝟙 and nothing else. Every use of compare below reduces to it.

theorem CategoryTheory.IsShiftBy.shiftMap_compare {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} {A'' B'' : C} (s : IsShiftBy A n A') (t : IsShiftBy A n A'') (s' : IsShiftBy B n B') (t' : IsShiftBy B n B'') (p : ℤ) (f : ↑((DGCategoryStruct.dgHom A B).X p)) : ((DGCategoryStruct.dgComp p 0 p ⋯) (s.shiftMap s' p f)) (s'.compare t') = ((DGCategoryStruct.dgComp 0 p p ⋯) (s.compare t)) (t.shiftMap t' p f)

Transport commutes with the comparison of chosen shifts.

Both sides are the transport of f from s to t', because both satisfy that one characterising square; shiftMap_unique is applied twice and the two results are compared. This is what lets a shift functor be built from chosen witnesses without the choice mattering, in every degree and not only in degree zero.

theorem CategoryTheory.IsShiftBy.comp'_shiftMap {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} {E E'' : C} {m : ℤ} (s : IsShiftBy A n A') (u : IsShiftBy A' m E) (s' : IsShiftBy B n B') (u' : IsShiftBy B' m E'') (nm : ℤ) (hnm : n + m = nm) (p : ℤ) (f : ↑((DGCategoryStruct.dgHom A B).X p)) : (s.comp' u nm hnm).shiftMap (s'.comp' u' nm hnm) p f = u.shiftMap u' p (s.shiftMap s' p f)

Transport across a composite shift is the two transports in turn.

IsShiftBy.comp' composes two shift witnesses; this says its shiftMap is the composite of the two shiftMaps. Together with shiftMap_compare it is the whole content of a shift functor being additive in the degree.

theorem CategoryTheory.IsShiftBy.comp'_shiftMap_smul {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} {E E'' : C} {m : ℤ} (s : IsShiftBy A n A') (u : IsShiftBy A' m E) (s' : IsShiftBy B n B') (u' : IsShiftBy B' m E'') (nm : ℤ) (hnm : n + m = nm) (p : ℤ) (f : ↑((DGCategoryStruct.dgHom A B).X p)) : (m * p).negOnePow • u.shiftMap u' p ((n * p).negOnePow • s.shiftMap s' p f) = (nm * p).negOnePow • (s.comp' u nm hnm).shiftMap (s'.comp' u' nm hnm) p f

The two transports and their two signs, merged.

This is comp'_shiftMap with the shift functor's Koszul signs already in place: shifting by n contributes (-1)^(n p) and then shifting by m contributes (-1)^(m p), and the product is the (-1)^(nm p) of the single shift because n p + m p = nm p. Stated here, with every object a variable, so that the functor-category proof can apply it instead of rewriting across two spellings of the same shifted object.

Coherence for three composed shifts

The binary comparison for shifted dg functors is canonical only if its two threefold composites agree. The two lemmas below isolate the remaining pointwise content of that coherence. They are stated for arbitrary shift witnesses so the functor-category proof does not have to unfold the chosen shifted objects.

theorem CategoryTheory.IsShiftBy.shiftMap_compare_compOfDegree {C : Type u} [DGCategory C] {A A' E : C} {n : ℤ} {A'' E'' : C} {m nm : ℤ} (s : IsShiftBy A n A') (t : IsShiftBy A n A'') (u : IsShiftBy A' m E) (v : IsShiftBy A'' m E'') (hnm : n + m = nm) : u.shiftMap v 0 (s.compare t) = (s.comp' u nm hnm).compare (t.comp' v nm hnm)

The degree-zero transport of a comparison is the comparison of the composite witnesses.

The total degree nm is explicit because the associativity proof compares the propositionally equal indices (n + m) + k and n + (m + k). The proof uses the characterising square of shiftMap; this is the all-degree counterpart of mapShift_compare_comp'.

theorem CategoryTheory.IsShiftBy.compare_compLeftOfDegree {C : Type u} [DGCategory C] {A A' : C} {n : ℤ} {Z Z' : C} {m nm : ℤ} (s : IsShiftBy A n A') (u : IsShiftBy A' m Z) (v : IsShiftBy A' m Z') (hnm : n + m = nm) : (s.comp' u nm hnm).compare (s.comp' v nm hnm) = u.compare v

Prefixing two witnesses by the same shift does not change their comparison: the common shift element and its inverse cancel. The explicit total degree keeps the statement usable under either bracketing of three integer shifts.

theorem CategoryTheory.IsShiftBy.shiftMap_zero_eq_mapShift {C : Type u} [DGCategory C] {A A' B B' : C} {n : ℤ} (s : IsShiftBy A n A') (s' : IsShiftBy B n B') (f : ↑((DGCategoryStruct.dgHom A B).X 0)) : s.shiftMap s' 0 f = s.mapShift s' f

In degree zero, transport is IsShiftBy.mapShift.

mapShift is the degree-zero transport that Pretriangulated/Basic.lean already had, and shiftMap is the all-degree one. They are the same map, but not definitionally: shiftMap indexes its middle composite by n + p, which at p = 0 is n + 0 and is only propositionally n. shiftMap_unique crosses that gap, because its result index is a free variable.

theorem CategoryTheory.IsShiftBy.shiftMap_self {C : Type u} [DGCategory C] {A B : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom A B).X p)) : (self A).shiftMap (self B) p f = f

Transport across the identity shift is the identity.