PR summary 0a63c1305f

Declarations diff

+ _root_.LinearMap.exists_rightInverse_of_surjective
- LinearMap.exists_rightInverse_of_surjective

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

I think this doesn't actually change that much in terms of the imports added in #17452 : the previous imports of Topology.MetricSpace.Algebra just happened to be very low in terms of algebra (e.g before tensor products). But maybe this just suggests that we shouldn't be scared of importing more algebra since it is still basic algebra.

But I think this change is good in itself, and we can do better by stating it for Module.Projective (the file about projective modules is at distance 1 from Mathlib.LinearAlgebra.FreeModule.Basic, all other imports are useless, so that doesn't sound like import creep) : it is just a special case of Module.projective_lifting_property.

At some point we should be able to do the same for LinearMap.exists_leftInverse_of_injective (in injective modules), but we don't seem to have the Free -> Injective instance so it's not useful for now. This is nonsense.

I'm not sure my explanations are clear, feel free to tell me if not 😅

The changes in this PR look sensible to me, but the proposed generalisation to projective modules also does. Let me label it awaiting-author accordingly.
awaiting-author

Module.projective_lifting_property is more general than this, right?

Yes, that's what I alluded to above. But I still think we should have a name for this special case which does not mention "projective", because some people will be looking for it without knowing what a projective module is.

At some point we should be able to do the same for LinearMap.exists_leftInverse_of_injective (in injective modules), but we don't seem to have the Free -> Injective instance so it's not useful for now.

Free modules are usually very far from being injective, and I don't think LinearMap.exists_leftInverse_of_injective hold for the injection from the Z-module Z into Q, for example. (Q is an injective Z-module but Z is not.)

At some point we should be able to do the same for LinearMap.exists_leftInverse_of_injective (in injective modules), but we don't seem to have the Free -> Injective instance so it's not useful for now.

Free modules are usually very far from being injective, and I don't think LinearMap.exists_leftInverse_of_injective hold for the injection from the Z-module Z into Q, for example. (Q is an injective Z-module but Z is not.)

Of course you're right, this was nonsense. But LinearMap.exists_leftInverse_of_injective should still generalize to the case where V is an injective module, right? So really the main thing is that it doesn't hold for free modules because they are not necessarily injective? Or am I saying nonsense again?

But LinearMap.exists_leftInverse_of_injective should still generalize to the case where V is an injective module, right? So really the main thing is that it doesn't hold for free modules because they are not necessarily injective?

Yeah, a injective linear map has a left inverse if the domain is injective, which is a direct application of Module.Injective.extension_property.

But LinearMap.exists_leftInverse_of_injective should still generalize to the case where V is an injective module, right?

Mathlib has no instance for Module.Injective, so I haven't made this generalization.

Though I've split out #17747 to make it easier to attempt that refactor in future.

maintainer merge

🚀 Pull request has been placed on the maintainer queue by alreadydone.

Thanks! 🎉
bors merge

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build