homology_functor_iso

Stream: condensed mathematics

[Johan Commelin]

We need a naturality statement of the following form:

section
variables {X A B : Type*} [category X] [category.{v} A] [category.{v} B] [abelian A] [abelian B]
variables {ι : Type*} {c : complex_shape ι} (i : ι)
variables (𝓕₁ 𝓕₂ : X ⥤ A) (φ : 𝓕₁ ⟶ 𝓕₂) (G : (X ⥤ A) ⥤ homological_complex (X ⥤ A) c) (S : X)

lemma homology_functor_iso_natural :
  (((category_theory.evaluation X A).obj S).homology_functor_iso c i).inv.app (G.obj M) ≫
    ((homology_functor (X ⥤ Ab) c i).map (G.map f)).app S =
    _ := sorry

end

[Johan Commelin]

I pushed this to Qprime_isoms2.lean. I now need to go offline for a while. If someone can fill in the right hand side + a proof, that would be cool.

[Johan Commelin]

Please ignore what I wrote. This doesn't typecheck at all.

[Johan Commelin]

I will be offline for the rest of the day, but I'll try to figure out what I want in the mean time.

[Adam Topaz]

@Joël Riou I noticed you recent comment -- take a look at docs#category_theory.whiskering_right and docs#category_theory.whiskering_left

[Joël Riou]

Yes, in between, I had found the right names!

[Johan Commelin]

I minimized the remaining sorry in this file

[Johan Commelin]

It's now purely a statement about homology_functor_iso. @Joël Riou would you want to give it a go?

[Joël Riou]

Yes, this sorry was easy :-)

[Johan Commelin]

Nice! I guess the "hole in one" emoji is quite appropriate here?

[Adam Topaz]

@Joël Riou somewhere in LTE (I don't remember exactly where) we have the isomorphism showing that homology of presheaves is the presheaf of homologies. I think that would help in your eval_freeFunc_homology_zero

[Adam Topaz]

Oh nevermind I see you already have that iso!