ΓSpecIso_obj_hom — Mathlib

English

For φ : B ⟶ Γ(X, ⊤) the appTop component of the homEquiv equals (ΓSpecIso B).hom ≫ φ.

Русский

Для φ: B ⟶ Γ(X, ⊤) компонент appTop гомэквивалентности равен композиции (ΓSpecIso B).hom с φ.

LaTeX

$$((ΓSpec.adjunction.homEquiv X (op B)) φ.op).appTop = (Scheme.ΓSpecIso B).hom ≫ φ$$

Lean4

theorem ΓSpecIso_obj_hom {X : Scheme.{u}} (U : X.Opens) :
    (Scheme.ΓSpecIso Γ(X, U)).hom = (Spec.map U.topIso.inv).appTop ≫ U.toScheme.toSpecΓ.appTop ≫ U.topIso.hom := by simp

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