Homological Algebra: Diagram chasing in practice #2344
Conversation
Added diagram chasing proofs to EpiStable.v and HomologicalAlgebra.v. Co-Authored-By: Dan Christensen <[email protected]>
|
I plan to take a look at this next weekend. |
|
You should add HomologicalAlgebra.v to Wildcat.v, after EpiStable.v. |
I meant to tag @ThomatoTomato |
Alizter
left a comment
Alizter
left a comment
There was a problem hiding this comment.
This is great to see. I have gone through the proofs and am generally happy with the style.
Just a minor comment, sometimes you break new lines in the proof and I find this is unnecessary as it breaks it up visually.
I'm interested to know if there is further followup work planned.
|
That is noted! I know we try to limit how long the lines get, but that was not the case for one of the lines in the baby dragon lemma. We want to add some examples of categories having these assumptions, as well as map creation lemmas. It is not yet clear to say how long it is until we get those parts done. |
|
On Jan 25, 2026, Ali Caglayan ***@***.***> wrote:
Just a minor comment, sometimes you break new lines in the proof and I find this is unnecessary as it breaks it up visually.
@Alizter Can you explain what you mean by "break new lines"? Do you mean "leave blank lines"? The proofs go in stages, where you create a lift, and then justify it, so I think the spacing helps. But maybe you meant something else?
|
3 participants
This PR continues the work of #2336, #2335, #2334, and #2333, and is joint work with @jdchristensen.
We are finally able to start reaping the fruits of our labor. In this PR we prove many lemmas using the diagram chasing tactic developed so far. In EpiStable.v we prove some cancellation properties of monics and epics in epi-stable categories. HomologicalAlgebra.v contains a lot of diagram lemmas one can prove in ab-enriched epi-stable categories, among these we find the familiar 4-lemmas and 3⨉3-lemmas.
This PR does not contain any diagram lemmas that would require us to create a map, as we don't have a tactic to achieve this. Therefore no kernel-cokernel sequence or snake lemma is present.