Involution associated with a contraction

def WickContraction.toInvolution {n : ℕ} (c : WickContraction n) : { f : Fin n → Fin n // Function.Involutive f }

The involution of Fin n associated with a Wick contraction c : WickContraction n as follows. If i : Fin n is contracted in c then it is taken to its dual, otherwise it is taken to itself.

Equations

• c.toInvolution = ⟨fun (i : Fin n) => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i, ⋯⟩

def WickContraction.fromInvolution {n : ℕ} (f : { f : Fin n → Fin n // Function.Involutive f }) : WickContraction n

The Wick contraction formed by an involution f of Fin n by taking as the contracted sets of the contraction the orbits of f of cardinality 2.

Equations

• WickContraction.fromInvolution f = ⟨{a : Finset (Fin n) | a.card = 2 ∧ ∃ (i : Fin n), {i, ↑f i} = a}, ⋯⟩

@[simp]

theorem WickContraction.fromInvolution_getDual?_isSome {n : ℕ} (f : { f : Fin n → Fin n // Function.Involutive f }) (i : Fin n) : ((fromInvolution f).getDual? i).isSome = true ↔ ↑f i ≠ i

theorem WickContraction.fromInvolution_getDual?_eq_some {n : ℕ} (f : { f : Fin n → Fin n // Function.Involutive f }) (i : Fin n) (h : ((fromInvolution f).getDual? i).isSome = true) : (fromInvolution f).getDual? i = some (↑f i)

@[simp]

theorem WickContraction.fromInvolution_getDual?_get {n : ℕ} (f : { f : Fin n → Fin n // Function.Involutive f }) (i : Fin n) (h : ((fromInvolution f).getDual? i).isSome = true) : ((fromInvolution f).getDual? i).get h = ↑f i

theorem WickContraction.toInvolution_fromInvolution {n : ℕ} (c : WickContraction n) : fromInvolution c.toInvolution = c

theorem WickContraction.fromInvolution_toInvolution {n : ℕ} (f : { f : Fin n → Fin n // Function.Involutive f }) : (fromInvolution f).toInvolution = f

def WickContraction.equivInvolution {n : ℕ} : WickContraction n ≃ { f : Fin n → Fin n // Function.Involutive f }

The equivalence between Wick contractions for n and involutions of Fin n. The involution of Fin n associated with a Wick contraction c : WickContraction n as follows. If i : Fin n is contracted in c then it is taken to its dual, otherwise it is taken to itself.

Equations

• WickContraction.equivInvolution = { toFun := WickContraction.toInvolution, invFun := WickContraction.fromInvolution, left_inv := ⋯, right_inv := ⋯ }