The category of `C^n` manifolds modeled on `I` #

This file defines the bundled category ModelWithCorners.MfldCat.{u} I n of C^n manifolds modeled on a fixed I : ModelWithCorners 𝕜 E H, along with the forgetful functor to TopCat.

Future work #

Show that ModelWithCorners.MfldCat I n has coproducts given by disjoint unions.

source

structure ModelWithCorners.MfldCat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) :

Type (max (u + 1) u_3)

The category of C^n manifolds modeled on a fixed model with corners I.

carrier : Type u
The underlying type.
topologicalSpace : TopologicalSpace ↑self
chartedSpace : ChartedSpace H ↑self
isManifold : IsManifold I n ↑self

Instances For

source

@[instance_reducible]

instance ModelWithCorners.MfldCat.instCoeSortType {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} :

CoeSort (I.MfldCat n) (Type u)

Equations

ModelWithCorners.MfldCat.instCoeSortType = { coe := ModelWithCorners.MfldCat.carrier }

source

@[reducible, inline]

abbrev ModelWithCorners.MfldCat.of {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} (X : Type u) [TopologicalSpace X] [ChartedSpace H X] [IsManifold I n X] :

I.MfldCat n

The object of ModelWithCorners.MfldCat I n associated to a C^n manifold X modeled on I.

This is the preferred way to construct a term of ModelWithCorners.MfldCat I n.

Equations

ModelWithCorners.MfldCat.of X = { carrier := X, topologicalSpace := inst✝², chartedSpace := inst✝¹, isManifold := inst✝ }

Instances For

source

theorem ModelWithCorners.MfldCat.coe_of {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {n : WithTop ℕ∞} (X : Type u) [TopologicalSpace X] [ChartedSpace H X] [IsManifold I n X] :

↑(of X) = X

source

structure ModelWithCorners.MfldCat.Hom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} (M N : I.MfldCat n) :

Type u

The type of morphisms in ModelWithCorners.MfldCat I n.

hom' : ContMDiffMap I I (↑M) (↑N) n
The underlying C^n map.

Instances For

source

theorem ModelWithCorners.MfldCat.Hom.ext {𝕜 : Type u_1} {inst✝ : NontriviallyNormedField 𝕜} {E : Type u_2} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace 𝕜 E} {H : Type u_3} {inst✝³ : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} {x y : M.Hom N} (hom' : x.hom' = y.hom') :

x = y

source

theorem ModelWithCorners.MfldCat.Hom.ext_iff {𝕜 : Type u_1} {inst✝ : NontriviallyNormedField 𝕜} {E : Type u_2} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace 𝕜 E} {H : Type u_3} {inst✝³ : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} {x y : M.Hom N} :

x = y ↔ x.hom' = y.hom'

source

@[instance_reducible]

instance ModelWithCorners.MfldCat.instCategory {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} :

CategoryTheory.Category.{u_4, max u_3 (u_4 + 1)} (I.MfldCat n)

Equations

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

source

@[instance_reducible]

instance ModelWithCorners.MfldCat.instConcreteCategoryContMDiffMapCarrier {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} :

CategoryTheory.ConcreteCategory (I.MfldCat n) fun (M N : I.MfldCat n) => ContMDiffMap I I (↑M) (↑N) n

Equations

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

source

@[reducible, inline]

abbrev ModelWithCorners.MfldCat.Hom.hom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (f : M.Hom N) :

ContMDiffMap I I (↑M) (↑N) n

Turn a morphism in ModelWithCorners.MfldCat back into a ContMDiffMap.

Equations

f.hom = CategoryTheory.ConcreteCategory.hom f

Instances For

source

@[reducible, inline]

abbrev ModelWithCorners.MfldCat.ofHom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X Y : Type u} [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) :

of X ⟶ of Y

Typecheck a ContMDiffMap as a morphism in ModelWithCorners.MfldCat.

Equations

ModelWithCorners.MfldCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

source

def ModelWithCorners.MfldCat.Hom.Simps.hom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} (M N : I.MfldCat n) (f : M.Hom N) :

ContMDiffMap I I (↑M) (↑N) n

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

ModelWithCorners.MfldCat.Hom.Simps.hom M N f = f.hom

Instances For

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

source

@[simp]

theorem ModelWithCorners.MfldCat.hom_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : I.MfldCat n} :

Hom.hom (CategoryTheory.CategoryStruct.id M) = ContMDiffMap.id

source

@[simp]

theorem ModelWithCorners.MfldCat.hom_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N P : I.MfldCat n} (f : M ⟶ N) (g : N ⟶ P) :

Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

source

theorem ModelWithCorners.MfldCat.id_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} (M : I.MfldCat n) (m : ↑M) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) m = m

source

theorem ModelWithCorners.MfldCat.comp_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N P : I.MfldCat n} (f : M ⟶ N) (g : N ⟶ P) (m : ↑M) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) m = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) m)

source

theorem ModelWithCorners.MfldCat.hom_ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} {f g : M ⟶ N} (hf : Hom.hom f = Hom.hom g) :

f = g

source

theorem ModelWithCorners.MfldCat.hom_ext_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} {f g : M ⟶ N} :

f = g ↔ Hom.hom f = Hom.hom g

source

@[simp]

theorem ModelWithCorners.MfldCat.hom_ofHom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X Y : Type u} [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) :

Hom.hom (ofHom f) = f

source

@[simp]

theorem ModelWithCorners.MfldCat.ofHom_hom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (f : M ⟶ N) :

ofHom (Hom.hom f) = f

source

@[simp]

theorem ModelWithCorners.MfldCat.ofHom_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X : Type u} [TopologicalSpace X] [ChartedSpace H X] [IsManifold I n X] :

ofHom ContMDiffMap.id = CategoryTheory.CategoryStruct.id (of X)

source

@[simp]

theorem ModelWithCorners.MfldCat.ofHom_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {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] (f : ContMDiffMap I I X Y n) (g : ContMDiffMap I I Y Z n) :

ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

source

theorem ModelWithCorners.MfldCat.ofHom_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {X Y : Type u} [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 : X) :

(CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

source

theorem ModelWithCorners.MfldCat.inv_hom_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (e : M ≅ N) (x : ↑M) :

(CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

source

theorem ModelWithCorners.MfldCat.hom_inv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (e : M ≅ N) (x : ↑N) :

(CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x

source

@[instance_reducible]

instance ModelWithCorners.MfldCat.inhabited {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} :

Inhabited (I.MfldCat n)

Equations

ModelWithCorners.MfldCat.inhabited = { default := ModelWithCorners.MfldCat.of H }

source

@[instance_reducible]

instance ModelWithCorners.MfldCat.hasForgetToTopCat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} :

CategoryTheory.HasForget₂ (I.MfldCat n) TopCat

Equations

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

source

@[simp]

theorem ModelWithCorners.MfldCat.forget₂_topCat_obj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} (M : I.MfldCat n) :

(CategoryTheory.forget₂ (I.MfldCat n) TopCat).obj M = TopCat.of ↑M

source

@[simp]

theorem ModelWithCorners.MfldCat.forget₂_topCat_map {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (f : M ⟶ N) :

(CategoryTheory.forget₂ (I.MfldCat n) TopCat).map f = TopCat.ofHom { toFun := ⇑(Hom.hom f), continuous_toFun := ⋯ }

source

def ModelWithCorners.MfldCat.isoOfDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (e : Diffeomorph I I (↑M) (↑N) n) :

M ≅ N

Build an isomorphism in ModelWithCorners.MfldCat I n from a diffeomorphism.

Equations

ModelWithCorners.MfldCat.isoOfDiffeomorph e = { hom := ModelWithCorners.MfldCat.ofHom ↑e, inv := ModelWithCorners.MfldCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

@[simp]

theorem ModelWithCorners.MfldCat.isoOfDiffeomorph_hom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (e : Diffeomorph I I (↑M) (↑N) n) :

(isoOfDiffeomorph e).hom = ofHom ↑e

source

@[simp]

theorem ModelWithCorners.MfldCat.isoOfDiffeomorph_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (e : Diffeomorph I I (↑M) (↑N) n) :

(isoOfDiffeomorph e).inv = ofHom ↑e.symm

source

def ModelWithCorners.MfldCat.diffeomorphOfIso {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (i : M ≅ N) :

Diffeomorph I I (↑M) (↑N) n

Build a diffeomorphism from an isomorphism in ModelWithCorners.MfldCat I n.

Equations

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

Instances For

source

@[simp]

theorem ModelWithCorners.MfldCat.diffeomorphOfIso_invFun {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (i : M ≅ N) (a : ↑N) :

(diffeomorphOfIso i).invFun a = (CategoryTheory.ConcreteCategory.hom i.inv) a

source

@[simp]

theorem ModelWithCorners.MfldCat.diffeomorphOfIso_toFun {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (i : M ≅ N) (a : ↑M) :

(diffeomorphOfIso i) a = (CategoryTheory.ConcreteCategory.hom i.hom) a

source

def ModelWithCorners.MfldCat.isoEquivDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} :

(M ≅ N) ≃ Diffeomorph I I (↑M) (↑N) n

Diffeomorphisms between manifolds modeled on I are the same as isomorphisms in ModelWithCorners.MfldCat I n.

Equations

ModelWithCorners.MfldCat.isoEquivDiffeomorph = { toFun := ModelWithCorners.MfldCat.diffeomorphOfIso, invFun := ModelWithCorners.MfldCat.isoOfDiffeomorph, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem ModelWithCorners.MfldCat.isoEquivDiffeomorph_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (i : M ≅ N) :

isoEquivDiffeomorph i = diffeomorphOfIso i

source

@[simp]

theorem ModelWithCorners.MfldCat.isoEquivDiffeomorph_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M N : I.MfldCat n} (e : Diffeomorph I I (↑M) (↑N) n) :

isoEquivDiffeomorph.symm e = isoOfDiffeomorph e

Documentation

Mathlib.Geometry.Manifold.Category.MfldCat.OfModel

The category of `C^n` manifolds modeled on `I` #

Future work #

The category of C^n manifolds modeled on I #

Future work #

The category of `C^n` manifolds modeled on `I` #