toSpecΓ_naturality — Mathlib

English

For any morphism f: X ⟶ Y of schemes, the unit morphisms commute with Spec.map of f.appTop.

Русский

Для любой морфизмы f: X ⟶ Y между схемами единицы от X и Y коммутируют с отображением Spec.map(f.appTop).

LaTeX

$$ΓSpec.adjunction.unit.naturality f$$

Lean4

@[reassoc]
theorem toSpecΓ_naturality {X Y : Scheme.{u}} (f : X ⟶ Y) : f ≫ Y.toSpecΓ = X.toSpecΓ ≫ Spec.map (f.appTop) :=
  ΓSpec.adjunction.unit.naturality f

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