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.

We also show that isomorphisms in the category of manifolds are diffeomorphisms and that some of the introduced object properties are invariant under isomorphism. Unfortunately, all properties pertaining to the model spaces of the manifolds are not invariant under isomorphism, because the empty type is a manifold for all model spaces simultaneously. One could try to work around this in the future by defining e.g. banach M as IsEmpty M ∨ CompleteSpace M.modelVectorSpace instead of just CompleteSpace M.modelVectorSpace; that way banach would be closed under isomorphisms, but instances like CompleteSpace M.obj.modelVectorSpace for M : BanachMfld 𝕜 n could only be provided under the assumption Nonempty M.

Lastly, we give a construction of finite products in Mfld 𝕜 n.

TODOs

• Show that boundaryless is closed under isomorphisms.
• Redefine banach and finiteDimensional such that they are closed under isomorphisms too.
• Show that various object properties are closed under finite products, and conclude that the subcategories under consideration also have finite products. This requires showing that they are closed under isomorphisms first, because ObjectProperty.IsClosedUnderLimitsOfShape is defined to mean that the property contains not just some but all limits of diagrams within it.
• Make use of Mathlib.CategoryTheory.ObjectProperty.FiniteProducts here once mathlib is bumped again.

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 = (IsEmpty M.carrier ∨ 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 = (IsEmpty M.carrier ∨ 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.instCompleteSpaceModelVectorSpaceObjOfFactLeObjectPropertyBanachOfNonemptyCarrier {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {P : CategoryTheory.ObjectProperty (Mfld 𝕜 n)} [Fact (P ≤ banach)] (M : P.FullSubcategory) [Nonempty M.obj.carrier] : CompleteSpace M.obj.modelVectorSpace

instance Mfld.instFiniteDimensionalModelVectorSpaceObjOfFactLeObjectPropertyFiniteDimensionalOfNonemptyCarrier {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {P : CategoryTheory.ObjectProperty (Mfld 𝕜 n)} [Fact (P ≤ finiteDimensional)] (M : P.FullSubcategory) [Nonempty M.obj.carrier] : 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)

def Mfld.isoOfDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (d : Diffeomorph M.modelWithCorners N.modelWithCorners M.carrier N.carrier n) : M ≅ N

Equations

• Mfld.isoOfDiffeomorph d = { hom := CategoryTheory.ConcreteCategory.ofHom ↑d, inv := CategoryTheory.ConcreteCategory.ofHom ↑d.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Mfld.isoOfDiffeomorph_hom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (d : Diffeomorph M.modelWithCorners N.modelWithCorners M.carrier N.carrier n) : (isoOfDiffeomorph d).hom = CategoryTheory.ConcreteCategory.ofHom ↑d

@[simp]

theorem Mfld.isoOfDiffeomorph_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (d : Diffeomorph M.modelWithCorners N.modelWithCorners M.carrier N.carrier n) : (isoOfDiffeomorph d).inv = CategoryTheory.ConcreteCategory.ofHom ↑d.symm

def Mfld.diffeomorphOfIso {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (i : M ≅ N) : Diffeomorph M.modelWithCorners N.modelWithCorners M.carrier N.carrier n

Equations

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

@[simp]

theorem Mfld.diffeomorphOfIso_toFun {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (i : M ≅ N) (a : M.carrier) : (diffeomorphOfIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a

@[simp]

theorem Mfld.diffeomorphOfIso_invFun {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (i : M ≅ N) (a : N.carrier) : (diffeomorphOfIso i).invFun a = (CategoryTheory.ConcreteCategory.hom i.inv) a

@[simp]

theorem Mfld.isoOfDiffeomorph_diffeomorphOfIso {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (i : M ≅ N) : isoOfDiffeomorph (diffeomorphOfIso i) = i

@[simp]

theorem Mfld.diffeomorphOfIso_isoOfDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (d : Diffeomorph M.modelWithCorners N.modelWithCorners M.carrier N.carrier n) : diffeomorphOfIso (isoOfDiffeomorph d) = d

def Mfld.isoEquivDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} : (M ≅ N) ≃ Diffeomorph M.modelWithCorners N.modelWithCorners M.carrier N.carrier n

Equations

• Mfld.isoEquivDiffeomorph = { toFun := Mfld.diffeomorphOfIso, invFun := Mfld.isoOfDiffeomorph, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Mfld.isoEquivDiffeomorph_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (d : Diffeomorph M.modelWithCorners N.modelWithCorners M.carrier N.carrier n) : isoEquivDiffeomorph.symm d = isoOfDiffeomorph d

@[simp]

theorem Mfld.isoEquivDiffeomorph_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {M N : Mfld 𝕜 n} (i : M ≅ N) : isoEquivDiffeomorph i = diffeomorphOfIso i

instance Mfld.instIsClosedUnderIsomorphismsHausdorff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : hausdorff.IsClosedUnderIsomorphisms

theorem Homeomorph.sigmaCompactSpace {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [SigmaCompactSpace X] (h : X ≃ₜ Y) : SigmaCompactSpace Y

instance Mfld.instIsClosedUnderIsomorphismsSigmaCompact {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : sigmaCompact.IsClosedUnderIsomorphisms

def ContinuousLinearEquiv.toUniformEquiv {R₁ : Type u_2} {R₂ : Type u_3} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_4} {E₂ : Type u_5} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (e : E₁ ≃SL[σ₁₂] E₂) : E₁ ≃ᵤ E₂

Every continuous linear equivalence is a uniform isomorphism. TODO: move to another file.

Equations

• e.toUniformEquiv = { toFun := ⇑e, invFun := ⇑e.symm, left_inv := ⋯, right_inv := ⋯, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.toUniformEquiv_apply {R₁ : Type u_2} {R₂ : Type u_3} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_4} {E₂ : Type u_5} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (e : E₁ ≃SL[σ₁₂] E₂) (a : E₁) : e.toUniformEquiv a = e a

@[simp]

theorem ContinuousLinearEquiv.toUniformEquiv_symm_apply {R₁ : Type u_2} {R₂ : Type u_3} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_4} {E₂ : Type u_5} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (e : E₁ ≃SL[σ₁₂] E₂) (a : E₂) : e.toUniformEquiv.symm a = e.symm a

instance Mfld.instIsClosedUnderIsomorphismsBanachOfNeZeroWithTopENat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [NeZero n] : banach.IsClosedUnderIsomorphisms

instance Mfld.instIsClosedUnderIsomorphismsFiniteDimensionalOfNeZeroWithTopENat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [NeZero n] : finiteDimensional.IsClosedUnderIsomorphisms

@[reducible, inline]

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

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

Equations

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

def Mfld.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 Mfld.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} (M N : Mfld 𝕜 n) : Mfld 𝕜 n

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def Mfld.prodBinaryFan {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} (M N : Mfld 𝕜 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 Mfld.prodFst Mfld.prodSnd

def Mfld.prodBinaryFanIsLimit {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} (M N : Mfld 𝕜 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 Mfld.instHasFiniteProducts {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : CategoryTheory.Limits.HasFiniteProducts (Mfld 𝕜 n)