docs(fermions): add Weyl and Dirac fermion API maps

Physlib/Relativity/Fermions/Dirac/API-map.yaml

@@ -0,0 +1,91 @@
+version: v0.1
+
+Title: "Dirac Fermions"
+
+Overview: |
+  A Dirac fermion is the four-component spinor built from a left-handed Weyl
+  fermion together with a dual right-handed one. The key data structure is the
+  structure `Dirac`, which carries a module structure over ℂ, the chiral basis
+  indexed by `Fin 4`, and the representation of SL(2, ℂ) induced from the two
+  Weyl factors. Alongside it sit the gamma matrices in the Dirac
+  representation, which generate the Dirac algebra and realize it as a
+  quotient of the Clifford algebra of the Minkowski quadratic form. Note that
+  the gamma matrices are written in the Dirac representation while `Dirac`
+  itself is presented in the chiral basis; the change of basis between the two
+  is not yet in the library, which is why the gamma action on `Dirac` is
+  recorded below as still to be built. Completing this API is what allows the
+  Dirac equation, the Dirac bilinears, and the fermionic terms of the Standard
+  Model Lagrangian to be stated.
+
+ParentAPIs:
+  - "Weyl Fermions (Physlib/Relativity/Fermions/Weyl)"
+  - "Lorentz Group (Physlib/Relativity/LorentzGroup)"
+
+References:
+  - "Dreiner, Haber and Martin, Two-component spinor techniques and Feynman rules for quantum field theory and supersymmetry, Phys. Rept. 494 (2010) 1-196. https://arxiv.org/abs/0812.1594 (Dirac fermions are treated on page 197 of the arXiv version)"
+
+Requirements:
+
+  - description: "The key data structure `Dirac` is defined, as a left-handed Weyl fermion together with a dual right-handed one."
+    done: true
+    location: Physlib/Relativity/Fermions/Dirac/Basic.lean (Dirac)
+
+  - description: "`Dirac` carries a module structure over ℂ, inherited from its two Weyl components."
+    done: true
+    location: Physlib/Relativity/Fermions/Dirac/Basic.lean (AddCommGroup Dirac, Module ℂ Dirac, left_add, dualRight_add, left_smul, dualRight_smul)
+
+  - description: "The decomposition of a Dirac fermion into its Weyl components is an equivalence, linear over ℂ."
+    done: true
+    location: Physlib/Relativity/Fermions/Dirac/Basic.lean (decomposeEquiv, decomposeLinEquiv)
+
+  - description: "The chiral basis of `Dirac` indexed by `Fin 4` is defined, and its elements are identified with the Weyl basis elements."
+    done: true
+    location: Physlib/Relativity/Fermions/Dirac/Basic.lean (chiralBasis, chiralBasis_cast_add, chiralBasis_nat_add)
+
+  - description: "`Dirac` carries a representation of SL(2, ℂ), acting componentwise on the two Weyl factors."
+    done: true
+    location: Physlib/Relativity/Fermions/Dirac/Basic.lean (rep, rep_apply_mk)
+
+  - description: "The representation on `Dirac` is equivalent to the product of the representations on its Weyl components."
+    done: true
+    location: Physlib/Relativity/Fermions/Dirac/Basic.lean (decomposeRepEquiv)
+
+  - description: "The gamma matrices in the Dirac representation are defined, together with the chirality matrix and the set they form."
+    done: true
+    location: Physlib/Relativity/CliffordAlgebra.lean (γ0, γ1, γ2, γ3, γ5, γ, γSet, γ_in_γSet)
+
+  - description: "The Dirac algebra generated over ℝ by the gamma matrices is defined, and contains each gamma matrix."
+    done: true
+    location: Physlib/Relativity/CliffordAlgebra.lean (diracAlgebra, γSet_subset_diracAlgebra, γ_in_diracAlgebra)
+
+  - description: "The Minkowski quadratic form is defined and the induced algebra map from its Clifford algebra onto the Dirac algebra is surjective."
+    done: true
+    location: Physlib/Relativity/CliffordAlgebra.lean (diracForm, ofCliffordAlgebra, ofCliffordAlgebra_ι_single, ofCliffordAlgebra_range_eq_top, ofCliffordAlgebra_surjective)
+
+  - description: "The API shall contain the isomorphism between the Clifford algebra of `diracForm` and `diracAlgebra` (blocked: needs injectivity of `ofCliffordAlgebra`, which requires dimension theory; recorded as a TODO in the source)."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the action of the gamma matrices on `Dirac` as linear maps (blocked: `γ0`--`γ3` are given in the Dirac representation while `chiralBasis` is the chiral basis, so this needs the change of basis between the two to be fixed first)."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the chiral projectors onto the left-handed and dual right-handed components, and their Lorentz equivariance."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the Dirac adjoint of a Dirac fermion."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the Dirac bilinears, and their transformation behaviour under the SL(2, ℂ) action."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the Dirac equation for a spinor field on spacetime."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the charge conjugate of a Dirac fermion, and the Majorana condition."
+    done: false
+    location: N/A

Physlib/Relativity/Fermions/Weyl/API-map.yaml

@@ -0,0 +1,95 @@
+version: v0.1
+
+Title: "Weyl Fermions"
+
+Overview: |
+  Weyl fermions are the two-component spinors carrying the fundamental
+  representations of SL(2, ℂ), the double cover of the restricted Lorentz group.
+  The API is built around four types: `LeftHandedWeyl` and `RightHandedWeyl`,
+  together with their duals `DualLeftHandedWeyl` and `DualRightHandedWeyl`.
+  Each carries a module structure over ℂ, a basis indexed by `Fin 2`, and a
+  representation of SL(2, ℂ). On top of these sit the invariant contractions,
+  the epsilon metrics raising and lowering spinor indices, the units realizing
+  the duality, and the identification of pairwise tensor products with
+  2 × 2 matrices. This API underlies the Dirac fermion API and the fermionic
+  sector of the Standard Model.
+
+ParentAPIs:
+  - "Lorentz Group (Physlib/Relativity/LorentzGroup)"
+
+References:
+  - "Dreiner, Haber and Martin, Two-component spinor techniques and Feynman rules for quantum field theory and supersymmetry, Phys. Rept. 494 (2010) 1-196. https://arxiv.org/abs/0812.1594"
+
+Requirements:
+
+  - description: "The key data structure `LeftHandedWeyl` is defined, with its module structure over ℂ."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/LeftHanded.lean (LeftHandedWeyl, AddCommMonoid LeftHandedWeyl, AddCommGroup LeftHandedWeyl, Module ℂ LeftHandedWeyl, toFin2ℂFun, toFin2ℂEquiv, toFin2ℂ)
+
+  - description: "The key data structure `RightHandedWeyl` is defined, with its module structure over ℂ."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/RightHanded.lean (RightHandedWeyl, AddCommMonoid RightHandedWeyl, AddCommGroup RightHandedWeyl, Module ℂ RightHandedWeyl, toFin2ℂFun, toFin2ℂEquiv, toFin2ℂ)
+
+  - description: "The dual data structures `DualLeftHandedWeyl` and `DualRightHandedWeyl` are defined, with their module structures over ℂ."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean (DualLeftHandedWeyl, AddCommGroup DualLeftHandedWeyl, Module ℂ DualLeftHandedWeyl, toFin2ℂEquiv); Physlib/Relativity/Fermions/Weyl/DualRightHanded.lean (DualRightHandedWeyl, AddCommGroup DualRightHandedWeyl, Module ℂ DualRightHandedWeyl, toFin2ℂEquiv)
+
+  - description: "Each Weyl type carries a basis indexed by `Fin 2`, and every element expands in it."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/LeftHanded.lean (basis, basis_apply, basis_val, eq_sum_basis); Physlib/Relativity/Fermions/Weyl/RightHanded.lean (basis, basis_apply, basis_val, eq_sum_basis); Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean (basis, basis_apply, basis_val, eq_sum_basis); Physlib/Relativity/Fermions/Weyl/DualRightHanded.lean (basis, basis_apply, basis_val, eq_sum_basis)
+
+  - description: "Each Weyl type carries a representation of SL(2, ℂ), with its matrix in the basis identified."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/LeftHanded.lean (rep, rep_apply, rep_toMatrix, rep_apply_basis, rep_apply_basis_repr); Physlib/Relativity/Fermions/Weyl/RightHanded.lean (rep, rep_apply, rep_toMatrix, rep_apply_basis, rep_apply_basis_repr); Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean (rep, rep_toMatrix, rep_apply_basis, rep_apply_basis_repr); Physlib/Relativity/Fermions/Weyl/DualRightHanded.lean (rep, rep_apply, rep_toMatrix, rep_apply_basis, rep_apply_basis_repr)
+
+  - description: "The invariant pairings between a Weyl type and its dual are defined as bilinear maps and as intertwining maps of representations."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/Contraction.lean (leftDualBi, dualLeftBi, rightDualBi, dualRightBi, leftDualContraction, dualLeftContraction, rightDualContraction, dualRightContraction)
+
+  - description: "The contractions are computed on basis elements and their symmetry under exchange is recorded."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/Contraction.lean (leftDualContraction_basis, dualLeftContraction_basis, rightDualContraction_basis, dualRightContraction_basis, leftDualContraction_tmul_symm, dualLeftContraction_tmul_symm, rightDualContraction_tmul_symm, dualRightContraction_tmul_symm)
+
+  - description: "The epsilon metrics on each Weyl type are defined as intertwining maps from the trivial representation, and expanded in the basis."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/Metric.lean (metricRaw, leftMetric, dualLeftMetric, rightMetric, dualRightMetric, leftMetricVal, dualLeftMetricVal, rightMetricVal, dualRightMetricVal, leftMetricVal_expand_tmul, dualLeftMetricVal_expand_tmul, rightMetricVal_expand_tmul, dualRightMetricVal_expand_tmul)
+
+  - description: "The interaction of the raw metric with SL(2, ℂ) is recorded, both directly and under the star operation."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/Metric.lean (comm_metricRaw, metricRaw_comm, star_comm_metricRaw, metricRaw_comm_star)
+
+  - description: "Contracting a metric against the corresponding contraction is computed."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/Metric.lean (leftDualContraction_apply_metric, dualLeftContraction_apply_metric, rightDualContraction_apply_metric, dualRightContraction_apply_metric)
+
+  - description: "The units realizing the duality between each Weyl type and its dual are defined, and their contraction with a spinor recovers the spinor."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/Unit.lean (leftDualLeftUnit, dualLeftLeftUnit, rightDualRightUnit, dualRightRightUnit, contr_dualLeftLeftUnit, contr_leftDualLeftUnit, contr_dualRightRightUnit, contr_rightDualRightUnit)
+
+  - description: "The symmetry of each unit under exchange of the two factors is recorded."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/Unit.lean (dualLeftLeftUnit_symm, leftDualLeftUnit_symm, dualRightRightUnit_symm, rightDualRightUnit_symm)
+
+  - description: "The dual of the left-handed Weyl representation is identified with the dual left-handed Weyl representation."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/Duals.lean (LeftHandedWeyl.dual, DualLeftHandedWeyl.dual, LeftHandedWeyl.dualEquiv, LeftHandedWeyl.dual_hom_apply, DualLeftHandedWeyl.dual_hom_apply)
+
+  - description: "Pairwise tensor products of Weyl types are identified with 2 x 2 complex matrices, equivariantly for the SL(2, ℂ) action."
+    done: true
+    location: Physlib/Relativity/Fermions/Weyl/Two.lean (leftLeftToMatrix, dualLeftdualLeftToMatrix, leftDualLeftToMatrix, dualLeftLeftToMatrix, rightRightToMatrix, dualRightDualRightToMatrix, rightDualRightToMatrix, dualRightRightToMatrix, dualLeftDualRightToMatrix, leftRightToMatrix, leftLeftToMatrix_ρ, dualLeftdualLeftToMatrix_ρ, leftDualLeftToMatrix_ρ, dualLeftLeftToMatrix_ρ, rightRightToMatrix_ρ, dualRightDualRightToMatrix_ρ, rightDualRightToMatrix_ρ, dualRightRightToMatrix_ρ, dualLeftDualRightToMatrix_ρ, leftRightToMatrix_ρ)
+
+  - description: "The API shall contain the equivalence between the right-handed Weyl representation and its dual, together with its SL(2, ℂ) equivariance (present only as `informal_definition RightHandedWeyl.dualEquiv` and `informal_lemma RightHandedWeyl.dualEquiv_equivariant` in `Duals.lean`)."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the identification of the right-handed Weyl representation with the complex conjugate of the left-handed one."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the Weyl equation for a massless spinor field."
+    done: false
+    location: N/A
+
+  - description: "The API shall contain the Majorana condition relating a left-handed Weyl fermion to a right-handed one."
+    done: false
+    location: N/A