The category FinDimMfld ℝ n as a site

In this file we equip the category FinDimMfld ℝ ∞ of finite-dimensional, Hausdorff, paracompact smooth real manifolds without boundary with the Grothendieck topology consisting of all sieves that contain a family of jointly surjective open smooth embeddings, also called the "open cover topology" because it equivalently consists of all sieves that contain the family of inclusions corresponding to an open cover. We also show that this topology is subcanonical.

Currently we only do this over ℝ and for smoothness degree ∞ because smooth embeddings are not defined in mathlib yet; we use diffeological inductions instead, which are equivalent to smooth embeddings but only available in the case of ℝ and ∞. Once smooth embeddings are defined, it should hopefully be easy to rephrase this in terms of smooth embeddings and generalise it.

Main definitions / results:

• FinDimMfld.openCoverCoverage: the open cover coverage on FinDimMfld ℝ ∞, consisting of all jointly surjective families of open inductions
• FinDimMfld.openCoverTopology: the open cover topology on FinDimMfld ℝ ∞, consisting of all sieves containing a jointly surjective family of open inductions
• FinDimMfld ℝ ∞ with the open cover topology is a concrete site
• the open cover topology on FinDimMfld ℝ ∞ is subcanonical
• EuclOp.toFinDimMfld: the inclusion functor EuclOp ⥤ FinDimMfld ℝ ∞ from open subsets of euclidean spaces to manifolds
• EuclOp.toFinDimMfld exhibits EuclOp as a dense sub-site of FinDimMfld ℝ ∞.

TODO

• Show that Functor.IsDenseSubsite is closed under compositions, so that CartSp is a dense sub-site of FinDimMfld ℝ ∞ too

theorem IsManifold.toDiffeology_eq_subtype {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (u : TopologicalSpace.Opens M) : toDiffeology I ↥u = instDiffeologicalSpaceSubtype

On any open subset u of a manifold M, the diffeology derived from the manifold structure on u and the subspace diffeology coming from the diffeology on M agree. TODO: move somewhere else.

def FinDimMfld.openCoverCoverage : CategoryTheory.Coverage (FinDimMfld ℝ ↑⊤)

The open cover coverage on FinDimMfld ℝ ∞, consisting of all coverings by open smooth embeddings. Since mathlib apparently doesn't have smooth embeddings yet, diffeological inductions are used instead.

Equations

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

def FinDimMfld.openCoverTopology : CategoryTheory.GrothendieckTopology (FinDimMfld ℝ ↑⊤)

The open cover grothendieck topology on FinDimMfld ℝ ∞.

Equations

• FinDimMfld.openCoverTopology = FinDimMfld.openCoverCoverage.toGrothendieck

theorem FinDimMfld.openCoverTopology.mem_sieves_iff {M : FinDimMfld ℝ ↑⊤} {s : CategoryTheory.Sieve M} : s ∈ openCoverTopology M ↔ ∃ r ≤ s.arrows, r ∈ openCoverCoverage.coverings M

A sieve belongs to FinDimMfld.openCoverTopology iff it contains a presieve from FinDimMfld.openCoverCoverage.

theorem FinDimMfld.openCoverTopology.mem_sieves_iff' {M : FinDimMfld ℝ ↑⊤} {s : CategoryTheory.Sieve M} : s ∈ openCoverTopology M ↔ ⋃ (N : FinDimMfld ℝ ↑⊤), ⋃ (f : N ⟶ M), ⋃ (_ : s.arrows f ∧ IsOpenInduction ⇑(CategoryTheory.ConcreteCategory.hom f)), Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) = Set.univ

noncomputable instance FinDimMfld.instIsConcreteSiteRealSomeENatTopOpenCoverTopology : openCoverTopology.IsConcreteSite

FinDimMfld ℝ ∞ is a concrete site, in that it is concrete with elements corresponding to morphisms from the terminal object and carries a topology consisting entirely of jointly surjective sieves.

Equations

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

instance FinDimMfld.instSubcanonicalRealSomeENatTopOpenCoverTopology : openCoverTopology.Subcanonical

FinDimMfld ℝ ∞ is a subcanonical site, i.e. all representable presheaves on it are sheaves.

noncomputable def EuclOp.toFinDimMfld : CategoryTheory.Functor EuclOp (FinDimMfld ℝ ↑⊤)

The embedding of EuclOp into FinDimMfld ℝ ∞.

Equations

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

@[simp]

theorem EuclOp.toFinDimMfld_obj_obj_modelWithCorners (u : EuclOp) : (toFinDimMfld.obj u).obj.modelWithCorners = modelWithCornersSelf ℝ (Eucl u.fst)

@[simp]

theorem EuclOp.toFinDimMfld_obj_obj_modelTopology (u : EuclOp) : (toFinDimMfld.obj u).obj.modelTopology = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

@[simp]

theorem EuclOp.toFinDimMfld_obj_obj_carrier (u : EuclOp) : (toFinDimMfld.obj u).obj.carrier = ↥u.snd

@[simp]

theorem EuclOp.toFinDimMfld_obj_obj_normedSpace (u : EuclOp) : (toFinDimMfld.obj u).obj.normedSpace = PiLp.normedSpace 2 ℝ fun (x : Fin u.fst) => ℝ

@[simp]

theorem EuclOp.toFinDimMfld_obj_obj_model (u : EuclOp) : (toFinDimMfld.obj u).obj.model = Eucl u.fst

@[simp]

theorem EuclOp.toFinDimMfld_obj_obj_topology (u : EuclOp) : (toFinDimMfld.obj u).obj.topology = instTopologicalSpaceSubtype

@[simp]

theorem EuclOp.toFinDimMfld_obj_obj_normedAddCommGroup (u : EuclOp) : (toFinDimMfld.obj u).obj.normedAddCommGroup = PiLp.normedAddCommGroup 2 fun (x : Fin u.fst) => ℝ

@[simp]

theorem EuclOp.toFinDimMfld_obj_obj_modelVectorSpace (u : EuclOp) : (toFinDimMfld.obj u).obj.modelVectorSpace = Eucl u.fst

@[simp]

theorem EuclOp.toFinDimMfld_obj_obj_chartedSpace (u : EuclOp) : (toFinDimMfld.obj u).obj.chartedSpace = u.snd.instChartedSpace

@[simp]

theorem EuclOp.toFinDimMfld_map_coe {X✝ Y✝ : EuclOp} (f : X✝ ⟶ Y✝) (a : ↥X✝.snd) : ↑(toFinDimMfld.map f) a = f a

def extChartAtDDiffeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (x : M) : ↑(extChartAt I x).source ᵈ≃ ↑(extChartAt I x).target

extChartAt I x as a diffeological diffeomorphism.

Equations

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

@[simp]

theorem extChartAtDDiffeomorph_toFun {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (x : M) (a✝ : ↑(extChartAt I x).source) : (extChartAtDDiffeomorph I x) a✝ = Set.MapsTo.restrict (↑(extChartAt I x)) (extChartAt I x).source (extChartAt I x).target ⋯ a✝

@[simp]

theorem extChartAtDDiffeomorph_invFun {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (x : M) (a✝ : ↑(extChartAt I x).target) : (extChartAtDDiffeomorph I x).invFun a✝ = Set.MapsTo.restrict (↑(extChartAt I x).symm) (extChartAt I x).target (extChartAt I x).source ⋯ a✝

instance instIsCoverDenseEuclOpFinDimMfldRealSomeENatTopToFinDimMfldOpenCoverTopology : EuclOp.toFinDimMfld.IsCoverDense FinDimMfld.openCoverTopology

Manifolds can be covered with open subsets of cartesian spaces.

instance instFullEuclOpFinDimMfldRealSomeENatTopToFinDimMfld : EuclOp.toFinDimMfld.Full

instance instFaithfulEuclOpFinDimMfldRealSomeENatTopToFinDimMfld : EuclOp.toFinDimMfld.Faithful

instance instIsDenseSubsiteEuclOpFinDimMfldRealSomeENatTopOpenCoverTopologyOpenCoverTopologyToFinDimMfld : CategoryTheory.Functor.IsDenseSubsite EuclOp.openCoverTopology FinDimMfld.openCoverTopology EuclOp.toFinDimMfld

EuclOp.toFinDimMfld exhibits EuclOp as a dense sub-site of FinDimMfld ℝ ∞ with respect to the open cover topologies. In particular, the sheaf topoi of the two sites are equivalent via IsDenseSubsite.sheafEquiv.