refactor: style lint
This commit is contained in:
jstoobysmith
parent
7026d8ce66
commit
408a676bbd
10 changed files with 111 additions and 113 deletions
|
|
@ -485,7 +485,7 @@ lemma pauliMatrix_contr_down_3 :
|
|||
rw [contrBasisVectorMul_pos _]
|
||||
conv =>
|
||||
lhs; rhs; rhs; lhs;
|
||||
rw [contrBasisVectorMul_pos _]
|
||||
rw [contrBasisVectorMul_pos _]
|
||||
conv =>
|
||||
lhs
|
||||
simp only [_root_.zero_smul, one_smul, _root_.smul_zero, _root_.add_zero, _root_.zero_add]
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
|
|||
toFun f := ⟨⟨
|
||||
fun i =>
|
||||
if h : f.1 i.succ = 0 then i
|
||||
else Fin.pred (f.1 i.succ) h , by
|
||||
else Fin.pred (f.1 i.succ) h, by
|
||||
intro i
|
||||
by_cases h : f.1 i.succ = 0
|
||||
· simp [h]
|
||||
|
|
@ -33,7 +33,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
|
|||
simp only [f.2 i.succ, Fin.pred_succ, dite_eq_ite, ite_eq_right_iff]
|
||||
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
|
||||
⟨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 only [succ_eq_add_one, h0, ↓reduceDIte, Option.isSome_some, Option.get_some,
|
||||
|
|
@ -43,8 +43,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
|
|||
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
|
||||
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
|
||||
|
|
@ -59,7 +58,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
|
|||
by_cases hja : j = a
|
||||
· subst hja
|
||||
simp
|
||||
· rw [Function.update_apply ]
|
||||
· rw [Function.update_apply]
|
||||
rw [if_neg hja]
|
||||
simp only [Function.comp_apply, Fin.cons_succ]
|
||||
have hf2 := f.2.2 hs
|
||||
|
|
@ -145,12 +144,12 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
|
|||
· rename_i h
|
||||
exact False.elim (Fin.succ_ne_zero (f i) h)
|
||||
· rfl
|
||||
· simp only [Nat.succ_eq_add_one, Option.mem_def,
|
||||
· 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 only [Fin.cons_zero, Fin.pred_succ, exists_prop]
|
||||
have hx : ¬ (f0.get hs).succ = 0 := (Fin.succ_ne_zero (f0.get hs))
|
||||
have hx : ¬ (f0.get hs).succ = 0 := (Fin.succ_ne_zero (f0.get hs))
|
||||
simp only [hx, not_false_eq_true, true_and]
|
||||
refine Iff.intro (fun hi => ?_) (fun hi => ?_)
|
||||
· rw [← hi]
|
||||
|
|
@ -166,7 +165,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
|
|||
subst hs
|
||||
exact ne_of_beq_false rfl
|
||||
|
||||
lemma involutionCons_ext {n : ℕ} {f1 f2 : (f : {f : Fin n → Fin n // Function.Involutive f}) ×
|
||||
lemma involutionCons_ext {n : ℕ} {f1 f2 : (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)}}
|
||||
(h1 : f1.1 = f2.1) (h2 : f1.2 = Equiv.subtypeEquivRight (by rw [h1]; simp) f2.2) : f1 = f2 := by
|
||||
cases f1
|
||||
|
|
@ -181,10 +180,9 @@ lemma involutionCons_ext {n : ℕ} {f1 f2 : (f : {f : Fin n → Fin n // Functi
|
|||
simp_all only
|
||||
rfl
|
||||
|
||||
|
||||
def involutionAddEquiv {n : ℕ} (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)} ≃
|
||||
Option (Fin (Finset.univ.filter fun i => f.1 i = i).card) := by
|
||||
Option (Fin (Finset.univ.filter fun i => f.1 i = i).card) := by
|
||||
let e1 : {i : Option (Fin n) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)}
|
||||
≃ Option {i : Fin n // f.1 i = i} :=
|
||||
{ toFun := fun i => match i with
|
||||
|
|
@ -208,14 +206,13 @@ def involutionAddEquiv {n : ℕ} (f : {f : Fin n → Fin n // Function.Involutiv
|
|||
funext i
|
||||
simp [s]
|
||||
let e2 : {i // i ∈ s} ≃ Fin (Finset.card s) := by
|
||||
refine (Finset.orderIsoOfFin _ ?_).symm.toEquiv
|
||||
simp [s]
|
||||
refine (Finset.orderIsoOfFin _ ?_).symm.toEquiv
|
||||
simp [s]
|
||||
refine e1.trans (Equiv.optionCongr (e2'.trans (e2)))
|
||||
|
||||
|
||||
lemma involutionAddEquiv_none_image_zero {n : ℕ} :
|
||||
{f : {f : Fin n.succ → Fin n.succ // Function.Involutive f}}
|
||||
→ involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none
|
||||
→ involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none
|
||||
→ f.1 ⟨0, Nat.zero_lt_succ n⟩ = ⟨0, Nat.zero_lt_succ n⟩ := by
|
||||
intro f h
|
||||
simp only [Nat.succ_eq_add_one, involutionCons, Equiv.coe_fn_mk, involutionAddEquiv,
|
||||
|
|
@ -235,28 +232,29 @@ lemma involutionAddEquiv_none_image_zero {n : ℕ} :
|
|||
next h_2 => simp_all only [Subtype.mk.injEq, reduceCtorEq]
|
||||
|
||||
lemma involutionAddEquiv_cast {n : ℕ} {f1 f2 : {f : Fin n → Fin n // Function.Involutive f}}
|
||||
(hf : f1 = f2):
|
||||
involutionAddEquiv f1 = (Equiv.subtypeEquivRight (by rw [hf]; simp)).trans
|
||||
((involutionAddEquiv f2).trans (Equiv.optionCongr (finCongr (by rw [hf])))):= by
|
||||
(hf : f1 = f2) :
|
||||
involutionAddEquiv f1 = (Equiv.subtypeEquivRight (by rw [hf]; simp)).trans
|
||||
((involutionAddEquiv f2).trans (Equiv.optionCongr (finCongr (by rw [hf])))) := by
|
||||
subst hf
|
||||
simp only [finCongr_refl, Equiv.optionCongr_refl, Equiv.trans_refl]
|
||||
rfl
|
||||
|
||||
|
||||
lemma involutionAddEquiv_cast' {m : ℕ} {f1 f2 : {f : Fin m → Fin m // Function.Involutive f}}
|
||||
{N : ℕ} (hf : f1 = f2) (n : Option (Fin N)) (hn1 : N = (Finset.filter (fun i => f1.1 i = i) Finset.univ).card)
|
||||
(hn2 : N = (Finset.filter (fun i => f2.1 i = i) Finset.univ).card):
|
||||
HEq ((involutionAddEquiv f1).symm (Option.map (finCongr hn1) n)) ((involutionAddEquiv f2).symm (Option.map (finCongr hn2) n)) := by
|
||||
{N : ℕ} (hf : f1 = f2) (n : Option (Fin N))
|
||||
(hn1 : N = (Finset.filter (fun i => f1.1 i = i) Finset.univ).card)
|
||||
(hn2 : N = (Finset.filter (fun i => f2.1 i = i) Finset.univ).card) :
|
||||
HEq ((involutionAddEquiv f1).symm (Option.map (finCongr hn1) n))
|
||||
((involutionAddEquiv f2).symm (Option.map (finCongr hn2) n)) := by
|
||||
subst hf
|
||||
rfl
|
||||
|
||||
lemma involutionAddEquiv_none_succ {n : ℕ}
|
||||
{f : {f : Fin n.succ → Fin n.succ // Function.Involutive f}}
|
||||
(h : involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none)
|
||||
(x : Fin n) : f.1 x.succ = x.succ ↔ (involutionCons n f).1.1 x = x := by
|
||||
(h : involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none)
|
||||
(x : Fin n) : f.1 x.succ = x.succ ↔ (involutionCons n f).1.1 x = x := by
|
||||
simp only [succ_eq_add_one, involutionCons, Fin.cons_update, Equiv.coe_fn_mk, dite_eq_left_iff]
|
||||
have hn' := involutionAddEquiv_none_image_zero h
|
||||
have hx : ¬ f.1 x.succ = ⟨0, Nat.zero_lt_succ n⟩:= by
|
||||
have hx : ¬ f.1 x.succ = ⟨0, Nat.zero_lt_succ n⟩:= by
|
||||
rw [← hn']
|
||||
exact fun hn => Fin.succ_ne_zero x (Function.Involutive.injective f.2 hn)
|
||||
apply Iff.intro
|
||||
|
|
@ -286,7 +284,7 @@ lemma involutionAddEquiv_isSome_image_zero {n : ℕ} :
|
|||
def involutionNoFixedEquivSum {n : ℕ} :
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
|
||||
∧ ∀ i, f i ≠ i} ≃ Σ (k : Fin (2 * n + 1)),
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
|
||||
∧ (∀ i, f i ≠ i) ∧ f 0 = k.succ} where
|
||||
toFun f := ⟨(f.1 0).pred (f.2.2 0), ⟨f.1, f.2.1, by simpa using f.2.2⟩⟩
|
||||
invFun f := ⟨f.2.1, ⟨f.2.2.1, f.2.2.2.1⟩⟩
|
||||
|
|
@ -310,7 +308,7 @@ The main aim of thes equivalences is to define `involutionNoFixedZeroEquivProd`.
|
|||
|
||||
def involutionNoFixedZeroSetEquivEquiv {n : ℕ}
|
||||
(k : Fin (2 * n + 1)) (e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f
|
||||
∧ (∀ i, f i ≠ i) ∧ f 0 = k.succ} ≃
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive (e.symm ∘ f ∘ e) ∧
|
||||
(∀ i, (e.symm ∘ f ∘ e) i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} where
|
||||
|
|
@ -332,11 +330,12 @@ def involutionNoFixedZeroSetEquivEquiv {n : ℕ}
|
|||
ext i
|
||||
simp
|
||||
|
||||
def involutionNoFixedZeroSetEquivSetEquiv {n : ℕ} (k : Fin (2 * n + 1)) (e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
|
||||
def involutionNoFixedZeroSetEquivSetEquiv {n : ℕ} (k : Fin (2 * n + 1))
|
||||
(e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive (e.symm ∘ f ∘ e) ∧
|
||||
(∀ i, (e.symm ∘ f ∘ e) i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} ≃
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} := by
|
||||
(∀ i, f i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} := by
|
||||
refine Equiv.subtypeEquivRight ?_
|
||||
intro f
|
||||
have h1 : Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive f := by
|
||||
|
|
@ -360,12 +359,12 @@ def involutionNoFixedZeroSetEquivSetEquiv {n : ℕ} (k : Fin (2 * n + 1)) (e : F
|
|||
nth_rewrite 2 [← hn] at hi
|
||||
simp at hi
|
||||
|
||||
|
||||
def involutionNoFixedZeroSetEquivEquiv' {n : ℕ} (k : Fin (2 * n + 1)) (e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
|
||||
def involutionNoFixedZeroSetEquivEquiv' {n : ℕ} (k : Fin (2 * n + 1))
|
||||
(e : Fin (2 * n.succ) ≃ Fin (2 * n.succ)) :
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ}
|
||||
(∀ i, f i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ}
|
||||
≃ {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i) ∧ f (e 0) = e k.succ} := by
|
||||
(∀ i, f i ≠ i) ∧ f (e 0) = e k.succ} := by
|
||||
refine Equiv.subtypeEquivRight ?_
|
||||
simp only [succ_eq_add_one, ne_eq, Function.comp_apply, and_congr_right_iff]
|
||||
intro f hi h1
|
||||
|
|
@ -373,13 +372,13 @@ def involutionNoFixedZeroSetEquivEquiv' {n : ℕ} (k : Fin (2 * n + 1)) (e : Fin
|
|||
|
||||
def involutionNoFixedZeroSetEquivSetOne {n : ℕ} (k : Fin (2 * n + 1)) :
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i) ∧ f 0 = k.succ}
|
||||
(∀ i, f i ≠ i) ∧ f 0 = k.succ}
|
||||
≃ {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i) ∧ f 0 = 1} := by
|
||||
(∀ i, f i ≠ i) ∧ f 0 = 1} := by
|
||||
refine Equiv.trans (involutionNoFixedZeroSetEquivEquiv k (Equiv.swap k.succ 1)) ?_
|
||||
refine Equiv.trans (involutionNoFixedZeroSetEquivSetEquiv k (Equiv.swap k.succ 1)) ?_
|
||||
refine Equiv.trans (involutionNoFixedZeroSetEquivEquiv' k (Equiv.swap k.succ 1)) ?_
|
||||
refine Equiv.subtypeEquivRight ?_
|
||||
refine Equiv.subtypeEquivRight ?_
|
||||
simp only [succ_eq_add_one, ne_eq, Equiv.swap_apply_left, and_congr_right_iff]
|
||||
intro f hi h1
|
||||
rw [Equiv.swap_apply_of_ne_of_ne]
|
||||
|
|
@ -387,10 +386,9 @@ def involutionNoFixedZeroSetEquivSetOne {n : ℕ} (k : Fin (2 * n + 1)) :
|
|||
· exact Fin.zero_ne_one
|
||||
|
||||
def involutionNoFixedSetOne {n : ℕ} :
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i) ∧ f 0 = 1} ≃
|
||||
{f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i)} where
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i) ∧ f 0 = 1} ≃ {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i)} where
|
||||
toFun f := by
|
||||
have hf1 : f.1 1 = 0 := by
|
||||
have hf := f.2.2.2
|
||||
|
|
@ -444,7 +442,7 @@ def involutionNoFixedSetOne {n : ℕ} :
|
|||
rename_i x r
|
||||
simp_all only [succ_eq_add_one, Fin.ext_iff, Fin.val_succ, add_left_inj]
|
||||
have hfn {a b : ℕ} {ha : a < 2 * n} {hb : b < 2 * n}
|
||||
(hab : ↑(f.1 ⟨a, ha⟩) = b): ↑(f.1 ⟨b, hb⟩) = a := by
|
||||
(hab : ↑(f.1 ⟨a, ha⟩) = b) : ↑(f.1 ⟨b, hb⟩) = a := by
|
||||
have ht : f.1 ⟨a, ha⟩ = ⟨b, hb⟩ := by
|
||||
simp [hab, Fin.ext_iff]
|
||||
rw [← ht, f.2.1]
|
||||
|
|
@ -504,7 +502,7 @@ def involutionNoFixedSetOne {n : ℕ} :
|
|||
simp only [Fin.coe_pred]
|
||||
split
|
||||
· rename_i h
|
||||
simp [Fin.ext_iff] at h
|
||||
simp [Fin.ext_iff] at h
|
||||
· rename_i h
|
||||
simp [Fin.ext_iff] at h
|
||||
· rename_i h
|
||||
|
|
@ -513,22 +511,23 @@ def involutionNoFixedSetOne {n : ℕ} :
|
|||
apply congrArg
|
||||
simp_all [Fin.ext_iff]
|
||||
|
||||
|
||||
def involutionNoFixedZeroSetEquiv {n : ℕ} (k : Fin (2 * n + 1)) :
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧
|
||||
(∀ i, f i ≠ i) ∧ f 0 = k.succ}
|
||||
(∀ i, f i ≠ i) ∧ f 0 = k.succ}
|
||||
≃ {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
|
||||
refine Equiv.trans (involutionNoFixedZeroSetEquivSetOne k) involutionNoFixedSetOne
|
||||
|
||||
def involutionNoFixedEquivSumSame {n : ℕ} :
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
|
||||
≃ Σ (_ : Fin (2 * n + 1)), {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
|
||||
≃ Σ (_ : Fin (2 * n + 1)),
|
||||
{f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
|
||||
refine Equiv.trans involutionNoFixedEquivSum ?_
|
||||
refine Equiv.sigmaCongrRight involutionNoFixedZeroSetEquiv
|
||||
|
||||
def involutionNoFixedZeroEquivProd {n : ℕ} :
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
|
||||
≃ Fin (2 * n + 1) × {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
|
||||
≃ Fin (2 * n + 1) ×
|
||||
{f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
|
||||
refine Equiv.trans involutionNoFixedEquivSumSame ?_
|
||||
exact Equiv.sigmaEquivProd (Fin (2 * n + 1))
|
||||
{ f // Function.Involutive f ∧ ∀ (i : Fin (2 * n)), f i ≠ i}
|
||||
|
|
@ -539,27 +538,24 @@ def involutionNoFixedZeroEquivProd {n : ℕ} :
|
|||
|
||||
-/
|
||||
|
||||
|
||||
instance {n : ℕ} : Fintype { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } := by
|
||||
haveI : DecidablePred fun x => Function.Involutive x := by
|
||||
intro f
|
||||
apply Fintype.decidableForallFintype (α := Fin n)
|
||||
haveI : DecidablePred fun x => Function.Involutive x ∧ ∀ (i : Fin n), x i ≠ i := by
|
||||
intro x
|
||||
apply instDecidableAnd
|
||||
instance {n : ℕ} : Fintype { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } := by
|
||||
haveI : DecidablePred fun x => Function.Involutive x :=
|
||||
fun f => Fintype.decidableForallFintype (α := Fin n)
|
||||
haveI : DecidablePred fun x => Function.Involutive x ∧ ∀ (i : Fin n), x i ≠ i :=
|
||||
fun x => instDecidableAnd
|
||||
apply Subtype.fintype
|
||||
|
||||
lemma involutionNoFixed_card_succ {n : ℕ} :
|
||||
Fintype.card {f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
|
||||
= (2 * n + 1) * Fintype.card {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
|
||||
rw [Fintype.card_congr (involutionNoFixedZeroEquivProd)]
|
||||
rw [Fintype.card_prod ]
|
||||
Fintype.card
|
||||
{f : Fin (2 * n.succ) → Fin (2 * n.succ) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
|
||||
= (2 * n + 1) *
|
||||
Fintype.card {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} := by
|
||||
rw [Fintype.card_congr (involutionNoFixedZeroEquivProd), Fintype.card_prod]
|
||||
congr
|
||||
exact Fintype.card_fin (2 * n + 1)
|
||||
|
||||
|
||||
lemma involutionNoFixed_card_mul_two : (n : ℕ) →
|
||||
Fintype.card {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
|
||||
Fintype.card {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)}
|
||||
= (2 * n - 1)‼
|
||||
| 0 => rfl
|
||||
| Nat.succ n => by
|
||||
|
|
@ -568,7 +564,7 @@ lemma involutionNoFixed_card_mul_two : (n : ℕ) →
|
|||
exact Eq.symm (Nat.doubleFactorial_add_one (Nat.mul 2 n))
|
||||
|
||||
lemma involutionNoFixed_card_even : (n : ℕ) → (he : Even n) →
|
||||
Fintype.card {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} = (n - 1)‼ := by
|
||||
Fintype.card {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} = (n - 1)‼ := by
|
||||
intro n he
|
||||
obtain ⟨r, hr⟩ := he
|
||||
have hr' : n = 2 * r := by omega
|
||||
|
|
|
|||
|
|
@ -662,7 +662,6 @@ def optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I :=
|
|||
| none => l
|
||||
| some i => List.eraseIdx l i
|
||||
|
||||
|
||||
lemma eraseIdx_length {I : Type} (l : List I) (i : Fin l.length) :
|
||||
(List.eraseIdx l i).length + 1 = l.length := by
|
||||
simp only [List.length_eraseIdx, Fin.is_lt, ↓reduceIte]
|
||||
|
|
@ -744,7 +743,7 @@ lemma optionEraseZ_some_length {I : Type} (l : List I) (a : I) (i : (Fin l.lengt
|
|||
lemma optionEraseZ_ext {I : Type} {l l' : List I} {a a' : I} {i : Option (Fin l.length)}
|
||||
{i' : Option (Fin l'.length)} (hl : l = l') (ha : a = a')
|
||||
(hi : Option.map (Fin.cast (by rw [hl])) i = i') :
|
||||
optionEraseZ l a i = optionEraseZ l' a' i' := by
|
||||
optionEraseZ l a i = optionEraseZ l' a' i' := by
|
||||
subst hl
|
||||
subst ha
|
||||
cases hi
|
||||
|
|
|
|||
|
|
@ -33,12 +33,12 @@ namespace Contractions
|
|||
|
||||
variable {l : List 𝓕} (c : Contractions l)
|
||||
|
||||
def auxCongr : {φs: List 𝓕} → {φsᵤₙ φsᵤₙ' : List 𝓕} → (h : φsᵤₙ = φsᵤₙ') →
|
||||
def auxCongr : {φs: List 𝓕} → {φsᵤₙ φsᵤₙ' : List 𝓕} → (h : φsᵤₙ = φsᵤₙ') →
|
||||
ContractionsAux φs φsᵤₙ ≃ ContractionsAux φs φsᵤₙ'
|
||||
| _, _, _, Eq.refl _ => Equiv.refl _
|
||||
|
||||
lemma auxCongr_ext {φs: List 𝓕} {c c2 : Contractions φs} (h : c.1 = c2.1)
|
||||
(hx : c.2 = auxCongr h.symm c2.2) : c = c2 := by
|
||||
(hx : c.2 = auxCongr h.symm c2.2) : c = c2 := by
|
||||
cases c
|
||||
cases c2
|
||||
simp only at h
|
||||
|
|
@ -50,7 +50,7 @@ lemma auxCongr_ext {φs: List 𝓕} {c c2 : Contractions φs} (h : c.1 = c2.1)
|
|||
/-- The list of uncontracted fields. -/
|
||||
def uncontracted : List 𝓕 := c.1
|
||||
|
||||
lemma uncontracted_length_even_iff : {l : List 𝓕} → (c : Contractions l) →
|
||||
lemma uncontracted_length_even_iff : {l : List 𝓕} → (c : Contractions l) →
|
||||
Even l.length ↔ Even c.uncontracted.length
|
||||
| [], ⟨[], ContractionsAux.nil⟩ => by
|
||||
simp [uncontracted]
|
||||
|
|
@ -76,7 +76,8 @@ lemma contractions_nil (a : Contractions ([] : List 𝓕)) : a = ⟨[], Contract
|
|||
cases c
|
||||
rfl
|
||||
|
||||
def embedUncontracted {l : List 𝓕} (c : Contractions l) : Fin c.uncontracted.length → Fin l.length :=
|
||||
def embedUncontracted {l : List 𝓕} (c : Contractions l) :
|
||||
Fin c.uncontracted.length → Fin l.length :=
|
||||
match l, c with
|
||||
| [], ⟨[], ContractionsAux.nil⟩ => Fin.elim0
|
||||
| φ :: φs, ⟨_, .cons (φsᵤₙ := aux) none c⟩ =>
|
||||
|
|
@ -93,7 +94,7 @@ def embedUncontracted {l : List 𝓕} (c : Contractions l) : Fin c.uncontracted.
|
|||
exact Fin.elim0 n
|
||||
omega
|
||||
|
||||
lemma embedUncontracted_injective {l : List 𝓕} (c : Contractions l) :
|
||||
lemma embedUncontracted_injective {l : List 𝓕} (c : Contractions l) :
|
||||
Function.Injective c.embedUncontracted := by
|
||||
match l, c with
|
||||
| [], ⟨[], ContractionsAux.nil⟩ =>
|
||||
|
|
@ -108,12 +109,12 @@ lemma embedUncontracted_injective {l : List 𝓕} (c : Contractions l) :
|
|||
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 only [List.length_cons, 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
|
||||
| φ :: φs, ⟨_, .cons (φsᵤₙ := aux) (some i) c⟩ =>
|
||||
dsimp only [List.length_cons, 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. -/
|
||||
|
|
@ -161,7 +162,7 @@ def consEquiv {φ : 𝓕} {φs : List 𝓕} :
|
|||
lemma consEquiv_ext {φs : List 𝓕} {c1 c2 : Contractions φs}
|
||||
{n1 : Option (Fin c1.uncontracted.length)} {n2 : Option (Fin c2.uncontracted.length)}
|
||||
(hc : c1 = c2) (hn : Option.map (finCongr (by rw [hc])) n1 = n2) :
|
||||
(⟨c1, n1⟩ : (c : Contractions φs) × Option (Fin c.uncontracted.length)) = ⟨c2, n2⟩ := by
|
||||
(⟨c1, n1⟩ : (c : Contractions φs) × Option (Fin c.uncontracted.length)) = ⟨c2, n2⟩ := by
|
||||
subst hc
|
||||
subst hn
|
||||
simp
|
||||
|
|
|
|||
|
|
@ -17,13 +17,13 @@ open HepLean.Fin
|
|||
open Nat
|
||||
|
||||
/-- There are `(φs.length - 1)‼` full contractions of a list `φs` with an even number of fields. -/
|
||||
lemma card_of_full_contractions_even {φs : List 𝓕} (he : Even φs.length ) :
|
||||
lemma card_of_full_contractions_even {φs : List 𝓕} (he : Even φs.length) :
|
||||
Fintype.card {c : Contractions φs // IsFull c} = (φs.length - 1)‼ := by
|
||||
rw [Fintype.card_congr (isFullInvolutionEquiv (φs := φs))]
|
||||
exact involutionNoFixed_card_even φs.length he
|
||||
|
||||
/-- There are no full contractions of a list with an odd number of fields. -/
|
||||
lemma card_of_full_contractions_odd {φs : List 𝓕} (ho : Odd φs.length ) :
|
||||
lemma card_of_full_contractions_odd {φs : List 𝓕} (ho : Odd φs.length) :
|
||||
Fintype.card {c : Contractions φs // IsFull c} = 0 := by
|
||||
rw [Fintype.card_eq_zero_iff, isEmpty_subtype]
|
||||
intro c
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ variable {l : List 𝓕}
|
|||
|
||||
/-- Given an involution the uncontracted fields associated with it (corresponding
|
||||
to the fixed points of that involution). -/
|
||||
def uncontractedFromInvolution : {φs : List 𝓕} →
|
||||
def uncontractedFromInvolution : {φs : List 𝓕} →
|
||||
(f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) →
|
||||
{l : List 𝓕 // l.length = (Finset.univ.filter fun i => f.1 i = i).card}
|
||||
| [], _ => ⟨[], by simp⟩
|
||||
|
|
@ -46,7 +46,7 @@ def uncontractedFromInvolution : {φs : List 𝓕} →
|
|||
let luc := uncontractedFromInvolution (involutionCons φs.length f).fst
|
||||
let n' := involutionAddEquiv (involutionCons φs.length f).1 (involutionCons φs.length f).2
|
||||
let np : Option (Fin luc.1.length) := Option.map (finCongr luc.2.symm) n'
|
||||
if hn : n' = none then
|
||||
if hn : n' = none then
|
||||
have hn' := involutionAddEquiv_none_image_zero (n := φs.length) (f := f) hn
|
||||
⟨optionEraseZ luc φ none, by
|
||||
simp only [optionEraseZ, Nat.succ_eq_add_one, List.length_cons, Mathlib.Vector.length_val]
|
||||
|
|
@ -55,7 +55,7 @@ def uncontractedFromInvolution : {φs : List 𝓕} →
|
|||
rw [Fin.sum_univ_succ]
|
||||
conv_rhs => erw [if_pos hn']
|
||||
ring_nf
|
||||
simp only [Nat.succ_eq_add_one, Mathlib.Vector.length_val, Nat.cast_id,
|
||||
simp only [Nat.succ_eq_add_one, Mathlib.Vector.length_val, Nat.cast_id,
|
||||
add_right_inj]
|
||||
rw [Finset.card_filter]
|
||||
apply congrArg
|
||||
|
|
@ -72,17 +72,18 @@ def uncontractedFromInvolution : {φs : List 𝓕} →
|
|||
Option.isSome_none, Equiv.trans_apply, Equiv.coe_fn_mk, Equiv.optionCongr_apply,
|
||||
Equiv.coe_trans, RelIso.coe_fn_toEquiv, Option.map_eq_none', n'] at hn
|
||||
split at hn
|
||||
· simp_all only [reduceCtorEq, not_false_eq_true, Nat.succ_eq_add_one, Option.isSome_some, k']
|
||||
· simp_all only [reduceCtorEq, not_false_eq_true, Nat.succ_eq_add_one,
|
||||
Option.isSome_some, k']
|
||||
· simp_all only [not_true_eq_false]
|
||||
let k := k'.1.get hkIsSome
|
||||
rw [optionEraseZ_some_length]
|
||||
have hksucc : k.succ = f.1 ⟨0, Nat.zero_lt_succ φs.length⟩ := by
|
||||
simp [k, k', involutionCons]
|
||||
have hzero : ⟨0, Nat.zero_lt_succ φs.length⟩ = f.1 k.succ := by
|
||||
have hzero : ⟨0, Nat.zero_lt_succ φs.length⟩ = f.1 k.succ := by
|
||||
rw [hksucc, f.2]
|
||||
have hksuccNe : f.1 k.succ ≠ k.succ := by
|
||||
conv_rhs => rw [hksucc]
|
||||
exact fun hn => Fin.succ_ne_zero k (Function.Involutive.injective f.2 hn )
|
||||
exact fun hn => Fin.succ_ne_zero k (Function.Involutive.injective f.2 hn)
|
||||
have hluc : 1 ≤ luc.1.length := by
|
||||
simp only [Nat.succ_eq_add_one, Mathlib.Vector.length_val, Finset.one_le_card]
|
||||
use k
|
||||
|
|
@ -131,8 +132,8 @@ lemma uncontractedFromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
|
|||
(involutionAddEquiv (involutionCons φs.length f).1 (involutionCons φs.length f).2)) := by
|
||||
let luc := uncontractedFromInvolution (involutionCons φs.length f).fst
|
||||
let n' := involutionAddEquiv (involutionCons φs.length f).1 (involutionCons φs.length f).2
|
||||
change _ = optionEraseZ luc φ
|
||||
(Option.map (finCongr ((uncontractedFromInvolution (involutionCons φs.length f).fst).2.symm)) n')
|
||||
change _ = optionEraseZ luc φ (Option.map
|
||||
(finCongr ((uncontractedFromInvolution (involutionCons φs.length f).fst).2.symm)) n')
|
||||
dsimp only [List.length_cons, uncontractedFromInvolution, Nat.succ_eq_add_one, Fin.zero_eta]
|
||||
by_cases hn : n' = none
|
||||
· have hn' := hn
|
||||
|
|
@ -165,10 +166,10 @@ lemma uncontractedFromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
|
|||
simp_all only [Option.get_some]
|
||||
|
||||
/-- The `ContractionsAux` associated to an involution. -/
|
||||
def fromInvolutionAux : {l : List 𝓕} →
|
||||
def fromInvolutionAux : {l : List 𝓕} →
|
||||
(f : {f : Fin l.length → Fin l.length // Function.Involutive f}) →
|
||||
ContractionsAux l (uncontractedFromInvolution f)
|
||||
| [] => fun _ => ContractionsAux.nil
|
||||
| [] => fun _ => ContractionsAux.nil
|
||||
| _ :: φs => fun f =>
|
||||
let f' := involutionCons φs.length f
|
||||
let c' := fromInvolutionAux f'.1
|
||||
|
|
@ -177,8 +178,9 @@ def fromInvolutionAux : {l : List 𝓕} →
|
|||
auxCongr (uncontractedFromInvolution_cons f).symm (ContractionsAux.cons n' c')
|
||||
|
||||
/-- The contraction associated with an involution. -/
|
||||
def fromInvolution {φs : List 𝓕} (f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) :
|
||||
Contractions φs := ⟨uncontractedFromInvolution f, fromInvolutionAux f⟩
|
||||
def fromInvolution {φs : List 𝓕}
|
||||
(f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) : Contractions φs :=
|
||||
⟨uncontractedFromInvolution f, fromInvolutionAux f⟩
|
||||
|
||||
lemma fromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
|
||||
(f : {f : Fin (φ :: φs).length → Fin (φ :: φs).length // Function.Involutive f}) :
|
||||
|
|
@ -195,8 +197,8 @@ lemma fromInvolution_cons {φs : List 𝓕} {φ : 𝓕}
|
|||
rfl
|
||||
|
||||
lemma fromInvolution_of_involutionCons {φs : List 𝓕} {φ : 𝓕}
|
||||
(f : {f : Fin (φs ).length → Fin (φs).length // Function.Involutive f})
|
||||
(n : { i : Option (Fin φs.length) // ∀ (h : i.isSome = true), f.1 (i.get h) = i.get h }):
|
||||
(f : {f : Fin φs.length → Fin φs.length // Function.Involutive f})
|
||||
(n : { i : Option (Fin φs.length) // ∀ (h : i.isSome = true), f.1 (i.get h) = i.get h }) :
|
||||
fromInvolution (φs := φ :: φs) ((involutionCons φs.length).symm ⟨f, n⟩) =
|
||||
consEquiv.symm ⟨fromInvolution f, Option.map (finCongr ((uncontractedFromInvolution f).2.symm))
|
||||
(involutionAddEquiv f n)⟩ := by
|
||||
|
|
@ -212,7 +214,7 @@ lemma fromInvolution_of_involutionCons {φs : List 𝓕} {φ : 𝓕}
|
|||
-/
|
||||
|
||||
/-- The involution associated with a contraction. -/
|
||||
def toInvolution : {φs : List 𝓕} → (c : Contractions φs) →
|
||||
def toInvolution : {φs : List 𝓕} → (c : Contractions φs) →
|
||||
{f : {f : Fin φs.length → Fin φs.length // Function.Involutive f} //
|
||||
uncontractedFromInvolution f = c.1}
|
||||
| [], ⟨[], ContractionsAux.nil⟩ => ⟨⟨fun i => i, by
|
||||
|
|
@ -223,22 +225,23 @@ def toInvolution : {φs : List 𝓕} → (c : Contractions φs) →
|
|||
let n' : Option (Fin (uncontractedFromInvolution ⟨f', hf1⟩).1.length) :=
|
||||
Option.map (finCongr (by rw [hf2])) n
|
||||
let F := (involutionCons φs.length).symm ⟨⟨f', hf1⟩,
|
||||
(involutionAddEquiv ⟨f', hf1⟩).symm
|
||||
(Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2)) n')⟩
|
||||
(involutionAddEquiv ⟨f', hf1⟩).symm
|
||||
(Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2)) n')⟩
|
||||
refine ⟨F, ?_⟩
|
||||
have hF0 : ((involutionCons φs.length) F) = ⟨⟨f', hf1⟩,
|
||||
(involutionAddEquiv ⟨f', hf1⟩).symm
|
||||
(Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2)) n')⟩ := by
|
||||
(involutionAddEquiv ⟨f', hf1⟩).symm
|
||||
(Option.map (finCongr ((uncontractedFromInvolution ⟨f', hf1⟩).2)) n')⟩ := by
|
||||
simp [F]
|
||||
have hF1 : ((involutionCons φs.length) F).fst = ⟨f', hf1⟩ := by
|
||||
rw [hF0]
|
||||
have hF2L : ((uncontractedFromInvolution ⟨f', hf1⟩)).1.length =
|
||||
(Finset.filter (fun i => ((involutionCons φs.length) F).1.1 i = i) Finset.univ).card := by
|
||||
apply Eq.trans ((uncontractedFromInvolution ⟨f', hf1⟩)).2
|
||||
apply Eq.trans ((uncontractedFromInvolution ⟨f', hf1⟩)).2
|
||||
congr
|
||||
rw [hF1]
|
||||
have hF2 : ((involutionCons φs.length) F).snd = (involutionAddEquiv ((involutionCons φs.length) F).fst).symm
|
||||
(Option.map (finCongr hF2L) n') := by
|
||||
have hF2 : ((involutionCons φs.length) F).snd =
|
||||
(involutionAddEquiv ((involutionCons φs.length) F).fst).symm
|
||||
(Option.map (finCongr hF2L) n') := by
|
||||
rw [@Sigma.subtype_ext_iff] at hF0
|
||||
ext1
|
||||
rw [hF0.2]
|
||||
|
|
@ -314,8 +317,9 @@ lemma toInvolution_fromInvolution : {φs : List 𝓕} → (c : Contractions φs)
|
|||
simp only [Option.mem_def, Option.map_eq_some', Function.comp_apply, Fin.cast_trans,
|
||||
Fin.cast_eq_self, exists_eq_right]
|
||||
|
||||
lemma fromInvolution_toInvolution : {φs : List 𝓕} → (f : {f : Fin (φs ).length → Fin (φs).length // Function.Involutive f})
|
||||
→ toInvolution (fromInvolution f) = f
|
||||
lemma fromInvolution_toInvolution : {φs : List 𝓕} →
|
||||
(f : {f : Fin φs.length → Fin φs.length // Function.Involutive f}) →
|
||||
toInvolution (fromInvolution f) = f
|
||||
| [], _ => by
|
||||
ext x
|
||||
exact Fin.elim0 x
|
||||
|
|
@ -331,7 +335,7 @@ lemma fromInvolution_toInvolution : {φs : List 𝓕} → (f : {f : Fin (φs ).
|
|||
rw [Equiv.symm_apply_eq]
|
||||
conv_rhs =>
|
||||
lhs
|
||||
rw [involutionAddEquiv_cast hx]
|
||||
rw [involutionAddEquiv_cast hx]
|
||||
simp only [Nat.succ_eq_add_one, Equiv.trans_apply]
|
||||
rfl
|
||||
|
||||
|
|
@ -339,7 +343,7 @@ lemma fromInvolution_toInvolution : {φs : List 𝓕} → (f : {f : Fin (φs ).
|
|||
Note: This shows that the type of contractions only depends on the length of the list `φs`. -/
|
||||
def equivInvolutions {φs : List 𝓕} :
|
||||
Contractions φs ≃ {f : Fin φs.length → Fin φs.length // Function.Involutive f} where
|
||||
toFun := fun c => toInvolution c
|
||||
toFun := fun c => toInvolution c
|
||||
invFun := fromInvolution
|
||||
left_inv := toInvolution_fromInvolution
|
||||
right_inv := fromInvolution_toInvolution
|
||||
|
|
@ -355,7 +359,7 @@ lemma isFull_iff_uncontractedFromInvolution_empty {φs : List 𝓕} (c : Contrac
|
|||
erw [l.2]
|
||||
rfl
|
||||
|
||||
lemma isFull_iff_filter_card_involution_zero {φs : List 𝓕} (c : Contractions φs) :
|
||||
lemma isFull_iff_filter_card_involution_zero {φs : List 𝓕} (c : Contractions φs) :
|
||||
IsFull c ↔ (Finset.univ.filter fun i => (equivInvolutions c).1 i = i).card = 0 := by
|
||||
rw [isFull_iff_uncontractedFromInvolution_empty, List.ext_get_iff]
|
||||
simp
|
||||
|
|
@ -372,21 +376,18 @@ lemma isFull_iff_involution_no_fixed_points {φs : List 𝓕} (c : Contractions
|
|||
· intro i h
|
||||
exact fun a => i h
|
||||
|
||||
|
||||
/-- The equivalence between full contractions and fixed-point free involutions. -/
|
||||
def isFullInvolutionEquiv {φs : List 𝓕} : {c : Contractions φs // IsFull c} ≃
|
||||
{f : Fin φs.length → Fin φs.length // Function.Involutive f ∧ (∀ i, f i ≠ i)} where
|
||||
toFun c := ⟨equivInvolutions c.1, by
|
||||
apply And.intro (equivInvolutions c.1).2
|
||||
rw [← isFull_iff_involution_no_fixed_points]
|
||||
exact c.2
|
||||
⟩
|
||||
exact c.2⟩
|
||||
invFun f := ⟨equivInvolutions.symm ⟨f.1, f.2.1⟩, by
|
||||
rw [isFull_iff_involution_no_fixed_points]
|
||||
simpa using f.2.2⟩
|
||||
left_inv c := by simp
|
||||
right_inv f := by simp
|
||||
|
||||
|
||||
end Contractions
|
||||
end Wick
|
||||
|
|
|
|||
|
|
@ -26,7 +26,8 @@ namespace CreateAnnihilateSect
|
|||
|
||||
section basic_defs
|
||||
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {φs : List 𝓕} (a : CreateAnnihilateSect f φs)
|
||||
variable {𝓕 : Type} {f : 𝓕 → Type} [∀ i, Fintype (f i)] {φs : List 𝓕}
|
||||
(a : CreateAnnihilateSect f φs)
|
||||
|
||||
/-- The type `CreateAnnihilateSect f φs` is finite. -/
|
||||
instance fintype : Fintype (CreateAnnihilateSect f φs) := Pi.fintype
|
||||
|
|
|
|||
|
|
@ -84,7 +84,7 @@ def insertSign (n : ℕ) (φ : 𝓕) (φs : List 𝓕) : ℂ :=
|
|||
superCommuteCoef q [φ] (List.take n φs)
|
||||
|
||||
/-- If `φ` is bosonic, there is no sign associated with inserting it into a list of fields. -/
|
||||
lemma insertSign_bosonic (n : ℕ) (φ : 𝓕) (φs : List 𝓕) (hφ : q φ = bosonic) :
|
||||
lemma insertSign_bosonic (n : ℕ) (φ : 𝓕) (φs : List 𝓕) (hφ : q φ = bosonic) :
|
||||
insertSign q n φ φs = 1 := by
|
||||
simp only [insertSign, superCommuteCoef, ofList_singleton, hφ, reduceCtorEq, false_and,
|
||||
↓reduceIte]
|
||||
|
|
|
|||
|
|
@ -160,10 +160,10 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
|
|||
rw [← insertionSortEquiv_get]
|
||||
simp only [Function.comp_apply, Equiv.symm_apply_apply, List.get_eq_getElem, ni]
|
||||
simp_all only [List.length_cons, add_le_add_iff_right, List.getElem_insertIdx_self]
|
||||
have hc1 (hninro : ni.castSucc < nro) : ¬ le φ1 φ := by
|
||||
have hc1 (hninro : ni.castSucc < nro) : ¬ le φ1 φ := by
|
||||
rw [← hns]
|
||||
exact lt_orderedInsertPos_rel le φ1 rs ni hninro
|
||||
have hc2 (hninro : ¬ ni.castSucc < nro) : le φ1 φ := by
|
||||
have hc2 (hninro : ¬ ni.castSucc < nro) : le φ1 φ := by
|
||||
rw [← hns]
|
||||
refine gt_orderedInsertPos_rel le φ1 rs ?_ ni hninro
|
||||
exact List.sorted_insertionSort le (List.insertIdx n φ φs)
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ lemma static_wick_nil {A : Type} [Semiring A] [Algebra ℂ A]
|
|||
rw [← Contractions.nilEquiv.symm.sum_comp]
|
||||
simp only [Finset.univ_unique, PUnit.default_eq_unit, Contractions.nilEquiv, Equiv.coe_fn_symm_mk,
|
||||
Finset.sum_const, Finset.card_singleton, one_smul]
|
||||
dsimp [Contractions.uncontracted, Contractions.toCenterTerm]
|
||||
dsimp only [Contractions.toCenterTerm, Contractions.uncontracted]
|
||||
simp [ofListLift_empty]
|
||||
|
||||
lemma static_wick_cons [IsTrans ((i : 𝓕) × f i) le] [IsTotal ((i : 𝓕) × f i) le]
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue