Lifting functors.

There is a functor from functors Discrete C ⥤ Rep k G to braided monoidal functors BraidedFunctor (OverColor C) (Rep k G). We call this functor lift. It is a lift in the sense that it is a section of the forgetful functor BraidedFunctor (OverColor C) (Rep k G) ⥤ (Discrete C ⥤ Rep k G).

Functors in Discrete C ⥤ Rep k G form the basic building blocks of tensor structures. The fact that they extend to monoidal functors OverColor C ⥤ Rep k G allows us to interact more generally with tensors.

def IndexNotation.OverColor.Discrete.homToIso {C : Type} {c1 c2 : CategoryTheory.Discrete C} (h : c1 ⟶ c2) : c1 ≅ c2

Takes a homomorphism in Discrete C to an isomorphism built on the same objects.

Equations

• IndexNotation.OverColor.Discrete.homToIso h = CategoryTheory.Discrete.eqToIso ⋯

To representation

Given an object in OverColor C and a functor F : Discrete C ⥤ Rep k G, we get an object of Rep k G by taking the tensor product of the representations.

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

Given an object f : OverColor C and a function F : Discrete C ⥤ Rep k G, the object in Rep k G obtained by taking the tensor product of all colors in f.

Equations

• IndexNotation.OverColor.lift.toRep F f = Rep.of { toFun := fun (M : G) => PiTensorProduct.map fun (x : f.left) => (F.obj { as := f.hom x }).ρ M, map_one' := ⋯, map_mul' := ⋯ }

theorem IndexNotation.OverColor.lift.toRep_ρ {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (f : OverColor C) (M : G) : (toRep F f).ρ M = PiTensorProduct.map fun (x : (CategoryTheory.Functor.id Type).obj f.of.left) => (F.obj { as := f.hom x }).ρ M

theorem IndexNotation.OverColor.lift.toRep_ρ_tprod {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (f : OverColor C) (M : G) (x : (i : f.left) → ↑(F.obj { as := f.hom i }).V) : ((toRep F f).ρ M) ((PiTensorProduct.tprod k) x) = (PiTensorProduct.tprod k) fun (i : (CategoryTheory.Functor.id Type).obj f.of.left) => ((F.obj { as := f.hom i }).ρ M) (x i)

theorem IndexNotation.OverColor.lift.toRep_ρ_empty {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (g : G) : (toRep F (CategoryTheory.MonoidalCategoryStruct.tensorUnit (OverColor C))).ρ g = LinearMap.id

theorem IndexNotation.OverColor.lift.toRep_ρ_from_fin0 {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c : Fin 0 → C) (g : G) : (toRep F (mk c)).ρ g = LinearMap.id

theorem IndexNotation.OverColor.lift.toRep_V_carrier {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (f : OverColor C) : ↑(toRep F f).V = PiTensorProduct k fun (i : f.left) => ↑(F.obj { as := f.hom i }).V

Hom to representation hom

Given a morphism in OverColor C, m : f ⟶ g and a functor F : Discrete C ⥤ Rep k G, we get an morphism in Rep k G between toRep F f and toRep F g by taking the tensor product.

def IndexNotation.OverColor.lift.linearIsoOfEq {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {c1 c2 : CategoryTheory.Discrete C} (h : c1.as = c2.as) : ↑(F.obj c1).V ≃ₗ[k] ↑(F.obj c2).V

For a function F : Discrete C ⥤ Rep k G, the linear equivalence (F.obj c1).V ≃ₗ[k] (F.obj c2).V induced by an equality of c1 and c2.

Equations

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

theorem IndexNotation.OverColor.lift.linearIsoOfEq_comm_ρ {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {c1 c2 : CategoryTheory.Discrete C} (h : c1.as = c2.as) (M : G) (x : ↑(F.obj c1).V) : (linearIsoOfEq F h) (((F.obj c1).ρ M) x) = ((F.obj c2).ρ M) ((linearIsoOfEq F h) x)

def IndexNotation.OverColor.lift.linearIsoOfHom {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {f g : OverColor C} (m : f ⟶ g) : ↑(toRep F f).V ≃ₗ[k] ↑(toRep F g).V

Given a morphism in OverColor C, m : f ⟶ g and a functor F : Discrete C ⥤ Rep k G, the linear equivalence (toRep F f).V ≃ₗ[k] (toRep F g).V formed by reindexing.

Equations

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

theorem IndexNotation.OverColor.lift.linearIsoOfHom_tprod {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {f g : OverColor C} (m : f ⟶ g) (x : (i : f.left) → ↑(F.obj { as := f.hom i }).V) : (linearIsoOfHom F m) ((PiTensorProduct.tprod k) x) = (PiTensorProduct.tprod k) fun (i : g.left) => (linearIsoOfEq F ⋯) (x ((Hom.toEquiv m).symm i))

def IndexNotation.OverColor.lift.homToRepHom {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {f g : OverColor C} (m : f ⟶ g) : toRep F f ⟶ toRep F g

Given a morphism in OverColor C, m : f ⟶ g and a functor F : Discrete C ⥤ Rep k G, the morphism (toRep F f) ⟶ (toRep F g) formed by reindexing.

Equations

• IndexNotation.OverColor.lift.homToRepHom F m = { hom := ModuleCat.ofHom ↑(IndexNotation.OverColor.lift.linearIsoOfHom F m), comm := ⋯ }

theorem IndexNotation.OverColor.lift.homToRepHom_tprod {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {X Y : OverColor C} (p : (i : X.left) → ↑(F.obj { as := X.hom i }).V) (f : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (homToRepHom F f).hom) ((PiTensorProduct.tprod k) p) = (PiTensorProduct.tprod k) fun (i : Y.left) => (linearIsoOfEq F ⋯) (p ((Hom.toEquiv f).symm i))

theorem IndexNotation.OverColor.lift.homToRepHom_id {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X : OverColor C) : homToRepHom F (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toRep F X)

theorem IndexNotation.OverColor.lift.homToRepHom_comp {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {X Y Z : OverColor C} (f : X ⟶ Y) (g : Y ⟶ Z) : homToRepHom F (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (homToRepHom F f) (homToRepHom F g)

toRepFunc

The functions toRep F and homToRepHom F together form a functor.

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

The Functor (OverColor C) (Rep k G) from a functor Discrete C ⥤ Rep k G.

Equations

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

The braiding of toRepFunc

The functor toRepFunc is a braided monodial functor. This is made manifest in the result

• toRepFunc_braidedFunctor.

def IndexNotation.OverColor.lift.toRepUnitIso {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (Rep k G) ≅ toRep F (CategoryTheory.MonoidalCategoryStruct.tensorUnit (OverColor C))

The unit isomorphism between 𝟙_ (Rep k G) and toRep F (𝟙_ (OverColor C)) generated using PiTensorProduct.isEmptyEquiv.

Equations

• IndexNotation.OverColor.lift.toRepUnitIso F = Action.mkIso (PiTensorProduct.isEmptyEquiv Empty).symm.toModuleIso ⋯

def IndexNotation.OverColor.lift.discreteSumEquiv {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {X Y : Type} {cX : X → C} {cY : Y → C} (i : X ⊕ Y) : Sum.elim (fun (i : X) => ↑(F.obj { as := cX i }).V) (fun (i : Y) => ↑(F.obj { as := cY i }).V) i ≃ₗ[k] ↑(F.obj { as := Sum.elim cX cY i }).V

An equivalence used in the lemma of μ_tmul_tprod_mk. Identical to μModEquiv except with arguments based on maps instead of elements of OverColor C.

Equations

• IndexNotation.OverColor.lift.discreteSumEquiv F (Sum.inl val) = LinearEquiv.refl k (Sum.elim (fun (i : X) => ↑(F.obj { as := cX i }).V) (fun (i : Y) => ↑(F.obj { as := cY i }).V) (Sum.inl val))
• IndexNotation.OverColor.lift.discreteSumEquiv F (Sum.inr val) = LinearEquiv.refl k (Sum.elim (fun (i : X) => ↑(F.obj { as := cX i }).V) (fun (i : Y) => ↑(F.obj { as := cY i }).V) (Sum.inr val))

def IndexNotation.OverColor.lift.μModEquiv {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X Y : OverColor C) : TensorProduct k ↑(toRep F X).V ↑(toRep F Y).V ≃ₗ[k] ↑(toRep F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).V

The equivalence of modules corresponding to the tensor.

Equations

• IndexNotation.OverColor.lift.μModEquiv F X Y = PhysLean.PiTensorProduct.tmulEquiv.trans (PiTensorProduct.congr (IndexNotation.OverColor.lift.discreteSumEquiv F))

theorem IndexNotation.OverColor.lift.μModEquiv_tmul_tprod {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {X Y : OverColor C} (p : (i : X.left) → ↑(F.obj { as := X.hom i }).V) (q : (i : Y.left) → ↑(F.obj { as := Y.hom i }).V) : (μModEquiv F X Y) ((PiTensorProduct.tprod k) p ⊗ₜ[k] (PiTensorProduct.tprod k) q) = (PiTensorProduct.tprod k) fun (i : X.left ⊕ Y.left) => (discreteSumEquiv F i) (PhysLean.PiTensorProduct.elimPureTensor p q i)

def IndexNotation.OverColor.lift.μ {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X Y : OverColor C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (toRep F X) (toRep F Y) ≅ toRep F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The natural isomorphism corresponding to the tensor.

Equations

• IndexNotation.OverColor.lift.μ F X Y = Action.mkIso (IndexNotation.OverColor.lift.μModEquiv F X Y).toModuleIso ⋯

theorem IndexNotation.OverColor.lift.μ_tmul_tprod {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {X Y : OverColor C} (p : (i : X.left) → ↑(F.obj { as := X.hom i }).V) (q : (i : Y.left) → ↑(F.obj { as := Y.hom i }).V) : (CategoryTheory.ConcreteCategory.hom (μ F X Y).hom.hom) ((PiTensorProduct.tprod k) p ⊗ₜ[k] (PiTensorProduct.tprod k) q) = (PiTensorProduct.tprod k) fun (i : X.left ⊕ Y.left) => (discreteSumEquiv F i) (PhysLean.PiTensorProduct.elimPureTensor p q i)

theorem IndexNotation.OverColor.lift.μ_tmul_tprod_mk {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {X Y : Type} {cX : X → C} {cY : Y → C} (p : (i : X) → ↑(F.obj { as := cX i }).V) (q : (i : Y) → ↑(F.obj { as := cY i }).V) : (CategoryTheory.ConcreteCategory.hom (μ F (mk cX) (mk cY)).hom.hom) ((PiTensorProduct.tprod k) p ⊗ₜ[k] (PiTensorProduct.tprod k) q) = (PiTensorProduct.tprod k) fun (i : X ⊕ Y) => (discreteSumEquiv F i) (PhysLean.PiTensorProduct.elimPureTensor p q i)

theorem IndexNotation.OverColor.lift.μ_natural_left {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {X Y : OverColor C} (f : X ⟶ Y) (Z : OverColor C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (homToRepHom F f) (toRep F Z)) (μ F Y Z).hom = CategoryTheory.CategoryStruct.comp (μ F X Z).hom (homToRepHom F (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))

theorem IndexNotation.OverColor.lift.μ_natural_right {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {X Y : OverColor C} (X' : OverColor C) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (toRep F X') (homToRepHom F f)) (μ F X' Y).hom = CategoryTheory.CategoryStruct.comp (μ F X' X).hom (homToRepHom F (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f))

theorem IndexNotation.OverColor.lift.associativity {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X Y Z : OverColor C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (μ F X Y).hom (toRep F Z)) (CategoryTheory.CategoryStruct.comp (μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom (homToRepHom F (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (toRep F X) (toRep F Y) (toRep F Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (toRep F X) (μ F Y Z).hom) (μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom)

theorem IndexNotation.OverColor.lift.left_unitality {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X : OverColor C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (toRep F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (toRepUnitIso F).hom (toRep F X)) (CategoryTheory.CategoryStruct.comp (μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit (OverColor C)) X).hom (homToRepHom F (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))

theorem IndexNotation.OverColor.lift.right_unitality {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X : OverColor C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor (toRep F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (toRep F X) (toRepUnitIso F).hom) (CategoryTheory.CategoryStruct.comp (μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (OverColor C))).hom (homToRepHom F (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))

theorem IndexNotation.OverColor.lift.braided' {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X Y : OverColor C) : CategoryTheory.CategoryStruct.comp (μ F X Y).hom (homToRepHom F (β_ X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (toRep F X) (toRep F Y)).hom (μ F Y X).hom

theorem IndexNotation.OverColor.lift.braided {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X Y : OverColor C) : homToRepHom F (β_ X Y).hom = CategoryTheory.CategoryStruct.comp (μ F X Y).inv (CategoryTheory.CategoryStruct.comp (β_ (toRep F X) (toRep F Y)).hom (μ F Y X).hom)

instance IndexNotation.OverColor.lift.toRepFunc_laxBraidedFunctor {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) : (toRepFunc F).LaxBraided

The lift of a functor is lax braided.

Equations

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

instance IndexNotation.OverColor.lift.toRepFunc_monoidalFunctor {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) : (toRepFunc F).Monoidal

The lift of a functor is monoidal.

Equations

• IndexNotation.OverColor.lift.toRepFunc_monoidalFunctor F = CategoryTheory.Functor.Monoidal.ofLaxMonoidal (IndexNotation.OverColor.lift.toRepFunc F)

instance IndexNotation.OverColor.lift.toRepFunc_braidedFunctor {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) : (toRepFunc F).Braided

The lift of a functor is braided.

Equations

• IndexNotation.OverColor.lift.toRepFunc_braidedFunctor F = { toMonoidal := IndexNotation.OverColor.lift.toRepFunc_monoidalFunctor F, braided := ⋯ }

The natural transformation repNatTransOfColor

Given two functors F F' : Discrete C ⥤ Rep k G and a natural transformation η : F ⟶ F', we construct a natural transformation repNatTransOfColor : toRepFunc F ⟶ toRepFunc F' by taking the tensor product of the corresponding morphisms in η.

def IndexNotation.OverColor.lift.repNatTransOfColorApp {C k : Type} [CommRing k] {G : Type} [Group G] {F F' : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)} (η : F ⟶ F') (X : OverColor C) : (toRepFunc F).obj X ⟶ (toRepFunc F').obj X

Given two functors F F' : Discrete C ⥤ Rep k G and a natural transformation η : F ⟶ F', and an X : OverColor C, the (toRepFunc F).obj X ⟶ (toRepFunc F').obj X in Rep k G constructed by the tensor product of the morphisms in η with corresponding color.

Equations

• IndexNotation.OverColor.lift.repNatTransOfColorApp η X = { hom := ModuleCat.ofHom (PiTensorProduct.map fun (x : X.left) => ModuleCat.Hom.hom (η.app { as := X.hom x }).hom), comm := ⋯ }

theorem IndexNotation.OverColor.lift.repNatTransOfColorApp_tprod {C k : Type} [CommRing k] {G : Type} [Group G] {F F' : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)} (η : F ⟶ F') (X : OverColor C) (p : (i : X.left) → ↑(F.obj { as := X.hom i }).V) : (CategoryTheory.ConcreteCategory.hom (repNatTransOfColorApp η X).hom) ((PiTensorProduct.tprod k) p) = (PiTensorProduct.tprod k) fun (i : (CategoryTheory.Functor.id Type).obj X.of.left) => (CategoryTheory.ConcreteCategory.hom (η.app { as := X.hom i }).hom) (p i)

theorem IndexNotation.OverColor.lift.repNatTransOfColorApp_naturality {C k : Type} [CommRing k] {G : Type} [Group G] {F F' : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)} (η : F ⟶ F') {X Y : OverColor C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((toRepFunc F).map f) (repNatTransOfColorApp η Y) = CategoryTheory.CategoryStruct.comp (repNatTransOfColorApp η X) ((toRepFunc F').map f)

def IndexNotation.OverColor.lift.repNatTransOfColor {C k : Type} [CommRing k] {G : Type} [Group G] {F F' : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)} (η : F ⟶ F') : toRepFunc F ⟶ toRepFunc F'

Given a natural transformation between F F' : Discrete C ⥤ Rep k G the monoidal natural transformation between toRepFunc F and toRepFunc F'.

Equations

• IndexNotation.OverColor.lift.repNatTransOfColor η = { app := IndexNotation.OverColor.lift.repNatTransOfColorApp η, naturality := ⋯ }

The Monoidal structure of repNatTransOfColor

The natural transformation repNatTransOfColor is monoidal, which is made manifest in the results

• repNatTransOfColor_isMonoidal.

theorem IndexNotation.OverColor.lift.repNatTransOfColorApp_unit {C k : Type} [CommRing k] {G : Type} [Group G] {F F' : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)} (η : F ⟶ F') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (toRepFunc F)) (repNatTransOfColorApp η (CategoryTheory.MonoidalCategoryStruct.tensorUnit (OverColor C))) = CategoryTheory.Functor.LaxMonoidal.ε (toRepFunc F')

theorem IndexNotation.OverColor.lift.repNatTransOfColorApp_tensor {C k : Type} [CommRing k] {G : Type} [Group G] {F F' : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)} (η : F ⟶ F') (X Y : OverColor C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (toRepFunc F) X Y) (repNatTransOfColorApp η (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (repNatTransOfColorApp η X) (repNatTransOfColorApp η Y)) (CategoryTheory.Functor.LaxMonoidal.μ (toRepFunc F') X Y)

instance IndexNotation.OverColor.lift.repNatTransOfColor_isMonoidal {C k : Type} [CommRing k] {G : Type} [Group G] {F F' : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)} (η : F ⟶ F') : CategoryTheory.NatTrans.IsMonoidal (repNatTransOfColor η)

The lift of a natural transformation is monoidal.

The functor lift

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

The functor taking functors in Discrete C ⥤ Rep k G to monoidal functors in BraidedFunctor (OverColor C) (Rep k G), built on the PiTensorProduct.

Equations

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

noncomputable instance IndexNotation.OverColor.lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) : (lift.obj F).Monoidal

The lift of a functor is monoidal.

Equations

• IndexNotation.OverColor.lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor F = IndexNotation.OverColor.lift.toRepFunc_monoidalFunctor F

noncomputable instance IndexNotation.OverColor.lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) : (lift.obj F).LaxBraided

The lift of a functor is lax-braided.

Equations

• IndexNotation.OverColor.lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor F = IndexNotation.OverColor.lift.toRepFunc_laxBraidedFunctor F

noncomputable instance IndexNotation.OverColor.lift.instBraidedRepObjFunctorDiscreteLaxBraidedFunctor {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) : (lift.obj F).Braided

The lift of a functor is braided.

Equations

• IndexNotation.OverColor.lift.instBraidedRepObjFunctorDiscreteLaxBraidedFunctor F = { toMonoidal := IndexNotation.OverColor.lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor F, braided := ⋯ }

theorem IndexNotation.OverColor.lift.map_tprod {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {X Y : OverColor C} (f : X ⟶ Y) (p : (i : X.left) → ↑(F.obj { as := X.hom i }).V) : (CategoryTheory.ConcreteCategory.hom ((lift.obj F).map f).hom) ((PiTensorProduct.tprod k) p) = (PiTensorProduct.tprod k) fun (i : Y.left) => (linearIsoOfEq F ⋯) (p ((Hom.toEquiv f).symm i))

theorem IndexNotation.OverColor.lift.obj_μ_tprod_tmul {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X Y : OverColor C) (p : (i : X.left) → ↑(F.obj { as := X.hom i }).V) (q : (i : Y.left) → ↑(F.obj { as := Y.hom i }).V) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom) ((PiTensorProduct.tprod k) p ⊗ₜ[k] (PiTensorProduct.tprod k) q) = (PiTensorProduct.tprod k) fun (i : X.left ⊕ Y.left) => (discreteSumEquiv F i) (PhysLean.PiTensorProduct.elimPureTensor p q i)

theorem IndexNotation.OverColor.lift.μIso_inv_tprod {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X Y : OverColor C) (p : (i : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).left) → ↑(F.obj { as := (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).hom i }).V) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.Monoidal.μIso (lift.obj F).toFunctor X Y).inv.hom) ((PiTensorProduct.tprod k) p) = ((PiTensorProduct.tprod k) fun (i : (CategoryTheory.Functor.id Type).obj X.of.left) => p (Sum.inl i)) ⊗ₜ[k] (PiTensorProduct.tprod k) fun (i : (CategoryTheory.Functor.id Type).obj Y.of.left) => p (Sum.inr i)

@[simp]

theorem IndexNotation.OverColor.lift.inv_μ {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X Y : OverColor C) : CategoryTheory.inv (CategoryTheory.Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y) = (μ F X Y).inv

The forgetful functor from BraidedFunctor (OverColor C) (Rep k G) to Discrete C ⥤ Rep k G

def IndexNotation.OverColor.incl {C : Type} : CategoryTheory.Functor (CategoryTheory.Discrete C) (OverColor C)

The natural inclusion of Discrete C into OverColor C.

Equations

• IndexNotation.OverColor.incl = CategoryTheory.Discrete.functor fun (c : C) => IndexNotation.OverColor.mk fun (x : Fin 1) => c

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

The forgetful map from BraidedFunctor (OverColor C) (Rep k G) to Discrete C ⥤ Rep k G built on the inclusion incl and forgetting the monoidal structure.

Equations

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

def IndexNotation.OverColor.forgetLiftAppV {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c : C) : ↑((lift.obj F).obj (mk fun (x : Fin 1) => c)).V ≃ₗ[k] ↑(F.obj { as := c }).V

The forgetLiftAppV function takes an object c of type C and returns a linear equivalence between the vector space obtained by applying the lift of F and that obtained by applying F.

Equations

• IndexNotation.OverColor.forgetLiftAppV F c = PiTensorProduct.subsingletonEquiv 0

@[simp]

theorem IndexNotation.OverColor.forgetLiftAppV_symm_apply {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c : C) (x : ↑(F.obj { as := c }).V) : (forgetLiftAppV F c).symm x = (PiTensorProduct.tprod k) fun (x_1 : (mk fun (x : Fin 1) => c).left) => x

def IndexNotation.OverColor.forgetLiftApp {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c : C) : (lift.obj F).obj (mk fun (x : Fin 1) => c) ≅ F.obj { as := c }

The forgetLiftAppV function takes an object c of type C and returns a isomorphism between the objects obtained by applying the lift of F and that obtained by applying F.

Equations

• IndexNotation.OverColor.forgetLiftApp F c = Action.mkIso (IndexNotation.OverColor.forgetLiftAppV F c).toModuleIso ⋯

theorem IndexNotation.OverColor.forgetLiftApp_naturality_eqToHom {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c c1 : C) (h : c = c1) : CategoryTheory.CategoryStruct.comp (forgetLiftApp F c).hom (F.map (CategoryTheory.Discrete.eqToHom h)) = CategoryTheory.CategoryStruct.comp ((lift.obj F).map (mkIso ⋯).hom) (forgetLiftApp F c1).hom

theorem IndexNotation.OverColor.forgetLiftApp_naturality_eqToHom_apply {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c c1 : C) (h : c = c1) (x : ↑((lift.obj F).obj (mk fun (x : Fin 1) => c)).V) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Discrete.eqToHom h)).hom) ((CategoryTheory.ConcreteCategory.hom (forgetLiftApp F c).hom.hom) x) = (CategoryTheory.ConcreteCategory.hom (forgetLiftApp F c1).hom.hom) ((CategoryTheory.ConcreteCategory.hom ((lift.obj F).map (mkIso ⋯).hom).hom) x)

theorem IndexNotation.OverColor.forgetLiftApp_hom_hom_apply_eq {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c : C) (x : ↑((lift.obj F).obj (mk fun (x : Fin 1) => c)).V) (y : ↑(F.obj { as := c }).V) : (CategoryTheory.ConcreteCategory.hom (forgetLiftApp F c).hom.hom) x = y ↔ x = (PiTensorProduct.tprod k) fun (x : (mk fun (x : Fin 1) => c).left) => y

def IndexNotation.OverColor.forgetLiftAppCon {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c : C) : (lift.obj F).obj (mk ![c]) ≅ F.obj { as := c }

The isomorphism between the representation (lift.obj F).obj (OverColor.mk ![c]) and the representation F.obj (Discrete.mk c). See forgetLiftApp for an alternative version.

Equations

• IndexNotation.OverColor.forgetLiftAppCon F c = (IndexNotation.OverColor.lift.obj F).mapIso (IndexNotation.OverColor.mkIso ⋯) ≪≫ IndexNotation.OverColor.forgetLiftApp F c

theorem IndexNotation.OverColor.forgetLiftAppCon_inv_apply_expand {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c : C) (x : ↑(F.obj { as := c }).V) : (CategoryTheory.ConcreteCategory.hom (forgetLiftAppCon F c).inv.hom) x = (CategoryTheory.ConcreteCategory.hom ((lift.obj F).map (mkIso ⋯).hom).hom) ((CategoryTheory.ConcreteCategory.hom (forgetLiftApp F c).inv.hom) x)

theorem IndexNotation.OverColor.forgetLiftAppCon_naturality_eqToHom {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c c1 : C) (h : c = c1) : CategoryTheory.CategoryStruct.comp (forgetLiftAppCon F c).hom (F.map (CategoryTheory.Discrete.eqToHom h)) = CategoryTheory.CategoryStruct.comp ((lift.obj F).map (mkIso ⋯).hom) (forgetLiftAppCon F c1).hom

theorem IndexNotation.OverColor.forgetLiftAppCon_naturality_eqToHom_apply {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (c c1 : C) (h : c = c1) (x : ↑((lift.obj F).obj (mk ![c])).V) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Discrete.eqToHom h)).hom) ((CategoryTheory.ConcreteCategory.hom (forgetLiftAppCon F c).hom.hom) x) = (CategoryTheory.ConcreteCategory.hom (forgetLiftAppCon F c1).hom.hom) ((CategoryTheory.ConcreteCategory.hom ((lift.obj F).map (mkIso ⋯).hom).hom) x)

def IndexNotation.OverColor.forgetLift : InformalDefinition

The natural isomorphism between lift (C := C) ⋙ forget and Functor.id (Discrete C ⥤ Rep k G).

Equations

• IndexNotation.OverColor.forgetLift = { deps := [`IndexNotation.OverColor.forget, `IndexNotation.OverColor.lift], tag := "6VZWS" }