complexes in the opposite category

Stream: maths

[Kevin Buzzard]

I'm enjoying doing category theory in Lean for pretty much the first time in my life. Turns out what I needed was a group law!

I've just been finding my way around. Do we have any of the below in mathlib or LTE? Do we want any of this stuff?

import category_theory.abelian.basic
import algebra.homology.homology
import algebra.homology.additive
import logic.equiv.transfer_instance
import category_theory.preadditive.opposite

open category_theory category_theory.limits opposite

variables (𝒞 : Type*) [category 𝒞]

-- is it definitely `simp`?
@[simp] lemma zero_op [has_zero_morphisms 𝒞] {x y : 𝒞}: (0 : x ⟶ y).op = 0 := rfl -- phew

variables (α : Type*) [add_right_cancel_semigroup α] [has_one α]
(my_shape : complex_shape α)

def homological_complex.op_symm {𝒞 : Type*} [category 𝒞] [has_zero_morphisms 𝒞]
{α : Type*} [add_right_cancel_semigroup α] [has_one α] {my_shape : complex_shape α}
(Xᵢ : homological_complex 𝒞 my_shape) :
homological_complex 𝒞ᵒᵖ (my_shape.symm) :=
{ X := λ i, op (Xᵢ.X i),
  d := λ i j, (Xᵢ.d j i).op,
  shape' := λ i j h, by simp only [homological_complex.shape' Xᵢ j i h, zero_op],
  d_comp_d' := λ i j k hij hjk, by simp only [←op_comp,
    homological_complex.d_comp_d' Xᵢ k j i hjk hij, zero_op], }

def homological_complex.op_symm' {𝒞 : Type*} [category 𝒞] [has_zero_morphisms 𝒞]
{α : Type*} [add_right_cancel_semigroup α] [has_one α] {my_shape : complex_shape α}
(Xᵢ : homological_complex 𝒞 my_shape.symm) :
homological_complex 𝒞ᵒᵖ my_shape :=
{ X := λ i, op (Xᵢ.X i),
  d := λ i j, (Xᵢ.d j i).op,
  shape' := λ i j h, by simp only [homological_complex.shape' Xᵢ j i h, zero_op],
  d_comp_d' := λ i j k hij hjk, by simp [← op_comp,
    homological_complex.d_comp_d' Xᵢ k j i hjk hij], }

variables [preadditive 𝒞] (𝒟 : Type*) [category 𝒟] [preadditive 𝒟] (f : 𝒞 ⥤ 𝒟)

instance category_theory.functor.unop_unop_additive : (unop_unop 𝒞).additive :=
{ map_add' := λ a b f g, by simp only [unop_unop_map, op_add]}

def some_triangle_commutes :
category_theory.functor.map_homological_complex (unop_unop 𝒞) my_shape ≅
{ obj := λ Xᵢ, Xᵢ.op_symm.op_symm',
  map := λ Xᵢ Yᵢ fᵢ,
  { f := λ i, (fᵢ.f i).op.op,
    comm' := λ i j hij, begin
      suffices : (fᵢ.f i).op.op ≫ (Yᵢ.d i j).op.op = (Xᵢ.d i j).op.op ≫ (fᵢ.f j).op.op,
        simpa,
      simp only [← op_comp],
      rw fᵢ.comm i j,
      end },
  map_id' := λ _, rfl,
  map_comp' := λ _ _ _ _ _, rfl, } :=
{ hom := { app := λ Xᵢ, 𝟙 _, },
  inv := { app := λ Xᵢ, 𝟙 _, }, }
-- a lot of background `tidy

[Kevin Buzzard]

Oh I found some of this in LTE in for_mathlib.homological_complex_op.