Painful `ContMDiff` proof

Stream: mathlib4

[Michael Rothgang]

In #22784, I'm trying to prove Diffeomorph.sumSumSumComm (for my bordism theory project). The result is painful, though:

Is there a tactic I'm missing? (fun_prop is not set up for ContMDiff; I imagine it would have trouble guessing the intermediate models I.) Or should I be writing lots of Diffeomorph.trans? (Doing that naively fails, but it's conceivable it could work with lots of additional type annotations.)

/-- Four-way commutativity of the disjoint union of manifolds -/
def sumSumSumComm : Diffeomorph I I ((M ⊕ M') ⊕ N ⊕ N') ((M ⊕ N) ⊕ M' ⊕ N') n where
  toEquiv := Equiv.sumSumSumComm M M' N N'
  contMDiff_toFun := by
    -- Please, tell me there is a tactic for this! Or is there a better way?
    dsimp [Equiv.sumSumSumComm]
    -- change ContMDiff I I n ((Diffeomorph.sumAssoc I (M ⊕ N) n M' N') ∘
    --   (Diffeomorph.sumCongr ((Diffeomorph.sumAssoc I M n N M').symm) (Diffeomorph.refl I N' n)) ∘
    --   Diffeomorph.sumCongr
    --     (Diffeomorph.sumCongr (Diffeomorph.refl I M n) (Diffeomorph.sumComm I M' n N))
    --     (Diffeomorph.refl I _ n) ∘
    --   (Diffeomorph.sumCongr (Diffeomorph.sumAssoc I M n M' N) (Diffeomorph.refl I _ n)) ∘
    --   (Diffeomorph.sumAssoc I (M ⊕ M') n N N').symm)
    apply ContMDiff.comp (I' := I)
    · exact Diffeomorph.contMDiff (sumAssoc I (M ⊕ N) n M' N')
    · apply ContMDiff.comp (I' := I)
      · exact Diffeomorph.contMDiff ((sumAssoc I M n N M').symm.sumCongr (Diffeomorph.refl I N' n))
      · apply ContMDiff.comp (I' := I)
        · exact Diffeomorph.contMDiff
            (((Diffeomorph.refl I M n).sumCongr (sumComm I M' n N)).sumCongr
              (Diffeomorph.refl I N' n))
        · apply ContMDiff.comp (I' := I)
          · exact Diffeomorph.contMDiff ((sumAssoc I M n M' N).sumCongr (Diffeomorph.refl I N' n))
          · exact Diffeomorph.contMDiff (sumAssoc I (M ⊕ M') n N N').symm
  contMDiff_invFun := sorry -- omitted

[Tomas Skrivan]

I would like fun_prop to be able to solve this and as you exactly pointed out, the issue is the intermediate model I'. There has to be some heuristic on how to pick it, or maybe I can keep it as a meta variable as long as possible and somehow resolve it at the end.

Anyway, if you have more examples of tedious proofs like this send them my way. I would like to have a look at this at some point.

[Floris van Doorn]

I haven't looked at differential geometry design decisions since Lean 4.
Should we investigate whether it is possible to make I an outParam in docs#IsManifold ? If that is possible, that would clean-up the manifold library substantially. A disadvantage is that we would require type synonyms whenever we change the field/model space, but that seems like a very small price to pay.

[Floris van Doorn]

Two other design decisions in the manifold library that should probably be changed/investigated:

• Is the library note Manifold type tags still relevant in Lean 4 now that we have structure-eta? (also rebutted by Sebastien below)
• Change the definition of docs#ModelWithCorners (see discussion in #18403)

[Sébastien Gouëzel]

No, it's not possible to make I an outparam, because E x F is a manifold in two different ways, when E and F are vector spaces: it's a product manifold (as the product of two manifolds), and it's a manifold because it's a vector space. Those two ways to be a manifold are not defeq, and to avoid diamonds they don't correspond to the same model with corners.

[Floris van Doorn]

That makes it indeed tricky. It might still be possible to do this if we add a type synonym for "treat this vector space as a manifold". Then a vector space is only a manifold when using the type synonym, and the product is an instance without type synonyms.
This change would be annoying in a lot more places, so is maybe not good. Then again, maybe not that annoying compared to the already existing type synonyms such as docs#ModelProd.

[Sébastien Gouëzel]

Here is another possibility, which would solve the prod diamond issue and make it possible to have I as an outparam (still depending on the field): forgetful inheritance.

In normed spaces, one would add another data field d which would essentially be a manifold structure over itself, and a prop field saying that this manifold structure coincides propositionally with the trivial one. Associating a manifold structure to a vector space would be done through d. Then, when declaring the product of two vector spaces, the d of the product would match exactly the one that is done when building the product of two manifolds. In this way, given E and F two vector spaces, seeing E and F as manifolds and taking their product would give definitionally the same manifold structure as the one on the vector space E x F.

I'm not sure how painful the refactor would be, but this idea seems quite promising to me. Any thoughts?

[Floris van Doorn]

Hmm... That's essentially what we do with MetricSpace + UniformSpace, and there it works very well. That sounds really promising.
It would result in import increases + extra work to define normed spaces... So it's not for free.

[Tomas Skrivan]

@Ben Eltschig There is an issue with topology on product spaces and diffeology. I have a feeling that the problem is very similar as with manifolds mentioned here. Is it the case? Would the proposed solution by @Sébastien Gouëzel . also help or the opposite? (I don't fully understand the math nor the TC voodoo here so these two problems might be completely unrelated)

[Tomas Skrivan]

In other words, if such a refactor happens it would be nice if it plays well with diffeology too. I know diffeology is not even in mathlib yet but future proofing for it would be nice and, I think, would make few physicists here happy.

[Kevin Buzzard]

@Tomas Skrivan here is an example of this phenomenon which is hopefully simpler to understand than this manifold stuff. A metric space structure on a type is a bunch of data (a distance function + axioms). A topological space structure on a type is another bunch of data (a collection of open sets + axioms). It's a standard result that "every metric space is a topological space" i.e. given a metric space structure on a type, there is a canonical topological space structure coming from the metric. Metric spaces and topological space structures on a type are implented as classes, and one can make an instance from MetricSpace X to TopologicalSpace X to capture this construction. So far so good.

It's also standard that the product of two metric spaces is a metric space, and the product of two topological spaces is a topological space. One can make these both instances too! And then bingo, you have a diamond in the typeclass system, because if you have two metric spaces X and Y, then there's two ways to get a topological space structure on the product X x Y, namely (1) take the product metric and then take the associated topology, or (2) take the associated topological spaces and then take the product topology. These two constructions are well-known to give the same answer, but the equality is not definitional, so typeclass inference breaks.

The way this issue is dealt with in mathlib is that the definition of a metric space also contains all the data of a topology, plus a proof field saying that the topology is the one coming from the metric! So internally a metric space is carrying around far more data than a mathematician would expect. But this solves the diamond problem because in the definition of the product of two metric spaces, you define the topology on the product to be the product of the topologies, and the proof field is not rfl, it is where you insert this well-known mathematical proof that the two topologies (one coming from the product metric, the other coming from the product topology) are equal.

So this is part of a phenomenon where you overload classes with extra information which can be derived from the data you have. It's the same sort of reason we have an action of Z in the definition of a group.

[Kevin Buzzard]

I've bent the truth a bit above: this is how it was in 2017. Now we actually have some slightly different structure called a uniform space embedded into the definition of a metric space, instead of a topological space. But the principle is exactly the same.

[Ben Eltschig]

Tomas Skrivan said:

Ben Eltschig There is an issue with topology on product spaces and diffeology. I have a feeling that the problem is very similar as with manifolds mentioned here. Is it the case? Would the proposed solution by Sébastien Gouëzel . also help or the opposite? (I don't fully understand the math nor the TC voodoo here so these two problems might be completely unrelated)

The issue with product spaces and the D-topology is actually worse than this, because the D-topology genuinely does not commute with binary products - the two topologies you get on products of topological spaces are actually different, not just non-defeq. So I don't think there really is a better solution than the IsDTopCompatible typeclass we have now.

[Tomas Skrivan]

Thanks a lot @Kevin Buzzard I had a very vague understanding of this but your explanation made it super clear!

[Ben Eltschig]

At least for the typical product types, that is - we can still introduce a type synonym that carries the topology of the product taken in the category of delta-generated spaces, and define the diffeology on it in such a way that the D-topology is defeq to the topology the type carries. I imagine a similar solution is probably getting thought about for CW complexes and products of compactly generated spaces, but I don't know for sure

[Ben Eltschig]

A more fitting parallel to the problem with manifolds this thread is about: the functor equipping normed spaces with their natural diffeologies does preserve products, but it can't be registered as an instance because the two diffeologies you get on products of normed spaces would be non-defeq despite being equal. This could in theory be fixed by making a diffeology part of the data of NormedSpace similar to what Sébastien suggested, but I imagine it's hard to do without creating an import loop (or even worse, an actual cyclic dependency in the definitions. Diffeologies depend on smoothness after all, which depends on normed spaces). I fear that in the case of manifolds you might run into the same problem, but that's also just a guess.

[Tomas Skrivan]

I see, yeah I don't fully understand the math :) I just know that diffeology provides some useful theorems I want to use at some point. Thanks for the explanation!

[Ben Eltschig]

A slightly different question: isn't it also the case that if I was an outparam, it would be hard to talk about manifolds as manifolds with (empty) boundary?