1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickContraction
  5. Involutions
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.WickContraction.Basic

Involution associated with a contraction

@[expose] public section

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.

def toInvolution : {f : Fin n → Fin n // Function.Involutive f} := ⟨fun i => if h : (c.getDual? i).isSome then (c.getDual? i).get h else i, 𝓕:FieldSpecificationn:ℕc:WickContraction n⊢ Function.Involutive fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i 𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin n⊢ (fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) ((fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) i) = i 𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ (fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) ((fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) i) = i𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nh:¬(c.getDual? i).isSome = true⊢ (fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) ((fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) i) = i 𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nh:(c.getDual? i).isSome = true⊢ (fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) ((fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) i) = i All goals completed! 🐙 𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nh:¬(c.getDual? i).isSome = true⊢ (fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) ((fun i => if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i) i) = i All goals completed! 🐙⟩

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.

𝓕:FieldSpecificationn:ℕc:WickContraction nf:{ f // Function.Involutive f }i:Fin nha:{i, ↑f i}.card = 2 ∧ ∃ i_1, {i_1, ↑f i_1} = {i, ↑f i}j:Fin nhb:{j, ↑f j}.card = 2 ∧ ∃ i, {i, ↑f i} = {j, ↑f j}h:¬i = jhi:¬i = ↑f j⊢ ¬j = i𝓕:FieldSpecificationn:ℕc:WickContraction nf:{ f // Function.Involutive f }i:Fin nha:{i, ↑f i}.card = 2 ∧ ∃ i_1, {i_1, ↑f i_1} = {i, ↑f i}j:Fin nhb:{j, ↑f j}.card = 2 ∧ ∃ i, {i, ↑f i} = {j, ↑f j}h:¬i = jhi:¬i = ↑f j⊢ Function.Injective ↑f 𝓕:FieldSpecificationn:ℕc:WickContraction nf:{ f // Function.Involutive f }i:Fin nha:{i, ↑f i}.card = 2 ∧ ∃ i_1, {i_1, ↑f i_1} = {i, ↑f i}j:Fin nhb:{j, ↑f j}.card = 2 ∧ ∃ i, {i, ↑f i} = {j, ↑f j}h:¬i = jhi:¬i = ↑f j⊢ Function.Injective ↑f All goals completed! 🐙⟩
n:ℕf:{ f // Function.Involutive f }a:↥↑(fromInvolution f)ha2:(↑a).card = 2 ∧ ∃ i, {i, ↑f i} = ↑aj:Fin nh:{j, ↑f j} = ↑ahj:↑f j ≠ j⊢ j ≠ ↑f j All goals completed! 🐙 n:ℕf:{ f // Function.Involutive f }i:Fin n⊢ ↑f i ≠ i → ∃ a, i ∈ ↑a n:ℕf:{ f // Function.Involutive f }i:Fin nhi:↑f i ≠ i⊢ ∃ a, i ∈ ↑a use ⟨{i, f.1 i}, n:ℕf:{ f // Function.Involutive f }i:Fin nhi:↑f i ≠ i⊢ {i, ↑f i} ∈ ↑(fromInvolution f) n:ℕf:{ f // Function.Involutive f }i:Fin nhi:↑f i ≠ i⊢ {i, ↑f i}.card = 2 All goals completed! 🐙⟩ All goals completed! 🐙n:ℕf:{ f // Function.Involutive f }i:Fin nh:((fromInvolution f).getDual? i).isSome = true⊢ {i, ↑f i} ∈ ↑(fromInvolution f) n:ℕf:{ f // Function.Involutive f }i:Fin nh:((fromInvolution f).getDual? i).isSome = true⊢ {i, ↑f i}.card = 2 All goals completed! 🐙@[simp] lemma fromInvolution_getDual?_get (f : {f : Fin n → Fin n // Function.Involutive f}) (i : Fin n) (h : ((fromInvolution f).getDual? i).isSome) : ((fromInvolution f).getDual? i).get h = (f.1 i) := Option.get_of_mem h (fromInvolution_getDual?_eq_some f i h)lemma toInvolution_fromInvolution : fromInvolution c.toInvolution = c := n:ℕc:WickContraction n⊢ fromInvolution c.toInvolution = c n:ℕc:WickContraction n⊢ ↑(fromInvolution c.toInvolution) = ↑c n:ℕc:WickContraction n⊢ {x | x.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = x} = ↑c n:ℕc:WickContraction na:Finset (Fin n)⊢ a ∈ {x | x.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = x} ↔ a ∈ ↑c n:ℕc:WickContraction na:Finset (Fin n)⊢ (a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = a) ↔ a ∈ ↑c n:ℕc:WickContraction na:Finset (Fin n)⊢ (a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = a) → a ∈ ↑cn:ℕc:WickContraction na:Finset (Fin n)⊢ a ∈ ↑c → a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = a n:ℕc:WickContraction na:Finset (Fin n)⊢ (a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = a) → a ∈ ↑c n:ℕc:WickContraction na:Finset (Fin n)h:a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = a⊢ a ∈ ↑c n:ℕc:WickContraction na:Finset (Fin n)h:a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = ai:Fin nhi:{i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = a⊢ a ∈ ↑c n:ℕc:WickContraction na:Finset (Fin n)h:a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = ai:Fin nh✝:(c.getDual? i).isSome = truehi:{i, (c.getDual? i).get h✝} = a⊢ a ∈ ↑cn:ℕc:WickContraction na:Finset (Fin n)h:a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = ai:Fin nh✝:¬(c.getDual? i).isSome = truehi:{i, i} = a⊢ a ∈ ↑c n:ℕc:WickContraction na:Finset (Fin n)h:a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = ai:Fin nh✝:(c.getDual? i).isSome = truehi:{i, (c.getDual? i).get h✝} = a⊢ a ∈ ↑c n:ℕc:WickContraction ni:Fin nh✝:(c.getDual? i).isSome = trueh:{i, (c.getDual? i).get h✝}.card = 2 ∧ ∃ i_1, {i_1, if h : (c.getDual? i_1).isSome = true then (c.getDual? i_1).get h else i_1} = {i, (c.getDual? i).get h✝}⊢ {i, (c.getDual? i).get h✝} ∈ ↑c All goals completed! 🐙 n:ℕc:WickContraction na:Finset (Fin n)h:a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = ai:Fin nh✝:¬(c.getDual? i).isSome = truehi:{i, i} = a⊢ a ∈ ↑c n:ℕc:WickContraction ni:Fin nh✝:¬(c.getDual? i).isSome = trueh:{i, i}.card = 2 ∧ ∃ i_1, {i_1, if h : (c.getDual? i_1).isSome = true then (c.getDual? i_1).get h else i_1} = {i, i}⊢ {i, i} ∈ ↑c All goals completed! 🐙 n:ℕc:WickContraction na:Finset (Fin n)⊢ a ∈ ↑c → a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = a n:ℕc:WickContraction na:Finset (Fin n)ha:a ∈ ↑c⊢ a.card = 2 ∧ ∃ i, {i, if h : (c.getDual? i).isSome = true then (c.getDual? i).get h else i} = a n:ℕc:WickContraction na:Finset (Fin n)ha:a ∈ ↑c⊢ {c.fstFieldOfContract ⟨a, ha⟩, if h : (c.getDual? (c.fstFieldOfContract ⟨a, ha⟩)).isSome = true then (c.getDual? (c.fstFieldOfContract ⟨a, ha⟩)).get h else c.fstFieldOfContract ⟨a, ha⟩} = a n:ℕc:WickContraction na:Finset (Fin n)ha:a ∈ ↑c⊢ {c.fstFieldOfContract ⟨a, ha⟩, c.sndFieldOfContract ⟨a, ha⟩} = a All goals completed! 🐙lemma fromInvolution_toInvolution (f : {f : Fin n → Fin n // Function.Involutive f}) : (fromInvolution f).toInvolution = f := n:ℕf:{ f // Function.Involutive f }⊢ (fromInvolution f).toInvolution = f n:ℕf:{ f // Function.Involutive f }⊢ ↑(fromInvolution f).toInvolution = ↑f n:ℕf:{ f // Function.Involutive f }i:Fin n⊢ ↑(fromInvolution f).toInvolution i = ↑f i n:ℕf:{ f // Function.Involutive f }i:Fin n⊢ (if h : ((fromInvolution f).getDual? i).isSome = true then ((fromInvolution f).getDual? i).get h else i) = ↑f i n:ℕf:{ f // Function.Involutive f }i:Fin nh✝:((fromInvolution f).getDual? i).isSome = true⊢ ((fromInvolution f).getDual? i).get h✝ = ↑f in:ℕf:{ f // Function.Involutive f }i:Fin nh✝:¬((fromInvolution f).getDual? i).isSome = true⊢ i = ↑f i n:ℕf:{ f // Function.Involutive f }i:Fin nh✝:((fromInvolution f).getDual? i).isSome = true⊢ ((fromInvolution f).getDual? i).get h✝ = ↑f i All goals completed! 🐙 n:ℕf:{ f // Function.Involutive f }i:Fin nh✝:¬((fromInvolution f).getDual? i).isSome = true⊢ i = ↑f i n:ℕf:{ f // Function.Involutive f }i:Fin nh:¬((fromInvolution f).getDual? i).isSome = true⊢ i = ↑f i n:ℕf:{ f // Function.Involutive f }i:Fin nh:↑f i = i⊢ i = ↑f i All goals completed! 🐙

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.

def equivInvolution : WickContraction n ≃ {f : Fin n → Fin n // Function.Involutive f} where toFun := toInvolution invFun := fromInvolution left_inv := toInvolution_fromInvolution right_inv := fromInvolution_toInvolution