completion

Stream: condensed mathematics

[Adam Topaz]

I just pushed a definition of system_of_complexes.completion in the additive branch:
https://github.com/leanprover-community/lean-liquid/blob/c6c56a207b264dd3dfe7c62478ee5aed69522a93/src/system_of_complexes/completion.lean#L17

[Adam Topaz]

If I recall correctly there was some work on the other sorry's in this file somewhere?

[Johan Commelin]

I guess the wip_dtt branch was working towards that, yes

[Adam Topaz]

Ok. I'm diagnosing some universe annoyances right now :sad:

[Adam Topaz]

For some reason NormedGroup.Completion did not have universe annotation {u u} but rather something like {(max u v) (max u v)} and that's breaking some things.

[Adam Topaz]

Okay, the universe nonsense should be fixed now.

[Adam Topaz]

I guess before we continue too far down the rabbit hole here, we should settle on the definition of a complex that we want to use.

What's the current preferred approach? The homological_complex defn from mathlib?

[Johan Commelin]

@Scott Morrison has been experimenting with different approaches lately

[Johan Commelin]

I agree that we should first settle on a defn that works

[Adam Topaz]

Okay, maybe I'll try to make a mathlib PR soon with additive_functor.