refactor: More spellings
This commit is contained in:
jstoobysmith
parent
dc5b63c4a7
commit
b4333f038a
10 changed files with 21 additions and 21 deletions
|
|
@ -61,7 +61,7 @@ lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor =
|
|||
(smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 3))))).tensor :=
|
||||
coMetric_basis_expand
|
||||
|
||||
/-- The expansion of the Lorentz contrvariant metric in terms of basis vectors. -/
|
||||
/-- The expansion of the Lorentz contravariant metric in terms of basis vectors. -/
|
||||
lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor =
|
||||
basisVector ![Color.up, Color.up] (fun _ => 0)
|
||||
- basisVector ![Color.up, Color.up] (fun _ => 1)
|
||||
|
|
@ -87,7 +87,7 @@ lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor =
|
|||
simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
|
||||
rfl
|
||||
|
||||
/-- The expansion of the Lorentz contrvariant metric in terms of basis vectors as
|
||||
/-- The expansion of the Lorentz contravariant metric in terms of basis vectors as
|
||||
a structured tensor tree. -/
|
||||
lemma contrMatrix_basis_expand_tree : {η | μ ν}ᵀ.tensor =
|
||||
(TensorTree.add (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 0))) <|
|
||||
|
|
|
|||
|
|
@ -118,7 +118,7 @@ def dual : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := η * Λᵀ * η
|
|||
lemma dual_id : @dual d 1 = 1 := by
|
||||
simpa only [dual, transpose_one, mul_one] using minkowskiMatrix.sq
|
||||
|
||||
/-- The Minkowski dual swaps multiplications (acts contrvariantly). -/
|
||||
/-- The Minkowski dual swaps multiplications (acts contravariantly). -/
|
||||
@[simp]
|
||||
lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by
|
||||
simp only [dual, transpose_mul]
|
||||
|
|
|
|||
|
|
@ -405,7 +405,7 @@ lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
|||
linear_combination (norm := ring_nf) -h0
|
||||
simp only [σSAL, Basis.mk_repr, Fin.isValue, sub_self]
|
||||
|
||||
/-- The relationship between the basis `σSA` of contrvariant Pauli-matrices and the basis
|
||||
/-- The relationship between the basis `σSA` of contravariant Pauli-matrices and the basis
|
||||
`σSAL` of covariant Pauli matrices is by multiplication by the Minkowski matrix. -/
|
||||
lemma σSA_minkowskiMetric_σSAL (i : Fin 1 ⊕ Fin 3) :
|
||||
σSA i = minkowskiMatrix i i • σSAL i := by
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ open minkowskiMatrix
|
|||
Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
|
||||
def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep
|
||||
|
||||
/-- The representation of contrvariant Lorentz vectors forms a topological space, induced
|
||||
/-- The representation of contravariant Lorentz vectors forms a topological space, induced
|
||||
by its equivalence to `Fin 1 ⊕ Fin d → ℝ`. -/
|
||||
instance : TopologicalSpace (Contr d) := TopologicalSpace.induced
|
||||
ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
|
||||
|
|
|
|||
|
|
@ -113,7 +113,7 @@ lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ =
|
|||
refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
|
||||
exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
|
||||
|
||||
/-- Decomposition of a contrvariant Lorentz vector into the standard basis. -/
|
||||
/-- Decomposition of a contravariant Lorentz vector into the standard basis. -/
|
||||
lemma stdBasis_decomp (v : ContrMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i := by
|
||||
apply toFin1dℝEquiv.injective
|
||||
simp only [map_sum, _root_.map_smul]
|
||||
|
|
|
|||
|
|
@ -755,7 +755,7 @@ lemma eraseIdx_insertionSort_fin {I : Type} (le1 : I → I → Prop) [DecidableR
|
|||
= List.insertionSort le1 (r.eraseIdx n) :=
|
||||
eraseIdx_insertionSort le1 n.val r (Fin.prop n)
|
||||
|
||||
/-- Given a list `i :: l` the left-most minimial position `a` of `i :: l` wrt `r`.
|
||||
/-- Given a list `i :: l` the left-most minimal position `a` of `i :: l` wrt `r`.
|
||||
That is the first position
|
||||
of `l` such that for every element `(i :: l)[b]` before that position
|
||||
`r ((i :: l)[b]) ((i :: l)[a])` is not true. The use of `i :: l` here
|
||||
|
|
|
|||
|
|
@ -19,8 +19,8 @@ open FieldStatistic
|
|||
|
||||
variable (𝓕 : FieldSpecification)
|
||||
|
||||
/-- The set contains the super-commutors equal to zero in the operator algebra.
|
||||
This contains e.g. the super-commutor of two creation operators. -/
|
||||
/-- The set contains the super-commutators equal to zero in the operator algebra.
|
||||
This contains e.g. the super-commutator of two creation operators. -/
|
||||
def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
|
||||
{ x |
|
||||
(∃ (φ1 φ2 φ3 : 𝓕.CrAnFieldOp),
|
||||
|
|
@ -42,7 +42,7 @@ def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
|
|||
This corresponds to the condition that two operators with different statistics always
|
||||
super-commute. In other words, fermions and bosons always super-commute.
|
||||
- `[ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛca]ₛca`. This corresponds to the condition,
|
||||
when combined with the conditions above, that the super-commutor is in the center of the
|
||||
when combined with the conditions above, that the super-commutator is in the center of the
|
||||
of the algebra.
|
||||
-/
|
||||
abbrev FieldOpAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotient
|
||||
|
|
|
|||
|
|
@ -229,8 +229,8 @@ The proof of this result ultimately goes as follows
|
|||
a `ofCrAnList φsn` where `φsn` is the normal ordering of `φ₀…φₙ`.
|
||||
- `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ`
|
||||
(considered as a list with one element) with
|
||||
`ofCrAnList φsn` as a sum of supercommutors, one for each element of `φsn`.
|
||||
- The fact that super-commutors are in the center of `𝓕.FieldOpAlgebra` is used to rearrange terms.
|
||||
`ofCrAnList φsn` as a sum of super commutators, one for each element of `φsn`.
|
||||
- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to rearrange terms.
|
||||
- Properties of ordered lists, and `normalOrderSign_eraseIdx` are then used to complete the proof.
|
||||
-/
|
||||
lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)
|
||||
|
|
@ -281,7 +281,7 @@ lemma ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum (φ : 𝓕.CrAnFieldOp
|
|||
rw [← Finset.sum_mul, ← map_sum, ← map_sum, ← ofFieldOp_eq_sum, ← ofFieldOpList_eq_sum]
|
||||
|
||||
/--
|
||||
The commutor of the annihilation part of a field operator with a normal ordered list of field
|
||||
The commutator of the annihilation part of a field operator with a normal ordered list of field
|
||||
operators can be decomposed into the sum of the commutators of the annihilation part with each
|
||||
element of the list of field operators, i.e.
|
||||
`[anPart φ, 𝓝(φ₀…φₙ)]ₛ= ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [anPart φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`.
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@ lemma ι_superCommuteF_eq_of_equiv_right (a b1 b2 : 𝓕.FieldOpFreeAlgebra) (h
|
|||
simp only [LinearMap.mem_ker, ← map_sub]
|
||||
exact ι_superCommuteF_right_zero_of_mem_ideal a (b1 - b2) h
|
||||
|
||||
/-- The super commutor on the `FieldOpAlgebra` defined as a linear map `[a,_]ₛ`. -/
|
||||
/-- The super commutator on the `FieldOpAlgebra` defined as a linear map `[a,_]ₛ`. -/
|
||||
noncomputable def superCommuteRight (a : 𝓕.FieldOpFreeAlgebra) :
|
||||
FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
|
||||
toFun := Quotient.lift (ι.toLinearMap ∘ₗ superCommuteF a)
|
||||
|
|
@ -367,7 +367,7 @@ lemma superCommute_anPart_ofFieldOp (φ φ' : 𝓕.FieldOp) :
|
|||
## Mul equal superCommute
|
||||
|
||||
Lemmas which rewrite a multiplication of two elements of the algebra as their commuted
|
||||
multiplication with a sign plus the super commutor.
|
||||
multiplication with a sign plus the super commutator.
|
||||
|
||||
-/
|
||||
|
||||
|
|
@ -446,7 +446,7 @@ lemma anPart_mul_anPart_swap (φ φ' : 𝓕.FieldOp) :
|
|||
|
||||
/-!
|
||||
|
||||
## Symmetry of the super commutor.
|
||||
## Symmetry of the super commutator.
|
||||
|
||||
-/
|
||||
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ namespace FieldOpFreeAlgebra
|
|||
|
||||
/-!
|
||||
|
||||
## The super commutor on the FieldOpFreeAlgebra.
|
||||
## The super commutator on the FieldOpFreeAlgebra.
|
||||
|
||||
-/
|
||||
|
||||
|
|
@ -40,7 +40,7 @@ scoped[FieldSpecification.FieldOpFreeAlgebra] notation "[" φs "," φs' "]ₛca"
|
|||
|
||||
/-!
|
||||
|
||||
## The super commutor of different types of elements
|
||||
## The super commutator of different types of elements
|
||||
|
||||
-/
|
||||
|
||||
|
|
@ -257,7 +257,7 @@ lemma superCommuteF_anPartF_ofFieldOpF (φ φ' : 𝓕.FieldOp) :
|
|||
## Mul equal superCommuteF
|
||||
|
||||
Lemmas which rewrite a multiplication of two elements of the algebra as their commuted
|
||||
multiplication with a sign plus the super commutor.
|
||||
multiplication with a sign plus the super commutator.
|
||||
|
||||
-/
|
||||
lemma ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF (φs φs' : List 𝓕.CrAnFieldOp) :
|
||||
|
|
@ -328,7 +328,7 @@ lemma ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF (φs : List 𝓕.CrAnField
|
|||
|
||||
/-!
|
||||
|
||||
## Symmetry of the super commutor.
|
||||
## Symmetry of the super commutator.
|
||||
|
||||
-/
|
||||
|
||||
|
|
@ -359,7 +359,7 @@ lemma superCommuteF_ofCrAnOpF_ofCrAnOpF_symm (φ φ' : 𝓕.CrAnFieldOp) :
|
|||
|
||||
/-!
|
||||
|
||||
## Splitting the super commutor on lists into sums.
|
||||
## Splitting the super commutator on lists into sums.
|
||||
|
||||
-/
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue