feat(Geometry/Manifold): MfldCat is a CartesianMonoidalCategory

Mathlib.lean

@@ -4482,6 +4482,8 @@ public import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
 public import Mathlib.Geometry.Manifold.Algebra.Structures
 public import Mathlib.Geometry.Manifold.Bordism
 public import Mathlib.Geometry.Manifold.BumpFunction
+public import Mathlib.Geometry.Manifold.Category.MfldCat.Basic
+public import Mathlib.Geometry.Manifold.Category.MfldCat.CartesianMonoidal
 public import Mathlib.Geometry.Manifold.ChartedSpace
 public import Mathlib.Geometry.Manifold.Complex
 public import Mathlib.Geometry.Manifold.ConformalGroupoid

Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean

@@ -0,0 +1,213 @@
+/-
+Copyright (c) 2026 Jack McCarthy. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jack McCarthy
+-/
+module
+
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import Mathlib.Topology.Category.TopCat.Basic
+
+/-!
+# The category of $C^n$ manifolds
+
+We introduce the category `MfldCat 𝕜 n` of `C^n` manifolds over a field `𝕜`. Each object bundles the
+underlying manifold together with its model vector space `E`, model space `H`, and
+`I : ModelWithCorners 𝕜 E H`. Thus, `MfldCat 𝕜 n` also includes manifolds with boundary and corners.
+
+We define a forgetful functor `forget₂ (MfldCat 𝕜 n) TopCat` taking smooth manifolds to topological
+spaces. We also define `MfldCat.ofNormedSpace` turning any `NormedSpace 𝕜 E` into a manifold. In the
+future, we plan to define a functor `FGModuleCat 𝕜 ⥤ MfldCat 𝕜 n` from the category of
+finite-dimensional vector spaces over `𝕜`.
+
+# Implementation Notes
+* We do not assume `[FiniteDimensional 𝕜 E] [T2Space M] [SigmaCompactSpace M]`, so this category
+  includes non-Hausdorff, non-paracompact, and infite-dimensional manifolds.
+* We keep `E`, `H` and `carrier` all in the same `Type u`; `𝕜` is given a seperate `Type v`.
+
+# Future Work
+* Define a functor `FGModuleCat 𝕜 ⥤ MfldCat 𝕜 n`.
+-/
+
+@[expose] public section
+
+open CategoryTheory
+open scoped Manifold ContDiff
+
+universe u v
+
+/-- The category of `C^n` 𝕜-manifolds. -/
+structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω) where
+  /-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
+  of ::
+  /-- The underlying type. -/
+  carrier : Type u
+  /-- The model normed space. -/
+  E : Type u
+  /-- The chart space. -/
+  H : Type u
+  [instNormedAddCommGroup : NormedAddCommGroup E]
+  [instNormedSpace : NormedSpace 𝕜 E]
+  [instTopologicalSpaceH : TopologicalSpace H]
+  /-- The model with corners. -/
+  I : ModelWithCorners 𝕜 E H
+  [instTopologicalSpace : TopologicalSpace carrier]
+  [instChartedSpace : ChartedSpace H carrier]
+  [instIsManifold : IsManifold I n carrier]
+
+section Notation
+
+open Lean.PrettyPrinter.Delaborator
+
+/-- This prevents `MfldCat.of M E H I` being printed as `{ carrier := M, ... }` by
+`delabStructureInstance`. -/
+@[app_delab MfldCat.of]
+meta def MfldCat.delabOf : Delab := delabApp
+
+end Notation
+
+attribute [instance] MfldCat.instNormedAddCommGroup MfldCat.instNormedSpace
+  MfldCat.instTopologicalSpaceH MfldCat.instTopologicalSpace
+  MfldCat.instChartedSpace MfldCat.instIsManifold
+
+initialize_simps_projections MfldCat
+  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH, -instTopologicalSpace,
+    -instChartedSpace, -instIsManifold)
+
+namespace MfldCat
+
+variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
+  {X Y Z : Type u} {E E' E'' : Type u} {H H' H'' : Type u}
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
+  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H']
+  [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H'']
+  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
+  {I'' : ModelWithCorners 𝕜 E'' H''}
+  [TopologicalSpace X] [ChartedSpace H X] [IsManifold I n X]
+  [TopologicalSpace Y] [ChartedSpace H' Y] [IsManifold I' n Y]
+  [TopologicalSpace Z] [ChartedSpace H'' Z] [IsManifold I'' n Z]
+
+instance : CoeSort (MfldCat 𝕜 n) (Type u) := ⟨MfldCat.carrier⟩
+
+attribute [coe] MfldCat.carrier
+
+variable (X E H I) in
+lemma coe_of : (of (n := n) X E H I : Type u) = X := rfl
+
+lemma of_carrier (M : MfldCat 𝕜 n) : of (n := n) M.carrier M.E M.H M.I = M := rfl
+
+/-- The type of morphisms in `MfldCat`. -/
+@[ext]
+structure Hom (M N : MfldCat.{u, v} 𝕜 n) where
+  private mk ::
+  /-- The underlying `C^n` map. -/
+  hom' : ContMDiffMap M.I N.I M N n
+
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
+instance : Category (MfldCat 𝕜 n) where
+  Hom M N := Hom M N
+  id M := ⟨ContMDiffMap.id⟩
+  comp f g := ⟨g.hom'.comp f.hom'⟩
+
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
+instance : ConcreteCategory (MfldCat 𝕜 n)
+    (fun M N => ContMDiffMap M.I N.I M N n) where
+  hom f := f.hom'
+  ofHom f := ⟨f⟩
+
+/-- Turn a morphism in `MfldCat` back into a `ContMDiffMap`. -/
+abbrev Hom.hom {M N : MfldCat 𝕜 n} (f : Hom M N) :=
+  ConcreteCategory.hom (C := MfldCat 𝕜 n) f
+
+/-- Typecheck a `ContMDiffMap` as a morphism in `MfldCat`. -/
+abbrev ofHom (f : ContMDiffMap I I' X Y n) : of (n := n) X E H I ⟶ of (n := n) Y E' H' I' :=
+  ConcreteCategory.ofHom (C := MfldCat 𝕜 n) f
+
+/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
+def Hom.Simps.hom (M N : MfldCat.{u, v} 𝕜 n) (f : Hom M N) :=
+  f.hom
+
+initialize_simps_projections Hom (hom' → hom)
+
+/-!
+The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`.
+-/
+
+@[simp]
+lemma hom_id {M : MfldCat 𝕜 n} :
+    (𝟙 M : M ⟶ M).hom = ContMDiffMap.id := rfl
+
+@[simp]
+lemma hom_comp {M N P : MfldCat 𝕜 n} (f : M ⟶ N) (g : N ⟶ P) :
+    (f ≫ g).hom = g.hom.comp f.hom := rfl
+
+
+section ofHom
+
+@[simp]
+lemma hom_ofHom (f : ContMDiffMap I I' X Y n) : (ofHom f).hom = f := rfl
+
+@[simp]
+lemma ofHom_hom {M N : MfldCat 𝕜 n} (f : M ⟶ N) :
+    ofHom (Hom.hom f) = f := rfl
+
+@[simp]
+lemma ofHom_id :
+    ofHom (ContMDiffMap.id : ContMDiffMap I I X X n) = 𝟙 (of (n := n) X E H I) := rfl
+
+@[simp]
+lemma ofHom_comp (f : ContMDiffMap I I' X Y n) (g : ContMDiffMap I' I'' Y Z n) :
+    ofHom (g.comp f) = ofHom f ≫ ofHom g := rfl
+
+end ofHom
+
+instance inhabited : Inhabited (MfldCat 𝕜 n) :=
+  ⟨of 𝕜 𝕜 𝕜 (modelWithCornersSelf 𝕜 𝕜)⟩
+
+/-- A normed space is a `C^n` manifold (modeled on itself). -/
+abbrev ofNormedSpace (n : ℕ∞ω) (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
+    MfldCat 𝕜 n :=
+  of E E E (modelWithCornersSelf 𝕜 E)
+
+/-- `MfldCat 𝕜 n` has a forgetful functor to `TopCat`. -/
+instance : HasForget₂ (MfldCat 𝕜 n) TopCat.{u} where
+  forget₂.obj M := TopCat.of M
+  forget₂.map f := TopCat.ofHom ⟨f.hom, f.hom.contMDiff.continuous⟩
+
+/-- Any diffeomorphism induces an isomorphism in `MfldCat`. -/
+@[simps]
+def isoOfDiffeomorph {M N : MfldCat 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) : M ≅ N where
+  hom := ofHom f.toContMDiffMap
+  inv := ofHom f.symm.toContMDiffMap
+
+/-- Any isomorphism in `MfldCat` induces a diffeomorphism. -/
+@[simps]
+def diffeomorphOfIso {M N : MfldCat 𝕜 n} (f : M ≅ N) : M ≃ₘ^n⟮M.I, N.I⟯ N where
+  toFun := f.hom
+  invFun := f.inv
+  left_inv _ := by simp
+  right_inv _ := by simp
+  contMDiff_toFun := f.hom.hom.contMDiff
+  contMDiff_invFun := f.inv.hom.contMDiff
+
+@[simp]
+theorem of_isoOfDiffeomorph {M N : MfldCat 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) :
+    diffeomorphOfIso (isoOfDiffeomorph f) = f :=
+  rfl
+
+@[simp]
+theorem of_diffeomorphOfIso {M N : MfldCat 𝕜 n} (f : M ≅ N) :
+    isoOfDiffeomorph (diffeomorphOfIso f) = f :=
+  rfl
+
+/-- The constant morphism `M ⟶ N` in `MfldCat` given by `y : N`. -/
+def const {M N : MfldCat 𝕜 n} (y : N) : M ⟶ N :=
+  ofHom <| ContMDiffMap.const y
+
+@[simp]
+lemma const_apply {M N : MfldCat 𝕜 n} (y : N) (x : M) :
+    const y x = y := rfl
+
+end MfldCat

Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Jack McCarthy. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jack McCarthy
+-/
+module
+
+public import Mathlib.Geometry.Manifold.Category.MfldCat.Basic
+public import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
+
+/-!
+# Cartesian monoidal structure on `MfldCat`
+
+We endow `MfldCat 𝕜 n` with its cartesian monoidal structure: the monoidal product is the
+product manifold, and the unit is `PUnit`, viewed as a zero-dimensional `𝕜`-manifold.
+We also derive the induced braided category structure.
+
+## Implementation notes
+
+We use `PUnit.{u + 1}` (rather than `Fin 0 → 𝕜`, which lives in `𝕜`'s universe) for the unit
+object so that it exists in `MfldCat.{u} 𝕜 n` for any universe of `𝕜`.
+-/
+
+@[expose] public section
+
+open CategoryTheory Limits MonoidalCategory
+open scoped Manifold ContDiff
+
+universe u v
+
+namespace MfldCat
+
+variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
+
+/-- Limit data for a binary product in `MfldCat`, using the product manifold `M × N`. -/
+@[simps! cone_pt isLimit_lift]
+def binaryProductLimitCone (M N : MfldCat.{u} 𝕜 n) : LimitCone (pair M N) where
+  cone := BinaryFan.mk (ofHom .fst) (ofHom .snd)
+  isLimit := BinaryFan.IsLimit.mk _ (fun l r => ofHom (l.hom.prodMk r.hom))
+    (fun _ _ => rfl) (fun _ _ => rfl) (by cat_disch)
+
+/-- We choose `MfldCat.of (M ⨯ N) (M.E × N.E) (ModelProd M.H N.H) (M.I.prod N.I)` as product  of `M`
+and `N`, and `ofNormedSpace n PUnit` as the terminal object. -/
+noncomputable instance cartesianMonoidalCategory :
+    CartesianMonoidalCategory (MfldCat.{u} 𝕜 n) :=
+  .ofChosenFiniteProducts
+    ⟨_, IsTerminal.ofUniqueHom (Y := ofNormedSpace n PUnit.{u + 1})
+      (fun _ => const PUnit.unit) (fun _ _ => by ext)⟩
+    binaryProductLimitCone
+
+noncomputable instance : BraidedCategory (MfldCat.{u} 𝕜 n) := .ofCartesianMonoidalCategory
+
+theorem tensorObj_eq (M N : MfldCat.{u} 𝕜 n) :
+    (M ⊗ N) = of (M × N) (M.E × N.E) (ModelProd M.H N.H) (M.I.prod N.I) := rfl
+
+end MfldCat

Mathlib/Geometry/Manifold/ContMDiffMap.lean

@@ -79,6 +79,12 @@ instance : ContinuousMapClass C^n⟮I, M; I', M'⟯ M M' where
 nonrec def id : C^n⟮I, M; I, M⟯ :=
   ⟨id, contMDiff_id⟩
 
+@[simp]
+theorem id_apply (x : M) : (ContMDiffMap.id : C^n⟮I, M; I, M⟯) x = x := rfl
+
+@[simp]
+theorem coe_id : ⇑(ContMDiffMap.id : C^n⟮I, M; I, M⟯) = _root_.id := rfl
+
 /-- The composition of `C^n` maps, as a `C^n` map. -/
 def comp (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) : C^n⟮I, M; I'', M''⟯ where
   val a := f (g a)
@@ -89,6 +95,10 @@ theorem comp_apply (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) (
     f.comp g x = f (g x) :=
   rfl
 
+@[simp]
+theorem coe_comp (f : C^n⟮I', M'; I'', M''⟯) (g : C^n⟮I, M; I', M'⟯) :
+    ⇑(f.comp g) = f ∘ g := rfl
+
 instance [Inhabited M'] : Inhabited C^n⟮I, M; I', M'⟯ :=
   ⟨⟨fun _ => default, contMDiff_const⟩⟩