Naturality of the symmetric-group action #
A morphism f : X ⟶ Y induces f ^ ⊗ n between the tensor powers,
and the permutation action of Envelope/SymPerm.lean is natural in
it: every braiding used there is a component of a natural
transformation, so the action of any group-algebra element commutes
with f ^ ⊗ n. The naturality lemmas follow the recursion that
defines the action — one lemma per auxiliary definition.
Two consequences are recorded. Tensor powers of monomorphisms are
monomorphisms (and dually for epimorphisms), because tensoring is
exact in a rigid category (TensorExact.lean); and Schur vanishing
passes to subobjects, quotients and isomorphs (the idempotent-level
form of Deligne's 1.19, Catégories tensorielles): a mono Y ⟶ X
intertwines the two actions, so if the block idempotent kills
X ^ ⊗ n it kills Y ^ ⊗ n as well.
Tensor powers of a morphism #
The tensor power of a morphism: f ^ ⊗ n acts as f on
every factor, by the same recursion that defines tensorPow.
Equations
Instances For
The empty power of a morphism is the identity of the unit.
The defining recursion of tensorPowMap.
Tensor powers of the identity are the identity.
Tensor powers are functorial in the morphism.
Mono and epi transport #
In a rigid category tensoring is exact (TensorExact.lean), so both
whiskerings preserve monomorphisms and epimorphisms, and hence so
does the tensor power of a morphism.
Tensor powers preserve monomorphisms in a rigid category:
each factor of f ⊗ₘ f's whiskering factorisation preserves
monomorphisms, because tensoring preserves limits.
Tensor powers preserve monomorphisms, from mono preservation of the tensor factors alone — the form consumed over an ind-completion, where tensoring is exact without rigidity.
Tensor powers preserve epimorphisms in a rigid category:
each factor of f ⊗ₘ f's whiskering factorisation preserves
epimorphisms, because tensoring preserves colimits.
Naturality of the action #
Each auxiliary morphism of Envelope/SymPerm.lean is built from
braidings and associators, which are components of natural
transformations, so each commutes with a tensor power of f. The
lemmas follow the definitions' recursions exactly.
Naturality of the top braiding: swapTop commutes with a
tensor power of f, by naturality of the associator and of the
braiding.
Naturality of the insertion cycle, by the recursion that
defines it: each bubbling step is a top braiding, natural by
swapTop_natural, whiskered by factors f passes through by
whisker_pass.
Naturality of the permutation action: the action of any
permutation commutes with a tensor power of f. The proof is the
recursion of permMor itself.
Naturality of the symmetric-group action: the action of any
group-algebra element commutes with a tensor power of f. Both
sides are ℂ-linear in the element, so the statement reduces to
basis permutations, where it is permMor_natural.
Stability of Schur vanishing #
The idempotent-level form of Deligne's 1.19 (Catégories tensorielles): Schur vanishing passes along monomorphisms, epimorphisms and isomorphisms, by cancelling the tensor power of the morphism against the naturality square.
Schur vanishing descends along monomorphisms (the
subobject half of Deligne's 1.19, at the idempotent level): if the
block idempotent of μ kills X ^ ⊗ μ.card and Y ⟶ X is a
monomorphism, it kills Y ^ ⊗ μ.card as well.
Schur vanishing descends along epimorphisms (the quotient half of Deligne's 1.19, at the idempotent level).
Schur vanishing is invariant under isomorphism. No rigidity
is needed: the tensor power of e.inv splits the tensor power of
e.hom, and the naturality square does the rest.