SpecΓIdentity

Mathlib.AlgebraicGeometry.Spec

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity

Lean4

/-- The counit (`SpecΓIdentity.inv.op`) of the adjunction `Γ ⊣ Spec` is an isomorphism. -/
@[simps! hom_app inv_app]
def SpecΓIdentity : Spec.toLocallyRingedSpace.rightOp ⋙ Γ ≅ 𝟭 _ :=
  Iso.symm <|
    NatIso.ofComponents.{u, u, u + 1, u + 1}
      (fun R =>
        letI : IsIso (toSpecΓ R) := StructureSheaf.isIso_to_global _
        asIso (toSpecΓ R))
      fun {X Y} f => by convert Spec_Γ_naturality (R := X) (S := Y) f

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru