CartSp and EuclOp

This file defines the sites CartSp and EuclOp of cartesian spaces resp. open subsets of cartesian spaces and smooth maps, both with the good open cover coverage. These sites are of relevance because concrete sheaves on them correspond to diffeological spaces, although sheaves on them are studied not in this file but in Orbifolds.Diffeology.SmoothSp.

See https://ncatlab.org/nlab/show/CartSp.

Note that with the current implementation, this could not be used to define diffeological spaces - it already uses diffeology in the definition of CartSp.openCoverCoverage. The reason is that smooth embeddings are apparently not yet implemented in mathlib, so diffeological inductions are used instead.

Main definitions / results:

• CartSp: the category of euclidean spaces and smooth maps between them
• CartSp.openCoverCoverage: the coverage given by jointly surjective open inductions
• CartSp has all finite products
• CartSp is a concrete, cohesive and subcanonical site
• EuclOp: the category of open subsets of euclidean spaces and smooth maps between them
• EuclOp.openCoverCoverage: the coverage given by jointly surjective open inductions
• EuclOp is a concrete subcanonical site
• CartSp.toEuclOp: the fully faithful embedding of CartSp into EuclOp
• CartSp.toEuclOp exhibits CartSp as a dense sub-site of EuclOp

TODO

• Show that EuclOp has all finite products
• Show that that CartSp.toEuclOp preserves finite products
• Switch from HasForget to the new ConcreteCategory design
• Use Presieve.IsJointlySurjective more (currently runs into problems regarding which FunLike instances are used)
• Generalise CartSp to take a smoothness parameter in ℕ∞
• Generalise EuclOp to take a smoothness parameter in WithTop ℕ∞
• General results about concrete sites

def CartSp : Type

Equations

• CartSp = ℕ

instance CartSp.instCoeSortType : CoeSort CartSp Type

Equations

• CartSp.instCoeSortType = { coe := fun (n : CartSp) => EuclideanSpace ℝ (Fin n) }

instance CartSp.instOfNat (n : ℕ) : OfNat CartSp n

Equations

• CartSp.instOfNat n = { ofNat := n }

instance CartSp.instSmallCategory : CategoryTheory.SmallCategory CartSp

Equations

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

instance CartSp.instHasForget : CategoryTheory.HasForget CartSp

Equations

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

instance CartSp.instFunLike (n m : CartSp) : FunLike (n ⟶ m) (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin m))

Equations

• n.instFunLike m = { coe := fun (f : n ⟶ m) => ⇑f, coe_injective' := ⋯ }

@[simp]

theorem CartSp.id_app (n : CartSp) (x : EuclideanSpace ℝ (Fin n)) : (CategoryTheory.CategoryStruct.id n) x = x

@[simp]

theorem CartSp.comp_app {n m k : CartSp} (f : n ⟶ m) (g : m ⟶ k) (x : EuclideanSpace ℝ (Fin n)) : (CategoryTheory.CategoryStruct.comp f g) x = g (f x)

def CartSp.openCoverCoverage : CategoryTheory.Coverage CartSp

The open cover coverage on CartSp, 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 CartSp.openCoverTopology : CategoryTheory.GrothendieckTopology CartSp

The open cover grothendieck topology on CartSp.

Equations

• CartSp.openCoverTopology = CategoryTheory.Coverage.toGrothendieck CartSp CartSp.openCoverCoverage

theorem CartSp.openCoverTopology.mem_sieves_iff {n : CartSp} {s : CategoryTheory.Sieve n} : s ∈ openCoverTopology n ↔ ∃ r ≤ s.arrows, r ∈ openCoverCoverage.covering n

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

theorem CartSp.openCoverTopology.mem_sieves_iff' {n : CartSp} {s : CategoryTheory.Sieve n} : s ∈ openCoverTopology n ↔ ⋃ (m : CartSp), ⋃ (f : m ⟶ n), ⋃ (_ : s.arrows f ∧ IsOpenInduction ⇑f), Set.range ⇑f = Set.univ

def CartSp.isTerminal0 : CategoryTheory.Limits.IsTerminal 0

The 0-dimensional cartesian space is terminal in CartSp.

Equations

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

def EuclideanSpace.sumEquivProd {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] : EuclideanSpace 𝕜 (ι ⊕ κ) ≃L[𝕜] EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ

The canonical linear homeomorphism between EuclideanSpace 𝕜 (ι ⊕ κ) and EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ. Note that this is not an isometry because product spaces are equipped with the supremum norm. TODO: remove next time mathlib is bumped

Equations

• EuclideanSpace.sumEquivProd = (PiLp.sumPiLpEquivProdLpPiLp 2 fun (x : ι ⊕ κ) => 𝕜).toContinuousLinearEquiv.trans (WithLp.prodContinuousLinearEquiv 2 𝕜 (WithLp 2 (ι → 𝕜)) (WithLp 2 (κ → 𝕜)))

def EuclideanSpace.finAddEquivProd {𝕜 : Type u_1} [RCLike 𝕜] {n m : ℕ} : EuclideanSpace 𝕜 (Fin (n + m)) ≃L[𝕜] EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m)

The canonical linear homeomorphism between EuclideanSpace 𝕜 (Fin (n + m)) and EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m). TODO: remove next time mathlib is bumped

Equations

• EuclideanSpace.finAddEquivProd = (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 finSumFinEquiv.symm).toContinuousLinearEquiv.trans EuclideanSpace.sumEquivProd

@[reducible, inline]

noncomputable abbrev CartSp.prodFst {n m : CartSp} : n + m ⟶ n

The first projection realising EuclideanSpace ℝ (Fin (n + m)) as the product of EuclideanSpace ℝ n and EuclideanSpace ℝ m.

Equations

• CartSp.prodFst = DSmoothMap.fst.comp EuclideanSpace.finAddEquivProd.toDDiffeomorph.toDSmoothMap

@[reducible, inline]

noncomputable abbrev CartSp.prodSnd {n m : CartSp} : n + m ⟶ m

The second projection realising EuclideanSpace ℝ (Fin (n + m)) as the product of EuclideanSpace ℝ n and EuclideanSpace ℝ m.

Equations

• CartSp.prodSnd = DSmoothMap.snd.comp EuclideanSpace.finAddEquivProd.toDDiffeomorph.toDSmoothMap

noncomputable def CartSp.prodBinaryFan (n m : CartSp) : CategoryTheory.Limits.BinaryFan n m

The explicit binary fan of EuclideanSpace ℝ n and EuclideanSpace ℝ m given by EuclideanSpace ℝ (Fin (n + m)).

Equations

• n.prodBinaryFan m = CategoryTheory.Limits.BinaryFan.mk CartSp.prodFst CartSp.prodSnd

noncomputable def CartSp.prodBinaryFanIsLimit (n m : CartSp) : 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 CartSp.instHasFiniteProducts : CategoryTheory.Limits.HasFiniteProducts CartSp

noncomputable instance CartSp.instUniqueEuclideanSpaceRealFinTerminal : Unique (EuclideanSpace ℝ (Fin (⊤_ CartSp)))

Equations

• CartSp.instUniqueEuclideanSpaceRealFinTerminal = ((CategoryTheory.forget CartSp).mapIso (CategoryTheory.Limits.terminalIsTerminal.uniqueUpToIso CartSp.isTerminal0)).toEquiv.unique

instance CartSp.instIsLocallyConnectedSiteOpenCoverTopology : openCoverTopology.IsLocallyConnectedSite

CartSp is a locally connected site, roughly meaning that each of its objects is connected. Note that this is different from EuclOp, which also contains disconnected open sets and thus isn't locally connected.

instance CartSp.instIsCohesiveSiteOpenCoverTopology : openCoverTopology.IsCohesiveSite

CartSp is a cohesive site (i.e. in particular locally connected and local, but with a few more properties). From this it follows that the sheaves on it form a cohesive topos. Note that EuclOp (defined below) is not a cohesive site, as it isn't locally connected. Sheaves on it form a cohesive topos too nonetheless, simply because the sheaf topoi on EuclOp and CartSp are equivalent.

noncomputable instance CartSp.instIsConcreteSiteOpenCoverTopology : openCoverTopology.IsConcreteSite

CartSp 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 CartSp.instSubcanonicalOpenCoverTopology : openCoverTopology.Subcanonical

CartSp is a subcanonical site, i.e. all representable presheaves on it are sheaves.

def EuclOp : Type

Equations

• EuclOp = ((n : ℕ) × TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n)))

instance EuclOp.instCoeSortType : CoeSort EuclOp Type

Equations

• EuclOp.instCoeSortType = { coe := fun (u : EuclOp) => ↥u.snd }

instance EuclOp.instSmallCategory : CategoryTheory.SmallCategory EuclOp

Equations

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

instance EuclOp.instHasForget : CategoryTheory.HasForget EuclOp

Equations

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

instance EuclOp.instFunLike (u v : EuclOp) : FunLike (u ⟶ v) ↥u.snd ↥v.snd

Equations

• u.instFunLike v = { coe := fun (f : u ⟶ v) => ⇑f, coe_injective' := ⋯ }

@[simp]

theorem EuclOp.id_app (u : EuclOp) (x : ↥u.snd) : (CategoryTheory.CategoryStruct.id u) x = x

@[simp]

theorem EuclOp.comp_app {u v w : EuclOp} (f : u ⟶ v) (g : v ⟶ w) (x : ↥u.snd) : (CategoryTheory.CategoryStruct.comp f g) x = g (f x)

def EuclOp.openCoverCoverage : CategoryTheory.Coverage EuclOp

The open cover coverage on EuclOp, 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 EuclOp.openCoverTopology : CategoryTheory.GrothendieckTopology EuclOp

The open cover grothendieck topology on EuclOp.

Equations

• EuclOp.openCoverTopology = CategoryTheory.Coverage.toGrothendieck EuclOp EuclOp.openCoverCoverage

theorem EuclOp.openCoverTopology.mem_sieves_iff {n : EuclOp} {s : CategoryTheory.Sieve n} : s ∈ openCoverTopology n ↔ ∃ r ≤ s.arrows, r ∈ openCoverCoverage.covering n

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

theorem EuclOp.openCoverTopology.mem_sieves_iff' {n : EuclOp} {s : CategoryTheory.Sieve n} : s ∈ openCoverTopology n ↔ ⋃ (m : EuclOp), ⋃ (f : m ⟶ n), ⋃ (_ : s.arrows f ∧ IsOpenInduction ⇑f), Set.range ⇑f = Set.univ

def EuclOp.isTerminal0Top : CategoryTheory.Limits.IsTerminal ⟨0, ⊤⟩

univ : Set (Eucl 0) is terminal in EuclOp.

Equations

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

instance EuclOp.instHasTerminal : CategoryTheory.Limits.HasTerminal EuclOp

noncomputable instance EuclOp.instUniqueSubtypeEuclideanSpaceRealFinFstNatOpensTerminalMemSnd : Unique ↥(⊤_ EuclOp).snd

Equations

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

noncomputable instance EuclOp.instIsConcreteSiteOpenCoverTopology : openCoverTopology.IsConcreteSite

EuclOp 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 EuclOp.instSubcanonicalOpenCoverTopology : openCoverTopology.Subcanonical

EuclOp is a subcanonical site, i.e. all representable presheaves on it are sheaves.

noncomputable def CartSp.toEuclOp : CategoryTheory.Functor CartSp EuclOp

The embedding of CartSp into EuclOp.

Equations

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

instance instIsCoverDenseCartSpEuclOpToEuclOpOpenCoverTopology : CartSp.toEuclOp.IsCoverDense EuclOp.openCoverTopology

Open subsets of cartesian spaces can be covered with cartesian spaces.

instance instFullCartSpEuclOpToEuclOp : CartSp.toEuclOp.Full

instance instFaithfulCartSpEuclOpToEuclOp : CartSp.toEuclOp.Faithful

instance instIsDenseSubsiteCartSpEuclOpOpenCoverTopologyOpenCoverTopologyToEuclOp : CategoryTheory.Functor.IsDenseSubsite CartSp.openCoverTopology EuclOp.openCoverTopology CartSp.toEuclOp

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

Embeddings into other categories

TODO: split this off into some other file, to reduce the imports of this file

noncomputable def CartSp.toAlgebraCatOp : CategoryTheory.Functor CartSp (AlgebraCat ℝ)ᵒᵖ

The embedding of CartSp into the opposite category of ℝ-algebras, sending each space X to the algebra of smooth maps X → ℝ. TODO: change this to the category of commutative algebras next time mathlib is bumped

Equations

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

@[simp]

theorem CartSp.toAlgebraCatOp_obj (X : CartSp) : toAlgebraCatOp.obj X = Opposite.op (AlgebraCat.of ℝ (DSmoothMap (EuclideanSpace ℝ (Fin X)) ℝ))

@[simp]

theorem CartSp.toAlgebraCatOp_map {n m : CartSp} (f : n ⟶ m) : toAlgebraCatOp.map f = (AlgebraCat.ofHom (DSmoothMap.compRightAlgHom f)).op

noncomputable def CartSp.toAlgebraCatOpFullyFaithful : toAlgebraCatOp.FullyFaithful

Equations

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

instance instFullCartSpOppositeAlgebraCatRealToAlgebraCatOp : CartSp.toAlgebraCatOp.Full

instance instFaithfulCartSpOppositeAlgebraCatRealToAlgebraCatOp : CartSp.toAlgebraCatOp.Faithful