Splitting a pairing along a closed finite block

A pairing which preserves a finite block is exactly a pair consisting of a pairing on that block and a pairing on its complement. This elementary equivalence is the finite combinatorial engine needed to sum all primitive pairings on one R-322/R-324 block before proceeding to the remaining variables.

def Anderson4D.PartialPairing.combineAlongFinset {α : Type u_1} [DecidableEq α] (B : Finset α) (κB : PartialPairing ↥B) (κC : PartialPairing { i : α // i ∉ B }) : PartialPairing α

Combine pairings on a finite block and its complement.

Equations

• Anderson4D.PartialPairing.combineAlongFinset B κB κC = { toFun := fun (i : α) => if hi : i ∈ B then ↑(κB ⟨i, hi⟩) else ↑(κC ⟨i, hi⟩), involutive := ⋯ }

@[simp]

theorem Anderson4D.PartialPairing.combineAlongFinset_apply_mem {α : Type u_1} [DecidableEq α] (B : Finset α) (κB : PartialPairing ↥B) (κC : PartialPairing { i : α // i ∉ B }) (i : α) (hi : i ∈ B) : (combineAlongFinset B κB κC) i = ↑(κB ⟨i, hi⟩)

@[simp]

theorem Anderson4D.PartialPairing.combineAlongFinset_apply_notMem {α : Type u_1} [DecidableEq α] (B : Finset α) (κB : PartialPairing ↥B) (κC : PartialPairing { i : α // i ∉ B }) (i : α) (hi : i ∉ B) : (combineAlongFinset B κB κC) i = ↑(κC ⟨i, hi⟩)

theorem Anderson4D.PartialPairing.combineAlongFinset_mapsTo {α : Type u_1} [DecidableEq α] (B : Finset α) (κB : PartialPairing ↥B) (κC : PartialPairing { i : α // i ∉ B }) (i : α) : i ∈ B → (combineAlongFinset B κB κC) i ∈ B

@[reducible, inline]

abbrev Anderson4D.PartialPairing.ClosedOn {α : Type u_1} (B : Finset α) : Type u_1

Pairings preserving B, with the closure certificate included in the finite type.

Equations

• Anderson4D.PartialPairing.ClosedOn B = { κ : Anderson4D.PartialPairing α // ∀ i ∈ B, κ i ∈ B }

def Anderson4D.PartialPairing.closedOnEquiv {α : Type u_1} [DecidableEq α] (B : Finset α) : ClosedOn B ≃ PartialPairing ↥B × PartialPairing { i : α // i ∉ B }

Exact decomposition of a pairing along a closed finite block.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.closedOnEquiv_apply_fst {α : Type u_1} [DecidableEq α] (B : Finset α) (κ : ClosedOn B) : ((closedOnEquiv B) κ).1 = (↑κ).restrictTo ⋯

@[simp]

theorem Anderson4D.PartialPairing.closedOnEquiv_apply_snd {α : Type u_1} [DecidableEq α] (B : Finset α) (κ : ClosedOn B) : ((closedOnEquiv B) κ).2 = (↑κ).restrictCompl ⋯

theorem Anderson4D.PartialPairing.combineAlongFinset_isFull_iff {α : Type u_1} [DecidableEq α] (B : Finset α) (κB : PartialPairing ↥B) (κC : PartialPairing { i : α // i ∉ B }) : (combineAlongFinset B κB κC).IsFull ↔ κB.IsFull ∧ κC.IsFull

Fullness of the combined pairing is equivalent to fullness on the block and on its complement.

theorem Anderson4D.PartialPairing.restrictTo_isFull_of_ne {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) (B : Finset α) (hclosed : ∀ i ∈ B, κ i ∈ B) (hne : ∀ i ∈ B, κ i ≠ i) : (κ.restrictTo hclosed).IsFull

Restriction to a closed block containing no fixed point is a full pairing.

theorem Anderson4D.PartialPairing.restrictCompl_isFull {α : Type u_1} (κ : PartialPairing α) (B : Finset α) (hclosed : ∀ i ∈ B, κ i ∈ B) (hfull : κ.IsFull) : (κ.restrictCompl hclosed).IsFull

If the ambient pairing is full, its restriction to the complement of a closed block is full as well.

theorem Anderson4D.PartialPairing.sum_closedOn_eq_sum_restrictions {α : Type u_1} [DecidableEq α] [Fintype α] {M : Type u_2} [AddCommMonoid M] (B : Finset α) (F : ClosedOn B → M) : ∑ κ : ClosedOn B, F κ = ∑ κB : PartialPairing ↥B, ∑ κC : PartialPairing { i : α // i ∉ B }, F ((closedOnEquiv B).symm (κB, κC))

A sum over pairings preserving B is exactly an iterated sum over the pairing on B and the pairing on its complement.