Zulip Chat Archive

Stream: condensed mathematics

Topic: homology op

Johan Commelin (Mar 10 2022 at 17:27):

Do we have the isomorphism between homology in C and Cᵒᵖ? I think this was discussed recently, right?

Johan Commelin (Apr 11 2022 at 13:16):

I searched for this again. We still don't have it, right?

Adam Topaz (Apr 11 2022 at 13:26):

sigh

Johan Commelin (Apr 11 2022 at 19:20):

def homology_unop_iso {A B C : 𝓐ᵒᵖ} (f : A ⟶ B) (g : B ⟶ C) (w : f ≫ g = 0) :
  homology f g w ≅ op (homology g.unop f.unop (by { rw [← unop_comp, w, unop_zero] })) :=
homology_iso_cokernel_lift _ _ _ ≪≫
  sorry ≪≫ -- goal is: cokernel (kernel.lift g f w) ≅ cokernel (cokernel.desc g.unop f.unop _).op
  cokernel_op_op _ ≪≫
  (homology_iso_kernel_desc _ _ _).op

Johan Commelin (Apr 11 2022 at 19:21):

cokernel.map_iso doesn't exist :sad:

Johan Commelin (Apr 11 2022 at 19:24):

I pushed to for_mathlib/salamander.lean

Last updated: Dec 20 2023 at 11:08 UTC