The kernel of a tensor power of an epimorphism

The exactness half of the mixed filtration for Deligne 1.19's extension argument (Catégories tensorielles): if ι : U ⟶ Z covers the kernel of an epimorphism π : Z ⟶ W, then the kernel of π ^ ⊗ m is covered by the images of the word maps of ι and 𝟙 Z with exactly one ι-slot (kernelSubobject_tensorPowMap_le).

The exactness hypothesis. The kernel condition is stated as hker : kernelSubobject π ≤ imageSubobject ι — only the covering half of exactness is consumed, so neither Mono ι nor ι ≫ π = 0 is assumed. For a genuinely exact pair, with Mono ι and hexact : imageSubobject ι = kernelSubobject π, apply the theorems at hker := hexact.ge.

Three layers:

• Word concatenation (pure monoidal coherence): appended words wordAppend concatenate word powers (wordPowConcatIso) and word maps (wordMap_append), mirroring wordMap_standard; letter counts add (popCount_wordAppend). At the level of images this is imageSubobject_wordMap_concat.
• The two-factor kernel (the abelian heart): in a rigid abelian monoidal category the kernel of p₁ ⊗ₘ p₂, for p₁ epi, is the join of the images of the two one-slot kernel insertions (kernelSubobject_tensorHom_le, an equality by kernelSubobject_tensorHom). The chase runs through the factorisation p₁ ⊗ₘ p₂ = (p₁ ▷ Z₂) ≫ (W₁ ◁ p₂), the identification of whiskered kernels (kernelSubobject_whiskerRight_le), and a pullback of the covering epimorphism (kernelSubobject_comp_le_of_cover).
• The iterated kernel: induction along tensorPowMap π (m + 1) = tensorPowMap π m ⊗ₘ π, transporting the inductive cover through the tensor structure. The cover is a single morphism from a biproduct of one-slot word powers (oneSlotCover), and the final statement is phrased as a Finset.sup of image subobjects: the ambient category is not assumed well-powered, so the subobject lattice carries finite joins but no indexed supremum.

Appended words

wordAppend is Fin.append: the first word occupies the low block. This matches the orientation of tensorPowConcat and standardWord, whose first factor is also the low block (wordAppend_const_true_false).

def RS.wordAppend {a b : ℕ} (wa : Fin a → Bool) (wb : Fin b → Bool) : Fin (a + b) → Bool

The appended word: wa on the low block, wb on the high block.

Equations

• RS.wordAppend wa wb = Fin.append wa wb

theorem RS.wordAppend_zero {a : ℕ} (wa : Fin a → Bool) (wb : Fin 0 → Bool) : wordAppend wa wb = wa

Appending the empty word is the identity.

theorem RS.wordAppend_castSucc {a b : ℕ} (wa : Fin a → Bool) (wb : Fin (b + 1) → Bool) : wordAppend wa wb ∘ Fin.castSucc = wordAppend wa (wb ∘ Fin.castSucc)

Restricting an appended word restricts the second word.

theorem RS.wordAppend_last {a b : ℕ} (wa : Fin a → Bool) (wb : Fin (b + 1) → Bool) : wordAppend wa wb (Fin.last (a + b)) = wb (Fin.last b)

The last letter of an appended word is the second word's last letter.

theorem RS.popCount_wordAppend {a b : ℕ} (wa : Fin a → Bool) (wb : Fin b → Bool) : popCount (wordAppend wa wb) = popCount wa + popCount wb

Letter counts add across an appended word.

theorem RS.wordAppend_const_true_false (p q : ℕ) : (wordAppend (fun (x : Fin p) => true) fun (x : Fin q) => false) = standardWord p q

The sorted word is the all-true word appended to the all-false word: wordAppend's low block matches standardWord's.

Word powers of appended words

theorem RS.wordPow_append_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (U V : A) {a : ℕ} (wa : Fin a → Bool) (wb : Fin 0 → Bool) : wordPow U V (a + 0) (wordAppend wa wb) = wordPow U V a wa

Appending the empty word does not change the word power.

theorem RS.wordPow_append_succ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (U V : A) {a b : ℕ} (wa : Fin a → Bool) (wb : Fin (b + 1) → Bool) : wordPow U V (a + (b + 1)) (wordAppend wa wb) = CategoryTheory.MonoidalCategoryStruct.tensorObj (wordPow U V (a + b) (wordAppend wa (wb ∘ Fin.castSucc))) (bif wb (Fin.last b) then U else V)

One more letter of the second word tensors the selected object.

noncomputable def RS.wordPowConcatIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (U V : A) {a : ℕ} (wa : Fin a → Bool) (b : ℕ) (wb : Fin b → Bool) : wordPow U V (a + b) (wordAppend wa wb) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (wordPow U V a wa) (wordPow U V b wb)

The word powers of an appended word concatenate: the word power of wordAppend wa wb is the tensor of the two word powers, by the recursion of the second word. Built stage by stage, mirror to standardMixedIso, so that consumers can compose with it.

Equations

• One or more equations did not get rendered due to their size.
• RS.wordPowConcatIso U V wa 0 wb = CategoryTheory.eqToIso ⋯ ≪≫ (CategoryTheory.MonoidalCategoryStruct.rightUnitor (RS.wordPow U V a wa)).symm

The concatenation square

The word map of an appended word is the tensor of the two word maps, followed by the concatenation of the target powers, under wordPowConcatIso. The gluing helpers replicate the private steps of wordMap_standard at general objects, applied by exact, so that no tensor-power arity enters the rewriting.

theorem RS.wordMap_append {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) {a : ℕ} (wa : Fin a → Bool) (b : ℕ) (wb : Fin b → Bool) : CategoryTheory.CategoryStruct.comp (wordPowConcatIso U V wa b wb).inv (wordMap f g (a + b) (wordAppend wa wb)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (wordMap f g a wa) (wordMap f g b wb)) (tensorPowConcat Z a b).hom

The concatenation square: the word map of an appended word is the tensor of the two word maps followed by the concatenation of the pure target powers, under wordPowConcatIso at the source.

Extended and all-false words

The one-slot insertions of the filtration are words extended by Fin.snoc, and the base insertion is an all-false word with one true slot on top. The lemmas mirror the all-true cases of WordMap.lean.

theorem RS.popCount_snoc {n : ℕ} (w : Fin n → Bool) (y : Bool) : popCount (Fin.snoc w y) = popCount w + bif y then 1 else 0

The letter count of an extended word.

theorem RS.popCount_const_false (n : ℕ) : (popCount fun (x : Fin n) => false) = 0

The all-false word has no true letters.

theorem RS.wordPow_snoc_false {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X Y : A) (n : ℕ) (w : Fin n → Bool) : wordPow X Y (n + 1) (Fin.snoc w false) = CategoryTheory.MonoidalCategoryStruct.tensorObj (wordPow X Y n w) Y

The word power of a false-extended word tensors a Y.

theorem RS.wordPow_snoc_true {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X Y : A) (n : ℕ) (w : Fin n → Bool) : wordPow X Y (n + 1) (Fin.snoc w true) = CategoryTheory.MonoidalCategoryStruct.tensorObj (wordPow X Y n w) X

The word power of a true-extended word tensors an X.

theorem RS.wordMap_snoc_false {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin n → Bool) : wordMap f g (n + 1) (Fin.snoc w false) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.MonoidalCategoryStruct.tensorHom (wordMap f g n w) g)

The word map of a false-extended word tensors a g.

theorem RS.wordMap_snoc_true {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) (w : Fin n → Bool) : wordMap f g (n + 1) (Fin.snoc w true) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.MonoidalCategoryStruct.tensorHom (wordMap f g n w) f)

The word map of a true-extended word tensors an f.

theorem RS.wordPow_const_false {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X Y : A) (n : ℕ) : (wordPow X Y n fun (x : Fin n) => false) = tensorPow A Y n

An all-false word power is a pure power of Y.

theorem RS.wordMap_const_false {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} (f : U ⟶ Z) (g : V ⟶ Z) (n : ℕ) : (wordMap f g n fun (x : Fin n) => false) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (tensorPowMap g n)

On an all-false word the word map is the pure power of g.

Concatenation at the level of images

theorem RS.imageSubobject_wordMap_concat {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {U V Z : A} [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] (f : U ⟶ Z) (g : V ⟶ Z) {a b : ℕ} (wa : Fin a → Bool) (wb : Fin b → Bool) : CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (wordMap f g a wa) (wordMap f g b wb)) (tensorPowConcat Z a b).hom) = CategoryTheory.Limits.imageSubobject (wordMap f g (a + b) (wordAppend wa wb))

Concatenation of word-map images: the tensor of two word maps followed by the target concatenation has the same image as the word map of the appended word — the concatenation square wordMap_append up to the isomorphism wordPowConcatIso of the sources.

The subobject toolkit

Factoring through subobjects in an abelian category: epi descent (factors_of_epi_comp, the monomorphism half of the kernel–cokernel duality), the kernel and image conversions, and the composite-kernel chase kernelSubobject_comp_le_of_cover — the kernel of u ≫ v is covered by the kernel of u together with any b whose image under u covers the kernel of v. This is the extension 0 ⟶ ker u ⟶ ker (u ≫ v) ⟶ ker v of the mixed filtration, phrased through a pullback of the covering epimorphism.

theorem RS.factors_of_epi_comp {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {P K B : A} (S : CategoryTheory.Subobject B) (e : P ⟶ K) [CategoryTheory.Epi e] (k : K ⟶ B) (h : S.Factors (CategoryTheory.CategoryStruct.comp e k)) : S.Factors k

Epi descent for factorisations: a morphism factors through a subobject as soon as its composite with an epimorphism does. The subobject's arrow is the kernel of its cokernel, so the factorisation is Abelian.monoLift.

theorem RS.factors_kernel_ι_of_le {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X Y : A} {p : X ⟶ Y} {S : CategoryTheory.Subobject X} (h : CategoryTheory.Limits.kernelSubobject p ≤ S) : S.Factors (CategoryTheory.Limits.kernel.ι p)

A subobject containing a kernel factors the kernel's arrow.

theorem RS.kernelSubobject_le_of_factors {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X Y : A} {p : X ⟶ Y} {S : CategoryTheory.Subobject X} (h : S.Factors (CategoryTheory.Limits.kernel.ι p)) : CategoryTheory.Limits.kernelSubobject p ≤ S

A subobject factoring a kernel's arrow contains the kernel.

theorem RS.imageSubobject_le_of_factors {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X B : A} {f : X ⟶ B} {S : CategoryTheory.Subobject B} (h : S.Factors f) : CategoryTheory.Limits.imageSubobject f ≤ S

A subobject factoring a morphism contains its image.

theorem RS.factors_self_imageSubobject {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X B : A} (f : X ⟶ B) : (CategoryTheory.Limits.imageSubobject f).Factors f

The image of a morphism factors it.

theorem RS.kernelSubobject_comp_le_of_cover {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {X Y T B : A} (u : X ⟶ Y) (v : Y ⟶ T) (b : B ⟶ X) (hv : CategoryTheory.Limits.kernelSubobject v ≤ CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp b u)) : CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp u v) ≤ CategoryTheory.Limits.kernelSubobject u ⊔ CategoryTheory.Limits.imageSubobject b

The composite-kernel chase: if the image of b ≫ u covers the kernel of v, then the kernel of u ≫ v is covered by the kernel of u together with the image of b. The kernel arrow of u ≫ v, pushed into Y, factors through the cover; pulling the covering epimorphism back splits the kernel arrow, up to an epimorphism, into a summand through ker u and a summand through b.

Whiskered epimorphisms and kernels

Whiskering preserves epimorphisms and kernels because tensoring is exact in a rigid category (TensorExact.lean).

theorem RS.epi_whiskerRight_of_epi {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] {X Y : A} (p : X ⟶ Y) [CategoryTheory.Epi p] (W : A) : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerRight p W)

Right whiskering preserves epimorphisms.

theorem RS.epi_whiskerLeft_of_epi {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] (W : A) {X Y : A} (p : X ⟶ Y) [CategoryTheory.Epi p] : CategoryTheory.Epi (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W p)

Left whiskering preserves epimorphisms.

theorem RS.factors_kernel_ι_whiskerRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] {X Y : A} (p : X ⟶ Y) {W : A} {S : CategoryTheory.Subobject (CategoryTheory.MonoidalCategoryStruct.tensorObj X W)} (h : S.Factors (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.kernel.ι p) W)) : S.Factors (CategoryTheory.Limits.kernel.ι (CategoryTheory.MonoidalCategoryStruct.whiskerRight p W))

A subobject factoring the whiskered kernel arrow factors the kernel arrow of the right-whiskered morphism.

theorem RS.factors_kernel_ι_whiskerLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] {W X Y : A} (p : X ⟶ Y) {S : CategoryTheory.Subobject (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)} (h : S.Factors (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.Limits.kernel.ι p))) : S.Factors (CategoryTheory.Limits.kernel.ι (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W p))

A subobject factoring the whiskered kernel arrow factors the kernel arrow of the left-whiskered morphism.

theorem RS.kernelSubobject_whiskerRight_le {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] {X Y : A} (p : X ⟶ Y) (W : A) : CategoryTheory.Limits.kernelSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerRight p W) ≤ CategoryTheory.Limits.imageSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.kernel.ι p) W)

The kernel of a right-whiskered morphism is covered by the image of the whiskered kernel arrow.

theorem RS.factors_imageSubobject_whiskerRight {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.RigidCategory A] {X B C' : A} {f : X ⟶ B} {c : C' ⟶ B} (h : (CategoryTheory.Limits.imageSubobject c).Factors f) (W : A) : (CategoryTheory.Limits.imageSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerRight c W)).Factors (CategoryTheory.MonoidalCategoryStruct.whiskerRight f W)

Factoring through an image is stable under right whiskering.

theorem RS.factors_imageSubobject_whiskerLeft {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.RigidCategory A] {X B C' : A} {f : X ⟶ B} {c : C' ⟶ B} (h : (CategoryTheory.Limits.imageSubobject c).Factors f) (W : A) : (CategoryTheory.Limits.imageSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W c)).Factors (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W f)

Factoring through an image is stable under left whiskering.

The two-factor kernel

theorem RS.kernelSubobject_tensorHom_le {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] {Z₁ W₁ Z₂ W₂ : A} (p₁ : Z₁ ⟶ W₁) (p₂ : Z₂ ⟶ W₂) [CategoryTheory.Epi p₁] : CategoryTheory.Limits.kernelSubobject (CategoryTheory.MonoidalCategoryStruct.tensorHom p₁ p₂) ≤ CategoryTheory.Limits.imageSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.kernel.ι p₁) Z₂) ⊔ CategoryTheory.Limits.imageSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z₁ (CategoryTheory.Limits.kernel.ι p₂))

The kernel of a tensor product of an epimorphism and a morphism is covered by the two one-slot kernel insertions: the whiskered kernels of the factors. The route is the factorisation p₁ ⊗ₘ p₂ = (p₁ ▷ Z₂) ≫ (W₁ ◁ p₂): the kernel of the second factor is covered by the image of Z₁ ◁ kernel.ι p₂ under the first — the whisker exchange against the epimorphism p₁ ▷ kernel p₂ — and the composite-kernel chase concludes.

theorem RS.sup_le_kernelSubobject_tensorHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] {Z₁ W₁ Z₂ W₂ : A} (p₁ : Z₁ ⟶ W₁) (p₂ : Z₂ ⟶ W₂) : CategoryTheory.Limits.imageSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.kernel.ι p₁) Z₂) ⊔ CategoryTheory.Limits.imageSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z₁ (CategoryTheory.Limits.kernel.ι p₂)) ≤ CategoryTheory.Limits.kernelSubobject (CategoryTheory.MonoidalCategoryStruct.tensorHom p₁ p₂)

The two one-slot kernel insertions land in the kernel of the tensor product; no epimorphism hypothesis is needed.

theorem RS.kernelSubobject_tensorHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] {Z₁ W₁ Z₂ W₂ : A} (p₁ : Z₁ ⟶ W₁) (p₂ : Z₂ ⟶ W₂) [CategoryTheory.Epi p₁] : CategoryTheory.Limits.kernelSubobject (CategoryTheory.MonoidalCategoryStruct.tensorHom p₁ p₂) = CategoryTheory.Limits.imageSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.kernel.ι p₁) Z₂) ⊔ CategoryTheory.Limits.imageSubobject (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z₁ (CategoryTheory.Limits.kernel.ι p₂))

The kernel of a tensor product of an epimorphism and a morphism, exactly: it is the join of the images of the two one-slot kernel insertions.

The iterated kernel

The kernel of π ^ ⊗ m is covered by the one-slot insertions: the word maps of ι and 𝟙 Z at words with exactly one true letter. The induction along tensorPowMap π (m + 1) = tensorPowMap π m ⊗ₘ π transports the inductive cover through the tensor structure, so the cover is kept as a single morphism out of the biproduct of the one-slot word powers (oneSlotCover); the Finset.sup phrasing is recovered at the end.

noncomputable def RS.oneSlotCover {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] {U Z : A} (ι : U ⟶ Z) (m : ℕ) : (⨁ fun (w : { w : Fin m → Bool // popCount w = 1 }) => wordPow U Z m ↑w) ⟶ tensorPow A Z m

The one-slot cover: the fold of all word maps of ι and 𝟙 Z with exactly one ι-slot, out of the biproduct of their word powers.

Equations

• RS.oneSlotCover ι m = CategoryTheory.Limits.biproduct.desc fun (w : { w : Fin m → Bool // RS.popCount w = 1 }) => RS.wordMap ι (CategoryTheory.CategoryStruct.id Z) m ↑w

theorem RS.kernelSubobject_tensorPowMap_le_cover {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] {U Z W : A} (ι : U ⟶ Z) (π : Z ⟶ W) [CategoryTheory.Epi π] (hker : CategoryTheory.Limits.kernelSubobject π ≤ CategoryTheory.Limits.imageSubobject ι) (m : ℕ) : CategoryTheory.Limits.kernelSubobject (tensorPowMap π m) ≤ CategoryTheory.Limits.imageSubobject (oneSlotCover ι m)

The kernel of a tensor power of an epimorphism, cover form: if ι covers the kernel of the epimorphism π, then the kernel of π ^ ⊗ m is covered by the image of the one-slot cover.

theorem RS.kernelSubobject_tensorPowMap_le {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] {U Z W : A} (ι : U ⟶ Z) (π : Z ⟶ W) [CategoryTheory.Epi π] (hker : CategoryTheory.Limits.kernelSubobject π ≤ CategoryTheory.Limits.imageSubobject ι) (m : ℕ) : CategoryTheory.Limits.kernelSubobject (tensorPowMap π m) ≤ {w : Fin m → Bool | popCount w = 1}.sup fun (w : Fin m → Bool) => CategoryTheory.Limits.imageSubobject (wordMap ι (CategoryTheory.CategoryStruct.id Z) m w)

The kernel of a tensor power of an epimorphism: if ι covers the kernel of the epimorphism π : Z ⟶ W, the kernel of π ^ ⊗ m is covered by the join of the images of the word maps of ι and 𝟙 Z over the words with exactly one ι-slot. The join is a Finset.sup: without well-poweredness the subobject lattice carries finite joins, and the index is the finite set of one-slot words.