Head recursion for partial pairings

This file classifies a partial pairing after adjoining one distinguished index. The distinguished index is either fixed, or it is paired with a unique old index and the remaining involution lives on the complement of that partner. This is the finite combinatorial split used by the creation--contraction recursion for Wick products.

def Anderson4D.PartialPairing.optionFixed {α : Type u_1} (κ : PartialPairing α) : PartialPairing (Option α)

Adjoin a new fixed point to a partial pairing.

Equations

• κ.optionFixed = { toFun := fun (x : Option α) => match x with | none => none | some i => some (κ i), involutive := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.optionFixed_none {α : Type u_1} (κ : PartialPairing α) : κ.optionFixed none = none

@[simp]

theorem Anderson4D.PartialPairing.optionFixed_some {α : Type u_1} (κ : PartialPairing α) (i : α) : κ.optionFixed (some i) = some (κ i)

def Anderson4D.PartialPairing.optionPaired {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : PartialPairing (Option α)

Pair the new point with j, and use κ on the complement of j.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.optionPaired_none {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : (optionPaired j κ) none = some j

@[simp]

theorem Anderson4D.PartialPairing.optionPaired_partner {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : (optionPaired j κ) (some j) = none

@[simp]

theorem Anderson4D.PartialPairing.optionPaired_some_ne {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) (i : α) (hi : i ≠ j) : (optionPaired j κ) (some i) = some ↑(κ ⟨i, hi⟩)

def Anderson4D.PartialPairing.optionFixedComplEquiv {α : Type u_1} : { o : Option α // o ∉ {none} } ≃ α

The complement of none in Option α is canonically α.

Equations

• Anderson4D.PartialPairing.optionFixedComplEquiv = { toFun := fun (o : { o : Option α // o ∉ {none} }) => (↑o).get ⋯, invFun := fun (i : α) => ⟨some i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.optionFixedComplEquiv_symm_apply {α : Type u_1} (i : α) : optionFixedComplEquiv.symm i = ⟨some i, ⋯⟩

def Anderson4D.PartialPairing.optionPairedComplEquiv {α : Type u_1} [DecidableEq α] (j : α) : { o : Option α // o ∉ {none, some j} } ≃ { i : α // i ≠ j }

The complement of none and some j is canonically the complement of j in α.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.optionPairedComplEquiv_symm_apply {α : Type u_1} [DecidableEq α] (j : α) (i : { i : α // i ≠ j }) : (optionPairedComplEquiv j).symm i = ⟨some ↑i, ⋯⟩

def Anderson4D.PartialPairing.optionTailOfFixed {α : Type u_1} (κ : PartialPairing (Option α)) (hκ : κ none = none) : PartialPairing α

Removing a fixed new point leaves a pairing of the old carrier.

Equations

• κ.optionTailOfFixed hκ = (Anderson4D.PartialPairing.congr Anderson4D.PartialPairing.optionFixedComplEquiv) (κ.restrictCompl ⋯)

@[simp]

theorem Anderson4D.PartialPairing.optionTailOfFixed_apply {α : Type u_1} (κ : PartialPairing (Option α)) (hκ : κ none = none) (i : α) : some ((κ.optionTailOfFixed hκ) i) = κ (some i)

def Anderson4D.PartialPairing.optionTailOfPaired {α : Type u_1} [DecidableEq α] (κ : PartialPairing (Option α)) (j : α) (hκ : κ none = some j) : PartialPairing { i : α // i ≠ j }

Removing the new point and its partner leaves a pairing of the complement of that partner.

Equations

• κ.optionTailOfPaired j hκ = (Anderson4D.PartialPairing.congr (Anderson4D.PartialPairing.optionPairedComplEquiv j)) (κ.restrictCompl ⋯)

@[simp]

theorem Anderson4D.PartialPairing.optionTailOfPaired_apply {α : Type u_1} [DecidableEq α] (κ : PartialPairing (Option α)) (j : α) (hκ : κ none = some j) (i : { i : α // i ≠ j }) : some ↑((κ.optionTailOfPaired j hκ) i) = κ (some ↑i)

theorem Anderson4D.PartialPairing.optionFixed_optionTailOfFixed {α : Type u_1} (κ : PartialPairing (Option α)) (hκ : κ none = none) : (κ.optionTailOfFixed hκ).optionFixed = κ

Reattaching a fixed head after removing it recovers the pairing.

theorem Anderson4D.PartialPairing.optionTailOfFixed_optionFixed {α : Type u_1} (κ : PartialPairing α) : κ.optionFixed.optionTailOfFixed ⋯ = κ

Removing the fixed head adjoined by optionFixed recovers the tail.

theorem Anderson4D.PartialPairing.optionPaired_optionTailOfPaired {α : Type u_1} [DecidableEq α] (κ : PartialPairing (Option α)) (j : α) (hκ : κ none = some j) : optionPaired j (κ.optionTailOfPaired j hκ) = κ

Reattaching a paired head and its partner after removing them recovers the pairing.

theorem Anderson4D.PartialPairing.optionTailOfPaired_optionPaired {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : (optionPaired j κ).optionTailOfPaired j ⋯ = κ

Removing the head and partner adjoined by optionPaired recovers the complement pairing.

def Anderson4D.PartialPairing.optionHeadClassify {α : Type u_1} [DecidableEq α] : PartialPairing (Option α) → PartialPairing α ⊕ (j : α) × PartialPairing { i : α // i ≠ j }

Classification map underlying optionHeadEquiv.

Equations

• κ.optionHeadClassify = match h : κ none with | none => Sum.inl (κ.optionTailOfFixed h) | some j => Sum.inr ⟨j, κ.optionTailOfPaired j h⟩

def Anderson4D.PartialPairing.optionHeadAssemble {α : Type u_1} [DecidableEq α] : PartialPairing α ⊕ (j : α) × PartialPairing { i : α // i ≠ j } → PartialPairing (Option α)

Assembly map underlying optionHeadEquiv.

Equations

• Anderson4D.PartialPairing.optionHeadAssemble (Sum.inl κ) = κ.optionFixed
• Anderson4D.PartialPairing.optionHeadAssemble (Sum.inr d) = Anderson4D.PartialPairing.optionPaired d.fst d.snd

theorem Anderson4D.PartialPairing.optionHeadAssemble_classify {α : Type u_1} [DecidableEq α] (κ : PartialPairing (Option α)) : optionHeadAssemble κ.optionHeadClassify = κ

theorem Anderson4D.PartialPairing.optionHeadClassify_assemble {α : Type u_1} [DecidableEq α] (s : PartialPairing α ⊕ (j : α) × PartialPairing { i : α // i ≠ j }) : (optionHeadAssemble s).optionHeadClassify = s

def Anderson4D.PartialPairing.optionHeadEquiv {α : Type u_1} [DecidableEq α] : PartialPairing (Option α) ≃ PartialPairing α ⊕ (j : α) × PartialPairing { i : α // i ≠ j }

Head classification equivalence. A pairing on Option α has either a fixed head and a pairing on α, or a unique partner j and a pairing on the complement of j.

Equations

• Anderson4D.PartialPairing.optionHeadEquiv = { toFun := Anderson4D.PartialPairing.optionHeadClassify, invFun := Anderson4D.PartialPairing.optionHeadAssemble, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.optionHeadEquiv_symm_inl {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) : optionHeadEquiv.symm (Sum.inl κ) = κ.optionFixed

@[simp]

theorem Anderson4D.PartialPairing.optionHeadEquiv_symm_inr {α : Type u_1} [DecidableEq α] (d : (j : α) × PartialPairing { i : α // i ≠ j }) : optionHeadEquiv.symm (Sum.inr d) = optionPaired d.fst d.snd

def Anderson4D.PartialPairing.finHeadEquiv (n : ℕ) : PartialPairing (Fin (n + 1)) ≃ PartialPairing (Fin n) ⊕ (j : Fin n) × PartialPairing { i : Fin n // i ≠ j }

Finite-ordinal form of optionHeadEquiv: after identifying the new zero of Fin (n + 1) with none, a pairing either fixes zero or pairs it with a unique old index.

Equations

• Anderson4D.PartialPairing.finHeadEquiv n = (Anderson4D.PartialPairing.congr (finSuccEquiv n)).trans Anderson4D.PartialPairing.optionHeadEquiv