Commit 2020-04-15 16:47 ce72cde8

feat(category_theory/limits): special shapes API cleanup (#2423) This is the 2.5th PR in a series of most likely three PRs about the cohomology functor. This PR has nothing to do with cohomology, but I'm going to need a lemma from this pull request in the final PR in the series. In this PR, I

• perform various documentation and cleanup tasks
• add lemmas similar to the ones seen in #2396 for equalizers, kernels and pullbacks (NB: these are not needed for biproducts since the simp and ext lemmas for products and coproducts readily fire)
• generalize prod.hom_ext to the situation where we have a binary_fan X Y and an is_limit for that specific fan (and similar for the other shapes)
• add "bundled" versions of lift and desc. Here is the most important example:

def kernel.lift' {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : {l : W ⟶ kernel f // l ≫ kernel.ι f = k} :=
⟨kernel.lift f k h, kernel.lift_ι _ _ _⟩

This definition doesn't really do anything by itself, but it makes proofs comforable and readable. For example, if you say obtain ⟨t, ht⟩ := kernel.lift' g p hpg, then the interesting property of t is right there in the tactic view, which I find helpful in keeping track of things when a proof invokes a lot of universal properties.