feat(linear_algebra/tensor_product): Generalise tensor product to non-commutative rings #10345
Conversation
github-actions
bot
added
the
merge-conflict
javra
force-pushed
the
noncomm_tensor_product
branch
from
3102dc0
to
45abc0a
Compare
github-actions
bot
removed
the
merge-conflict
github-actions
bot
added
the
merge-conflict
| /- | ||
| Copyright (c) 2021 Jakob von Raumer. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Jakob von Raumer, Eric Wieser | ||
| -/ | ||
| import algebra.opposites | ||
| import group_theory.group_action.defs | ||
| import group_theory.group_action.prod | ||
| import algebra.direct_sum.basic | ||
|
|
||
| /-! | ||
| # Symmetric group actions | ||
|
|
||
| This file defines a class of group actions which are invariant unter taking the `opposite` of | ||
| the operating type/(semi)group/monoid. | ||
|
|
||
| The main definition is the one of the typeclass `is_symmetric_smul` which states that for a | ||
| pair of types `R` and `M`, the actions of `R` and its opposite `Rᵐᵒᵖ` on `M` coincide. | ||
|
|
||
| We then provide the alternate version of its constructor, `unop_smul_eq_smul` about general | ||
| instance of `Rᵐᵒᵖ` and several instances for closure properties. | ||
|
|
||
| ## Tags | ||
|
|
||
| group action | ||
| -/ |
There was a problem hiding this comment.
Note that #10543 ended up calling this is_central_scalar instead, and distributed some of the defs in this file to other places. Some of the lemmas in this file did not make it into that PR (units.is_symmetric_smul can't be stated without other instances that are new in this PR, for instance), so it's not quite as easy as deleting this file. Hopefully simply replacing is_symmetric_smul with is_central_scalar will do most of the work, and then lean will tell you which definitions are duplicates.
github-actions
bot
removed
the
merge-conflict
…distribute the lemmas to other files?)
|
|
||
| -- TODO there might be a more general version of this | ||
| instance smul_comm_class.of_is_central_scalar {R α} [has_scalar R α] [has_scalar Rᵐᵒᵖ α] | ||
| [is_central_scalar R α] [smul_comm_class R R α] : smul_comm_class Rᵐᵒᵖ R α := |
There was a problem hiding this comment.
I would guess the generalization is
| [is_central_scalar R α] [smul_comm_class R R α] : smul_comm_class Rᵐᵒᵖ R α := | |
| [is_central_scalar R α] [smul_comm_class R S α] : smul_comm_class Rᵐᵒᵖ S α := |
or similar
| instance mul_action.of_is_central_scalar {R α} [comm_monoid R] [mul_action R α] [has_scalar Rᵐᵒᵖ α] | ||
| [is_central_scalar R α] : mul_action Rᵐᵒᵖ α := | ||
| ⟨λ a, by rw [←op_one, op_smul_eq_smul (1 : R) a, one_smul], | ||
| λ r s a, by rw [mul_comm, ←op_unop (s * r), op_smul_eq_smul, unop_mul, mul_smul, | ||
| unop_smul_eq_smul, unop_smul_eq_smul]⟩ |
There was a problem hiding this comment.
This instance looks dangerous to me, as it forms a loop.
There was a problem hiding this comment.
Does keeping it as a def and letI :=ing it seem like a good option?
There was a problem hiding this comment.
That would cease to be dangerous, but I suspect in review I will tell you to replace each of those letIs with something better. Feel free to add them anyway though if it unblocks you.
There was a problem hiding this comment.
Looking forward to seeing how you'd solve it 😃
github-actions
bot
added
the
merge-conflict
semorrison
added
the
too-late
Replaces
linear_algebra.tensor_productby a whole folder of files, generalising it to non-commutative rings and isolating everything that depends on the left action on the tensor product. A file containing the corresponding right action can be added in future.Still quite a lot of work to do, I haven't fixed any of the files importing
linear_algebra.tensor_productand we will likely need to create or presume instances foris_symmetric_smulin some cases.