Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeJan 29th 2018
   • (edited Jan 29th 2018)
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexOver at _[[coverage]]_, we write: > Any presheaf which is a sheaf for a family $\{f_i:U_i\to U\}_{i\in I}$ and also for some family $\{h_{i j}:U_{i j} \to U_i\}_{j\in J_i}$ for each $i$ is also a sheaf for the family of all composites $\{f_i h_{i j}:U_{i j}\to U\}_{i\in I, j\in U_i}$. Which shows that the coverings can be closed up so that the following is true: > For any covering $\{f_i : U_i \to U\}_{i \in I}$ and any function $h$ which associates to any $i \in I$ a covering $\{h_{ij} : U_{ij} \to U_i\}_{j \in J_i}$ of $U_i$, the family of all composites $\{f_i h_{ij}\}_{i \in I, j \in U_i}\}$ is a covering of $U$. I believe that: 1. It's constructively provable that we can, indeed, close any given coverage such that this condition is satisfied. 2. While constructively provable, it's not constructively useful, because in applications we won't be able to construct a *function* h as in the condition. Instead, we'll only be able to show that for any $i$ *there exists* a covering of $U_i$ such that some property holds. Do you agree with this analysis? For a constructive context, I propose the following stronger saturation condition: > For any object $U$, any set $M$ of morphisms with target $U$ and any covering $\{f_i : U_i \to U\}_{i \in I}$ such that for every $i$ there exists a covering $\{h_{ij} : U_{ij} \to U_i\}_{j \in J}$ such that $\{ f_i h_{ij} | j \in J \} \subseteq M$, there is a covering $\{g_k : V_k \to U\}_{k \in K}$ such that all $g_k$ are contained in $M$. (We could add the further condition that each of the $g_k$ factors over one of the $f_i$, to be closer to the classical condition.) I noticed this subtletly when trying to prove, without skipping details, that the Kripke–Joyal semantics for a sheaf topos satisfies the usual properties we expect of it (monotonicity, locality, soundness with respect to intuitionistic logic).

   Over at coverage, we write:

   Any presheaf which is a sheaf for a family $\{f_i:U_i\to U\}_{i\in I}$ and also for some family $\{h_{i j}:U_{i j} \to U_i\}_{j\in J_i}$ for each $i$ is also a sheaf for the family of all composites $\{f_i h_{i j}:U_{i j}\to U\}_{i\in I, j\in U_i}$.

   Which shows that the coverings can be closed up so that the following is true:

   For any covering $\{f_i : U_i \to U\}_{i \in I}$ and any function $h$ which associates to any $i \in I$ a covering $\{h_{ij} : U_{ij} \to U_i\}_{j \in J_i}$ of $U_i$, the family of all composites $\{f_i h_{ij}\}_{i \in I, j \in U_i}\}$ is a covering of $U$.

   I believe that:

   1. It’s constructively provable that we can, indeed, close any given coverage such that this condition is satisfied.

   2. While constructively provable, it’s not constructively useful, because in applications we won’t be able to construct a function h as in the condition. Instead, we’ll only be able to show that for any $i$ there exists a covering of $U_i$ such that some property holds.

   Do you agree with this analysis? For a constructive context, I propose the following stronger saturation condition:

   For any object $U$, any set $M$ of morphisms with target $U$ and any covering $\{f_i : U_i \to U\}_{i \in I}$ such that for every $i$ there exists a covering $\{h_{ij} : U_{ij} \to U_i\}_{j \in J}$ such that $\{ f_i h_{ij} | j \in J \} \subseteq M$, there is a covering $\{g_k : V_k \to U\}_{k \in K}$ such that all $g_k$ are contained in $M$.

   (We could add the further condition that each of the $g_k$ factors over one of the $f_i$, to be closer to the classical condition.)

   I noticed this subtletly when trying to prove, without skipping details, that the Kripke–Joyal semantics for a sheaf topos satisfies the usual properties we expect of it (monotonicity, locality, soundness with respect to intuitionistic logic).

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJan 29th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexCouldn't you just let $I'$ be the set of pairs $(i,(h_{i j})_j)$ where $i\in I$ and $(h_{i j})_i$ is a covering of $U_i$ having the desired property? Then if you define $U_{(i,(h_{i j})_i)} = U_i$, we have another covering of $U$ indexed by $I'$ (it's again a covering because the original covering factors through it --- as long as you phrase that closure condition using an existential rather than a function) for which there is such a function.

   Couldn’t you just let $I'$ be the set of pairs $(i,(h_{i j})_j)$ where $i\in I$ and $(h_{i j})_i$ is a covering of $U_i$ having the desired property? Then if you define $U_{(i,(h_{i j})_i)} = U_i$, we have another covering of $U$ indexed by $I'$ (it’s again a covering because the original covering factors through it — as long as you phrase that closure condition using an existential rather than a function) for which there is such a function.

3. • CommentRowNumber3.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeJan 30th 2018
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexOh, yes! I overlooked that we could use this trick. I'm not entirely sure yet which set of saturation conditions I prefer. The verification of the properties of the Kripke–Joyal semantics goes through very cleanly with precisely the following saturation conditions: 1. The basic condition which makes up our definition of a coverage. 2. The condition that singleton families consisting only of an identity morphism are coverings. 3. The condition stated in my post. But maybe the Kripke–Joyal semantics are not the ideal yardstick for calibrating the site axioms.

   Oh, yes! I overlooked that we could use this trick.

   I’m not entirely sure yet which set of saturation conditions I prefer. The verification of the properties of the Kripke–Joyal semantics goes through very cleanly with precisely the following saturation conditions:

   1. The basic condition which makes up our definition of a coverage.

   2. The condition that singleton families consisting only of an identity morphism are coverings.

   3. The condition stated in my post.

   But maybe the Kripke–Joyal semantics are not the ideal yardstick for calibrating the site axioms.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJan 30th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexA better-known variant, which is similar to your condition, is the one stated in terms of sieves: if $R$ is a sieve on $U$, and $S$ is a covering sieve on $U$ such that for all $f\in S$ the restricted sieve $f^*R$ is covering on the domain of $f$, then $R$ is covering.

   A better-known variant, which is similar to your condition, is the one stated in terms of sieves: if $R$ is a sieve on $U$, and $S$ is a covering sieve on $U$ such that for all $f\in S$ the restricted sieve $f^*R$ is covering on the domain of $f$, then $R$ is covering.

5. • CommentRowNumber5.
   • CommentAuthorDavidRoberts
   • CommentTimeJan 30th 2018
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexThere is of course a definition in the Elephant for internal sites, but it might not be helpful for what you want.

   There is of course a definition in the Elephant for internal sites, but it might not be helpful for what you want.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeJan 30th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe definition of internal site in the Elephant uses sieves, as in #4.

   The definition of internal site in the Elephant uses sieves, as in #4.

7. • CommentRowNumber7.
   • CommentAuthorDavidRoberts
   • CommentTimeJan 31st 2018
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItex>But maybe the Kripke–Joyal semantics are not the ideal yardstick for calibrating the site axioms. I think it's a good yardstick, even if there are others. One would ideally like to argue about iterated forcing in non-classical set theories using the internal language of Grothendieck toposes over Grothendieck toposes. Set theorists who work with ZFC and forcing have a good collection of working rules and lemmas etc that allow one to move from the forcing semantics of the final model to talking about the notion of forcing inside the intermediate model. I don't recall seeing this type of thing before in the more general sheaf-theoretic forcing setting.

   But maybe the Kripke–Joyal semantics are not the ideal yardstick for calibrating the site axioms.

   I think it’s a good yardstick, even if there are others. One would ideally like to argue about iterated forcing in non-classical set theories using the internal language of Grothendieck toposes over Grothendieck toposes. Set theorists who work with ZFC and forcing have a good collection of working rules and lemmas etc that allow one to move from the forcing semantics of the final model to talking about the notion of forcing inside the intermediate model. I don’t recall seeing this type of thing before in the more general sheaf-theoretic forcing setting.