[Merged by Bors] - feat(RingTheory/TensorProduct): heterogenize#6417
[Merged by Bors] - feat(RingTheory/TensorProduct): heterogenize#6417eric-wieser wants to merge 8 commits intomasterfrom
Conversation
3ef7201 to
367508b
Compare
| theorem rid_tmul (r : R) (a : A) : (TensorProduct.rid R A : A ⊗ R → A) (a ⊗ₜ r) = r • a := by | ||
| simp [TensorProduct.rid] | ||
| theorem rid_tmul (r : R) (a : A) : TensorProduct.rid R S A (a ⊗ₜ r) = a * algebraMap _ _ r := rfl |
There was a problem hiding this comment.
Is this change reasonable? Or was the old defeq better?
There was a problem hiding this comment.
I've pinged Kevin and Antoine on Zulip just to be safe; I'll probably merge tomorrow if they don't reply before then.
There was a problem hiding this comment.
I have a slight preference for the old version, but I can't bet it is reasonable.
According to my own programming habit, keepingr • a (smul) as long as possible is safer, and one can always rewrite it to multiplication using algebraMap_eq_smul.
There was a problem hiding this comment.
@AntoineChambert-Loir, note this is a * algebraMap _ _ r not algebraMap _ _ r * a; though admittedly that's only one more rewrite away.
There was a problem hiding this comment.
I've changed it to r • a
| apply AlgHom.restrictScalars_injective R | ||
| apply TensorProduct.ext | ||
| intro b a | ||
| have : b ⊗ₜ[R] a = b • (1 : B) ⊗ₜ a := by rw [TensorProduct.smul_tmul', smul_eq_mul, mul_one] | ||
| rw [this, AlgHom.restrictScalars_apply, AlgHom.restrictScalars_apply, map_smul, map_smul] | ||
| congr 1 | ||
| change | ||
| ((f₁.restrictScalars R).comp TensorProduct.includeRight) a = | ||
| ((f₂.restrictScalars R).comp TensorProduct.includeRight) a | ||
| congr 1 | ||
| refine' FormallyUnramified.ext I ⟨2, hI⟩ _ | ||
| intro x | ||
| exact AlgHom.congr_fun e (1 ⊗ₜ x) | ||
| ext : 1 | ||
| · exact Subsingleton.elim _ _ | ||
| · exact FormallyUnramified.ext I ⟨2, hI⟩ fun x => AlgHom.congr_fun e (1 ⊗ₜ x) |
There was a problem hiding this comment.
Only after writing Algebra.TensorProduct.ext did I find out that there was a duplicate implementation hiding here!
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Johan Commelin <johan@commelin.net>
|
bors merge |
This: * Improves the module docstring, which was both out of date and not very informative * Addresses a `TODO` to generalize `includeLeft` to commuting actions. As a result a few downstream results are changed to be about `includeLeftRingHom` or `a ⊗ₜ 1`, as carrying around the extra useless ring just makes the lemmas harder to use. Nothing seems to suffer from this change. * Introduces `TensorProduct.AlgebraTensorModule.rid` * Generalizes the following to work for towers of rings: * `Algebra.TensorProduct.algHomOfLinearMapTensorProduct` * `Algebra.TensorProduct.map` * `Algebra.TensorProduct.congr` * `Algebra.TensorProduct.endTensorEndAlgHom` * `Algebra.TensorProduct.ext` (and renames it to `Algebra.TensorProduct.ext'`) * `Algebra.TensorProduct.rid` * Introduces a new `Algebra.TensorProduct.ext` which follows "partially-applied ext lemmas", and uses it to golf a proof in `RingTheory/Etale.lean` I need many of these results for building `AlgEquiv`s relating to the base change of clifford algebras.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
This: * Improves the module docstring, which was both out of date and not very informative * Addresses a `TODO` to generalize `includeLeft` to commuting actions. As a result a few downstream results are changed to be about `includeLeftRingHom` or `a ⊗ₜ 1`, as carrying around the extra useless ring just makes the lemmas harder to use. Nothing seems to suffer from this change. * Introduces `TensorProduct.AlgebraTensorModule.rid` * Generalizes the following to work for towers of rings: * `Algebra.TensorProduct.algHomOfLinearMapTensorProduct` * `Algebra.TensorProduct.map` * `Algebra.TensorProduct.congr` * `Algebra.TensorProduct.endTensorEndAlgHom` * `Algebra.TensorProduct.ext` (and renames it to `Algebra.TensorProduct.ext'`) * `Algebra.TensorProduct.rid` * Introduces a new `Algebra.TensorProduct.ext` which follows "partially-applied ext lemmas", and uses it to golf a proof in `RingTheory/Etale.lean` I need many of these results for building `AlgEquiv`s relating to the base change of clifford algebras.
This:
TODOto generalizeincludeLeftto commuting actions. As a result a few downstream results are changed to be aboutincludeLeftRingHomora ⊗ₜ 1, as carrying around the extra useless ring just makes the lemmas harder to use. Nothing seems to suffer from this change.TensorProduct.AlgebraTensorModule.ridAlgebra.TensorProduct.algHomOfLinearMapTensorProductAlgebra.TensorProduct.mapAlgebra.TensorProduct.congrAlgebra.TensorProduct.endTensorEndAlgHomAlgebra.TensorProduct.ext(and renames it toAlgebra.TensorProduct.ext')Algebra.TensorProduct.ridAlgebra.TensorProduct.extwhich follows "partially-applied ext lemmas", and uses it to golf a proof inRingTheory/Etale.leanI need many of these results for building
AlgEquivs relating to the base change of clifford algebras.