instPreservesLimitUnderDiscreteFunctorTensorProdOfFinite

English

The canonical piFan construction over a family under R yields a limit in the Under category when ι is finite.

Русский

Конструкция piFan над семейством объектов Under R образует предел в категории Under при конечном ι.

LaTeX

$$$\\text{Under.piFanIsLimit } f : IsLimit (Under.piFan f)$$$

Lean4

instance (J : Type u) [Finite J] (f : J → Under R) : PreservesLimit (Discrete.functor f) (tensorProd R S) :=
  let c : Fan _ := Under.piFan f
  have hc : IsLimit c := Under.piFanIsLimit f
  preservesLimit_of_preserves_limit_cone hc (piFanTensorProductIsLimit f)

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