Shuffles and the wedge formula for left Kan extensions along the block sum #
A subset S of Fin n determines the shuffle FiniteBijection.shuffle S : mk #S ⊗ mk #Sᶜ ⟶ n,
which enumerates S on the first block and its complement on the second block, both in
increasing order. Every bijection σ : p ⊗ q ⟶ n factors uniquely as a pair of block
bijections followed by the shuffle of the image blockImage σ of the first block:
(blockLeft σ ⊗ₘ blockRight σ) ≫ shuffle (blockImage σ) = σ. Equivalently, the comma category
CostructuredArrow (tensor FiniteBijection) n is equivalent to the discrete category on the
subsets of Fin n (shuffleFunctor n).
Consequently, a pointwise left Kan extension L of a functor H along the block sum has levels
L(n) = ∐_{S ⊆ Fin n} H(#S, #Sᶜ), with the summand of S included along the shuffle of S
(IsPointwiseLeftKanExtensionAt.isColimitShuffleCofan). For Day convolution of symmetric
sequences this is the wedge formula of Hovey, Shipley and Smith,
(X ⊗ Y)_n = ⋁_{p+q=n} (Σ_n)₊ ∧_{Σ_p × Σ_q} (X_p ∧ Y_q):
the subsets of Fin n with p elements are the cosets Σ_n / (Σ_p × Σ_q), and the shuffles
are the standard coset representatives. The action of a bijection τ : n ⟶ m carries the
summand of S to the summand of S.map τ, through the block bijections of shuffle S ≫ τ
(hom_app_comp_map_eq_map_comp_shuffleCofan_inj,
DayFunctor.η_app_comp_map_eq_tensorHom_comp_shuffleCofan_inj, blockImage_shuffle_comp).
Main definitions #
FiniteBijection.shuffle S: the shuffle of a subsetSofFin n.FiniteBijection.blockImage σ,FiniteBijection.blockLeft σ,FiniteBijection.blockRight σ: the shuffle factorization of a bijectionσ : p ⊗ q ⟶ n.FiniteBijection.shuffleFunctor n: the equivalence from the discrete category on the subsets ofFin ntoCostructuredArrow (tensor FiniteBijection) n.Functor.LeftExtension.shuffleCofan E n: the cofan of the shuffle summands of a left extension along the block sum, andDayFunctor.shuffleCofan F G n, its specialization to Day convolution.
Main statements #
FiniteBijection.blockLeft_tensorHom_blockRight_comp_shuffle: the shuffle factorization.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isColimitShuffleCofan: the levels of a pointwise left Kan extension along the block sum are the coproducts of the shuffle summands.DayFunctor.isColimitShuffleCofan: the wedge formula for Day convolution of functors out ofFiniteBijection.
References #
- M. Hovey, B. Shipley and J. Smith, Symmetric spectra, J. Amer. Math. Soc. 13 (2000), Section 2.1.
- S. Schwede, Symmetric spectra, book project, Chapter I.
Shuffles #
The shuffle of a subset S of Fin n: the bijection mk #S ⊗ mk #Sᶜ ⟶ n enumerating S
on the first block and Sᶜ on the second block, both in increasing order.
Instances For
The shuffle factorization #
The image of the first block under a bijection σ : p ⊗ q ⟶ n.
Instances For
A point lies outside the image of the first block exactly when it is the image of a point of the second block.
The first factor of the shuffle factorization of σ : p ⊗ q ⟶ n: the bijection from the first
block onto the enumeration of its image.
Instances For
The second factor of the shuffle factorization of σ : p ⊗ q ⟶ n: the bijection from the
second block onto the enumeration of the complement of the image of the first block.
Instances For
Shuffle factorization. Every bijection σ : p ⊗ q ⟶ n is a pair of block bijections
followed by the shuffle of the image of the first block.
Shuffle factorization. Every bijection σ : p ⊗ q ⟶ n is a pair of block bijections
followed by the shuffle of the image of the first block.
Precomposing with a pair of block bijections does not change the image of the first block.
Postcomposing with a bijection τ moves the image of the first block along τ.
The subset carried by the shuffle shuffle S ≫ τ is the image of S under τ.
The comma category of the block sum #
A morphism of the comma category of the block sum is determined by its source and target: the block bijections of a factorization through a bijection are unique.
The shuffle of a subset S of Fin n, as an object of the comma category of the block sum
over n.
Instances For
The functor from the discrete category on the subsets of Fin n to the comma category of the
block sum over n, sending a subset to its shuffle. It is an equivalence.
Instances For
The wedge formula for left Kan extensions along the block sum #
The cofan of the shuffle summands of a left extension E of H along the block sum: the
summand H(#S, #Sᶜ) of a subset S of Fin n maps to E(n) through the unit of E followed
by the action of the shuffle of S.
Instances For
The wedge formula. If E is a pointwise left Kan extension of H along the block sum at
n, then E(n) is the coproduct over the subsets S of Fin n of H(#S, #Sᶜ), with the
summand of S included through the shuffle of S.
Instances For
The unit of a left extension along the block sum, followed by the action of any bijection
σ : p ⊗ q ⟶ n, factors through the shuffle summand of blockImage σ, through the block
bijections of σ. For σ = shuffle S ≫ τ, this describes the action of τ on the summands.
The wedge formula for Day convolution #
The cofan of the shuffle summands of the Day convolution of F and G at n: the summand
F(#S) ⊗ G(#Sᶜ) of a subset S of Fin n maps to (F ⊗ G)(n) through the Day convolution unit
followed by the action of the shuffle of S.
Instances For
The wedge formula for Day convolution. For functors F and G out of the
finite-bijection groupoid, the level (F ⊗ G)(n) of their Day convolution is the coproduct over
the subsets S of Fin n of F(#S) ⊗ G(#Sᶜ), with the summand of S included through the Day
convolution unit followed by the action of the shuffle of S.
Instances For
The Day convolution unit followed by the action of a bijection σ : p ⊗ q ⟶ n factors through
the shuffle summand of blockImage σ, through the block bijections of σ. For
σ = shuffle S ≫ τ, this describes the action of τ on the summands.