The category Mfld of manifolds

In this file we define a general category Mfld 𝕜 n of all manifolds of a given smoothness degree n : WithTop ℕ∞ over a nontrivially normed ground field 𝕜, imposing no conditions like Hausdorffness, paracompactness, finite-dimensionality or boundarylessness. We instead set up these properties as object properties, and define other categories of manifolds as full subcategories in terms of them.

Currently this is all written with a focus on avoiding boilderplate code: we define each subcategory as P.FullSubcategory for some object property P, and provide instances such as {P : ObjectProperty (Mfld 𝕜 n)} [Fact (P ≤ hausdorff)] (M : P.FullSubcategory) : T2Space M to avoid having to set up T2Space-instances for each considere subcategory separately. The downsides of this approach are that dot notation doesn't carry over to full subcategories, and that we have to define some instances like [Fact (a ≤ c)] : Fact (a ⊓ b ≤ c).

Main definitions / results

• Mfld 𝕜 n: the category of all Cⁿ manifolds with corners over a fixed ground field 𝕜.
• FinDimMfld 𝕜 n: the category of Hausdorff, paracompact finite-dimensional manifolds without boundary, defined as a full subcategory of Mfld 𝕜 n.
• FinDimMfldWCorners 𝕜 n: the category of Hausdorff, paracompact finite-dimensional manifolds with corners, defined as a full subcategory of Mfld 𝕜 n.
• BanachMfld 𝕜 n: the category of Hausdorff, paracompact Banach manifolds without boundary, defined as a full subcategory of Mfld 𝕜 n.
• All of these subcategories are concrete.

For each of these subcategories a forgetful functor to TopCat, an inclusion into Mfld 𝕜 n and inclusions into other subcategories are provided in the form of HasForget₂-instances.

TODOs

• Show that Mfld 𝕜 n has all products.
• Show that various object properties are closed under arbitrary / finite products, and conclude that the subcategories under consideration also have arbitrary / finite products.

structure Mfld (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) : Type (max (u + 1) u_1)

The category of all (possbily non-Hausdorff, non-paracompact and infinite-dimensional) manifolds with corners for a fixed ground field 𝕜 and smoothness degree n : WithTop ℕ∞. The main purpose of this category is to act as an ambient category for nicer categories of manifolds to be considered as full subcategories of.

• carrier : Type u
• topology : TopologicalSpace self.carrier
• modelVectorSpace : Type u
• normedAddCommGroup : NormedAddCommGroup self.modelVectorSpace
• normedSpace : NormedSpace 𝕜 self.modelVectorSpace
• model : Type u
• modelTopology : TopologicalSpace self.model
• modelWithCorners : ModelWithCorners 𝕜 self.modelVectorSpace self.model
• chartedSpace : ChartedSpace self.model self.carrier
• isManifold : IsManifold self.modelWithCorners n self.carrier

instance Mfld.instCoeSortType {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CoeSort (Mfld 𝕜 n) (Type u)

Equations

• Mfld.instCoeSortType = { coe := Mfld.carrier }

instance Mfld.instCategory (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) : CategoryTheory.Category.{u_3, max u_2 (u_3 + 1)} (Mfld 𝕜 n)

Equations

• One or more equations did not get rendered due to their size.

instance Mfld.instConcreteCategoryContMDiffMapModelVectorSpaceModelModelWithCornersCarrier {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.ConcreteCategory (Mfld 𝕜 n) fun (M N : Mfld 𝕜 n) => ContMDiffMap M.modelWithCorners N.modelWithCorners M.carrier N.carrier n

Equations

• One or more equations did not get rendered due to their size.

instance Mfld.instHasForget₂TopCat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.HasForget₂ (Mfld 𝕜 n) TopCat

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Mfld.forget₂_map {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {X✝ Y✝ : Mfld 𝕜 n} (f : ContMDiffMap X✝.modelWithCorners Y✝.modelWithCorners X✝.carrier Y✝.carrier n) : CategoryTheory.HasForget₂.forget₂.map f = TopCat.ofHom ↑f

@[simp]

theorem Mfld.forget₂_obj_carrier {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} (M : Mfld 𝕜 n) : ↑(CategoryTheory.HasForget₂.forget₂.obj M) = M.carrier

def Mfld.hausdorff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.ObjectProperty (Mfld 𝕜 n)

The object property satisfied by all manifolds whose underlying topological space is T2.

Equations

• M.hausdorff = T2Space M.carrier

def Mfld.sigmaCompact {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.ObjectProperty (Mfld 𝕜 n)

The object property satisfied by all σ-compact manifolds.

Equations

• M.sigmaCompact = SigmaCompactSpace M.carrier

def Mfld.boundaryless {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.ObjectProperty (Mfld 𝕜 n)

The object property satisfied by all manifolds that are boundaryless in the sense of BoundarylessManifold. Note that such manifolds can still be modelled on non-boundaryless models with corners, they just need to consist entirely of interior points.

Equations

• M.boundaryless = BoundarylessManifold M.modelWithCorners M.carrier

def Mfld.banach {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.ObjectProperty (Mfld 𝕜 n)

The object property satisfied by all manifolds whose model vector space is complete.

Equations

• M.banach = CompleteSpace M.modelVectorSpace

def Mfld.finiteDimensional {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.ObjectProperty (Mfld 𝕜 n)

The object property satisfied by all manifolds whose model vector space is finite-dimensional.

Equations

• M.finiteDimensional = FiniteDimensional 𝕜 M.modelVectorSpace

theorem Mfld.finiteDimensional_le_banach {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [CompleteSpace 𝕜] : finiteDimensional ≤ banach

@[reducible, inline]

abbrev Mfld.finDimMfld {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.ObjectProperty (Mfld 𝕜 n)

The object property corresponding to Hausdorff, sigma-compact and finite-dimensional manifolds without boundary.

Equations

• Mfld.finDimMfld = Mfld.hausdorff ⊓ Mfld.sigmaCompact ⊓ Mfld.boundaryless ⊓ Mfld.finiteDimensional

@[reducible, inline]

abbrev Mfld.finDimMfldWCorners {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.ObjectProperty (Mfld 𝕜 n)

The object property corresponding to Hausdorff, sigma-compact and finite-dimensional manifolds with corners.

Equations

• Mfld.finDimMfldWCorners = Mfld.hausdorff ⊓ Mfld.sigmaCompact ⊓ Mfld.finiteDimensional

@[reducible, inline]

abbrev Mfld.banachMfld {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.ObjectProperty (Mfld 𝕜 n)

The object property corresponding to Hausdorff sigma-compact Banach manifolds without boundary.

Equations

• Mfld.banachMfld = Mfld.hausdorff ⊓ Mfld.sigmaCompact ⊓ Mfld.boundaryless ⊓ Mfld.banach

theorem Mfld.finDimMfld_le_finDimMfldWCorners {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : finDimMfld ≤ finDimMfldWCorners

theorem Mfld.finDimMfld_le_banachMfld {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [CompleteSpace 𝕜] : finDimMfld ≤ banachMfld

@[reducible, inline]

abbrev FinDimMfld (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) : Type (max (u + 1) u_2)

The category of (Hausdorff, paracompact) finite-dimensional manifolds without boundary, defined as a full subcategory of Mfld 𝕜 n.

Equations

• FinDimMfld 𝕜 n = Mfld.finDimMfld.FullSubcategory

@[reducible, inline]

abbrev FinDimMfldWCorners (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) : Type (max (u + 1) u_2)

The category of (Hausdorff, paracompact) finite-dimensional manifolds with corners, defined as a full subcategory of Mfld 𝕜 n.

Equations

• FinDimMfldWCorners 𝕜 n = Mfld.finDimMfldWCorners.FullSubcategory

@[reducible, inline]

abbrev BanachMfld (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞) : Type (max (u + 1) u_2)

The category of (Hausdorff, paracompact) Banach manifolds without boundary, defined as a full subcategory of Mfld 𝕜 n.

Equations

• BanachMfld 𝕜 n = Mfld.banachMfld.FullSubcategory

instance Mfld.instCoeSortFullSubcategoryType {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CoeSort C (Type u)] (P : CategoryTheory.ObjectProperty C) : CoeSort P.FullSubcategory (Type u)

Equations

• Mfld.instCoeSortFullSubcategoryType P = { coe := fun (X : P.FullSubcategory) => CoeSort.coe X.obj }

instance Mfld.instFactLe {α : Type u} [SemilatticeInf α] {a : α} : Fact (a ≤ a)

instance Mfld.instFactLeMin {α : Type u} [SemilatticeInf α] {a b c : α} [Fact (a ≤ c)] : Fact (a ⊓ b ≤ c)

instance Mfld.instFactLeMin_1 {α : Type u} [SemilatticeInf α] {a b c : α} [Fact (b ≤ c)] : Fact (a ⊓ b ≤ c)

instance Mfld.instT2SpaceCarrierObjOfFactLeObjectPropertyHausdorff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {P : CategoryTheory.ObjectProperty (Mfld 𝕜 n)} [Fact (P ≤ hausdorff)] (M : P.FullSubcategory) : T2Space M.obj.carrier

instance Mfld.instSigmaCompactSpaceCarrierObjOfFactLeObjectPropertySigmaCompact {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {P : CategoryTheory.ObjectProperty (Mfld 𝕜 n)} [Fact (P ≤ sigmaCompact)] (M : P.FullSubcategory) : SigmaCompactSpace M.obj.carrier

instance Mfld.instBoundarylessManifoldModelVectorSpaceObjModelModelWithCornersCarrierOfFactLeObjectPropertyBoundaryless {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {P : CategoryTheory.ObjectProperty (Mfld 𝕜 n)} [Fact (P ≤ boundaryless)] (M : P.FullSubcategory) : BoundarylessManifold M.obj.modelWithCorners M.obj.carrier

instance Mfld.instCompleteSpaceModelVectorSpaceObjOfFactLeObjectPropertyBanach {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {P : CategoryTheory.ObjectProperty (Mfld 𝕜 n)} [Fact (P ≤ banach)] (M : P.FullSubcategory) : CompleteSpace M.obj.modelVectorSpace

instance Mfld.instFiniteDimensionalModelVectorSpaceObjOfFactLeObjectPropertyFiniteDimensional {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {P : CategoryTheory.ObjectProperty (Mfld 𝕜 n)} [Fact (P ≤ finiteDimensional)] (M : P.FullSubcategory) : FiniteDimensional 𝕜 M.obj.modelVectorSpace

instance Mfld.instHasForget₂FullSubcategory {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.HasForget C] [CategoryTheory.HasForget D] [CategoryTheory.HasForget₂ C D] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.HasForget₂ P.FullSubcategory D

Equations

• Mfld.instHasForget₂FullSubcategory P = { forget₂ := (CategoryTheory.forget₂ P.FullSubcategory C).comp (CategoryTheory.forget₂ C D), forget_comp := ⋯ }

@[simp]

theorem Mfld.forget₂_def {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_5, u_3} D] [CategoryTheory.HasForget C] [CategoryTheory.HasForget D] [CategoryTheory.HasForget₂ C D] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.HasForget₂.forget₂ = (CategoryTheory.forget₂ P.FullSubcategory C).comp (CategoryTheory.forget₂ C D)

instance Mfld.instHasForget₂FullSubcategoryOfFactLeObjectProperty {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.HasForget C] (P Q : CategoryTheory.ObjectProperty C) [Fact (P ≤ Q)] : CategoryTheory.HasForget₂ P.FullSubcategory Q.FullSubcategory

Equations

• Mfld.instHasForget₂FullSubcategoryOfFactLeObjectProperty P Q = { forget₂ := CategoryTheory.ObjectProperty.ιOfLE ⋯, forget_comp := ⋯ }

instance Mfld.instFactLeObjectPropertyFinDimMfldFinDimMfldWCorners {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : Fact (finDimMfld ≤ finDimMfldWCorners)

instance Mfld.instFactLeObjectPropertyFinDimMfldBanachMfldOfCompleteSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [CompleteSpace 𝕜] : Fact (finDimMfld ≤ banachMfld)