Sheaf conditions

Stream: condensed mathematics

[Adam Topaz]

I proved the sheaf condition (for condensed sets) in terms of finite products and equalizers associated to surjective maps of Profinite sets here
https://github.com/leanprover-community/lean-liquid/blob/b8ebef1943604d3b8af4cb65eb9d313e15f65dcc/src/condensed/is_proetale_sheaf.lean#L351

Now the question is how to formulate the condition in terms of exteremally disconnected sets. Any ideas?

[Johan Commelin]

@Adam Topaz Can you remind me why we need P.is_proetale_sheaf_of_types? Why can't we use the generic sheaf condition?

[Johan Commelin]

I see that we have

theorem is_proetale_sheaf_of_types_iff :
  P.is_proetale_sheaf_of_types ↔ presieve.is_sheaf proetale_topology P :=

[Johan Commelin]

Shouldn't that RHS be the main way of talking about condensed gadgets?

[Adam Topaz]

The general sheaf condition uses coyoneda to reduce to the condition for types.

[Adam Topaz]

For types the two are equivalent

[Adam Topaz]

See docs#category_theory.presheaf.is_sheaf_iff_is_sheaf_of_type

[Johan Commelin]

Isn't presieve.is_sheaf the thing that the rest of category_theory/ communicates with and has API for?

[Johan Commelin]

That's why I would guess it should be the default way of talking about condensed things.

[Johan Commelin]

But maybe that's also what is already happening.

[Adam Topaz]

I'm not sure I understand what you're asking

[Adam Topaz]

The RHS of that lemma is indeed the general sheaf of types condition, but the LHS is specific for condensed sets

[Johan Commelin]

So how many ways do we now have to say: presheaf X is a condensed sheaf?

[Adam Topaz]

Lots :wink:

[Johan Commelin]

Right. So I guess we need to assemble them in a tfae at some point.

[Adam Topaz]

Yeah of course

[Johan Commelin]

And then there will be the question: what is going to be the definition, in terms of which we build the rest of the API.

[Johan Commelin]

I somehow thought that you wanted to use P.is_proetale_sheaf_of_types for that. But maybe that's just wrong. In that case, please ignore everything I said.

[Adam Topaz]

Oh for that I think we should use that presieve.is_sheaf condition, since that's essentially how sheaves are defined

[Johan Commelin]

Thanks. I'm back on track.

[Johan Commelin]

Now about the extremally disconnected condition. That's p12 of Condensed.pdf, right? Just below 2.7.

[Johan Commelin]

And it's basicallly just the product condition that you phrased for Profinites.

[Johan Commelin]

And if I understand you correctly, you are asking whether we should do something like "build the category of extr.disc.s, the inclusion functor to Profinite, and then phrase the product condition for inclusion ⋙ X" ... or ... something else, like a hand-rolled Sigma-type like product condition.

[Johan Commelin]

Is that right? Or was your question something else?

[Adam Topaz]

Yup, that's right, but only when restricted to extr.disc sets

[Adam Topaz]

The question is whether we want to actually deal with restricting and extending back to profinites all the time, or if we want to come up with a condition that works while remaining in profinite

[Adam Topaz]

Johan Commelin said:

And if I understand you correctly, you are asking whether we should do something like "build the category of extr.disc.s, the inclusion functor to Profinite, and then phrase the product condition for inclusion ⋙ X" ... or ... something else, like a hand-rolled Sigma-type like product condition.

Does this actually work? If I have some random presheaf on Profinite whose restriction to ExtrDisc satisfies the finite product condition, is it really the case that the original presheaf is a sheaf? I don't think that's right...

[Adam Topaz]

I think a general condition in terms of ExtrDisc sets for presheaves on Profinite could like like this:

1. For all profinite $X$ and extr.disc. $E$ with a surjection $E \to X$ and all extr.disc $E'$ with a surjection to $E \times_X E$, the map $P(X) \to eq(P(E) \to P(E'))$ is a bijection (this is an equalizer, so there are two maps, I don't remember how to typeset that).
2. For all finite families of extr.disc. $X_i$, the map $P(\coprod_i X_i) \to \prod_i P(X_i)$ is a bijection.

[Johan Commelin]

@Adam Topaz I got the impression that the product condition is all you need. At least, that's how I understand the observation just after Prop 2.7.

[Adam Topaz]

If you consider presheaves on ExtrDisc, yes

[Johan Commelin]

But that's what I said, right? You restrict the presheaf X to a presheaf on ExtrDisc by composing with inclusion : ExtrDisc ⥤ Profinite

[Johan Commelin]

And then you impose the product condition.

[Adam Topaz]

Ok, but there may be many presheaves X on Profinite with the same restriction to ExtrDisc

[Johan Commelin]

Hmm, that's a good point.

[Adam Topaz]

If you start with a sheaf X on Profinite, then it's uniquely determined by the restriction to ExtrDosc, but that relies on that equalizer condition

[Johan Commelin]

@Adam Topaz Yeah, I see it now. So I think it should be something like the two conditions you listed above.

[Johan Commelin]

On the other hand, I don't know how important that sheaf condition is for LTE.

[Johan Commelin]

I guess what's more important for us, is for example: f : X ⟶ Y is an iso iff X(S) → Y(S) is an iso for all S : ExtrDisc.

[Johan Commelin]

And other checks that only have to be performed on ExtrDisc. But I don't think we'll leave the sheaf world. And the examples of condensed sets that we construct will probably not use this sheaf condition, right?

[Adam Topaz]

We will need to do something with the sheaf condition when we want to sheafify, when we go to prove that Cond Ab is abelian, to prove it has enough projectives, etc.

[Adam Topaz]

I added:

theorem is_proetale_sheaf_of_types_tfae :
  [ presieve.is_sheaf proetale_topology P
  , P.is_proetale_sheaf_of_types
  , P.is_proetale_sheaf_of_types_pullback
  , P.is_proetale_sheaf_of_types_explicit_pullback
  , P.finite_product_condition ∧ P.equalizer_condition
  ].tfae := ...