universal maps

Stream: condensed mathematics

[Kevin Buzzard]

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]

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]

Maybe now is the time to learn about ulift.

[Johan Commelin]

:thumbs_up: = cool, go ahead

[Kevin Buzzard]

⊢ add_comm_group (ulift ℤ ^ m)

[Kevin Buzzard]

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

[Adam Topaz]

@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]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

Knowing Kenny, this is probably not an accident.

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Adam Topaz]

Is that a typo?

[Kevin Buzzard]

no

[Kevin Buzzard]

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

[Adam Topaz]

Oh right. okay.

[Kevin Buzzard]

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]

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]

I've pushed to the universal_universe branch.

[Adam Topaz]

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,
  map_add' := by tidy }

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

@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]

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]

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]

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]

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

[Kevin Buzzard]

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]

aah, cool. I think there is some stuff about this in the lecture notes

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Let me see if I understand what you mean.

[Kevin Buzzard]

$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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

Are you live streaming it, by chance?

[Kevin Buzzard]

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

[Kevin Buzzard]

Sure, I'll live stream on the discord

[Kevin Buzzard]

give me 10 minutes

[Johan Commelin]

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

[Johan Commelin]

give me 10 minutes :rofl:

[Adam Topaz]

(I'm therre now :smile: )

[Riccardo Brasca]

Can someone send me an invitation link? :)

[Adam Topaz]

@Kevin Buzzard :up: ?

[Kevin Buzzard]

https://discord.gg/JRXBh4HR

[Kevin Buzzard]

expires in 24 hours

[Riccardo Brasca]

Thank you!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

Done it :-)

[Kevin Buzzard]

I did the induction, on the integer corresponding to c

[Kevin Buzzard]

@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.

[Johan Commelin]

sure, just merge

[Johan Commelin]

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

[Johan Commelin]

so be sure to pull that in before you merge

[Kevin Buzzard]

Ok I finally merged this