Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.comp_ring_hom_ext

∀ {X : AlgebraicGeometry.LocallyRingedSpace} {R : CommRingCat}
  {f : R ⟶ AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)}
  {β : X ⟶ AlgebraicGeometry.Spec.locallyRingedSpaceObj R},
  CategoryTheory.CategoryStruct.comp X.toΓSpec.base (AlgebraicGeometry.Spec.locallyRingedSpaceMap f).base = β.base →
    (∀ (r : ↑R),
        CategoryTheory.CategoryStruct.comp f (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) =
          CategoryTheory.CategoryStruct.comp
            (CommRingCat.ofHom
              (algebraMap (↑R)
                ((AlgebraicGeometry.structureSheafInType ↑R ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r)))))
            (β.c.app (Opposite.op (PrimeSpectrum.basicOpen r)))) →
      CategoryTheory.CategoryStruct.comp X.toΓSpec (AlgebraicGeometry.Spec.locallyRingedSpaceMap f) = β

Defined in

Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Cited by

1 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound