Wick contractions

def WickContraction (n : ℕ) : Type

Given a natural number n, which will correspond to the number of fields needing contracting, a Wick contraction is a finite set of pairs of Fin n (numbers 0, ..., n-1), such that no element of Fin n occurs in more than one pair. The pairs are the positions of fields we 'contract' together.

Equations

• WickContraction n = { f : Finset (Finset (Fin n)) // (∀ a ∈ f, a.card = 2) ∧ ∀ a ∈ f, ∀ b ∈ f, a = b ∨ Disjoint a b }

instance WickContraction.instDecidableEq {n : ℕ} : DecidableEq (WickContraction n)

Wick contractions are decidable.

Equations

• WickContraction.instDecidableEq = Subtype.instDecidableEq

def WickContraction.empty {n : ℕ} : WickContraction n

The contraction consisting of no contracted pairs.

Equations

• WickContraction.empty = ⟨∅, ⋯⟩

theorem WickContraction.card_zero_iff_empty {n : ℕ} (c : WickContraction n) : (↑c).card = 0 ↔ c = empty

theorem WickContraction.exists_pair_of_not_eq_empty {n : ℕ} (c : WickContraction n) (h : c ≠ empty) : ∃ (i : Fin n) (j : Fin n), {i, j} ∈ ↑c

def WickContraction.congr {n m : ℕ} (h : n = m) : WickContraction n ≃ WickContraction m

The equivalence between WickContraction n and WickContraction m derived from a propositional equality of n and m.

Equations

• WickContraction.congr ⋯ = Equiv.refl (WickContraction x✝)

@[simp]

theorem WickContraction.congr_refl {n : ℕ} (c : WickContraction n) : (congr ⋯) c = c

@[simp]

theorem WickContraction.card_congr {n m : ℕ} (h : n = m) (c : WickContraction n) : (↑((congr h) c)).card = (↑c).card

theorem WickContraction.congr_contractions {n m : ℕ} (h : n = m) (c : WickContraction n) : ↑((congr h) c) = Finset.map (Finset.mapEmbedding (finCongr h).toEmbedding).toEmbedding ↑c

@[simp]

theorem WickContraction.congr_trans {n m o : ℕ} (h1 : n = m) (h2 : m = o) : (congr h1).trans (congr h2) = congr ⋯

@[simp]

theorem WickContraction.congr_trans_apply {n m o : ℕ} (h1 : n = m) (h2 : m = o) (c : WickContraction n) : (congr h2) ((congr h1) c) = (congr ⋯) c

theorem WickContraction.mem_congr_iff {n m : ℕ} (h : n = m) {c : WickContraction n} {a : Finset (Fin m)} : a ∈ ↑((congr h) c) ↔ Finset.map (finCongr ⋯).toEmbedding a ∈ ↑c

def WickContraction.congrLift {n m : ℕ} (h : n = m) {c : WickContraction n} (a : { x : Finset (Fin n) // x ∈ ↑c }) : { x : Finset (Fin m) // x ∈ ↑((congr h) c) }

Given a contracted pair in c : WickContraction n the contracted pair in congr h c.

Equations

• WickContraction.congrLift h a = ⟨Finset.map (finCongr h).toEmbedding ↑a, ⋯⟩

@[simp]

theorem WickContraction.congrLift_rfl {n : ℕ} {c : WickContraction n} : congrLift ⋯ = id

theorem WickContraction.congrLift_injective {n m : ℕ} {c : WickContraction n} (h : n = m) : Function.Injective (congrLift h)

theorem WickContraction.congrLift_surjective {n m : ℕ} {c : WickContraction n} (h : n = m) : Function.Surjective (congrLift h)

theorem WickContraction.congrLift_bijective {n m : ℕ} {c : WickContraction n} (h : n = m) : Function.Bijective (congrLift h)

def WickContraction.congrLiftInv {n m : ℕ} (h : n = m) {c : WickContraction n} (a : { x : Finset (Fin m) // x ∈ ↑((congr h) c) }) : { x : Finset (Fin n) // x ∈ ↑c }

Given a contracted pair in c : WickContraction n the contracted pair in congr h c.

Equations

• WickContraction.congrLiftInv h a = ⟨Finset.map (finCongr ⋯).toEmbedding ↑a, ⋯⟩

theorem WickContraction.congrLiftInv_rfl {n : ℕ} {c : WickContraction n} : congrLiftInv ⋯ = id

theorem WickContraction.eq_filter_mem_self {n : ℕ} (c : WickContraction n) : ↑c = Finset.filter (fun (x : Finset (Fin n)) => x ∈ ↑c) Finset.univ

def WickContraction.getDual? {n : ℕ} (c : WickContraction n) (i : Fin n) : Option (Fin n)

For a contraction c : WickContraction n and i : Fin n the j such that {i, j} is a contracted pair in c. If such an j does not exist, this returns none.

Equations

• c.getDual? i = Fin.find fun (j : Fin n) => {i, j} ∈ ↑c

theorem WickContraction.getDual?_congr {n m : ℕ} (h : n = m) (c : WickContraction n) (i : Fin m) : ((congr h) c).getDual? i = Option.map (⇑(finCongr h)) (c.getDual? ((finCongr ⋯) i))

theorem WickContraction.getDual?_congr_get {n m : ℕ} (h : n = m) (c : WickContraction n) (i : Fin m) (hg : (((congr h) c).getDual? i).isSome = true) : (((congr h) c).getDual? i).get hg = (finCongr h) ((c.getDual? ((finCongr ⋯) i)).get ⋯)

theorem WickContraction.getDual?_eq_some_iff_mem {n : ℕ} (c : WickContraction n) (i j : Fin n) : c.getDual? i = some j ↔ {i, j} ∈ ↑c

@[simp]

theorem WickContraction.getDual?_one_eq_none (c : WickContraction 1) (i : Fin 1) : c.getDual? i = none

@[simp]

theorem WickContraction.getDual?_get_self_mem {n : ℕ} (c : WickContraction n) (i : Fin n) (h : (c.getDual? i).isSome = true) : {(c.getDual? i).get h, i} ∈ ↑c

@[simp]

theorem WickContraction.self_getDual?_get_mem {n : ℕ} (c : WickContraction n) (i : Fin n) (h : (c.getDual? i).isSome = true) : {i, (c.getDual? i).get h} ∈ ↑c

theorem WickContraction.getDual?_eq_some_neq {n : ℕ} (c : WickContraction n) (i j : Fin n) (h : c.getDual? i = some j) : ¬i = j

@[simp]

theorem WickContraction.self_neq_getDual?_get {n : ℕ} (c : WickContraction n) (i : Fin n) (h : (c.getDual? i).isSome = true) : ¬i = (c.getDual? i).get h

@[simp]

theorem WickContraction.getDual?_get_self_neq {n : ℕ} (c : WickContraction n) (i : Fin n) (h : (c.getDual? i).isSome = true) : ¬(c.getDual? i).get h = i

theorem WickContraction.getDual?_isSome_iff {n : ℕ} (c : WickContraction n) (i : Fin n) : (c.getDual? i).isSome = true ↔ ∃ (a : { x : Finset (Fin n) // x ∈ ↑c }), i ∈ ↑a

theorem WickContraction.getDual?_isSome_of_mem {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) (i : { x : Fin n // x ∈ ↑a }) : (c.getDual? ↑i).isSome = true

@[simp]

theorem WickContraction.getDual?_getDual?_get_get {n : ℕ} (c : WickContraction n) (i : Fin n) (h : (c.getDual? i).isSome = true) : c.getDual? ((c.getDual? i).get h) = some i

theorem WickContraction.getDual?_getDual?_get_isSome {n : ℕ} (c : WickContraction n) (i : Fin n) (h : (c.getDual? i).isSome = true) : (c.getDual? ((c.getDual? i).get h)).isSome = true

theorem WickContraction.getDual?_getDual?_get_not_none {n : ℕ} (c : WickContraction n) (i : Fin n) (h : (c.getDual? i).isSome = true) : ¬c.getDual? ((c.getDual? i).get h) = none

Extracting parts from a contraction.

def WickContraction.fstFieldOfContract {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : Fin n

The smallest of the two positions in a contracted pair given a Wick contraction.

Equations

• c.fstFieldOfContract a = (Finset.sort (fun (x1 x2 : Fin n) => x1 ≤ x2) ↑a).head ⋯

@[simp]

theorem WickContraction.fstFieldOfContract_congr {n m : ℕ} (h : n = m) (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : ((congr h) c).fstFieldOfContract (congrLift h a) = (finCongr h) (c.fstFieldOfContract a)

def WickContraction.sndFieldOfContract {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : Fin n

The largest of the two positions in a contracted pair given a Wick contraction.

Equations

• c.sndFieldOfContract a = (Finset.sort (fun (x1 x2 : Fin n) => x1 ≤ x2) ↑a).tail.head ⋯

@[simp]

theorem WickContraction.sndFieldOfContract_congr {n m : ℕ} (h : n = m) (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : ((congr h) c).sndFieldOfContract (congrLift h a) = (finCongr h) (c.sndFieldOfContract a)

theorem WickContraction.finset_eq_fstFieldOfContract_sndFieldOfContract {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : ↑a = {c.fstFieldOfContract a, c.sndFieldOfContract a}

theorem WickContraction.fstFieldOfContract_neq_sndFieldOfContract {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : c.fstFieldOfContract a ≠ c.sndFieldOfContract a

theorem WickContraction.fstFieldOfContract_le_sndFieldOfContract {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : c.fstFieldOfContract a ≤ c.sndFieldOfContract a

theorem WickContraction.fstFieldOfContract_lt_sndFieldOfContract {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : c.fstFieldOfContract a < c.sndFieldOfContract a

@[simp]

theorem WickContraction.fstFieldOfContract_mem {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : c.fstFieldOfContract a ∈ ↑a

theorem WickContraction.fstFieldOfContract_getDual?_isSome {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : (c.getDual? (c.fstFieldOfContract a)).isSome = true

@[simp]

theorem WickContraction.fstFieldOfContract_getDual? {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : c.getDual? (c.fstFieldOfContract a) = some (c.sndFieldOfContract a)

@[simp]

theorem WickContraction.sndFieldOfContract_mem {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : c.sndFieldOfContract a ∈ ↑a

theorem WickContraction.sndFieldOfContract_getDual?_isSome {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : (c.getDual? (c.sndFieldOfContract a)).isSome = true

@[simp]

theorem WickContraction.sndFieldOfContract_getDual? {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : c.getDual? (c.sndFieldOfContract a) = some (c.fstFieldOfContract a)

theorem WickContraction.eq_fstFieldOfContract_of_mem {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) (i j : Fin n) (hi : i ∈ ↑a) (hj : j ∈ ↑a) (hij : i < j) : c.fstFieldOfContract a = i

theorem WickContraction.eq_sndFieldOfContract_of_mem {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) (i j : Fin n) (hi : i ∈ ↑a) (hj : j ∈ ↑a) (hij : i < j) : c.sndFieldOfContract a = j

def WickContraction.contractEquivFinTwo {n : ℕ} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) : { x : Fin n // x ∈ ↑a } ≃ Fin 2

As a type, any pair of contractions is equivalent to Fin 2 with 0 being associated with c.fstFieldOfContract a and 1 being associated with c.sndFieldOfContract.

Equations

• One or more equations did not get rendered due to their size.

theorem WickContraction.prod_finset_eq_mul_fst_snd {n : ℕ} {M : Type u_1} (c : WickContraction n) (a : { x : Finset (Fin n) // x ∈ ↑c }) (f : { x : Fin n // x ∈ ↑a } → M) [CommMonoid M] : ∏ x : { x : Fin n // x ∈ ↑a }, f x = f ⟨c.fstFieldOfContract a, ⋯⟩ * f ⟨c.sndFieldOfContract a, ⋯⟩

def WickContraction.GradingCompliant {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : Prop

For a field specification 𝓕, φs a list of 𝓕.FieldOp and a Wick contraction φsΛ of φs, the Wick contraction φsΛ is said to be GradingCompliant if for every pair in φsΛ the contracted fields are either both fermionic or both bosonic. In other words, in a GradingCompliant Wick contraction if no contracted pairs occur between fermionic and bosonic fields.

Equations

• WickContraction.GradingCompliant φs φsΛ = ∀ (a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }), 𝓕.fieldOpStatistic φs[φsΛ.fstFieldOfContract a] = 𝓕.fieldOpStatistic φs[φsΛ.sndFieldOfContract a]

theorem WickContraction.gradingCompliant_congr {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (φsΛ : WickContraction φs.length) : GradingCompliant φs φsΛ ↔ GradingCompliant φs' ((congr ⋯) φsΛ)

def WickContraction.sigmaContractedEquiv {n : ℕ} (c : WickContraction n) : (a : { x : Finset (Fin n) // x ∈ ↑c }) × { x : Fin n // x ∈ ↑a } ≃ { x : Fin n // (c.getDual? x).isSome = true }

An equivalence from the sigma type (a : c.1) × a to the subtype of Fin n consisting of those positions which are contracted.

Equations

• One or more equations did not get rendered due to their size.