Kevin Buzzard asked this question, which incorporated a long section of background discussion. Federico Poloni removed that section. Yemon Choi commented that he thought it was OK. I agree, and plan to put it back in in a moment. We can discuss further here if necessary.