Barring more embarrassing mistakes the slicing lemma (Lemma Tag 0461) is now fixed, as well as the only application of it in the stacks project, namely Lemma Tag 0489. Roughly speaking this last lemma states that given an equivalence relation j : R —> U x U of schemes such that both morphisms R —> U are flat and locally of finite presentation, there exists another equivalence relation j’ : R’ —> U’ x U’ such that the quotient sheaves are isomorphic: U/R = U’/R’ and such that the two morphisms R’ —> U’ are flat, locally of finite presentation and locally quasi-finite.

This is one step towards the goal of proving that R/U is an algebraic space if j : R —> U x U satisfies the assumptions above. The final steps are to fix the etale localization lemma (as discussed before on this blog), and apply it to U’/R’.

I think there are two interesting aspects of the fix we just implemented.

The first is that we used the notion of a point of finite type of a scheme, see Definition Tag 02J1. Basically a point of finite type of a scheme S is a closed point of an open affine of S. If you like working with very general schemes (non-Noetherian or non-quasi-separated, etc, etc) then using the points of finite type can be useful since (a) there are always enough of them: they are dense in any locally closed subset of S, and (b) they behave pretty much like closed points do. Take a look at the section on points of finite type in the chapter on Morphisms of Schemes.

The second is the digression on groupoids on fields we added. Its main goal was to prove Lemma Tag 04MQ which states that dim(R) = dim(G) for a locally finite type groupoid on a field. It is a bit subtle to explain precisely what this means, but the underlying result that makes it work is not hard to understand: It says simply that if we have a scheme X and two morphisms X —> Spec(k_1) and X —> Spec(k_2) both of which turn X into a geometrically integral variety over k_i, then actually k_1 = k_2 and the maps are identified too, see Proposition Tag 04MK.