feat: Add Quarks#1328
Conversation
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
nateabr
left a comment
nateabr
left a comment
There was a problem hiding this comment.
Overall everything looks great, just some comments on how we could make this approach standard for other particle fields.
I hope they help :)
| @[ext] | ||
| structure Quark where | ||
| /-- The underlying value of the quark field in the tensor product space. -/ | ||
| val : Fermion.LeftHandedWeyl ⊗[ℂ] EuclideanSpace ℂ (Fin 3) ⊗[ℂ] EuclideanSpace ℂ (Fin 2) |
There was a problem hiding this comment.
I'm assuming that we would add more fermions in successsive PR's, so would this being called Quark help with the naming?
Maybe LeftDoublet so if assume the namespace is Quark, the naming would be Quark.LeftDoublet ?
| one_smul := by intros; ext; simp [one_smul] | ||
| smul_zero := by intros; ext; simp [smul_zero] | ||
| zero_smul := by intros; ext; simp [zero_smul] | ||
|
|
There was a problem hiding this comment.
Regarding the above, would it be possible to define an equivalence between the Quark and its tensor product space? Something like valEquiv : Quark ≃ WrappedSpace.
Im thinking since the tensor product space already carries the necessary group and module structures, we can use Equiv.addCommGroup valEquiv and Equiv.module ℂ valEquiv to derive the group/module instances automatically.
This would then allow the valLinEquiv to be to be written with rfl proofs, maybe this approach might generalize when adding the other fermions.
| map_mul' := by intros; simp [map_mul]; rfl | ||
|
|
||
| /-! | ||
|
|
There was a problem hiding this comment.
Maybe we could define repLorentzGroup with valLineEquiv , such that it can match the style of repGuageGroup .
|
awaiting-author |
github-actions
Bot
added
the
awaiting-author
|
t-particles |
2 participants
Adding quarks to ./StandardModel, defining their representation under the Lorentz group and under the gauge group.