Discrete color category

noncomputable def IndexNotation.OverColor.Discrete.pair {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)

The functor taking c to F c ⊗ F c.

Equations

• IndexNotation.OverColor.Discrete.pair F = CategoryTheory.MonoidalCategoryStruct.tensorObj F F

noncomputable def IndexNotation.OverColor.Discrete.pairτ {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (τ : C → C) : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)

The functor taking c to F c ⊗ F (τ c).

Equations

• IndexNotation.OverColor.Discrete.pairτ F τ = CategoryTheory.MonoidalCategoryStruct.tensorObj F ((CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ τ)).comp F)

theorem IndexNotation.OverColor.Discrete.pairτ_tmul {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {τ : C → C} {c1 c : C} (x : ↑(F.obj { as := c })) (y : ↑(((CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ τ)).comp F).obj { as := c })) (h : c = c1) : (Rep.Hom.hom ((pairτ F τ).map (CategoryTheory.Discrete.eqToHom h))) (x ⊗ₜ[k] y) = (Rep.Hom.hom (F.map (CategoryTheory.Discrete.eqToHom h))) x ⊗ₜ[k] (Rep.Hom.hom (F.map (CategoryTheory.Discrete.eqToHom ⋯))) y

noncomputable def IndexNotation.OverColor.Discrete.τPair {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (τ : C → C) : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)

The functor taking c to F (τ c) ⊗ F c.

Equations

• IndexNotation.OverColor.Discrete.τPair F τ = CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ τ)).comp F) F