map_appLE — Mathlib

English

For opens U,V with e: U ≤ (Spec.map f)^{-1}(V), the appLE component equals the StructureSheaf comap map.

Русский

Для открытых U,V и включения e: U ≤ (Spec.map f)^{-1}(V) компонент AppLE равен отображению по StructureSheaf.

LaTeX

$$$ (\mathrm{Spec.map} f).\mathrm{appLE} V U e = \mathrm{CommRingCat.ofHom} (\mathrm{StructureSheaf.comap} (\mathrm{CommRingCat.Hom.hom} f) V U e). $$$

Lean4

theorem map_appLE {U V} (e : U ≤ Spec.map f ⁻¹ᵁ V) :
    (Spec.map f).appLE V U e = CommRingCat.ofHom (StructureSheaf.comap f.hom V U e) :=
  rfl

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