tensorProductFan' — Mathlib

English

A variant of the previous fan, where the target is the limit cone built from ∀i, S ⊗R P i, giving a family of maps indexed by i.

Русский

Вариант предыдущего веера, где целевой конус строится из ∀i, S ⊗R P i, образуя семейство отображений индексируемых по i.

LaTeX

$$$\\text{tensorProductFan'} : \\text{Fan}\\; (i \\mapsto \\mathrm{mkUnder}\ S\\ (S \\otimes_R (P i).right\\, .carrier))$$$

Lean4

/-- The fan on `i ↦ S ⊗[R] P i` given by `∀ i, S ⊗[R] P i` -/
def tensorProductFan' : Fan (fun i ↦ mkUnder S (S ⊗[R] (P i).right)) :=
  Fan.mk (mkUnder S <| ∀ i, S ⊗[R] (P i).right) (fun i ↦ AlgHom.toUnder <| Pi.evalAlgHom S _ i)

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