pro-manifold in nLab

Context

Differential geometry

• Idea
• Pro-Cartesian spaces
• Embedding into smooth loci
• The site of towers of Cartesian spaces and pro-morphisms

Proof

Since Pro(𝒞)≃(Ind(𝒞 op)) opPro(\mathcal{C}) \simeq (Ind(\mathcal{C}^{op}))^{op} (remark) it is sufficient to show that the functor in question is on opposite categories a fully faithful functor of the form

Ind(CartSp op)↪SmthLoc op=SmthAlg ℝ, Ind(CartSp^{op}) \hookrightarrow SmthLoc^{op} = SmthAlg_{\mathbb{R}} \,,

where SmothAlg ℝSmothAlg_{\mathbb{R}} is the category of smooth algebras.

Now, there is the fully faithful functor

i:CartSp↪SmthLoc i \;\colon\; CartSp \hookrightarrow SmthLoc

(prop.) hence a fully faithful functor

i op:CartSp op↪SmthAlg ℝ. i^{op} \colon CartSp^{op} \hookrightarrow SmthAlg_{\mathbb{R}} \,.

Moreover, the image of the latter is in compact objects i op:CartSp op↪(SmthAlg ℝ) cpt↪SmthAlgi^{op} \colon CartSp^{op} \hookrightarrow (SmthAlg_{\mathbb{R}})_{cpt} \hookrightarrow SmthAlg, because

C ∞(ℝ n)≃y(ℝ n)∈SmthAlg ℝ≃Func ×(CartSp,Set) C^\infty(\mathbb{R}^n) \simeq y(\mathbb{R}^n) \in SmthAlg_{\mathbb{R}} \simeq Func_\times(CartSp,Set)

is co-representable, hence compact (by the Yoneda lemma and since colimits are computed objectwise prop.).

This implies that the composite

Ind(CartSp op)↪Ind(i op)Ind(SmthAlg ℝ)⟶LSmthAlg ℝ Ind(CartSp^{op}) \overset{Ind(i^{op})}{\hookrightarrow} Ind(SmthAlg_{\mathbb{R}}) \overset{L}{\longrightarrow} SmthAlg_{\mathbb{R}}

is also fully faithful (prop.).

Here Ind(i op)Ind(i^{op}) takes formal filtered colimits in CartSp opCartSp^{op} to the corresponding formal colimits in SmthAlg ℝSmthAlg_{\mathbb{R}} (prop.), while LL takes formal filtered colimits to actual filtered colimits (prop.). Hence this is indeed the functor in question.

Definition

For U∈TowCartSpU \in TowCartSp a tower of Cartesian spaces (def. ), say that a tower of good open covers of UU is a sequence of morphisms {U i→ϕ iU}\{U_i \overset{\phi_i}{\to} U\} in TowCartSpTowCartSp such that these are the formal sequential limit of a cofiltered diagram of good open covers {U i k→ϕ i kU k}\{U_i^k \overset{\phi_i^k}{\to} U^k\}.

U i k ↦lim⟵ f U i ϕ i k↓ ↓ ϕ i U k ↦lim⟵ f U \array{ U_i^{k} &\overset{\underset{\longleftarrow}{\lim}^f}{\mapsto}& U_i \\ {}^{\mathllap{\phi_i^k}}\downarrow && \downarrow^{\mathrlap{\phi_i}} \\ U^k &\overset{\underset{\longleftarrow}{\lim}^f}{\mapsto}& U }

Definition

The collection of towers of good open covers on TowCartSpTowCartSp, according to def. , constitutes a coverage.

Proof

By the definition of coverage (def.) we need to check that for every tower of good open covers {U i→ϕ iU}\{U_i \overset{\phi_i}{\to} U\} and for every morphism V⟶gUV \overset{g}{\longrightarrow} U in TowCartSpTowCartSp, there exists a tower of good open covers {V j⟶ψ jV}\{V_j \overset{\psi_j}{\longrightarrow} V\} of VV such that for each index jj we may find an index ii and a morphism V j→U iV_j \overset{}{\to} U_i such as to make a commuting diagram of the form

V j ⟶ U i ↓ ↓ ϕ i V ⟶g U. \array{ V_j &\overset{}{\longrightarrow}& U_i \\ \downarrow && \downarrow^{\mathrlap{\phi_i}} \\ V &\underset{g}{\longrightarrow}& U } \,.

Now by this prop. the bottom morphism is represented by a sequence of component morphisms

V n(k)⟶U k. V^{n(k)} \overset{}{\longrightarrow} U^k \,.

Since ordinary good open covers do form a coverage on CartSp (prop.) each of these component diagrams may be completed

V˜ j n(k) ⟶ U i k ↓ ↓ ϕ i k V n(k) ⟶g k U k \array{ \tilde V^{n(k)}_j &\overset{}{\longrightarrow}& U^k_i \\ \downarrow && \downarrow^{\mathrlap{\phi^k_i}} \\ V^{n(k)} &\underset{g^k}{\longrightarrow}& U^k }

by first forming the pullback open cover (g k) *U i k→V n(k)(g^k)^\ast U^k_i \to V^{n(k)} and then refining this to a good open cover V˜ j n(k)→V n(k)\tilde V^{n(k)}_j \to V^{n(k)}. By the universal property of the pullback, there are morphisms

V˜ n(k+1)⟶(g k) *U i k \tilde V^{n(k+1)} \longrightarrow (g^k)^\ast U^k_i

that make the evident cube commute

V˜ j n(k+1) ⟶ U i k+1 ↓ ↓ ϕ i k+1 V n(k+1) ⟶g k+1 U k+1⇒(g k) *U i k ⟶ U i k ↓ ↓ ϕ i k V n(k) ⟶g k U k \array{ \tilde V^{n(k+1)}_j &\overset{}{\longrightarrow}& U^{k+1}_i \\ \downarrow && \downarrow^{\mathrlap{\phi^{k+1}_i}} \\ V^{n(k+1)} &\underset{g^{k+1}}{\longrightarrow}& U^{k+1} } \;\;\;\;\;\;\;\;\;\;\;\; \Rightarrow \;\;\;\;\;\;\;\;\;\;\;\; \array{ (g^{k})^\ast U_i^k &\overset{}{\longrightarrow}& U^k_i \\ \downarrow && \downarrow^{\mathrlap{\phi^k_i}} \\ V^{n(k)} &\underset{g^k}{\longrightarrow}& U^k }

Take

V j n(0)≔V˜ j n(0) V^{n(0)}_j \coloneqq \tilde V^{n(0)}_j

and then inductively define

V j n(k+1) V^{n(k+1)}_j

to be a refinement by a good open cover of the joint refinement of {V˜ j n(k+1)}\{\tilde V^{n(k+1)}_j\} with the pullback of {V j n(k)}\{V^{n(k)}_j\} to V n(k+1)V^{n(k+1)}.

This refines the above commuting cubes to

V j n(k+1) ⟶ U i k+1 ↓ ↓ ϕ i k+1 V n(k+1) ⟶g k+1 U k+1⇒V j n(k) ⟶ U i k ↓ ↓ ϕ i k V n(k) ⟶g k U k \array{ V_j^{n(k+1)} &\overset{}{\longrightarrow}& U^{k+1}_i \\ \downarrow && \downarrow^{\mathrlap{\phi^{k+1}_i}} \\ V^{n(k+1)} &\underset{g^{k+1}}{\longrightarrow}& U^{k+1} } \;\;\;\;\;\;\;\;\;\;\;\; \Rightarrow \;\;\;\;\;\;\;\;\;\;\;\; \array{ V_j^{n(k)} &\overset{}{\longrightarrow}& U^k_i \\ \downarrow && \downarrow^{\mathrlap{\phi^k_i}} \\ V^{n(k)} &\underset{g^k}{\longrightarrow}& U^k }

and hence provides components for the required diagram in TowCartSpTowCartSp.