SemiNormedGroup completion

Stream: condensed mathematics

[Riccardo Brasca]

I created a new file src/for_mathlib/SemiNormedGroup_Completion.lean that contains all the category theory stuff related to completion of seminormed groups. This was before in src/locally_constant/Vhat.lean, that is now smaller.
I also semplified some proofs, using the stuff in src/for_mathlib/normed_group_hom_completion.lean, but I am sure it can be simplified further. For example, indef Completion, the long map =... should be map := λ V W f, normed_group_hom.completion f. This works in that file, but then I get errors in other places that I am not able to solve. I am not very familiar with the category theory part of the library, so I didn't spent too much time in trying to solve them, can someone have a look at them?

Beside that, I think that we should start PRing at least src/for_mathlib/normed_group_hom_completion.lean.

[Patrick Massot]

I'll handle src/for_mathlib/normed_group_hom_completion.lean

[Riccardo Brasca]

If you want you can also add lemmas like Completion.lift in src/for_mathlib/SemiNormedGroup_Completion.lean. They are stated categorically, but the "concrete statement" should probably be proved first.

[Johan Commelin]

Thanks for dissecting Vhat.lean. It was a mess.

[Johan Commelin]

I can take a look at what's wrong with the map := and the category stuff.

[Riccardo Brasca]

Using

def Completion : SemiNormedGroup.{u} ⥤ SemiNormedGroup.{u} :=
{ obj := λ V, SemiNormedGroup.of (completion V),
  map := λ V W f, normed_group_hom.completion f,
  map_id' := λ V, by { ext1 v, show completion.map id v = v, rw completion.map_id, refl },
  map_comp' :=
  begin
    intros U V W f g, ext1 v, show completion.map (g ∘ f) v = _, rw ← completion.map_comp,
    { refl },
    { exact normed_group_hom.uniform_continuous _ },
    { exact normed_group_hom.uniform_continuous _ }
  end }

I get an error in src/prop819.lean.

[Johan Commelin]

I'll have a look right now

[Riccardo Brasca]

I am also moving src/normed_group/SemiNormedGroup.lean to for_mathlib. All the results there are completely general.

[Johan Commelin]

Completion now has the short definition that @Riccardo Brasca wrote above

[Riccardo Brasca]

#7860