instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine

English

If X is an affine scheme, the unit of the adjunction between Spec and Γ at X is an isomorphism.

Русский

Если X — аффинная схема, то единица сопряжения между Spec и Γ на X является изоморфизмом.

LaTeX

$$$\\eta_X:\\; X \\to \\mathrm{Spec}(\\Gamma(X)) \\text{ is an isomorphism, i.e. } \\eta_X\\text{ is invertible.}$$$

Lean4

instance (X : Scheme.{u}) [IsAffine X] : IsIso (ΓSpec.adjunction.unit.app X) :=
  @IsAffine.affine X _

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