[Merged by Bors] - refactor(RingTheory/TensorProduct): simplify assumptions #7403
Conversation
Rather than showing agreement on all the scalars, it suffices to show agreement on `1`.
eric-wieser
added
awaiting-review
| def algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[S] C) | ||
| (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) | ||
| (w₂ : ∀ r, f (algebraMap S A r ⊗ₜ[R] 1) = algebraMap S C r) : A ⊗[R] B →ₐ[S] C := | ||
| { f with | ||
| map_one' := by rw [← (algebraMap S C).map_one, ← w₂, (algebraMap S A).map_one]; rfl | ||
| map_zero' := by simp only; rw [LinearMap.toFun_eq_coe, map_zero] | ||
| map_mul' := fun x y => by | ||
| (map_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) | ||
| (map_one : f (1 ⊗ₜ[R] 1) = 1) : A ⊗[R] B →ₐ[S] C := | ||
| AlgHom.ofLinearMap f map_one fun x y => by |
There was a problem hiding this comment.
This is the main change of this PR, everything else is just fallout.
…fLinearMapTensorProduct
| (map_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) | ||
| (map_one : f (1 ⊗ₜ[R] 1) = 1) : A ⊗[R] B →ₐ[S] C := |
There was a problem hiding this comment.
I agree that w₁ and w₂ were terrible names, but I don't like map_mul and map_one either since they shadow the corresponding lemmas, and then it's confusing reading the source. Can we call them h_map_mul and h_map_one, or h_mul and h_one?
Also, can you fix the docstring? Is it supposed to say "from a nonzero map" or something to reflect the f 1 = 1 condition?
Aside: is there a reason not to just write f 1 = 1 in the hypothesis? I'm okay either way.
There was a problem hiding this comment.
Can we call them ...
Also, can you fix the docstring?
Done
Aside: is there a reason not to just write f 1 = 1 in the hypothesis? I'm okay either way.
Yes, I explained this in the new docstring
|
bors d+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
|
bors merge |
Rather than showing agreement on all the scalars in `algHomOfLinearMapTensorProduct`, it suffices to show agreement on `1`. This also replaces a few downstream proofs with `rfl` in order to make them eligible for `dsimp`. These results were always true by `rfl`, but it was easier to make this change than fix the old proofs.
|
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. |
bors
bot
changed the title
Rather than showing agreement on all the scalars in
algHomOfLinearMapTensorProduct, it suffices to show agreement on1.This also replaces a few downstream proofs with
rflin order to make them eligible fordsimp.These results were always true by
rfl, but it was easier to make this change than fix the old proofs.