affine space as a manifold

Stream: maths

[Yury G. Kudryashov]

I'm trying to find a way to introduce a manifold instance on a NormedAddTorsor over a normed space without generating diamonds.

[Yury G. Kudryashov]

No progress so far.

[Yury G. Kudryashov]

The problem is that the normed space itself is an affine space over itself.

[Yury G. Kudryashov]

So, the most natural atlas (as in docs#ChartedSpace) for an affine space (given by docs#AffineEquiv.vaddConst at every point) conflicts with docs#chartedSpaceSelf for E as an affine space over E.

[Yury G. Kudryashov]

Any ideas?

[Sebastien Gouezel]

One way would be to change the standard atlas on a vector space: instead of just using the identity, we could use all the translations to get the same atlas as what would come from the AddTorsor structure. I don't know if we use a lot the current choice of atlas currently.

[Yury G. Kudryashov]

E.g., we use chartedSpaceSelf in docs#mdifferentiable_chart

[Yury G. Kudryashov]

And docs#contMDiffOn_chart

[Sebastien Gouezel]

All these statements would still be true, right? If we just have to fix a few proofs, it doesn't look too bad.

[Yury G. Kudryashov]

No, for docs#EuclideanHalfSpace we need the old instance.

[Yury G. Kudryashov]

I mean, for the codomain of the EuclideanHalfSpace.

[Yury G. Kudryashov]

Can we completely drop ChartedSpace and formulate the definition of a manifold in terms of what is now called extended charts?

[Yury G. Kudryashov]

Something like (not tested):

structure ModelWithCorners (k E : Type _) [NontriviallyNormedField k] [AdddCommGroup E]
    [Module k E] [TopologicalSpace E] where
  carrier : Set E
  uniqueDiffOn : UniqueDiffOn carrier
  isClosed_carrier : IsClosed carrier

structure ManifoldChart {k E : Type _}  [NontriviallyNormedField k] [AdddCommGroup E]
    [Module k E] [TopologicalSpace E] (I : ModelWithCorners k E)
    (M : Type _) [TopologicalSpace M] extends LocalEquiv M E where
  open_source : IsOpen source
  continuous_toFun : ContinuousOn toFun source
  continuous_invFun : ContinuousOn invFun target
  target_subset : target ⊆ I.carrier
  nhdsWithin_target : ∀ x ∈ target, 𝓝[target] x = 𝓝[I.carrier] x

nhdsWithin_target is equivalent to IsOpen (target ∪ I.carrierᶜ) or IsOpen ((↑) ⁻¹' target : Set I.carrier)

[Yury G. Kudryashov]

We still need a ModelWithCorners as an extra tag to choose between two non-defeq atlases on E × F.

[Sebastien Gouezel]

I don't see a reason why it wouldn't work, although it would probably be a crazy refactor. Some things would become more complicated (like recasting a complex manifold as a real manifold, or composing manifold instances -- if E is a charted space modelled on F, and F is a charted space modelled on G, then E is a charted space modelled on G). Some applications of charted spaces I have in mind (like flat surfaces, where some charts go into a vector space, other charts go into a branched cover of a vector space over a point) would not be possible any more, though, so I would have to be convinced that the reduced generality has clear gains to compensate for the losses.

[Sebastien Gouezel]

I would welcome the thoughts of @Heather Macbeth , @Floris van Doorn and @Patrick Massot on this.

[Yury G. Kudryashov]

In any case, I suggest that we redefine the ModelWithCorners as a Set + properties.

[Yury G. Kudryashov]

This way we can avoid the ModelProd + simp issues.

[Yury G. Kudryashov]

BTW, this could solve the diamond with affine spaces too.

[Yury G. Kudryashov]

It's 1am here, so I'll think about it again in the morning.

[Yury G. Kudryashov]

Though this means that we'll have to use Set.prod in place of ModelProd.

[Yury G. Kudryashov]

No longer sure if this is a good idea.

[Yury G. Kudryashov]

I think that I found another solution both to the "affine space as a manifold" and to the "ModelProd in simp".

1. We introduce

def ModelWithCorners.Self (E : Type _) : Type _ := E

(or Model.Self; BTW, should we move it to Manifold.Model?)

2. We drop ModelProd and ModelPi. Instead, we can tell the difference between Model.Self E × Model.Self F vs Model.Self (E × F).
3. We introduce an instance [NormedAddTorsor E PE] : ChartedSpace (Model.Self E) PE that uses shifts by constants. It no longer conflicts with ChartedSpace α α.

[Yury G. Kudryashov]

@Sebastien Gouezel @Floris van Doorn @Heather Macbeth @Patrick Massot :up:

[Yury G. Kudryashov]

No, we'll still have a diamond for ChartedSpace (α × α) (α × α).

[Yury G. Kudryashov]

Possible solution: drop the instance for ChartedSpace α α, add it as a def Homeomorph.chartedSpace, and add an instance for ChartedSpace (Model.Self α) (Model.Self α) so that we can talk about smoothness of chartAt.