## Stream: Is there code for X?

### Topic: free_abelian_group.of is injective

#### 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?

Yes

#### 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

#### Eric Wieser (Nov 18 2020 at 12:36):

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

#### Adam Topaz (Nov 18 2020 at 12:36):

The free abelian group

#### Adam Topaz (Nov 18 2020 at 12:36):

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

#### Adam Topaz (Nov 18 2020 at 12:37):

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

#### Adam Topaz (Nov 18 2020 at 12:37):

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

#### 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

#### Adam Topaz (Nov 18 2020 at 12:38):

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

#### Adam Topaz (Nov 18 2020 at 12:39):

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

#### 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

#### Adam Topaz (Nov 18 2020 at 12:43):

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

#### 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

#### Adam Topaz (Nov 18 2020 at 12:54):

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

That one is

#### Eric Wieser (Nov 18 2020 at 12:59):

That statement isn't true?

#### Eric Wieser (Nov 18 2020 at 12:59):

g needs to be only injective over the range of f

#### Reid Barton (Nov 18 2020 at 13:00):

You're reading it backwards

#### 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)

#### Eric Wieser (Nov 18 2020 at 13:03):

Johan Commelin said:

That one is

Found it, docs#function.injective.of_comp

#### 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

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

#### 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:

#### 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