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 ⋯

def IndexNotation.OverColor.lift.discreteFunctorMapIso {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 ⟶ c2) : F.obj c1 ≅ F.obj c2

Takes a homomorphism of Discrete C to an isomorphism F.obj c1 ≅ F.obj c2.

Equations

• IndexNotation.OverColor.lift.discreteFunctorMapIso F h = F.mapIso (IndexNotation.OverColor.Discrete.homToIso h)

theorem IndexNotation.OverColor.lift.discreteFun_hom_trans {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) {c1 c2 c3 : CategoryTheory.Discrete C} (h1 : c1 = c2) (h2 : c2 = c3) (v : ↑(F.obj c1).V) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom h2)).hom) ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom h1)).hom) v) = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯)).hom) v

def IndexNotation.OverColor.lift.discreteFunctorMapEqIso {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

The linear equivalence between (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.discreteFunctorMapEqIso_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) : (discreteFunctorMapEqIso F h) (((F.obj c1).ρ M) x) = ((F.obj c2).ρ M) ((discreteFunctorMapEqIso F h) x)

def IndexNotation.OverColor.lift.objObj' {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 a object in OverColor Color the corresponding tensor product of representations.

Equations

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

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

theorem IndexNotation.OverColor.lift.objObj'_ρ_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) : ((objObj' F f).ρ M) ((PiTensorProduct.tprod k) x) = (PiTensorProduct.tprod k) fun (i : (CategoryTheory.Functor.id Type).obj f.left) => ((F.obj { as := f.hom i }).ρ M) (x i)

theorem IndexNotation.OverColor.lift.objObj'_ρ_empty {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (g : G) : (objObj' F (𝟙_ (OverColor C))).ρ g = LinearMap.id

@[simp]

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

def IndexNotation.OverColor.lift.mapToLinearEquiv' {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) : ↑(objObj' F f).V ≃ₗ[k] ↑(objObj' F g).V

Given a morphism in OverColor C the corresponding linear equivalence between obj' _ induced by reindexing.

Equations

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

theorem IndexNotation.OverColor.lift.mapToLinearEquiv'_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) : (mapToLinearEquiv' F m) ((PiTensorProduct.tprod k) x) = (PiTensorProduct.tprod k) fun (i : g.left) => (discreteFunctorMapEqIso F ⋯) (x ((Hom.toEquiv m).symm i))

def IndexNotation.OverColor.lift.objMap' {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) : objObj' F f ⟶ objObj' F g

Given a morphism in OverColor C the corresponding map of representations induced by reindexing.

Equations

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

theorem IndexNotation.OverColor.lift.objMap'_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 (objMap' F f).hom) ((PiTensorProduct.tprod k) p) = (PiTensorProduct.tprod k) fun (i : Y.left) => (discreteFunctorMapEqIso F ⋯) (p ((Hom.toEquiv f).symm i))

def IndexNotation.OverColor.lift.ε {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) : 𝟙_ (Rep k G) ≅ objObj' F (𝟙_ (OverColor C))

The unit natural isomorphism.

Equations

• IndexNotation.OverColor.lift.ε 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 : OverColor C} (i : X.left ⊕ Y.left) : Sum.elim (fun (i : (CategoryTheory.Functor.id Type).obj X.left) => ↑(F.obj { as := X.hom i }).V) (fun (i : (CategoryTheory.Functor.id Type).obj Y.left) => ↑(F.obj { as := Y.hom i }).V) i ≃ₗ[k] ↑(F.obj { as := (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).hom i }).V

An auxiliary equivalence, and trivial, of modules needed to define μModEquiv.

Equations

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

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

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

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) : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (objObj' F X) (objObj' F Y)).V ≃ₗ[k] ↑(objObj' 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 (objObj' F X) (objObj' F Y) ≅ objObj' 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 (objMap' F f) (objObj' F Z)) (μ F Y Z).hom = CategoryTheory.CategoryStruct.comp (μ F X Z).hom (objMap' 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 (objObj' F X') (objMap' F f)) (μ F X' Y).hom = CategoryTheory.CategoryStruct.comp (μ F X' X).hom (objMap' 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 (objObj' F Z)) (CategoryTheory.CategoryStruct.comp (μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom (objMap' F (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (objObj' F X) (objObj' F Y) (objObj' F Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (objObj' 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 (objObj' F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε F).hom (objObj' F X)) (CategoryTheory.CategoryStruct.comp (μ F (𝟙_ (OverColor C)) X).hom (objMap' 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 (objObj' F X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (objObj' F X) (ε F).hom) (CategoryTheory.CategoryStruct.comp (μ F X (𝟙_ (OverColor C))).hom (objMap' 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 (objMap' F (β_ X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (objObj' F X) (objObj' 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) : objMap' F (β_ X Y).hom = CategoryTheory.CategoryStruct.comp (μ F X Y).inv (CategoryTheory.CategoryStruct.comp (β_ (objObj' F X) (objObj' F Y)).hom (μ F Y X).hom)

theorem IndexNotation.OverColor.lift.objMap'_id {C k : Type} [CommRing k] {G : Type} [Group G] (F : CategoryTheory.Functor (CategoryTheory.Discrete C) (Rep k G)) (X : OverColor C) : objMap' F (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (objObj' F X)

theorem IndexNotation.OverColor.lift.objMap'_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) : objMap' F (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (objMap' F f) (objMap' F g)

def IndexNotation.OverColor.lift.obj' {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.

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

The lift of a functor is lax braided.

Equations

• IndexNotation.OverColor.lift.obj'_laxBraidedFunctor F = CategoryTheory.Functor.LaxBraided.mk ⋯

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

The lift of a functor is monoidal.

Equations

• IndexNotation.OverColor.lift.obj'_monoidalFunctor F = CategoryTheory.Functor.Monoidal.ofLaxMonoidal (IndexNotation.OverColor.lift.obj' F)

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

The lift of a functor is braided.

Equations

• IndexNotation.OverColor.lift.obj'_braided F = CategoryTheory.Functor.Braided.mk ⋯

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

The maps for a natural transformation between obj' F and obj' F'.

Equations

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

theorem IndexNotation.OverColor.lift.mapApp'_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 (mapApp' η X).hom) ((PiTensorProduct.tprod k) p) = (PiTensorProduct.tprod k) fun (i : (CategoryTheory.Functor.id Type).obj X.left) => (CategoryTheory.ConcreteCategory.hom (η.app { as := X.hom i }).hom) (p i)

theorem IndexNotation.OverColor.lift.mapApp'_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 ((obj' F).map f) (mapApp' η Y) = CategoryTheory.CategoryStruct.comp (mapApp' η X) ((obj' F').map f)

theorem IndexNotation.OverColor.lift.mapApp'_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.ε (obj' F)) (mapApp' η (𝟙_ (OverColor C))) = CategoryTheory.Functor.LaxMonoidal.ε (obj' F')

theorem IndexNotation.OverColor.lift.mapApp'_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.μ (obj' F) X Y) (mapApp' η (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (mapApp' η X) (mapApp' η Y)) (CategoryTheory.Functor.LaxMonoidal.μ (obj' F') X Y)

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

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

Equations

• IndexNotation.OverColor.lift.map' η = { app := IndexNotation.OverColor.lift.mapApp' η, naturality := ⋯ }

instance IndexNotation.OverColor.lift.map'_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 (map' η)

The lift of a natural transformation is monoidal.

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.obj'_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.obj'_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 = CategoryTheory.Functor.Braided.mk ⋯

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) => (discreteFunctorMapEqIso 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.left) => p (Sum.inl i)) ⊗ₜ[k] (PiTensorProduct.tprod k) fun (i : (CategoryTheory.Functor.id Type).obj Y.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

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 : (CategoryTheory.Functor.id Type).obj (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 : (CategoryTheory.Functor.id Type).obj (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] }