Commit 2026-05-04 13:04 7925e51c

View on Github →

feat(Topology/Algebra/Module): bundle Submodule.mkQ as a continuous linear map (#38811) This PR adds Submodule.mkQL, the bundled continuous linear map version of Submodule.mkQ, paralleling the existing Submodule.subtypeL for Submodule.subtype. Two related lemmas are also added: Submodule.continuous_mkQ records that Submodule.mkQ is continuous, and Submodule.isQuotientMap_mkQL records that the bundled map is a quotient map.

Estimated changes

Modified Mathlib/Topology/Algebra/Module/Basic.lean

added theorem Submodule.continuous_mkQ

added theorem Submodule.isQuotientMap_mkQ

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

added theorem Submodule.coe_mkQL

added theorem Submodule.isOpenQuotientMap_mkQL

added theorem Submodule.isQuotientMap_mkQL

added def Submodule.mkQL

added theorem Submodule.mkQL_apply

added theorem Submodule.toLinearMap_mkQL