Zulip Chat Archive

Stream: new members

Topic: pullback vs pushforward


Damiano Testa (Mar 01 2021 at 04:00):

Dear All,

I am just reading the docs#function.injective.semiring and docs#function.surjective.semiring in algebra/ring/basic and the docstrings say "Pullback" in both cases. If I were to call these, I would probably call the second one a "push-forward", instead of a "pull-back", since you deduce something about the target of a map from the source. I am happy to PR the change in the doc-string, but I first wanted to make sure that this is also the mathlib convention!

Adam Topaz (Mar 01 2021 at 04:04):

Re docs#function.surjective.semiring it looks like the docstring was just copied from docs#function.injective.semiring

Adam Topaz (Mar 01 2021 at 04:05):

And pullback certainly makes sense for the injective case.

Adam Topaz (Mar 01 2021 at 04:05):

(note both docstrings say "injective")

Damiano Testa (Mar 01 2021 at 04:06):

Ah, I had stopped at pull-back, since I was confused by this, but I can also change the injective part!

Damiano Testa (Mar 01 2021 at 04:11):

PR #6487


Last updated: Dec 20 2023 at 11:08 UTC