pullback vs pushforward

Stream: new members

[Damiano Testa]

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]

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

[Adam Topaz]

And pullback certainly makes sense for the injective case.

[Adam Topaz]

(note both docstrings say "injective")

[Damiano Testa]

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

[Damiano Testa]

PR #6487