From 46db87e1e3c7638cecd9431157bd0b63c8bfc1f7 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sat, 18 Apr 2026 20:10:01 -0400
Subject: [PATCH 01/36] Added a new file
 Geometry/Manifold/Category/MfldCat/Basic.lean

---
 Mathlib.lean                                  |   1 +
 .../Manifold/Category/MfldCat/Basic.lean      | 278 ++++++++++++++++++
 2 files changed, 279 insertions(+)
 create mode 100644 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 51561e14b0c337..710110e96cc514 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4460,6 +4460,7 @@ 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.ChartedSpace
 public import Mathlib.Geometry.Manifold.Complex
 public import Mathlib.Geometry.Manifold.ConformalGroupoid
diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
new file mode 100644
index 00000000000000..e2bac2b30cd50d
--- /dev/null
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -0,0 +1,278 @@
+/-
+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.CategoryTheory.Elementwise
+public import Mathlib.Geometry.Manifold.ContMDiffMap
+public import Mathlib.Geometry.Manifold.ContMDiff.Constructions
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import Mathlib.Topology.Category.TopCat.Basic
+
+/-!
+# Category instance for smooth manifolds
+
+We introduce the category `MfldCat 𝕜 n` of `C^n` manifolds over a field `𝕜`. Each object bundles the
+underlying manifold together with its model space `E`, chart 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 `𝕜`.
+-/
+
+@[expose] public section
+
+set_option autoImplicit false
+
+open CategoryTheory
+open scoped Manifold
+
+universe u
+
+/-- The category of `C^n` 𝕜-manifolds. -/
+structure MfldCat (𝕜 : Type u) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) 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
+  [instNAG : NormedAddCommGroup E]
+  [instNS : NormedSpace 𝕜 E]
+  [instTopH : TopologicalSpace H]
+  /-- The model with corners. -/
+  I : ModelWithCorners 𝕜 E H
+  [instTop : TopologicalSpace carrier]
+  [instCharted : ChartedSpace H carrier]
+  [instManifold : 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.instNAG MfldCat.instNS MfldCat.instTopH MfldCat.instTop
+  MfldCat.instCharted MfldCat.instManifold
+
+initialize_simps_projections MfldCat
+  (-instNAG, -instNS, -instTopH, -instTop, -instCharted, -instManifold)
+
+namespace MfldCat
+
+variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
+
+instance : CoeSort (MfldCat 𝕜 n) (Type u) := ⟨MfldCat.carrier⟩
+
+attribute [coe] MfldCat.carrier
+
+lemma coe_of (M : Type u) (E : Type u) (H : Type u)
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
+    (I : ModelWithCorners 𝕜 E H) [TopologicalSpace M] [ChartedSpace H M]
+    [IsManifold I n M] : (of (n := n) M E H I : Type u) = M := rfl
+
+lemma of_carrier (M : MfldCat.{u} 𝕜 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 𝕜 n) where
+  /-- The underlying `C^n` map. -/
+  hom' : ContMDiffMap M.I N.I M N n
+
+instance : Category (MfldCat 𝕜 n) where
+  Hom M N := Hom M N
+  id M := ⟨ContMDiffMap.id⟩
+  comp f g := ⟨g.hom'.comp f.hom'⟩
+
+instance : ConcreteCategory.{u} (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.{u} 𝕜 n} (f : Hom M N) :=
+  ConcreteCategory.hom (C := MfldCat 𝕜 n) f
+
+/-- Typecheck a `ContMDiffMap` as a morphism in `MfldCat`. -/
+abbrev ofHom {M N : Type u} {E E' : Type u} {H H' : Type u}
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
+    [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H']
+    {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
+    [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M]
+    [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' n N]
+    (f : ContMDiffMap I I' M N n) :
+    of (n := n) M E H I ⟶ of (n := n) N 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} 𝕜 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]
+theorem id_app (M : MfldCat 𝕜 n) (x : ↑M) : (𝟙 M : M ⟶ M) x = x := rfl
+
+@[simp]
+theorem coe_id (M : MfldCat 𝕜 n) : (𝟙 M : M → M) = _root_.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
+
+@[simp]
+theorem comp_app {M N P : MfldCat 𝕜 n} (f : M ⟶ N) (g : N ⟶ P) (x : M) :
+    (f ≫ g : M → P) x = g (f x) := rfl
+
+@[simp]
+theorem coe_comp {M N P : MfldCat 𝕜 n} (f : M ⟶ N) (g : N ⟶ P) :
+    (f ≫ g : M → P) = g ∘ f := rfl
+
+@[ext]
+lemma hom_ext {M N : MfldCat 𝕜 n} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g :=
+  Hom.ext hf
+
+@[ext]
+lemma ext {M N : MfldCat 𝕜 n} {f g : M ⟶ N} (w : ∀ x : M, f x = g x) : f = g :=
+  ConcreteCategory.hom_ext _ _ w
+
+section ofHom
+
+variable {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]
+
+@[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
+
+lemma ofHom_apply (f : ContMDiffMap I I' X Y n) (x : X) : (ofHom f) x = f x := rfl
+
+lemma hom_inv_id_apply {M N : MfldCat 𝕜 n} (f : M ≅ N) (x : M) : f.inv (f.hom x) = x := by
+  simp
+
+lemma inv_hom_id_apply {M N : MfldCat 𝕜 n} (f : M ≅ N) (y : N) : f.hom (f.inv y) = y := by
+  simp
+
+end ofHom
+
+/-- Morphisms in `MfldCat` are equivalent to `ContMDiffMap`s. -/
+@[simps]
+def Hom.equivContMDiffMap (M N : MfldCat.{u} 𝕜 n) :
+    (M ⟶ N) ≃ ContMDiffMap M.I N.I M N n where
+  toFun f := f.hom
+  invFun f := ofHom f
+
+/-- Replace a function coercion for a morphism `MfldCat.of X E H I ⟶ MfldCat.of Y E' H' I'` with
+the definitionally equal function coercion for a `ContMDiffMap I I' X Y n`. -/
+@[simp] theorem coe_of_of {X Y E E' H H' : Type u}
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
+    [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace 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]
+    {f : ContMDiffMap I I' X Y n} {x} :
+    @DFunLike.coe (of (n := n) X E H I ⟶ of (n := n) Y E' H' I')
+      ((CategoryTheory.forget (MfldCat 𝕜 n)).obj (of (n := n) X E H I))
+      (fun _ ↦ (CategoryTheory.forget (MfldCat 𝕜 n)).obj (of (n := n) Y E' H' I'))
+      ConcreteCategory.instFunLike
+      (ofHom f) x =
+    @DFunLike.coe (ContMDiffMap I I' X Y n) X
+      (fun _ ↦ Y) _
+      f x :=
+  rfl
+
+instance inhabited : Inhabited (MfldCat 𝕜 n) :=
+  ⟨of 𝕜 𝕜 𝕜 (modelWithCornersSelf 𝕜 𝕜)⟩
+
+/-- Bundle a normed space as a `C^n` manifold without boundary (modeled on itself). -/
+@[simps]
+abbrev ofNormedSpace (n : WithTop ℕ∞) (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
+    MfldCat.{u} 𝕜 n :=
+  of E E E (modelWithCornersSelf 𝕜 E)
+
+/-- `MfldCat 𝕜 n` has a forgetful functor to `TopCat`, sending a manifold to its underlying
+topological space and a `C^n` map to its underlying continuous map. -/
+instance : HasForget₂ (MfldCat.{u} 𝕜 n) TopCat.{u} where
+  forget₂.obj M := TopCat.of M
+  forget₂.map f := TopCat.ofHom ⟨f.hom, f.hom.contMDiff.continuous⟩
+
+-- TODO: define a functor `FGModuleCat 𝕜 ⥤ MfldCat 𝕜 n` from the category of
+-- finite-dimensional `𝕜`-vector spaces. Requires `[CompleteSpace 𝕜]` and a choice of norm on each
+-- object (e.g. via `Module.finBasis 𝕜 V` transporting the norm from `EuclideanSpace 𝕜 (Fin _)`).
+
+/-- Any diffeomorphism induces an isomorphism in `MfldCat`. -/
+@[simps]
+def isoOfDiffeomorph {M N : MfldCat.{u} 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) : M ≅ N where
+  hom := ofHom f.toContMDiffMap
+  inv := ofHom f.symm.toContMDiffMap
+  hom_inv_id := by ext x; exact f.left_inv x
+  inv_hom_id := by ext x; exact f.right_inv x
+
+/-- Any isomorphism in `MfldCat` induces a diffeomorphism. -/
+@[simps]
+def diffeomorphOfIso {M N : MfldCat.{u} 𝕜 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.{u} 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) :
+    diffeomorphOfIso (isoOfDiffeomorph f) = f := by
+  ext
+  rfl
+
+@[simp]
+theorem of_diffeomorphOfIso {M N : MfldCat.{u} 𝕜 n} (f : M ≅ N) :
+    isoOfDiffeomorph (diffeomorphOfIso f) = f := by
+  ext
+  rfl
+
+/-- The constant morphism `M ⟶ N` in `MfldCat` given by `y : N`. -/
+def const {M N : MfldCat.{u} 𝕜 n} (y : N) : M ⟶ N :=
+  ofHom ⟨fun _ ↦ y, contMDiff_const⟩
+
+@[simp]
+lemma const_apply {M N : MfldCat.{u} 𝕜 n} (y : N) (x : M) :
+    const y x = y := rfl
+
+end MfldCat

From 61c3aaa9f27d586867e368342b2bd7d40489f16c Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sat, 18 Apr 2026 20:54:21 -0400
Subject: [PATCH 02/36] Fixed CI errors. Added simp lemmas for ContMDiffMap
 analogous to those for ContinuousMap.

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean |  1 -
 Mathlib/Geometry/Manifold/ContMDiffMap.lean           | 10 ++++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index e2bac2b30cd50d..01fe5b43711f42 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -222,7 +222,6 @@ instance inhabited : Inhabited (MfldCat 𝕜 n) :=
   ⟨of 𝕜 𝕜 𝕜 (modelWithCornersSelf 𝕜 𝕜)⟩
 
 /-- Bundle a normed space as a `C^n` manifold without boundary (modeled on itself). -/
-@[simps]
 abbrev ofNormedSpace (n : WithTop ℕ∞) (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
     MfldCat.{u} 𝕜 n :=
   of E E E (modelWithCornersSelf 𝕜 E)
diff --git a/Mathlib/Geometry/Manifold/ContMDiffMap.lean b/Mathlib/Geometry/Manifold/ContMDiffMap.lean
index e0fce000c3f725..049d54c2b870e1 100644
--- a/Mathlib/Geometry/Manifold/ContMDiffMap.lean
+++ b/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⟩⟩
 

From 9364918d8d6f314e8bf5a1104e22b1c415a8a1c8 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 03:28:24 -0400
Subject: [PATCH 03/36] Reduced variable overhead.

---
 .../Manifold/Category/MfldCat/Basic.lean      | 54 ++++++-------------
 1 file changed, 16 insertions(+), 38 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 01fe5b43711f42..a67b74108e7e79 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -5,9 +5,6 @@ Authors: Jack McCarthy
 -/
 module
 
-public import Mathlib.CategoryTheory.Elementwise
-public import Mathlib.Geometry.Manifold.ContMDiffMap
-public import Mathlib.Geometry.Manifold.ContMDiff.Constructions
 public import Mathlib.Geometry.Manifold.Diffeomorph
 public import Mathlib.Topology.Category.TopCat.Basic
 
@@ -72,15 +69,22 @@ initialize_simps_projections MfldCat
 namespace MfldCat
 
 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
+  {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
 
-lemma coe_of (M : Type u) (E : Type u) (H : Type u)
-    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
-    (I : ModelWithCorners 𝕜 E H) [TopologicalSpace M] [ChartedSpace H M]
-    [IsManifold I n M] : (of (n := n) M E H I : Type u) = M := rfl
+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.{u} 𝕜 n) : of (n := n) M.carrier M.E M.H M.I = M := rfl
 
@@ -105,14 +109,7 @@ abbrev Hom.hom {M N : MfldCat.{u} 𝕜 n} (f : Hom M N) :=
   ConcreteCategory.hom (C := MfldCat 𝕜 n) f
 
 /-- Typecheck a `ContMDiffMap` as a morphism in `MfldCat`. -/
-abbrev ofHom {M N : Type u} {E E' : Type u} {H H' : Type u}
-    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
-    [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H']
-    {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
-    [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M]
-    [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' n N]
-    (f : ContMDiffMap I I' M N n) :
-    of (n := n) M E H I ⟶ of (n := n) N E' H' I' :=
+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. -/
@@ -157,16 +154,6 @@ lemma ext {M N : MfldCat 𝕜 n} {f g : M ⟶ N} (w : ∀ x : M, f x = g x) : f
 
 section ofHom
 
-variable {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]
-
 @[simp]
 lemma hom_ofHom (f : ContMDiffMap I I' X Y n) : (ofHom f).hom = f := rfl
 
@@ -201,13 +188,7 @@ def Hom.equivContMDiffMap (M N : MfldCat.{u} 𝕜 n) :
 
 /-- Replace a function coercion for a morphism `MfldCat.of X E H I ⟶ MfldCat.of Y E' H' I'` with
 the definitionally equal function coercion for a `ContMDiffMap I I' X Y n`. -/
-@[simp] theorem coe_of_of {X Y E E' H H' : Type u}
-    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
-    [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace 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]
-    {f : ContMDiffMap I I' X Y n} {x} :
+@[simp] theorem coe_of_of {f : ContMDiffMap I I' X Y n} {x} :
     @DFunLike.coe (of (n := n) X E H I ⟶ of (n := n) Y E' H' I')
       ((CategoryTheory.forget (MfldCat 𝕜 n)).obj (of (n := n) X E H I))
       (fun _ ↦ (CategoryTheory.forget (MfldCat 𝕜 n)).obj (of (n := n) Y E' H' I'))
@@ -221,20 +202,17 @@ the definitionally equal function coercion for a `ContMDiffMap I I' X Y n`. -/
 instance inhabited : Inhabited (MfldCat 𝕜 n) :=
   ⟨of 𝕜 𝕜 𝕜 (modelWithCornersSelf 𝕜 𝕜)⟩
 
-/-- Bundle a normed space as a `C^n` manifold without boundary (modeled on itself). -/
+/-- A normed space is a `C^n` manifold (modeled on itself). -/
 abbrev ofNormedSpace (n : WithTop ℕ∞) (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
     MfldCat.{u} 𝕜 n :=
   of E E E (modelWithCornersSelf 𝕜 E)
 
-/-- `MfldCat 𝕜 n` has a forgetful functor to `TopCat`, sending a manifold to its underlying
-topological space and a `C^n` map to its underlying continuous map. -/
+/-- `MfldCat 𝕜 n` has a forgetful functor to `TopCat`. -/
 instance : HasForget₂ (MfldCat.{u} 𝕜 n) TopCat.{u} where
   forget₂.obj M := TopCat.of M
   forget₂.map f := TopCat.ofHom ⟨f.hom, f.hom.contMDiff.continuous⟩
 
--- TODO: define a functor `FGModuleCat 𝕜 ⥤ MfldCat 𝕜 n` from the category of
--- finite-dimensional `𝕜`-vector spaces. Requires `[CompleteSpace 𝕜]` and a choice of norm on each
--- object (e.g. via `Module.finBasis 𝕜 V` transporting the norm from `EuclideanSpace 𝕜 (Fin _)`).
+-- TODO: define a functor `FGModuleCat 𝕜 ⥤ MfldCat 𝕜 n`.
 
 /-- Any diffeomorphism induces an isomorphism in `MfldCat`. -/
 @[simps]

From b15c221991f228ab8a271e2fc528c0111fe9a6e1 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 03:43:25 -0400
Subject: [PATCH 04/36] Added justification for universe.

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index a67b74108e7e79..e0a94046efd1ab 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -30,6 +30,11 @@ open scoped Manifold
 
 universe u
 
+/- Implementation note: `carrier`, `E`, `H`, and `I` all live in the same `Type u`. This assumption
+is essential to differential geometry because we wish to compare the linear model (`E`, `H`, `I`)
+with the manifold itself. For example, the Whitney Embedding Theorem says that an n-manifold
+should embed into `E^2m`.
+ -/
 /-- The category of `C^n` 𝕜-manifolds. -/
 structure MfldCat (𝕜 : Type u) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) where
   /-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/

From ef19c3ee33c994cd5c8be9316ee4a8ab1897e42b Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 03:46:58 -0400
Subject: [PATCH 05/36] Clean up

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index e0a94046efd1ab..a9afa26eff0a66 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -32,7 +32,7 @@ universe u
 
 /- Implementation note: `carrier`, `E`, `H`, and `I` all live in the same `Type u`. This assumption
 is essential to differential geometry because we wish to compare the linear model (`E`, `H`, `I`)
-with the manifold itself. For example, the Whitney Embedding Theorem says that an n-manifold
+with the manifold itself. Example: the Whitney Embedding Theorem says that an n-manifold
 should embed into `E^2m`.
  -/
 /-- The category of `C^n` 𝕜-manifolds. -/

From edc9395e510e8c61023392a1822fe1d21045e9d2 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 04:02:42 -0400
Subject: [PATCH 06/36] Wording

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index a9afa26eff0a66..9d7df1b728dee0 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -32,8 +32,8 @@ universe u
 
 /- Implementation note: `carrier`, `E`, `H`, and `I` all live in the same `Type u`. This assumption
 is essential to differential geometry because we wish to compare the linear model (`E`, `H`, `I`)
-with the manifold itself. Example: the Whitney Embedding Theorem says that an n-manifold
-should embed into `E^2m`.
+with the manifold itself. E.g. the Whitney Embedding Theorem says that any n-dimensional
+manifold should embed into `E^2m`.
  -/
 /-- The category of `C^n` 𝕜-manifolds. -/
 structure MfldCat (𝕜 : Type u) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) where

From 0125e2b7ff55bf96458fe8d056ccf35fbd3d2c81 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 05:24:13 -0400
Subject: [PATCH 07/36] =?UTF-8?q?Added=20universe=20polymorphism=20for=20t?=
 =?UTF-8?q?ype=20=F0=9D=95=9C.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Manifold/Category/MfldCat/Basic.lean      | 40 +++++++++----------
 1 file changed, 20 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 9d7df1b728dee0..2033cf4addbb79 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -28,7 +28,7 @@ set_option autoImplicit false
 open CategoryTheory
 open scoped Manifold
 
-universe u
+universe u v
 
 /- Implementation note: `carrier`, `E`, `H`, and `I` all live in the same `Type u`. This assumption
 is essential to differential geometry because we wish to compare the linear model (`E`, `H`, `I`)
@@ -36,7 +36,7 @@ with the manifold itself. E.g. the Whitney Embedding Theorem says that any n-dim
 manifold should embed into `E^2m`.
  -/
 /-- The category of `C^n` 𝕜-manifolds. -/
-structure MfldCat (𝕜 : Type u) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) where
+structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) where
   /-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
   of ::
   /-- The underlying type. -/
@@ -73,7 +73,7 @@ initialize_simps_projections MfldCat
 
 namespace MfldCat
 
-variable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
+variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
   {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']
@@ -91,34 +91,34 @@ 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.{u} 𝕜 n) : of (n := n) M.carrier M.E M.H M.I = M := rfl
+lemma of_carrier (M : MfldCat.{u, v} 𝕜 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 𝕜 n) where
+structure Hom (M N : MfldCat.{u, v} 𝕜 n) where
   /-- The underlying `C^n` map. -/
   hom' : ContMDiffMap M.I N.I M N n
 
-instance : Category (MfldCat 𝕜 n) where
+instance : Category (MfldCat.{u, v} 𝕜 n) where
   Hom M N := Hom M N
   id M := ⟨ContMDiffMap.id⟩
   comp f g := ⟨g.hom'.comp f.hom'⟩
 
-instance : ConcreteCategory.{u} (MfldCat 𝕜 n)
+instance : ConcreteCategory.{u} (MfldCat.{u, v} 𝕜 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.{u} 𝕜 n} (f : Hom M N) :=
-  ConcreteCategory.hom (C := MfldCat 𝕜 n) f
+abbrev Hom.hom {M N : MfldCat.{u, v} 𝕜 n} (f : Hom M N) :=
+  ConcreteCategory.hom (C := MfldCat.{u, v} 𝕜 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
+  ConcreteCategory.ofHom (C := MfldCat.{u, v} 𝕜 n) f
 
 /-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
-def Hom.Simps.hom (M N : MfldCat.{u} 𝕜 n) (f : Hom M N) :=
+def Hom.Simps.hom (M N : MfldCat.{u, v} 𝕜 n) (f : Hom M N) :=
   f.hom
 
 initialize_simps_projections Hom (hom' → hom)
@@ -186,7 +186,7 @@ end ofHom
 
 /-- Morphisms in `MfldCat` are equivalent to `ContMDiffMap`s. -/
 @[simps]
-def Hom.equivContMDiffMap (M N : MfldCat.{u} 𝕜 n) :
+def Hom.equivContMDiffMap (M N : MfldCat.{u, v} 𝕜 n) :
     (M ⟶ N) ≃ ContMDiffMap M.I N.I M N n where
   toFun f := f.hom
   invFun f := ofHom f
@@ -209,11 +209,11 @@ instance inhabited : Inhabited (MfldCat 𝕜 n) :=
 
 /-- A normed space is a `C^n` manifold (modeled on itself). -/
 abbrev ofNormedSpace (n : WithTop ℕ∞) (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
-    MfldCat.{u} 𝕜 n :=
+    MfldCat 𝕜 n :=
   of E E E (modelWithCornersSelf 𝕜 E)
 
 /-- `MfldCat 𝕜 n` has a forgetful functor to `TopCat`. -/
-instance : HasForget₂ (MfldCat.{u} 𝕜 n) TopCat.{u} where
+instance : HasForget₂ (MfldCat 𝕜 n) TopCat.{u} where
   forget₂.obj M := TopCat.of M
   forget₂.map f := TopCat.ofHom ⟨f.hom, f.hom.contMDiff.continuous⟩
 
@@ -221,7 +221,7 @@ instance : HasForget₂ (MfldCat.{u} 𝕜 n) TopCat.{u} where
 
 /-- Any diffeomorphism induces an isomorphism in `MfldCat`. -/
 @[simps]
-def isoOfDiffeomorph {M N : MfldCat.{u} 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) : M ≅ N where
+def isoOfDiffeomorph {M N : MfldCat.{u, v} 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) : M ≅ N where
   hom := ofHom f.toContMDiffMap
   inv := ofHom f.symm.toContMDiffMap
   hom_inv_id := by ext x; exact f.left_inv x
@@ -229,7 +229,7 @@ def isoOfDiffeomorph {M N : MfldCat.{u} 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N)
 
 /-- Any isomorphism in `MfldCat` induces a diffeomorphism. -/
 @[simps]
-def diffeomorphOfIso {M N : MfldCat.{u} 𝕜 n} (f : M ≅ N) : M ≃ₘ^n⟮M.I, N.I⟯ N where
+def diffeomorphOfIso {M N : MfldCat.{u, v} 𝕜 n} (f : M ≅ N) : M ≃ₘ^n⟮M.I, N.I⟯ N where
   toFun := f.hom
   invFun := f.inv
   left_inv _ := by simp
@@ -238,23 +238,23 @@ def diffeomorphOfIso {M N : MfldCat.{u} 𝕜 n} (f : M ≅ N) : M ≃ₘ^n⟮M.I
   contMDiff_invFun := f.inv.hom.contMDiff
 
 @[simp]
-theorem of_isoOfDiffeomorph {M N : MfldCat.{u} 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) :
+theorem of_isoOfDiffeomorph {M N : MfldCat 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) :
     diffeomorphOfIso (isoOfDiffeomorph f) = f := by
   ext
   rfl
 
 @[simp]
-theorem of_diffeomorphOfIso {M N : MfldCat.{u} 𝕜 n} (f : M ≅ N) :
+theorem of_diffeomorphOfIso {M N : MfldCat 𝕜 n} (f : M ≅ N) :
     isoOfDiffeomorph (diffeomorphOfIso f) = f := by
   ext
   rfl
 
 /-- The constant morphism `M ⟶ N` in `MfldCat` given by `y : N`. -/
-def const {M N : MfldCat.{u} 𝕜 n} (y : N) : M ⟶ N :=
+def const {M N : MfldCat.{u, v} 𝕜 n} (y : N) : M ⟶ N :=
   ofHom ⟨fun _ ↦ y, contMDiff_const⟩
 
 @[simp]
-lemma const_apply {M N : MfldCat.{u} 𝕜 n} (y : N) (x : M) :
+lemma const_apply {M N : MfldCat 𝕜 n} (y : N) (x : M) :
     const y x = y := rfl
 
 end MfldCat

From c4f24b1b5e381fab61d8b5fe130a4737c6992b72 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 05:27:55 -0400
Subject: [PATCH 08/36] Updated docs to explain universe polynomorphism
 situation.

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 2033cf4addbb79..ab2f761c8880a4 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -28,13 +28,12 @@ set_option autoImplicit false
 open CategoryTheory
 open scoped Manifold
 
+/- Implementation note: `carrier`, `E`, `H`, and `I` all live in the same `Type u`. This assumption
+is essential (?) to differential geometry because we wish to compare the linear model
+(`E`, `H`, `I`) with the manifold itself. E.g. the tangent bundle should also be a manifold.
+The field `𝕜` lives in a seperate `Type v`, according to the convention of `ModuleCat` -/
 universe u v
 
-/- Implementation note: `carrier`, `E`, `H`, and `I` all live in the same `Type u`. This assumption
-is essential to differential geometry because we wish to compare the linear model (`E`, `H`, `I`)
-with the manifold itself. E.g. the Whitney Embedding Theorem says that any n-dimensional
-manifold should embed into `E^2m`.
- -/
 /-- The category of `C^n` 𝕜-manifolds. -/
 structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) where
   /-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/

From 3823e594dddb953ae4dbd958bfc2581fed875619 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 05:59:17 -0400
Subject: [PATCH 09/36] Added full universe polymorphism.

---
 .../Manifold/Category/MfldCat/Basic.lean      | 46 +++++++++----------
 1 file changed, 23 insertions(+), 23 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index ab2f761c8880a4..ff35db89931e5c 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -32,18 +32,18 @@ open scoped Manifold
 is essential (?) to differential geometry because we wish to compare the linear model
 (`E`, `H`, `I`) with the manifold itself. E.g. the tangent bundle should also be a manifold.
 The field `𝕜` lives in a seperate `Type v`, according to the convention of `ModuleCat` -/
-universe u v
+universe u₁ u₂ u₃ u₄
 
 /-- The category of `C^n` 𝕜-manifolds. -/
-structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) where
+structure MfldCat (𝕜 : Type u₁) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) where
   /-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
   of ::
   /-- The underlying type. -/
-  carrier : Type u
+  carrier : Type u₂
   /-- The model normed space. -/
-  E : Type u
+  E : Type u₃
   /-- The chart space. -/
-  H : Type u
+  H : Type u₄
   [instNAG : NormedAddCommGroup E]
   [instNS : NormedSpace 𝕜 E]
   [instTopH : TopologicalSpace H]
@@ -72,8 +72,8 @@ initialize_simps_projections MfldCat
 
 namespace MfldCat
 
-variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
-  {X Y Z : Type u} {E E' E'' : Type u} {H H' H'' : Type u}
+variable {𝕜 : Type u₁} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
+  {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'']
@@ -83,41 +83,41 @@ variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
   [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⟩
+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 coe_of : (of (n := n) X E H I : Type u₂) = X := rfl
 
-lemma of_carrier (M : MfldCat.{u, v} 𝕜 n) : of (n := n) M.carrier M.E M.H M.I = M := 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
+structure Hom (M N : MfldCat.{u₁, u₂, u₃, u₄} 𝕜 n) where
   /-- The underlying `C^n` map. -/
   hom' : ContMDiffMap M.I N.I M N n
 
-instance : Category (MfldCat.{u, v} 𝕜 n) where
+instance : Category (MfldCat 𝕜 n) where
   Hom M N := Hom M N
   id M := ⟨ContMDiffMap.id⟩
   comp f g := ⟨g.hom'.comp f.hom'⟩
 
-instance : ConcreteCategory.{u} (MfldCat.{u, v} 𝕜 n)
+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.{u, v} 𝕜 n} (f : Hom M N) :=
-  ConcreteCategory.hom (C := MfldCat.{u, v} 𝕜 n) f
+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.{u, v} 𝕜 n) f
+  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) :=
+def Hom.Simps.hom (M N : MfldCat 𝕜 n) (f : Hom M N) :=
   f.hom
 
 initialize_simps_projections Hom (hom' → hom)
@@ -185,7 +185,7 @@ end ofHom
 
 /-- Morphisms in `MfldCat` are equivalent to `ContMDiffMap`s. -/
 @[simps]
-def Hom.equivContMDiffMap (M N : MfldCat.{u, v} 𝕜 n) :
+def Hom.equivContMDiffMap (M N : MfldCat 𝕜 n) :
     (M ⟶ N) ≃ ContMDiffMap M.I N.I M N n where
   toFun f := f.hom
   invFun f := ofHom f
@@ -207,12 +207,12 @@ instance inhabited : Inhabited (MfldCat 𝕜 n) :=
   ⟨of 𝕜 𝕜 𝕜 (modelWithCornersSelf 𝕜 𝕜)⟩
 
 /-- A normed space is a `C^n` manifold (modeled on itself). -/
-abbrev ofNormedSpace (n : WithTop ℕ∞) (E : Type u) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
+abbrev ofNormedSpace (n : WithTop ℕ∞) (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
+instance : HasForget₂ (MfldCat 𝕜 n) TopCat.{u₂} where
   forget₂.obj M := TopCat.of M
   forget₂.map f := TopCat.ofHom ⟨f.hom, f.hom.contMDiff.continuous⟩
 
@@ -220,7 +220,7 @@ instance : HasForget₂ (MfldCat 𝕜 n) TopCat.{u} where
 
 /-- Any diffeomorphism induces an isomorphism in `MfldCat`. -/
 @[simps]
-def isoOfDiffeomorph {M N : MfldCat.{u, v} 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) : M ≅ N where
+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
   hom_inv_id := by ext x; exact f.left_inv x
@@ -228,7 +228,7 @@ def isoOfDiffeomorph {M N : MfldCat.{u, v} 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯
 
 /-- Any isomorphism in `MfldCat` induces a diffeomorphism. -/
 @[simps]
-def diffeomorphOfIso {M N : MfldCat.{u, v} 𝕜 n} (f : M ≅ N) : M ≃ₘ^n⟮M.I, N.I⟯ N where
+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
@@ -249,7 +249,7 @@ theorem of_diffeomorphOfIso {M N : MfldCat 𝕜 n} (f : M ≅ N) :
   rfl
 
 /-- The constant morphism `M ⟶ N` in `MfldCat` given by `y : N`. -/
-def const {M N : MfldCat.{u, v} 𝕜 n} (y : N) : M ⟶ N :=
+def const {M N : MfldCat 𝕜 n} (y : N) : M ⟶ N :=
   ofHom ⟨fun _ ↦ y, contMDiff_const⟩
 
 @[simp]

From 53aeaa1cdc5558abb0ac5f071a5754783697a46f Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 06:01:09 -0400
Subject: [PATCH 10/36] Removed implementation note explaining universe
 polymorphism descision.

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index ff35db89931e5c..22d257c71fb484 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -28,10 +28,6 @@ set_option autoImplicit false
 open CategoryTheory
 open scoped Manifold
 
-/- Implementation note: `carrier`, `E`, `H`, and `I` all live in the same `Type u`. This assumption
-is essential (?) to differential geometry because we wish to compare the linear model
-(`E`, `H`, `I`) with the manifold itself. E.g. the tangent bundle should also be a manifold.
-The field `𝕜` lives in a seperate `Type v`, according to the convention of `ModuleCat` -/
 universe u₁ u₂ u₃ u₄
 
 /-- The category of `C^n` 𝕜-manifolds. -/

From 4b0d75900dce4dd449cae711a52c4aee7e6b3221 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 20:43:26 -0400
Subject: [PATCH 11/36] Added [nolint checkUnivs] to pass CI.

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 22d257c71fb484..6fd2580e0e1011 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -5,6 +5,7 @@ Authors: Jack McCarthy
 -/
 module
 
+public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 public import Mathlib.Geometry.Manifold.Diffeomorph
 public import Mathlib.Topology.Category.TopCat.Basic
 
@@ -31,6 +32,8 @@ open scoped Manifold
 universe u₁ u₂ u₃ u₄
 
 /-- The category of `C^n` 𝕜-manifolds. -/
+-- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
+@[pp_with_univ, nolint checkUnivs]
 structure MfldCat (𝕜 : Type u₁) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) where
   /-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
   of ::

From af76b4d55ac6692eb310d731a45ff59f043a2aa3 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 20 Apr 2026 12:59:49 -0400
Subject: [PATCH 12/36] Responded to first round of review from Ben Eltschig.

---
 .../Manifold/Category/MfldCat/Basic.lean      | 60 +++++++++++--------
 1 file changed, 34 insertions(+), 26 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 6fd2580e0e1011..e2fca6ce4131e0 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -10,16 +10,22 @@ public import Mathlib.Geometry.Manifold.Diffeomorph
 public import Mathlib.Topology.Category.TopCat.Basic
 
 /-!
-# Category instance for smooth manifolds
+# 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 space `E`, chart space `H`, and
+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` since we do not care about large manifolds
+  modelled on small spaces. `𝕜` is given a seperate `Type v`.
 -/
 
 @[expose] public section
@@ -27,30 +33,30 @@ finite-dimensional vector spaces over `𝕜`.
 set_option autoImplicit false
 
 open CategoryTheory
-open scoped Manifold
+open scoped Manifold ContDiff
 
-universe u₁ u₂ u₃ u₄
+universe u v
 
 /-- The category of `C^n` 𝕜-manifolds. -/
 -- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
 @[pp_with_univ, nolint checkUnivs]
-structure MfldCat (𝕜 : Type u₁) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) where
+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₂
+  carrier : Type u
   /-- The model normed space. -/
-  E : Type u₃
+  E : Type u
   /-- The chart space. -/
-  H : Type u₄
-  [instNAG : NormedAddCommGroup E]
-  [instNS : NormedSpace 𝕜 E]
-  [instTopH : TopologicalSpace H]
+  H : Type u
+  [instNormedAddCommGroup : NormedAddCommGroup E]
+  [instNormedSpace : NormedSpace 𝕜 E]
+  [instTopologicalSpaceH : TopologicalSpace H]
   /-- The model with corners. -/
   I : ModelWithCorners 𝕜 E H
-  [instTop : TopologicalSpace carrier]
-  [instCharted : ChartedSpace H carrier]
-  [instManifold : IsManifold I n carrier]
+  [instTopologicalSpace : TopologicalSpace carrier]
+  [instChartedSpace : ChartedSpace H carrier]
+  [instIsManifold : IsManifold I n carrier]
 
 section Notation
 
@@ -63,16 +69,18 @@ meta def MfldCat.delabOf : Delab := delabApp
 
 end Notation
 
-attribute [instance] MfldCat.instNAG MfldCat.instNS MfldCat.instTopH MfldCat.instTop
-  MfldCat.instCharted MfldCat.instManifold
+attribute [instance] MfldCat.instNormedAddCommGroup MfldCat.instNormedSpace
+  MfldCat.instTopologicalSpaceH MfldCat.instTopologicalSpace
+  MfldCat.instChartedSpace MfldCat.instIsManifold
 
 initialize_simps_projections MfldCat
-  (-instNAG, -instNS, -instTopH, -instTop, -instCharted, -instManifold)
+  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH, -instTopologicalSpace,
+    -instChartedSpace, -instIsManifold)
 
 namespace MfldCat
 
-variable {𝕜 : Type u₁} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
-  {X Y Z : Type u₂} {E E' E'' : Type u₃} {H H' H'' : Type u₄}
+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'']
@@ -82,18 +90,18 @@ variable {𝕜 : Type u₁} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
   [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⟩
+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 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₁, u₂, u₃, u₄} 𝕜 n) where
+structure Hom (M N : MfldCat.{u, v} 𝕜 n) where
   /-- The underlying `C^n` map. -/
   hom' : ContMDiffMap M.I N.I M N n
 
@@ -116,7 +124,7 @@ abbrev ofHom (f : ContMDiffMap I I' X Y n) : of (n := n) X E H I ⟶ of (n := n)
   ConcreteCategory.ofHom (C := MfldCat 𝕜 n) f
 
 /-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
-def Hom.Simps.hom (M N : MfldCat 𝕜 n) (f : Hom M N) :=
+def Hom.Simps.hom (M N : MfldCat.{u, v} 𝕜 n) (f : Hom M N) :=
   f.hom
 
 initialize_simps_projections Hom (hom' → hom)
@@ -206,12 +214,12 @@ instance inhabited : Inhabited (MfldCat 𝕜 n) :=
   ⟨of 𝕜 𝕜 𝕜 (modelWithCornersSelf 𝕜 𝕜)⟩
 
 /-- A normed space is a `C^n` manifold (modeled on itself). -/
-abbrev ofNormedSpace (n : WithTop ℕ∞) (E : Type u₃) [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
+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
+instance : HasForget₂ (MfldCat 𝕜 n) TopCat.{u} where
   forget₂.obj M := TopCat.of M
   forget₂.map f := TopCat.ofHom ⟨f.hom, f.hom.contMDiff.continuous⟩
 
@@ -249,7 +257,7 @@ theorem of_diffeomorphOfIso {M N : MfldCat 𝕜 n} (f : M ≅ N) :
 
 /-- The constant morphism `M ⟶ N` in `MfldCat` given by `y : N`. -/
 def const {M N : MfldCat 𝕜 n} (y : N) : M ⟶ N :=
-  ofHom ⟨fun _ ↦ y, contMDiff_const⟩
+  ofHom <| ContMDiffMap.const y
 
 @[simp]
 lemma const_apply {M N : MfldCat 𝕜 n} (y : N) (x : M) :

From 8874aeba4f886d9d2cf1415a6f64b15064643ed4 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 20 Apr 2026 13:02:19 -0400
Subject: [PATCH 13/36] Removed unnecessary import

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index e2fca6ce4131e0..d75a095766fac7 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -5,7 +5,6 @@ Authors: Jack McCarthy
 -/
 module
 
-public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 public import Mathlib.Geometry.Manifold.Diffeomorph
 public import Mathlib.Topology.Category.TopCat.Basic
 

From 83e73faa10ce8331c8976c0313a62fec70dd6114 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 20 Apr 2026 13:46:49 -0400
Subject: [PATCH 14/36] Removed nolint

---
 .../Manifold/Category/MfldCat/Basic.lean      | 273 ++++++++++++++++--
 1 file changed, 242 insertions(+), 31 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index d75a095766fac7..ed52b95969f209 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -11,20 +11,28 @@ 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 introduce two categories of `C^n` manifolds:
+* `ModelWithCorners.MfldCat I n`: the category of `C^n` manifolds modeled on a fixed
+  `I : ModelWithCorners 𝕜 E H`. For example, choosing `I = 𝓘(ℝ, EuclideanSpace ℝ (Fin d))`
+  yields the category of `C^n` real `d`-manifolds without boundary.
+* `MfldCat 𝕜 n`: the category of `C^n` 𝕜-manifolds whose model can vary from object to object.
+  Each object bundles a model vector space `E`, a model chart space `H`,
+  `I : ModelWithCorners 𝕜 E H`, and a term of `ModelWithCorners.MfldCat I n`. Thus
+  `MfldCat 𝕜 n` also includes manifolds with boundary and corners, of any dimension.
 
 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
+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` since we do not care about large manifolds
-  modelled on small spaces. `𝕜` is given a seperate `Type v`.
+* We do not assume `[FiniteDimensional 𝕜 E] [T2Space M] [SigmaCompactSpace M]`, so these categories
+  include non-Hausdorff, non-paracompact, and infite-dimensional manifolds.
+* We keep `E`, `H` and `carrier` all in the same `Type u` since we do not care about large
+  manifolds modelled on small spaces. `𝕜` is given a seperate `Type v`.
+* The split between `ModelWithCorners.MfldCat` and `MfldCat` follows the principle that it is
+  cheap to bundle an unbundled structure but expensive to do the reverse. Downstream code that
+  wants "all manifolds modeled on `I`" can use the unbundled category directly.
 -/
 
 @[expose] public section
@@ -36,14 +44,210 @@ open scoped Manifold ContDiff
 
 universe u v
 
-/-- The category of `C^n` 𝕜-manifolds. -/
--- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
+/-! ### The category `ModelWithCorners.MfldCat I n` of manifolds on a fixed model -/
+
+namespace ModelWithCorners
+
+/-- The category of `C^n` manifolds modeled on a fixed `I : ModelWithCorners 𝕜 E H`. -/
 @[pp_with_univ, nolint checkUnivs]
-structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω) where
-  /-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
+structure MfldCat {𝕜 : Type v} [NontriviallyNormedField 𝕜]
+    {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+    {H : Type u} [TopologicalSpace H]
+    (I : ModelWithCorners 𝕜 E H) (n : ℕ∞ω) where
+  /-- The object in `ModelWithCorners.MfldCat I n` associated to a type equipped with the
+  appropriate typeclasses. -/
   of ::
   /-- The underlying type. -/
   carrier : Type u
+  [instTopologicalSpace : TopologicalSpace carrier]
+  [instChartedSpace : ChartedSpace H carrier]
+  [instIsManifold : IsManifold I n carrier]
+
+attribute [instance] MfldCat.instTopologicalSpace MfldCat.instChartedSpace MfldCat.instIsManifold
+
+initialize_simps_projections MfldCat
+  (-instTopologicalSpace, -instChartedSpace, -instIsManifold)
+
+namespace MfldCat
+
+variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
+  {E : Type u} {H : Type u}
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
+  {I : ModelWithCorners 𝕜 E H}
+  {X Y Z : Type u}
+  [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 I n) (Type u) := ⟨MfldCat.carrier⟩
+
+attribute [coe] MfldCat.carrier
+
+variable (X) in
+lemma coe_of : (of (I := I) (n := n) X : Type u) = X := rfl
+
+lemma of_carrier (M : MfldCat I n) : of (I := I) (n := n) M.carrier = M := rfl
+
+/-- The type of morphisms in `ModelWithCorners.MfldCat I n`. -/
+@[ext]
+structure Hom (M N : MfldCat.{u, v} I n) where
+  /-- The underlying `C^n` map. -/
+  hom' : ContMDiffMap I I M N n
+
+instance : Category (MfldCat I n) where
+  Hom M N := Hom M N
+  id M := ⟨ContMDiffMap.id⟩
+  comp f g := ⟨g.hom'.comp f.hom'⟩
+
+instance : ConcreteCategory (MfldCat I n)
+    (fun M N => ContMDiffMap I I M N n) where
+  hom f := f.hom'
+  ofHom f := ⟨f⟩
+
+/-- Turn a morphism in `ModelWithCorners.MfldCat I n` back into a `ContMDiffMap`. -/
+abbrev Hom.hom {M N : MfldCat I n} (f : Hom M N) :=
+  ConcreteCategory.hom (C := MfldCat I n) f
+
+/-- Typecheck a `ContMDiffMap` as a morphism in `ModelWithCorners.MfldCat I n`. -/
+abbrev ofHom (f : ContMDiffMap I I X Y n) :
+    of (I := I) (n := n) X ⟶ of (I := I) (n := n) Y :=
+  ConcreteCategory.ofHom (C := MfldCat I n) f
+
+/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
+def Hom.Simps.hom (M N : MfldCat.{u, v} I n) (f : Hom M N) :=
+  f.hom
+
+initialize_simps_projections Hom (hom' → hom)
+
+@[simp]
+lemma hom_id {M : MfldCat I n} :
+    (𝟙 M : M ⟶ M).hom = ContMDiffMap.id := rfl
+
+@[simp]
+theorem id_app (M : MfldCat I n) (x : ↑M) : (𝟙 M : M ⟶ M) x = x := rfl
+
+@[simp]
+theorem coe_id (M : MfldCat I n) : (𝟙 M : M → M) = _root_.id := rfl
+
+@[simp]
+lemma hom_comp {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) :
+    (f ≫ g).hom = g.hom.comp f.hom := rfl
+
+@[simp]
+theorem comp_app {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) (x : M) :
+    (f ≫ g : M → P) x = g (f x) := rfl
+
+@[simp]
+theorem coe_comp {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) :
+    (f ≫ g : M → P) = g ∘ f := rfl
+
+@[ext]
+lemma hom_ext {M N : MfldCat I n} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g :=
+  Hom.ext hf
+
+@[ext]
+lemma ext {M N : MfldCat I n} {f g : M ⟶ N} (w : ∀ x : M, f x = g x) : f = g :=
+  ConcreteCategory.hom_ext _ _ w
+
+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 I n} (f : M ⟶ N) :
+    ofHom (Hom.hom f) = f := rfl
+
+@[simp]
+lemma ofHom_id :
+    ofHom (ContMDiffMap.id : ContMDiffMap I I X X n) = 𝟙 (of (I := I) (n := n) X) := 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
+
+lemma ofHom_apply (f : ContMDiffMap I I X Y n) (x : X) : (ofHom f) x = f x := rfl
+
+lemma hom_inv_id_apply {M N : MfldCat I n} (f : M ≅ N) (x : M) : f.inv (f.hom x) = x := by
+  simp
+
+lemma inv_hom_id_apply {M N : MfldCat I n} (f : M ≅ N) (y : N) : f.hom (f.inv y) = y := by
+  simp
+
+end ofHom
+
+/-- Morphisms in `ModelWithCorners.MfldCat I n` are equivalent to same-model `ContMDiffMap`s. -/
+@[simps]
+def Hom.equivContMDiffMap (M N : MfldCat I n) :
+    (M ⟶ N) ≃ ContMDiffMap I I M N n where
+  toFun f := f.hom
+  invFun f := ofHom f
+
+/-- Replace a function coercion for a morphism `ModelWithCorners.MfldCat.of X ⟶
+ModelWithCorners.MfldCat.of Y` with the definitionally equal function coercion for a
+`ContMDiffMap I I X Y n`. -/
+@[simp] theorem coe_of_of {f : ContMDiffMap I I X Y n} {x} :
+    @DFunLike.coe (of (I := I) (n := n) X ⟶ of (I := I) (n := n) Y)
+      ((CategoryTheory.forget (MfldCat I n)).obj (of (I := I) (n := n) X))
+      (fun _ ↦ (CategoryTheory.forget (MfldCat I n)).obj (of (I := I) (n := n) Y))
+      ConcreteCategory.instFunLike
+      (ofHom f) x =
+    @DFunLike.coe (ContMDiffMap I I X Y n) X
+      (fun _ ↦ Y) _
+      f x :=
+  rfl
+
+/-- Any diffeomorphism induces an isomorphism in `ModelWithCorners.MfldCat I n`. -/
+@[simps]
+def isoOfDiffeomorph {M N : MfldCat I n} (f : M ≃ₘ^n⟮I, I⟯ N) : M ≅ N where
+  hom := ofHom f.toContMDiffMap
+  inv := ofHom f.symm.toContMDiffMap
+  hom_inv_id := by ext x; exact f.left_inv x
+  inv_hom_id := by ext x; exact f.right_inv x
+
+/-- Any isomorphism in `ModelWithCorners.MfldCat I n` induces a diffeomorphism. -/
+@[simps]
+def diffeomorphOfIso {M N : MfldCat I n} (f : M ≅ N) : M ≃ₘ^n⟮I, 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 I n} (f : M ≃ₘ^n⟮I, I⟯ N) :
+    diffeomorphOfIso (isoOfDiffeomorph f) = f := by
+  ext
+  rfl
+
+@[simp]
+theorem of_diffeomorphOfIso {M N : MfldCat I n} (f : M ≅ N) :
+    isoOfDiffeomorph (diffeomorphOfIso f) = f := by
+  ext
+  rfl
+
+/-- The constant morphism `M ⟶ N` in `ModelWithCorners.MfldCat I n` given by `y : N`. -/
+def const {M N : MfldCat I n} (y : N) : M ⟶ N :=
+  ofHom <| ContMDiffMap.const y
+
+@[simp]
+lemma const_apply {M N : MfldCat I n} (y : N) (x : M) :
+    const y x = y := rfl
+
+end MfldCat
+
+end ModelWithCorners
+
+/-! ### The category `MfldCat 𝕜 n` of `C^n` 𝕜-manifolds with varying models -/
+
+/-- The category of `C^n` 𝕜-manifolds. Each object bundles a model `I : ModelWithCorners 𝕜 E H`
+together with a term of `ModelWithCorners.MfldCat I n`. -/
+-- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
+@[pp_with_univ, nolint checkUnivs]
+structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω) where
+  /-- Bundle an object of `ModelWithCorners.MfldCat I n` into an object of `MfldCat`. -/
+  mk ::
   /-- The model normed space. -/
   E : Type u
   /-- The chart space. -/
@@ -53,28 +257,14 @@ structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω)
   [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
+  /-- The underlying object in the fixed-model category `ModelWithCorners.MfldCat I n`. -/
+  toMfldCat : ModelWithCorners.MfldCat I n
 
 attribute [instance] MfldCat.instNormedAddCommGroup MfldCat.instNormedSpace
-  MfldCat.instTopologicalSpaceH MfldCat.instTopologicalSpace
-  MfldCat.instChartedSpace MfldCat.instIsManifold
+  MfldCat.instTopologicalSpaceH
 
 initialize_simps_projections MfldCat
-  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH, -instTopologicalSpace,
-    -instChartedSpace, -instIsManifold)
+  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH)
 
 namespace MfldCat
 
@@ -89,10 +279,31 @@ variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
   [TopologicalSpace Y] [ChartedSpace H' Y] [IsManifold I' n Y]
   [TopologicalSpace Z] [ChartedSpace H'' Z] [IsManifold I'' n Z]
 
+/-- The underlying type of an object in `MfldCat`. -/
+abbrev carrier (M : MfldCat 𝕜 n) : Type u := M.toMfldCat.carrier
+
 instance : CoeSort (MfldCat 𝕜 n) (Type u) := ⟨MfldCat.carrier⟩
 
 attribute [coe] MfldCat.carrier
 
+/-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
+abbrev of (X : Type u) (E : Type u) (H : Type u)
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
+    (I : ModelWithCorners 𝕜 E H)
+    [TopologicalSpace X] [ChartedSpace H X] [IsManifold I n X] : MfldCat.{u, v} 𝕜 n :=
+  .mk E H I (.of X)
+
+section Notation
+
+open Lean.PrettyPrinter.Delaborator
+
+/-- This prevents `MfldCat.of M E H I` being printed as `{ E := E, ... }` by
+`delabStructureInstance`. -/
+@[app_delab MfldCat.of]
+meta def delabOf : Delab := delabApp
+
+end Notation
+
 variable (X E H I) in
 lemma coe_of : (of (n := n) X E H I : Type u) = X := rfl
 

From e1e7f6f6cf7c6743b7bd9a5dc3917f8c0866081c Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 20 Apr 2026 13:49:22 -0400
Subject: [PATCH 15/36] Clean up

---
 .../Manifold/Category/MfldCat/Basic.lean      | 273 ++----------------
 1 file changed, 31 insertions(+), 242 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index ed52b95969f209..d75a095766fac7 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -11,28 +11,20 @@ public import Mathlib.Topology.Category.TopCat.Basic
 /-!
 # The category of $C^n$ manifolds
 
-We introduce two categories of `C^n` manifolds:
-* `ModelWithCorners.MfldCat I n`: the category of `C^n` manifolds modeled on a fixed
-  `I : ModelWithCorners 𝕜 E H`. For example, choosing `I = 𝓘(ℝ, EuclideanSpace ℝ (Fin d))`
-  yields the category of `C^n` real `d`-manifolds without boundary.
-* `MfldCat 𝕜 n`: the category of `C^n` 𝕜-manifolds whose model can vary from object to object.
-  Each object bundles a model vector space `E`, a model chart space `H`,
-  `I : ModelWithCorners 𝕜 E H`, and a term of `ModelWithCorners.MfldCat I n`. Thus
-  `MfldCat 𝕜 n` also includes manifolds with boundary and corners, of any dimension.
+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
+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 these categories
-  include non-Hausdorff, non-paracompact, and infite-dimensional manifolds.
-* We keep `E`, `H` and `carrier` all in the same `Type u` since we do not care about large
-  manifolds modelled on small spaces. `𝕜` is given a seperate `Type v`.
-* The split between `ModelWithCorners.MfldCat` and `MfldCat` follows the principle that it is
-  cheap to bundle an unbundled structure but expensive to do the reverse. Downstream code that
-  wants "all manifolds modeled on `I`" can use the unbundled category directly.
+* 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` since we do not care about large manifolds
+  modelled on small spaces. `𝕜` is given a seperate `Type v`.
 -/
 
 @[expose] public section
@@ -44,210 +36,14 @@ open scoped Manifold ContDiff
 
 universe u v
 
-/-! ### The category `ModelWithCorners.MfldCat I n` of manifolds on a fixed model -/
-
-namespace ModelWithCorners
-
-/-- The category of `C^n` manifolds modeled on a fixed `I : ModelWithCorners 𝕜 E H`. -/
+/-- The category of `C^n` 𝕜-manifolds. -/
+-- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
 @[pp_with_univ, nolint checkUnivs]
-structure MfldCat {𝕜 : Type v} [NontriviallyNormedField 𝕜]
-    {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-    {H : Type u} [TopologicalSpace H]
-    (I : ModelWithCorners 𝕜 E H) (n : ℕ∞ω) where
-  /-- The object in `ModelWithCorners.MfldCat I n` associated to a type equipped with the
-  appropriate typeclasses. -/
+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
-  [instTopologicalSpace : TopologicalSpace carrier]
-  [instChartedSpace : ChartedSpace H carrier]
-  [instIsManifold : IsManifold I n carrier]
-
-attribute [instance] MfldCat.instTopologicalSpace MfldCat.instChartedSpace MfldCat.instIsManifold
-
-initialize_simps_projections MfldCat
-  (-instTopologicalSpace, -instChartedSpace, -instIsManifold)
-
-namespace MfldCat
-
-variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
-  {E : Type u} {H : Type u}
-  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
-  {I : ModelWithCorners 𝕜 E H}
-  {X Y Z : Type u}
-  [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 I n) (Type u) := ⟨MfldCat.carrier⟩
-
-attribute [coe] MfldCat.carrier
-
-variable (X) in
-lemma coe_of : (of (I := I) (n := n) X : Type u) = X := rfl
-
-lemma of_carrier (M : MfldCat I n) : of (I := I) (n := n) M.carrier = M := rfl
-
-/-- The type of morphisms in `ModelWithCorners.MfldCat I n`. -/
-@[ext]
-structure Hom (M N : MfldCat.{u, v} I n) where
-  /-- The underlying `C^n` map. -/
-  hom' : ContMDiffMap I I M N n
-
-instance : Category (MfldCat I n) where
-  Hom M N := Hom M N
-  id M := ⟨ContMDiffMap.id⟩
-  comp f g := ⟨g.hom'.comp f.hom'⟩
-
-instance : ConcreteCategory (MfldCat I n)
-    (fun M N => ContMDiffMap I I M N n) where
-  hom f := f.hom'
-  ofHom f := ⟨f⟩
-
-/-- Turn a morphism in `ModelWithCorners.MfldCat I n` back into a `ContMDiffMap`. -/
-abbrev Hom.hom {M N : MfldCat I n} (f : Hom M N) :=
-  ConcreteCategory.hom (C := MfldCat I n) f
-
-/-- Typecheck a `ContMDiffMap` as a morphism in `ModelWithCorners.MfldCat I n`. -/
-abbrev ofHom (f : ContMDiffMap I I X Y n) :
-    of (I := I) (n := n) X ⟶ of (I := I) (n := n) Y :=
-  ConcreteCategory.ofHom (C := MfldCat I n) f
-
-/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
-def Hom.Simps.hom (M N : MfldCat.{u, v} I n) (f : Hom M N) :=
-  f.hom
-
-initialize_simps_projections Hom (hom' → hom)
-
-@[simp]
-lemma hom_id {M : MfldCat I n} :
-    (𝟙 M : M ⟶ M).hom = ContMDiffMap.id := rfl
-
-@[simp]
-theorem id_app (M : MfldCat I n) (x : ↑M) : (𝟙 M : M ⟶ M) x = x := rfl
-
-@[simp]
-theorem coe_id (M : MfldCat I n) : (𝟙 M : M → M) = _root_.id := rfl
-
-@[simp]
-lemma hom_comp {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) :
-    (f ≫ g).hom = g.hom.comp f.hom := rfl
-
-@[simp]
-theorem comp_app {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) (x : M) :
-    (f ≫ g : M → P) x = g (f x) := rfl
-
-@[simp]
-theorem coe_comp {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) :
-    (f ≫ g : M → P) = g ∘ f := rfl
-
-@[ext]
-lemma hom_ext {M N : MfldCat I n} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g :=
-  Hom.ext hf
-
-@[ext]
-lemma ext {M N : MfldCat I n} {f g : M ⟶ N} (w : ∀ x : M, f x = g x) : f = g :=
-  ConcreteCategory.hom_ext _ _ w
-
-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 I n} (f : M ⟶ N) :
-    ofHom (Hom.hom f) = f := rfl
-
-@[simp]
-lemma ofHom_id :
-    ofHom (ContMDiffMap.id : ContMDiffMap I I X X n) = 𝟙 (of (I := I) (n := n) X) := 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
-
-lemma ofHom_apply (f : ContMDiffMap I I X Y n) (x : X) : (ofHom f) x = f x := rfl
-
-lemma hom_inv_id_apply {M N : MfldCat I n} (f : M ≅ N) (x : M) : f.inv (f.hom x) = x := by
-  simp
-
-lemma inv_hom_id_apply {M N : MfldCat I n} (f : M ≅ N) (y : N) : f.hom (f.inv y) = y := by
-  simp
-
-end ofHom
-
-/-- Morphisms in `ModelWithCorners.MfldCat I n` are equivalent to same-model `ContMDiffMap`s. -/
-@[simps]
-def Hom.equivContMDiffMap (M N : MfldCat I n) :
-    (M ⟶ N) ≃ ContMDiffMap I I M N n where
-  toFun f := f.hom
-  invFun f := ofHom f
-
-/-- Replace a function coercion for a morphism `ModelWithCorners.MfldCat.of X ⟶
-ModelWithCorners.MfldCat.of Y` with the definitionally equal function coercion for a
-`ContMDiffMap I I X Y n`. -/
-@[simp] theorem coe_of_of {f : ContMDiffMap I I X Y n} {x} :
-    @DFunLike.coe (of (I := I) (n := n) X ⟶ of (I := I) (n := n) Y)
-      ((CategoryTheory.forget (MfldCat I n)).obj (of (I := I) (n := n) X))
-      (fun _ ↦ (CategoryTheory.forget (MfldCat I n)).obj (of (I := I) (n := n) Y))
-      ConcreteCategory.instFunLike
-      (ofHom f) x =
-    @DFunLike.coe (ContMDiffMap I I X Y n) X
-      (fun _ ↦ Y) _
-      f x :=
-  rfl
-
-/-- Any diffeomorphism induces an isomorphism in `ModelWithCorners.MfldCat I n`. -/
-@[simps]
-def isoOfDiffeomorph {M N : MfldCat I n} (f : M ≃ₘ^n⟮I, I⟯ N) : M ≅ N where
-  hom := ofHom f.toContMDiffMap
-  inv := ofHom f.symm.toContMDiffMap
-  hom_inv_id := by ext x; exact f.left_inv x
-  inv_hom_id := by ext x; exact f.right_inv x
-
-/-- Any isomorphism in `ModelWithCorners.MfldCat I n` induces a diffeomorphism. -/
-@[simps]
-def diffeomorphOfIso {M N : MfldCat I n} (f : M ≅ N) : M ≃ₘ^n⟮I, 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 I n} (f : M ≃ₘ^n⟮I, I⟯ N) :
-    diffeomorphOfIso (isoOfDiffeomorph f) = f := by
-  ext
-  rfl
-
-@[simp]
-theorem of_diffeomorphOfIso {M N : MfldCat I n} (f : M ≅ N) :
-    isoOfDiffeomorph (diffeomorphOfIso f) = f := by
-  ext
-  rfl
-
-/-- The constant morphism `M ⟶ N` in `ModelWithCorners.MfldCat I n` given by `y : N`. -/
-def const {M N : MfldCat I n} (y : N) : M ⟶ N :=
-  ofHom <| ContMDiffMap.const y
-
-@[simp]
-lemma const_apply {M N : MfldCat I n} (y : N) (x : M) :
-    const y x = y := rfl
-
-end MfldCat
-
-end ModelWithCorners
-
-/-! ### The category `MfldCat 𝕜 n` of `C^n` 𝕜-manifolds with varying models -/
-
-/-- The category of `C^n` 𝕜-manifolds. Each object bundles a model `I : ModelWithCorners 𝕜 E H`
-together with a term of `ModelWithCorners.MfldCat I n`. -/
--- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
-@[pp_with_univ, nolint checkUnivs]
-structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω) where
-  /-- Bundle an object of `ModelWithCorners.MfldCat I n` into an object of `MfldCat`. -/
-  mk ::
   /-- The model normed space. -/
   E : Type u
   /-- The chart space. -/
@@ -257,14 +53,28 @@ structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω)
   [instTopologicalSpaceH : TopologicalSpace H]
   /-- The model with corners. -/
   I : ModelWithCorners 𝕜 E H
-  /-- The underlying object in the fixed-model category `ModelWithCorners.MfldCat I n`. -/
-  toMfldCat : ModelWithCorners.MfldCat I n
+  [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.instTopologicalSpaceH MfldCat.instTopologicalSpace
+  MfldCat.instChartedSpace MfldCat.instIsManifold
 
 initialize_simps_projections MfldCat
-  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH)
+  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH, -instTopologicalSpace,
+    -instChartedSpace, -instIsManifold)
 
 namespace MfldCat
 
@@ -279,31 +89,10 @@ variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
   [TopologicalSpace Y] [ChartedSpace H' Y] [IsManifold I' n Y]
   [TopologicalSpace Z] [ChartedSpace H'' Z] [IsManifold I'' n Z]
 
-/-- The underlying type of an object in `MfldCat`. -/
-abbrev carrier (M : MfldCat 𝕜 n) : Type u := M.toMfldCat.carrier
-
 instance : CoeSort (MfldCat 𝕜 n) (Type u) := ⟨MfldCat.carrier⟩
 
 attribute [coe] MfldCat.carrier
 
-/-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
-abbrev of (X : Type u) (E : Type u) (H : Type u)
-    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
-    (I : ModelWithCorners 𝕜 E H)
-    [TopologicalSpace X] [ChartedSpace H X] [IsManifold I n X] : MfldCat.{u, v} 𝕜 n :=
-  .mk E H I (.of X)
-
-section Notation
-
-open Lean.PrettyPrinter.Delaborator
-
-/-- This prevents `MfldCat.of M E H I` being printed as `{ E := E, ... }` by
-`delabStructureInstance`. -/
-@[app_delab MfldCat.of]
-meta def delabOf : Delab := delabApp
-
-end Notation
-
 variable (X E H I) in
 lemma coe_of : (of (n := n) X E H I : Type u) = X := rfl
 

From 1b4bee95d2b88ef242c740028c0bc39881334caf Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 20 Apr 2026 13:54:46 -0400
Subject: [PATCH 16/36] Revert "Clean up"

This reverts commit e1e7f6f6cf7c6743b7bd9a5dc3917f8c0866081c.
---
 .../Manifold/Category/MfldCat/Basic.lean      | 273 ++++++++++++++++--
 1 file changed, 242 insertions(+), 31 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index d75a095766fac7..ed52b95969f209 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -11,20 +11,28 @@ 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 introduce two categories of `C^n` manifolds:
+* `ModelWithCorners.MfldCat I n`: the category of `C^n` manifolds modeled on a fixed
+  `I : ModelWithCorners 𝕜 E H`. For example, choosing `I = 𝓘(ℝ, EuclideanSpace ℝ (Fin d))`
+  yields the category of `C^n` real `d`-manifolds without boundary.
+* `MfldCat 𝕜 n`: the category of `C^n` 𝕜-manifolds whose model can vary from object to object.
+  Each object bundles a model vector space `E`, a model chart space `H`,
+  `I : ModelWithCorners 𝕜 E H`, and a term of `ModelWithCorners.MfldCat I n`. Thus
+  `MfldCat 𝕜 n` also includes manifolds with boundary and corners, of any dimension.
 
 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
+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` since we do not care about large manifolds
-  modelled on small spaces. `𝕜` is given a seperate `Type v`.
+* We do not assume `[FiniteDimensional 𝕜 E] [T2Space M] [SigmaCompactSpace M]`, so these categories
+  include non-Hausdorff, non-paracompact, and infite-dimensional manifolds.
+* We keep `E`, `H` and `carrier` all in the same `Type u` since we do not care about large
+  manifolds modelled on small spaces. `𝕜` is given a seperate `Type v`.
+* The split between `ModelWithCorners.MfldCat` and `MfldCat` follows the principle that it is
+  cheap to bundle an unbundled structure but expensive to do the reverse. Downstream code that
+  wants "all manifolds modeled on `I`" can use the unbundled category directly.
 -/
 
 @[expose] public section
@@ -36,14 +44,210 @@ open scoped Manifold ContDiff
 
 universe u v
 
-/-- The category of `C^n` 𝕜-manifolds. -/
--- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
+/-! ### The category `ModelWithCorners.MfldCat I n` of manifolds on a fixed model -/
+
+namespace ModelWithCorners
+
+/-- The category of `C^n` manifolds modeled on a fixed `I : ModelWithCorners 𝕜 E H`. -/
 @[pp_with_univ, nolint checkUnivs]
-structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω) where
-  /-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
+structure MfldCat {𝕜 : Type v} [NontriviallyNormedField 𝕜]
+    {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+    {H : Type u} [TopologicalSpace H]
+    (I : ModelWithCorners 𝕜 E H) (n : ℕ∞ω) where
+  /-- The object in `ModelWithCorners.MfldCat I n` associated to a type equipped with the
+  appropriate typeclasses. -/
   of ::
   /-- The underlying type. -/
   carrier : Type u
+  [instTopologicalSpace : TopologicalSpace carrier]
+  [instChartedSpace : ChartedSpace H carrier]
+  [instIsManifold : IsManifold I n carrier]
+
+attribute [instance] MfldCat.instTopologicalSpace MfldCat.instChartedSpace MfldCat.instIsManifold
+
+initialize_simps_projections MfldCat
+  (-instTopologicalSpace, -instChartedSpace, -instIsManifold)
+
+namespace MfldCat
+
+variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
+  {E : Type u} {H : Type u}
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
+  {I : ModelWithCorners 𝕜 E H}
+  {X Y Z : Type u}
+  [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 I n) (Type u) := ⟨MfldCat.carrier⟩
+
+attribute [coe] MfldCat.carrier
+
+variable (X) in
+lemma coe_of : (of (I := I) (n := n) X : Type u) = X := rfl
+
+lemma of_carrier (M : MfldCat I n) : of (I := I) (n := n) M.carrier = M := rfl
+
+/-- The type of morphisms in `ModelWithCorners.MfldCat I n`. -/
+@[ext]
+structure Hom (M N : MfldCat.{u, v} I n) where
+  /-- The underlying `C^n` map. -/
+  hom' : ContMDiffMap I I M N n
+
+instance : Category (MfldCat I n) where
+  Hom M N := Hom M N
+  id M := ⟨ContMDiffMap.id⟩
+  comp f g := ⟨g.hom'.comp f.hom'⟩
+
+instance : ConcreteCategory (MfldCat I n)
+    (fun M N => ContMDiffMap I I M N n) where
+  hom f := f.hom'
+  ofHom f := ⟨f⟩
+
+/-- Turn a morphism in `ModelWithCorners.MfldCat I n` back into a `ContMDiffMap`. -/
+abbrev Hom.hom {M N : MfldCat I n} (f : Hom M N) :=
+  ConcreteCategory.hom (C := MfldCat I n) f
+
+/-- Typecheck a `ContMDiffMap` as a morphism in `ModelWithCorners.MfldCat I n`. -/
+abbrev ofHom (f : ContMDiffMap I I X Y n) :
+    of (I := I) (n := n) X ⟶ of (I := I) (n := n) Y :=
+  ConcreteCategory.ofHom (C := MfldCat I n) f
+
+/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
+def Hom.Simps.hom (M N : MfldCat.{u, v} I n) (f : Hom M N) :=
+  f.hom
+
+initialize_simps_projections Hom (hom' → hom)
+
+@[simp]
+lemma hom_id {M : MfldCat I n} :
+    (𝟙 M : M ⟶ M).hom = ContMDiffMap.id := rfl
+
+@[simp]
+theorem id_app (M : MfldCat I n) (x : ↑M) : (𝟙 M : M ⟶ M) x = x := rfl
+
+@[simp]
+theorem coe_id (M : MfldCat I n) : (𝟙 M : M → M) = _root_.id := rfl
+
+@[simp]
+lemma hom_comp {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) :
+    (f ≫ g).hom = g.hom.comp f.hom := rfl
+
+@[simp]
+theorem comp_app {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) (x : M) :
+    (f ≫ g : M → P) x = g (f x) := rfl
+
+@[simp]
+theorem coe_comp {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) :
+    (f ≫ g : M → P) = g ∘ f := rfl
+
+@[ext]
+lemma hom_ext {M N : MfldCat I n} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g :=
+  Hom.ext hf
+
+@[ext]
+lemma ext {M N : MfldCat I n} {f g : M ⟶ N} (w : ∀ x : M, f x = g x) : f = g :=
+  ConcreteCategory.hom_ext _ _ w
+
+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 I n} (f : M ⟶ N) :
+    ofHom (Hom.hom f) = f := rfl
+
+@[simp]
+lemma ofHom_id :
+    ofHom (ContMDiffMap.id : ContMDiffMap I I X X n) = 𝟙 (of (I := I) (n := n) X) := 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
+
+lemma ofHom_apply (f : ContMDiffMap I I X Y n) (x : X) : (ofHom f) x = f x := rfl
+
+lemma hom_inv_id_apply {M N : MfldCat I n} (f : M ≅ N) (x : M) : f.inv (f.hom x) = x := by
+  simp
+
+lemma inv_hom_id_apply {M N : MfldCat I n} (f : M ≅ N) (y : N) : f.hom (f.inv y) = y := by
+  simp
+
+end ofHom
+
+/-- Morphisms in `ModelWithCorners.MfldCat I n` are equivalent to same-model `ContMDiffMap`s. -/
+@[simps]
+def Hom.equivContMDiffMap (M N : MfldCat I n) :
+    (M ⟶ N) ≃ ContMDiffMap I I M N n where
+  toFun f := f.hom
+  invFun f := ofHom f
+
+/-- Replace a function coercion for a morphism `ModelWithCorners.MfldCat.of X ⟶
+ModelWithCorners.MfldCat.of Y` with the definitionally equal function coercion for a
+`ContMDiffMap I I X Y n`. -/
+@[simp] theorem coe_of_of {f : ContMDiffMap I I X Y n} {x} :
+    @DFunLike.coe (of (I := I) (n := n) X ⟶ of (I := I) (n := n) Y)
+      ((CategoryTheory.forget (MfldCat I n)).obj (of (I := I) (n := n) X))
+      (fun _ ↦ (CategoryTheory.forget (MfldCat I n)).obj (of (I := I) (n := n) Y))
+      ConcreteCategory.instFunLike
+      (ofHom f) x =
+    @DFunLike.coe (ContMDiffMap I I X Y n) X
+      (fun _ ↦ Y) _
+      f x :=
+  rfl
+
+/-- Any diffeomorphism induces an isomorphism in `ModelWithCorners.MfldCat I n`. -/
+@[simps]
+def isoOfDiffeomorph {M N : MfldCat I n} (f : M ≃ₘ^n⟮I, I⟯ N) : M ≅ N where
+  hom := ofHom f.toContMDiffMap
+  inv := ofHom f.symm.toContMDiffMap
+  hom_inv_id := by ext x; exact f.left_inv x
+  inv_hom_id := by ext x; exact f.right_inv x
+
+/-- Any isomorphism in `ModelWithCorners.MfldCat I n` induces a diffeomorphism. -/
+@[simps]
+def diffeomorphOfIso {M N : MfldCat I n} (f : M ≅ N) : M ≃ₘ^n⟮I, 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 I n} (f : M ≃ₘ^n⟮I, I⟯ N) :
+    diffeomorphOfIso (isoOfDiffeomorph f) = f := by
+  ext
+  rfl
+
+@[simp]
+theorem of_diffeomorphOfIso {M N : MfldCat I n} (f : M ≅ N) :
+    isoOfDiffeomorph (diffeomorphOfIso f) = f := by
+  ext
+  rfl
+
+/-- The constant morphism `M ⟶ N` in `ModelWithCorners.MfldCat I n` given by `y : N`. -/
+def const {M N : MfldCat I n} (y : N) : M ⟶ N :=
+  ofHom <| ContMDiffMap.const y
+
+@[simp]
+lemma const_apply {M N : MfldCat I n} (y : N) (x : M) :
+    const y x = y := rfl
+
+end MfldCat
+
+end ModelWithCorners
+
+/-! ### The category `MfldCat 𝕜 n` of `C^n` 𝕜-manifolds with varying models -/
+
+/-- The category of `C^n` 𝕜-manifolds. Each object bundles a model `I : ModelWithCorners 𝕜 E H`
+together with a term of `ModelWithCorners.MfldCat I n`. -/
+-- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
+@[pp_with_univ, nolint checkUnivs]
+structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω) where
+  /-- Bundle an object of `ModelWithCorners.MfldCat I n` into an object of `MfldCat`. -/
+  mk ::
   /-- The model normed space. -/
   E : Type u
   /-- The chart space. -/
@@ -53,28 +257,14 @@ structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω)
   [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
+  /-- The underlying object in the fixed-model category `ModelWithCorners.MfldCat I n`. -/
+  toMfldCat : ModelWithCorners.MfldCat I n
 
 attribute [instance] MfldCat.instNormedAddCommGroup MfldCat.instNormedSpace
-  MfldCat.instTopologicalSpaceH MfldCat.instTopologicalSpace
-  MfldCat.instChartedSpace MfldCat.instIsManifold
+  MfldCat.instTopologicalSpaceH
 
 initialize_simps_projections MfldCat
-  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH, -instTopologicalSpace,
-    -instChartedSpace, -instIsManifold)
+  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH)
 
 namespace MfldCat
 
@@ -89,10 +279,31 @@ variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
   [TopologicalSpace Y] [ChartedSpace H' Y] [IsManifold I' n Y]
   [TopologicalSpace Z] [ChartedSpace H'' Z] [IsManifold I'' n Z]
 
+/-- The underlying type of an object in `MfldCat`. -/
+abbrev carrier (M : MfldCat 𝕜 n) : Type u := M.toMfldCat.carrier
+
 instance : CoeSort (MfldCat 𝕜 n) (Type u) := ⟨MfldCat.carrier⟩
 
 attribute [coe] MfldCat.carrier
 
+/-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
+abbrev of (X : Type u) (E : Type u) (H : Type u)
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
+    (I : ModelWithCorners 𝕜 E H)
+    [TopologicalSpace X] [ChartedSpace H X] [IsManifold I n X] : MfldCat.{u, v} 𝕜 n :=
+  .mk E H I (.of X)
+
+section Notation
+
+open Lean.PrettyPrinter.Delaborator
+
+/-- This prevents `MfldCat.of M E H I` being printed as `{ E := E, ... }` by
+`delabStructureInstance`. -/
+@[app_delab MfldCat.of]
+meta def delabOf : Delab := delabApp
+
+end Notation
+
 variable (X E H I) in
 lemma coe_of : (of (n := n) X E H I : Type u) = X := rfl
 

From c66b1cf87ad9d56eabbdee9a71d313b184a5ecf6 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 20 Apr 2026 13:54:46 -0400
Subject: [PATCH 17/36] Revert "Removed nolint"

This reverts commit 83e73faa10ce8331c8976c0313a62fec70dd6114.
---
 .../Manifold/Category/MfldCat/Basic.lean      | 273 ++----------------
 1 file changed, 31 insertions(+), 242 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index ed52b95969f209..d75a095766fac7 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -11,28 +11,20 @@ public import Mathlib.Topology.Category.TopCat.Basic
 /-!
 # The category of $C^n$ manifolds
 
-We introduce two categories of `C^n` manifolds:
-* `ModelWithCorners.MfldCat I n`: the category of `C^n` manifolds modeled on a fixed
-  `I : ModelWithCorners 𝕜 E H`. For example, choosing `I = 𝓘(ℝ, EuclideanSpace ℝ (Fin d))`
-  yields the category of `C^n` real `d`-manifolds without boundary.
-* `MfldCat 𝕜 n`: the category of `C^n` 𝕜-manifolds whose model can vary from object to object.
-  Each object bundles a model vector space `E`, a model chart space `H`,
-  `I : ModelWithCorners 𝕜 E H`, and a term of `ModelWithCorners.MfldCat I n`. Thus
-  `MfldCat 𝕜 n` also includes manifolds with boundary and corners, of any dimension.
+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
+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 these categories
-  include non-Hausdorff, non-paracompact, and infite-dimensional manifolds.
-* We keep `E`, `H` and `carrier` all in the same `Type u` since we do not care about large
-  manifolds modelled on small spaces. `𝕜` is given a seperate `Type v`.
-* The split between `ModelWithCorners.MfldCat` and `MfldCat` follows the principle that it is
-  cheap to bundle an unbundled structure but expensive to do the reverse. Downstream code that
-  wants "all manifolds modeled on `I`" can use the unbundled category directly.
+* 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` since we do not care about large manifolds
+  modelled on small spaces. `𝕜` is given a seperate `Type v`.
 -/
 
 @[expose] public section
@@ -44,210 +36,14 @@ open scoped Manifold ContDiff
 
 universe u v
 
-/-! ### The category `ModelWithCorners.MfldCat I n` of manifolds on a fixed model -/
-
-namespace ModelWithCorners
-
-/-- The category of `C^n` manifolds modeled on a fixed `I : ModelWithCorners 𝕜 E H`. -/
+/-- The category of `C^n` 𝕜-manifolds. -/
+-- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
 @[pp_with_univ, nolint checkUnivs]
-structure MfldCat {𝕜 : Type v} [NontriviallyNormedField 𝕜]
-    {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-    {H : Type u} [TopologicalSpace H]
-    (I : ModelWithCorners 𝕜 E H) (n : ℕ∞ω) where
-  /-- The object in `ModelWithCorners.MfldCat I n` associated to a type equipped with the
-  appropriate typeclasses. -/
+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
-  [instTopologicalSpace : TopologicalSpace carrier]
-  [instChartedSpace : ChartedSpace H carrier]
-  [instIsManifold : IsManifold I n carrier]
-
-attribute [instance] MfldCat.instTopologicalSpace MfldCat.instChartedSpace MfldCat.instIsManifold
-
-initialize_simps_projections MfldCat
-  (-instTopologicalSpace, -instChartedSpace, -instIsManifold)
-
-namespace MfldCat
-
-variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
-  {E : Type u} {H : Type u}
-  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
-  {I : ModelWithCorners 𝕜 E H}
-  {X Y Z : Type u}
-  [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 I n) (Type u) := ⟨MfldCat.carrier⟩
-
-attribute [coe] MfldCat.carrier
-
-variable (X) in
-lemma coe_of : (of (I := I) (n := n) X : Type u) = X := rfl
-
-lemma of_carrier (M : MfldCat I n) : of (I := I) (n := n) M.carrier = M := rfl
-
-/-- The type of morphisms in `ModelWithCorners.MfldCat I n`. -/
-@[ext]
-structure Hom (M N : MfldCat.{u, v} I n) where
-  /-- The underlying `C^n` map. -/
-  hom' : ContMDiffMap I I M N n
-
-instance : Category (MfldCat I n) where
-  Hom M N := Hom M N
-  id M := ⟨ContMDiffMap.id⟩
-  comp f g := ⟨g.hom'.comp f.hom'⟩
-
-instance : ConcreteCategory (MfldCat I n)
-    (fun M N => ContMDiffMap I I M N n) where
-  hom f := f.hom'
-  ofHom f := ⟨f⟩
-
-/-- Turn a morphism in `ModelWithCorners.MfldCat I n` back into a `ContMDiffMap`. -/
-abbrev Hom.hom {M N : MfldCat I n} (f : Hom M N) :=
-  ConcreteCategory.hom (C := MfldCat I n) f
-
-/-- Typecheck a `ContMDiffMap` as a morphism in `ModelWithCorners.MfldCat I n`. -/
-abbrev ofHom (f : ContMDiffMap I I X Y n) :
-    of (I := I) (n := n) X ⟶ of (I := I) (n := n) Y :=
-  ConcreteCategory.ofHom (C := MfldCat I n) f
-
-/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
-def Hom.Simps.hom (M N : MfldCat.{u, v} I n) (f : Hom M N) :=
-  f.hom
-
-initialize_simps_projections Hom (hom' → hom)
-
-@[simp]
-lemma hom_id {M : MfldCat I n} :
-    (𝟙 M : M ⟶ M).hom = ContMDiffMap.id := rfl
-
-@[simp]
-theorem id_app (M : MfldCat I n) (x : ↑M) : (𝟙 M : M ⟶ M) x = x := rfl
-
-@[simp]
-theorem coe_id (M : MfldCat I n) : (𝟙 M : M → M) = _root_.id := rfl
-
-@[simp]
-lemma hom_comp {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) :
-    (f ≫ g).hom = g.hom.comp f.hom := rfl
-
-@[simp]
-theorem comp_app {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) (x : M) :
-    (f ≫ g : M → P) x = g (f x) := rfl
-
-@[simp]
-theorem coe_comp {M N P : MfldCat I n} (f : M ⟶ N) (g : N ⟶ P) :
-    (f ≫ g : M → P) = g ∘ f := rfl
-
-@[ext]
-lemma hom_ext {M N : MfldCat I n} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g :=
-  Hom.ext hf
-
-@[ext]
-lemma ext {M N : MfldCat I n} {f g : M ⟶ N} (w : ∀ x : M, f x = g x) : f = g :=
-  ConcreteCategory.hom_ext _ _ w
-
-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 I n} (f : M ⟶ N) :
-    ofHom (Hom.hom f) = f := rfl
-
-@[simp]
-lemma ofHom_id :
-    ofHom (ContMDiffMap.id : ContMDiffMap I I X X n) = 𝟙 (of (I := I) (n := n) X) := 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
-
-lemma ofHom_apply (f : ContMDiffMap I I X Y n) (x : X) : (ofHom f) x = f x := rfl
-
-lemma hom_inv_id_apply {M N : MfldCat I n} (f : M ≅ N) (x : M) : f.inv (f.hom x) = x := by
-  simp
-
-lemma inv_hom_id_apply {M N : MfldCat I n} (f : M ≅ N) (y : N) : f.hom (f.inv y) = y := by
-  simp
-
-end ofHom
-
-/-- Morphisms in `ModelWithCorners.MfldCat I n` are equivalent to same-model `ContMDiffMap`s. -/
-@[simps]
-def Hom.equivContMDiffMap (M N : MfldCat I n) :
-    (M ⟶ N) ≃ ContMDiffMap I I M N n where
-  toFun f := f.hom
-  invFun f := ofHom f
-
-/-- Replace a function coercion for a morphism `ModelWithCorners.MfldCat.of X ⟶
-ModelWithCorners.MfldCat.of Y` with the definitionally equal function coercion for a
-`ContMDiffMap I I X Y n`. -/
-@[simp] theorem coe_of_of {f : ContMDiffMap I I X Y n} {x} :
-    @DFunLike.coe (of (I := I) (n := n) X ⟶ of (I := I) (n := n) Y)
-      ((CategoryTheory.forget (MfldCat I n)).obj (of (I := I) (n := n) X))
-      (fun _ ↦ (CategoryTheory.forget (MfldCat I n)).obj (of (I := I) (n := n) Y))
-      ConcreteCategory.instFunLike
-      (ofHom f) x =
-    @DFunLike.coe (ContMDiffMap I I X Y n) X
-      (fun _ ↦ Y) _
-      f x :=
-  rfl
-
-/-- Any diffeomorphism induces an isomorphism in `ModelWithCorners.MfldCat I n`. -/
-@[simps]
-def isoOfDiffeomorph {M N : MfldCat I n} (f : M ≃ₘ^n⟮I, I⟯ N) : M ≅ N where
-  hom := ofHom f.toContMDiffMap
-  inv := ofHom f.symm.toContMDiffMap
-  hom_inv_id := by ext x; exact f.left_inv x
-  inv_hom_id := by ext x; exact f.right_inv x
-
-/-- Any isomorphism in `ModelWithCorners.MfldCat I n` induces a diffeomorphism. -/
-@[simps]
-def diffeomorphOfIso {M N : MfldCat I n} (f : M ≅ N) : M ≃ₘ^n⟮I, 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 I n} (f : M ≃ₘ^n⟮I, I⟯ N) :
-    diffeomorphOfIso (isoOfDiffeomorph f) = f := by
-  ext
-  rfl
-
-@[simp]
-theorem of_diffeomorphOfIso {M N : MfldCat I n} (f : M ≅ N) :
-    isoOfDiffeomorph (diffeomorphOfIso f) = f := by
-  ext
-  rfl
-
-/-- The constant morphism `M ⟶ N` in `ModelWithCorners.MfldCat I n` given by `y : N`. -/
-def const {M N : MfldCat I n} (y : N) : M ⟶ N :=
-  ofHom <| ContMDiffMap.const y
-
-@[simp]
-lemma const_apply {M N : MfldCat I n} (y : N) (x : M) :
-    const y x = y := rfl
-
-end MfldCat
-
-end ModelWithCorners
-
-/-! ### The category `MfldCat 𝕜 n` of `C^n` 𝕜-manifolds with varying models -/
-
-/-- The category of `C^n` 𝕜-manifolds. Each object bundles a model `I : ModelWithCorners 𝕜 E H`
-together with a term of `ModelWithCorners.MfldCat I n`. -/
--- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
-@[pp_with_univ, nolint checkUnivs]
-structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω) where
-  /-- Bundle an object of `ModelWithCorners.MfldCat I n` into an object of `MfldCat`. -/
-  mk ::
   /-- The model normed space. -/
   E : Type u
   /-- The chart space. -/
@@ -257,14 +53,28 @@ structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω)
   [instTopologicalSpaceH : TopologicalSpace H]
   /-- The model with corners. -/
   I : ModelWithCorners 𝕜 E H
-  /-- The underlying object in the fixed-model category `ModelWithCorners.MfldCat I n`. -/
-  toMfldCat : ModelWithCorners.MfldCat I n
+  [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.instTopologicalSpaceH MfldCat.instTopologicalSpace
+  MfldCat.instChartedSpace MfldCat.instIsManifold
 
 initialize_simps_projections MfldCat
-  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH)
+  (-instNormedAddCommGroup, -instNormedSpace, -instTopologicalSpaceH, -instTopologicalSpace,
+    -instChartedSpace, -instIsManifold)
 
 namespace MfldCat
 
@@ -279,31 +89,10 @@ variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
   [TopologicalSpace Y] [ChartedSpace H' Y] [IsManifold I' n Y]
   [TopologicalSpace Z] [ChartedSpace H'' Z] [IsManifold I'' n Z]
 
-/-- The underlying type of an object in `MfldCat`. -/
-abbrev carrier (M : MfldCat 𝕜 n) : Type u := M.toMfldCat.carrier
-
 instance : CoeSort (MfldCat 𝕜 n) (Type u) := ⟨MfldCat.carrier⟩
 
 attribute [coe] MfldCat.carrier
 
-/-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
-abbrev of (X : Type u) (E : Type u) (H : Type u)
-    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
-    (I : ModelWithCorners 𝕜 E H)
-    [TopologicalSpace X] [ChartedSpace H X] [IsManifold I n X] : MfldCat.{u, v} 𝕜 n :=
-  .mk E H I (.of X)
-
-section Notation
-
-open Lean.PrettyPrinter.Delaborator
-
-/-- This prevents `MfldCat.of M E H I` being printed as `{ E := E, ... }` by
-`delabStructureInstance`. -/
-@[app_delab MfldCat.of]
-meta def delabOf : Delab := delabApp
-
-end Notation
-
 variable (X E H I) in
 lemma coe_of : (of (n := n) X E H I : Type u) = X := rfl
 

From 17c6dbde00b603829fbaa2a2422d227dc0d4922c Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 20 Apr 2026 13:56:12 -0400
Subject: [PATCH 18/36] Removed nolint

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index d75a095766fac7..26017a20bd264f 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -37,8 +37,6 @@ open scoped Manifold ContDiff
 universe u v
 
 /-- The category of `C^n` 𝕜-manifolds. -/
--- Note: Copied from `PFunctor`, but do we need seperate universe levels here? Seems perverse.
-@[pp_with_univ, nolint checkUnivs]
 structure MfldCat (𝕜 : Type v) [NontriviallyNormedField 𝕜] (n : ℕ∞ω) where
   /-- The object in `MfldCat` associated to a type equipped with the appropriate typeclasses. -/
   of ::

From 350feafe1dd5f053b9b1273cdc8d28f3995b0afe Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Fri, 24 Apr 2026 20:38:38 -0400
Subject: [PATCH 19/36] Apply suggestion from @dagurtomas

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 26017a20bd264f..31920e24c441db 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -177,13 +177,6 @@ lemma ofHom_id :
 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
 
-lemma ofHom_apply (f : ContMDiffMap I I' X Y n) (x : X) : (ofHom f) x = f x := rfl
-
-lemma hom_inv_id_apply {M N : MfldCat 𝕜 n} (f : M ≅ N) (x : M) : f.inv (f.hom x) = x := by
-  simp
-
-lemma inv_hom_id_apply {M N : MfldCat 𝕜 n} (f : M ≅ N) (y : N) : f.hom (f.inv y) = y := by
-  simp
 
 end ofHom
 

From a657b91dfc952717512e643a92e2e8413743f881 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Fri, 24 Apr 2026 20:39:10 -0400
Subject: [PATCH 20/36] Apply suggestion from @dagurtomas

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 .../Geometry/Manifold/Category/MfldCat/Basic.lean    | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 31920e24c441db..a9193991bdce88 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -187,18 +187,6 @@ def Hom.equivContMDiffMap (M N : MfldCat 𝕜 n) :
   toFun f := f.hom
   invFun f := ofHom f
 
-/-- Replace a function coercion for a morphism `MfldCat.of X E H I ⟶ MfldCat.of Y E' H' I'` with
-the definitionally equal function coercion for a `ContMDiffMap I I' X Y n`. -/
-@[simp] theorem coe_of_of {f : ContMDiffMap I I' X Y n} {x} :
-    @DFunLike.coe (of (n := n) X E H I ⟶ of (n := n) Y E' H' I')
-      ((CategoryTheory.forget (MfldCat 𝕜 n)).obj (of (n := n) X E H I))
-      (fun _ ↦ (CategoryTheory.forget (MfldCat 𝕜 n)).obj (of (n := n) Y E' H' I'))
-      ConcreteCategory.instFunLike
-      (ofHom f) x =
-    @DFunLike.coe (ContMDiffMap I I' X Y n) X
-      (fun _ ↦ Y) _
-      f x :=
-  rfl
 
 instance inhabited : Inhabited (MfldCat 𝕜 n) :=
   ⟨of 𝕜 𝕜 𝕜 (modelWithCornersSelf 𝕜 𝕜)⟩

From 1d00a662fac232252187350c7445f8e3f6f4558c Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Fri, 24 Apr 2026 20:39:37 -0400
Subject: [PATCH 21/36] Apply suggestion from @dagurtomas

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index a9193991bdce88..10f8abb143bc98 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -229,8 +229,7 @@ theorem of_isoOfDiffeomorph {M N : MfldCat 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯
 
 @[simp]
 theorem of_diffeomorphOfIso {M N : MfldCat 𝕜 n} (f : M ≅ N) :
-    isoOfDiffeomorph (diffeomorphOfIso f) = f := by
-  ext
+    isoOfDiffeomorph (diffeomorphOfIso f) = f :=
   rfl
 
 /-- The constant morphism `M ⟶ N` in `MfldCat` given by `y : N`. -/

From 70d85045b1daab3ff7c358f7186690894a955b35 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Fri, 24 Apr 2026 20:39:51 -0400
Subject: [PATCH 22/36] Apply suggestion from @dagurtomas

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 10f8abb143bc98..60837d6eac8543 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -223,8 +223,7 @@ def diffeomorphOfIso {M N : MfldCat 𝕜 n} (f : M ≅ N) : M ≃ₘ^n⟮M.I, N.
 
 @[simp]
 theorem of_isoOfDiffeomorph {M N : MfldCat 𝕜 n} (f : M ≃ₘ^n⟮M.I, N.I⟯ N) :
-    diffeomorphOfIso (isoOfDiffeomorph f) = f := by
-  ext
+    diffeomorphOfIso (isoOfDiffeomorph f) = f :=
   rfl
 
 @[simp]

From a6b73b25d64fff1c2caee9e9e31ea3b358210648 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Fri, 24 Apr 2026 20:40:01 -0400
Subject: [PATCH 23/36] Apply suggestion from @dagurtomas

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 60837d6eac8543..92665cdcbca10f 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -208,8 +208,6 @@ instance : HasForget₂ (MfldCat 𝕜 n) TopCat.{u} where
 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
-  hom_inv_id := by ext x; exact f.left_inv x
-  inv_hom_id := by ext x; exact f.right_inv x
 
 /-- Any isomorphism in `MfldCat` induces a diffeomorphism. -/
 @[simps]

From 51e5072d610cc169c1b072bb157f08b69ae93ad4 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Fri, 24 Apr 2026 20:41:22 -0400
Subject: [PATCH 24/36] Apply suggestions from code review

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 .../Manifold/Category/MfldCat/Basic.lean      | 32 +------------------
 1 file changed, 1 insertion(+), 31 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 92665cdcbca10f..4730fefdbccb96 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -23,14 +23,11 @@ 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` since we do not care about large manifolds
-  modelled on small spaces. `𝕜` is given a seperate `Type v`.
+* We keep `E`, `H` and `carrier` all in the same `Type u`; `𝕜` is given a seperate `Type v`.
 -/
 
 @[expose] public section
 
-set_option autoImplicit false
-
 open CategoryTheory
 open scoped Manifold ContDiff
 
@@ -134,31 +131,10 @@ The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep
 lemma hom_id {M : MfldCat 𝕜 n} :
     (𝟙 M : M ⟶ M).hom = ContMDiffMap.id := rfl
 
-@[simp]
-theorem id_app (M : MfldCat 𝕜 n) (x : ↑M) : (𝟙 M : M ⟶ M) x = x := rfl
-
-@[simp]
-theorem coe_id (M : MfldCat 𝕜 n) : (𝟙 M : M → M) = _root_.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
 
-@[simp]
-theorem comp_app {M N P : MfldCat 𝕜 n} (f : M ⟶ N) (g : N ⟶ P) (x : M) :
-    (f ≫ g : M → P) x = g (f x) := rfl
-
-@[simp]
-theorem coe_comp {M N P : MfldCat 𝕜 n} (f : M ⟶ N) (g : N ⟶ P) :
-    (f ≫ g : M → P) = g ∘ f := rfl
-
-@[ext]
-lemma hom_ext {M N : MfldCat 𝕜 n} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g :=
-  Hom.ext hf
-
-@[ext]
-lemma ext {M N : MfldCat 𝕜 n} {f g : M ⟶ N} (w : ∀ x : M, f x = g x) : f = g :=
-  ConcreteCategory.hom_ext _ _ w
 
 section ofHom
 
@@ -180,12 +156,6 @@ lemma ofHom_comp (f : ContMDiffMap I I' X Y n) (g : ContMDiffMap I' I'' Y Z n) :
 
 end ofHom
 
-/-- Morphisms in `MfldCat` are equivalent to `ContMDiffMap`s. -/
-@[simps]
-def Hom.equivContMDiffMap (M N : MfldCat 𝕜 n) :
-    (M ⟶ N) ≃ ContMDiffMap M.I N.I M N n where
-  toFun f := f.hom
-  invFun f := ofHom f
 
 
 instance inhabited : Inhabited (MfldCat 𝕜 n) :=

From 2faa31f4bf676a62cf7b19c80cdf5eb6fa2a1db4 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Fri, 24 Apr 2026 20:46:26 -0400
Subject: [PATCH 25/36] Updated module docstring.

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 4730fefdbccb96..08d2c37519eaa5 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -24,6 +24,10 @@ finite-dimensional vector spaces over `𝕜`.
 * 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`.
+* Show that `MfldCat` is a `CartesianMonoidalCategory`.
 -/
 
 @[expose] public section
@@ -171,8 +175,6 @@ instance : HasForget₂ (MfldCat 𝕜 n) TopCat.{u} where
   forget₂.obj M := TopCat.of M
   forget₂.map f := TopCat.ofHom ⟨f.hom, f.hom.contMDiff.continuous⟩
 
--- TODO: define a functor `FGModuleCat 𝕜 ⥤ MfldCat 𝕜 n`.
-
 /-- 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

From b355864b7146d3cf5ab1d84f24c6a0e9491e0157 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Fri, 24 Apr 2026 20:56:23 -0400
Subject: [PATCH 26/36] Made `Hom` constructor private

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 08d2c37519eaa5..a46c88bd7f6c8b 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -100,14 +100,19 @@ lemma of_carrier (M : MfldCat 𝕜 n) : of (n := n) M.carrier M.E M.H M.I = M :=
 /-- 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'
@@ -157,11 +162,8 @@ lemma ofHom_id :
 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 𝕜 𝕜)⟩
 

From ccf72ba9a375ac314826e97c0acab5c90836584a Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 26 Apr 2026 18:05:23 -0400
Subject: [PATCH 27/36] ...

Added CatesianMonoidal structure analogous to GrpCat
---
 Mathlib.lean                                  |  1 +
 .../Category/MfldCat/CartesianMonoidal.lean   | 66 +++++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 1667cc3fa2c1b6..0e3a8cad35c394 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4483,6 +4483,7 @@ 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
diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
new file mode 100644
index 00000000000000..d46644ae67a1fc
--- /dev/null
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
@@ -0,0 +1,66 @@
+/-
+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
+
+/-!
+# The cartesian monoidal structure on `MfldCat`
+
+We endow `MfldCat 𝕜 n` with its cartesian monoidal structure: the monoidal product is the
+product manifold `prodObj M N`, and the unit is the singleton `PUnit`, viewed as a
+zero-dimensional `𝕜`-manifold (`point`). We also derive the induced braided category structure.
+-/
+
+@[expose] public section
+
+open CategoryTheory Limits MonoidalCategory
+open scoped Manifold ContDiff
+
+universe u v
+
+namespace MfldCat
+
+variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
+
+/-- The product of two manifolds as an object of `MfldCat`. The chart space is
+`ModelProd M.H N.H` and the model is `M.I.prod N.I`, so `prodObj M N` is the product manifold
+in the standard sense. -/
+def prodObj (M N : MfldCat.{u} 𝕜 n) : MfldCat.{u} 𝕜 n :=
+  of (M × N) (M.E × N.E) (ModelProd M.H N.H) (M.I.prod N.I)
+
+/-- Limit data for the binary product of `M` and `N` in `MfldCat`, using `prodObj M N`. -/
+def binaryProductLimitCone (M N : MfldCat.{u} 𝕜 n) : LimitCone (pair M N) where
+  cone := BinaryFan.mk (P := prodObj M N)
+    (ofHom ⟨Prod.fst, contMDiff_fst⟩) (ofHom ⟨Prod.snd, contMDiff_snd⟩)
+  isLimit := BinaryFan.IsLimit.mk _
+    (fun l r => ofHom ⟨fun s => (l s, r s), l.hom.contMDiff.prodMk r.hom.contMDiff⟩)
+    (fun _ _ => rfl) (fun _ _ => rfl)
+    (fun _ _ _ h₁ h₂ => by
+      ext x
+      exact Prod.ext (ConcreteCategory.congr_hom h₁ x) (ConcreteCategory.congr_hom h₂ x))
+
+/-- The singleton `PUnit`, viewed as a zero-dimensional `𝕜`-manifold. We use `PUnit.{u + 1}`
+(rather than `Fin 0 → 𝕜`, which lives in `𝕜`'s universe) so that `point` exists in
+`MfldCat.{u} 𝕜 n` for any universe `v` of `𝕜`. -/
+def point : MfldCat.{u} 𝕜 n := ofNormedSpace n PUnit.{u + 1}
+
+/-- The point manifold is terminal in `MfldCat 𝕜 n`. -/
+def isTerminalPoint : IsTerminal (point (𝕜 := 𝕜) (n := n)) :=
+  IsTerminal.ofUniqueHom (fun _ => ofHom ⟨fun _ => PUnit.unit, contMDiff_const⟩)
+    (fun _ _ => by ext; rfl)
+
+/-- We choose `prodObj M N` as the product of `M` and `N` and `point` as the terminal object. -/
+noncomputable instance cartesianMonoidalCategory :
+    CartesianMonoidalCategory (MfldCat.{u} 𝕜 n) :=
+  .ofChosenFiniteProducts ⟨_, isTerminalPoint⟩ binaryProductLimitCone
+
+noncomputable instance : BraidedCategory (MfldCat.{u} 𝕜 n) := .ofCartesianMonoidalCategory
+
+@[simp] theorem tensorObj_eq (M N : MfldCat.{u} 𝕜 n) : (M ⊗ N) = prodObj M N := rfl
+
+end MfldCat

From 46643c443950f0d4cf7e826e605605f87ef482fd Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 26 Apr 2026 18:41:13 -0400
Subject: [PATCH 28/36] Removed TODO

---
 Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index a46c88bd7f6c8b..5a94de71cf9332 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -27,7 +27,6 @@ finite-dimensional vector spaces over `𝕜`.
 
 # Future Work
 * Define a functor `FGModuleCat 𝕜 ⥤ MfldCat 𝕜 n`.
-* Show that `MfldCat` is a `CartesianMonoidalCategory`.
 -/
 
 @[expose] public section

From 71a4ba104a1d927a441ea094b8fdc82cb43fef0f Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Tue, 28 Apr 2026 01:51:30 -0400
Subject: [PATCH 29/36] Inlined point

---
 .../Category/MfldCat/CartesianMonoidal.lean   | 25 ++++++++-----------
 1 file changed, 10 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
index d46644ae67a1fc..efa8a0e9a03f01 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
@@ -13,7 +13,7 @@ public import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 
 We endow `MfldCat 𝕜 n` with its cartesian monoidal structure: the monoidal product is the
 product manifold `prodObj M N`, and the unit is the singleton `PUnit`, viewed as a
-zero-dimensional `𝕜`-manifold (`point`). We also derive the induced braided category structure.
+zero-dimensional `𝕜`-manifold. We also derive the induced braided category structure.
 -/
 
 @[expose] public section
@@ -35,8 +35,7 @@ def prodObj (M N : MfldCat.{u} 𝕜 n) : MfldCat.{u} 𝕜 n :=
 
 /-- Limit data for the binary product of `M` and `N` in `MfldCat`, using `prodObj M N`. -/
 def binaryProductLimitCone (M N : MfldCat.{u} 𝕜 n) : LimitCone (pair M N) where
-  cone := BinaryFan.mk (P := prodObj M N)
-    (ofHom ⟨Prod.fst, contMDiff_fst⟩) (ofHom ⟨Prod.snd, contMDiff_snd⟩)
+  cone := BinaryFan.mk (ofHom ⟨Prod.fst, contMDiff_fst⟩) (ofHom ⟨Prod.snd, contMDiff_snd⟩)
   isLimit := BinaryFan.IsLimit.mk _
     (fun l r => ofHom ⟨fun s => (l s, r s), l.hom.contMDiff.prodMk r.hom.contMDiff⟩)
     (fun _ _ => rfl) (fun _ _ => rfl)
@@ -44,20 +43,16 @@ def binaryProductLimitCone (M N : MfldCat.{u} 𝕜 n) : LimitCone (pair M N) whe
       ext x
       exact Prod.ext (ConcreteCategory.congr_hom h₁ x) (ConcreteCategory.congr_hom h₂ x))
 
-/-- The singleton `PUnit`, viewed as a zero-dimensional `𝕜`-manifold. We use `PUnit.{u + 1}`
-(rather than `Fin 0 → 𝕜`, which lives in `𝕜`'s universe) so that `point` exists in
-`MfldCat.{u} 𝕜 n` for any universe `v` of `𝕜`. -/
-def point : MfldCat.{u} 𝕜 n := ofNormedSpace n PUnit.{u + 1}
-
-/-- The point manifold is terminal in `MfldCat 𝕜 n`. -/
-def isTerminalPoint : IsTerminal (point (𝕜 := 𝕜) (n := n)) :=
-  IsTerminal.ofUniqueHom (fun _ => ofHom ⟨fun _ => PUnit.unit, contMDiff_const⟩)
-    (fun _ _ => by ext; rfl)
-
-/-- We choose `prodObj M N` as the product of `M` and `N` and `point` as the terminal object. -/
+/-- We choose `prodObj M N` as the product of `M` and `N`, and the singleton `PUnit.{u + 1}`
+(viewed as a zero-dimensional `𝕜`-manifold via `ofNormedSpace`) as the terminal object. We use
+`PUnit.{u + 1}` rather than `Fin 0 → 𝕜` so that the unit object exists in `MfldCat.{u} 𝕜 n` for
+any universe `v` of `𝕜`. -/
 noncomputable instance cartesianMonoidalCategory :
     CartesianMonoidalCategory (MfldCat.{u} 𝕜 n) :=
-  .ofChosenFiniteProducts ⟨_, isTerminalPoint⟩ binaryProductLimitCone
+  .ofChosenFiniteProducts
+    ⟨_, IsTerminal.ofUniqueHom (Y := ofNormedSpace n PUnit.{u + 1})
+      (fun _ => ofHom ⟨fun _ => PUnit.unit, contMDiff_const⟩) (fun _ _ => by ext)⟩
+    binaryProductLimitCone
 
 noncomputable instance : BraidedCategory (MfldCat.{u} 𝕜 n) := .ofCartesianMonoidalCategory
 

From a9be79e9d6aab93183fd77383687ee2afd7616e8 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Tue, 28 Apr 2026 02:12:16 -0400
Subject: [PATCH 30/36] Improved docstrings

---
 .../Category/MfldCat/CartesianMonoidal.lean   | 31 +++++++------------
 1 file changed, 11 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
index efa8a0e9a03f01..a2290d07a9d684 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
@@ -9,11 +9,11 @@ public import Mathlib.Geometry.Manifold.Category.MfldCat.Basic
 public import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 
 /-!
-# The cartesian monoidal structure on `MfldCat`
+# Cartesian monoidal structure on `MfldCat`
 
 We endow `MfldCat 𝕜 n` with its cartesian monoidal structure: the monoidal product is the
-product manifold `prodObj M N`, and the unit is the singleton `PUnit`, viewed as a
-zero-dimensional `𝕜`-manifold. We also derive the induced braided category structure.
+product manifold, and the unit is `PUnit`, viewed as a zero-dimensional `𝕜`-manifold.
+We also derive the induced braided category structure.
 -/
 
 @[expose] public section
@@ -27,26 +27,15 @@ namespace MfldCat
 
 variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
 
-/-- The product of two manifolds as an object of `MfldCat`. The chart space is
-`ModelProd M.H N.H` and the model is `M.I.prod N.I`, so `prodObj M N` is the product manifold
-in the standard sense. -/
-def prodObj (M N : MfldCat.{u} 𝕜 n) : MfldCat.{u} 𝕜 n :=
-  of (M × N) (M.E × N.E) (ModelProd M.H N.H) (M.I.prod N.I)
-
-/-- Limit data for the binary product of `M` and `N` in `MfldCat`, using `prodObj M N`. -/
+/-- Limit data for a binary product in `MfldCat`, using the product manifold `M × N`. -/
 def binaryProductLimitCone (M N : MfldCat.{u} 𝕜 n) : LimitCone (pair M N) where
   cone := BinaryFan.mk (ofHom ⟨Prod.fst, contMDiff_fst⟩) (ofHom ⟨Prod.snd, contMDiff_snd⟩)
   isLimit := BinaryFan.IsLimit.mk _
     (fun l r => ofHom ⟨fun s => (l s, r s), l.hom.contMDiff.prodMk r.hom.contMDiff⟩)
-    (fun _ _ => rfl) (fun _ _ => rfl)
-    (fun _ _ _ h₁ h₂ => by
-      ext x
-      exact Prod.ext (ConcreteCategory.congr_hom h₁ x) (ConcreteCategory.congr_hom h₂ x))
-
-/-- We choose `prodObj M N` as the product of `M` and `N`, and the singleton `PUnit.{u + 1}`
-(viewed as a zero-dimensional `𝕜`-manifold via `ofNormedSpace`) as the terminal object. We use
-`PUnit.{u + 1}` rather than `Fin 0 → 𝕜` so that the unit object exists in `MfldCat.{u} 𝕜 n` for
-any universe `v` of `𝕜`. -/
+    (fun _ _ => rfl) (fun _ _ => rfl) (by cat_disch)
+
+/-- We choose the product manifold `M × N` as the product of `M` and `N`, and `PUnit` as the
+terminal object. -/
 noncomputable instance cartesianMonoidalCategory :
     CartesianMonoidalCategory (MfldCat.{u} 𝕜 n) :=
   .ofChosenFiniteProducts
@@ -56,6 +45,8 @@ noncomputable instance cartesianMonoidalCategory :
 
 noncomputable instance : BraidedCategory (MfldCat.{u} 𝕜 n) := .ofCartesianMonoidalCategory
 
-@[simp] theorem tensorObj_eq (M N : MfldCat.{u} 𝕜 n) : (M ⊗ N) = prodObj M N := rfl
+@[simp]
+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

From 599a903ee1f037c5b81232996b412f8dda2f2a62 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Tue, 28 Apr 2026 02:20:00 -0400
Subject: [PATCH 31/36] micro golf

---
 .../Manifold/Category/MfldCat/CartesianMonoidal.lean         | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
index a2290d07a9d684..c564c35e1685ea 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
@@ -30,8 +30,7 @@ variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
 /-- Limit data for a binary product in `MfldCat`, using the product manifold `M × N`. -/
 def binaryProductLimitCone (M N : MfldCat.{u} 𝕜 n) : LimitCone (pair M N) where
   cone := BinaryFan.mk (ofHom ⟨Prod.fst, contMDiff_fst⟩) (ofHom ⟨Prod.snd, contMDiff_snd⟩)
-  isLimit := BinaryFan.IsLimit.mk _
-    (fun l r => ofHom ⟨fun s => (l s, r s), l.hom.contMDiff.prodMk r.hom.contMDiff⟩)
+  isLimit := BinaryFan.IsLimit.mk _ (fun l r => ofHom (l.hom.prodMk r.hom))
     (fun _ _ => rfl) (fun _ _ => rfl) (by cat_disch)
 
 /-- We choose the product manifold `M × N` as the product of `M` and `N`, and `PUnit` as the
@@ -40,7 +39,7 @@ noncomputable instance cartesianMonoidalCategory :
     CartesianMonoidalCategory (MfldCat.{u} 𝕜 n) :=
   .ofChosenFiniteProducts
     ⟨_, IsTerminal.ofUniqueHom (Y := ofNormedSpace n PUnit.{u + 1})
-      (fun _ => ofHom ⟨fun _ => PUnit.unit, contMDiff_const⟩) (fun _ _ => by ext)⟩
+      (fun _ => const PUnit.unit) (fun _ _ => by ext)⟩
     binaryProductLimitCone
 
 noncomputable instance : BraidedCategory (MfldCat.{u} 𝕜 n) := .ofCartesianMonoidalCategory

From b5bc47b6fe3deb81f17d22db5c64f395b7b02079 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Tue, 28 Apr 2026 02:26:59 -0400
Subject: [PATCH 32/36] micro golf

---
 .../Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean   | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
index c564c35e1685ea..bbacd5e0b92e09 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
@@ -29,7 +29,7 @@ variable {𝕜 : Type v} [NontriviallyNormedField 𝕜] {n : ℕ∞ω}
 
 /-- Limit data for a binary product in `MfldCat`, using the product manifold `M × N`. -/
 def binaryProductLimitCone (M N : MfldCat.{u} 𝕜 n) : LimitCone (pair M N) where
-  cone := BinaryFan.mk (ofHom ⟨Prod.fst, contMDiff_fst⟩) (ofHom ⟨Prod.snd, contMDiff_snd⟩)
+  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)
 

From 00aaddacf5bf0170cacc2a762ac8c3f8b276ca7b Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Tue, 28 Apr 2026 02:31:16 -0400
Subject: [PATCH 33/36] Added implementation note

---
 .../Manifold/Category/MfldCat/CartesianMonoidal.lean         | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
index bbacd5e0b92e09..8ee3bd823486b7 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
@@ -14,6 +14,11 @@ public import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 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

From 152e333407be9d8bcdc40bf34c98bfd5181b17a2 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Tue, 28 Apr 2026 02:37:45 -0400
Subject: [PATCH 34/36] Docstring change

---
 .../Manifold/Category/MfldCat/CartesianMonoidal.lean         | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
index 8ee3bd823486b7..1c2072b8ea6745 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
@@ -38,8 +38,8 @@ def binaryProductLimitCone (M N : MfldCat.{u} 𝕜 n) : LimitCone (pair M N) whe
   isLimit := BinaryFan.IsLimit.mk _ (fun l r => ofHom (l.hom.prodMk r.hom))
     (fun _ _ => rfl) (fun _ _ => rfl) (by cat_disch)
 
-/-- We choose the product manifold `M × N` as the product of `M` and `N`, and `PUnit` as the
-terminal object. -/
+/-- We choose the product manifold of `M` and `N` (with carrier `M × N`) as the binary product,
+and `PUnit` as the terminal object. -/
 noncomputable instance cartesianMonoidalCategory :
     CartesianMonoidalCategory (MfldCat.{u} 𝕜 n) :=
   .ofChosenFiniteProducts
@@ -49,7 +49,6 @@ noncomputable instance cartesianMonoidalCategory :
 
 noncomputable instance : BraidedCategory (MfldCat.{u} 𝕜 n) := .ofCartesianMonoidalCategory
 
-@[simp]
 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
 

From 7e5b39a0805db3d39bfd738251a35a2d4054d404 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Tue, 28 Apr 2026 02:47:41 -0400
Subject: [PATCH 35/36] Added simps

---
 .../Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean    | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
index 1c2072b8ea6745..b3ffbffbfe4619 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
@@ -33,6 +33,7 @@ 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))

From 309e7cddce6ef0364d90ab7ffe499242d2c2c4b5 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Tue, 28 Apr 2026 02:59:41 -0400
Subject: [PATCH 36/36] Improved docstring

---
 .../Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
index b3ffbffbfe4619..8fe3b75c3eb823 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/CartesianMonoidal.lean
@@ -39,8 +39,8 @@ def binaryProductLimitCone (M N : MfldCat.{u} 𝕜 n) : LimitCone (pair M N) whe
   isLimit := BinaryFan.IsLimit.mk _ (fun l r => ofHom (l.hom.prodMk r.hom))
     (fun _ _ => rfl) (fun _ _ => rfl) (by cat_disch)
 
-/-- We choose the product manifold of `M` and `N` (with carrier `M × N`) as the binary product,
-and `PUnit` as the terminal object. -/
+/-- 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