Zulip Chat Archive

Stream: condensed mathematics

Topic: universal maps


view this post on Zulip 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 Z[Am]Z[An]\mathbb{Z}[A^m]\to\mathbb{Z}[A^n] which are functorial in AA. I may as well just write this up if nobody has done it already. Has anyone?

view this post on Zulip 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 Zm\mathbb{Z}^m to be the universal object because it's in Type.

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 18:53):

Maybe now is the time to learn about ulift.

view this post on Zulip Johan Commelin (Jan 31 2021 at 18:54):

:thumbs_up: = cool, go ahead

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 18:54):

⊢ add_comm_group (ulift ℤ ^ m)

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 18:54):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 21:37):

Knowing Kenny, this is probably not an accident.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Jan 31 2021 at 21:43):

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

view this post on Zulip Adam Topaz (Jan 31 2021 at 21:43):

Is that a typo?

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 21:43):

no

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Jan 31 2021 at 21:44):

Oh right. okay.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 21:51):

Given a functorial (in A, an abelian group in universe u) group hom Z[Am]Z[An]\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 (Zn)m(\mathbb{Z}^n)^m. The idea is to evaluate at A=ZmA=\Z'^m (where the prime indicates a Z\mathbb{Z} in universe u), and then evaluate the group hom at the identity matrix in (Zm)m(\mathbb{Z}^m)^m giving an element of Z[(Zm)n]\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.

view this post on Zulip Kevin Buzzard (Jan 31 2021 at 21:52):

I've pushed to the universal_universe branch.

view this post on Zulip 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,
  map_add' := by tidy }

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:Z[Am]Z[An]u : \mathbb{Z}[A^m]\to\mathbb{Z}[A^n] and v:Z[An]Z[Ar]v:\mathbb{Z}[A^n]\to\mathbb{Z}[A^r] satisfy im(u)=ker(v)im(u)=\ker(v) for all AA?

view this post on Zulip 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.

view this post on Zulip 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:=uAu:=u_A is determined by uZmu_{\mathbb{Z}^m} (and even the value of that function on "the identity matrix" in (Zm)m(\mathbb{Z}^m)^m). But you can't let AA be Zm\mathbb{Z}^m and Zn\mathbb{Z}^n at the same time.

view this post on Zulip Johan Commelin (Feb 01 2021 at 09:00):

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

view this post on Zulip 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 uZmu_{\mathbb Z^m}", right?)

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 09:01):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 09:02):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 09:02):

Let me see if I understand what you mean.

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 09:02):

uAu_A is determined by its values on a general element (ai)(a_i) of AmA^m and there's a map from Zm\mathbb{Z}^m to AA sending eie_i to aia_i.

view this post on Zulip 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:Z[Am]Z[An]u : \mathbb{Z}[A^m]\to\mathbb{Z}[A^n] and v:Z[An]Z[Ar]v:\mathbb{Z}[A^n]\to\mathbb{Z}[A^r] satisfy im(u)=ker(v)im(u)=\ker(v) for all AA?

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 AA. However, one can prove with very little effort (certainly on paper, and I would even expect in Lean) that for any torsion-free AA, the homology of his complex for AA is the homology of his complex for Z\mathbb Z, tensored with AA. This is good enough to conclude 9.1.

view this post on Zulip 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.

view this post on Zulip 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 Z\mathbb Z).

view this post on Zulip Johan Commelin (Feb 01 2021 at 14:09):

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

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 14:10):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 14:10):

Are you live streaming it, by chance?

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 14:10):

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

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 14:10):

Sure, I'll live stream on the discord

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 14:10):

give me 10 minutes

view this post on Zulip Johan Commelin (Feb 01 2021 at 14:13):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 14:13):

give me 10 minutes :rofl:

view this post on Zulip Adam Topaz (Feb 01 2021 at 14:20):

(I'm therre now :smile: )

view this post on Zulip Riccardo Brasca (Feb 01 2021 at 14:21):

Can someone send me an invitation link? :)

view this post on Zulip Adam Topaz (Feb 01 2021 at 14:22):

@Kevin Buzzard :up: ?

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 14:29):

https://discord.gg/JRXBh4HR

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 14:29):

expires in 24 hours

view this post on Zulip Riccardo Brasca (Feb 01 2021 at 14:33):

Thank you!

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 01 2021 at 20:32):

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

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 20:42):

Done it :-)

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 20:44):

I did the induction, on the integer corresponding to c

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 05 2021 at 20:41):

sure, just merge

view this post on Zulip Johan Commelin (Feb 05 2021 at 20:52):

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

view this post on Zulip Johan Commelin (Feb 05 2021 at 20:52):

so be sure to pull that in before you merge

view this post on Zulip Kevin Buzzard (Feb 12 2021 at 09:29):

Ok I finally merged this


Last updated: May 09 2021 at 16:20 UTC