refactor: Koszul Order

This commit is contained in:
jstoobysmith 2024-12-20 12:45:55 +00:00
parent 3073aa0ab3
commit bbd9be965b

View file

@ -16,18 +16,20 @@ import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
namespace Wick
noncomputable section
open FieldStatistic
variable {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕𝓕 → Prop) [DecidableRel le]
/-- Given a relation `r` on `I` sorts elements of `MonoidAlgebra (FreeMonoid I)` by `r` giving it
a signed dependent on `q`. -/
def koszulOrderMonoidAlgebra {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
MonoidAlgebra (FreeMonoid I) →ₗ[] MonoidAlgebra (FreeMonoid I) :=
Finsupp.lift (MonoidAlgebra (FreeMonoid I)) (List I)
(fun i => Finsupp.lsingle (R := ) (List.insertionSort r i) (koszulSign r q i))
def koszulOrderMonoidAlgebra :
MonoidAlgebra (FreeMonoid 𝓕) →ₗ[] MonoidAlgebra (FreeMonoid 𝓕) :=
Finsupp.lift (MonoidAlgebra (FreeMonoid 𝓕)) (List 𝓕)
(fun i => Finsupp.lsingle (R := ) (List.insertionSort le i) (koszulSign q le i))
lemma koszulOrderMonoidAlgebra_ofList {I : Type} (r : I → I → Prop) [DecidableRel r]
(q : I → Fin 2) (i : List I) :
koszulOrderMonoidAlgebra r q (MonoidAlgebra.of (FreeMonoid I) i) =
(koszulSign r q i) • (MonoidAlgebra.of (FreeMonoid I) (List.insertionSort r i)) := by
lemma koszulOrderMonoidAlgebra_ofList (i : List 𝓕) :
koszulOrderMonoidAlgebra q le (MonoidAlgebra.of (FreeMonoid 𝓕) i) =
(koszulSign q le i) • (MonoidAlgebra.of (FreeMonoid 𝓕) (List.insertionSort le i)) := by
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.of_apply,
MonoidAlgebra.smul_single', mul_one]
rw [MonoidAlgebra.ext_iff]
@ -37,10 +39,9 @@ lemma koszulOrderMonoidAlgebra_ofList {I : Type} (r : I → I → Prop) [Decidab
one_mul]
@[simp]
lemma koszulOrderMonoidAlgebra_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : FreeMonoid I) (x : ) :
koszulOrderMonoidAlgebra r q (MonoidAlgebra.single l x)
= (koszulSign r q l) • (MonoidAlgebra.single (List.insertionSort r l) x) := by
lemma koszulOrderMonoidAlgebra_single (l : FreeMonoid 𝓕) (x : ) :
koszulOrderMonoidAlgebra q le (MonoidAlgebra.single l x)
= (koszulSign q le l) • (MonoidAlgebra.single (List.insertionSort le l) x) := by
simp only [koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, MonoidAlgebra.smul_single']
rw [MonoidAlgebra.ext_iff]
intro x'
@ -52,15 +53,13 @@ lemma koszulOrderMonoidAlgebra_single {I : Type} (r : I → I → Prop) [Decidab
/-- Given a relation `r` on `I` sorts elements of `FreeAlgebra I` by `r` giving it
a signed dependent on `q`. -/
def koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
FreeAlgebra I →ₗ[] FreeAlgebra I :=
def koszulOrder : FreeAlgebra 𝓕 →ₗ[] FreeAlgebra 𝓕 :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm.toAlgHom.toLinearMap
∘ₗ koszulOrderMonoidAlgebra r q
∘ₗ koszulOrderMonoidAlgebra q le
∘ₗ FreeAlgebra.equivMonoidAlgebraFreeMonoid.toAlgHom.toLinearMap
@[simp]
lemma koszulOrder_ι {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i : I) :
koszulOrder r q (FreeAlgebra.ι i) = FreeAlgebra.ι i := by
lemma koszulOrder_ι (i : 𝓕) : koszulOrder q le (FreeAlgebra.ι i) = FreeAlgebra.ι i := by
simp only [koszulOrder, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toLinearMap,
koszulOrderMonoidAlgebra, Finsupp.lsingle_apply, LinearMap.coe_comp, Function.comp_apply,
AlgEquiv.toLinearMap_apply]
@ -75,18 +74,16 @@ lemma koszulOrder_ι {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I
rfl
@[simp]
lemma koszulOrder_single {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(l : FreeMonoid I) :
koszulOrder r q (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
lemma koszulOrder_single (l : FreeMonoid 𝓕) :
koszulOrder q le (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x))
= FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single (List.insertionSort r l) (koszulSign r q l * x)) := by
(MonoidAlgebra.single (List.insertionSort le l) (koszulSign q le l * x)) := by
simp [koszulOrder]
@[simp]
lemma koszulOrder_ι_pair {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (i j : I) :
koszulOrder r q (FreeAlgebra.ι i * FreeAlgebra.ι j) =
if r i j then FreeAlgebra.ι i * FreeAlgebra.ι j else
(koszulSign r q [i, j]) • (FreeAlgebra.ι j * FreeAlgebra.ι i) := by
lemma koszulOrder_ι_pair (i j : 𝓕) : koszulOrder q le (FreeAlgebra.ι i * FreeAlgebra.ι j) =
if le i j then FreeAlgebra.ι i * FreeAlgebra.ι j else
(koszulSign q le [i, j]) • (FreeAlgebra.ι j * FreeAlgebra.ι i) := by
have h1 : FreeAlgebra.ι i * FreeAlgebra.ι j =
FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [i, j] 1) := by
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
@ -97,11 +94,11 @@ lemma koszulOrder_ι_pair {I : Type} (r : I → I → Prop) [DecidableRel r] (q
LinearMap.coe_comp, Function.comp_apply, AlgEquiv.toLinearMap_apply, AlgEquiv.apply_symm_apply,
koszulOrderMonoidAlgebra_single, List.insertionSort, List.orderedInsert,
MonoidAlgebra.smul_single', mul_one]
by_cases hr : r i j
by_cases hr : le i j
· rw [if_pos hr, if_pos hr]
simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single]
have hKS : koszulSign r q [i, j] = 1 := by
have hKS : koszulSign q le [i, j] = 1 := by
simp only [koszulSign, koszulSignInsert, Fin.isValue, mul_one, ite_eq_left_iff,
ite_eq_right_iff, and_imp]
exact fun a a_1 a_2 => False.elim (a hr)
@ -114,9 +111,8 @@ lemma koszulOrder_ι_pair {I : Type} (r : I → I → Prop) [DecidableRel r] (q
rfl
@[simp]
lemma koszulOrder_one {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
koszulOrder r q 1 = 1 := by
trans koszulOrder r q (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1))
lemma koszulOrder_one : koszulOrder q le 1 = 1 := by
trans koszulOrder q le (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single [] 1))
congr
· simp only [FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
@ -124,16 +120,15 @@ lemma koszulOrder_one {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I
· simp only [koszulOrder_single, List.insertionSort, mul_one, EmbeddingLike.map_eq_one_iff]
rfl
lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(i : I) (A : FreeAlgebra I) (hi : ∀ j, r i j) :
FreeAlgebra.ι i * koszulOrder r q A = koszulOrder r q (FreeAlgebra.ι i * A) := by
let f : FreeAlgebra I →ₗ[] FreeAlgebra I := {
lemma mul_koszulOrder_le (i : 𝓕) (A : FreeAlgebra 𝓕) (hi : ∀ j, le i j) :
FreeAlgebra.ι i * koszulOrder q le A = koszulOrder q le (FreeAlgebra.ι i * A) := by
let f : FreeAlgebra 𝓕 →ₗ[] FreeAlgebra 𝓕 := {
toFun := fun x => FreeAlgebra.ι i * x,
map_add' := fun x y => by
simp [mul_add],
map_smul' := by simp}
change (f ∘ₗ koszulOrder r q) A = (koszulOrder r q ∘ₗ f) _
have f_single (l : FreeMonoid I) (x : ) :
change (f ∘ₗ koszulOrder q le) A = (koszulOrder q le ∘ₗ f) _
have f_single (l : FreeMonoid 𝓕) (x : ) :
f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
= (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single (i :: l) x)) := by
simp only [LinearMap.coe_mk, AddHom.coe_mk, f]
@ -146,8 +141,8 @@ lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
rw [@AlgEquiv.eq_symm_apply]
simp only [map_mul, AlgEquiv.apply_symm_apply, MonoidAlgebra.single_mul_single, one_mul]
rfl
have h1 : f ∘ₗ koszulOrder r q = koszulOrder r q ∘ₗ f := by
let e : FreeAlgebra I ≃ₗ[] MonoidAlgebra (FreeMonoid I) :=
have h1 : f ∘ₗ koszulOrder q le = koszulOrder q le ∘ₗ f := by
let e : FreeAlgebra 𝓕 ≃ₗ[] MonoidAlgebra (FreeMonoid 𝓕) :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
apply MonoidAlgebra.lhom_ext'
@ -162,30 +157,29 @@ lemma mul_koszulOrder_le {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
rw [koszulOrder_single]
congr 2
· simp only [List.insertionSort]
have hi (l : List I) : i :: l = List.orderedInsert r i l := by
have hi (l : List 𝓕) : i :: l = List.orderedInsert le i l := by
induction l with
| nil => rfl
| cons j l ih =>
refine (List.orderedInsert_of_le r l (hi j)).symm
refine (List.orderedInsert_of_le le l (hi j)).symm
exact hi _
· congr 1
rw [koszulSign]
have h1 (l : List I) : koszulSignInsert r q i l = 1 := by
exact koszulSignInsert_le_forall r q i l hi
have h1 (l : List 𝓕) : koszulSignInsert q le i l = 1 := by
exact koszulSignInsert_le_forall q le i l hi
rw [h1]
simp
rw [h1]
lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
(i : I) (A : FreeAlgebra I) (hi : ∀ j, r j i) :
koszulOrder r q A * FreeAlgebra.ι i = koszulOrder r q (A * FreeAlgebra.ι i) := by
let f : FreeAlgebra I →ₗ[] FreeAlgebra I := {
lemma koszulOrder_mul_ge (i : 𝓕) (A : FreeAlgebra 𝓕) (hi : ∀ j, le j i) :
koszulOrder q le A * FreeAlgebra.ι i = koszulOrder q le (A * FreeAlgebra.ι i) := by
let f : FreeAlgebra 𝓕 →ₗ[] FreeAlgebra 𝓕 := {
toFun := fun x => x * FreeAlgebra.ι i,
map_add' := fun x y => by
simp [add_mul],
map_smul' := by simp}
change (f ∘ₗ koszulOrder r q) A = (koszulOrder r q ∘ₗ f) A
have f_single (l : FreeMonoid I) (x : ) :
change (f ∘ₗ koszulOrder q le) A = (koszulOrder q le ∘ₗ f) A
have f_single (l : FreeMonoid 𝓕) (x : ) :
f ((FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)))
= (FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm
(MonoidAlgebra.single (l.toList ++ [i]) x)) := by
@ -199,8 +193,8 @@ lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
rw [@AlgEquiv.eq_symm_apply]
simp only [map_mul, AlgEquiv.apply_symm_apply, MonoidAlgebra.single_mul_single, mul_one]
rfl
have h1 : f ∘ₗ koszulOrder r q = koszulOrder r q ∘ₗ f := by
let e : FreeAlgebra I ≃ₗ[] MonoidAlgebra (FreeMonoid I) :=
have h1 : f ∘ₗ koszulOrder q le = koszulOrder q le ∘ₗ f := by
let e : FreeAlgebra 𝓕 ≃ₗ[] MonoidAlgebra (FreeMonoid 𝓕) :=
FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
apply (LinearEquiv.eq_comp_toLinearMap_iff (e₁₂ := e.symm) _ _).mp
apply MonoidAlgebra.lhom_ext'
@ -214,20 +208,21 @@ lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
erw [f_single]
rw [koszulOrder_single]
congr 3
· change (List.insertionSort r l) ++ [i] = List.insertionSort r (l.toList ++ [i])
have hoi (l : List I) (j : I) : List.orderedInsert r j (l ++ [i]) =
List.orderedInsert r j l ++ [i] := by
· change (List.insertionSort le l) ++ [i] = List.insertionSort le (l.toList ++ [i])
have hoi (l : List 𝓕) (j : 𝓕) : List.orderedInsert le j (l ++ [i]) =
List.orderedInsert le j l ++ [i] := by
induction l with
| nil => simp [hi]
| cons b l ih =>
simp only [List.orderedInsert, List.append_eq]
by_cases hr : r j b
by_cases hr : le j b
· rw [if_pos hr, if_pos hr]
rfl
· rw [if_neg hr, if_neg hr]
rw [ih]
rfl
have hI (l : List I) : (List.insertionSort r l) ++ [i] = List.insertionSort r (l ++ [i]) := by
have hI (l : List 𝓕) : (List.insertionSort le l) ++ [i] =
List.insertionSort le (l ++ [i]) := by
induction l with
| nil => rfl
| cons j l ih =>
@ -236,7 +231,7 @@ lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
rw [hoi]
rw [hI]
rfl
· have hI (l : List I) : koszulSign r q l = koszulSign r q (l ++ [i]) := by
· have hI (l : List 𝓕) : koszulSign q le l = koszulSign q le (l ++ [i]) := by
induction l with
| nil => simp [koszulSign, koszulSignInsert]
| cons j l ih =>
@ -244,7 +239,7 @@ lemma koszulOrder_mul_ge {I : Type} (r : I → I → Prop) [DecidableRel r] (q :
rw [ih]
simp only [mul_eq_mul_right_iff]
apply Or.inl
rw [koszulSignInsert_ge_forall_append r q l j i hi]
rw [koszulSignInsert_ge_forall_append q le l j i hi]
rw [hI]
rfl
rw [h1]