cech predicate

Stream: condensed mathematics

[Adam Topaz]

We will eventually need a characteristic predicate asserting that a certain (augmented) simplicial object is a cech nerve. I want to get people's thoughts on the best way to approach this.

I just added some definitions to the cech_stuff branch of LTE in the following file:
https://github.com/leanprover-community/lean-liquid/blob/cech_stuff/src/for_mathlib/cech.lean

One possible definition is to say:

is_iso (cech_unit M)

(see line 65 of the above file.)

The point is that the cech functor is right adjoint to the forgetful functor sending an augmented simplicial object to the augmentation itself (considered as an arrow). Does anyone have any thoughts about this potential definition? I'm concerned that it would be difficult to prove that anything that's not obviously of the form cech.obj foo actually satisfies this.

[Johan Commelin]

I think the most important property that we need from this predicate is that if F is a functor (satisfying some assumptions), then pushing a Cech cover through F will give back a Cech cover.

[Johan Commelin]

In fact, let me be a bit more precise:

1. @Adam Topaz does your Cech machinery so far also handle the cosimplicial case?
2. We start with an (augmented) cosimplicial object in PolyhedralLattice
3. We push this through Hom(_, M) to end up with an (augmented) simplicial object in ProFiltPseuNrmGrp r'
4. We modify the augmentation map a little bit, to get into a situation where 9.8 applies.
5. The resulting gadget should satisfy the is_Cech_nerve predicate.
6. We push this through the $\hat V(\_)$ functor to end up with something (very close) to the columns in the double complex.
7. By 8.19 and friends, we derive the desired exactness conditions.

[Adam Topaz]

I don't have anything Cech related in the cosimplicial case, but it should be easy to add analogous definitions using Lan instead of Ran. I guess we need the equiv between arrows and functors from with_initial (discrete punit) as well.

[Adam Topaz]

Pushing through Hom should be fine, since Hom sends colimits in the first variable to limits, and Lan is constructed as a bunch of colimits

[Johan Commelin]

I mean, whatever we end up doing, it should be able to either handle cosimplicial things, or be able to connect to ad-hoc cosimplicial constructions (which we have now).

[Adam Topaz]

@Johan Commelin could you take a look at the augmented_refactor branch and see if you're happy to merge it to master? It doesn't actually refactor anything, but the constructions there will be helpful in the cech_stuff branch, so it would simplify some things if it gets merged

[Johan Commelin]

Ok, let me finish what I'm doing atm, and then I'll look.

[Adam Topaz]

Thanks :smile:

[Johan Commelin]

@Adam Topaz Just to be sure

$ gdms
 src/for_mathlib/preadditive_category.lean |  20 ++++++++++++
 src/for_mathlib/simplicial/augmented.lean |  81 +++++++++++++++++++++++++++++++++++++++++++++++++
 src/for_mathlib/simplicial/complex.lean   | 157 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 258 insertions(+)

[Johan Commelin]

That's the sort of diff I should be looking at, right?

[Adam Topaz]

Sounds right!

[Johan Commelin]

@Adam Topaz What I can see so far looks fine!

[Johan Commelin]

The proof of the pudding will be in the eating.

[Adam Topaz]

Alright, I'll merge it to master when I get to my computer this afternoon.

[Adam Topaz]

Alright then! I merged augmented_refactor into master:;
https://github.com/leanprover-community/lean-liquid/compare/6768307..e023f5f
CI should go through with no issues (supposedly...)

[Johan Commelin]

Thanks!