mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Feat(LinearAlgebra/TensorProduct/RightExactness): Tensoring with a quotient of the ring

Open Shamrock-Frost opened this issue 1 year ago • 1 comments

Informally we show (R⧸I) ⊗ M = M/IM.

  • [ ] depends on: #13119

If someone can golf away this dependency I'd be happy! The existing proof that Submodule.map (TensorProduct.lid R M) (range (rTensor M (Submodule.subtype I))) = I • ⊤ isn't great.

Open in Gitpod

Shamrock-Frost avatar May 22 '24 22:05 Shamrock-Frost

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#13119~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar May 23 '24 04:05 leanprover-community-mathlib4-bot

Also can you provide _ ∘ₗ TensorProduct.mk R _ M 1 = Submodule.mkQ _? Just found out that I needed them :D

erdOne avatar May 23 '24 06:05 erdOne

Also can you provide _ ∘ₗ TensorProduct.mk R _ M 1 = Submodule.mkQ _? Just found out that I needed them :D

I'm not sure what you have in mind exactly. I added four new lemmas in terms of composition of linear maps, do any of them fit your use case?

Edit: Oh I see, you want (LinearEquiv.toLinearMap_symm_comp_eq _ _).mp (quotTensorEquivQuotSMul_symm_comp_mkQ I). I'll add a lemma for that

Shamrock-Frost avatar May 23 '24 18:05 Shamrock-Frost

Thanks a lot! maintainer merge

erdOne avatar May 23 '24 19:05 erdOne

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

github-actions[bot] avatar May 23 '24 19:05 github-actions[bot]

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 24 '24 04:05 mathlib-bors[bot]