[Merged by Bors] - feat(linear_algebra/trace): trace of prod_map #13872
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
antoinelab01
added
awaiting-review
antoinelab01
changed the title
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
antoinelab01
added
the
awaiting-CI
github-actions
bot
removed
the
awaiting-CI
|
Can you please add a description of the results in this PR? Thanks! |
| { simp only [dual_tensor_hom_equiv, tensor_product.algebra_tensor_module.curry_apply, | ||
| to_fun_eq_coe, tensor_product.curry_apply, coe_restrict_scalars_eq_coe, coe_comp, | ||
| linear_equiv.coe_to_linear_map, coe_inl, function.comp_app, linear_equiv.prod_apply, | ||
| dual_tensor_hom_equiv_of_basis_apply, map_zero, prod_map_apply, coprod_apply, id_coe, id.def, | ||
| add_zero, prod_map_linear_apply, dual_tensor_hom_prod_map_zero, trace_eq_contract_apply, | ||
| contract_left_apply, fst_apply] }, | ||
| { simp only [dual_tensor_hom_equiv, tensor_product.algebra_tensor_module.curry_apply, | ||
| to_fun_eq_coe, tensor_product.curry_apply, coe_restrict_scalars_eq_coe, coe_comp, | ||
| linear_equiv.coe_to_linear_map, coe_inr, function.comp_app, linear_equiv.prod_apply, | ||
| dual_tensor_hom_equiv_of_basis_apply, map_zero, prod_map_apply, coprod_apply, id_coe, id.def, | ||
| zero_add, prod_map_linear_apply, zero_prod_map_dual_tensor_hom, trace_eq_contract_apply, | ||
| contract_left_apply, snd_apply], }, |
There was a problem hiding this comment.
If you added @[simp] to dual_tensor_hom_prod_map_zero and zero_prod_map_dual_tensor_hom (seems reasonable?), then this could just be ext; simp.
I wouldn't insist on this, however.
(I think unnecessarily squeezing simps can obfuscate proofs: it's hard to tell by looking at a big simp only if it is only there to speed things up, or there is real work happening.)
There was a problem hiding this comment.
Sounds fair. I was unsure for these kinds of proofs whether to prioritize conciseness with simp or speed with simp only. Since the difference in loading time was significant I chose simp only but I can totally change to simp if you believe that's a better practice.
There was a problem hiding this comment.
Hm, I did the change and even though it works locally now CI fails at build mathlib with a deterministic timeout... Maybe we don't really have the choice to use simp only here
There was a problem hiding this comment.
Sadness. Lean 3 is running out of steam.
|
bors merge |
github-actions
bot
added
ready-to-merge
|
Canceled. |
|
Can you please merge master and see if it works? |
Done. I think that someone needs to call "bors merge" again. |
|
bors merge |
In this PR I prove that the trace is additive under `prod_map`, i.e. that `trace (prod_map f g) = trace f + trace g`. Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This is proved under the `field` assumption instead of the finite free module assumptions generally used to talk about the trace because we need the submodules `p` and `f.ker` to also be free and finite. - [x] depends on: #13872 Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
In this PR I prove that the trace is additive under
prod_map, i.e. thattrace (prod_map f g) = trace f + trace g.