toSpecMvPolyIntEquiv_comp — Mathlib

English

Functorial compatibility: toSpecMvPolyIntEquiv n respects composition, i.e., toSpecMvPolyIntEquiv n (f ≫ g) i = f.appTop (toSpecMvPolyIntEquiv n g i).

Русский

Совместимость по отношению к композиции: toSpecMvPolyIntEquiv n сохраняет композицию, то есть toSpecMvPolyIntEquiv n (f ≫ g) i = f.appTop (toSpecMvPolyIntEquiv n g i).

LaTeX

$$$ toSpecMvPolyIntEquiv_n (f \gg g) = (f) \circ (toSpecMvPolyIntEquiv_n g)$$$

Lean4

theorem toSpecMvPolyIntEquiv_comp {X Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ Spec ℤ[n]) (i) :
    toSpecMvPolyIntEquiv n (f ≫ g) i = f.appTop (toSpecMvPolyIntEquiv n g i) :=
  rfl

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