/- 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 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Grading /-! # Super Commute -/ namespace FieldSpecification variable {๐“• : FieldSpecification} namespace CrAnAlgebra /-! ## 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 ฯ†, crPart ฯ†']โ‚›ca = anPart ฯ† * crPart ฯ†' - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข crPart ฯ†' * anPart ฯ† := 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 ฯ†, anPart ฯ†']โ‚›ca = crPart ฯ† * anPart ฯ†' - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข anPart ฯ†' * crPart ฯ† := 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 ฯ†, crPart ฯ†']โ‚›ca = crPart ฯ† * crPart ฯ†' - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข crPart ฯ†' * crPart ฯ† := 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 ฯ†, anPart ฯ†']โ‚›ca = anPart ฯ† * anPart ฯ†' - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข anPart ฯ†' * anPart ฯ† := 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 ฯ†, ofStateList ฯ†s]โ‚›ca = crPart ฯ† * ofStateList ฯ†s - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s) โ€ข ofStateList ฯ†s * crPart ฯ† := 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 ฯ†, ofStateList ฯ†s]โ‚›ca = anPart ฯ† * ofStateList ฯ†s - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s) โ€ข ofStateList ฯ†s * anPart ฯ† := 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 ฯ†, ofState ฯ†']โ‚›ca = crPart ฯ† * ofState ฯ†' - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ofState ฯ†' * crPart ฯ† := by rw [โ† ofStateList_singleton, superCommute_crPart_ofStateList] simp lemma superCommute_anPart_ofState (ฯ† ฯ†' : ๐“•.States) : [anPart ฯ†, ofState ฯ†']โ‚›ca = anPart ฯ† * ofState ฯ†' - ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข ofState ฯ†' * anPart ฯ† := 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 ฯ† * anPart ฯ†' = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข anPart ฯ†' * crPart ฯ† + [crPart ฯ†, anPart ฯ†']โ‚›ca := by rw [superCommute_crPart_anPart] simp lemma anPart_mul_crPart_eq_superCommute (ฯ† ฯ†' : ๐“•.States) : anPart ฯ† * crPart ฯ†' = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข crPart ฯ†' * anPart ฯ† + [anPart ฯ†, crPart ฯ†']โ‚›ca := by rw [superCommute_anPart_crPart] simp lemma crPart_mul_crPart_eq_superCommute (ฯ† ฯ†' : ๐“•.States) : crPart ฯ† * crPart ฯ†' = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข crPart ฯ†' * crPart ฯ† + [crPart ฯ†, crPart ฯ†']โ‚›ca := by rw [superCommute_crPart_crPart] simp lemma anPart_mul_anPart_eq_superCommute (ฯ† ฯ†' : ๐“•.States) : anPart ฯ† * anPart ฯ†' = ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†') โ€ข anPart ฯ†' * anPart ฯ† + [anPart ฯ†, anPart ฯ†']โ‚›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] lemma summerCommute_jacobi_ofCrAnList (ฯ†s1 ฯ†s2 ฯ†s3 : List ๐“•.CrAnStates) : [ofCrAnList ฯ†s1, [ofCrAnList ฯ†s2, ofCrAnList ฯ†s3]โ‚›ca]โ‚›ca = ๐“ข(๐“• |>โ‚› ฯ†s1, ๐“• |>โ‚› ฯ†s3) โ€ข (- ๐“ข(๐“• |>โ‚› ฯ†s2, ๐“• |>โ‚› ฯ†s3) โ€ข [ofCrAnList ฯ†s3, [ofCrAnList ฯ†s1, ofCrAnList ฯ†s2]โ‚›ca]โ‚›ca - ๐“ข(๐“• |>โ‚› ฯ†s1, ๐“• |>โ‚› ฯ†s2) โ€ข [ofCrAnList ฯ†s2, [ofCrAnList ฯ†s3, ofCrAnList ฯ†s1]โ‚›ca]โ‚›ca) := by repeat rw [superCommute_ofCrAnList_ofCrAnList] simp repeat rw [superCommute_ofCrAnList_ofCrAnList] simp only [instCommGroup.eq_1, ofList_append_eq_mul, List.append_assoc] by_cases h1 : (๐“• |>โ‚› ฯ†s1) = bosonic <;> by_cases h2 : (๐“• |>โ‚› ฯ†s2) = bosonic <;> by_cases h3 : (๐“• |>โ‚› ฯ†s3) = bosonic ยท simp [h1, h2, exchangeSign_bosonic, h3, mul_one, one_smul] abel ยท simp [h1, h2, exchangeSign_bosonic, bosonic_exchangeSign, mul_one, one_smul] abel ยท simp [h1, bosonic_exchangeSign, h3, exchangeSign_bosonic, mul_one, one_smul] abel ยท simp at h1 h2 h3 simp [h1, h2, h3] abel ยท simp at h1 h2 h3 simp [h1, h2, h3] abel ยท simp at h1 h2 h3 simp [h1, h2, h3] abel ยท simp at h1 h2 h3 simp [h1, h2, h3] abel ยท simp at h1 h2 h3 simp [h1, h2, h3] abel /-! ## Interaction with grading. -/ lemma superCommute_grade {a b : ๐“•.CrAnAlgebra} {f1 f2 : FieldStatistic} (ha : a โˆˆ statisticSubmodule f1) (hb : b โˆˆ statisticSubmodule f2) : [a, b]โ‚›ca โˆˆ statisticSubmodule (f1 + f2) := by let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule f2) : Prop := [a, a2]โ‚›ca โˆˆ statisticSubmodule (f1 + f2) change p b hb apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s, rfl, hฯ†sโŸฉ := hx simp [p] let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule f1) : Prop := [a2, ofCrAnList ฯ†s]โ‚›ca โˆˆ statisticSubmodule (f1 + f2) change p a ha apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s', rfl, hฯ†s'โŸฉ := hx simp [p] rw [superCommute_ofCrAnList_ofCrAnList] apply Submodule.sub_mem _ ยท apply ofCrAnList_mem_statisticSubmodule_of rw [ofList_append_eq_mul, hฯ†s, hฯ†s'] ยท apply Submodule.smul_mem apply ofCrAnList_mem_statisticSubmodule_of rw [ofList_append_eq_mul, hฯ†s, hฯ†s'] rw [mul_comm] ยท simp [p] ยท intro x y hx hy hp1 hp2 simp [p] exact Submodule.add_mem _ hp1 hp2 ยท intro c x hx hp1 simp [p] exact Submodule.smul_mem _ c hp1 ยท exact ha ยท simp [p] ยท intro x y hx hy hp1 hp2 simp [p] exact Submodule.add_mem _ hp1 hp2 ยท intro c x hx hp1 simp [p] exact Submodule.smul_mem _ c hp1 ยท exact hb lemma superCommute_bosonic_bosonic {a b : ๐“•.CrAnAlgebra} (ha : a โˆˆ statisticSubmodule bosonic) (hb : b โˆˆ statisticSubmodule bosonic) : [a, b]โ‚›ca = a * b - b * a := by let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule bosonic) : Prop := [a, a2]โ‚›ca = a * a2 - a2 * a change p b hb apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s, rfl, hฯ†sโŸฉ := hx let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule bosonic) : Prop := [a2, ofCrAnList ฯ†s]โ‚›ca = a2 * ofCrAnList ฯ†s - ofCrAnList ฯ†s * a2 change p a ha apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s', rfl, hฯ†s'โŸฉ := hx simp [p] rw [superCommute_ofCrAnList_ofCrAnList] simp [hฯ†s, ofCrAnList_append] ยท simp [p] ยท intro x y hx hy hp1 hp2 simp_all [p, mul_add, add_mul] abel ยท intro c x hx hp1 simp_all [p, smul_sub] ยท exact ha ยท simp [p] ยท intro x y hx hy hp1 hp2 simp_all [p, mul_add, add_mul] abel ยท intro c x hx hp1 simp_all [p, smul_sub] ยท exact hb lemma superCommute_bosonic_fermionic {a b : ๐“•.CrAnAlgebra} (ha : a โˆˆ statisticSubmodule bosonic) (hb : b โˆˆ statisticSubmodule fermionic) : [a, b]โ‚›ca = a * b - b * a := by let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule fermionic) : Prop := [a, a2]โ‚›ca = a * a2 - a2 * a change p b hb apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s, rfl, hฯ†sโŸฉ := hx let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule bosonic) : Prop := [a2, ofCrAnList ฯ†s]โ‚›ca = a2 * ofCrAnList ฯ†s - ofCrAnList ฯ†s * a2 change p a ha apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s', rfl, hฯ†s'โŸฉ := hx simp [p] rw [superCommute_ofCrAnList_ofCrAnList] simp [hฯ†s, hฯ†s', ofCrAnList_append] ยท simp [p] ยท intro x y hx hy hp1 hp2 simp_all [p, mul_add, add_mul] abel ยท intro c x hx hp1 simp_all [p, smul_sub] ยท exact ha ยท simp [p] ยท intro x y hx hy hp1 hp2 simp_all [p, mul_add, add_mul] abel ยท intro c x hx hp1 simp_all [p, smul_sub] ยท exact hb lemma superCommute_fermionic_bonsonic {a b : ๐“•.CrAnAlgebra} (ha : a โˆˆ statisticSubmodule fermionic) (hb : b โˆˆ statisticSubmodule bosonic) : [a, b]โ‚›ca = a * b - b * a := by let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule bosonic) : Prop := [a, a2]โ‚›ca = a * a2 - a2 * a change p b hb apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s, rfl, hฯ†sโŸฉ := hx let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule fermionic) : Prop := [a2, ofCrAnList ฯ†s]โ‚›ca = a2 * ofCrAnList ฯ†s - ofCrAnList ฯ†s * a2 change p a ha apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s', rfl, hฯ†s'โŸฉ := hx simp [p] rw [superCommute_ofCrAnList_ofCrAnList] simp [hฯ†s, hฯ†s', ofCrAnList_append] ยท simp [p] ยท intro x y hx hy hp1 hp2 simp_all [p, mul_add, add_mul] abel ยท intro c x hx hp1 simp_all [p, smul_sub] ยท exact ha ยท simp [p] ยท intro x y hx hy hp1 hp2 simp_all [p, mul_add, add_mul] abel ยท intro c x hx hp1 simp_all [p, smul_sub] ยท exact hb lemma superCommute_bonsonic {a b : ๐“•.CrAnAlgebra} (hb : b โˆˆ statisticSubmodule bosonic) : [a, b]โ‚›ca = a * b - b * a := by rw [โ† bosonicProj_add_fermionicProj a] simp only [map_add, LinearMap.add_apply] rw [superCommute_bosonic_bosonic (by simp) hb, superCommute_fermionic_bonsonic (by simp) hb] simp only [add_mul, mul_add] abel lemma bosonic_superCommute {a b : ๐“•.CrAnAlgebra} (ha : a โˆˆ statisticSubmodule bosonic) : [a, b]โ‚›ca = a * b - b * a := by rw [โ† bosonicProj_add_fermionicProj b] simp only [map_add, LinearMap.add_apply] rw [superCommute_bosonic_bosonic ha (by simp), superCommute_bosonic_fermionic ha (by simp)] simp only [add_mul, mul_add] abel lemma superCommute_bonsonic_symm {a b : ๐“•.CrAnAlgebra} (hb : b โˆˆ statisticSubmodule bosonic) : [a, b]โ‚›ca = - [b, a]โ‚›ca := by rw [bosonic_superCommute hb, superCommute_bonsonic hb] simp lemma bonsonic_superCommute_symm {a b : ๐“•.CrAnAlgebra} (ha : a โˆˆ statisticSubmodule bosonic) : [a, b]โ‚›ca = - [b, a]โ‚›ca := by rw [bosonic_superCommute ha, superCommute_bonsonic ha] simp lemma superCommute_fermionic_fermionic {a b : ๐“•.CrAnAlgebra} (ha : a โˆˆ statisticSubmodule fermionic) (hb : b โˆˆ statisticSubmodule fermionic) : [a, b]โ‚›ca = a * b + b * a := by let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule fermionic) : Prop := [a, a2]โ‚›ca = a * a2 + a2 * a change p b hb apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s, rfl, hฯ†sโŸฉ := hx let p (a2 : ๐“•.CrAnAlgebra) (hx : a2 โˆˆ statisticSubmodule fermionic) : Prop := [a2, ofCrAnList ฯ†s]โ‚›ca = a2 * ofCrAnList ฯ†s + ofCrAnList ฯ†s * a2 change p a ha apply Submodule.span_induction (p := p) ยท intro x hx obtain โŸจฯ†s', rfl, hฯ†s'โŸฉ := hx simp [p] rw [superCommute_ofCrAnList_ofCrAnList] simp [hฯ†s, hฯ†s', ofCrAnList_append] ยท simp [p] ยท intro x y hx hy hp1 hp2 simp_all [p, mul_add, add_mul] abel ยท intro c x hx hp1 simp_all [p, smul_sub] ยท exact ha ยท simp [p] ยท intro x y hx hy hp1 hp2 simp_all [p, mul_add, add_mul] abel ยท intro c x hx hp1 simp_all [p, smul_sub] ยท exact hb lemma superCommute_fermionic_fermionic_symm {a b : ๐“•.CrAnAlgebra} (ha : a โˆˆ statisticSubmodule fermionic) (hb : b โˆˆ statisticSubmodule fermionic) : [a, b]โ‚›ca = [b, a]โ‚›ca := by rw [superCommute_fermionic_fermionic ha hb] rw [superCommute_fermionic_fermionic hb ha] abel lemma superCommute_expand_bosonicProj_fermionicProj (a b : ๐“•.CrAnAlgebra) : [a, b]โ‚›ca = bosonicProj a * bosonicProj b - bosonicProj b * bosonicProj a + bosonicProj a * fermionicProj b - fermionicProj b * bosonicProj a + fermionicProj a * bosonicProj b - bosonicProj b * fermionicProj a + fermionicProj a * fermionicProj b + fermionicProj b * fermionicProj a := by conv_lhs => rw [โ† bosonicProj_add_fermionicProj a, โ† bosonicProj_add_fermionicProj b] simp rw [superCommute_bonsonic (by simp), superCommute_bosonic_fermionic (by simp) (by simp), superCommute_fermionic_bonsonic (by simp) (by simp), superCommute_fermionic_fermionic (by simp) (by simp)] abel lemma superCommute_ofCrAnList_ofCrAnList_bosonic_or_fermionic (ฯ†s ฯ†s' : List ๐“•.CrAnStates) : [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca โˆˆ statisticSubmodule bosonic โˆจ [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca โˆˆ statisticSubmodule fermionic := by by_cases h1 : (๐“• |>โ‚› ฯ†s) = bosonic <;> by_cases h2 : (๐“• |>โ‚› ฯ†s') = bosonic ยท left have h : bosonic = bosonic + bosonic := by simp only [add_eq_mul, instCommGroup, mul_self] rfl rw [h] apply superCommute_grade apply ofCrAnList_mem_statisticSubmodule_of _ _ h1 apply ofCrAnList_mem_statisticSubmodule_of _ _ h2 ยท right have h : fermionic = bosonic + fermionic := by simp only [add_eq_mul, instCommGroup, mul_self] rfl rw [h] apply superCommute_grade apply ofCrAnList_mem_statisticSubmodule_of _ _ h1 apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h2) ยท right have h : fermionic = fermionic + bosonic := by simp only [add_eq_mul, instCommGroup, mul_self] rfl rw [h] apply superCommute_grade apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h1) apply ofCrAnList_mem_statisticSubmodule_of _ _ h2 ยท left have h : bosonic = fermionic + fermionic := by simp only [add_eq_mul, instCommGroup, mul_self] rfl rw [h] apply superCommute_grade apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h1) apply ofCrAnList_mem_statisticSubmodule_of _ _ (by simpa using h2) lemma superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic (ฯ† ฯ†' : ๐“•.CrAnStates) : [ofCrAnState ฯ†, ofCrAnState ฯ†']โ‚›ca โˆˆ statisticSubmodule bosonic โˆจ [ofCrAnState ฯ†, ofCrAnState ฯ†']โ‚›ca โˆˆ statisticSubmodule fermionic := by rw [โ† ofCrAnList_singleton, โ† ofCrAnList_singleton] exact superCommute_ofCrAnList_ofCrAnList_bosonic_or_fermionic [ฯ†] [ฯ†'] lemma superCommute_superCommute_ofCrAnState_bosonic_or_fermionic (ฯ†1 ฯ†2 ฯ†3 : ๐“•.CrAnStates) : [ofCrAnState ฯ†1, [ofCrAnState ฯ†2, ofCrAnState ฯ†3]โ‚›ca]โ‚›ca โˆˆ statisticSubmodule bosonic โˆจ [ofCrAnState ฯ†1, [ofCrAnState ฯ†2, ofCrAnState ฯ†3]โ‚›ca]โ‚›ca โˆˆ statisticSubmodule fermionic := by rcases superCommute_ofCrAnState_ofCrAnState_bosonic_or_fermionic ฯ†2 ฯ†3 with hs | hs <;> rcases ofCrAnState_bosonic_or_fermionic ฯ†1 with h1 | h1 ยท left have h : bosonic = bosonic + bosonic := by simp only [add_eq_mul, instCommGroup, mul_self] rfl rw [h] apply superCommute_grade h1 hs ยท right have h : fermionic = fermionic + bosonic := by simp only [add_eq_mul, instCommGroup, mul_self] rfl rw [h] apply superCommute_grade h1 hs ยท right have h : fermionic = bosonic + fermionic := by simp only [add_eq_mul, instCommGroup, mul_self] rfl rw [h] apply superCommute_grade h1 hs ยท left have h : bosonic = fermionic + fermionic := by simp only [add_eq_mul, instCommGroup, mul_self] rfl rw [h] apply superCommute_grade h1 hs lemma superCommute_bosonic_ofCrAnList_eq_sum (a : ๐“•.CrAnAlgebra) (ฯ†s : List ๐“•.CrAnStates) (ha : a โˆˆ statisticSubmodule bosonic) : [a, ofCrAnList ฯ†s]โ‚›ca = โˆ‘ (n : Fin ฯ†s.length), ofCrAnList (ฯ†s.take n) * [a, ofCrAnState (ฯ†s.get n)]โ‚›ca * ofCrAnList (ฯ†s.drop (n + 1)) := by let p (a : ๐“•.CrAnAlgebra) (ha : a โˆˆ statisticSubmodule bosonic) : Prop := [a, ofCrAnList ฯ†s]โ‚›ca = โˆ‘ (n : Fin ฯ†s.length), ofCrAnList (ฯ†s.take n) * [a, ofCrAnState (ฯ†s.get n)]โ‚›ca * ofCrAnList (ฯ†s.drop (n + 1)) change p a ha apply Submodule.span_induction (p := p) ยท intro a ha obtain โŸจฯ†s, rfl, hฯ†sโŸฉ := ha simp [p] rw [superCommute_ofCrAnList_ofCrAnList_eq_sum] congr funext n simp [hฯ†s] ยท simp [p] ยท intro x y hx hy hpx hpy simp_all [p] rw [โ† Finset.sum_add_distrib] congr funext n simp [mul_add, add_mul] ยท intro c x hx hpx simp_all [p, Finset.smul_sum] ยท exact ha lemma superCommute_fermionic_ofCrAnList_eq_sum (a : ๐“•.CrAnAlgebra) (ฯ†s : List ๐“•.CrAnStates) (ha : a โˆˆ statisticSubmodule fermionic) : [a, ofCrAnList ฯ†s]โ‚›ca = โˆ‘ (n : Fin ฯ†s.length), ๐“ข(fermionic, ๐“• |>โ‚› ฯ†s.take n) โ€ข ofCrAnList (ฯ†s.take n) * [a, ofCrAnState (ฯ†s.get n)]โ‚›ca * ofCrAnList (ฯ†s.drop (n + 1)) := by let p (a : ๐“•.CrAnAlgebra) (ha : a โˆˆ statisticSubmodule fermionic) : Prop := [a, ofCrAnList ฯ†s]โ‚›ca = โˆ‘ (n : Fin ฯ†s.length), ๐“ข(fermionic, ๐“• |>โ‚› ฯ†s.take n) โ€ข ofCrAnList (ฯ†s.take n) * [a, ofCrAnState (ฯ†s.get n)]โ‚›ca * ofCrAnList (ฯ†s.drop (n + 1)) change p a ha apply Submodule.span_induction (p := p) ยท intro a ha obtain โŸจฯ†s, rfl, hฯ†sโŸฉ := ha simp [p] rw [superCommute_ofCrAnList_ofCrAnList_eq_sum] congr funext n simp [hฯ†s] ยท simp [p] ยท intro x y hx hy hpx hpy simp_all [p] rw [โ† Finset.sum_add_distrib] congr funext n simp [mul_add, add_mul] ยท intro c x hx hpx simp_all [p, Finset.smul_sum] congr funext x simp [smul_smul, mul_comm] ยท exact ha lemma statistic_neq_of_superCommute_fermionic {ฯ†s ฯ†s' : List ๐“•.CrAnStates} (h : [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca โˆˆ statisticSubmodule fermionic) : (๐“• |>โ‚› ฯ†s) โ‰  (๐“• |>โ‚› ฯ†s') โˆจ [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca = 0 := by by_cases h0 : [ofCrAnList ฯ†s, ofCrAnList ฯ†s']โ‚›ca = 0 ยท simp [h0] simp [h0] by_contra hn refine h0 (eq_zero_of_bosonic_and_fermionic ?_ h) by_cases hc : (๐“• |>โ‚› ฯ†s) = bosonic ยท have h1 : bosonic = bosonic + bosonic := by simp rfl rw [h1] apply superCommute_grade apply ofCrAnList_mem_statisticSubmodule_of _ _ hc apply ofCrAnList_mem_statisticSubmodule_of _ _ rw [โ† hn, hc] ยท have h1 : bosonic = fermionic + fermionic := by simp rfl rw [h1] apply superCommute_grade apply ofCrAnList_mem_statisticSubmodule_of _ _ simpa using hc apply ofCrAnList_mem_statisticSubmodule_of _ _ rw [โ† hn] simpa using hc end CrAnAlgebra end FieldSpecification