Zulip Chat Archive

Stream: condensed mathematics

Topic: breen_deligne.suitable


view this post on Zulip Johan Commelin (Apr 07 2021 at 21:34):

I pushed some sorrys to breen_deligne.suitable. Anyone interested in fooling around with Breen--Deligne data and explicit (block) matrices should feel free to kill them (-;

view this post on Zulip Kevin Buzzard (Apr 07 2021 at 21:49):

Do we still only have 2x2 block matrices?

view this post on Zulip Adam Topaz (Apr 07 2021 at 21:53):

Doesn't 2×2 suffice for the BD stuff? These are used in the BD homotopy from addition, right?

view this post on Zulip Kevin Buzzard (Apr 07 2021 at 21:56):

Yes I should think so, I just noticed it when I was documenting the files :-)

view this post on Zulip Johan Commelin (Apr 09 2021 at 06:54):

I've added

def very_suitable (f : universal_map m n) (r r' : out_param 0) (c₁ c₂ : 0) : Prop :=
 (N k : ) (c' : 0), f.bound_by N  f.suitable c₁ c'  r ^ k * N  1  c'  r' ^ k * c₂

and

class very_suitable (BD : data) (r r' : out_param 0) (c_ :   0) : Prop :=
(universal_very_suitable :  i j, (BD.d i j).very_suitable r r' (c_ i) (c_ j))

view this post on Zulip Johan Commelin (Apr 09 2021 at 06:54):

Under the assumption BD.very_suitable r r' c_, Lean now agrees that the double complex used in the proof of thm9.5 is admissible


Last updated: May 09 2021 at 16:20 UTC