feat: Properties of super commute
This commit is contained in:
jstoobysmith
parent
f7e669910c
commit
c18b4850e5
3 changed files with 357 additions and 13 deletions
|
|
@ -117,5 +117,312 @@ scoped[FieldSpecification.FieldOpAlgebra] notation "[" a "," b "]ₛ" => superCo
|
|||
lemma superCommute_eq_ι_superCommuteF (a b : 𝓕.CrAnAlgebra) :
|
||||
[ι a, ι b]ₛ = ι [a, b]ₛca := rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Properties of `superCommute`.
|
||||
|
||||
-/
|
||||
|
||||
/-!
|
||||
|
||||
## Properties from the definition of FieldOpAlgebra
|
||||
|
||||
-/
|
||||
|
||||
|
||||
lemma superCommute_create_create {φ φ' : 𝓕.CrAnStates}
|
||||
(h : 𝓕 |>ᶜ φ = .create) (h' : 𝓕 |>ᶜ φ' = .create) :
|
||||
[ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ = 0 := by
|
||||
rw [ofCrAnFieldOp, ofCrAnFieldOp]
|
||||
rw [superCommute_eq_ι_superCommuteF, ι_superCommuteF_of_create_create _ _ h h']
|
||||
|
||||
lemma superCommute_annihilate_annihilate {φ φ' : 𝓕.CrAnStates}
|
||||
(h : 𝓕 |>ᶜ φ = .annihilate) (h' : 𝓕 |>ᶜ φ' = .annihilate) :
|
||||
[ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ = 0 := by
|
||||
rw [ofCrAnFieldOp, ofCrAnFieldOp]
|
||||
rw [superCommute_eq_ι_superCommuteF, ι_superCommuteF_of_annihilate_annihilate _ _ h h']
|
||||
|
||||
lemma superCommute_diff_statistic {φ φ' : 𝓕.CrAnStates} (h : (𝓕 |>ₛ φ) ≠ 𝓕 |>ₛ φ') :
|
||||
[ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ = 0 := by
|
||||
rw [ofCrAnFieldOp, ofCrAnFieldOp]
|
||||
rw [superCommute_eq_ι_superCommuteF, ι_superCommuteF_of_diff_statistic h]
|
||||
|
||||
lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_mem_center (φ φ' : 𝓕.CrAnStates) :
|
||||
[ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ ∈ Subalgebra.center ℂ (FieldOpAlgebra 𝓕) := by
|
||||
rw [ofCrAnFieldOp, ofCrAnFieldOp, superCommute_eq_ι_superCommuteF]
|
||||
exact ι_superCommuteF_ofCrAnState_ofCrAnState_mem_center φ φ'
|
||||
|
||||
/-!
|
||||
|
||||
### `superCommute` on different constructors.
|
||||
|
||||
-/
|
||||
|
||||
lemma superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList (φs φs' : List 𝓕.CrAnStates) :
|
||||
[ofCrAnFieldOpList φs, ofCrAnFieldOpList φs']ₛ =
|
||||
ofCrAnFieldOpList (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnFieldOpList (φs' ++ φs) := by
|
||||
rw [ofCrAnFieldOpList_eq_ι_ofCrAnList, ofCrAnFieldOpList_eq_ι_ofCrAnList]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofCrAnList_ofCrAnList]
|
||||
rfl
|
||||
|
||||
lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp (φ φ' : 𝓕.CrAnStates) :
|
||||
[ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ = ofCrAnFieldOp φ * ofCrAnFieldOp φ' -
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofCrAnFieldOp φ' * ofCrAnFieldOp φ := by
|
||||
rw [ofCrAnFieldOp, ofCrAnFieldOp]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofCrAnState_ofCrAnState]
|
||||
rfl
|
||||
|
||||
lemma superCommute_ofCrAnFieldOpList_ofFieldOpList (φcas : List 𝓕.CrAnStates)
|
||||
(φs : List 𝓕.States) :
|
||||
[ofCrAnFieldOpList φcas, ofFieldOpList φs]ₛ = ofCrAnFieldOpList φcas * ofFieldOpList φs -
|
||||
𝓢(𝓕 |>ₛ φcas, 𝓕 |>ₛ φs) • ofFieldOpList φs * ofCrAnFieldOpList φcas := by
|
||||
rw [ofCrAnFieldOpList, ofFieldOpList]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofCrAnList_ofStatesList]
|
||||
rfl
|
||||
|
||||
lemma superCommute_ofFieldOpList_ofFieldOpList (φs φs' : List 𝓕.States) :
|
||||
[ofFieldOpList φs, ofFieldOpList φs']ₛ = ofFieldOpList φs * ofFieldOpList φs' -
|
||||
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofFieldOpList φs := by
|
||||
rw [ofFieldOpList, ofFieldOpList]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofStateList_ofStatesList]
|
||||
rfl
|
||||
|
||||
lemma superCommute_ofFieldOp_ofFieldOpList (φ : 𝓕.States) (φs : List 𝓕.States) :
|
||||
[ofFieldOp φ, ofFieldOpList φs]ₛ = ofFieldOp φ * ofFieldOpList φs -
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofFieldOpList φs * ofFieldOp φ := by
|
||||
rw [ofFieldOp, ofFieldOpList]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofState_ofStatesList]
|
||||
rfl
|
||||
|
||||
lemma superCommute_ofFieldOpList_ofFieldOp (φs : List 𝓕.States) (φ : 𝓕.States) :
|
||||
[ofFieldOpList φs, ofFieldOp φ]ₛ = ofFieldOpList φs * ofFieldOp φ -
|
||||
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) • ofFieldOp φ * ofFieldOpList φs := by
|
||||
rw [ofFieldOpList, ofFieldOp]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofStateList_ofState]
|
||||
rfl
|
||||
|
||||
lemma superCommute_anPart_crPart (φ φ' : 𝓕.States) :
|
||||
[anPart φ, crPart φ']ₛ = anPart φ * crPart φ' -
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart φ' * anPart φ := by
|
||||
rw [anPart, crPart]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_anPartF_crPartF]
|
||||
rfl
|
||||
|
||||
lemma superCommute_crPart_anPart (φ φ' : 𝓕.States) :
|
||||
[crPart φ, anPart φ']ₛ = crPart φ * anPart φ' -
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart φ' * crPart φ := by
|
||||
rw [anPart, crPart]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_crPartF_anPartF]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma superCommute_crPart_crPart (φ φ' : 𝓕.States) : [crPart φ, crPart φ']ₛ = 0 := by
|
||||
match φ, φ' with
|
||||
| States.outAsymp φ, _ =>
|
||||
simp
|
||||
| _, States.outAsymp φ =>
|
||||
simp
|
||||
| States.position φ, States.position φ' =>
|
||||
simp only [crPart_position]
|
||||
apply superCommute_create_create
|
||||
· rfl
|
||||
· rfl
|
||||
| States.position φ, States.inAsymp φ' =>
|
||||
simp only [crPart_position, crPart_negAsymp]
|
||||
apply superCommute_create_create
|
||||
· rfl
|
||||
· rfl
|
||||
| States.inAsymp φ, States.inAsymp φ' =>
|
||||
simp only [crPart_negAsymp]
|
||||
apply superCommute_create_create
|
||||
· rfl
|
||||
· rfl
|
||||
| States.inAsymp φ, States.position φ' =>
|
||||
simp only [crPart_negAsymp, crPart_position]
|
||||
apply superCommute_create_create
|
||||
· rfl
|
||||
· rfl
|
||||
|
||||
@[simp]
|
||||
lemma superCommute_anPart_anPart (φ φ' : 𝓕.States) : [anPart φ, anPart φ']ₛ = 0 := by
|
||||
match φ, φ' with
|
||||
| States.inAsymp φ, _ =>
|
||||
simp
|
||||
| _, States.inAsymp φ =>
|
||||
simp
|
||||
| States.position φ, States.position φ' =>
|
||||
simp only [anPart_position]
|
||||
apply superCommute_annihilate_annihilate
|
||||
· rfl
|
||||
· rfl
|
||||
| States.position φ, States.outAsymp φ' =>
|
||||
simp only [anPart_position, anPart_posAsymp]
|
||||
apply superCommute_annihilate_annihilate
|
||||
· rfl
|
||||
· rfl
|
||||
| States.outAsymp φ, States.outAsymp φ' =>
|
||||
simp only [anPart_posAsymp]
|
||||
apply superCommute_annihilate_annihilate
|
||||
· rfl
|
||||
· rfl
|
||||
| States.outAsymp φ, States.position φ' =>
|
||||
simp only [anPart_posAsymp, anPart_position]
|
||||
apply superCommute_annihilate_annihilate
|
||||
· rfl
|
||||
· rfl
|
||||
|
||||
lemma superCommute_crPart_ofFieldOpList (φ : 𝓕.States) (φs : List 𝓕.States) :
|
||||
[crPart φ, ofFieldOpList φs]ₛ = crPart φ * ofFieldOpList φs -
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofFieldOpList φs * crPart φ := by
|
||||
rw [crPart, ofFieldOpList]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_crPartF_ofStateList]
|
||||
rfl
|
||||
|
||||
lemma superCommute_anPart_ofFieldOpList (φ : 𝓕.States) (φs : List 𝓕.States) :
|
||||
[anPart φ, ofFieldOpList φs]ₛ = anPart φ * ofFieldOpList φs -
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofFieldOpList φs * anPart φ := by
|
||||
rw [anPart, ofFieldOpList]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_anPartF_ofStateList]
|
||||
rfl
|
||||
|
||||
lemma superCommute_crPart_ofFieldOp (φ φ' : 𝓕.States) :
|
||||
[crPart φ, ofFieldOp φ']ₛ = crPart φ * ofFieldOp φ' -
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofFieldOp φ' * crPart φ := by
|
||||
rw [crPart, ofFieldOp]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_crPartF_ofState]
|
||||
rfl
|
||||
|
||||
lemma superCommute_anPart_ofFieldOp (φ φ' : 𝓕.States) :
|
||||
[anPart φ, ofFieldOp φ']ₛ = anPart φ * ofFieldOp φ' -
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofFieldOp φ' * anPart φ := by
|
||||
rw [anPart, ofFieldOp]
|
||||
rw [superCommute_eq_ι_superCommuteF, superCommuteF_anPartF_ofState]
|
||||
rfl
|
||||
|
||||
|
||||
/-!
|
||||
|
||||
## 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.
|
||||
|
||||
-/
|
||||
|
||||
lemma ofCrAnFieldOpList_mul_ofCrAnFieldOpList_eq_superCommute (φs φs' : List 𝓕.CrAnStates) :
|
||||
ofCrAnFieldOpList φs * ofCrAnFieldOpList φs' =
|
||||
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnFieldOpList φs' * ofCrAnFieldOpList φs
|
||||
+ [ofCrAnFieldOpList φs, ofCrAnFieldOpList φs']ₛ := by
|
||||
rw [superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList]
|
||||
simp [ofCrAnFieldOpList_append]
|
||||
|
||||
lemma ofCrAnFieldOp_mul_ofCrAnFieldOpList_eq_superCommute (φ : 𝓕.CrAnStates)
|
||||
(φs' : List 𝓕.CrAnStates) : ofCrAnFieldOp φ * ofCrAnFieldOpList φs' =
|
||||
𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • ofCrAnFieldOpList φs' * ofCrAnFieldOp φ
|
||||
+ [ofCrAnFieldOp φ, ofCrAnFieldOpList φs']ₛ := by
|
||||
rw [← ofCrAnFieldOpList_singleton, ofCrAnFieldOpList_mul_ofCrAnFieldOpList_eq_superCommute]
|
||||
simp
|
||||
|
||||
lemma ofFieldOpList_mul_ofFieldOpList_eq_superCommute (φs φs' : List 𝓕.States) :
|
||||
ofFieldOpList φs * ofFieldOpList φs' =
|
||||
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofFieldOpList φs
|
||||
+ [ofFieldOpList φs, ofFieldOpList φs']ₛ := by
|
||||
rw [superCommute_ofFieldOpList_ofFieldOpList]
|
||||
simp
|
||||
|
||||
lemma ofFieldOp_mul_ofFieldOpList_eq_superCommute (φ : 𝓕.States) (φs' : List 𝓕.States) :
|
||||
ofFieldOp φ * ofFieldOpList φs' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofFieldOp φ
|
||||
+ [ofFieldOp φ, ofFieldOpList φs']ₛ := by
|
||||
rw [superCommute_ofFieldOp_ofFieldOpList]
|
||||
simp
|
||||
|
||||
lemma ofFieldOpList_mul_ofFieldOp_eq_superCommute (φs : List 𝓕.States) (φ : 𝓕.States) :
|
||||
ofFieldOpList φs * ofFieldOp φ = 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) • ofFieldOp φ * ofFieldOpList φs
|
||||
+ [ofFieldOpList φs, ofFieldOp φ]ₛ := by
|
||||
rw [superCommute_ofFieldOpList_ofFieldOp]
|
||||
simp
|
||||
|
||||
lemma ofCrAnFieldOpList_mul_ofFieldOpList_eq_superCommute (φs : List 𝓕.CrAnStates)
|
||||
(φs' : List 𝓕.States) : ofCrAnFieldOpList φs * ofFieldOpList φs' =
|
||||
𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofCrAnFieldOpList φs
|
||||
+ [ofCrAnFieldOpList φs, ofFieldOpList φs']ₛ := by
|
||||
rw [superCommute_ofCrAnFieldOpList_ofFieldOpList]
|
||||
simp
|
||||
|
||||
lemma crPart_mul_anPart_eq_superCommute (φ φ' : 𝓕.States) :
|
||||
crPart φ * anPart φ' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart φ' * crPart φ
|
||||
+ [crPart φ, anPart φ']ₛ := by
|
||||
rw [superCommute_crPart_anPart]
|
||||
simp
|
||||
|
||||
lemma anPart_mul_crPart_eq_superCommute (φ φ' : 𝓕.States) :
|
||||
anPart φ * crPart φ' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart φ' * anPart φ
|
||||
+ [anPart φ, crPart φ']ₛ := by
|
||||
rw [superCommute_anPart_crPart]
|
||||
simp
|
||||
|
||||
lemma crPart_mul_crPart_swap (φ φ' : 𝓕.States) :
|
||||
crPart φ * crPart φ' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart φ' * crPart φ := by
|
||||
trans 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart φ' * crPart φ + [crPart φ, crPart φ']ₛ
|
||||
· rw [crPart, crPart, superCommute_eq_ι_superCommuteF, superCommuteF_crPartF_crPartF]
|
||||
simp
|
||||
· simp
|
||||
|
||||
lemma anPart_mul_anPart_swap (φ φ' : 𝓕.States) :
|
||||
anPart φ * anPart φ' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart φ' * anPart φ := by
|
||||
trans 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart φ' * anPart φ + [anPart φ, anPart φ']ₛ
|
||||
· rw [anPart, anPart, superCommute_eq_ι_superCommuteF, superCommuteF_anPartF_anPartF]
|
||||
simp
|
||||
· simp
|
||||
|
||||
/-!
|
||||
|
||||
## Symmetry of the super commutor.
|
||||
|
||||
-/
|
||||
|
||||
lemma superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList_symm (φs φs' : List 𝓕.CrAnStates) :
|
||||
[ofCrAnFieldOpList φs, ofCrAnFieldOpList φs']ₛ =
|
||||
(- 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs')) • [ofCrAnFieldOpList φs', ofCrAnFieldOpList φs]ₛ := by
|
||||
rw [ofCrAnFieldOpList, ofCrAnFieldOpList, superCommute_eq_ι_superCommuteF,
|
||||
superCommuteF_ofCrAnList_ofCrAnList_symm]
|
||||
rfl
|
||||
|
||||
lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_symm (φ φ' : 𝓕.CrAnStates) :
|
||||
[ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ =
|
||||
(- 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ')) • [ofCrAnFieldOp φ', ofCrAnFieldOp φ]ₛ := by
|
||||
rw [ofCrAnFieldOp, ofCrAnFieldOp, superCommute_eq_ι_superCommuteF,
|
||||
superCommuteF_ofCrAnState_ofCrAnState_symm]
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## splitting the super commute into sums
|
||||
|
||||
-/
|
||||
|
||||
lemma superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList_eq_sum (φs φs' : List 𝓕.CrAnStates) :
|
||||
[ofCrAnFieldOpList φs, ofCrAnFieldOpList φs']ₛ =
|
||||
∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs'.take n) •
|
||||
ofCrAnFieldOpList (φs'.take n) * [ofCrAnFieldOpList φs, ofCrAnFieldOp (φs'.get n)]ₛ *
|
||||
ofCrAnFieldOpList (φs'.drop (n + 1)) := by
|
||||
conv_lhs =>
|
||||
rw [ofCrAnFieldOpList, ofCrAnFieldOpList, superCommute_eq_ι_superCommuteF,
|
||||
superCommuteF_ofCrAnList_ofCrAnList_eq_sum]
|
||||
rw [map_sum]
|
||||
rfl
|
||||
|
||||
lemma superCommute_ofCrAnFieldOpList_ofFieldOpList_eq_sum (φs : List 𝓕.CrAnStates)
|
||||
(φs' : List 𝓕.States) : [ofCrAnFieldOpList φs, ofFieldOpList φs']ₛ =
|
||||
∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs'.take n) •
|
||||
ofFieldOpList (φs'.take n) * [ofCrAnFieldOpList φs, ofFieldOp (φs'.get n)]ₛ *
|
||||
ofFieldOpList (φs'.drop (n + 1)) := by
|
||||
conv_lhs =>
|
||||
rw [ofCrAnFieldOpList, ofFieldOpList, superCommute_eq_ι_superCommuteF,
|
||||
superCommuteF_ofCrAnList_ofStateList_eq_sum]
|
||||
rw [map_sum]
|
||||
rfl
|
||||
|
||||
|
||||
end FieldOpAlgebra
|
||||
end FieldSpecification
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue