From b4333f038aff74ea55e698cdaae06190f3353bdb Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 10 Feb 2025 10:59:09 +0000 Subject: [PATCH] refactor: More spellings --- HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean | 4 ++-- HepLean/Lorentz/MinkowskiMatrix.lean | 2 +- HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean | 2 +- HepLean/Lorentz/RealVector/Basic.lean | 2 +- HepLean/Lorentz/RealVector/Modules.lean | 2 +- HepLean/Mathematics/List.lean | 2 +- HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean | 6 +++--- .../FieldOpAlgebra/NormalOrder/Lemmas.lean | 6 +++--- .../FieldOpAlgebra/SuperCommute.lean | 6 +++--- .../FieldOpFreeAlgebra/SuperCommute.lean | 10 +++++----- 10 files changed, 21 insertions(+), 21 deletions(-) diff --git a/HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean b/HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean index cbbf5a4..fc2f828 100644 --- a/HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean +++ b/HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean @@ -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))) <| diff --git a/HepLean/Lorentz/MinkowskiMatrix.lean b/HepLean/Lorentz/MinkowskiMatrix.lean index 24fea36..fbc57ae 100644 --- a/HepLean/Lorentz/MinkowskiMatrix.lean +++ b/HepLean/Lorentz/MinkowskiMatrix.lean @@ -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] diff --git a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean index 2028b8c..acf5c9d 100644 --- a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean +++ b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean @@ -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 diff --git a/HepLean/Lorentz/RealVector/Basic.lean b/HepLean/Lorentz/RealVector/Basic.lean index efc3717..3ab80f1 100644 --- a/HepLean/Lorentz/RealVector/Basic.lean +++ b/HepLean/Lorentz/RealVector/Basic.lean @@ -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) diff --git a/HepLean/Lorentz/RealVector/Modules.lean b/HepLean/Lorentz/RealVector/Modules.lean index bc38c7c..b78c999 100644 --- a/HepLean/Lorentz/RealVector/Modules.lean +++ b/HepLean/Lorentz/RealVector/Modules.lean @@ -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] diff --git a/HepLean/Mathematics/List.lean b/HepLean/Mathematics/List.lean index b4cd91c..6cfa02c 100644 --- a/HepLean/Mathematics/List.lean +++ b/HepLean/Mathematics/List.lean @@ -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 diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean index a4bd1ef..7779877 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean @@ -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 diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean index 97ac79d..e1e3f04 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean @@ -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 φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`. diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean index f37ea26..cce56cd 100644 --- a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean @@ -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. -/ diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean index ba365d2..77046ea 100644 --- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean @@ -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. -/