tensorProductFanIsLimit — Mathlib

English

If ι is finite, the canonical tensorProductFan S P forms a limit cone over the diagram of Under objects indexed by ι.

Русский

Если ι конечен, канонический веер tensorProductFan S P образует предел-конус над диаграммой объектов Under индексированной по ι.

LaTeX

$$$\\text{IsLimit}(\\text{tensorProductFan } S P)$ for finite ι$$

Lean4

/-- The fan on `i ↦ S ⊗[R] P i` given by `S ⊗[R] ∀ i, P i` is limiting if `ι` is finite. -/
def tensorProductFanIsLimit [Finite ι] : IsLimit (tensorProductFan S P) :=
  letI : Fintype ι := Fintype.ofFinite ι
  (IsLimit.equivIsoLimit (tensorProductFanIso P)).symm (Under.piFanIsLimit _)

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