Discrete color category

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

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 }).V) (y : ↑(((Action.functorCategoryEquivalence (ModuleCat k) ↑(MonCat.of G)).symm.inverse.obj (((CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ τ)).comp F).obj { as := c })).obj PUnit.unit)) (h : c = c1) : (CategoryTheory.ConcreteCategory.hom ((pairτ F τ).map (CategoryTheory.Discrete.eqToHom h)).hom) (x ⊗ₜ[k] y) = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Discrete.eqToHom h)).hom) x ⊗ₜ[k] (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Discrete.eqToHom ⋯)).hom) y

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