Transport of tensor powers and the permutation action along

C ⥤ Ind C

The embedding RS.indOf : C ⥤ Ind C is monoidal up to isomorphism (RS.indOfTensorIso, RS.Classical.Deligne.IndTensorExact). This file upgrades that comparison to the full coherent package needed to transport the symmetric-group action on tensor powers (RS.Novel.Envelope.SymPerm) across the embedding:

• RS.dayCoyonedaIso_hom_braiding and RS.dayCoyonedaIso_hom_associator — the co-Yoneda identifications of RS.dayCoyonedaIso intertwine the Day braiding and the Day associator with the braiding and associator of the base, with Yoneda forms RS.dayYonedaIso_hom_braiding and RS.dayYonedaIso_hom_associator;
• RS.indOfUnitIso — the unit of Ind C is the embedded unit;
• RS.indOfTensorIso_hom_braiding and RS.indOfTensorIso_hom_associator — the embedding-tensor comparison is compatible with braiding and associator: indOf with indOfTensorIso is a braided monoidal functor up to isomorphism;
• RS.indOfPowIso — the tensor powers of an embedded object are the embedded tensor powers, with recursion lemmas RS.indOfPowIso_zero/RS.indOfPowIso_succ;
• RS.indOfPowIso_swapTop/RS.indOfPowIso_insertTop/ RS.indOfPowIso_permMor — the permutation action on the tensor powers of indOf.obj X is conjugate, under indOfPowIso, to the embedded permutation action;
• RS.permMor_indOf_eq_zero_iff and RS.schurKilled_iff_indOf_map_permAlg_eq_zero — vanishing of the action transports faithfully across the embedding.

The Mathlib pin has Preadditive (Ind C) (for C preadditive with finite colimits) but no Linear ℂ (Ind C) instance, so Ind C carries no permAlg, so Schur vanishing cannot be stated on Ind C; the lemmas above are the permMor-level substrate, which is what the group-algebra layer would rest on were Linear ℂ (Ind C) available.

The single-element method used throughout the Day-level proofs: a morphism out of a (possibly iterated) Day tensor of corepresentables is classified, through the Kan-extension universal property and the Yoneda lemma, by one element — its value on the canonical element RS.dayCoyonedaUnitElt assembled from identities. All coherence comparisons are decided by evaluating both sides there.

@[reducible]

noncomputable def RS.dayConvPlain {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F G : CategoryTheory.Functor D (Type v)) : CategoryTheory.MonoidalCategory.DayConvolution F G

The Day-convolution structure of a plain presheaf pair, read through the synonym: makes the DayConvolution API available on underlying functors of the Day category.

Equations

• RS.dayConvPlain F G = RS.dayConv { functor := F } { functor := G }

noncomputable def RS.dayCoyonedaUnitElt {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b : D) : (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) }).functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj a b)

The canonical element of the Day tensor of two corepresentables: the Kan-extension unit evaluated on the pair of identities.

Equations

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

noncomputable def RS.dayCoyonedaUnitElt₂ {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b c : D) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) }) { functor := CategoryTheory.coyoneda.obj (Opposite.op c) }).functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) c)

The canonical element of a left-nested triple Day tensor of corepresentables.

Equations

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

noncomputable def RS.dayCoyonedaUnitElt₂' {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b c : D) : (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op b) } { functor := CategoryTheory.coyoneda.obj (Opposite.op c) })).functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj a (CategoryTheory.MonoidalCategoryStruct.tensorObj b c))

The canonical element of a right-nested triple Day tensor of corepresentables.

Equations

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

noncomputable def RS.dayCoyonedaCorepresentableBy₂ {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b c : D) : (dayEvaluation (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) c)).CorepresentableBy (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) }) { functor := CategoryTheory.coyoneda.obj (Opposite.op c) })

The left-nested triple Day tensor of corepresentables corepresents evaluation at (a ⊗ b) ⊗ c: iterate the Kan-extension universal property twice and read off the Yoneda lemma on the external product of three corepresentables, which is definitionally the corepresentable of the triple product category.

Equations

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

theorem RS.dayEvaluation_map_apply {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (d : D) {F K : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)} (g : F ⟶ K) (x : (dayEvaluation d).obj F) : (CategoryTheory.ConcreteCategory.hom ((dayEvaluation d).map g)) x = (CategoryTheory.ConcreteCategory.hom (g.natTrans.app d)) x

Evaluation of RS.dayEvaluation on a morphism of the Day category.

theorem RS.dayCoyonedaCorepresentableBy_homEquiv_apply {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b : D) {K : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) } ⟶ K) : (dayCoyonedaCorepresentableBy a b).homEquiv f = (CategoryTheory.ConcreteCategory.hom (f.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj a b))) (dayCoyonedaUnitElt a b)

The corepresentability of a Day tensor of two corepresentables classifies a morphism by its value on the canonical element.

theorem RS.dayCoyonedaCorepresentableBy₂_homEquiv_apply {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b c : D) {K : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) }) { functor := CategoryTheory.coyoneda.obj (Opposite.op c) } ⟶ K) : (dayCoyonedaCorepresentableBy₂ a b c).homEquiv f = (CategoryTheory.ConcreteCategory.hom (f.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) c))) (dayCoyonedaUnitElt₂ a b c)

The corepresentability of a left-nested triple Day tensor of corepresentables classifies a morphism by its value on the canonical element.

theorem RS.dayCoyonedaCorepresentableBy_homEquiv_iso {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (p q : D) : (dayCoyonedaCorepresentableBy p q).homEquiv (dayCoyonedaIso p q).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj p q)

The classification of RS.dayCoyonedaIso under the corepresentability of the Day tensor of two corepresentables: its value is the identity of p ⊗ q.

theorem RS.dayCoyonedaIso_hom_app_unitElt {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (p q : D) : (CategoryTheory.ConcreteCategory.hom ((dayCoyonedaIso p q).hom.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj p q))) (dayCoyonedaUnitElt p q) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj p q)

RS.dayCoyonedaIso sends the canonical element to the identity.

theorem RS.whiskerRight_dayCoyonedaIso_app_unitElt {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b c : D) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.whiskerRight (dayCoyonedaIso a b).hom { functor := CategoryTheory.coyoneda.obj (Opposite.op c) }).natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) c))) (dayCoyonedaUnitElt₂ a b c) = dayCoyonedaUnitElt (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) c

Right-whiskering RS.dayCoyonedaIso sends the left-nested canonical element to the canonical element at (a ⊗ b, c).

theorem RS.whiskerLeft_dayCoyonedaIso_app_unitElt {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b c : D) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.whiskerLeft { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } (dayCoyonedaIso b c).hom).natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj a (CategoryTheory.MonoidalCategoryStruct.tensorObj b c)))) (dayCoyonedaUnitElt₂' a b c) = dayCoyonedaUnitElt a (CategoryTheory.MonoidalCategoryStruct.tensorObj b c)

Left-whiskering RS.dayCoyonedaIso sends the right-nested canonical element to the canonical element at (a, b ⊗ c).

theorem RS.dayAssociator_hom_app_unitElt {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b c : D) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.associator { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) } { functor := CategoryTheory.coyoneda.obj (Opposite.op c) }).hom.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) c))) (dayCoyonedaUnitElt₂ a b c) = (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } (CategoryTheory.MonoidalCategoryStruct.tensorObj { functor := CategoryTheory.coyoneda.obj (Opposite.op b) } { functor := CategoryTheory.coyoneda.obj (Opposite.op c) })).functor.map (CategoryTheory.MonoidalCategoryStruct.associator a b c).inv)) (dayCoyonedaUnitElt₂' a b c)

The Day associator carries the left-nested canonical element to the image of the right-nested one under the base associator.

theorem RS.dayCoyonedaIso_hom_associator {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a b c : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (dayCoyonedaIso a b).hom { functor := CategoryTheory.coyoneda.obj (Opposite.op c) }) (CategoryTheory.CategoryStruct.comp (dayCoyonedaIso (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) c).hom { natTrans := CategoryTheory.coyoneda.map (CategoryTheory.MonoidalCategoryStruct.associator a b c).inv.op }) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) } { functor := CategoryTheory.coyoneda.obj (Opposite.op c) }).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } (dayCoyonedaIso b c).hom) (dayCoyonedaIso a (CategoryTheory.MonoidalCategoryStruct.tensorObj b c)).hom)

Day convolution of corepresentables intertwines the associator: under the co-Yoneda identifications, the two reassociation routes of a triple Day tensor of corepresentables differ by precomposition with the associator of the base.

theorem RS.dayCoyonedaIso_hom_braiding {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (a b : D) : CategoryTheory.CategoryStruct.comp (β_ { functor := CategoryTheory.coyoneda.obj (Opposite.op a) } { functor := CategoryTheory.coyoneda.obj (Opposite.op b) }).hom (dayCoyonedaIso b a).hom = CategoryTheory.CategoryStruct.comp (dayCoyonedaIso a b).hom { natTrans := CategoryTheory.coyoneda.map (β_ b a).hom.op }

Day convolution of corepresentables intertwines the braiding: under the co-Yoneda identifications, the braiding of the Day tensor of two corepresentables is precomposition with the braiding of the base.

theorem RS.dayMkIso_hom_symm_hom {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] {A B : CategoryTheory.Functor Dᵒᵖ (Type v)} (e : A ≅ B) : CategoryTheory.CategoryStruct.comp (dayMkIso e).hom (dayMkIso e.symm).hom = CategoryTheory.CategoryStruct.id { functor := A }

The forward and reversed transports along RS.dayMkIso compose to the identity.

theorem RS.comp_dayMkIso_hom_symm_hom {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] {A B : CategoryTheory.Functor Dᵒᵖ (Type v)} (e : A ≅ B) {X : CategoryTheory.MonoidalCategory.DayFunctor Dᵒᵖ (Type v)} (f : X ⟶ { functor := A }) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (dayMkIso e).hom (dayMkIso e.symm).hom) = f

Cancellation form of RS.dayMkIso_hom_symm_hom, stated against a leading morphism so that no identity is left behind.

theorem RS.coyoneda_map_op_op_comp_objOpOp_hom {C : Type v} [CategoryTheory.SmallCategory C] {z z' : C} (u : z ⟶ z') : CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map u.op.op) (CategoryTheory.Coyoneda.objOpOp z').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Coyoneda.objOpOp z).hom (CategoryTheory.yoneda.map u)

Naturality of Coyoneda.objOpOp, forward form, at a general double-opposite morphism.

theorem RS.dayYonedaIso_hom_braiding {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (x y : C) : CategoryTheory.CategoryStruct.comp (β_ { functor := CategoryTheory.yoneda.obj x } { functor := CategoryTheory.yoneda.obj y }).hom (dayYonedaIso y x).hom = CategoryTheory.CategoryStruct.comp (dayYonedaIso x y).hom { natTrans := CategoryTheory.yoneda.map (β_ x y).hom }

The Day tensor of representables intertwines the braiding: the Yoneda form of RS.dayCoyonedaIso_hom_braiding.

theorem RS.dayYonedaIso_hom_associator {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (dayYonedaIso x y).hom { functor := CategoryTheory.yoneda.obj z }) (CategoryTheory.CategoryStruct.comp (dayYonedaIso (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z).hom { natTrans := CategoryTheory.yoneda.map (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom }) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator { functor := CategoryTheory.yoneda.obj x } { functor := CategoryTheory.yoneda.obj y } { functor := CategoryTheory.yoneda.obj z }).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft { functor := CategoryTheory.yoneda.obj x } (dayYonedaIso y z).hom) (dayYonedaIso x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)).hom)

The Day tensor of representables intertwines the associator: the Yoneda form of RS.dayCoyonedaIso_hom_associator.

theorem RS.indToDay_map_indOfTensorIso_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y : C) : indToDay.map (indOfTensorIso x y).hom = (indToDayTensorIso x y).hom

The embedding into the Day presheaf category carries the embedding-tensor comparison to the Day-level comparison.

@[instance_reducible]

noncomputable instance RS.instBraidedIndFullSubcategoryDayFunctorOppositeTypeIsIndDayFunctorIndDayEquivalence {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (indDayEquivalence C).functor.Braided

The indization equivalence's forward functor is braided: the braiding of Ind C is transported across it.

Equations

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

@[instance_reducible]

noncomputable instance RS.instBraidedIndDayFunctorOppositeTypeIndToDay {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : indToDay.Braided

The embedding into the Day presheaf category is braided.

Equations

• RS.instBraidedIndDayFunctorOppositeTypeIndToDay = { toMonoidal := RS.instMonoidalIndDayFunctorOppositeTypeIndToDay, braided := ⋯ }

theorem RS.indOfTensorIso_hom_braiding {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (x y : C) : CategoryTheory.CategoryStruct.comp (β_ (indOf.obj x) (indOf.obj y)).hom (indOfTensorIso y x).hom = CategoryTheory.CategoryStruct.comp (indOfTensorIso x y).hom (indOf.map (β_ x y).hom)

The embedding-tensor comparison intertwines the braiding: indOf with indOfTensorIso is a braided functor up to isomorphism.

theorem RS.indOfTensorIso_hom_associator {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x y z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (indOfTensorIso x y).hom (indOf.obj z)) (CategoryTheory.CategoryStruct.comp (indOfTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z).hom (indOf.map (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (indOf.obj x) (indOf.obj y) (indOf.obj z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (indOf.obj x) (indOfTensorIso y z).hom) (indOfTensorIso x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)).hom)

The embedding-tensor comparison intertwines the associator: the associativity axiom of the monoidal-functor-up-to-isomorphism structure of indOf.

def RS.indOfPowIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) : tensorPow (CategoryTheory.Ind C) (indOf.obj X) n ≅ indOf.obj (tensorPow C X n)

The tensor powers of an embedded object are the embedded tensor powers: n = 0 is RS.indOfUnitIso, and each successor stage tensors the previous one with indOf.obj X and applies the embedding-tensor comparison.

Equations

• RS.indOfPowIso X 0 = RS.indOfUnitIso
• RS.indOfPowIso X n.succ = CategoryTheory.MonoidalCategory.whiskerRightIso (RS.indOfPowIso X n) (RS.indOf.obj X) ≪≫ RS.indOfTensorIso (RS.tensorPow C X n) X

@[simp]

theorem RS.indOfPowIso_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : C) : indOfPowIso X 0 = indOfUnitIso

The base case of the power comparison.

theorem RS.indOfPowIso_succ {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : C) (n : ℕ) : indOfPowIso X (n + 1) = CategoryTheory.MonoidalCategory.whiskerRightIso (indOfPowIso X n) (indOf.obj X) ≪≫ indOfTensorIso (tensorPow C X n) X

The defining recursion of the power comparison.

theorem RS.indOfTensorIso_swap_conj {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (a z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (indOf.obj a) (indOf.obj z) (indOf.obj z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (indOf.obj a) (β_ (indOf.obj z) (indOf.obj z)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (indOf.obj a) (indOf.obj z) (indOf.obj z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (indOfTensorIso a z).hom (indOf.obj z)) (indOfTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorObj a z) z).hom))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (indOfTensorIso a z).hom (indOf.obj z)) (CategoryTheory.CategoryStruct.comp (indOfTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorObj a z) z).hom (indOf.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator a z z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft a (β_ z z).hom) (CategoryTheory.MonoidalCategoryStruct.associator a z z).inv))))

The embedding-tensor comparison conjugates the braiding block of swapTop to its embedded form.

theorem RS.indOfPowIso_swapTop {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (X : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp (swapTop (indOf.obj X) n) (indOfPowIso X (n + 2)).hom = CategoryTheory.CategoryStruct.comp (indOfPowIso X (n + 2)).hom (indOf.map (swapTop X n))

Transport of the top braiding: swapTop on the powers of an embedded object is conjugate to the embedded swapTop.

theorem RS.indOfPowIso_whiskerRight {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : C) {m : ℕ} {f : tensorPow (CategoryTheory.Ind C) (indOf.obj X) m ⟶ tensorPow (CategoryTheory.Ind C) (indOf.obj X) m} {u : tensorPow C X m ⟶ tensorPow C X m} (h : CategoryTheory.CategoryStruct.comp f (indOfPowIso X m).hom = CategoryTheory.CategoryStruct.comp (indOfPowIso X m).hom (indOf.map u)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (indOf.obj X)) (indOfPowIso X (m + 1)).hom = CategoryTheory.CategoryStruct.comp (indOfPowIso X (m + 1)).hom (indOf.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight u X))

Whiskering by one more embedded factor preserves the transport relation.

theorem RS.indOfPowIso_insertTop {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (X : C) (n k : ℕ) : CategoryTheory.CategoryStruct.comp (insertTop (indOf.obj X) n k) (indOfPowIso X (n + 1)).hom = CategoryTheory.CategoryStruct.comp (indOfPowIso X (n + 1)).hom (indOf.map (insertTop X n k))

Transport of the insertion cycle: insertTop on the powers of an embedded object is conjugate to the embedded insertTop.

theorem RS.indOfPowIso_permMor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (X : C) (n : ℕ) (σ : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (permMor (indOf.obj X) n σ) (indOfPowIso X n).hom = CategoryTheory.CategoryStruct.comp (indOfPowIso X n).hom (indOf.map (permMor X n σ))

Transport of the permutation action along the embedding C ⥤ Ind C: the action of a permutation on the tensor powers of an embedded object is conjugate, under RS.indOfPowIso, to the embedded action.

theorem RS.permMor_indOf_conj {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (X : C) (n : ℕ) (σ : Equiv.Perm (Fin n)) : permMor (indOf.obj X) n σ = CategoryTheory.CategoryStruct.comp (indOfPowIso X n).hom (CategoryTheory.CategoryStruct.comp (indOf.map (permMor X n σ)) (indOfPowIso X n).inv)

Conjugation form of RS.indOfPowIso_permMor.

theorem RS.indOf_map_eq_zero_iff {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] {P Q : C} (f : P ⟶ Q) : indOf.map f = 0 ↔ f = 0

The faithfulness bridge: the embedding C ⥤ Ind C reflects and preserves vanishing of morphisms.

theorem RS.permMor_indOf_eq_zero_iff_map {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.SymmetricCategory C] (X : C) (n : ℕ) (σ : Equiv.Perm (Fin n)) : permMor (indOf.obj X) n σ = 0 ↔ indOf.map (permMor X n σ) = 0

Vanishing of the permutation action on an embedded object is vanishing of the embedded action.

theorem RS.permMor_indOf_eq_zero_iff {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.SymmetricCategory C] (X : C) (n : ℕ) (σ : Equiv.Perm (Fin n)) : permMor (indOf.obj X) n σ = 0 ↔ permMor X n σ = 0

Vanishing of the permutation action transports faithfully along the embedding C ⥤ Ind C. This is the permMor-level form of Schur-vanishing transport: the group-algebra form waits on a Linear ℂ (Ind C) instance, which the Mathlib pin does not provide.

theorem RS.schurKilled_iff_indOf_map_permAlg_eq_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.Limits.HasFiniteColimits C] (P : SchurPackage) (X : C) (μ : YoungDiagram) : SchurKilled P X μ ↔ indOf.map ((permAlg X μ.card) (P.e μ)) = 0

Schur vanishing, read through the embedding: the shape μ kills X precisely when the embedded action of its block idempotent vanishes. Together with RS.permMor_indOf_eq_zero_iff this is the substrate for transporting RS.SchurKilled to Ind C; phrasing the Ind C side through permAlg needs Linear ℂ (Ind C), which is a mainline decision.