The site EuclOp of open subsets of ℝⁿ

This file defines the category EuclOp of open subsets of the cartesian spaces ℝⁿ and smooth maps between them and equips it with the good open cover coverage. This site is of relevance because it is one of several sites on which concrete sheaves correspond exactly to diffeological spaces.

Main definitions / results:

• 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 EuclOp to take a smoothness parameter in WithTop ℕ∞

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 }

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

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

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