Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have been adding basic propositons and their (farily) detailed proofs at injective object in the section Existence of enough injectives.
This expands on statements and proofs mentioned in other entries, notably at injective object, also at coextension of scalars (stuff added by Todd, I think).
Generally, it is often hard to decide in which entry exactly to put a theorem. Often there are several choices. Best of course to copy stuff to each relevant point or at least link to it from there.
But I am quite a bit time pressured now (and I hope that does not already show too much in what I just typed). So I won’t do any further such organization right now. But if anyone feels like looking into this, please don’t hesitate.
1 to 1 of 1