Projective space

Stream: mathlib4

[Sophie Morel]

This is the result of a discussion with @Heather Macbeth last February where she lamented the fact that there aren't a lot of examples of smooth manifolds in mathlib, and in particular we don't have projective space. So I put the manifold structure on ℙ 𝕜 E as a way to learn a bit of differential geometry in Lean4:
https://github.com/smorel394/ProjectiveSpace_lean4

The level of generality is the following: k is a complete nontrivially normed field, E is a normed k-vector space. The charts are modeled on closed hyperplanes so we need to have these, which means that we need a SeparatingDual instance on E. As a side note, I couldn't find code in Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual that proved that E has a separating dual of it is finite-dimensional, so I wrote it.

An annoying technical thing is that we need to choose a particular nonzero continuous linear form to define ChartedSpace and SmoothManifoldWithCorners instances on projective space, because we need to have a fixed model. I pick it using a choice function, but this forces me to have a Nonempty instance on {u : E // u ≠ 0} and somehow this instance seems hard to generate (say from the fact that E is of finrank at least 1). This instance is also needed to get the manifold structure on {u : E // u ≠ 0} from its open embedding into E.

As a test of the definition, I also wrote some helper lemmas to prove that functions to/from projective space are smooth. More precisely:

• The quotient map from {u : E // u ≠ 0} to projective space is smooth;
• The quotient map has local sections which are smooth;
• A map from projective space to a manifold M is smooth if its composition with the quotient map is smooth. Also a more general version where the source is a product N × ℙ 𝕜 E.

And to test these lemmas, I constructed the action of (E →L[𝕜] E)ˣ on projective space and proved that the action map (E →L[𝕜] E)ˣ × (ℙ 𝕜 E) → (ℙ 𝕜 E) is smooth. This requires E to be complete. I also wrote the fact that the map from the unit sphere in E to projective space is smooth (if E is a euclidian space), but that was almost trivial at this point.

Here comes my final question: should any of these be added to mathlib ? If so, how should I go about it ? (There might be code duplication, for example.) I once contributed to mathlib3 but that was a long long time ago.

[Scott Morrison]

Oh my, yes, all of those things should go in Mathlib. :-)

[Scott Morrison]

I would guess this will need to be chopped up into quite a few separate PRs. This unfortunately adds some bureaucratic overhead, but is the best way to get things reviewed efficiently.

[Sophie Morel]

I would guess so too. The fact about SeparatingDual for example should probably go somewhere near Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual, unless it is already in mathlib and I missed it.

[Scott Morrison]

As a first step, I've just given you write permissions on the mathlib4 repository. You'll need to check https://github.com/leanprover-community/mathlib4/invitations to accept this.

[Scott Morrison]

(It's easiest if you make PRs from branches in the main repository: CI runs better than PRs from a fork.)

[Sophie Morel]

There is also a fact which I used several times: if we have an OpenEmbedding u from A to B and B has a smooth manifold structure, if we have the open embedding to put a smooth manifold structure on A, then a map from a manifold M to A is smooth if and only if its composition with u is smooth. I also couldn't find code for it in mathlib, and to be honest I didn't (yet) write a separate lemma for it, but it might be worth it.

[Sebastien Gouezel]

About the Nonempty instance on {u : E // u ≠ 0}, the standard assumption for this kind of things is to require [Nontrivial E]. It has the advantage of not mentioning the base field, so it is something that can be found by typeclass inference.

[Sophie Morel]

Sebastien Gouezel said:

About the Nonempty instance on {u : E // u ≠ 0}, the standard assumption for this kind of things is to require [Nontrivial E]. It has the advantage of not mentioning the base field, so it is something that can be found by typeclass inference.

Thank you, I did not know about Nontrivial E ! I am going to rewrite a couple lemmas with it.

[Sophie Morel]

In the Mathlib.Geometry.Manifold.Instances.Sphere file we don't have Nontrivial E, but we have Fact (FiniteDimensional.finrank ℝ E = n + 1)] which implies it. I don't know what typeclass inference will think of that.

[Yaël Dillies]

I think that belongs in #mathlib4 or #maths! Think of all the mathematicians who never check the computer science talk going on in #lean4 :smile:

[Sebastien Gouezel]

You can not have an instance that [Fact (FiniteDimensional.finrank ℝ E = n + 1)] implies [Nonempty E], because Lean can not guess n when trying to apply this would-be instance. If you are constructing your charted space based on 𝕜^n, you should probably also use a similar assumption [Fact (FiniteDimensional.finrank 𝕜 E = n + 1)].

[Notification Bot]

This topic was moved here from #lean4 > Projective space by Scott Morrison.

[Sophie Morel]

I am not constructing my charted space based on 𝕜^n even in the finite-dimensional case; in fact, I never distinguish the finite-dimensional case from the general case. The issue only arises when I am constructing the map from the euclidian sphere, since Heather used ℝⁿ as a model and has a [Fact (FiniteDimensional.finrank ℝ E = n + 1)].

[Sophie Morel]

The easiest solution would be to have a Nontrivial E instance floating around in that case, but it hurts my mathematical pride to have to add an assumption that is implied by another already existing one.

[Sebastien Gouezel]

If you are using an arbitrary hyperplane as the reference vector space for your construction, do I understand correctly that you don't get the usual ℝ^n manifold structure on the projective space of an (n+1)-dimensional real vector space?

[Sophie Morel]

Sebastien Gouezel said:

If you are using an arbitrary hyperplane as the reference vector space for your construction, do I understand correctly that you don't get the usual ℝ^n manifold structure on the projective space of an (n+1)-dimensional real vector space?

I don't, but I could if I wanted. I wrote some code that does that and commented it, because what the model didn't seem to make a difference, and this way I can handle the finite-dimensional and infinite-dimensional cases in a uniform way.

[Sophie Morel]

By which I mean, if you convince me that it would be useful to specifically have a ℝ^n manifold structure on the projective space of an (n+1)-dimensional real vector space, I'll write it. I was planning to do that at first, but then I realized that all continuous linear maps are smooth, so it made no difference in proofs of smoothness (which should mostly go through maps to/from E-{0} once you have a few basic results).

[Sebastien Gouezel]

I don't know if it is important to have a ℝ^n manifold structure on the projective space of an (n+1)-dimensional real vector space. Only applications can tell. It would just feel a little bit weird to have a different design for spheres and projective spaces -- but time will probably tell which one works better.

[Johan Commelin]

I don't have much to add, except that I want to say that I think it's really cool that you did all this, and that I agree with others that this certainly deserves to be part of mathlib.

[Kevin Buzzard]

I think another nice (and even harder) project would be to put a complex manifold structure on the complex points of a smooth scheme of finite type over the complexes.

[Johan Commelin]

We need a nerdsnipe emoji

[Patrick Massot]

I don't think there is any natural model space for $\mathbb{P}(E)$. There is a natural atlas but the model depends on the chart. Forgetting topology for a while, I think the story is the following. Given any hyperplane $H$ in $E$, the affine chart associated to $E$ is the set of lines transverse to $H$, which an affine space over the vector space $Hom(E/H, H)$. Indeed, denoting by $\pi$ the projection of $E$ onto $E/H$ the action of $\varphi : Hom(E/H, H)$ onto a line $\Delta$ transverse to $H$ is $(Id + \varphi \circ \pi)(\Delta)$. If we want a map from the model $Hom(E/H, H)$ into $\mathbb{P}(E)$ then we need to also fix a line transverse to $H$. This way we get an atlas indexed by pairs $(H, \Delta)$ made of a transverse hyperplanes and lines, with model space $Hom(E/H, H)$. Of course this has a lot more charts than necessary, but it does not involve any choice. If we want to include topology to the discussion than we can use closed hyperplanes and get a nice $E/H$.

But none of this fits with our current formalization where the model space needs to be fixed and we must choose a preferred chart for each point.

[Adam Topaz]

When I thought about this some time ago, I wanted to fix some perfect pairing $E \times E’ \to k$ and to use this fixed pairing to obtain the charts. You can get whatever definitional properties you want by changing the pairing.

[Patrick Massot]

Sure, a more elementary special case is you can fix an inner product structure. Then any line $\Delta : \mathbb{P}(E)$ gets its pair $(\Delta^\perp, \Delta)$ indexing a preferred chart containing $\Delta$. But I don't think it gives you a fixed model space.

[Adam Topaz]

Yeah it doesn’t give a fixed model space. IIRC I was thinking of how one might mimic Heather’s approach for the manifold structure on the sphere (where each point has some “canonical” chart) and that’s what I came up with. It’s been a while since I thought about this…

[Junyan Xu]

In finite dimensions, the topology is unique, so it's natural to use k^{dim-1} as the model space. In infinite dimensions, maybe we can always use E itself as the model space, I'm not sure. In either case, I think the charts should be indexed by ContinuousLinearEquiv f between E and M × k, where M is the model space: the domain of the chart should be (the image in the projectivization of) {e : E | (f e).2 ≠ 0} (i.e. where the k component of f e doesn't vanish) and the map to M is given by (f e).1 / (f e).2. (No choice is involved.)

By the way, is it possible/easy to generalize to DivisionRing k?

[Sophie Morel]

I spent some time thinking about whether the projective space of $E$ should be the set of lines in $E$ or the set of hyperplanes. I wanted to say hyperplanes because I'm an algebraic geometer, but unfortunately projective space is already defined in mathlib as the quotient of $E\setminus\{0\}$$ by homotheties. :-(
Anyway, my charts are indexed by pairs $(\varphi,v)$ where $\varphi$ is a continuous linear form and $v$ is a vector such that $\varphi(v)=1$. (It would be just as natural to require $\varphi(v)\ne 0$, but it makes the formulas nicer to take $\varphi(v)=1$, and we get enough charts anyway.) The domain of the chart is the set of lines tranverse to $\{\varphi = 1\}$, the chart sends such a line to its unique intersection point with $\{\varphi =1\}$, then uses $v$ to construct an affine isomorphism between $\{\varphi =1\}$ and $Ker(\varphi)$.
To get charts with a fixed codomain, I brutally use choice to pick a fixed continuous linear $\chi$ form on $E$, then use choice again to pick a continuous linear equivalence between $Ker(\varphi)$$ and $Ker(\chi)$ for every $$\varphi$$. In finite dimension, for $\dim(E)=n+1$, I used to have an alternative definition that used choice to pick a continuous linear equivalence between $Ker(\varphi)$ and $\mathbb{k}^n$, but it didn't seem to make any difference.

[Sophie Morel]

Junyan Xu said:

In finite dimensions, the topology is unique, so it's natural to use k^{dim-1} as the model space. In infinite dimensions, maybe we can always use E itself as the model space, I'm not sure. In either case, I think the charts should be indexed by ContinuousLinearEquiv f between E and M × k, where M is the model space: the domain of the chart should be (the image in the projectivization of) {e : E | (f e).2 ≠ 0} (i.e. where the k component of f e doesn't vanish) and the map to M is given by (f e).1 / (f e).2. (No choice is involved.)

By the way, is it possible/easy to generalize to DivisionRing k?

I like your idea for charts, it is elegant. I don't know whether $E$ and $E\oplus\mathbb{k}$ are always isomorphic as topological vector spaces if $E$ is infinite-dimensional, it is true for Hilbert spaces but seems too good to be true for general normed vector spaces. So choice might be needed to get a chart.
We also have to use choice in the construction because the current implementation of manifolds in mathlib requires the choice of a preferred chart at each point.
I have not thought about normed divison rings, some things like the construction of the charts might still work. But all the differentiability stuff in mathlib requires $\mathbb{k}$ to be a field.

[Oliver Nash]

Thank you for doing this!

At the risk of making you feel that "no good deed goes unpunished" I'll also add two quick passing remarks:

1. It would be nice if we could use this machinery to obtain the canonical smooth real manifold structure on quaternionic projective space
2. I claim that it is often eventually painful to have a typeclass indexed by a non-carrier type(s). With that in mind it would be nice if we had ChartedSpace F (ℙ 𝕜 E) where F : Type* together with appropriate typeclasses on F etc.

Thank you again for doing all of this. It's a big deal IMHO and the best way forward is definitely to start the PR process.

[Junyan Xu]

Yeah, I think we can even get a canonical (analytic) complex manifold structure on quaternionic projective spaces (we probably won't define quaternionic manifolds yet). I think we can be satisfied with ℍ^n (or a more general ℍ-vector spaces) as the model space with complex analytic transition functions. The current code already produces a (smooth = analytic) complex manifold structure on complex projective spaces, I think. If we work with a general model space, then going from complex to real is just a matter of switching to a larger StructureGroupoid, which should be trivial to do. (But we need to assume something like [Module ℝ V] [Module ℂ V] [Module ℍ V] [IsScalarTower ℝ ℂ V] [IsScalarTower ℂ ℍ V] which can be annoying.) If we work with ℍ^n then we probably need an instance from [ChartedSpace (ℍ^n) P] to [ChartedSpace (ℂ^2n) P], another similar complex-to-real instance, and corresponding HasGroupoid instances.

I don't know whether E and E⊕k are always isomorphic as topological vector spaces if E is infinite-dimensional, it is true for Hilbert spaces but seems too good to be true for general normed vector spaces.

Indeed some TVS has trivial dual and therefore such isomorphism can't exist. There's still hope for locally convex spaces, though. For Banach spaces enough such isomorphisms exist, but you're not assuming completeness ...

We also have to use choice in the construction because the current implementation of manifolds in mathlib requires the choice of a preferred chart at each point.

Sounds like we're missing a constructor that takes in charts whose domains form an open cover ... I'd prefer ChartedSpace to not have such preferred choices as part of its data, but instead provide preferred choices through its API, but I wouldn't urge anyone to change the current design.

[Antoine Chambert-Loir]

Kevin Buzzard said:

I think another nice (and even harder) project would be to put a complex manifold structure on the complex points of a smooth scheme of finite type over the complexes.

Well, while you wish to push in this direction, do it over any complete normed field. And that could be a good test of what has to be known about smooth schemes.

[Sophie Morel]

Junyan Xu said:

I don't know whether E and E⊕k are always isomorphic as topological vector spaces if E is infinite-dimensional, it is true for Hilbert spaces but seems too good to be true for general normed vector spaces.

Indeed some TVS has trivial dual and therefore such isomorphism can't exist. There's still hope for locally convex spaces, though. For Banach spaces enough such isomorphisms exist, but you're not assuming completeness ...

I am assuming that the dual is separating so that weeds out the obvious counterexamples , but it is true that I am not assuming completeness to defined the charted space structure. I'll have a look at the proof that finite codimension subspaces of an infinite-dimensional Banach are isomorphic to it, maybe we don't need completeness ? It would be nice to limit the number of times choice is used. (On the other hand, while I like your description of the charts mathematically, if it becomes to painful to implement in Lean I might still stick to mine.)

[Oliver Nash]

Junyan Xu said:

Yeah, I think we can even get a canonical (analytic) complex manifold structure on quaternionic projective spaces (we probably won't define quaternionic manifolds yet). I think we can be satisfied with ℍ^n (or a more general ℍ-vector spaces) as the model space with complex analytic transition functions.

I remember being surprised when I first learned this but quaternionic projective spaces are not complex manifolds. More precisely, ℍℙⁿ does not even admit any almost complex structure (I think this is an old theorem of Massey from the 1960s). It starts to be less surprising when you recall that ℍℙ¹ = S⁴.

(Of course the question then is: "where is the quaternionic geometry that ℍℙⁿ should carry?" and the answer is that its natural metric has reduced holonomy giving it a quaternion-Kahler structure.)

[Sophie Morel]

Oliver Nash said:

Thank you for doing this!

At the risk of making you feel that "no good deed goes unpunished" I'll also add two quick passing remarks:

1. It would be nice if we could use this machinery to obtain the canonical smooth real manifold structure on quaternionic projective space
2. I claim that it is often eventually painful to have a typeclass indexed by a non-carrier type(s). With that in mind it would be nice if we had ChartedSpace F (ℙ 𝕜 E) where F : Type* together with appropriate typeclasses on F etc.

Thank you again for doing all of this. It's a big deal IMHO and the best way forward is definitely to start the PR process.

I'm afraid I don't understand your second point. Do you mean that it would be nice to define ChartedSpace F (ℙ 𝕜 E) where F is any normed 𝕜-vector space with a continuous linear equivalence between F ⊕ 𝕜 and E, for example ? I wanted to pick a particular F because I wanted to make the ChartedSpace an instance, otherwise I run into a lot of pain when talking about ContMDiff maps, but I thought that instances didn't like to have non-canonical arguments ? (Maybe this is all stupid, I am still treating instances like black magic mostly.)

[Oliver Nash]

I think you have understood my point :) I did indeed mean indexing the ChartedSpace instance using any F together with additional data (which as you suggest should just be an equivalence between F ⊕ 𝕜 and E). I'm not sure at all that this would be worth the trouble so you should probably not action this suggestion, but I think you could still set up everything using typeclass instances.

[Oliver Nash]

-- We'd need some new data-carrying typeclass like this:
class MySpecialEquiv (F E : Type*)
    [NormedAddCommGroup ℝ] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] :=
  (myEquiv : F × ℝ ≃L[ℝ] E)

instance [MySpecialEquiv F E] : ChartedSpace F (ℙ ℝ E) := ...

and then the idea would be that we could create instances of MySpecialEquiv corresponding to the various model spaces we'd like to use in various situations.

(None of the above was tested in Lean btw --- it may be full of syntax errors or worse.)

[Oliver Nash]

And (unless I'm talking through my hat) you'd recover your current instance once you also authored:

instance : MySpecialEquiv (LinearMap.ker (Chi 𝕜 E)) E := ...

[Sophie Morel]

Ah, I see, thanks!
And for your first suggestion, I guess what you mean is do as much as possible for E a NormedSpace over a NormedDivisionRing, and then when we get to the manifold/differentiability stuff make the NormedDivisionRing an algebra over a NormedField (with a scalar tower in the appropriate place). It seems that the linear algebra stuff should go through, but of course I have to try it.
I'll start the PR process on the basic linear algebra lemmas at least (well, I'll see again if I can find some of them in mathlib first), and see if I can use some of the nice suggestions people made.

[Oliver Nash]

Yes, exactly. But if it turns out to be too tricky to get this working then we can settle for just a single set of scalars and leave the quaternions for another day.

[Sophie Morel]

Junyan Xu said:

Indeed some TVS has trivial dual and therefore such isomorphism can't exist. There's still hope for locally convex spaces, though. For Banach spaces enough such isomorphisms exist, but you're not assuming completeness ...

I'm a bit confused by this problem ( = if a normed vector space has enough continuous linear forms to separate points, then is it isomorphic to its closed hyperplanes ?). The wikipedia article you refer to asserts that a subspace of finite codimension in an infinite-dimensional Banach space $E$ is isomorphic to $E$ (I assume that the subspace is closed), but gives no reference. On the other hand, there is something called Banach's hyperplane problem, which asks whether any infinite-dimensional Banach space is isomorphic to its (closed) hyperplanes, and that problem seems to have a negative solution, cf https://zbmath.org/0838.46011.
Since the wikipedia article gives no reference, I am going to trust Gowers instead.

[Antoine Chambert-Loir]

This assertion in Wikipedia is really strange, and I wonder whether it could be caused by a misinterpretion of a typo in Lindenstrauss (1971), Decompositions in Banach spaces. There, he defines indecomposable, prime and primary Banach spaces and writes: “Clearly, => prime => primary.” The temptation is huge to add “indecomposable” before the first “=>” sign, while that sign should probably just be deleted.

[Antoine Chambert-Loir]

On the other hand, all (closed) hyperplanes are isomorphic, and apparently that suffices for this approach...

[Junyan Xu]

Thanks for finding and sharing the counterexample! Looks like we have to use closed hyperplanes as model spaces in the infinite dimensional case as well.

all (closed) hyperplanes are isomorphic, and apparently that suffices for this approach...

Indeed, I think this holds for any Hausdorff TVS (proof is found here) (w* can be taken to be one of u* , v* , and u* + v*).

class MySpecialEquiv (F E : Type*)
    [NormedAddCommGroup ℝ] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] :=
  (myEquiv : F × ℝ ≃L[ℝ] E)

Do you really want that to be data carrying? I think the isomorphism will almost never be canonical, apart from the case F := Fin n → ℝ and E := Fin (n+1) → ℝ.

if a normed vector space has enough continuous linear forms to separate points

Normed vector spaces over the reals are locally convex and therefore by Hahn-Banach has enough continuous linear forms to separate points (SeparatingDual), and Lean knows about this (docs#instSeparatingDualRealInstRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpace), but I don't know whether it generalizes to a general complete NontriviallyNormedField.

Certainly, SeparatingDual is equivalent to the domains of the charts forming an open cover, at least in my approach: for any linear nonzero (continuous) linear functional f : E → 𝕜 and any e : E not in the kernel we
get a decomposition into closed subspaces E ≅ ker f ⊕ 𝕜e.

I guess we're not assuming anything weaker than NormedSpace because we want to talk about differentiability. If we only want a topological manifold there's a lot more flexibility in choosing the model space.

[Junyan Xu]

Oliver Nash said:

I remember being surprised when I first learned this but quaternionic projective spaces are not complex manifolds. More precisely, ℍℙⁿ does not even admit any almost complex structure (I think this is an old theorem of Massey from the 1960s). It starts to be less surprising when you recall that ℍℙ¹ = S⁴.

Indeed, thanks for pointing this out! My thoughts were flawed in two ways: first there isn't even a canonical embedding of ℂ into ℍ (there's a S²'s worth of them). Second, if I sat down and do the calculation with the most obvious embedding a + bi ↦ a + bi + 0j + 0k I would quickly find out (from the expressions involving complex conjugates) that multiplication on ℍ is not ℂ-differentiable in the first argument, and inverse isn't ℂ-differentiable either.

[Sophie Morel]

Junyan Xu said:

Normed vector spaces over the reals are locally convex and therefore by Hahn-Banach has enough continuous linear forms to separate points (SeparatingDual), and Lean knows about this (docs#instSeparatingDualRealInstRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpace), but I don't know whether it generalizes to a general complete NontriviallyNormedField.

It does not, Hahn-Banach is false even for some complete p-adic fields (it fails for non spherically complete fields like $\mathbb{C}_p$). I don't want to have to restrict to real and complex vector spaces, hence the SeparatingDual assumption.

Certainly, SeparatingDual is equivalent to the domains of the charts forming an open cover, at least in my approach: for any linear nonzero (continuous) linear functional f : E → 𝕜 and any e : E not in the kernel we
get a decomposition into closed subspaces E ≅ ker f ⊕ 𝕜e.

Yes, it is equivalent to the domains of the chart forming an open cover in the approach I coded (which is equivalent to yours).

I guess we're not assuming anything weaker than NormedSpace because we want to talk about differentiability. If we only want a topological manifold there's a lot more flexibility in choosing the model space.

Yes, that was because of differentiability. Some of the lemmas are more general, for example I wrote a proof that all closed hyperplanes are isomorphic that would probably work verbatim in any TVS.

[Oliver Nash]

Junyan Xu said:

Do you really want that to be data carrying? I think the isomorphism will almost never be canonical, apart from the case F := Fin n → ℝ and E := Fin (n+1) → ℝ.

Yes, I would want such a typeclass to contain data.The point about there being pairs F, E where there is no (or many) "canonical" equivalences says to me that one should be careful about global instances (like we are with algebra) but I claim the typeclass itself makes good sense.

However to be clear, I'm not pushing this approach at all: I was just trying to highlight that indexing typeclasses on non-carrier types can lead to pain eventually (and to suggest a way around this). I'd rather not harp on more about this point because I feel I've derailed this thread enough already.

[Junyan Xu]

Yes, I would want such a typeclass to contain data.

I think it would use [Nonempty (MySpecialEquiv F E)] in the infinite-dimensional case then. In the finite-dimensional case I still prefer to use k^{dim E-1} as the (only) model.

[Junyan Xu]

I realized we can also do Grassmannians under the same setup. For any subspace W of E of finite dimension r, the image of E* in W* must be the whole space, because any proper subspace U of W* annihilate some nonzero vector in W, but E* doesn't annihilate any nonzero vector by SeparatingDual. (This isn't proved in the file defining SeparatingDual.) Therefore, there exists continuous linear f : E → k^r that restricts to an isomorphism on W, and we obtain a decomposition E = ker f ⊕ W ≅ ker f ⊕ k^r. U := ker f is a closed subspace of E of finite codimension r, and all such subspaces are isomorphic (again I think this is true in any Hausdorff (implied by SepartingDual) TVS), so U^r serves as the model space. Given an isomorphism g : E ≅ U ⊕ k^r, the corresponding chart has domain consisting of r-dimensional subspaces W such that g composed with the projection to k^r restricts to an isomorphism from W to k^r. Then we can take images of the r standard basis vectors in k^r under the map k^r → W ⊆ E -g→ U ⊕ k^r → U to obtain the image of W in U^r under the chart.

[Kevin Buzzard]

I think it would be particularly nice to do Grassmannians as it's unknown how to do them synthetically.

[Sophie Morel]

I had written (on paper) the charts for Grassmannians (I don't remember where those notes are, I was using something like $Hom(W,V/W)$ as model for the chart around a point corresponding to a $r$-dimensional subspace $W$. I concentrated on projective space because I was already have enough trouble at the time proving that all closed hyperplanes are isomorphic (not mathematical trouble, lean trouble). Maybe I'll have a look again.

[Junyan Xu]

U := ker f is a closed subspace of E of finite codimension r, and all such subspaces are isomorphic (again I think this is true in any Hausdorff (implied by SepartingDual) TVS)

Actually, not even Hausdorffness is needed. The simplest proof I currently have of this fact is as follows: if V and W both have finite codimension r in E, then V ∩ W has some finite codimension s in both V and W, and there exists an algebraic isomorphism (V ∩ W) ⊕ k^s ≅ V that restricts to the inclusion on V ∩ W, which is trivially continuous (similarly for W). We just need to show the inverse is also continuous: the projection to the k^s component has kernel V ∩ W, which is closed because both V and W are, so the projection is continuous by this answer; mathlib has docs#ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range but it needs to be generalized from the normed setting. The projection to the V ∩ W component is then also continuous because it's identity minus the composition of the map V → k^s that we've just shown to be continuous and the trivially continuous map k^s → V.

(A more principled approach would be to prove the equivalent conditions of being a topological direct sum on this Wikipedia page, and use condition 2d, where we'd need to show that any algebraic complement of a closed subspace (which always contain the closure of {0}) is Hausdorff.)