The site CartSp of cartesian spaces ℝⁿ and smooth maps

In this file we define the category CartSp of cartesian spaces ℝⁿ and smooth maps between them, and equip it with the open cover coverage. This site is of relevance because it is the simplest of several sites on which concrete sheaves correspond exactly to diffeological spaces.

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

TODO

• 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 ℕ∞
• 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 }

noncomputable 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 = CartSp.openCoverCoverage.toGrothendieck

theorem CartSp.openCoverTopology.mem_sieves_iff {n : CartSp} {s : CategoryTheory.Sieve n} : s ∈ openCoverTopology n ↔ ∃ r ≤ s.arrows, r ∈ openCoverCoverage.coverings 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

noncomputable 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.

@[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 in another file) 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.