## Stream: condensed mathematics

### Topic: universal maps

#### Kevin Buzzard (Jan 31 2021 at 13:51):

I worked through the relatively straightforward argument that these universal_maps we defined are indeed the same as maps $\mathbb{Z}[A^m]\to\mathbb{Z}[A^n]$ which are functorial in $A$. I may as well just write this up if nobody has done it already. Has anyone?

#### Kevin Buzzard (Jan 31 2021 at 18:53):

I hope the thumbs-up doesn't mean "I've done it already" :-) Working on branch universal_universe. I've just run into an issue. I was working with universes, but because Lean's universes aren't cumulative I find that I can't use $\mathbb{Z}^m$ to be the universal object because it's in Type.

#### Kevin Buzzard (Jan 31 2021 at 18:53):

Maybe now is the time to learn about ulift.

#### Kevin Buzzard (Jan 31 2021 at 18:54):

⊢ add_comm_group (ulift ℤ ^ m)

#### Kevin Buzzard (Jan 31 2021 at 18:54):

Is there a machine for this or do I just give up now?

#### Adam Topaz (Jan 31 2021 at 19:40):

@Kevin Buzzard

import tactic
import algebra

example {α β : Type*} [add_comm_group α] (f : β ≃ α) : add_comm_group β :=
by transport using f.symm

universes u
example {α : Type} [add_comm_group α] : add_comm_group (ulift α : Type u) :=
by transport using (equiv.ulift : (ulift α : Type u) ≃ α).symm


#### Kevin Buzzard (Jan 31 2021 at 19:41):

I've started on this using free_abelian_group (punit) now. But this is a great trick!

#### Adam Topaz (Jan 31 2021 at 19:42):

Yeah, I never heard about this transport tactic before. I just found it in the API docs 5 minutes ago :)

#### Kevin Buzzard (Jan 31 2021 at 20:06):

Scott wrote it IIRC, after I was complaining that if R and S were isomorphic rings and R was local then I couldn't prove S was local. I can't remember if he got this far with it.

#### Alex J. Best (Jan 31 2021 at 21:34):

This is in algebra.group.ulift I think

import algebra.group.ulift
import tactic

universes u
example {α : Type} [add_comm_group α] : add_comm_group (ulift α : Type u) :=
by apply_instance


#### Kevin Buzzard (Jan 31 2021 at 21:36):

I am running into other problems. docs#free_abelian_group.map wants the two types to be in the same universe.

#### Kevin Buzzard (Jan 31 2021 at 21:37):

Knowing Kenny, this is probably not an accident.

#### Adam Topaz (Jan 31 2021 at 21:40):

I think map is mostly used for the monad instance, where you need the same universe for join. Why not use lift instead?

#### Kevin Buzzard (Jan 31 2021 at 21:42):

I need an isomorphism free_abelian_group ((Z^m)^n) = free_abelian_group (((some Z in universe u)^n)^m)

#### Adam Topaz (Jan 31 2021 at 21:43):

Oh? The free abelian group on the free abelian group?

Is that a typo?

no

#### Kevin Buzzard (Jan 31 2021 at 21:44):

universal map m n is defined to be the LHS, and I have an element of the RHS.

Oh right. okay.

#### Kevin Buzzard (Jan 31 2021 at 21:46):

All these problems would go away if I stopped being universe polymorphic but then I think that this would force all the profinite sets in the application to be in Type.

#### Kevin Buzzard (Jan 31 2021 at 21:51):

Given a functorial (in A, an abelian group in universe u) group hom $\mathbb{Z}[A^m]\to\mathbb{Z}[A^n]$ we need to construct a term of type universal_map m n, the free abelian group on $(\mathbb{Z}^n)^m$. The idea is to evaluate at $A=\Z'^m$ (where the prime indicates a $\mathbb{Z}$ in universe u), and then evaluate the group hom at the identity matrix in $(\mathbb{Z}^m)^m$ giving an element of $\mathbb{Z}[(\mathbb{Z}'^m)^n]$. I just keep running into annoying things, and there will probably be more annoyances in the proof that the diagram commutes, but I might just grit my teeth and press on.

#### Kevin Buzzard (Jan 31 2021 at 21:52):

I've pushed to the universal_universe branch.

#### Adam Topaz (Jan 31 2021 at 21:53):

It's not the prettiest:

import group_theory.free_abelian_group

variables {α β : Type*}

def foo (f : α ≃ β) : free_abelian_group α ≃+ free_abelian_group β :=
{ to_fun := free_abelian_group.lift $free_abelian_group.of ∘ f, inv_fun := free_abelian_group.lift$ free_abelian_group.of ∘ f.symm,
left_inv := begin
intros x,
apply free_abelian_group.induction_on x,
simp,
simp,
simp,
intros x y h,
simp [h],
end,
right_inv := begin
intros x,
apply free_abelian_group.induction_on x,
simp,
simp,
simp,
intros x y h,
simp [h],
end,


#### Kevin Buzzard (Jan 31 2021 at 23:43):

yeah I've written several other proofs like that today :-) Thanks! by tidy is just by {intros, simp} in this case.

#### Kevin Buzzard (Feb 01 2021 at 00:09):

I've defined both maps (from universal_map m n to the functors and back) and almost proved one of the compositions is the identity. Will finish it tomorrow. Would have been easier but for universe issues.

#### Johan Commelin (Feb 01 2021 at 05:44):

@Kevin Buzzard thanks for doing this! It's one of those things that we probably don't need in the strictest sense of the word, but that are really good to have.

#### Kevin Buzzard (Feb 01 2021 at 07:55):

To be quite frank the reason I was interested was that I'd not seen a proof written down but I'd noticed that what we were doing seemed to rely on the truth of the statement.

#### Johan Commelin (Feb 01 2021 at 08:17):

I think that the part that we really rely on is the direction universal_map -> functorial complex. If there are functorial complexes that somehow didn't come from universal maps... well, we just made our statement more restrictive, but not necessarily false.
But I'm happy that you wrote up this proof.

#### Kevin Buzzard (Feb 01 2021 at 08:53):

Here's a question I don't understand: how does one tell if two universal maps $u : \mathbb{Z}[A^m]\to\mathbb{Z}[A^n]$ and $v:\mathbb{Z}[A^n]\to\mathbb{Z}[A^r]$ satisfy $im(u)=\ker(v)$ for all $A$?

#### Johan Commelin (Feb 01 2021 at 08:53):

I thought a bit about this. But it seems quite non-trivial. I didn't find a linear-algebraic condition for this.

#### Kevin Buzzard (Feb 01 2021 at 08:59):

What I am trying to convince Lean of right now (and will hopefully finish today) is that $u:=u_A$ is determined by $u_{\mathbb{Z}^m}$ (and even the value of that function on "the identity matrix" in $(\mathbb{Z}^m)^m$). But you can't let $A$ be $\mathbb{Z}^m$ and $\mathbb{Z}^n$ at the same time.

#### Johan Commelin (Feb 01 2021 at 09:01):

where you look at functors on the category of all finite rank lattices (which is what you mean with "determined by $u_{\mathbb Z^m}$", right?)

#### Kevin Buzzard (Feb 01 2021 at 09:01):

No, the value of the functor on any abelian group is determined by the value on $\mathbb{Z}^m$.

#### Johan Commelin (Feb 01 2021 at 09:02):

ooh, ok. (Btw, I was thinking of p28ff from Condensed.pdf)

#### Johan Commelin (Feb 01 2021 at 09:02):

Let me see if I understand what you mean.

#### Kevin Buzzard (Feb 01 2021 at 09:02):

$u_A$ is determined by its values on a general element $(a_i)$ of $A^m$ and there's a map from $\mathbb{Z}^m$ to $A$ sending $e_i$ to $a_i$.

#### Peter Scholze (Feb 01 2021 at 10:05):

Kevin Buzzard said:

Here's a question I don't understand: how does one tell if two universal maps $u : \mathbb{Z}[A^m]\to\mathbb{Z}[A^n]$ and $v:\mathbb{Z}[A^n]\to\mathbb{Z}[A^r]$ satisfy $im(u)=\ker(v)$ for all $A$?

Good question! I don't think it's easy to formalize that. Fortunately, I think you don't need to. Namely, any Breen-Deligne data as formalized by Johan should satisfy 9.4+9.5, and he gives one nontrivial example of such data. This example is however not a resolution of $A$. However, one can prove with very little effort (certainly on paper, and I would even expect in Lean) that for any torsion-free $A$, the homology of his complex for $A$ is the homology of his complex for $\mathbb Z$, tensored with $A$. This is good enough to conclude 9.1.

#### Johan Commelin (Feb 01 2021 at 10:06):

I still need to understand this "very little effort" proof :rofl: I think you wrote a sketch of the proof in some message before. I'll have to look it up again.

#### Peter Scholze (Feb 01 2021 at 10:12):

Johan Commelin said:

I still need to understand this "very little effort" proof :rofl: I think you wrote a sketch of the proof in some message before. I'll have to look it up again.

Maybe I should stress that the proof works for any Breen-Deligne data (with homotopy). Regarding the example, you only need to check that it is "nontrivial", for which it's enough to compute its zeroth homology (which is $\mathbb Z$).

#### Johan Commelin (Feb 01 2021 at 14:09):

@Kevin Buzzard did you push your work to some branch?

#### Kevin Buzzard (Feb 01 2021 at 14:10):

universal_universe. I'm about to spend another hour on it.

#### Johan Commelin (Feb 01 2021 at 14:10):

Are you live streaming it, by chance?

#### Kevin Buzzard (Feb 01 2021 at 14:10):

It has got to the point where I believe it though :-)

#### Kevin Buzzard (Feb 01 2021 at 14:10):

Sure, I'll live stream on the discord

#### Kevin Buzzard (Feb 01 2021 at 14:10):

give me 10 minutes

#### Johan Commelin (Feb 01 2021 at 14:13):

ooh, I'll need to figure out how to get into discord...

#### Johan Commelin (Feb 01 2021 at 14:13):

give me 10 minutes :rofl:

#### Adam Topaz (Feb 01 2021 at 14:20):

(I'm therre now :smile: )

#### Riccardo Brasca (Feb 01 2021 at 14:21):

Can someone send me an invitation link? :)

#### Adam Topaz (Feb 01 2021 at 14:22):

@Kevin Buzzard :up: ?

#### Kevin Buzzard (Feb 01 2021 at 14:29):

https://discord.gg/JRXBh4HR

#### Kevin Buzzard (Feb 01 2021 at 14:29):

expires in 24 hours

Thank you!

#### Kevin Buzzard (Feb 01 2021 at 15:07):

Sorry, I'll be back in ten, I just need to deal with real life for a second

#### Kevin Buzzard (Feb 01 2021 at 15:08):

I have a meeting with Amelia at 4, I'll try and persuade her to show off Koszul complexes :-)

#### Kevin Buzzard (Feb 01 2021 at 20:06):

The code takes a long time to compile but I've got it down to

lemma aux_lemma {A : Type*} [add_comm_group A] (a : A) (c : ℤ[punit]) :
(free_abelian_group.lift (λ _, (1 : ℤ))) c • a = free_abelian_group.lift (λ _, a) c :=


:D . I should really be preparing my course but I'm so close!

#### Johan Commelin (Feb 01 2021 at 20:31):

I guess the trick is to somehow show that this is an equality of two monoid homs : ℤ[punit] ->+ A applied to c. Then you can congr c away, and use ext.

#### Johan Commelin (Feb 01 2021 at 20:32):

Alternatively, you apply induction on c, but then you have to prove stupid cases.

Done it :-)

#### Kevin Buzzard (Feb 01 2021 at 20:44):

I did the induction, on the integer corresponding to c

#### Kevin Buzzard (Feb 05 2021 at 20:26):

@Johan Commelin this code is in some kind of shape now. Shall I merge to master? Right now I'm on universal_universe branch. It takes a while to compile unfortunately, but I don't really know what to do about this.

sure, just merge

#### Johan Commelin (Feb 05 2021 at 20:52):

@Kevin Buzzard I just pushed a commit that fixes the broken build on github

#### Johan Commelin (Feb 05 2021 at 20:52):

so be sure to pull that in before you merge

#### Kevin Buzzard (Feb 12 2021 at 09:29):

Ok I finally merged this

Last updated: May 09 2021 at 16:20 UTC