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/10] 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/10] 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 3d17542d3c61506fa18564f86c1c954781f2d2a8 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 05:18:10 -0400
Subject: [PATCH 03/10] Added tangent functor.

---
 .../Manifold/Category/MfldCat/Basic.lean      | 28 ++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 01fe5b43711f42..d38d47ed1e6326 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -8,7 +8,9 @@ module
 public import Mathlib.CategoryTheory.Elementwise
 public import Mathlib.Geometry.Manifold.ContMDiffMap
 public import Mathlib.Geometry.Manifold.ContMDiff.Constructions
+public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 public import Mathlib.Geometry.Manifold.Diffeomorph
+public import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
 public import Mathlib.Topology.Category.TopCat.Basic
 
 /-!
@@ -29,7 +31,7 @@ finite-dimensional vector spaces over `𝕜`.
 set_option autoImplicit false
 
 open CategoryTheory
-open scoped Manifold
+open scoped Manifold ContDiff
 
 universe u
 
@@ -274,4 +276,28 @@ def const {M N : MfldCat.{u} 𝕜 n} (y : N) : M ⟶ N :=
 lemma const_apply {M N : MfldCat.{u} 𝕜 n} (y : N) (x : M) :
     const y x = y := rfl
 
+section TangentFunctor
+
+variable (M : MfldCat.{u} 𝕜 (n + 1))
+
+local instance : IsManifold M.I 1 M := IsManifold.of_le (n := n + 1) le_add_self
+local instance : IsManifold M.I n M := IsManifold.of_le (n := n + 1) le_self_add
+-- This implies  `TangentBundle M.I M` is a manifold by `Bundle.TotalSpace.isManifold`
+local instance : ContMDiffVectorBundle n M.E (TangentSpace M.I : M → Type u) M.I :=
+  TangentBundle.contMDiffVectorBundle
+
+
+/-- The tangent functor `MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n` -- Sends a `C^(n+1)` manifold to its
+tangent bundle; Sends a `C^(n+1)` map to it's pushforward. -/
+noncomputable def tangentFunctor : MfldCat.{u} 𝕜 (n + 1) ⥤ MfldCat.{u} 𝕜 n where
+  obj M := of (TangentBundle M.I M) (M.E × M.E) (ModelProd M.H M.E) M.I.tangent
+  map {M N} f :=
+    ofHom ⟨tangentMap M.I N.I f.hom, f.hom.contMDiff.contMDiff_tangentMap le_rfl⟩
+  map_id _ := Hom.ext <| Subtype.ext tangentMap_id
+  map_comp f g := Hom.ext <| Subtype.ext <| tangentMap_comp
+    (g.hom.contMDiff.mdifferentiable (by simp))
+    (f.hom.contMDiff.mdifferentiable (by simp))
+
+end TangentFunctor
+
 end MfldCat

From d1b20275e5095a9aafee36b9ad9f897ea0856db3 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 05:40:10 -0400
Subject: [PATCH 04/10] Changed to 2 universes instead of 1.

---
 .../Manifold/Category/MfldCat/Basic.lean      | 102 +++++++-----------
 1 file changed, 41 insertions(+), 61 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index d38d47ed1e6326..4e110573d642f0 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -5,12 +5,7 @@ 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.ContMDiffMFDeriv
 public import Mathlib.Geometry.Manifold.Diffeomorph
-public import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
 public import Mathlib.Topology.Category.TopCat.Basic
 
 /-!
@@ -31,12 +26,16 @@ finite-dimensional vector spaces over `𝕜`.
 set_option autoImplicit false
 
 open CategoryTheory
-open scoped Manifold ContDiff
+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. 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
 
 /-- 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,52 +72,52 @@ 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']
+  [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
+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 {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
+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
 
 /-- 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)
@@ -159,16 +158,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
 
@@ -196,20 +185,14 @@ 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
 
 /-- 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'))
@@ -223,24 +206,21 @@ 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 :=
+    MfldCat 𝕜 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
+/-- `MfldCat 𝕜 n` has a forgetful functor to `TopCat`. -/
+instance : HasForget₂ (MfldCat 𝕜 n) TopCat.{u} where
   forget₂.obj M := TopCat.of M
   forget₂.map f := TopCat.ofHom ⟨f.hom, f.hom.contMDiff.continuous⟩
 
--- 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]
-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
@@ -248,7 +228,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
@@ -257,23 +237,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
 
 section TangentFunctor

From 8a35dc63ae579d081c189394ae8824841749123e Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 06:06:24 -0400
Subject: [PATCH 05/10] Added universe polymorphism for tangentFunctor.

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

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index 4e110573d642f0..e2c38e67ef9fec 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
 
@@ -28,22 +29,18 @@ 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
+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 +69,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 +80,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 +182,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 +204,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 +217,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 +225,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 +246,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]
@@ -258,21 +255,22 @@ lemma const_apply {M N : MfldCat 𝕜 n} (y : N) (x : M) :
 
 section TangentFunctor
 
-variable (M : MfldCat.{u} 𝕜 (n + 1))
+variable (M : MfldCat 𝕜 (n + 1))
 
 local instance : IsManifold M.I 1 M := IsManifold.of_le (n := n + 1) le_add_self
 local instance : IsManifold M.I n M := IsManifold.of_le (n := n + 1) le_self_add
 -- This implies  `TangentBundle M.I M` is a manifold by `Bundle.TotalSpace.isManifold`
-local instance : ContMDiffVectorBundle n M.E (TangentSpace M.I : M → Type u) M.I :=
+local instance : ContMDiffVectorBundle n M.E (TangentSpace M.I : M → Type u₃) M.I :=
   TangentBundle.contMDiffVectorBundle
 
 
 /-- The tangent functor `MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n` -- Sends a `C^(n+1)` manifold to its
 tangent bundle; Sends a `C^(n+1)` map to it's pushforward. -/
-noncomputable def tangentFunctor : MfldCat.{u} 𝕜 (n + 1) ⥤ MfldCat.{u} 𝕜 n where
+noncomputable def tangentFunctor :
+    MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n where
   obj M := of (TangentBundle M.I M) (M.E × M.E) (ModelProd M.H M.E) M.I.tangent
   map {M N} f :=
-    ofHom ⟨tangentMap M.I N.I f.hom, f.hom.contMDiff.contMDiff_tangentMap le_rfl⟩
+    ofHom ⟨tangentMap M.I N.I f.hom, ContMDiff.contMDiff_tangentMap f.hom.contMDiff le_rfl⟩
   map_id _ := Hom.ext <| Subtype.ext tangentMap_id
   map_comp f g := Hom.ext <| Subtype.ext <| tangentMap_comp
     (g.hom.contMDiff.mdifferentiable (by simp))

From 7d4554639d536c95b0b0e0656a6e846283991acd Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 19:34:42 -0400
Subject: [PATCH 06/10] Pulled out the Tangent Functor into a seperate file.

---
 Mathlib.lean                                  |  1 +
 .../Manifold/Category/MfldCat/Basic.lean      | 25 ---------
 .../Category/MfldCat/TangentFunctor.lean      | 51 +++++++++++++++++++
 3 files changed, 52 insertions(+), 25 deletions(-)
 create mode 100644 Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 212f0cd349b9a8..d2bbd7576603de 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4481,6 +4481,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.TangentFunctor
 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
index e2c38e67ef9fec..d65101e3f0d166 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -253,29 +253,4 @@ def const {M N : MfldCat 𝕜 n} (y : N) : M ⟶ N :=
 lemma const_apply {M N : MfldCat 𝕜 n} (y : N) (x : M) :
     const y x = y := rfl
 
-section TangentFunctor
-
-variable (M : MfldCat 𝕜 (n + 1))
-
-local instance : IsManifold M.I 1 M := IsManifold.of_le (n := n + 1) le_add_self
-local instance : IsManifold M.I n M := IsManifold.of_le (n := n + 1) le_self_add
--- This implies  `TangentBundle M.I M` is a manifold by `Bundle.TotalSpace.isManifold`
-local instance : ContMDiffVectorBundle n M.E (TangentSpace M.I : M → Type u₃) M.I :=
-  TangentBundle.contMDiffVectorBundle
-
-
-/-- The tangent functor `MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n` -- Sends a `C^(n+1)` manifold to its
-tangent bundle; Sends a `C^(n+1)` map to it's pushforward. -/
-noncomputable def tangentFunctor :
-    MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n where
-  obj M := of (TangentBundle M.I M) (M.E × M.E) (ModelProd M.H M.E) M.I.tangent
-  map {M N} f :=
-    ofHom ⟨tangentMap M.I N.I f.hom, ContMDiff.contMDiff_tangentMap f.hom.contMDiff le_rfl⟩
-  map_id _ := Hom.ext <| Subtype.ext tangentMap_id
-  map_comp f g := Hom.ext <| Subtype.ext <| tangentMap_comp
-    (g.hom.contMDiff.mdifferentiable (by simp))
-    (f.hom.contMDiff.mdifferentiable (by simp))
-
-end TangentFunctor
-
 end MfldCat
diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
new file mode 100644
index 00000000000000..c7a3f791a11570
--- /dev/null
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
@@ -0,0 +1,51 @@
+/-
+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.Geometry.Manifold.ContMDiffMFDeriv
+
+/-!
+# The tangent functor on `MfldCat`
+
+We define the tangent functor `MfldCat.tangentFunctor : MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n`, sending a
+`C^(n+1)` manifold to its tangent bundle and a `C^(n+1)` map to its pushforward (tangent map).
+-/
+
+@[expose] public section
+
+set_option autoImplicit false
+
+open CategoryTheory
+open scoped Manifold
+
+universe u₁ u₂ u₃ u₄
+
+namespace MfldCat
+
+variable {𝕜 : Type u₁} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
+
+variable (M : MfldCat.{u₁, u₂, u₃, u₄} 𝕜 (n + 1))
+
+local instance : IsManifold M.I 1 M := IsManifold.of_le (n := n + 1) le_add_self
+local instance : IsManifold M.I n M := IsManifold.of_le (n := n + 1) le_self_add
+/- This implies `TangentBundle M.I M` is a manifold by `Bundle.TotalSpace.isManifold`. -/
+local instance : ContMDiffVectorBundle n M.E (TangentSpace M.I : M → Type u₃) M.I :=
+  TangentBundle.contMDiffVectorBundle
+
+/-- The tangent functor `MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n` sends a `C^(n+1)` manifold to its
+tangent bundle and a `C^(n+1)` map to its pushforward (tangent map). -/
+noncomputable def tangentFunctor :
+    MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n where
+  obj M := of (TangentBundle M.I M) (M.E × M.E) (ModelProd M.H M.E) M.I.tangent
+  map {M N} f :=
+    ofHom ⟨tangentMap M.I N.I f.hom, ContMDiff.contMDiff_tangentMap f.hom.contMDiff le_rfl⟩
+  map_id _ := Hom.ext <| Subtype.ext tangentMap_id
+  map_comp f g := Hom.ext <| Subtype.ext <| tangentMap_comp
+    (g.hom.contMDiff.mdifferentiable (by simp))
+    (f.hom.contMDiff.mdifferentiable (by simp))
+
+end MfldCat

From 3d9fc8591c1174ee40e4e2b09db901604c409b19 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 21:20:54 -0400
Subject: [PATCH 07/10] Clean up

---
 .../Manifold/Category/MfldCat/TangentFunctor.lean     | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
index c7a3f791a11570..d20cb0ec9c6091 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
@@ -17,8 +17,6 @@ We define the tangent functor `MfldCat.tangentFunctor : MfldCat 𝕜 (n + 1) ⥤
 
 @[expose] public section
 
-set_option autoImplicit false
-
 open CategoryTheory
 open scoped Manifold
 
@@ -32,12 +30,11 @@ variable (M : MfldCat.{u₁, u₂, u₃, u₄} 𝕜 (n + 1))
 
 local instance : IsManifold M.I 1 M := IsManifold.of_le (n := n + 1) le_add_self
 local instance : IsManifold M.I n M := IsManifold.of_le (n := n + 1) le_self_add
-/- This implies `TangentBundle M.I M` is a manifold by `Bundle.TotalSpace.isManifold`. -/
 local instance : ContMDiffVectorBundle n M.E (TangentSpace M.I : M → Type u₃) M.I :=
   TangentBundle.contMDiffVectorBundle
+-- The above instance implies `TangentBundle M.I M` is a manifold by `Bundle.TotalSpace.isManifold`.
 
-/-- The tangent functor `MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n` sends a `C^(n+1)` manifold to its
-tangent bundle and a `C^(n+1)` map to its pushforward (tangent map). -/
+/-- Sends a `C^(n+1)` manifold to its tangent bundle and a `C^(n+1)` map to its `TangentMap`. -/
 noncomputable def tangentFunctor :
     MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n where
   obj M := of (TangentBundle M.I M) (M.E × M.E) (ModelProd M.H M.E) M.I.tangent
@@ -45,7 +42,7 @@ noncomputable def tangentFunctor :
     ofHom ⟨tangentMap M.I N.I f.hom, ContMDiff.contMDiff_tangentMap f.hom.contMDiff le_rfl⟩
   map_id _ := Hom.ext <| Subtype.ext tangentMap_id
   map_comp f g := Hom.ext <| Subtype.ext <| tangentMap_comp
-    (g.hom.contMDiff.mdifferentiable (by simp))
-    (f.hom.contMDiff.mdifferentiable (by simp))
+    (g.hom.contMDiff.mdifferentiable (by positivity))
+    (f.hom.contMDiff.mdifferentiable (by positivity))
 
 end MfldCat

From 10b255fef31a7543926cbc265981320c8ef76ec7 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 21:26:45 -0400
Subject: [PATCH 08/10] Typo

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

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
index d20cb0ec9c6091..5f88dd859512b1 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
@@ -12,7 +12,7 @@ public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 # The tangent functor on `MfldCat`
 
 We define the tangent functor `MfldCat.tangentFunctor : MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n`, sending a
-`C^(n+1)` manifold to its tangent bundle and a `C^(n+1)` map to its pushforward (tangent map).
+`C^(n+1)` manifold to its tangent bundle and a `C^(n+1)` map to its pushforward `tangentMap`.
 -/
 
 @[expose] public section
@@ -34,7 +34,7 @@ local instance : ContMDiffVectorBundle n M.E (TangentSpace M.I : M → Type u₃
   TangentBundle.contMDiffVectorBundle
 -- The above instance implies `TangentBundle M.I M` is a manifold by `Bundle.TotalSpace.isManifold`.
 
-/-- Sends a `C^(n+1)` manifold to its tangent bundle and a `C^(n+1)` map to its `TangentMap`. -/
+/-- Sends a `C^(n+1)` manifold to its tangent bundle and a `C^(n+1)` map to its `tangentMap`. -/
 noncomputable def tangentFunctor :
     MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n where
   obj M := of (TangentBundle M.I M) (M.E × M.E) (ModelProd M.H M.E) M.I.tangent

From 1f71b8c9264d91708fd5972a7c2237fe2b63eeec Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 21:33:40 -0400
Subject: [PATCH 09/10] Added John Lee reference

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

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
index 5f88dd859512b1..a2d894aa5ec504 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/TangentFunctor.lean
@@ -13,6 +13,9 @@ public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 
 We define the tangent functor `MfldCat.tangentFunctor : MfldCat 𝕜 (n + 1) ⥤ MfldCat 𝕜 n`, sending a
 `C^(n+1)` manifold to its tangent bundle and a `C^(n+1)` map to its pushforward `tangentMap`.
+
+## References
+* [J. M. Lee, *Introduction to Smooth Manifolds*][lee2012] (2nd Edition, p. 75)
 -/
 
 @[expose] public section

From a491fa46ff143f39665d472cc5460bf8724497e8 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Sun, 19 Apr 2026 21:49:09 -0400
Subject: [PATCH 10/10] Added nolint checkUnivs

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

diff --git a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
index d65101e3f0d166..de10c10dc1b37d 100644
--- a/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
+++ b/Mathlib/Geometry/Manifold/Category/MfldCat/Basic.lean
@@ -32,6 +32,7 @@ open scoped Manifold
 universe u₁ u₂ u₃ u₄
 
 /-- The category of `C^n` 𝕜-manifolds. -/
+@[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 ::