derived_cat

Stream: condensed mathematics

[Scott Morrison]

#13262 is a PR I'd like to land in mathlib before I finish off the triangulated.pretriangulated (bounded_derived_category A) instance in derived/derivated_cat.lean. This instance is essentially done now.

[Scott Morrison]

@Adam Topaz, I'd like to add the following lemmas about lift:

@[simp]
lemma lift_self {P X : 𝒦} [is_K_projective P.val] (g : P ⟶ X) [is_quasi_iso g] :
  lift g g = 𝟙 _ :=
(lift_unique _ _ _ (by simp)).symm

@[simp]
lemma lift_comp {P X Y : 𝒦} [is_K_projective P.val] (f : P ⟶ X) (g : X ⟶ Y) [is_quasi_iso g] :
  lift (f ≫ g) g = f :=
(lift_unique _ _ _ (by simp)).symm

@[simp, reassoc]
lemma lift_comp_lift_self {P X Y Z : 𝒦} [is_K_projective P.val] [is_K_projective X.val]
  (f : P ⟶ Y) (g : X ⟶ Y) [is_quasi_iso g] (k : Z ⟶ Y) [is_quasi_iso k] :
  lift f g ≫ lift g k = lift f k :=
lift_unique _ _ _ (by simp)

@[simp, reassoc]
lemma lift_comp_lift_comp {P W X Y Z : 𝒦} [is_K_projective P.val] [is_K_projective X.val]
  (f : P ⟶ Y) (g : X ⟶ Y) [is_quasi_iso g] (h : Y ⟶ Z) (k : W ⟶ Z) [is_quasi_iso k] :
  lift f g ≫ lift (g ≫ h) k = lift (f ≫ h) k :=
lift_unique _ _ _ (by simp)

Any objections?

[Johan Commelin]

@Scott Morrison I reviewed that PR, but CI is unhappy. So I gave a bors d+

[Scott Morrison]

It seems the linter crashed? I can't view the lint output. I'll restart CI.

[Adam Topaz]

Those lemmas look good to me!

[Scott Morrison]

I'm pretty unhappy with the current approach to constructing the shift on bounded_derived_category. It runs into lots of definitional equality problems, and suffers from the fact that people have previously abused local attribute [reducible] endofunctor_monoidal_category in setting up the theory of shifts....

I'd like to rip this out and start over, by showing that a full subcategory of a category with a shift, which is closed under the shift, has an induced shift, and then apply this to the forgetful functor from bounded_derived_category to bounded_homotopy_category.

[Scott Morrison]

Possibly doing the same for bounded_homotopy_category ⥤ homotopy_category.

[Johan Commelin]

I guess that's fair.

[Scott Morrison]

PR at #13265. I need to actually try it out in LTE still.

[Johan Commelin]

Thanks, lgtm

[Scott Morrison]

It works very nicely in LTE. Once #13265 has hit master, we can merge the branch shifts on lean-liquid. After that derived_cat.lean is completely sorry free!

[Scott Morrison]

I did create two sorries in an earlier file, but hopefully they are easy: the shift of a K-projective object is K-projective, and the shift of a quasi-isomorphism is a quasi-isomorphism.

[Adam Topaz]

I'm fairly sure I proved those two things somewhere.

[Scott Morrison]

I couldn't find is_K_projective.*shift with grep (similarly for is_quasi_iso.*shift)

[Adam Topaz]

I think it's in derived/lemmas with some strange auto-generated instance name

[Scott Morrison]

yup, found it

[Scott Morrison]

didn't find one for is_K_projective, however

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/e40a6c1646b82a99a5cc1bf0d1e86601128e4f29/src/for_mathlib/derived/lemmas.lean#L389

[Scott Morrison]

These funny [[ ]] brackets foiled my search. :-)

[Adam Topaz]

I'm curious... What's the auto-generated name for that?

[Scott Morrison]

I manually named it :-)

[Adam Topaz]

BTW, I think the pretriangulated constructor for a subcat is the way to go. The stuff in the for_mathlib/derived folder should be considered as mostly experimental.

[Adam Topaz]

I guess we could use the same constructor to obtain the pretriangulated structure on the bounded homotopy category as well.

[Matthew Ballard]

Scott Morrison said:

I'd like to rip this out and start over, by showing that a full subcategory of a category with a shift, which is closed under the shift, has an induced shift, and then apply this to the forgetful functor from bounded_derived_category to bounded_homotopy_category.

The version of this for (pre)triangulated categories was the most used Lemma from my derived categories course.

[Scott Morrison]

Yes, it sounds a good idea to have. It's on my intentions list, but I may have run out of significant mathlib time for a while.