tensorProductFan — Mathlib

English

Define a canonical fan on i ↦ mkUnder S (S ⊗R P i). The legs are given by the natural algebra maps, forming a cone over the diagram of tensor products.

Русский

Задан канонический веер на i ↦ mkUnder S (S ⊗R P i). Наборы ребер даны естественными отображениями алгебр, образуя конус над диаграммой тензорных произведений.

LaTeX

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

Lean4

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

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