instIsMonoidalClosedModuleCatIsFG

English

Over a field K, the monoidal category FGModuleCat K is closed: for fg modules X,Y the internal hom is the finite-dimensional K-vector space of linear maps X → Y, and Hom(Z ⊗ X, Y) ≅ Hom(Z, X → Y) naturally.

Русский

Над полем K категория FGModuleCat K замкнута: внутреннее гом-объект между X и Y равно конечномерному пространству линейных отображений X → Y, и естественное изоморфизм Hom(Z ⊗ X, Y) ≅ Hom(Z, Hom(X,Y)) существует.

LaTeX

$$$FGModuleCat(K)$ is monoidal closed with internal hom $[X,Y] \cong \mathrm{Hom}_K(X,Y)$ and natural isomorphisms $\mathrm{Hom}(Z\otimes X,Y) \cong \mathrm{Hom}(Z,[X,Y])$ for all finite $X,Y$.$$

Lean4

instance : (ModuleCat.isFG K).IsMonoidalClosed where
  prop_ihom {X Y} (_ : Module.Finite _ _)
    (_ : Module.Finite _ _) := (inferInstanceAs <| Module.Finite K (X →ₗ[K] Y)).equiv ModuleCat.homLinearEquiv.symm

Похожие утверждения