free_abelian_group.of is injective

Stream: Is there code for X?

[Eric Wieser]

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?

[Adam Topaz]

Yes

[Adam Topaz]

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

[Eric Wieser]

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

[Adam Topaz]

The free abelian group

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Eric Wieser]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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]

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

[Eric Wieser]

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]

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

[Johan Commelin]

That one is

[Eric Wieser]

That statement isn't true?

[Eric Wieser]

g needs to be only injective over the range of f

[Reid Barton]

You're reading it backwards

[Adam Topaz]

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

[Eric Wieser]

Johan Commelin said:

That one is

Found it, docs#function.injective.of_comp

[Adam Topaz]

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]

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]

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

[Johan Commelin]

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