instPreservesFiniteProductsUnderTensorProd

English

For the functor tensorProd R S, the underlying object preserves finite products in the Under category, i.e., it respects finite limits through a natural isomorphism.

Русский

Для тензорного произведения tensorProd R S функция сохраняет конечные произведения в категории Under, то есть сохраняет конечные пределы через естественное изоморфизм.

LaTeX

$$$\\text{PreservesFiniteProducts }(R \\otimes S) $ in Under$$

Lean4

instance : PreservesFiniteProducts (tensorProd R S) where
  preserves
    n :=
    let J : Type u := ULift.{u} (Fin n)
    have : PreservesLimitsOfShape (Discrete J) (tensorProd R S) := preservesLimitsOfShape_of_discrete (tensorProd R S)
    preservesLimitsOfShape_of_equiv (Discrete.equivalence Equiv.ulift) (R.tensorProd S)

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