ι_sigmaSpec — Mathlib

English

For a family of commutative rings R indexed by ι, the ith structural inclusion in the Sigma-construction composed with sigmaSpec is equal to the Spec-map induced by the ith projection (evaluation) map.

Русский

Для семейства коммутативных колец R, индексируемого ι, i-ая компонентная вложение в конструкцию Sigma после применения sigmaSpec равно отображению Spec, полученному из i-й проекции (итеративное вычисление).

LaTeX

$$$\forall (ι : Type) (R : ι \to \mathrm{CommRingCat}),\ (i : ι),\\ Sigma.ι _ i \\;=\\; Spec.map (CommRingCat.ofHom (Pi.evalRingHom _ i)).$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_sigmaSpec (R : ι → CommRingCat) (i) :
    Sigma.ι _ i ≫ sigmaSpec R = Spec.map (CommRingCat.ofHom (Pi.evalRingHom _ i)) :=
  Sigma.ι_desc _ _

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