/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic /-! # Super Commute -/ namespace FieldSpecification variable {๐“• : FieldSpecification} namespace CrAnAlgebra open StateAlgebra /-! ## The super commutor on the CrAnAlgebra. -/ open FieldStatistic /-- The super commutor on the creation and annihlation algebra. For two bosonic operators or a bosonic and fermionic operator this corresponds to the usual commutator whilst for two fermionic operators this corresponds to the anti-commutator. -/ noncomputable def superCommute : ๐“•.CrAnAlgebra โ†’โ‚—[โ„‚] ๐“•.CrAnAlgebra โ†’โ‚—[โ„‚] ๐“•.CrAnAlgebra := Basis.constr ofCrAnListBasis โ„‚ fun ฯ†s => Basis.constr ofCrAnListBasis โ„‚ fun ฯ†s' => ofCrAnList (ฯ†s ++ ฯ†s') - ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s') โ€ข ofCrAnList (ฯ†s' ++ ฯ†s) /-- The super commutor on the creation and annihlation algebra. For two bosonic operators or a bosonic and fermionic operator this corresponds to the usual commutator whilst for two fermionic operators this corresponds to the anti-commutator. -/ scoped[FieldSpecification.CrAnAlgebra] notation "[" ฯ†s "," ฯ†s' "]โ‚›ca" => superCommute ฯ†s ฯ†s' /-! ## The super commutor of different types of elements -/ lemma superCommute_ofCrAnList_ofCrAnList (ฯ†s ฯ†s' : List ๐“•.CrAnStates) : [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca = ofCrAnList (ฯ†s ++ ฯ†s') - ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s') โ€ข ofCrAnList (ฯ†s' ++ ฯ†s) := by rw [โ† ofListBasis_eq_ofList, โ† ofListBasis_eq_ofList] simp only [superCommute, Basis.constr_basis] lemma superCommute_ofCrAnState_ofCrAnState (ฯ† ฯ†' : ๐“•.CrAnStates) : [ofCrAnState ฯ†, ofCrAnState ฯ†']โ‚›ca = ofCrAnState ฯ† * ofCrAnState ฯ†' - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ofCrAnState ฯ†' * ofCrAnState ฯ† := by rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton] rw [superCommute_ofCrAnList_ofCrAnList, ofCrAnList_append] congr rw [ofCrAnList_append] rw [FieldStatistic.ofList_singleton, FieldStatistic.ofList_singleton, smul_mul_assoc] lemma superCommute_ofCrAnList_ofStatesList (ฯ†cas : List ๐“•.CrAnStates) (ฯ†s : List ๐“•.States) : [ofCrAnList ฯ†cas, ofStateList ฯ†s]โ‚›ca = ofCrAnList ฯ†cas * ofStateList ฯ†s - ๐“ข(๐“• |>โ‚› ฯ†cas, ๐“• |>โ‚› ฯ†s) โ€ข ofStateList ฯ†s * ofCrAnList ฯ†cas := by conv_lhs => rw [ofStateList_sum] rw [map_sum] conv_lhs => enter [2, x] rw [superCommute_ofCrAnList_ofCrAnList, CrAnSection.statistics_eq_state_statistics, ofCrAnList_append, ofCrAnList_append] rw [Finset.sum_sub_distrib, โ† Finset.mul_sum, โ† Finset.smul_sum, โ† Finset.sum_mul, โ† ofStateList_sum] simp lemma superCommute_ofStateList_ofStatesList (ฯ† : List ๐“•.States) (ฯ†s : List ๐“•.States) : [ofStateList ฯ†, ofStateList ฯ†s]โ‚›ca = ofStateList ฯ† * ofStateList ฯ†s - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s) โ€ข ofStateList ฯ†s * ofStateList ฯ† := by conv_lhs => rw [ofStateList_sum] simp only [map_sum, LinearMap.coeFn_sum, Finset.sum_apply, instCommGroup.eq_1, Algebra.smul_mul_assoc] conv_lhs => enter [2, x] rw [superCommute_ofCrAnList_ofStatesList] simp only [instCommGroup.eq_1, CrAnSection.statistics_eq_state_statistics, Algebra.smul_mul_assoc, Finset.sum_sub_distrib] rw [โ† Finset.sum_mul, โ† Finset.smul_sum, โ† Finset.mul_sum, โ† ofStateList_sum] lemma superCommute_ofState_ofStatesList (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : [ofState ฯ†, ofStateList ฯ†s]โ‚›ca = ofState ฯ† * ofStateList ฯ†s - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s) โ€ข ofStateList ฯ†s * ofState ฯ† := by rw [โ† ofStateList_singleton, superCommute_ofStateList_ofStatesList, ofStateList_singleton] simp lemma superCommute_ofStateList_ofState (ฯ†s : List ๐“•.States) (ฯ† : ๐“•.States) : [ofStateList ฯ†s, ofState ฯ†]โ‚›ca = ofStateList ฯ†s * ofState ฯ† - ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†) โ€ข ofState ฯ† * ofStateList ฯ†s := by rw [โ† ofStateList_singleton, superCommute_ofStateList_ofStatesList, ofStateList_singleton] simp lemma superCommute_anPart_crPart (ฯ† ฯ†' : ๐“•.States) : [anPart (StateAlgebra.ofState ฯ†), crPart (StateAlgebra.ofState ฯ†')]โ‚›ca = anPart (StateAlgebra.ofState ฯ†) * crPart (StateAlgebra.ofState ฯ†') - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข crPart (StateAlgebra.ofState ฯ†') * anPart (StateAlgebra.ofState ฯ†) := by match ฯ†, ฯ†' with | States.inAsymp ฯ†, _ => simp | _, States.outAsymp ฯ† => simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self] | States.position ฯ†, States.position ฯ†' => simp only [anPart_position, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.outAsymp ฯ†, States.position ฯ†' => simp only [anPart_posAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.position ฯ†, States.inAsymp ฯ†' => simp only [anPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp only [List.singleton_append, instCommGroup.eq_1, crAnStatistics, FieldStatistic.ofList_singleton, Function.comp_apply, crAnStatesToStates_prod, โ† ofCrAnList_append] | States.outAsymp ฯ†, States.inAsymp ฯ†' => simp only [anPart_posAsymp, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] lemma superCommute_crPart_anPart (ฯ† ฯ†' : ๐“•.States) : [crPart (StateAlgebra.ofState ฯ†), anPart (StateAlgebra.ofState ฯ†')]โ‚›ca = crPart (StateAlgebra.ofState ฯ†) * anPart (StateAlgebra.ofState ฯ†') - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข anPart (StateAlgebra.ofState ฯ†') * crPart (StateAlgebra.ofState ฯ†) := by match ฯ†, ฯ†' with | States.outAsymp ฯ†, _ => simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1, mul_zero, sub_self] | _, States.inAsymp ฯ† => simp only [anPart_negAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self] | States.position ฯ†, States.position ฯ†' => simp only [crPart_position, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.position ฯ†, States.outAsymp ฯ†' => simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.inAsymp ฯ†, States.position ฯ†' => simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.inAsymp ฯ†, States.outAsymp ฯ†' => simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] lemma superCommute_crPart_crPart (ฯ† ฯ†' : ๐“•.States) : [crPart (StateAlgebra.ofState ฯ†), crPart (StateAlgebra.ofState ฯ†')]โ‚›ca = crPart (StateAlgebra.ofState ฯ†) * crPart (StateAlgebra.ofState ฯ†') - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข crPart (StateAlgebra.ofState ฯ†') * crPart (StateAlgebra.ofState ฯ†) := by match ฯ†, ฯ†' with | States.outAsymp ฯ†, _ => simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1, mul_zero, sub_self] | _, States.outAsymp ฯ† => simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self] | States.position ฯ†, States.position ฯ†' => simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.position ฯ†, States.inAsymp ฯ†' => simp only [crPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.inAsymp ฯ†, States.position ฯ†' => simp only [crPart_negAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.inAsymp ฯ†, States.inAsymp ฯ†' => simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] lemma superCommute_anPart_anPart (ฯ† ฯ†' : ๐“•.States) : [anPart (StateAlgebra.ofState ฯ†), anPart (StateAlgebra.ofState ฯ†')]โ‚›ca = anPart (StateAlgebra.ofState ฯ†) * anPart (StateAlgebra.ofState ฯ†') - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข anPart (StateAlgebra.ofState ฯ†') * anPart (StateAlgebra.ofState ฯ†) := by match ฯ†, ฯ†' with | States.inAsymp ฯ†, _ => simp | _, States.inAsymp ฯ† => simp | States.position ฯ†, States.position ฯ†' => simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.position ฯ†, States.outAsymp ฯ†' => simp only [anPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.outAsymp ฯ†, States.position ฯ†' => simp only [anPart_posAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] | States.outAsymp ฯ†, States.outAsymp ฯ†' => simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList] simp [crAnStatistics, โ† ofCrAnList_append] lemma superCommute_crPart_ofStateList (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : [crPart (StateAlgebra.ofState ฯ†), ofStateList ฯ†s]โ‚›ca = crPart (StateAlgebra.ofState ฯ†) * ofStateList ฯ†s - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s) โ€ข ofStateList ฯ†s * crPart (StateAlgebra.ofState ฯ†) := by match ฯ† with | States.inAsymp ฯ† => simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList] simp [crAnStatistics] | States.position ฯ† => simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList] simp [crAnStatistics] | States.outAsymp ฯ† => simp lemma superCommute_anPart_ofStateList (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.States) : [anPart (StateAlgebra.ofState ฯ†), ofStateList ฯ†s]โ‚›ca = anPart (StateAlgebra.ofState ฯ†) * ofStateList ฯ†s - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s) โ€ข ofStateList ฯ†s * anPart (StateAlgebra.ofState ฯ†) := by match ฯ† with | States.inAsymp ฯ† => simp | States.position ฯ† => simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList] simp [crAnStatistics] | States.outAsymp ฯ† => simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc] rw [โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList] simp [crAnStatistics] lemma superCommute_crPart_ofState (ฯ† ฯ†' : ๐“•.States) : [crPart (StateAlgebra.ofState ฯ†), ofState ฯ†']โ‚›ca = crPart (StateAlgebra.ofState ฯ†) * ofState ฯ†' - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ofState ฯ†' * crPart (StateAlgebra.ofState ฯ†) := by rw [โ† ofStateList_singleton, superCommute_crPart_ofStateList] simp lemma superCommute_anPart_ofState (ฯ† ฯ†' : ๐“•.States) : [anPart (StateAlgebra.ofState ฯ†), ofState ฯ†']โ‚›ca = anPart (StateAlgebra.ofState ฯ†) * ofState ฯ†' - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ofState ฯ†' * anPart (StateAlgebra.ofState ฯ†) := by rw [โ† ofStateList_singleton, superCommute_anPart_ofStateList] simp /-! ## 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 ofCrAnList_mul_ofCrAnList_eq_superCommute (ฯ†s ฯ†s' : List ๐“•.CrAnStates) : ofCrAnList ฯ†s * ofCrAnList ฯ†s' = ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s') โ€ข ofCrAnList ฯ†s' * ofCrAnList ฯ†s + [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca := by rw [superCommute_ofCrAnList_ofCrAnList] simp [ofCrAnList_append] lemma ofCrAnState_mul_ofCrAnList_eq_superCommute (ฯ† : ๐“•.CrAnStates) (ฯ†s' : List ๐“•.CrAnStates) : ofCrAnState ฯ† * ofCrAnList ฯ†s' = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s') โ€ข ofCrAnList ฯ†s' * ofCrAnState ฯ† + [ofCrAnState ฯ†, ofCrAnList ฯ†s']โ‚›ca := by rw [โ† ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_eq_superCommute] simp lemma ofStateList_mul_ofStateList_eq_superCommute (ฯ†s ฯ†s' : List ๐“•.States) : ofStateList ฯ†s * ofStateList ฯ†s' = ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s') โ€ข ofStateList ฯ†s' * ofStateList ฯ†s + [ofStateList ฯ†s, ofStateList ฯ†s']โ‚›ca := by rw [superCommute_ofStateList_ofStatesList] simp lemma ofState_mul_ofStateList_eq_superCommute (ฯ† : ๐“•.States) (ฯ†s' : List ๐“•.States) : ofState ฯ† * ofStateList ฯ†s' = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s') โ€ข ofStateList ฯ†s' * ofState ฯ† + [ofState ฯ†, ofStateList ฯ†s']โ‚›ca := by rw [superCommute_ofState_ofStatesList] simp lemma ofStateList_mul_ofState_eq_superCommute (ฯ†s : List ๐“•.States) (ฯ† : ๐“•.States) : ofStateList ฯ†s * ofState ฯ† = ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†) โ€ข ofState ฯ† * ofStateList ฯ†s + [ofStateList ฯ†s, ofState ฯ†]โ‚›ca := by rw [superCommute_ofStateList_ofState] simp lemma crPart_mul_anPart_eq_superCommute (ฯ† ฯ†' : ๐“•.States) : crPart (StateAlgebra.ofState ฯ†) * anPart (StateAlgebra.ofState ฯ†') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข anPart (StateAlgebra.ofState ฯ†') * crPart (StateAlgebra.ofState ฯ†) + [crPart (StateAlgebra.ofState ฯ†), anPart (StateAlgebra.ofState ฯ†')]โ‚›ca := by rw [superCommute_crPart_anPart] simp lemma anPart_mul_crPart_eq_superCommute (ฯ† ฯ†' : ๐“•.States) : anPart (StateAlgebra.ofState ฯ†) * crPart (StateAlgebra.ofState ฯ†') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข crPart (StateAlgebra.ofState ฯ†') * anPart (StateAlgebra.ofState ฯ†) + [anPart (StateAlgebra.ofState ฯ†), crPart (StateAlgebra.ofState ฯ†')]โ‚›ca := by rw [superCommute_anPart_crPart] simp lemma crPart_mul_crPart_eq_superCommute (ฯ† ฯ†' : ๐“•.States) : crPart (StateAlgebra.ofState ฯ†) * crPart (StateAlgebra.ofState ฯ†') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข crPart (StateAlgebra.ofState ฯ†') * crPart (StateAlgebra.ofState ฯ†) + [crPart (StateAlgebra.ofState ฯ†), crPart (StateAlgebra.ofState ฯ†')]โ‚›ca := by rw [superCommute_crPart_crPart] simp lemma anPart_mul_anPart_eq_superCommute (ฯ† ฯ†' : ๐“•.States) : anPart (StateAlgebra.ofState ฯ†) * anPart (StateAlgebra.ofState ฯ†') = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข anPart (StateAlgebra.ofState ฯ†') * anPart (StateAlgebra.ofState ฯ†) + [anPart (StateAlgebra.ofState ฯ†), anPart (StateAlgebra.ofState ฯ†')]โ‚›ca := by rw [superCommute_anPart_anPart] simp lemma ofCrAnList_mul_ofStateList_eq_superCommute (ฯ†s : List ๐“•.CrAnStates) (ฯ†s' : List ๐“•.States) : ofCrAnList ฯ†s * ofStateList ฯ†s' = ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s') โ€ข ofStateList ฯ†s' * ofCrAnList ฯ†s + [ofCrAnList ฯ†s, ofStateList ฯ†s']โ‚›ca := by rw [superCommute_ofCrAnList_ofStatesList] simp /-! ## Symmetry of the super commutor. -/ lemma superCommute_ofCrAnList_ofCrAnList_symm (ฯ†s ฯ†s' : List ๐“•.CrAnStates) : [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca = (- ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s')) โ€ข [ofCrAnList ฯ†s', ofCrAnList ฯ†s]โ‚›ca := by rw [superCommute_ofCrAnList_ofCrAnList, superCommute_ofCrAnList_ofCrAnList, smul_sub] simp only [instCommGroup.eq_1, neg_smul, sub_neg_eq_add] rw [smul_smul] conv_rhs => rhs rw [exchangeSign_symm, exchangeSign_mul_self] simp only [one_smul] abel lemma superCommute_ofCrAnState_ofCrAnState_symm (ฯ† ฯ†' : ๐“•.CrAnStates) : [ofCrAnState ฯ†, ofCrAnState ฯ†']โ‚›ca = (- ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†')) โ€ข [ofCrAnState ฯ†', ofCrAnState ฯ†]โ‚›ca := by rw [superCommute_ofCrAnState_ofCrAnState, superCommute_ofCrAnState_ofCrAnState] rw [smul_sub] simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, neg_smul, sub_neg_eq_add] rw [smul_smul] conv_rhs => rhs rw [exchangeSign_symm, exchangeSign_mul_self] simp only [one_smul] abel /-! ## Splitting the super commutor on lists into sums. -/ lemma superCommute_ofCrAnList_ofCrAnList_cons (ฯ† : ๐“•.CrAnStates) (ฯ†s ฯ†s' : List ๐“•.CrAnStates) : [ofCrAnList ฯ†s, ofCrAnList (ฯ† :: ฯ†s')]โ‚›ca = [ofCrAnList ฯ†s, ofCrAnState ฯ†]โ‚›ca * ofCrAnList ฯ†s' + ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†) โ€ข ofCrAnState ฯ† * [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca := by rw [superCommute_ofCrAnList_ofCrAnList] conv_rhs => lhs rw [โ† ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList, sub_mul, โ† ofCrAnList_append] rhs rw [FieldStatistic.ofList_singleton, ofCrAnList_append, ofCrAnList_singleton, smul_mul_assoc, mul_assoc, โ† ofCrAnList_append] conv_rhs => rhs rw [superCommute_ofCrAnList_ofCrAnList, mul_sub, smul_mul_assoc] simp only [instCommGroup.eq_1, List.cons_append, List.append_assoc, List.nil_append, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, sub_add_sub_cancel, sub_right_inj] rw [โ† ofCrAnList_cons, smul_smul, FieldStatistic.ofList_cons_eq_mul] simp only [instCommGroup, map_mul, mul_comm] lemma superCommute_ofCrAnList_ofStateList_cons (ฯ† : ๐“•.States) (ฯ†s : List ๐“•.CrAnStates) (ฯ†s' : List ๐“•.States) : [ofCrAnList ฯ†s, ofStateList (ฯ† :: ฯ†s')]โ‚›ca = [ofCrAnList ฯ†s, ofState ฯ†]โ‚›ca * ofStateList ฯ†s' + ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†) โ€ข ofState ฯ† * [ofCrAnList ฯ†s, ofStateList ฯ†s']โ‚›ca := by rw [superCommute_ofCrAnList_ofStatesList] conv_rhs => lhs rw [โ† ofStateList_singleton, superCommute_ofCrAnList_ofStatesList, sub_mul, mul_assoc, โ† ofStateList_append] rhs rw [FieldStatistic.ofList_singleton, ofStateList_singleton, smul_mul_assoc, smul_mul_assoc, mul_assoc] conv_rhs => rhs rw [superCommute_ofCrAnList_ofStatesList, mul_sub, smul_mul_assoc] simp only [instCommGroup, Algebra.smul_mul_assoc, List.singleton_append, Algebra.mul_smul_comm, sub_add_sub_cancel, sub_right_inj] rw [ofStateList_cons, mul_assoc, smul_smul, FieldStatistic.ofList_cons_eq_mul] simp [mul_comm] /-- Within the creation and annihilation algebra, we have that `[ฯ†แถœแตƒs, ฯ†แถœแตƒโ‚€ โ€ฆ ฯ†แถœแตƒโ‚™]โ‚›ca = โˆ‘ i, sแตข โ€ข ฯ†แถœแตƒsโ‚€ โ€ฆ ฯ†แถœแตƒแตขโ‚‹โ‚ * [ฯ†แถœแตƒs, ฯ†แถœแตƒแตข]โ‚›ca * ฯ†แถœแตƒแตขโ‚Šโ‚ โ€ฆ ฯ†แถœแตƒโ‚™` where `sแตข` is the exchange sign for `ฯ†แถœแตƒs` and `ฯ†แถœแตƒsโ‚€ โ€ฆ ฯ†แถœแตƒแตขโ‚‹โ‚`. -/ lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (ฯ†s : List ๐“•.CrAnStates) : (ฯ†s' : List ๐“•.CrAnStates) โ†’ [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca = โˆ‘ (n : Fin ฯ†s'.length), ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s'.take n) โ€ข ofCrAnList (ฯ†s'.take n) * [ofCrAnList ฯ†s, ofCrAnState (ฯ†s'.get n)]โ‚›ca * ofCrAnList (ฯ†s'.drop (n + 1)) | [] => by simp [โ† ofCrAnList_nil, superCommute_ofCrAnList_ofCrAnList] | ฯ† :: ฯ†s' => by rw [superCommute_ofCrAnList_ofCrAnList_cons, superCommute_ofCrAnList_ofCrAnList_eq_sum ฯ†s ฯ†s'] conv_rhs => erw [Fin.sum_univ_succ] congr 1 ยท simp ยท simp [Finset.mul_sum, smul_smul, ofCrAnList_cons, mul_assoc, FieldStatistic.ofList_cons_eq_mul, mul_comm] lemma superCommute_ofCrAnList_ofStateList_eq_sum (ฯ†s : List ๐“•.CrAnStates) : (ฯ†s' : List ๐“•.States) โ†’ [ofCrAnList ฯ†s, ofStateList ฯ†s']โ‚›ca = โˆ‘ (n : Fin ฯ†s'.length), ๐“ข(๐“• |>โ‚› ฯ†s, ๐“• |>โ‚› ฯ†s'.take n) โ€ข ofStateList (ฯ†s'.take n) * [ofCrAnList ฯ†s, ofState (ฯ†s'.get n)]โ‚›ca * ofStateList (ฯ†s'.drop (n + 1)) | [] => by simp only [superCommute_ofCrAnList_ofStatesList, instCommGroup, ofList_empty, exchangeSign_bosonic, one_smul, List.length_nil, Finset.univ_eq_empty, List.take_nil, List.get_eq_getElem, List.drop_nil, Finset.sum_empty] simp | ฯ† :: ฯ†s' => by rw [superCommute_ofCrAnList_ofStateList_cons, superCommute_ofCrAnList_ofStateList_eq_sum ฯ†s ฯ†s'] conv_rhs => erw [Fin.sum_univ_succ] congr 1 ยท simp ยท simp [Finset.mul_sum, smul_smul, ofStateList_cons, mul_assoc, FieldStatistic.ofList_cons_eq_mul, mul_comm] end CrAnAlgebra end FieldSpecification