[Merged by Bors] - feat: some basic quaternion facts #7119
Conversation
ericrbg
commented
Sep 12, 2023
ericrbg
commented
ericrbg
added
awaiting-review
Mathlib/Algebra/Quaternion.lean
Outdated
| @@ -102,6 +102,10 @@ theorem mk.eta {R : Type*} {c₁ c₂} (a : ℍ[R,c₁,c₂]) : mk a.1 a.2 a.3 a | |||
|
|
|||
| variable {S T R : Type*} [CommRing R] {c₁ c₂ : R} (r x y z : R) (a b c : ℍ[R,c₁,c₂]) | |||
|
|
|||
| instance : Nonempty ℍ[R, c₁, c₂] := ⟨⟨c₁,c₁,c₁,c₁⟩⟩ | |||
There was a problem hiding this comment.
| instance : Nonempty ℍ[R, c₁, c₂] := ⟨⟨c₁,c₁,c₁,c₁⟩⟩ | |
| instance : Inhabited ℍ[R, c₁, c₂] := ⟨0⟩ |
would be more canonical
There was a problem hiding this comment.
Oh, I just noticed I accidentally put a Ring in there. I wanted to make them general, so that TC has to do less searching.
There was a problem hiding this comment.
I think TC is fast enough when it comes to finding a zero element.
There was a problem hiding this comment.
this Inhabited instance already exists further down the file, L189. Should I just delete this?
There was a problem hiding this comment.
Deleting it sounds good to me.
Mathlib/Algebra/Quaternion.lean
Outdated
| /-- There is a natural equivalence when swapping the coefficients of a quaternion algebra. -/ | ||
| def swapEquiv : ℍ[R,c₁,c₂] ≃ₐ[R] ℍ[R, c₂, c₁] where |
There was a problem hiding this comment.
In the context of ℍ, this doesn't seem natural at all; it treats i and j specially, without swapping the others!
I suppose this is natural for ℍ[R,c₁,c₂], though I believe it is still available as dot notation on Quaternion.
There was a problem hiding this comment.
I mean, technically it turns ij into ji = -ij in that special case, I think. Did I mess up the namespacing?
There was a problem hiding this comment.
No, but Quaternion := QuaternionAlgebra _ _ _ so dot notation naturally falls back on this definition.
There was a problem hiding this comment.
I didn't know dot notation could see through defs. Not sure what's best to do in this case. This is obviously not the standard involution...
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Mathlib/Algebra/Quaternion.lean
Outdated
| @@ -102,6 +102,10 @@ theorem mk.eta {R : Type*} {c₁ c₂} (a : ℍ[R,c₁,c₂]) : mk a.1 a.2 a.3 a | |||
|
|
|||
| variable {S T R : Type*} [CommRing R] {c₁ c₂ : R} (r x y z : R) (a b c : ℍ[R,c₁,c₂]) | |||
|
|
|||
| instance : Nonempty ℍ[R, c₁, c₂] := ⟨⟨c₁,c₁,c₁,c₁⟩⟩ | |||
There was a problem hiding this comment.
I think TC is fast enough when it comes to finding a zero element.
jcommelin
added
awaiting-author
ericrbg
added
awaiting-review
| instance [Subsingleton R] : Subsingleton ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).subsingleton | ||
| instance [Nontrivial R] : Nontrivial ℍ[R, c₁, c₂] := (equivTuple c₁ c₂).surjective.nontrivial |
There was a problem hiding this comment.
Do we have these instances for Quaternion? If not, can you add them?
|
✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
bors r+ |
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
|
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
