Defining Prism Operator

Stream: mathlib4

[Rui Chen]

Do anyone have idea about how to define a prism operator in algebraic topology, to show that 2 homotopic maps f g : X to Y (where x and Y are topological spaces) deduce same chain map?

[Notification Bot]

This topic was moved here from #lean4 > Defining Prism Operator by Johan Commelin.

[Johan Commelin]

@Rui Chen I don't think that mathlib has anything in that direction yet. @Brendan Seamas Murphy is our local expert on this kind of stuff.

[Brendan Seamas Murphy]

Yes, although in my implementation of singular homology I deduced this via the method of acyclic models instead of defining an explicit chain homotopy

[Brendan Seamas Murphy]

In hindsight I don't think this was a good decision

[Joël Riou]

I have not checked 100% of the details, but I think that it should follow from the similar statement for simplicial sets (if two maps A ⟶ B are homotopic, then the induced chain maps are homotopic): apply it to the morphism of simplicials sets Sing X ⟶ Sing Y deduced from the two homotopic maps of topological spaces X ⟶ Y.

In order to prove the fact for simplicial sets, it seems to me that we could prove that if h is an homotopy between two morphisms of simplicial objects in a preadditive category (in our case the category of abelian groups), then the corresponding induced morphisms on the alternating face map complexes are also chain homotopic.

(Note that in mathlib we do not have yet the notion of homotopy between morphisms of simplicial objects, but we shall have soon the notion of simplicial categories in mathlib, see #11398, and the fact that the category of simplicial objects in a category is a simplicial category should be obtained soon: @Jack McKoen and I are working on this.)