The category of finite-dimensional manifolds

Results on the category FinDimMfld 𝕜 n of finite-dimensional, Hausdorff, sigma-compact manifolds without boundary, for any given smoothness degree n : WithTop ℕ∞ and nontrivially normed ground field 𝕜.

This category is already defined in CatDG.ForMathlib.Mfld as a full subcategory of Mfld 𝕜 n and equipped with forgetful functors to various categories there; here we only prove more specific results.

Main definitions / results

• FinDimMfld 𝕜 n: the category of all finite-dimensional Hausdorff σ-compact Cⁿ manifolds without boundary over a fixed ground field 𝕜.
• FinDimMfld 𝕜 n has all finite products.
• FinDimMfld.mono_iff_injective: morphisms in FinDimMfld 𝕜 n are monomorphisms iff they are injective
• FinDimMfld.epi_iff_denseRange: morphisms in FinDimMfld ℝ ∞ are epimorphisms iff their range is dense

TODOs

• show that FinDimMfld 𝕜 n is essentially small
• generalise epi_iff_denseRange to smoothness degrees in ℕ∞
• can anything interesting be said about extremal monomorphisms / epimorphisms?
• define the embedding into (CommAlgCat ℝ)ᵒᵖ and show that it is fully faithful. Fullness will likely require a stronger Whitney embedding theorem than currently is in mathlib.

@[reducible, inline]

abbrev FinDimMfld.mk' {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} (M : Type u) [TopologicalSpace M] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [ChartedSpace H M] [IsManifold I n M] [FiniteDimensional 𝕜 E] [T2Space M] [SigmaCompactSpace M] [BoundarylessManifold I M] : FinDimMfld 𝕜 n

Equations

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

@[reducible, inline]

abbrev FinDimMfld.pt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : FinDimMfld 𝕜 n

A choice of terminal object in the category of manifolds, given by PUnit.

Equations

• FinDimMfld.pt = FinDimMfld.mk' PUnit.{?u.14 + 1} (modelWithCornersSelf 𝕜 PUnit.{?u.14 + 1})

def FinDimMfld.isTerminalPt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.Limits.IsTerminal pt

The choice FinDimMfld.pt of terminal object is indeed terminal.

Equations

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

@[reducible, inline]

abbrev FinDimMfld.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} (M N : FinDimMfld 𝕜 n) : FinDimMfld 𝕜 n

An explicit choice of product in the category of manifolds, given by the product of the underlying types and models with corners.

Equations

• M.prod N = FinDimMfld.mk' (M.obj.carrier × N.obj.carrier) (M.obj.modelWithCorners.prod N.obj.modelWithCorners)

def FinDimMfld.prodFst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : FinDimMfld 𝕜 n} : M.prod N ⟶ M

The first projection realising M.prod N as the product of M and N.

Equations

• FinDimMfld.prodFst = CategoryTheory.ConcreteCategory.ofHom ContMDiffMap.fst

def FinDimMfld.prodSnd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : FinDimMfld 𝕜 n} : M.prod N ⟶ N

The second projection realising M.prod N as the product of M and N.

Equations

• FinDimMfld.prodSnd = CategoryTheory.ConcreteCategory.ofHom ContMDiffMap.snd

def FinDimMfld.prodBinaryFan {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} (M N : FinDimMfld 𝕜 n) : CategoryTheory.Limits.BinaryFan N M

An explicit binary fan of M and N given by M.prod N.

Equations

• M.prodBinaryFan N = CategoryTheory.Limits.BinaryFan.mk FinDimMfld.prodFst FinDimMfld.prodSnd

def FinDimMfld.prodBinaryFanIsLimit {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} (M N : FinDimMfld 𝕜 n) : CategoryTheory.Limits.IsLimit (N.prodBinaryFan M)

The constructed binary fan is indeed a limit.

Equations

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

instance FinDimMfld.instHasFiniteProducts {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.Limits.HasFiniteProducts (FinDimMfld 𝕜 n)

theorem FinDimMfld.mono_iff_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : FinDimMfld 𝕜 n} (f : M ⟶ N) : CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem FinDimMfld.epi_iff_denseRange {M N : FinDimMfld ℝ ↑⊤} (f : M ⟶ N) : CategoryTheory.Epi f ↔ DenseRange ⇑(CategoryTheory.ConcreteCategory.hom f)