Zulip Chat Archive

Stream: condensed mathematics

Topic: breen_deligne refactor


view this post on Zulip Johan Commelin (Apr 09 2021 at 20:03):

I'm refactoring a bunch of stuff in breen_deligne/* to make it easier to prove things about the homotopy.
Going to bed now. Pushed my wip to bd_refactor.
There were some sorries in those files (on master) but it probably doesn't make sense to work on those, until the refactor is done.

view this post on Zulip Johan Commelin (Apr 13 2021 at 15:05):

This refactor is now done, and merged into master.

view this post on Zulip Johan Commelin (Apr 13 2021 at 15:09):

At some point we'll need some constants c_ c' : nat -> nnreal that play well with breen_deligne.eg.
Here eg is the explicit example of breen_deligne.package, see breen_deligne/eg.lean.

What we need is that for variable r r' : nnreal (satisfying [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r' ≤ 1)]) we have

  • eg.very_suitable r r' c_ (so c_ shall depend on r and r')
  • eg.adept c_ c' (so c' shall be constructed in terms of a c_, here r and r' don't play a role)

view this post on Zulip Johan Commelin (Apr 13 2021 at 15:10):

So, if you like playing with division/inverses of non-negative reals, then feel free to add constructions of such sequences to eg.lean.


Last updated: May 09 2021 at 21:10 UTC