[Merged by Bors] - refactor(group_theory/free_*): remove API duplicated by lift, promote lift functions to equivs #6311
Conversation
This removes `free_group.to_group.to_fun` and `free_group.to_group`, as these are both subsumed by the stronger `lift`.
eric-wieser
changed the title
| by the map `f`. | ||
|
|
||
| * `hom_equiv : (free_abelian_group α →+ A) ≃ (α → A)` : the bijection witnessing adjointness. | ||
| * `lift : (α → A) ≃ free_abelian_group α →+ A` : the group homomorphism induced |
There was a problem hiding this comment.
I'm not sure whether this might be confusing to newcomers.
There was a problem hiding this comment.
I suppose I could leave the docstring as it was, and just remove the entry about hom_equiv?
There was a problem hiding this comment.
What about: the adjunction isomorphism between the free abelian group functor and the forgetful functor or the bijection witnessing adjointness between the free abelian group functor and the forgetful functor combined with something like: for a function `f: \alpha\to A` the unique group homomorphism `free_abelian_group \alpha\to+ A` can be accessed using `lift f` ? This is probably a bit much for experts, but for beginners it is maybe appropriate? Here it is maybe not as relevant, but maybe if one wants to be uniform over all such constructions, one could also explain how to access the restriction of g for a group homomorphism g.
There was a problem hiding this comment.
I feel like the category theory interpretation is probably not something we want to include in the description - although it would be quite sensible to add cross-links to the actual definitions of the adjunctions (in a follow-up PR, from someone else who actually knows the lexicon to precisely describe these things!)
There was a problem hiding this comment.
I think, there is a link to the category theory interpretation in the first paragraph of the module doc. Maybe that is sufficient?
| @@ -19,7 +19,7 @@ functor from groups to types, see `algebra/category/Group/adjunctions`. | |||
| modulo the relation `a * x * x⁻¹ * b = a * b`. | |||
| * `mk`: the canonical quotient map `list (α × bool) → free_group α`. | |||
| * `of`: the canoical injection `α → free_group α`. | |||
| * `to_group f`: the canonical group homomorphism `free_group α →* G` given a group `G` and a | |||
| * `lift f`: the canonical group homomorphism `free_group α →* G` given a group `G` and a | |||
There was a problem hiding this comment.
lift should have similar docstrings throughout.
There was a problem hiding this comment.
Any suggestions for how best to document it?
eric-wieser
added
the
awaiting-review
|
LGTM. I don't have time at the moment to think about a suggestion for a universal docstring but can do so later. In principle I agree with the motivation of making things uniform and lift was easy to use for me as a relative beginner. |
github-actions
bot
added
ready-to-merge
… lift functions to equivs (#6311) This removes: * `free_group.to_group.to_fun` and `free_group.to_group`, as these are both subsumed by the stronger `lift`. * `abelianization.hom_equiv` as this is now `abelianization.lift.symm` * `free_abelian_group.hom_equiv` as this is now `free_abelian_group.lift.symm`
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
… lift functions to equivs (#6311) This removes: * `free_group.to_group.to_fun` and `free_group.to_group`, as these are both subsumed by the stronger `lift`. * `abelianization.hom_equiv` as this is now `abelianization.lift.symm` * `free_abelian_group.hom_equiv` as this is now `free_abelian_group.lift.symm`
This removes:
free_group.to_group.to_funandfree_group.to_group, as these are both subsumed by the strongerlift.abelianization.hom_equivas this is nowabelianization.lift.symmfree_abelian_group.hom_equivas this is nowfree_abelian_group.lift.symm