How do I (not) understand Ivan's local space construction of loop Grassmannian