completion of locally constant functions

Stream: condensed mathematics

[Johan Commelin]

At some point we will need to know that continuous functions S → V for profinite S and a complete normed group V is isomorphic to the completion of locally_constant S V (wrt the sup norm).

[Johan Commelin]

This seems to me like a self-contained gadget that doesn't need any category theory or homological algebra.
So if you've been wanting to contribute, but don't like categories, this might be for you.

[Johan Commelin]

A precise statement is now located at: https://github.com/leanprover-community/lean-liquid/blob/master/src/free_pfpng/acyclic.lean#L39L41

[Johan Commelin]

It's wrapped in a thin layer of category theory. If that's a problem, I can help strip it away.

[Johan Commelin]

I moved the statement to a new file src/normed_to_cond.

[Kevin Buzzard]

@Ashvni Narayanan do you have something like this already?

[Johan Commelin]

src/normed_to_cond now contains a skeleton that is basically category_theory-free

[Johan Commelin]

The only thing left in this file is the following goal:

S: Profinite.{u}
V': Type u
_inst_3: normed_group.{u} V'
_inst_4: complete_space.{u} V'
f: C(↥S, V')
ε: ℝ
hε: ε > 0
⊢ ∃ (y : locally_constant.{u u} ↥S V'), dist.{u} f y.to_continuous_map < ε

[Johan Commelin]

@Ashvni Narayanan did this over at https://github.com/leanprover-community/mathlib/blob/f2fd1fb4507431cf2f2a873db4b97d360633fb69/src/number_theory/L_functions.lean#L453 !

[Johan Commelin]

I copied the file with Ashvni's permission, and made a few little tweaks. This sorry is now gone as well.