As I get further into an area of math I start getting familiar with tricks or results which are repeatedly used but whose citation or verification gets annoying to write out every single time. I have this tendency to write out every single detail, usually taking advantage of parenthetical remarks which seriously destroy the flow of the argument and cause it to take up way more room than it needs to. I think this comes from a passionate hatred for moments where I'm reading a proof and some step is skipped and I cannot see why it's true.
I'm fine doing this for hard proofs - I think the details should be made as clear as possible because there are difficult, probably unfamiliar steps. For example, I wrote an arrow-theoretic proof of the snake lemma, and it is over 5 ungodly pages long. But part of me is okay with this because it is filled with many diagrams and explanations for everything - I put a new diagram the instant I construct a new morphism or object, and sometimes consecutive diagrams will differ only by the existence of a single morphism. And I didn't even get around to proving naturality of the kernel-cokernel sequence! So I have sacrificed brevity for clarity because, as anyone familiar with arrow theoretic proofs (not even using MacLane's elements) of the snake lemma knows, it's quite a nontrivial proof.
I am focusing more on proofs of claims which can be described easily but take a while to work through rigorously. Anyone familiar with category theory will know what I'm talking about: proofs which require one to check functorality, or naturality of some construction, or that the induced map between isomorphic objects is actually an isomorphism, etc. For instance, I wrote up a proof of the five lemma using the two four lemmas, using the snake lemma and it is over a page long.
I don't think it should be this long, and the reason is I can describe the overall process very quickly. Indeed suppose we have this diagram. Decompose $b^1$, $a^3$, $a^2$, and $b^2$ through their images, giving diagram 1 and diagram 2. Then apply the snake lemma to diagram 1 to conclude $c:\text{im }a^2\to\text{im }b^2$ is mono. Then apply the snake lemma to diagram 2 to conclude $f^3$ is mono. By duality we get the other four lemma, and now the five lemma is immediate.
But doing the above proof takes way more time than it "should". You have to show the diagrams exist. Unless you're willing to do things like write "$\ker(A^1\to A^2)$" everywhere you will probably have to give names to all your morphisms (I actually felt the need to construct a naming scheme for things in homological algebra precisely because of this). You have to show commutativity. You have to show the rows are exact. These routine verifications are obvious to me, but not things I would totally shrug off in practice because sometimes, the diagram you create is not commutative, or the isomorphism not natural. So I will verify them on my scratch work, but do they really deserve a full write-up?
I know what is obvious to one not obvious to another - that's why I write with painstaking detail. But I think both the beginner and expert lose out when reading a highly detailed proof, because they can lose sight of the forest for the trees. The overall strategy is how you actually remember a proof, the details being necessary but eventually (hopefully) second nature. Also, if I refer to my notes later when the proof is less fresh in my head I don't want to get stuck on my own proof.
Even my snake lemma proof leaves much to be desired. Its extreme length makes it very hard for me to see the overall strategy, to decompose it into well-motivated and easy pieces. So I don't really feel like I learned anything from the proof. Then again I suppose it is a theorem whose result tends to be more useful than the proof.
It's like a proof is a binary tree, the top vertex being the result, the first layer consisting of subproblems it is broken into (hopefully these are already obvious), then each of those broken further and further. I feel like I'm traversing this tree in some linear manner which is making the structure of the tree totally nonobvious. Ideally my proof would just consist of the layer 1 or perhaps layer 1 and layer 2 nodes, I can cite some results, and the path is clear.
So my question to finish off this overly long post (how ironic) is this: What are techniques for helping to convey the overall message of a proof? When should I exclude details/routine verifications, or how can I better include them to keep the overall flow of the proof as uninterrupted as possible? For example, in the proof of the four lemma used above, I want to convey the idea that we are splitting up the eight-term diagram into two natural-to-consider 6 term diagrams, with a bit of fudging here and there to ensure we get 0s where we want so we can actually use the snake lemma. There's actually a very natural symmetry which arises if you draw everything out in a big diagram which also makes it clear how to prove the other four lemma immediately without appealing to duality. These are the intuitions and tricks which guide the path to a solution, which I want to include in my proofs because that is (or should be) the point of a proof.
Some ideas:
- Using footnotes to justify claims which I think are a bit on the easier side but maybe not worth leaving out
- Use lemmas as much as possible (though I am kind of asking about situations where there isn't really a lemma to cite, or where citing one over and over again would only hamper readability)
- Describing the game plan at the beginning of a proof, e.g. my "quick description" of the above proof of the five lemma
- Similar to the previous point, use the whole "Assuming X, the theorem follows because... Now we must prove X" which seems to help readability
- Judiciously decide which details are too trivial to include (but how?)
- "Know when to fold them" - sometimes a proof is just painful to work through and has many "hard" details