New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(Algebra/DualNumber): generalize the universal property to non-commutative rings #7934
Conversation
…n-commutative rings
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
This PR/issue depends on:
|
Mathlib/Algebra/DualNumber.lean
Outdated
theorem algHom_ext {A} [CommSemiring R] [Semiring A] [Algebra R A] ⦃f g : R[ε] →ₐ[R] A⦄ | ||
(h : f ε = g ε) : f = g := | ||
algHom_ext' <| LinearMap.ext_ring <| h | ||
theorem algHom_ext {A} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think there is value in keeping the old version of ext. It is a special case, but the side conditions are a lot simpler.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That seems fair, I've added it back. Ideally it would follow from ext <;> simp [*]
, but apparently some results needed to make that work are in un-imported files.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, it now works with a similar proof!
variable {A : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] | ||
|
||
/-- For two `R`-algebra morphisms out of `A[ε]` to agree, it suffices for them to agree on the | ||
elements of `A` and the `A`-multiples of `ε`. -/ | ||
@[ext 1100] | ||
nonrec theorem algHom_ext' ⦃f g : A[ε] →ₐ[R] B⦄ | ||
(hinl : f.comp (inlAlgHom _ _ _) = g.comp (inlAlgHom _ _ _)) | ||
(hinr : f.toLinearMap ∘ₗ (LinearMap.toSpanSingleton A A[ε] ε).restrictScalars R = | ||
g.toLinearMap ∘ₗ (LinearMap.toSpanSingleton A A[ε] ε).restrictScalars R) : | ||
f = g := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry, I'm failing to understand what you generalised. What was assumed commutative before which is not anymore?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The generalization is from R[ε] →ₐ[R] B
to A[ε] →ₐ[R] B
, where A
is not commutative
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Added to the PR description
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah I see
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good!
maintainer merge
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by eric-wieser. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
…n-commutative rings (#7934) The current universal properties of `TrivSqZeroExt` and `DualNumber` work only when the underlying ring is commutative. This is not the case for things like the dual quaternions. This generalizes both sets of results to the non-commutative case. Unfortunately the new `TrivSqZeroExt` version is rather involved, so this keeps the old statement as a special case. The new `DualNumber` version is less bad, so I just discarded the commutative special case. For dual numbers, the generalization is from `R[ε] →ₐ[R] B` to `A[ε] →ₐ[R] B`, where `R` is commutative but `A` may not be. Some variable names had to be shuffled to make the new statement look nice.
Build failed: |
bors merge |
…n-commutative rings (#7934) The current universal properties of `TrivSqZeroExt` and `DualNumber` work only when the underlying ring is commutative. This is not the case for things like the dual quaternions. This generalizes both sets of results to the non-commutative case. Unfortunately the new `TrivSqZeroExt` version is rather involved, so this keeps the old statement as a special case. The new `DualNumber` version is less bad, so I just discarded the commutative special case. For dual numbers, the generalization is from `R[ε] →ₐ[R] B` to `A[ε] →ₐ[R] B`, where `R` is commutative but `A` may not be. Some variable names had to be shuffled to make the new statement look nice.
…n-commutative rings (#7934) The current universal properties of `TrivSqZeroExt` and `DualNumber` work only when the underlying ring is commutative. This is not the case for things like the dual quaternions. This generalizes both sets of results to the non-commutative case. Unfortunately the new `TrivSqZeroExt` version is rather involved, so this keeps the old statement as a special case. The new `DualNumber` version is less bad, so I just discarded the commutative special case. For dual numbers, the generalization is from `R[ε] →ₐ[R] B` to `A[ε] →ₐ[R] B`, where `R` is commutative but `A` may not be. Some variable names had to be shuffled to make the new statement look nice.
Pull request successfully merged into master. Build succeeded: |
…n-commutative rings (#7934) The current universal properties of `TrivSqZeroExt` and `DualNumber` work only when the underlying ring is commutative. This is not the case for things like the dual quaternions. This generalizes both sets of results to the non-commutative case. Unfortunately the new `TrivSqZeroExt` version is rather involved, so this keeps the old statement as a special case. The new `DualNumber` version is less bad, so I just discarded the commutative special case. For dual numbers, the generalization is from `R[ε] →ₐ[R] B` to `A[ε] →ₐ[R] B`, where `R` is commutative but `A` may not be. Some variable names had to be shuffled to make the new statement look nice.
…n-commutative rings (#7934) The current universal properties of `TrivSqZeroExt` and `DualNumber` work only when the underlying ring is commutative. This is not the case for things like the dual quaternions. This generalizes both sets of results to the non-commutative case. Unfortunately the new `TrivSqZeroExt` version is rather involved, so this keeps the old statement as a special case. The new `DualNumber` version is less bad, so I just discarded the commutative special case. For dual numbers, the generalization is from `R[ε] →ₐ[R] B` to `A[ε] →ₐ[R] B`, where `R` is commutative but `A` may not be. Some variable names had to be shuffled to make the new statement look nice.
The current universal properties of
TrivSqZeroExt
andDualNumber
work only when the underlying ring is commutative.This is not the case for things like the dual quaternions.
This generalizes both sets of results to the non-commutative case.
Unfortunately the new
TrivSqZeroExt
version is rather involved, so this keeps the old statement as a special case.The new
DualNumber
version is less bad, so I just discarded the commutative special case.For dual numbers, the generalization is from
R[ε] →ₐ[R] B
toA[ε] →ₐ[R] B
, whereR
is commutative butA
may not be.Some variable names had to be shuffled to make the new statement look nice.
ε
commutes #7928