Inserting an element into a contraction

Inserting an element into a contraction

def WickContraction.insertAndContractNat {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Option { x : Fin n // x ∈ c.uncontracted }) : WickContraction n.succ

Given a Wick contraction c for n, a position i : Fin n.succ and an optional uncontracted element j : Option (c.uncontracted) of c. The Wick contraction for n.succ formed by 'inserting' i into Fin n and contracting it optionally with j.

Equations

• c.insertAndContractNat i none = ⟨Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c, ⋯⟩
• c.insertAndContractNat i (some j_2) = ⟨insert {i, i.succAbove ↑j_2} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c), ⋯⟩

theorem WickContraction.insertAndContractNat_of_isSome {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Option { x : Fin n // x ∈ c.uncontracted }) (hj : j.isSome = true) : ↑(c.insertAndContractNat i j) = insert {i, i.succAbove ↑(j.get hj)} (Finset.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding ↑c)

@[simp]

theorem WickContraction.self_mem_uncontracted_of_insertAndContractNat_none {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : i ∈ (c.insertAndContractNat i none).uncontracted

@[simp]

theorem WickContraction.self_not_mem_uncontracted_of_insertAndContractNat_some {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) : i ∉ (c.insertAndContractNat i (some j)).uncontracted

theorem WickContraction.insertAndContractNat_succAbove_mem_uncontracted_iff {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : i.succAbove j ∈ (c.insertAndContractNat i none).uncontracted ↔ j ∈ c.uncontracted

@[simp]

theorem WickContraction.mem_uncontracted_insertAndContractNat_none_iff {n : ℕ} (c : WickContraction n) (i k : Fin n.succ) : k ∈ (c.insertAndContractNat i none).uncontracted ↔ k = i ∨ ∃ (j : Fin n), k = i.succAbove j ∧ j ∈ c.uncontracted

theorem WickContraction.insertAndContractNat_none_uncontracted {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : (c.insertAndContractNat i none).uncontracted = insert i (Finset.map i.succAboveEmb c.uncontracted)

@[simp]

theorem WickContraction.mem_uncontracted_insertAndContractNat_some_iff {n : ℕ} (c : WickContraction n) (i k : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) : k ∈ (c.insertAndContractNat i (some j)).uncontracted ↔ ∃ (z : Fin n), k = i.succAbove z ∧ z ∈ c.uncontracted ∧ z ≠ ↑j

theorem WickContraction.insertAndContractNat_some_uncontracted {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) : (c.insertAndContractNat i (some j)).uncontracted = Finset.map i.succAboveEmb (c.uncontracted.erase ↑j)

Insert and getDual?

theorem WickContraction.insertAndContractNat_none_getDual?_isNone {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : ((c.insertAndContractNat i none).getDual? i).isNone = true

@[simp]

theorem WickContraction.insertAndContractNat_none_getDual?_eq_none {n : ℕ} (c : WickContraction n) (i : Fin n.succ) : (c.insertAndContractNat i none).getDual? i = none

@[simp]

theorem WickContraction.insertAndContractNat_succAbove_getDual?_eq_none_iff {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : (c.insertAndContractNat i none).getDual? (i.succAbove j) = none ↔ c.getDual? j = none

@[simp]

theorem WickContraction.insertAndContractNat_succAbove_getDual?_isSome_iff {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : ((c.insertAndContractNat i none).getDual? (i.succAbove j)).isSome = true ↔ (c.getDual? j).isSome = true

@[simp]

theorem WickContraction.insertAndContractNat_succAbove_getDual?_get {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Fin n) (h : ((c.insertAndContractNat i none).getDual? (i.succAbove j)).isSome = true) : ((c.insertAndContractNat i none).getDual? (i.succAbove j)).get h = i.succAbove ((c.getDual? j).get ⋯)

@[simp]

theorem WickContraction.insertAndContractNat_some_getDual?_eq {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) : (c.insertAndContractNat i (some j)).getDual? i = some (i.succAbove ↑j)

@[simp]

theorem WickContraction.insertAndContractNat_some_getDual?_neq_none {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) (k : Fin n) (hkj : k ≠ ↑j) : (c.insertAndContractNat i (some j)).getDual? (i.succAbove k) = none ↔ c.getDual? k = none

@[simp]

theorem WickContraction.insertAndContractNat_some_getDual?_neq_isSome {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) (k : Fin n) (hkj : k ≠ ↑j) : ((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).isSome = true ↔ (c.getDual? k).isSome = true

@[simp]

theorem WickContraction.insertAndContractNat_some_getDual?_neq_isSome_get {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) (k : Fin n) (hkj : k ≠ ↑j) (h : ((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).isSome = true) : ((c.insertAndContractNat i (some j)).getDual? (i.succAbove k)).get h = i.succAbove ((c.getDual? k).get ⋯)

@[simp]

theorem WickContraction.insertAndContractNat_some_getDual?_of_neq {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) (k : Fin n) (hkj : k ≠ ↑j) : (c.insertAndContractNat i (some j)).getDual? (i.succAbove k) = Option.map i.succAbove (c.getDual? k)

Interaction with erase.

@[simp]

theorem WickContraction.insertAndContractNat_erase {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Option { x : Fin n // x ∈ c.uncontracted }) : (c.insertAndContractNat i j).erase i = c

theorem WickContraction.insertAndContractNat_getDualErase {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Option { x : Fin n // x ∈ c.uncontracted }) : (c.insertAndContractNat i j).getDualErase i = (uncontractedCongr ⋯) j

@[simp]

theorem WickContraction.erase_insert {n : ℕ} (c : WickContraction n.succ) (i : Fin n.succ) : (c.erase i).insertAndContractNat i (c.getDualErase i) = c

def WickContraction.insertLift {n : ℕ} {c : WickContraction n} (i : Fin n.succ) (j : Option { x : Fin n // x ∈ c.uncontracted }) (a : { x : Finset (Fin n) // x ∈ ↑c }) : { x : Finset (Fin n.succ) // x ∈ ↑(c.insertAndContractNat i j) }

Lifts a contraction in c to a contraction in (c.insert i j).

Equations

• WickContraction.insertLift i j a = ⟨Finset.map i.succAboveEmb ↑a, ⋯⟩

theorem WickContraction.insertLift_injective {n : ℕ} {c : WickContraction n} (i : Fin n.succ) (j : Option { x : Fin n // x ∈ c.uncontracted }) : Function.Injective (insertLift i j)

theorem WickContraction.insertLift_none_surjective {n : ℕ} {c : WickContraction n} (i : Fin n.succ) : Function.Surjective (insertLift i none)

theorem WickContraction.insertLift_none_bijective {n : ℕ} {c : WickContraction n} (i : Fin n.succ) : Function.Bijective (insertLift i none)

@[simp]

theorem WickContraction.insertAndContractNat_fstFieldOfContract {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Option { x : Fin n // x ∈ c.uncontracted }) (a : { x : Finset (Fin n) // x ∈ ↑c }) : (c.insertAndContractNat i j).fstFieldOfContract (insertLift i j a) = i.succAbove (c.fstFieldOfContract a)

@[simp]

theorem WickContraction.insertAndContractNat_sndFieldOfContract {n : ℕ} (c : WickContraction n) (i : Fin n.succ) (j : Option { x : Fin n // x ∈ c.uncontracted }) (a : { x : Finset (Fin n) // x ∈ ↑c }) : (c.insertAndContractNat i j).sndFieldOfContract (insertLift i j a) = i.succAbove (c.sndFieldOfContract a)

def WickContraction.insertLiftSome {n : ℕ} {c : WickContraction n} (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) (a : Unit ⊕ { x : Finset (Fin n) // x ∈ ↑c }) : { x : Finset (Fin n.succ) // x ∈ ↑(c.insertAndContractNat i (some j)) }

Given a contracted pair for a Wick contraction WickContraction n, the corresponding contracted pair of a wick contraction (c.insert i (some j)) formed by inserting an element i into the contraction.

Equations

• WickContraction.insertLiftSome i j (Sum.inl PUnit.unit) = ⟨{i, i.succAbove ↑j}, ⋯⟩
• WickContraction.insertLiftSome i j (Sum.inr a_2) = WickContraction.insertLift i (some j) a_2

theorem WickContraction.insertLiftSome_injective {n : ℕ} {c : WickContraction n} (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) : Function.Injective (insertLiftSome i j)

theorem WickContraction.insertLiftSome_surjective {n : ℕ} {c : WickContraction n} (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) : Function.Surjective (insertLiftSome i j)

theorem WickContraction.insertLiftSome_bijective {n : ℕ} {c : WickContraction n} (i : Fin n.succ) (j : { x : Fin n // x ∈ c.uncontracted }) : Function.Bijective (insertLiftSome i j)

insertAndContractNat c i none and injection

theorem WickContraction.insertAndContractNat_injective {n : ℕ} (i : Fin n.succ) : Function.Injective fun (c : WickContraction n) => c.insertAndContractNat i none

theorem WickContraction.insertAndContractNat_surjective_on_nodual {n : ℕ} (i : Fin n.succ) (c : WickContraction n.succ) (hc : c.getDual? i = none) : ∃ (c' : WickContraction n), c'.insertAndContractNat i none = c

theorem WickContraction.insertAndContractNat_bijective {n : ℕ} (i : Fin n.succ) : Function.Bijective fun (c : WickContraction n) => ⟨c.insertAndContractNat i none, ⋯⟩