[GOAL]
R : Type u
inst✝ : Ring R
M : FGModuleCat R
⊢ AddCommGroup ↑M
[PROOFSTEP]
change AddCommGroup M.obj
[GOAL]
R : Type u
inst✝ : Ring R
M : FGModuleCat R
⊢ AddCommGroup ↑M.obj
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
M : FGModuleCat R
⊢ Module R ↑M
[PROOFSTEP]
change Module R M.obj
[GOAL]
R : Type u
inst✝ : Ring R
M : FGModuleCat R
⊢ Module R ↑M.obj
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
⊢ LargeCategory (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : Ring R
⊢ LargeCategory (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
⊢ ConcreteCategory (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : Ring R
⊢ ConcreteCategory (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
⊢ Preadditive (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : Ring R
⊢ Preadditive (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝³ : Ring R
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Finite R V
⊢ Module.Finite R ↑(ModuleCat.of R V)
[PROOFSTEP]
change Module.Finite R V
[GOAL]
R : Type u
inst✝³ : Ring R
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Finite R V
⊢ Module.Finite R V
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : Ring R
⊢ HasForget₂ (FGModuleCat R) (ModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : Ring R
⊢ HasForget₂ (FullSubcategory fun V => Module.Finite R ↑V) (ModuleCat R)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝⁶ : Ring R
V W : Type u
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
⊢ ↑e ≫ ↑(LinearEquiv.symm e) = 𝟙 (of R V)
[PROOFSTEP]
ext x
[GOAL]
case w
R : Type u
inst✝⁶ : Ring R
V W : Type u
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : (forget (FGModuleCat R)).obj (of R V)
⊢ ↑(↑e ≫ ↑(LinearEquiv.symm e)) x = ↑(𝟙 (of R V)) x
[PROOFSTEP]
exact e.left_inv x
[GOAL]
R : Type u
inst✝⁶ : Ring R
V W : Type u
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
⊢ ↑(LinearEquiv.symm e) ≫ ↑e = 𝟙 (of R W)
[PROOFSTEP]
ext x
[GOAL]
case w
R : Type u
inst✝⁶ : Ring R
V W : Type u
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : (forget (FGModuleCat R)).obj (of R W)
⊢ ↑(↑(LinearEquiv.symm e) ≫ ↑e) x = ↑(𝟙 (of R W)) x
[PROOFSTEP]
exact e.right_inv x
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Linear R (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Linear R (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalCategory (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalCategory (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ SymmetricCategory (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ SymmetricCategory (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalPreadditive (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalPreadditive (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalLinear R (FGModuleCat R)
[PROOFSTEP]
dsimp [FGModuleCat]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalLinear R (FullSubcategory fun V => Module.Finite R ↑V)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Faithful (forget₂Monoidal R).toLaxMonoidalFunctor.toFunctor
[PROOFSTEP]
dsimp [forget₂Monoidal]
  -- Porting note: was `infer_instance`
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Faithful (fullSubcategoryInclusion fun V => Module.Finite R ↑V)
[PROOFSTEP]
exact FullSubcategory.faithful _
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Functor.Additive (forget₂Monoidal R).toLaxMonoidalFunctor.toFunctor
[PROOFSTEP]
dsimp [forget₂Monoidal]
  -- Porting note: was `infer_instance`
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Functor.Additive (fullSubcategoryInclusion fun V => Module.Finite R ↑V)
[PROOFSTEP]
exact Functor.fullSubcategoryInclusion_additive _
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Functor.Linear R (forget₂Monoidal R).toLaxMonoidalFunctor.toFunctor
[PROOFSTEP]
dsimp [forget₂Monoidal]
  -- Porting note: was `infer_instance`
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ Functor.Linear R (fullSubcategoryInclusion fun V => Module.Finite R ↑V)
[PROOFSTEP]
exact Functor.fullSubcategoryInclusionLinear _ _
[GOAL]
K : Type u
inst✝ : Field K
V W : FGModuleCat K
⊢ Module.Finite K (↑V →ₗ[K] ↑W)
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u
inst✝ : Field K
⊢ MonoidalClosed (FGModuleCat K)
[PROOFSTEP]
dsimp [FGModuleCat]
  -- Porting note: was `infer_instance`
[GOAL]
K : Type u
inst✝ : Field K
⊢ MonoidalClosed (FullSubcategory fun V => Module.Finite K ↑V)
[PROOFSTEP]
exact MonoidalCategory.fullMonoidalClosedSubcategory _
[GOAL]
K : Type u
inst✝ : Field K
V W : FGModuleCat K
⊢ (𝟙 (FGModuleCatDual K V) ⊗ FGModuleCatCoevaluation K V) ≫
      (α_ (FGModuleCatDual K V) V (FGModuleCatDual K V)).inv ≫ (FGModuleCatEvaluation K V ⊗ 𝟙 (FGModuleCatDual K V)) =
    (ρ_ (FGModuleCatDual K V)).hom ≫ (λ_ (FGModuleCatDual K V)).inv
[PROOFSTEP]
apply contractLeft_assoc_coevaluation K V
[GOAL]
K : Type u
inst✝ : Field K
V W : FGModuleCat K
⊢ (FGModuleCatCoevaluation K V ⊗ 𝟙 V) ≫ (α_ V (FGModuleCatDual K V) V).hom ≫ (𝟙 V ⊗ FGModuleCatEvaluation K V) =
    (λ_ V).hom ≫ (ρ_ V).inv
[PROOFSTEP]
apply contractLeft_assoc_coevaluation' K V
