feat(Geometry/Manifold): add MfldCat, the category of C^n manifolds

[Deicyde]

We define MfldCat 𝕜 n: the category of C^n manifolds over a field 𝕜, following the pattern of TopCat in
Mathlib.Topology.Category.TopCat.Basic. We also implement HasForget₂ (MfldCat 𝕜 n) TopCat—the forgetful functor into the category of topological spaces. For more discussion see the Zulip thread: #PR reviews > #38223 The Category of C^n Manifolds

Also added: ContMDiffMap.id_apply, .coe_id and .coe_comp which are comparable to ContinuousMap API.

Future work

• Define a Monoidal structure via product manifolds, analogous to Manifold.Topology.Category.TopCat.Monoidal
• ✅ Define the tangent functor: M ↦ TM, F ↦ F.tangentMap from MfldCat (n+1) 𝕜 to MfldCat n 𝕜 feat(Geometry/Manifold): The Tangent Functor on MfldCat #38270
• Functor FGModuleCat 𝕜 ⥤ MfldCat 𝕜 n sending a finite-dimensional 𝕜-vector space to the manifold modeled on itself. Left as TODO.
• Define FGModuleCat 𝕜 as an enriched category over MfldCat n 𝕜. The smooth functors can be realized as endofunctors on the enriched category. This is the main motivation for this construction.

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 9ee33d6428

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.Category.MfldCat.Basic (new file)	2210

---

Declarations diff

+ Hom
+ Hom.Simps.hom
+ Hom.equivContMDiffMap
+ Hom.hom
+ MfldCat
+ coe_of
+ coe_of_of
+ comp_app
+ const
+ const_apply
+ diffeomorphOfIso
+ ext
+ hom_comp
+ hom_ext
+ hom_id
+ hom_inv_id_apply
+ hom_ofHom
+ id_app
+ id_apply
+ inhabited
+ instance : Category (MfldCat 𝕜 n)
+ instance : CoeSort (MfldCat 𝕜 n) (Type u) := ⟨MfldCat.carrier⟩
+ instance : ConcreteCategory (MfldCat 𝕜 n)
+ instance : HasForget₂ (MfldCat 𝕜 n) TopCat.{u}
+ inv_hom_id_apply
+ isoOfDiffeomorph
+ ofHom
+ ofHom_apply
+ ofHom_comp
+ ofHom_hom
+ ofHom_id
+ ofNormedSpace
+ of_carrier
+ of_diffeomorphOfIso
+ of_isoOfDiffeomorph
++ coe_comp
++ coe_id

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[idontgetoutmuch]

I had to translate carrier to M for manifold in my head. What is the rationale for not staying with the usual notational choice?

[Deicyde]

From what I can tell, carrier seems to be the standard choice across all of the Category Theory codebase. Whenever a category is wrapping an existing type, that type is called carrier.

I agree M would be a more natural name for this field. If another reviewer agrees, I'm happy to change it.

[peabrainiac]

I think carrier as a name is fine - it is standard, and shouldn't appear much in later code anyway since we set up a coercion to Type (i.e. instead of M.carrier or M.M with the rename you should be able to just write M).

[chrisflav]

How about splitting this into two structures? The first one, let's call it ModelWithCorners.MfldCat, would have E, H and I as parameters. This would give a natural way to consider e.g. the category of manifolds of dimension n without boundary.

The second one would be equivalent to the one you currently have: It would take E, H and I as fields and a term of ModelWithCorners.MfldCat I.

[peabrainiac]

Do we have any reason to ever consider the category of manifolds of some fixed dimension? The only thing I can see that it has going for it is that it has coproducts whereas MfldCat doesn't, but that alone doesn't make it interesting

[chrisflav]

Certainly the category of manifolds without boundary is relevant. We can of course alternatively take the subcategory defined by something like BoundarylessManifold, but the model with corners will satisfy worse definitional properties.

Generally, it is easy to combine unbundled structures into bundled ones, but going the other way always requires a refactor. So we should check now if we later need the unbundled version.

[peabrainiac]

Using a subcategory defined by things like BoundarylessManifold seems more natural to me - we will have to do that anyway if we want to talk about boundaryless manifolds of non-fixed dimension, there are plenty of boundaryless manifolds on non-boundaryless models (e.g. the interior of any manifold with boundary), and we already have some well-behavedness results like that BoundarylessManifold is invariant under isomorphism

[peabrainiac]

I left a few smaller comments - my main takeaway aside from those is that this PR contains a lot more boilerplate API (e.g. Hom as a type synonym instead of working with ContMDiffMap directly) than my earlier version here, but this is probably a good thing because my code was based on an earlier version of TopCat and there are likely good reasons why those changes have been made to the design of TopCat since.

Thanks for your work on this, getting this category into mathlib is indeed long overdue.

[peabrainiac]

Aside from the point on Zulip that I would prefer just two universe levels, one for the field and one for the other types - if you put u₁ last, you can do e.g. MfldCat.{u₂, u₃, u₄} ℝ n where currently you would have to write MfldCat.{0, u₂, u₃, u₄} ℝ n.

[Deicyde]

I changed it to two universe levels. I'm more confident in this choice now that you and Kevin seem to support it.

[peabrainiac]

I think "The category of $C^n$ manifolds" would make a lot more sense, since we don't just provide a category instance on an existing type but define a new type MfldCat here. I see Mathlib.Topology.Category.TopCat.Basic was also named in this way though, so I guess it would be fine to stick with it for consistency?

The "smooth" should probably go though, since we define categories for all smoothness degrees here.

[Deicyde]

I agree, "The Category of C^n Manifolds" is a much nicer title. I'm going to change it and see if any other reviewer objects.