## Stream: condensed mathematics

### Topic: completion

#### Adam Topaz (Feb 22 2021 at 15:07):

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 (Feb 22 2021 at 15:08):

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

#### Johan Commelin (Feb 22 2021 at 15:17):

I guess the wip_dtt branch was working towards that, yes

#### Adam Topaz (Feb 22 2021 at 15:18):

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

#### Adam Topaz (Feb 22 2021 at 15:20):

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 (Feb 22 2021 at 15:35):

Okay, the universe nonsense should be fixed now.

#### Adam Topaz (Feb 22 2021 at 16:02):

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 (Feb 22 2021 at 16:03):

@Scott Morrison has been experimenting with different approaches lately

#### Johan Commelin (Feb 22 2021 at 16:03):

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

#### Adam Topaz (Feb 22 2021 at 16:04):

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

Last updated: May 09 2021 at 15:11 UTC