Sheaves on ExtrDisc

Stream: condensed mathematics

[Adam Topaz]

A quick update:
I defined:

def finite_product_condition [limits.has_finite_products C] (F : ExtrDisc.{u}ᵒᵖ ⥤ C) :
  Prop := ∀ (ι : Type u) [fintype ι] (X : ι → ExtrDisc),
begin
  -- Lean is being annoying here...
  resetI,
  let t : Π i, F.obj (op (sigma X)) ⟶ F.obj (op (X i)) := λ i, F.map (sigma.ι X i).op,
  exact is_iso (limits.pi.lift t)
end

and

structure ExtrSheafProd (C : Type.{u'}) [category.{v'} C] [limits.has_finite_products C] :=
(val : ExtrDisc.{u}ᵒᵖ ⥤ C)
(cond : ExtrDisc.finite_product_condition val)

with the natural category structure obtained from the category structure for presheaves.

And the following equivalence is now sorry-free:

noncomputable
def Condensed_ExtrSheafProd_equiv (C : Type.{u'}) [category.{u+1} C] [limits.has_limits C] :
  Condensed.{u} C ≌ ExtrSheafProd.{u} C :=
(Condensed_ExtrSheaf_equiv C).symm.trans (ExtrSheaf_ExtrSheafProd_equiv C)

-- Sanity check
@[simp]
lemma Condensed_ExtrSheafProd_equiv_functor_obj_val
  {C : Type.{u'}} [category.{u+1} C] [limits.has_limits C] (F : Condensed C) :
  ((Condensed_ExtrSheafProd_equiv C).functor.obj F).val = ExtrDisc_to_Profinite.op ⋙ F.val := rfl

This was harder to formalize than I had expected, because ExtrDisc does not have pullbacks. Can anyone think of a reasonable generalization of docs#category_theory.pretopology that does not require pullbacks?

I have an idea, essentially using the following fact about ExtrDisc: For any objects $X_1, X_2, B$ and $f_i : X_i \to B$, there is an object $G$ and morphisms $p_i : G \to X_i$ making the obvious diagram commute, such whenever $H$ and $g_i : H \to X_i$ also satisfy this condition, there is a morphism $H \to G$ such that $g_i$ factors through $H \to G$ via $p_i$ (essentially, take $G$ to be a projective presentation of the pullback in Profinite). This is not as strong as having actual pullbacks, but seems to be good enough for most things.

[Bhavik Mehta]

Adam Topaz said:

This was harder to formalize than I had expected, because ExtrDisc does not have pullbacks. Can anyone think of a reasonable generalization of docs#category_theory.pretopology that does not require pullbacks?

The Elephant defines essentially this exact thing - I decided not to put it in mathlib because I thought it was never useful! In particular, we replace the pullback part of the condition with this: http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/coverage#Definition, and the other two conditions remain the same

[Reid Barton]

I was confused because I thought I remembered seeing a Lean definition of a coverage but then I couldn't find it in mathlib--was it in your other library?

[Bhavik Mehta]

I don't think I ever wrote down a "coverage" as it is there - and most of the stuff which is about sites and not more general is in mathlib by now

[Bhavik Mehta]

docs#category_theory.grothendieck_topology just to make sure!

[Reid Barton]

Hmm maybe I imagined it then, or maybe it was in what Johan wrote in 2019.

[Reid Barton]

Anyways, I definitely think coverages are important, at least from a theoretical perspective. It's the least condition you can have on something defining a topology.

[Adam Topaz]

I should mention that I spent most of my mathematical life completely happy with the definition on the stacks project, which is essentially mathlib's current def of a pretopology, pullbacks and all!

In this case, the Grothendieck topology on Profinite is the one generated by a pretopology, and the one of ExtrDisc is the induced one. It would have made some of the proofs easier if I was able to obtain an induced pretopology on ExtrDisc (which I see now would require changing the def to use coverages!), but that's mostly just because I wanted to prove the equivalence with a "simple" sheaf condition on ExtrDisc. But the key part of the argument showing the equivalence with the condition involving only products is a separate thing (involving splitting a coequalizer). BTW, do we have some API for split (co)equalizers?

[Adam Topaz]

Ha, we have docs#category_theory.is_split_coequalizer

[Johan Commelin]

@Reid Barton Indeed, that's what I did back in A'dam in 2019. And I got horribly stuck, because I had no clue what I was doing Leanwise.

[Adam Topaz]

Another update:

noncomputable
instance preserves_colimits_Condensed_evaluation'
  (S : Profinite.{u}) [projective S] (C : Type w) [category.{u+1} C]
  [has_limits C] [has_colimits C] [has_zero_morphisms C] [has_finite_biproducts C] :
  limits.preserves_colimits (Condensed.evaluation C S) :=
preserves_colimits_Condensed_evaluation ⟨S⟩ _

is sorry-free, and as a result, we have

instance (S : Profinite.{u}) [projective S] :
  projective (ℤ[S]) :=

sorry-free as well!

[Adam Topaz]

Even better, we also have:

-- Forgetting to presheaves, and restricting to `ExtrDisc` creates colimits.
instance Condensed_to_ExtrDisc_presheaf_creates_colimits [has_colimits C] :
  creates_colimits
  ((Sheaf_to_presheaf _ _ : Condensed C ⥤ _) ⋙
  (whiskering_left _ _ _).obj (ExtrDisc_to_Profinite.op)) :=

which says that colimits can be computed objectwise using ExtrDisc.

[Johan Commelin]

Fantastic!

[Adam Topaz]

instance Condensed_Ab_has_enough_projective : enough_projectives (Condensed.{u} Ab.{u+1}) :=

https://github.com/leanprover-community/lean-liquid/blob/088847b7403edd8e4bd6f625140091e48a1b75cb/src/condensed/projective_resolution.lean#L258

[Johan Commelin]

This is now sorry-free ?!?!

[Adam Topaz]

yeah ;)

[Johan Commelin]

Nice! That took a long breath. Great milestone.

[Adam Topaz]

I'm building now (after changing some imports) to double check everything is working.

[Filippo A. E. Nuccio]

Great job, @Adam Topaz !

[Adam Topaz]

So now Ext actually means something ;)

[Johan Commelin]

@Adam Topaz I still see 23 sorry's in extr.lean. Are those unrelated?

[Adam Topaz]

try now

[Johan Commelin]

1       src/challenge.lean
6       src/condensed/basic.lean
4       src/condensed/ab.lean
2       src/condensed/is_proetale_sheaf.lean
1       src/combinatorial_lemma/profinite.lean
9       src/laurent_measures/aux_lemmas.lean
2       src/laurent_measures/thm69.lean
2       src/for_mathlib/derived_functor.lean
1       src/for_mathlib/homological_complex.lean
1       src/for_mathlib/short_exact_sequence.lean
Total:  29

[Johan Commelin]

Wonderful!

[Filippo A. E. Nuccio]

Can't we add 8 sorries?

[Johan Commelin]

0 > 37

[Johan Commelin]

It's even better:

1       src/challenge.lean
3       src/condensed/basic.lean
2       src/condensed/ab.lean
2       src/condensed/is_proetale_sheaf.lean
1       src/combinatorial_lemma/profinite.lean
9       src/laurent_measures/aux_lemmas.lean
2       src/laurent_measures/thm69.lean
2       src/for_mathlib/derived_functor.lean
1       src/for_mathlib/homological_complex.lean
1       src/for_mathlib/short_exact_sequence.lean
Total:  24