Zulip Chat Archive

Stream: Is there code for X?

Topic: free_abelian_group.of is injective


view this post on Zulip Eric Wieser (Nov 18 2020 at 12:32):

This strikes me as an obviously true statement, but it seems difficult to prove.

free_abelian_group.of x is defined as abelianization.of $ free_group.of x, where we already have docs#free_group.of.inj.

Obviously docs#abelianization.of is not injective, but it should be injective on the range of free_group.of, right?

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:34):

Yes

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:35):

The image is a basis as a Z-module. If this fact is in mathlib, you can use that to prove injectivity

view this post on Zulip Eric Wieser (Nov 18 2020 at 12:36):

The image of abelianization.of or of free_group.of? (or both?)

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:36):

The free abelian group

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:36):

(which happens to be the abelianization of the free group)

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:37):

So the map from X to the free abelian group generated by X is injective

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:37):

The abelianization map from a group to its abelianization is almost never injective

view this post on Zulip Eric Wieser (Nov 18 2020 at 12:38):

If "The image is a basis as a Z-module" is in mathlib, it's hiding in another file somewhere

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:38):

(it's injective if and only if your original group was already abelian :wink:)

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:39):

You can still use it though, using the universal prop of the free abelian geoup

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:43):

I.e. take the free Z-module on X, say M, which comes with an injective map f : X -> M. Now lift f to a map from the free abelian group on X, say F, to a map of abelian groups F -> M. The universal prop says that the composition with g : X -> F is just f, which in injective, so g must be injective too

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:43):

(sorry for the bad typesetting, I'm on mobile)

view this post on Zulip Eric Wieser (Nov 18 2020 at 12:48):

I think your closing injectiveness argument may be missing from mathlib too - is it this one? https://github.com/leanprover-community/mathlib/compare/flat-module#diff-0dc822e485488f721fc8ef8bd0401825688b5e8b6e30d48decc73024f66e472cR37-R56

(f : α → β) (e : β ≃ γ) : function.injective (e ∘ f) ↔ function.injective f

view this post on Zulip Adam Topaz (Nov 18 2020 at 12:54):

I'm just saying that if fgf \circ g is injective then so is gg. Is this not mathlib?!

view this post on Zulip Johan Commelin (Nov 18 2020 at 12:54):

That one is

view this post on Zulip Eric Wieser (Nov 18 2020 at 12:59):

That statement isn't true?

view this post on Zulip Eric Wieser (Nov 18 2020 at 12:59):

g needs to be only injective over the range of f

view this post on Zulip Reid Barton (Nov 18 2020 at 13:00):

You're reading it backwards

view this post on Zulip Adam Topaz (Nov 18 2020 at 13:02):

@Eric Wieser you're turning into a true category theorist! (who never remember the order of function composition)

view this post on Zulip Eric Wieser (Nov 18 2020 at 13:03):

Johan Commelin said:

That one is

Found it, docs#function.injective.of_comp

view this post on Zulip Adam Topaz (Nov 18 2020 at 13:03):

Don't worry though, it gets much worse when you start thinking about concatenation of paths when defining fundamental groups, and how to reconcile that with monodromy actions

view this post on Zulip Kevin Buzzard (Nov 18 2020 at 13:08):

In Freitag-Kiehl, the appendix on the fundamental group, covering groups always act on the right. I was initially surprised by this convention but things work out great with it.

view this post on Zulip Adam Topaz (Nov 18 2020 at 13:09):

I think if you always define fundamental groups as automorphism groups of fibre/fiber functors, you will never get confused :big_smile:

view this post on Zulip Johan Commelin (Nov 18 2020 at 13:09):

In mathlib, however... we don't have right actions


Last updated: May 16 2021 at 05:21 UTC