[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ Linear k (FdRep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ AddCommGroup (CoeSort.coe V)
[PROOFSTEP]
change AddCommGroup ((forget₂ (FdRep k G) (FGModuleCat k)).obj V).obj
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ AddCommGroup ↑((forget₂ (FdRep k G) (FGModuleCat k)).obj V).obj
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ Module k (CoeSort.coe V)
[PROOFSTEP]
change Module k ((forget₂ (FdRep k G) (FGModuleCat k)).obj V).obj
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ Module k ↑((forget₂ (FdRep k G) (FGModuleCat k)).obj V).obj
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ FiniteDimensional k (CoeSort.coe V)
[PROOFSTEP]
change FiniteDimensional k ((forget₂ (FdRep k G) (FGModuleCat k)).obj V)
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ FiniteDimensional k ↑((forget₂ (FdRep k G) (FGModuleCat k)).obj V)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ ↑(ρ W) g = ↑(LinearEquiv.conj (isoToLinearEquiv i)) (↑(ρ V) g)
[PROOFSTEP]
erw [FdRep.isoToLinearEquiv, ← FGModuleCat.Iso.conj_eq_conj, Iso.conj_apply]
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ ↑(ρ W) g =
    ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).inv ≫
      ↑(ρ V) g ≫ ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).hom
[PROOFSTEP]
rw [Iso.eq_inv_comp ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i)]
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).hom ≫ ↑(ρ W) g =
    ↑(ρ V) g ≫ ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).hom
[PROOFSTEP]
exact (i.hom.comm g).symm
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ Rep.ρ ((forget₂ (FdRep k G) (Rep k G)).obj V) = ρ V
[PROOFSTEP]
ext g v
[GOAL]
case h.h
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
g : G
v : CoeSort.coe ((forget₂ (FdRep k G) (Rep k G)).obj V)
⊢ ↑(↑(Rep.ρ ((forget₂ (FdRep k G) (Rep k G)).obj V)) g) v = ↑(↑(ρ V) g) v
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalCategory (FdRep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalPreadditive (FdRep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalLinear k (FdRep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ HasKernels (FdRep k G)
[PROOFSTEP]
infer_instance
  -- Verify that Schur's lemma applies out of the box.
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FdRep k G
x✝ : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y
⊢ (fun f => Action.Hom.mk ((forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => Action.Hom.mk f.hom,
                map_add' :=
                  (_ :
                    ∀ (x x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                      (fun f => Action.Hom.mk f.hom) (x + x_1) = (fun f => Action.Hom.mk f.hom) (x + x_1)) },
            map_smul' :=
              (_ :
                ∀ (x : k) (x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                  AddHom.toFun
                      { toFun := fun f => Action.Hom.mk f.hom,
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                              (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                      (x • x_1) =
                    AddHom.toFun
                      { toFun := fun f => Action.Hom.mk f.hom,
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                              (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                      (x • x_1)) }.toAddHom
        x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case h.h
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FdRep k G
x✝¹ : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y
x✝ : ↑((forget₂ (FdRep k G) (Rep k G)).obj X).V
⊢ ↑((fun f => Action.Hom.mk ((forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom))
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := fun f => Action.Hom.mk f.hom,
                      map_add' :=
                        (_ :
                          ∀ (x x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                            (fun f => Action.Hom.mk f.hom) (x + x_1) = (fun f => Action.Hom.mk f.hom) (x + x_1)) },
                  map_smul' :=
                    (_ :
                      ∀ (x : k) (x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                        AddHom.toFun
                            { toFun := fun f => Action.Hom.mk f.hom,
                              map_add' :=
                                (_ :
                                  ∀
                                    (x x_2 :
                                      (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                                    (fun f => Action.Hom.mk f.hom) (x + x_2) =
                                      (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                            (x • x_1) =
                          AddHom.toFun
                            { toFun := fun f => Action.Hom.mk f.hom,
                              map_add' :=
                                (_ :
                                  ∀
                                    (x x_2 :
                                      (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                                    (fun f => Action.Hom.mk f.hom) (x + x_2) =
                                      (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                            (x • x_1)) }.toAddHom
              x✝¹)).hom
      x✝ =
    ↑x✝¹.hom x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FdRep k G
x✝ : X ⟶ Y
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => Action.Hom.mk f.hom,
              map_add' :=
                (_ :
                  ∀ (x x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                    (fun f => Action.Hom.mk f.hom) (x + x_1) = (fun f => Action.Hom.mk f.hom) (x + x_1)) },
          map_smul' :=
            (_ :
              ∀ (x : k) (x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                AddHom.toFun
                    { toFun := fun f => Action.Hom.mk f.hom,
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                            (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                    (x • x_1) =
                  AddHom.toFun
                    { toFun := fun f => Action.Hom.mk f.hom,
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                            (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                    (x • x_1)) }.toAddHom
      ((fun f => Action.Hom.mk ((forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom)) x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case h.w
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FdRep k G
x✝¹ : X ⟶ Y
x✝ : (forget (FGModuleCat k)).obj X.V
⊢ ↑(AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => Action.Hom.mk f.hom,
                    map_add' :=
                      (_ :
                        ∀ (x x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                          (fun f => Action.Hom.mk f.hom) (x + x_1) = (fun f => Action.Hom.mk f.hom) (x + x_1)) },
                map_smul' :=
                  (_ :
                    ∀ (x : k) (x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                      AddHom.toFun
                          { toFun := fun f => Action.Hom.mk f.hom,
                            map_add' :=
                              (_ :
                                ∀
                                  (x x_2 :
                                    (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                                  (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                          (x • x_1) =
                        AddHom.toFun
                          { toFun := fun f => Action.Hom.mk f.hom,
                            map_add' :=
                              (_ :
                                ∀
                                  (x x_2 :
                                    (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                                  (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                          (x • x_1)) }.toAddHom
            ((fun f => Action.Hom.mk ((forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom)) x✝¹)).hom
      x✝ =
    ↑x✝¹.hom x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Group G
⊢ RightRigidCategory (FdRep k G)
[PROOFSTEP]
change RightRigidCategory (Action (FGModuleCat k) (GroupCat.of G))
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Group G
⊢ RightRigidCategory (Action (FGModuleCat k) ((forget₂ GroupCat MonCat).obj (GroupCat.of G)))
[PROOFSTEP]
infer_instance
[GOAL]
k G V : Type u
inst✝⁴ : Field k
inst✝³ : Group G
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : FiniteDimensional k V
ρV : Representation k G V
W : FdRep k G
⊢ of (dual ρV) ⊗ W ≅ of (linHom ρV (ρ W))
[PROOFSTEP]
refine Action.mkIso (dualTensorIsoLinHomAux ρV W) ?_
[GOAL]
k G V : Type u
inst✝⁴ : Field k
inst✝³ : Group G
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : FiniteDimensional k V
ρV : Representation k G V
W : FdRep k G
⊢ ∀ (g : ↑(MonCat.of G)),
    ↑(of (dual ρV) ⊗ W).ρ g ≫ (dualTensorIsoLinHomAux ρV W).hom =
      (dualTensorIsoLinHomAux ρV W).hom ≫ ↑(of (linHom ρV (ρ W))).ρ g
[PROOFSTEP]
convert dualTensorHom_comm ρV W.ρ
