feat: Contractions and involutions
This commit is contained in:
jstoobysmith
parent
bab9f10763
commit
7d1f15e18a
5 changed files with 662 additions and 99 deletions
|
|
@ -17,15 +17,15 @@ open FieldStatistic
|
|||
|
||||
variable {𝓕 : Type}
|
||||
|
||||
/-- Given a list of fields `l`, the type of pairwise-contractions associated with `l`
|
||||
which have the list `aux` uncontracted. -/
|
||||
inductive ContractionsAux : (l : List 𝓕) → (aux : List 𝓕) → Type
|
||||
/-- Given a list of fields `φs`, the type of pairwise-contractions associated with `φs`
|
||||
which have the list `φsᵤₙ` uncontracted. -/
|
||||
inductive ContractionsAux : (φs : List 𝓕) → (φsᵤₙ : List 𝓕) → Type
|
||||
| nil : ContractionsAux [] []
|
||||
| cons {l : List 𝓕} {aux : List 𝓕} {a : 𝓕} (i : Option (Fin aux.length)) :
|
||||
ContractionsAux l aux → ContractionsAux (a :: l) (optionEraseZ aux a i)
|
||||
| cons {φs : List 𝓕} {φsᵤₙ : List 𝓕} {φ : 𝓕} (i : Option (Fin φsᵤₙ.length)) :
|
||||
ContractionsAux φs φsᵤₙ → ContractionsAux (φ :: φs) (optionEraseZ φsᵤₙ φ i)
|
||||
|
||||
/-- Given a list of fields `l`, the type of pairwise-contractions associated with `l`. -/
|
||||
def Contractions (l : List 𝓕) : Type := Σ aux, ContractionsAux l aux
|
||||
def Contractions (φs : List 𝓕) : Type := Σ aux, ContractionsAux φs aux
|
||||
|
||||
namespace Contractions
|
||||
|
||||
|
|
@ -40,6 +40,47 @@ lemma contractions_nil (a : Contractions ([] : List 𝓕)) : a = ⟨[], Contract
|
|||
cases c
|
||||
rfl
|
||||
|
||||
def embedUncontracted {l : List 𝓕} (c : Contractions l) : Fin c.normalize.length → Fin l.length :=
|
||||
match l, c with
|
||||
| [], ⟨[], ContractionsAux.nil⟩ => Fin.elim0
|
||||
| φ :: φs, ⟨_, .cons (φsᵤₙ := aux) none c⟩ =>
|
||||
Fin.cons ⟨0, Nat.zero_lt_succ φs.length⟩ (Fin.succ ∘ (embedUncontracted ⟨aux, c⟩))
|
||||
| φ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some n) c⟩ => by
|
||||
let lc := embedUncontracted ⟨aux, c⟩
|
||||
refine Fin.succ ∘ lc ∘ Fin.cast ?_ ∘ Fin.succAbove ⟨n, by
|
||||
rw [normalize, optionEraseZ_some_length]
|
||||
omega⟩
|
||||
simp only [normalize, optionEraseZ_some_length]
|
||||
have hq : aux.length ≠ 0 := by
|
||||
by_contra hn
|
||||
rw [hn] at n
|
||||
exact Fin.elim0 n
|
||||
omega
|
||||
|
||||
lemma embedUncontracted_injective {l : List 𝓕} (c : Contractions l) :
|
||||
Function.Injective c.embedUncontracted := by
|
||||
match l, c with
|
||||
| [], ⟨[], ContractionsAux.nil⟩ =>
|
||||
dsimp [embedUncontracted]
|
||||
intro i
|
||||
exact Fin.elim0 i
|
||||
| φ :: φs, ⟨_, .cons (φsᵤₙ := aux) none c⟩ =>
|
||||
dsimp [embedUncontracted]
|
||||
refine Fin.cons_injective_iff.mpr ?_
|
||||
apply And.intro
|
||||
· simp only [Set.mem_range, Function.comp_apply, not_exists]
|
||||
exact fun x => Fin.succ_ne_zero (embedUncontracted ⟨aux, c⟩ x)
|
||||
· exact Function.Injective.comp (Fin.succ_injective φs.length)
|
||||
(embedUncontracted_injective ⟨aux, c⟩)
|
||||
| φ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some i) c⟩ =>
|
||||
dsimp [embedUncontracted]
|
||||
refine Function.Injective.comp (Fin.succ_injective φs.length) ?hf
|
||||
refine Function.Injective.comp (embedUncontracted_injective ⟨aux, c⟩) ?hf.hf
|
||||
refine Function.Injective.comp (Fin.cast_injective (embedUncontracted.proof_5 φ φs aux i c))
|
||||
Fin.succAbove_right_injective
|
||||
|
||||
|
||||
|
||||
/-- Establishes uniqueness of contractions for a single field, showing that any contraction
|
||||
of a single field must be equivalent to the trivial contraction with no pairing. -/
|
||||
lemma contractions_single {i : 𝓕} (a : Contractions [i]) : a =
|
||||
|
|
@ -67,46 +108,46 @@ def nilEquiv : Contractions ([] : List 𝓕) ≃ Unit where
|
|||
/-- The equivalence between contractions of `a :: l` and contractions of
|
||||
`Contractions l` paired with an optional element of `Fin (c.normalize).length` specifying
|
||||
what `a` contracts with if any. -/
|
||||
def consEquiv {a : 𝓕} {l : List 𝓕} :
|
||||
Contractions (a :: l) ≃ (c : Contractions l) × Option (Fin (c.normalize).length) where
|
||||
def consEquiv {φ : 𝓕} {φs : List 𝓕} :
|
||||
Contractions (φ :: φs) ≃ (c : Contractions φs) × Option (Fin c.normalize.length) where
|
||||
toFun c :=
|
||||
match c with
|
||||
| ⟨aux, c⟩ =>
|
||||
match c with
|
||||
| ContractionsAux.cons (aux := aux') i c => ⟨⟨aux', c⟩, i⟩
|
||||
| ContractionsAux.cons (φsᵤₙ := aux') i c => ⟨⟨aux', c⟩, i⟩
|
||||
invFun ci :=
|
||||
⟨(optionEraseZ (ci.fst.normalize) a ci.2), ContractionsAux.cons (a := a) ci.2 ci.1.2⟩
|
||||
⟨(optionEraseZ (ci.fst.normalize) φ ci.2), ContractionsAux.cons (φ := φ) ci.2 ci.1.2⟩
|
||||
left_inv c := by
|
||||
match c with
|
||||
| ⟨aux, c⟩ =>
|
||||
match c with
|
||||
| ContractionsAux.cons (aux := aux') i c => rfl
|
||||
| ContractionsAux.cons (φsᵤₙ := aux') i c => rfl
|
||||
right_inv ci := by rfl
|
||||
|
||||
/-- The type of contractions is decidable. -/
|
||||
instance decidable : (l : List 𝓕) → DecidableEq (Contractions l)
|
||||
instance decidable : (φs : List 𝓕) → DecidableEq (Contractions φs)
|
||||
| [] => fun a b =>
|
||||
match a, b with
|
||||
| ⟨_, a⟩, ⟨_, b⟩ =>
|
||||
match a, b with
|
||||
| ContractionsAux.nil, ContractionsAux.nil => isTrue rfl
|
||||
| _ :: l =>
|
||||
haveI : DecidableEq (Contractions l) := decidable l
|
||||
haveI : DecidableEq ((c : Contractions l) × Option (Fin (c.normalize).length)) :=
|
||||
| _ :: φs =>
|
||||
haveI : DecidableEq (Contractions φs) := decidable φs
|
||||
haveI : DecidableEq ((c : Contractions φs) × Option (Fin (c.normalize).length)) :=
|
||||
Sigma.instDecidableEqSigma
|
||||
Equiv.decidableEq consEquiv
|
||||
|
||||
/-- The type of contractions is finite. -/
|
||||
instance fintype : (l : List 𝓕) → Fintype (Contractions l)
|
||||
instance fintype : (φs : List 𝓕) → Fintype (Contractions φs)
|
||||
| [] => {
|
||||
elems := {⟨[], ContractionsAux.nil⟩}
|
||||
complete := by
|
||||
intro a
|
||||
rw [Finset.mem_singleton]
|
||||
exact contractions_nil a}
|
||||
| a :: l =>
|
||||
haveI : Fintype (Contractions l) := fintype l
|
||||
haveI : Fintype ((c : Contractions l) × Option (Fin (c.normalize).length)) :=
|
||||
| φ :: φs =>
|
||||
haveI : Fintype (Contractions φs) := fintype φs
|
||||
haveI : Fintype ((c : Contractions φs) × Option (Fin (c.normalize).length)) :=
|
||||
Sigma.instFintype
|
||||
Fintype.ofEquiv _ consEquiv.symm
|
||||
|
||||
|
|
@ -120,10 +161,525 @@ instance isFull_decidable : Decidable c.IsFull := by
|
|||
simp [IsFull]
|
||||
apply decidable_of_decidable_of_iff hn.symm
|
||||
|
||||
def toOptionList : {l : List 𝓕} → (c : Contractions l) → List (Option (Fin l.length))
|
||||
| [], ⟨[], ContractionsAux.nil⟩ => []
|
||||
| _ :: _, ⟨_, .cons (φsᵤₙ := aux) none c⟩ => none ::
|
||||
List.map (Option.map Fin.succ) (toOptionList ⟨aux, c⟩)
|
||||
| _ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some n) c⟩ =>
|
||||
some (Fin.succ (embedUncontracted ⟨aux, c⟩ n)) ::
|
||||
List.set ((List.map (Option.map Fin.succ) (toOptionList ⟨aux, c⟩)))
|
||||
(embedUncontracted ⟨aux, c⟩ n) (some ⟨0, Nat.zero_lt_succ φs.length⟩)
|
||||
|
||||
lemma toOptionList_length {l : List 𝓕} (c : Contractions l) : c.toOptionList.length = l.length := by
|
||||
match l, c with
|
||||
| [], ⟨[], ContractionsAux.nil⟩ =>
|
||||
dsimp [toOptionList]
|
||||
| _ :: _, ⟨_, .cons (φsᵤₙ := aux) none c⟩ =>
|
||||
dsimp [toOptionList]
|
||||
rw [List.length_map, toOptionList_length ⟨aux, c⟩]
|
||||
| _ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some n) c⟩ =>
|
||||
dsimp [toOptionList]
|
||||
rw [List.length_set, List.length_map, toOptionList_length ⟨aux, c⟩]
|
||||
|
||||
def toFinOptionMap {l : List 𝓕} (c : Contractions l) : Fin l.length → Option (Fin l.length) :=
|
||||
c.toOptionList.get ∘ Fin.cast (toOptionList_length c).symm
|
||||
|
||||
lemma toFinOptionMap_neq_self {l : List 𝓕} (c : Contractions l) (i : Fin l.length) :
|
||||
c.toFinOptionMap i ≠ some i := by
|
||||
match l, c with
|
||||
| [], ⟨[], ContractionsAux.nil⟩ =>
|
||||
exact Fin.elim0 i
|
||||
| _ :: _, ⟨_, .cons (φsᵤₙ := aux) none c⟩ =>
|
||||
dsimp [toFinOptionMap, toOptionList]
|
||||
match i with
|
||||
| ⟨0, _⟩ =>
|
||||
exact Option.noConfusion
|
||||
| ⟨n + 1, h⟩ =>
|
||||
simp only [List.getElem_cons_succ, List.getElem_map, List.length_cons]
|
||||
have hn := toFinOptionMap_neq_self ⟨aux, c⟩ ⟨n, Nat.succ_lt_succ_iff.mp h⟩
|
||||
simp only [Option.map_eq_some', not_exists, not_and]
|
||||
intro x hx
|
||||
simp only [toFinOptionMap, Function.comp_apply, Fin.cast_mk, List.get_eq_getElem, hx, ne_eq,
|
||||
Option.some.injEq] at hn
|
||||
rw [Fin.ext_iff] at hn ⊢
|
||||
simp_all
|
||||
| _ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some n) c⟩ =>
|
||||
dsimp [toFinOptionMap, toOptionList]
|
||||
match i with
|
||||
| ⟨0, _⟩ =>
|
||||
simp only [List.getElem_cons_zero, List.length_cons, Fin.zero_eta, Option.some.injEq, ne_eq]
|
||||
exact Fin.succ_ne_zero (embedUncontracted ⟨aux, c⟩ n)
|
||||
| ⟨n + 1, h⟩ =>
|
||||
simp only [List.getElem_cons_succ, List.length_cons, ne_eq]
|
||||
rw [List.getElem_set]
|
||||
split
|
||||
· exact ne_of_beq_false rfl
|
||||
· simp only [List.getElem_map, Option.map_eq_some', not_exists, not_and]
|
||||
intro x hx
|
||||
have hn := toFinOptionMap_neq_self ⟨aux, c⟩ ⟨n, Nat.succ_lt_succ_iff.mp h⟩
|
||||
simp only [toFinOptionMap, Function.comp_apply, Fin.cast_mk, List.get_eq_getElem, hx, ne_eq,
|
||||
Option.some.injEq] at hn
|
||||
rw [Fin.ext_iff] at hn ⊢
|
||||
simp_all
|
||||
|
||||
@[simp]
|
||||
lemma toFinOptionMap_embedUncontracted {l : List 𝓕} (c : Contractions l)
|
||||
(i : Fin c.normalize.length) : c.toFinOptionMap (embedUncontracted c i) = none := by
|
||||
match l, c with
|
||||
| [], ⟨[], ContractionsAux.nil⟩ =>
|
||||
exact Fin.elim0 i
|
||||
| _ :: _, ⟨_, .cons (φsᵤₙ := aux) none c⟩ =>
|
||||
dsimp [toFinOptionMap, toOptionList, embedUncontracted]
|
||||
match i with
|
||||
| ⟨0, _⟩ =>
|
||||
rfl
|
||||
| ⟨n + 1, h⟩ =>
|
||||
rw [show ⟨n + 1, h⟩ = Fin.succ ⟨n, Nat.succ_lt_succ_iff.mp h⟩ by rfl]
|
||||
rw [Fin.cons_succ]
|
||||
simp only [Function.comp_apply, Fin.val_succ, List.getElem_cons_succ, List.getElem_map,
|
||||
Option.map_eq_none']
|
||||
exact toFinOptionMap_embedUncontracted ⟨aux, c⟩ ⟨n, Nat.succ_lt_succ_iff.mp h⟩
|
||||
| _ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some n) c⟩ =>
|
||||
dsimp [toFinOptionMap, toOptionList, embedUncontracted]
|
||||
rw [List.getElem_set]
|
||||
split
|
||||
· rename_i hs
|
||||
have hx := embedUncontracted_injective ⟨aux, c⟩ (Fin.val_injective hs)
|
||||
refine False.elim ?_
|
||||
have hn := Fin.succAbove_ne ⟨n, embedUncontracted.proof_6 _ φs aux n c⟩ i
|
||||
simp [Fin.ext_iff] at hx
|
||||
simp [Fin.ext_iff] at hn
|
||||
exact hn (id (Eq.symm hx))
|
||||
· simp
|
||||
exact toFinOptionMap_embedUncontracted ⟨aux, c⟩ _
|
||||
|
||||
lemma toFinOptionMap_involutive {l : List 𝓕} (c : Contractions l) (i j : Fin l.length) :
|
||||
c.toFinOptionMap i = some j → c.toFinOptionMap j = some i := by
|
||||
match l, c with
|
||||
| [], ⟨[], ContractionsAux.nil⟩ =>
|
||||
exact Fin.elim0 i
|
||||
| _ :: _, ⟨_, .cons (φsᵤₙ := aux) none c⟩ =>
|
||||
dsimp [toFinOptionMap, toOptionList]
|
||||
match i, j with
|
||||
| ⟨0, _⟩, j =>
|
||||
exact Option.noConfusion
|
||||
| ⟨n + 1, h⟩, ⟨0, _⟩ =>
|
||||
simp
|
||||
intro x hx
|
||||
exact Fin.succ_ne_zero x
|
||||
| ⟨n + 1, hn⟩, ⟨m + 1, hm⟩ =>
|
||||
intro h1
|
||||
have hnm := toFinOptionMap_involutive ⟨aux, c⟩ ⟨n, Nat.succ_lt_succ_iff.mp hn⟩
|
||||
⟨m, Nat.succ_lt_succ_iff.mp hm⟩
|
||||
simp
|
||||
simp [toFinOptionMap] at hnm
|
||||
have hnm' := hnm (by
|
||||
simp at h1
|
||||
obtain ⟨a, ha, ha2⟩ := h1
|
||||
rw [ha]
|
||||
simp only [Option.some.injEq]
|
||||
rw [Fin.ext_iff] at ha2 ⊢
|
||||
simp_all)
|
||||
use ⟨n, Nat.succ_lt_succ_iff.mp hn⟩
|
||||
simpa using hnm'
|
||||
| _ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some n) c⟩ =>
|
||||
dsimp [toFinOptionMap, toOptionList]
|
||||
match i, j with
|
||||
| ⟨0, _⟩, j =>
|
||||
intro hj
|
||||
simp only [List.getElem_cons_zero, Option.some.injEq] at hj
|
||||
subst hj
|
||||
simp
|
||||
| ⟨n' + 1, h⟩, ⟨0, _⟩ =>
|
||||
intro hj
|
||||
simp at hj
|
||||
simp
|
||||
rw [List.getElem_set] at hj
|
||||
simp_all only [List.length_cons, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true, List.getElem_map,
|
||||
ite_eq_left_iff, Option.map_eq_some']
|
||||
simp [Fin.ext_iff]
|
||||
by_contra hn
|
||||
have hn' := hj hn
|
||||
obtain ⟨a, ha, ha2⟩ := hn'
|
||||
exact Fin.succ_ne_zero a ha2
|
||||
| ⟨n' + 1, hn⟩, ⟨m + 1, hm⟩ =>
|
||||
simp
|
||||
rw [List.getElem_set, List.getElem_set]
|
||||
simp
|
||||
split
|
||||
· intro h
|
||||
simp [Fin.ext_iff] at h
|
||||
rename_i hn'
|
||||
intro h1
|
||||
split
|
||||
· rename_i hnx
|
||||
have hnm := toFinOptionMap_involutive ⟨aux, c⟩ ⟨n', Nat.succ_lt_succ_iff.mp hn⟩
|
||||
⟨m, Nat.succ_lt_succ_iff.mp hm⟩
|
||||
subst hnx
|
||||
simp at hnm
|
||||
refine False.elim (hnm ?_)
|
||||
simp at h1
|
||||
obtain ⟨a, ha, ha2⟩ := h1
|
||||
have ha' : (embedUncontracted ⟨aux, c⟩ n) = a := by
|
||||
rw [Fin.ext_iff] at ha2 ⊢
|
||||
simp_all
|
||||
rw [ha']
|
||||
rw [← ha]
|
||||
rfl
|
||||
· rename_i hnx
|
||||
have hnm := toFinOptionMap_involutive ⟨aux, c⟩ ⟨n', Nat.succ_lt_succ_iff.mp hn⟩
|
||||
⟨m, Nat.succ_lt_succ_iff.mp hm⟩ (by
|
||||
dsimp [toFinOptionMap]
|
||||
simp at h1
|
||||
obtain ⟨a, ha, ha2⟩ := h1
|
||||
have ha' : a = ⟨m, by exact Nat.succ_lt_succ_iff.mp hm⟩ := by
|
||||
rw [Fin.ext_iff] at ha2 ⊢
|
||||
simp_all
|
||||
rw [← ha', ← ha])
|
||||
change Option.map Fin.succ (toFinOptionMap ⟨aux, c⟩ ⟨m, Nat.succ_lt_succ_iff.mp hm⟩) = _
|
||||
rw [hnm]
|
||||
rfl
|
||||
|
||||
def toInvolution {l : List 𝓕} (c : Contractions l) : Fin l.length → Fin l.length :=
|
||||
fun i =>
|
||||
if h : Option.isSome (c.toFinOptionMap i) then Option.get (c.toFinOptionMap i) h else i
|
||||
|
||||
lemma toInvolution_of_isSome {l : List 𝓕} {c : Contractions l} {i : Fin l.length}
|
||||
(hs : Option.isSome (c.toFinOptionMap i)) :
|
||||
c.toInvolution i = Option.get (c.toFinOptionMap i) hs := by
|
||||
dsimp [toInvolution]
|
||||
rw [dif_pos hs]
|
||||
|
||||
lemma toInvolution_of_eq_none {l : List 𝓕} {c : Contractions l} {i : Fin l.length}
|
||||
(hs : (c.toFinOptionMap i) = none) :
|
||||
c.toInvolution i = i := by
|
||||
dsimp [toInvolution]
|
||||
rw [dif_neg]
|
||||
simp_all
|
||||
|
||||
lemma toInvolution_image_isSome {l : List 𝓕} {c : Contractions l} {i : Fin l.length}
|
||||
(hs : Option.isSome (c.toFinOptionMap i)) :
|
||||
Option.isSome (c.toFinOptionMap (c.toInvolution i)) := by
|
||||
dsimp [toInvolution]
|
||||
rw [dif_pos hs]
|
||||
have hx := toFinOptionMap_involutive c i ((c.toFinOptionMap i).get hs)
|
||||
simp at hx
|
||||
rw [hx]
|
||||
rfl
|
||||
|
||||
lemma toInvolution_involutive {l : List 𝓕} (c : Contractions l) :
|
||||
Function.Involutive c.toInvolution := by
|
||||
intro i
|
||||
by_cases h : Option.isSome (c.toFinOptionMap i)
|
||||
· have hx := toFinOptionMap_involutive c i ((c.toFinOptionMap i).get h)
|
||||
rw [toInvolution_of_isSome (toInvolution_image_isSome h)]
|
||||
simp only [Option.some_get, forall_const] at hx
|
||||
simp only [toInvolution_of_isSome h, hx, Option.get_some]
|
||||
· simp at h
|
||||
rw [toInvolution_of_eq_none h]
|
||||
rw [toInvolution_of_eq_none h]
|
||||
|
||||
def involutionEquiv1 {l : List 𝓕} :
|
||||
{f : Fin l.length → Fin l.length // Function.Involutive f } ≃
|
||||
{f : Fin l.length → Option (Fin l.length) // (∀ i, f i ≠ some i) ∧
|
||||
∀ i j, f i = some j → f j = some i} where
|
||||
toFun f := ⟨fun i => if h : f.1 i = i then none else f.1 i,
|
||||
fun i => by
|
||||
simp,
|
||||
fun i j => by
|
||||
simp
|
||||
intro hi hij
|
||||
subst hij
|
||||
rw [f.2]
|
||||
simp
|
||||
exact fun a => hi (id (Eq.symm a))⟩
|
||||
invFun f := ⟨fun i => if h : (f.1 i).isSome then Option.get (f.1 i) h else i,
|
||||
fun i => by
|
||||
by_cases h : Option.isSome (f.1 i)
|
||||
· simp [h]
|
||||
have hf := f.2.2 i (Option.get (f.1 i) h) (by simp)
|
||||
simp [hf]
|
||||
· simp
|
||||
rw [dif_neg]
|
||||
· rw [dif_neg h]
|
||||
· rw [dif_neg h]
|
||||
exact h⟩
|
||||
left_inv f := by
|
||||
simp
|
||||
ext i
|
||||
simp
|
||||
by_cases hf : f.1 i = i
|
||||
· simp [hf]
|
||||
· simp [hf]
|
||||
right_inv f := by
|
||||
simp
|
||||
ext1
|
||||
simp
|
||||
funext i
|
||||
obtain ⟨val, property⟩ := f
|
||||
obtain ⟨left, right⟩ := property
|
||||
simp_all only [ne_eq]
|
||||
split
|
||||
next h =>
|
||||
ext a : 1
|
||||
simp_all only [Option.mem_def, reduceCtorEq, false_iff]
|
||||
apply Aesop.BuiltinRules.not_intro
|
||||
intro a_1
|
||||
simp_all only [Option.isSome_some, Option.get_some, forall_const]
|
||||
next h =>
|
||||
simp_all only [not_forall]
|
||||
obtain ⟨w, h⟩ := h
|
||||
simp_all only [↓reduceDIte, Option.some_get]
|
||||
|
||||
def involutionCons (n : ℕ):
|
||||
{f : Fin n.succ → Fin n.succ // Function.Involutive f } ≃
|
||||
(f : {f : Fin n → Fin n // Function.Involutive f}) × {i : Option (Fin n) //
|
||||
∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)} where
|
||||
toFun f := ⟨⟨
|
||||
fun i =>
|
||||
if h : f.1 i.succ = 0 then i
|
||||
else Fin.pred (f.1 i.succ) h , by
|
||||
intro i
|
||||
by_cases h : f.1 i.succ = 0
|
||||
· simp [h]
|
||||
· simp [h]
|
||||
simp [f.2 i.succ]
|
||||
intro h
|
||||
exact False.elim (Fin.succ_ne_zero i h)⟩,
|
||||
⟨if h : f.1 0 = 0 then none else Fin.pred (f.1 0) h , by
|
||||
by_cases h0 : f.1 0 = 0
|
||||
· simp [h0]
|
||||
· simp [h0]
|
||||
refine fun h => False.elim (h (f.2 0))⟩⟩
|
||||
invFun f := ⟨
|
||||
if h : (f.2.1).isSome then
|
||||
Fin.cons (f.2.1.get h).succ (Function.update (Fin.succ ∘ f.1.1) (f.2.1.get h) 0)
|
||||
else
|
||||
Fin.cons 0 (Fin.succ ∘ f.1.1)
|
||||
, by
|
||||
by_cases hs : (f.2.1).isSome
|
||||
· simp only [Nat.succ_eq_add_one, hs, ↓reduceDIte, Fin.coe_eq_castSucc]
|
||||
let a := f.2.1.get hs
|
||||
change Function.Involutive (Fin.cons a.succ (Function.update (Fin.succ ∘ ↑f.fst) a 0))
|
||||
intro i
|
||||
rcases Fin.eq_zero_or_eq_succ i with hi | ⟨j, hj⟩
|
||||
· subst hi
|
||||
rw [Fin.cons_zero, Fin.cons_succ]
|
||||
simp
|
||||
· subst hj
|
||||
rw [Fin.cons_succ]
|
||||
by_cases hja : j = a
|
||||
· subst hja
|
||||
simp
|
||||
· rw [Function.update_apply ]
|
||||
rw [if_neg hja]
|
||||
simp
|
||||
have hf2 := f.2.2 hs
|
||||
change f.1.1 a = a at hf2
|
||||
have hjf1 : f.1.1 j ≠ a := by
|
||||
by_contra hn
|
||||
have haj : j = f.1.1 a := by
|
||||
rw [← hn]
|
||||
rw [f.1.2]
|
||||
rw [hf2] at haj
|
||||
exact hja haj
|
||||
rw [Function.update_apply, if_neg hjf1]
|
||||
simp
|
||||
rw [f.1.2]
|
||||
· simp [hs]
|
||||
intro i
|
||||
rcases Fin.eq_zero_or_eq_succ i with hi | ⟨j, hj⟩
|
||||
· subst hi
|
||||
simp
|
||||
· subst hj
|
||||
simp
|
||||
rw [f.1.2]⟩
|
||||
left_inv f := by
|
||||
match f with
|
||||
| ⟨f, hf⟩ =>
|
||||
simp
|
||||
ext i
|
||||
by_cases h0 : f 0 = 0
|
||||
· simp [h0]
|
||||
rcases Fin.eq_zero_or_eq_succ i with hi | ⟨j, hj⟩
|
||||
· subst hi
|
||||
simp [h0]
|
||||
· subst hj
|
||||
simp [h0]
|
||||
by_cases hj : f j.succ =0
|
||||
· rw [← h0] at hj
|
||||
have hn := Function.Involutive.injective hf hj
|
||||
exact False.elim (Fin.succ_ne_zero j hn)
|
||||
· simp [hj]
|
||||
rw [Fin.ext_iff] at hj
|
||||
simp at hj
|
||||
omega
|
||||
· rw [if_neg h0]
|
||||
by_cases hf' : i = f 0
|
||||
· subst hf'
|
||||
simp
|
||||
rw [hf]
|
||||
simp
|
||||
· rw [Function.update_apply, if_neg hf']
|
||||
rcases Fin.eq_zero_or_eq_succ i with hi | ⟨j, hj⟩
|
||||
· subst hi
|
||||
simp
|
||||
· subst hj
|
||||
simp
|
||||
by_cases hj : f j.succ =0
|
||||
· rw [← hj] at hf'
|
||||
rw [hf] at hf'
|
||||
simp at hf'
|
||||
· simp [hj]
|
||||
rw [Fin.ext_iff] at hj
|
||||
simp at hj
|
||||
omega
|
||||
right_inv f := by
|
||||
match f with
|
||||
| ⟨⟨f, hf⟩, ⟨f0, hf0⟩⟩ =>
|
||||
ext i
|
||||
· simp
|
||||
by_cases hs : f0.isSome
|
||||
· simp [hs]
|
||||
by_cases hi : i = f0.get hs
|
||||
· simp [hi, Function.update_apply]
|
||||
exact Eq.symm (Fin.val_eq_of_eq (hf0 hs))
|
||||
· simp [hi]
|
||||
split
|
||||
· rename_i h
|
||||
exact False.elim (Fin.succ_ne_zero (f i) h)
|
||||
· rfl
|
||||
· simp [hs]
|
||||
split
|
||||
· rename_i h
|
||||
exact False.elim (Fin.succ_ne_zero (f i) h)
|
||||
· rfl
|
||||
· simp only [Nat.succ_eq_add_one, Option.mem_def,
|
||||
Option.dite_none_left_eq_some, Option.some.injEq]
|
||||
by_cases hs : f0.isSome
|
||||
· simp only [hs, ↓reduceDIte]
|
||||
simp [Fin.cons_zero]
|
||||
have hx : ¬ (f0.get hs).succ = 0 := (Fin.succ_ne_zero (f0.get hs))
|
||||
simp [hx]
|
||||
refine Iff.intro (fun hi => ?_) (fun hi => ?_)
|
||||
· rw [← hi]
|
||||
exact
|
||||
Option.eq_some_of_isSome
|
||||
(Eq.mpr_prop (Eq.refl (f0.isSome = true))
|
||||
(of_eq_true (Eq.trans (congrArg (fun x => x = true) hs) (eq_self true))))
|
||||
· subst hi
|
||||
exact rfl
|
||||
· simp [hs]
|
||||
simp at hs
|
||||
subst hs
|
||||
exact ne_of_beq_false rfl
|
||||
|
||||
def uncontractedFromInduction : {l : List 𝓕} → (f : {f : Fin l.length → Fin l.length // Function.Involutive f}) →
|
||||
List 𝓕
|
||||
| [], _ => []
|
||||
| φ :: φs, f =>
|
||||
let f' := involutionCons φs.length f
|
||||
let c' := uncontractedFromInduction f'.1
|
||||
if f'.2.1.isSome then
|
||||
c'
|
||||
else
|
||||
φ :: c'
|
||||
|
||||
lemma uncontractedFromInduction_length : {l : List 𝓕} → (f : {f : Fin l.length → Fin l.length // Function.Involutive f}) →
|
||||
(uncontractedFromInduction f).length = ∑ i, if f.1 i = i then 1 else 0
|
||||
| [] => by
|
||||
intro f
|
||||
rfl
|
||||
| φ :: φs => by
|
||||
intro f
|
||||
let f' := involutionCons φs.length f
|
||||
let c' := uncontractedFromInduction f'.1
|
||||
by_cases h : f'.2.1.isSome
|
||||
· dsimp [uncontractedFromInduction]
|
||||
rw [if_pos h]
|
||||
rw [uncontractedFromInduction_length f'.1]
|
||||
rw [Fin.sum_univ_succ]
|
||||
simp [f', involutionCons] at h
|
||||
rw [if_neg h]
|
||||
simp
|
||||
sorry
|
||||
· sorry
|
||||
|
||||
|
||||
|
||||
|
||||
def uncontractedEquiv {l : List 𝓕} (f : {f : Fin l.length → Fin l.length // Function.Involutive f}) :
|
||||
{i : Option (Fin l.length) //
|
||||
∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)} ≃
|
||||
Option (Fin (uncontractedFromInduction f).length) := by
|
||||
let e1 : {i : Option (Fin l.length) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)}
|
||||
≃ Option {i : Fin l.length // f.1 i = i} :=
|
||||
{ toFun := fun i => match i with
|
||||
| ⟨some i, h⟩ => some ⟨i, by simpa using h⟩
|
||||
| ⟨none, h⟩ => none
|
||||
invFun := fun i => match i with
|
||||
| some ⟨i, h⟩ => ⟨some i, by simpa using h⟩
|
||||
| none => ⟨none, by simp⟩
|
||||
left_inv := by
|
||||
intro a
|
||||
cases a
|
||||
aesop
|
||||
right_inv := by
|
||||
intro a
|
||||
cases a
|
||||
rfl
|
||||
simp_all only [Subtype.coe_eta] }
|
||||
let s : Finset (Fin l.length) := Finset.univ.filter fun i => f.1 i = i
|
||||
let e2' : { i : Fin l.length // f.1 i = i} ≃ {i // i ∈ s} := by
|
||||
refine Equiv.subtypeEquivProp ?h
|
||||
funext i
|
||||
simp [s]
|
||||
let e2 : {i // i ∈ s} ≃ Fin (Finset.card s) := by
|
||||
refine (Finset.orderIsoOfFin _ ?_).symm.toEquiv
|
||||
simp [s]
|
||||
have hcard : (uncontractedFromInduction f).length = Finset.card s := by
|
||||
simp [s]
|
||||
rw [Finset.card_filter]
|
||||
rw [uncontractedFromInduction_length]
|
||||
sorry
|
||||
|
||||
|
||||
|
||||
|
||||
def involutionEquiv : (l : List 𝓕) → Contractions l ≃
|
||||
{f : Fin l.length → Fin l.length // Function.Involutive f}
|
||||
| [] => {
|
||||
toFun := fun c => ⟨fun i => i, fun i => rfl⟩,
|
||||
invFun := fun f => ⟨[], ContractionsAux.nil⟩,
|
||||
left_inv := by
|
||||
intro a
|
||||
cases a
|
||||
rename_i aux c
|
||||
cases c
|
||||
rfl
|
||||
right_inv := by
|
||||
intro f
|
||||
ext i
|
||||
exact Fin.elim0 i}
|
||||
| φ :: φs => by
|
||||
refine Equiv.trans consEquiv ?_
|
||||
refine Equiv.trans ?_ (involutionCons φs.length).symm
|
||||
refine Equiv.sigmaCongr (involutionEquiv φs) (fun c => ?_)
|
||||
exact {
|
||||
toFun := fun i? => ⟨Option.map c.embedUncontracted i?, by
|
||||
intro h
|
||||
|
||||
sorry⟩
|
||||
invFun := fun i => sorry
|
||||
left_inv := by
|
||||
sorry
|
||||
right_inv := by sorry
|
||||
}
|
||||
|
||||
/-- A structure specifying when a type `I` and a map `f :I → Type` corresponds to
|
||||
the splitting of a fields `φ` into a creation `n` and annihlation part `p`. -/
|
||||
structure Splitting (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] where
|
||||
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le] where
|
||||
/-- The creation part of the fields. The label `n` corresponds to the fact that
|
||||
in normal ordering these feilds get pushed to the negative (left) direction. -/
|
||||
𝓑n : 𝓕 → (Σ i, f i)
|
||||
|
|
@ -135,22 +691,23 @@ structure Splitting (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
|||
/-- The complex coefficent of annhilation part of a field `i`. This is usually `0` or `1`. -/
|
||||
𝓧p : 𝓕 → ℂ
|
||||
h𝓑 : ∀ i, ofListLift f [i] 1 = ofList [𝓑n i] (𝓧n i) + ofList [𝓑p i] (𝓧p i)
|
||||
h𝓑n : ∀ i j, le1 (𝓑n i) j
|
||||
h𝓑p : ∀ i j, le1 j (𝓑p i)
|
||||
h𝓑n : ∀ i j, le (𝓑n i) j
|
||||
h𝓑p : ∀ i j, le j (𝓑p i)
|
||||
|
||||
/-- In the static wick's theorem, the term associated with a contraction `c` containing
|
||||
the contractions. -/
|
||||
noncomputable def toCenterTerm (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
||||
(q : 𝓕 → FieldStatistic)
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A) :
|
||||
{r : List 𝓕} → (c : Contractions r) → (S : Splitting f le1) → A
|
||||
{φs : List 𝓕} → (c : Contractions φs) → (S : Splitting f le) → A
|
||||
| [], ⟨[], .nil⟩, _ => 1
|
||||
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S
|
||||
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S *
|
||||
| _ :: _, ⟨_, .cons (φsᵤₙ := aux') none c⟩, S => toCenterTerm f q le F ⟨aux', c⟩ S
|
||||
| a :: _, ⟨_, .cons (φsᵤₙ := aux') (some n) c⟩, S => toCenterTerm f q le F ⟨aux', c⟩ S *
|
||||
superCommuteCoef q [aux'.get n] (List.take (↑n) aux') •
|
||||
F (((superCommute fun i => q i.fst) (ofList [S.𝓑p a] (S.𝓧p a))) (ofListLift f [aux'.get n] 1))
|
||||
F (((superCommute fun i => q i.fst) (ofList [S.𝓑p a] (S.𝓧p a)))
|
||||
(ofListLift f [aux'.get n] 1))
|
||||
|
||||
/-- Shows that adding a field with no contractions (none) to an existing set of contractions
|
||||
results in the same center term as the original contractions.
|
||||
|
|
@ -158,13 +715,13 @@ noncomputable def toCenterTerm (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
|||
Physically, this represents that an uncontracted (free) field does not affect
|
||||
the contraction structure of other fields in Wick's theorem. -/
|
||||
lemma toCenterTerm_none (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
||||
(q : 𝓕 → FieldStatistic) {r : List 𝓕}
|
||||
(le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
|
||||
(q : 𝓕 → FieldStatistic) {φs : List 𝓕}
|
||||
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A)
|
||||
(S : Splitting f le1) (a : 𝓕) (c : Contractions r) :
|
||||
toCenterTerm (r := a :: r) f q le1 F (Contractions.consEquiv.symm ⟨c, none⟩) S =
|
||||
toCenterTerm f q le1 F c S := by
|
||||
(S : Splitting f le) (φ : 𝓕) (c : Contractions φs) :
|
||||
toCenterTerm (φs := φ :: φs) f q le F (Contractions.consEquiv.symm ⟨c, none⟩) S =
|
||||
toCenterTerm f q le F c S := by
|
||||
rw [consEquiv]
|
||||
simp only [Equiv.coe_fn_symm_mk]
|
||||
dsimp [toCenterTerm]
|
||||
|
|
@ -177,15 +734,15 @@ lemma toCenterTerm_center (f : 𝓕 → Type) [∀ i, Fintype (f i)]
|
|||
(le : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A]
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F] :
|
||||
{r : List 𝓕} → (c : Contractions r) → (S : Splitting f le) →
|
||||
{φs : List 𝓕} → (c : Contractions φs) → (S : Splitting f le) →
|
||||
(c.toCenterTerm f q le F S) ∈ Subalgebra.center ℂ A
|
||||
| [], ⟨[], .nil⟩, _ => by
|
||||
dsimp [toCenterTerm]
|
||||
exact Subalgebra.one_mem (Subalgebra.center ℂ A)
|
||||
| _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => by
|
||||
| _ :: _, ⟨_, .cons (φsᵤₙ := aux') none c⟩, S => by
|
||||
dsimp [toCenterTerm]
|
||||
exact toCenterTerm_center f q le F ⟨aux', c⟩ S
|
||||
| a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => by
|
||||
| a :: _, ⟨_, .cons (φsᵤₙ := aux') (some n) c⟩, S => by
|
||||
dsimp [toCenterTerm]
|
||||
refine Subalgebra.mul_mem (Subalgebra.center ℂ A) ?hx ?hy
|
||||
exact toCenterTerm_center f q le F ⟨aux', c⟩ S
|
||||
|
|
|
|||
|
|
@ -14,37 +14,37 @@ namespace Wick
|
|||
open HepLean.List
|
||||
open FieldStatistic
|
||||
|
||||
/-- The sections of `Σ i, f i` over a list `l : List 𝓕`.
|
||||
/-- The sections of `Σ i, f i` over a list `φs : List 𝓕`.
|
||||
In terms of physics, given some fields `φ₁...φₙ`, the different ways one can associate
|
||||
each field as a `creation` or an `annilation` operator. E.g. the number of terms
|
||||
`φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation
|
||||
operators at this point (e.g. ansymptotic states) this is accounted for. -/
|
||||
def CreateAnnihilateSect {𝓕 : Type} (f : 𝓕 → Type) (l : List 𝓕) : Type :=
|
||||
Π i, f (l.get i)
|
||||
def CreateAnnihilateSect {𝓕 : Type} (f : 𝓕 → Type) (φs : List 𝓕) : Type :=
|
||||
Π i, f (φs.get i)
|
||||
|
||||
namespace CreateAnnihilateSect
|
||||
|
||||
section basic_defs
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {l : List 𝓕} (a : CreateAnnihilateSect f l)
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {φs : List 𝓕} (a : CreateAnnihilateSect f φs)
|
||||
|
||||
/-- The type `CreateAnnihilateSect f l` is finite. -/
|
||||
instance fintype : Fintype (CreateAnnihilateSect f l) := Pi.fintype
|
||||
/-- The type `CreateAnnihilateSect f φs` is finite. -/
|
||||
instance fintype : Fintype (CreateAnnihilateSect f φs) := Pi.fintype
|
||||
|
||||
/-- The section got by dropping the first element of `l` if it exists. -/
|
||||
def tail : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → CreateAnnihilateSect f l.tail
|
||||
/-- The section got by dropping the first element of `φs` if it exists. -/
|
||||
def tail : {φs : List 𝓕} → (a : CreateAnnihilateSect f φs) → CreateAnnihilateSect f φs.tail
|
||||
| [], a => a
|
||||
| _ :: _, a => fun i => a (Fin.succ i)
|
||||
|
||||
/-- For a list of fields `i :: l` the value of the section at the head `i`. -/
|
||||
def head {i : 𝓕} (a : CreateAnnihilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
|
||||
def head {φ : 𝓕} (a : CreateAnnihilateSect f (φ :: φs)) : f φ := a ⟨0, Nat.zero_lt_succ φs.length⟩
|
||||
|
||||
end basic_defs
|
||||
|
||||
section toList_basic
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} (q : 𝓕 → FieldStatistic)
|
||||
{l : List 𝓕} (a : CreateAnnihilateSect f l)
|
||||
{φs : List 𝓕} (a : CreateAnnihilateSect f φs)
|
||||
|
||||
/-- The list `List (Σ i, f i)` defined by `a`. -/
|
||||
def toList : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → List (Σ i, f i)
|
||||
|
|
@ -52,8 +52,8 @@ def toList : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → List (Σ i,
|
|||
| i :: _, a => ⟨i, a.head⟩ :: toList a.tail
|
||||
|
||||
@[simp]
|
||||
lemma toList_length : (toList a).length = l.length := by
|
||||
induction l with
|
||||
lemma toList_length : (toList a).length = φs.length := by
|
||||
induction φs with
|
||||
| nil => rfl
|
||||
| cons i l ih =>
|
||||
simp only [toList, List.length_cons, Fin.zero_eta]
|
||||
|
|
@ -64,13 +64,13 @@ lemma toList_tail : {l : List 𝓕} → (a : CreateAnnihilateSect f l) → toLis
|
|||
| i :: l, a => by
|
||||
simp [toList]
|
||||
|
||||
lemma toList_cons {i : 𝓕} (a : CreateAnnihilateSect f (i :: l)) :
|
||||
lemma toList_cons {i : 𝓕} (a : CreateAnnihilateSect f (i :: φs)) :
|
||||
(toList a) = ⟨i, a.head⟩ :: toList a.tail := by
|
||||
rfl
|
||||
|
||||
lemma toList_get (a : CreateAnnihilateSect f l) :
|
||||
(toList a).get = (fun i => ⟨l.get i, a i⟩) ∘ Fin.cast (by simp) := by
|
||||
induction l with
|
||||
lemma toList_get (a : CreateAnnihilateSect f φs) :
|
||||
(toList a).get = (fun i => ⟨φs.get i, a i⟩) ∘ Fin.cast (by simp) := by
|
||||
induction φs with
|
||||
| nil =>
|
||||
funext i
|
||||
exact Fin.elim0 i
|
||||
|
|
@ -89,8 +89,8 @@ lemma toList_get (a : CreateAnnihilateSect f l) :
|
|||
@[simp]
|
||||
lemma toList_grade :
|
||||
FieldStatistic.ofList (fun i => q i.fst) a.toList = fermionic ↔
|
||||
FieldStatistic.ofList q l = fermionic := by
|
||||
induction l with
|
||||
FieldStatistic.ofList q φs = fermionic := by
|
||||
induction φs with
|
||||
| nil =>
|
||||
simp [toList]
|
||||
| cons i r ih =>
|
||||
|
|
|
|||
|
|
@ -20,57 +20,57 @@ variable {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Pro
|
|||
/-- Gives a factor of `-1` when inserting `a` into a list `List I` in the ordered position
|
||||
for each fermion-fermion cross. -/
|
||||
def koszulSignInsert {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop)
|
||||
[DecidableRel le] (a : 𝓕) : List 𝓕 → ℂ
|
||||
[DecidableRel le] (φ : 𝓕) : List 𝓕 → ℂ
|
||||
| [] => 1
|
||||
| b :: l => if le a b then koszulSignInsert q le a l else
|
||||
if q a = fermionic ∧ q b = fermionic then - koszulSignInsert q le a l else
|
||||
koszulSignInsert q le a l
|
||||
| φ' :: φs => if le φ φ' then koszulSignInsert q le φ φs else
|
||||
if q φ = fermionic ∧ q φ' = fermionic then - koszulSignInsert q le φ φs else
|
||||
koszulSignInsert q le φ φs
|
||||
|
||||
/-- When inserting a boson the `koszulSignInsert` is always `1`. -/
|
||||
lemma koszulSignInsert_boson (q : 𝓕 → FieldStatistic) (le : 𝓕 → 𝓕 → Prop) [DecidableRel le]
|
||||
(a : 𝓕) (ha : q a = bosonic) : (φs : List 𝓕) → koszulSignInsert q le a φs = 1
|
||||
(φ : 𝓕) (ha : q φ = bosonic) : (φs : List 𝓕) → koszulSignInsert q le φ φs = 1
|
||||
| [] => by
|
||||
simp [koszulSignInsert]
|
||||
| b :: l => by
|
||||
| φ' :: φs => by
|
||||
simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
|
||||
rw [koszulSignInsert_boson q le a ha l, ha]
|
||||
rw [koszulSignInsert_boson q le φ ha φs, ha]
|
||||
simp only [reduceCtorEq, false_and, ↓reduceIte, ite_self]
|
||||
|
||||
@[simp]
|
||||
lemma koszulSignInsert_mul_self (a : 𝓕) :
|
||||
(φs : List 𝓕) → koszulSignInsert q le a φs * koszulSignInsert q le a φs = 1
|
||||
lemma koszulSignInsert_mul_self (φ : 𝓕) :
|
||||
(φs : List 𝓕) → koszulSignInsert q le φ φs * koszulSignInsert q le φ φs = 1
|
||||
| [] => by
|
||||
simp [koszulSignInsert]
|
||||
| b :: l => by
|
||||
| φ' :: φs => by
|
||||
simp only [koszulSignInsert, Fin.isValue, mul_ite, ite_mul, neg_mul, mul_neg]
|
||||
by_cases hr : le a b
|
||||
by_cases hr : le φ φ'
|
||||
· simp only [hr, ↓reduceIte]
|
||||
rw [koszulSignInsert_mul_self]
|
||||
· simp only [hr, ↓reduceIte]
|
||||
by_cases hq : q a = fermionic ∧ q b = fermionic
|
||||
by_cases hq : q φ = fermionic ∧ q φ' = fermionic
|
||||
· simp only [hq, and_self, ↓reduceIte, neg_neg]
|
||||
rw [koszulSignInsert_mul_self]
|
||||
· simp only [hq, ↓reduceIte]
|
||||
rw [koszulSignInsert_mul_self]
|
||||
|
||||
lemma koszulSignInsert_le_forall (a : 𝓕) (l : List 𝓕) (hi : ∀ b, le a b) :
|
||||
koszulSignInsert q le a l = 1 := by
|
||||
induction l with
|
||||
lemma koszulSignInsert_le_forall (φ : 𝓕) (φs : List 𝓕) (hi : ∀ φ', le φ φ') :
|
||||
koszulSignInsert q le φ φs = 1 := by
|
||||
induction φs with
|
||||
| nil => rfl
|
||||
| cons j l ih =>
|
||||
| cons φ' φs ih =>
|
||||
simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
|
||||
rw [ih]
|
||||
simp only [Fin.isValue, ite_eq_left_iff, ite_eq_right_iff, and_imp]
|
||||
intro h
|
||||
exact False.elim (h (hi j))
|
||||
exact False.elim (h (hi φ'))
|
||||
|
||||
lemma koszulSignInsert_ge_forall_append (φs : List 𝓕) (j i : 𝓕) (hi : ∀ j, le j i) :
|
||||
koszulSignInsert q le j φs = koszulSignInsert q le j (φs ++ [i]) := by
|
||||
lemma koszulSignInsert_ge_forall_append (φs : List 𝓕) (φ' φ : 𝓕) (hi : ∀ φ'', le φ'' φ) :
|
||||
koszulSignInsert q le φ' φs = koszulSignInsert q le φ' (φs ++ [φ]) := by
|
||||
induction φs with
|
||||
| nil => simp [koszulSignInsert, hi]
|
||||
| cons b l ih =>
|
||||
| cons φ'' φs ih =>
|
||||
simp only [koszulSignInsert, Fin.isValue, List.append_eq]
|
||||
by_cases hr : le j b
|
||||
by_cases hr : le φ' φ''
|
||||
· rw [if_pos hr, if_pos hr, ih]
|
||||
· rw [if_neg hr, if_neg hr, ih]
|
||||
|
||||
|
|
@ -136,20 +136,20 @@ lemma koszulSignInsert_eq_grade (φ : 𝓕) (φs : List 𝓕) :
|
|||
simpa [ofList] using ih
|
||||
simpa using hr1
|
||||
|
||||
lemma koszulSignInsert_eq_perm (φs φs' : List 𝓕) (a : 𝓕) (h : φs.Perm φs') :
|
||||
koszulSignInsert q le a φs = koszulSignInsert q le a φs' := by
|
||||
lemma koszulSignInsert_eq_perm (φs φs' : List 𝓕) (φ : 𝓕) (h : φs.Perm φs') :
|
||||
koszulSignInsert q le φ φs = koszulSignInsert q le φ φs' := by
|
||||
rw [koszulSignInsert_eq_grade, koszulSignInsert_eq_grade]
|
||||
congr 1
|
||||
simp only [Fin.isValue, decide_not, eq_iff_iff, and_congr_right_iff]
|
||||
intro h'
|
||||
have hg : ofList q (List.filter (fun i => !decide (le a i)) φs) =
|
||||
ofList q (List.filter (fun i => !decide (le a i)) φs') := by
|
||||
have hg : ofList q (List.filter (fun i => !decide (le φ i)) φs) =
|
||||
ofList q (List.filter (fun i => !decide (le φ i)) φs') := by
|
||||
apply ofList_perm
|
||||
exact List.Perm.filter (fun i => !decide (le a i)) h
|
||||
exact List.Perm.filter (fun i => !decide (le φ i)) h
|
||||
rw [hg]
|
||||
|
||||
lemma koszulSignInsert_eq_sort (φs : List 𝓕) (a : 𝓕) :
|
||||
koszulSignInsert q le a φs = koszulSignInsert q le a (List.insertionSort le φs) := by
|
||||
lemma koszulSignInsert_eq_sort (φs : List 𝓕) (φ : 𝓕) :
|
||||
koszulSignInsert q le φ φs = koszulSignInsert q le φ (List.insertionSort le φs) := by
|
||||
apply koszulSignInsert_eq_perm
|
||||
exact List.Perm.symm (List.perm_insertionSort le φs)
|
||||
|
||||
|
|
|
|||
|
|
@ -33,13 +33,13 @@ lemma static_wick_nil {A : Type} [Semiring A] [Algebra ℂ A]
|
|||
simp [ofListLift_empty]
|
||||
|
||||
lemma static_wick_cons [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) × f i) le]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A] (r : List 𝓕) (a : 𝓕)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A] (φs : List 𝓕) (φ : 𝓕)
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F]
|
||||
(S : Contractions.Splitting f le)
|
||||
(ih : F (ofListLift f r 1) =
|
||||
∑ c : Contractions r, c.toCenterTerm f q le F S * F (koszulOrder (fun i => q i.fst) le
|
||||
(ih : F (ofListLift f φs 1) =
|
||||
∑ c : Contractions φs, c.toCenterTerm f q le F S * F (koszulOrder (fun i => q i.fst) le
|
||||
(ofListLift f c.normalize 1))) :
|
||||
F (ofListLift f (a :: r) 1) = ∑ c : Contractions (a :: r),
|
||||
F (ofListLift f (φ :: φs) 1) = ∑ c : Contractions (φ :: φs),
|
||||
c.toCenterTerm f q le F S *
|
||||
F (koszulOrder (fun i => q i.fst) le (ofListLift f c.normalize 1)) := by
|
||||
rw [ofListLift_cons_eq_ofListLift, map_mul, ih, Finset.mul_sum,
|
||||
|
|
@ -47,7 +47,7 @@ lemma static_wick_cons [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) ×
|
|||
erw [Finset.sum_sigma]
|
||||
congr
|
||||
funext c
|
||||
have hb := S.h𝓑 a
|
||||
have hb := S.h𝓑 φ
|
||||
rw [← mul_assoc]
|
||||
have hi := c.toCenterTerm_center f q le F S
|
||||
rw [Subalgebra.mem_center_iff] at hi
|
||||
|
|
@ -80,16 +80,16 @@ lemma static_wick_cons [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) ×
|
|||
funext n
|
||||
rw [← mul_assoc]
|
||||
rfl
|
||||
exact S.h𝓑p a
|
||||
exact S.h𝓑n a
|
||||
exact S.h𝓑p φ
|
||||
exact S.h𝓑n φ
|
||||
|
||||
theorem static_wick_theorem [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) × f i) le]
|
||||
{A : Type} [Semiring A] [Algebra ℂ A] (r : List 𝓕)
|
||||
{A : Type} [Semiring A] [Algebra ℂ A] (φs : List 𝓕)
|
||||
(F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le F]
|
||||
(S : Contractions.Splitting f le) :
|
||||
F (ofListLift f r 1) = ∑ c : Contractions r, c.toCenterTerm f q le F S *
|
||||
F (ofListLift f φs 1) = ∑ c : Contractions φs, c.toCenterTerm f q le F S *
|
||||
F (koszulOrder (fun i => q i.fst) le (ofListLift f c.normalize 1)) := by
|
||||
induction r with
|
||||
induction φs with
|
||||
| nil => exact static_wick_nil q le F S
|
||||
| cons a r ih => exact static_wick_cons q le r a F S ih
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue