instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace

English

The morphism (Scheme.ΓSpecIso Γ(X, U)).hom equals (Spec.map U.topIso.inv).appTop ≫ U.toScheme.toSpecΓ.appTop ≫ U.topIso.hom.

Русский

Гомоморфизм (Scheme.ΓSpecIso Γ(X, U)).hom равен последовательности (Spec.map U.topIso.inv).appTop ≫ U.toScheme.toSpecΓ.appTop ≫ U.topIso.hom.

LaTeX

$$((Scheme.ΓSpecIso (X.presheaf.obj { unop := U })).hom) = ((Spec.map U.topIso.inv).appTop) ≫ U.toScheme.toSpecΓ.appTop ≫ U.topIso.hom$$

Lean4

/-- Spec is a full functor. -/
instance : Spec.toLocallyRingedSpace.Full :=
  Spec.fullyFaithfulToLocallyRingedSpace.full

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