Adjunction between Γ and Spec

We define the adjunction ΓSpec.adjunction : Γ ⊣ Spec by defining the unit (toΓSpec, in multiple steps in this file) and counit (done in Spec.lean) and checking that they satisfy the left and right triangle identities. The constructions and proofs make use of maps and lemmas defined and proved in Mathlib/AlgebraicGeometry/StructureSheaf.lean extensively.

Notice that since the adjunction is between contravariant functors, you get to choose one of the two categories to have arrows reversed, and it is equally valid to present the adjunction as Spec ⊣ Γ (Spec.to_LocallyRingedSpace.right_op ⊣ Γ), in which case the unit and the counit would switch to each other.

Main definition

• AlgebraicGeometry.identityToΓSpec : The natural transformation 𝟭 _ ⟶ Γ ⋙ Spec.
• AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction : The adjunction Γ ⊣ Spec from CommRingᵒᵖ to LocallyRingedSpace.
• AlgebraicGeometry.ΓSpec.adjunction : The adjunction Γ ⊣ Spec from CommRingᵒᵖ to Scheme.

noncomputable def AlgebraicGeometry.LocallyRingedSpace.toΓSpecFun (X : LocallyRingedSpace) : ↑X.toTopCat → PrimeSpectrum ↑(Γ.obj (Opposite.op X))

The canonical map from the underlying set to the prime spectrum of Γ(X).

theorem AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) (x : ↑X.toTopCat) : r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.Γgerm x)) r)

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) : X.toΓSpecFun ⁻¹' ↑(PrimeSpectrum.basicOpen r) = ↑(X.toRingedSpace.basicOpen r)

The preimage of a basic open in Spec Γ(X) under the unit is the basic open in X defined by the same element (they are equal as sets).

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_continuous (X : LocallyRingedSpace) : Continuous X.toΓSpecFun

toΓSpecFun is continuous.

noncomputable def AlgebraicGeometry.LocallyRingedSpace.toΓSpecBase (X : LocallyRingedSpace) : X.toTopCat ⟶ Spec.topObj (Γ.obj (Opposite.op X))

The canonical (bundled) continuous map from the underlying topological space of X to the prime spectrum of its global sections.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) : TopologicalSpace.Opens ↑X.toTopCat

The preimage in X of a basic open in Spec Γ(X) (as an open set).

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) : X.toΓSpecMapBasicOpen r = X.toRingedSpace.basicOpen r

The preimage is the basic open in X defined by the same element r.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.LocallyRingedSpace.toToΓSpecMapBasicOpen (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) : X.presheaf.obj (Opposite.op ⊤) ⟶ X.presheaf.obj (Opposite.op (X.toΓSpecMapBasicOpen r))

The map from the global sections Γ(X) to the sections on the (preimage of) a basic open.

theorem AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpen (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) : IsUnit ((CategoryTheory.ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r)

r is a unit as a section on the basic open defined by r.

noncomputable def AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) : (Spec.structureSheaf ↑(Γ.obj (Opposite.op X))).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r)) ⟶ X.presheaf.obj (Opposite.op (X.toΓSpecMapBasicOpen r))

Define the sheaf hom on individual basic opens for the unit.

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) (f : (Spec.structureSheaf ↑(Γ.obj (Opposite.op X))).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r)) ⟶ X.presheaf.obj (Opposite.op (X.toΓSpecMapBasicOpen r))) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑(Γ.obj (Opposite.op X))) ((structureSheafInType ↑(Γ.obj (Opposite.op X)) ↑(Γ.obj (Opposite.op X))).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r))))) f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r

Characterization of the sheaf hom on basic opens, direction ← (next lemma) is used at various places, but → is not used in this file.

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑(Γ.obj (Opposite.op X))) ((structureSheafInType ↑(Γ.obj (Opposite.op X)) ↑(Γ.obj (Opposite.op X))).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r))))) (X.toΓSpecCApp r) = X.toToΓSpecMapBasicOpen r

noncomputable def AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens (X : LocallyRingedSpace) : (CategoryTheory.inducedFunctor PrimeSpectrum.basicOpen).op.comp (Spec.structureSheaf ↑(Γ.obj (Opposite.op X))).obj ⟶ (CategoryTheory.inducedFunctor PrimeSpectrum.basicOpen).op.comp ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj

The sheaf hom on all basic opens, commuting with restrictions.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app (X : LocallyRingedSpace) (r : (CategoryTheory.InducedCategory (TopologicalSpace.Opens (PrimeSpectrum ↑(Γ.obj (Opposite.op X)))) PrimeSpectrum.basicOpen)ᵒᵖ) : X.toΓSpecCBasicOpens.app r = X.toΓSpecCApp (Opposite.unop r)

noncomputable def AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace (X : LocallyRingedSpace) : X.toSheafedSpace ⟶ Spec.toSheafedSpace.obj (Opposite.op (Γ.obj (Opposite.op X)))

The canonical morphism of sheafed spaces from X to the spectrum of its global sections.

theorem AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal (X : LocallyRingedSpace) (a✝ : ↑X.toTopCat) : ↑((TopCat.Hom.hom X.toΓSpecSheafedSpace.hom.base) a✝).asIdeal = ⇑(CommRingCat.Hom.hom (X.presheaf.Γgerm a✝)) ⁻¹' ↑(IsLocalRing.closedPoint ↑(X.presheaf.stalk a✝)).asIdeal

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app (X : LocallyRingedSpace) (X✝ : (TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑(Γ.obj (Opposite.op X))))ᵒᵖ) : X.toΓSpecSheafedSpace.hom.c.app X✝ = CategoryTheory.yoneda.preimage ((CategoryTheory.Functor.IsCoverDense.sheafYonedaHom X.toΓSpecCBasicOpens).app X✝)

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) : X.toΓSpecSheafedSpace.hom.c.app (Opposite.op (PrimeSpectrum.basicOpen r)) = X.toΓSpecCApp r

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑(Γ.obj (Opposite.op X))) ((structureSheafInType ↑(Opposite.unop (Opposite.op (Γ.obj (Opposite.op X)))) ↑(Opposite.unop (Opposite.op (Γ.obj (Opposite.op X))))).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r))))) (X.toΓSpecSheafedSpace.hom.c.app (Opposite.op (PrimeSpectrum.basicOpen r))) = X.toToΓSpecMapBasicOpen r

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc (X : LocallyRingedSpace) (r : ↑(Γ.obj (Opposite.op X))) {Z : CommRingCat} (h : ((TopCat.Presheaf.pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).obj (Opposite.op (PrimeSpectrum.basicOpen r)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑(Γ.obj (Opposite.op X))) ((structureSheafInType ↑(Γ.obj (Opposite.op X)) ↑(Γ.obj (Opposite.op X))).obj.obj (Opposite.op (PrimeSpectrum.basicOpen r))))) (CategoryTheory.CategoryStruct.comp (X.toΓSpecSheafedSpace.hom.c.app (Opposite.op (PrimeSpectrum.basicOpen r))) h) = CategoryTheory.CategoryStruct.comp (X.toToΓSpecMapBasicOpen r) h

theorem AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec (X : LocallyRingedSpace) (x : ↑X.toTopCat) : CategoryTheory.CategoryStruct.comp (StructureSheaf.toStalk (↑(Opposite.unop (Opposite.op (Γ.obj (Opposite.op X))))) ((CategoryTheory.ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x)) (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) = X.presheaf.Γgerm x

The map on stalks induced by the unit commutes with maps from Γ(X) to stalks (in Spec Γ(X) and in X).

noncomputable def AlgebraicGeometry.LocallyRingedSpace.toΓSpec (X : LocallyRingedSpace) : X ⟶ Spec.locallyRingedSpaceObj (Γ.obj (Opposite.op X))

The canonical morphism from X to the spectrum of its global sections.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_base (X : LocallyRingedSpace) : X.toΓSpec.base = X.toΓSpecBase

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq {X : LocallyRingedSpace} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑(CategoryTheory.ConcreteCategory.hom X.toΓSpec.base) ⁻¹' PrimeSpectrum.zeroLocus s = X.toRingedSpace.zeroLocus s

On a locally ringed space X, the preimage of the zero locus of the prime spectrum of Γ(X, ⊤) under toΓSpec agrees with the associated zero locus on X.

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

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle (X : LocallyRingedSpace) : CategoryTheory.CategoryStruct.comp (toSpecΓ (Γ.obj (Opposite.op X))) (X.toΓSpec.c.app (Opposite.op ⊤)) = CategoryTheory.CategoryStruct.id (Γ.obj (Opposite.op X))

toSpecΓ _ is an isomorphism so these are mutually two-sided inverses.

noncomputable def AlgebraicGeometry.identityToΓSpec : CategoryTheory.Functor.id LocallyRingedSpace ⟶ LocallyRingedSpace.Γ.rightOp.comp Spec.toLocallyRingedSpace

The unit as a natural transformation.

theorem AlgebraicGeometry.ΓSpec.left_triangle (X : LocallyRingedSpace) : CategoryTheory.CategoryStruct.comp (LocallyRingedSpace.SpecΓIdentity.inv.app (LocallyRingedSpace.Γ.obj (Opposite.op X))) ((identityToΓSpec.app X).c.app (Opposite.op ⊤)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id CommRingCat).obj (LocallyRingedSpace.Γ.obj (Opposite.op X)))

theorem AlgebraicGeometry.ΓSpec.right_triangle (R : CommRingCat) : CategoryTheory.CategoryStruct.comp (identityToΓSpec.app (Spec.toLocallyRingedSpace.obj (Opposite.op R))) (Spec.toLocallyRingedSpace.map (LocallyRingedSpace.SpecΓIdentity.inv.app R).op) = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (Opposite.op R)))

SpecΓIdentity is iso so these are mutually two-sided inverses.

noncomputable def AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction : LocallyRingedSpace.Γ.rightOp ⊣ Spec.toLocallyRingedSpace

The adjunction Γ ⊣ Spec from CommRingᵒᵖ to LocallyRingedSpace.

@[simp]

theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_unit : locallyRingedSpaceAdjunction.unit = identityToΓSpec

@[simp]

theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit : locallyRingedSpaceAdjunction.counit = (CategoryTheory.NatIso.op LocallyRingedSpace.SpecΓIdentity).inv

theorem AlgebraicGeometry.ΓSpec.toSpecΓ_unop (R : CommRingCatᵒᵖ) : toSpecΓ (Opposite.unop R) = CommRingCat.ofHom (algebraMap (↑R.1) ((structureSheafInType ↑(Opposite.unop (Opposite.op (Opposite.unop R))) ↑(Opposite.unop (Opposite.op (Opposite.unop R)))).obj.obj (Opposite.op ⊤)))

@[simp]

theorem AlgebraicGeometry.ΓSpec.toSpecΓ_of (R : Type u) [CommRing R] : toSpecΓ (CommRingCat.of R) = CommRingCat.ofHom (algebraMap R ((structureSheafInType ↑(Opposite.unop (Opposite.op (CommRingCat.of R))) ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))).obj.obj (Opposite.op ⊤)))

@[simp]-normal form of locallyRingedSpaceAdjunction_counit_app'.

theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app (R : CommRingCatᵒᵖ) : locallyRingedSpaceAdjunction.counit.app R = (CommRingCat.ofHom (algebraMap (↑R.1) ((structureSheafInType ↑(Opposite.unop R) ↑(Opposite.unop R)).obj.obj (Opposite.op ⊤)))).op

theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app' (R : Type u) [CommRing R] : locallyRingedSpaceAdjunction.counit.app (Opposite.op (CommRingCat.of R)) = (CommRingCat.ofHom (algebraMap R ((structureSheafInType ↑(Opposite.unop (Opposite.op (CommRingCat.of R))) ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))).obj.obj (Opposite.op ⊤)))).op

theorem AlgebraicGeometry.ΓSpec.unop_locallyRingedSpaceAdjunction_counit_app' (R : Type u) [CommRing R] : (locallyRingedSpaceAdjunction.counit.app (Opposite.op (CommRingCat.of R))).unop = CommRingCat.ofHom (algebraMap R ((structureSheafInType ↑(Opposite.unop (Opposite.op (CommRingCat.of R))) ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))).obj.obj (Opposite.op ⊤)))

theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply {X : LocallyRingedSpace} {R : CommRingCatᵒᵖ} (f : LocallyRingedSpace.Γ.rightOp.obj X ⟶ R) : (locallyRingedSpaceAdjunction.homEquiv X R) f = CategoryTheory.CategoryStruct.comp (identityToΓSpec.app X) (Spec.locallyRingedSpaceMap f.unop)

theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply' {X : LocallyRingedSpace} {R : Type u} [CommRing R] (f : CommRingCat.of R ⟶ LocallyRingedSpace.Γ.obj (Opposite.op X)) : (locallyRingedSpaceAdjunction.homEquiv X (Opposite.op (CommRingCat.of R))) (Opposite.op f) = CategoryTheory.CategoryStruct.comp (identityToΓSpec.app X) (Spec.locallyRingedSpaceMap f)

theorem AlgebraicGeometry.ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app {X : LocallyRingedSpace} {R : Type u} [CommRing R] (f : LocallyRingedSpace.Γ.rightOp.obj X ⟶ Opposite.op (CommRingCat.of R)) (U : (TopologicalSpace.Opens ↑↑(Spec.toLocallyRingedSpace.obj (Opposite.op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap R ((structureSheafInType ↑(Opposite.unop (Opposite.op (CommRingCat.of R))) ↑(Opposite.unop (Opposite.op (CommRingCat.of R)))).obj.obj U))) (((locallyRingedSpaceAdjunction.homEquiv X (Opposite.op (CommRingCat.of R))) f).c.app U) = CategoryTheory.CategoryStruct.comp f.unop (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)

noncomputable def AlgebraicGeometry.ΓSpec.adjunction : Scheme.Γ.rightOp ⊣ Scheme.Spec

The adjunction Γ ⊣ Spec from CommRingᵒᵖ to Scheme.

theorem AlgebraicGeometry.ext_to_Spec {X : Scheme} {R : Type u_1} [CommRing R] {f g : X ⟶ Spec (CommRingCat.of R)} (h : CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (CommRingCat.of R)).inv (Scheme.Γ.map f.op) = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (CommRingCat.of R)).inv (Scheme.Γ.map g.op)) : f = g

Given f, g : X ⟶ Spec(R), if the two induced maps R ⟶ Γ(X) are equal, then f = g.

theorem AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply {X : Scheme} {R : CommRingCatᵒᵖ} (f : Opposite.op (Scheme.Γ.obj (Opposite.op X)) ⟶ R) : (adjunction.homEquiv X R) f = { toLRSHom' := (locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R) f }

theorem AlgebraicGeometry.ΓSpec.adjunction_homEquiv_symm_apply {X : Scheme} {R : CommRingCatᵒᵖ} (f : X ⟶ Scheme.Spec.obj R) : (adjunction.homEquiv X R).symm f = (locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R).symm (Scheme.Hom.toLRSHom f)

theorem AlgebraicGeometry.ΓSpec.adjunction_counit_app' {R : CommRingCatᵒᵖ} : adjunction.counit.app R = locallyRingedSpaceAdjunction.counit.app R

@[simp]

theorem AlgebraicGeometry.ΓSpec.adjunction_counit_app {R : CommRingCatᵒᵖ} : adjunction.counit.app R = (Scheme.ΓSpecIso (Opposite.unop R)).inv.op

noncomputable def AlgebraicGeometry.Scheme.toSpecΓ (X : Scheme) : X ⟶ Spec (X.presheaf.obj (Opposite.op ⊤))

The canonical map X ⟶ Spec Γ(X, ⊤). This is the unit of the Γ-Spec adjunction.

@[simp]

theorem AlgebraicGeometry.ΓSpec.adjunction_unit_app {X : Scheme} : adjunction.unit.app X = X.toSpecΓ

instance AlgebraicGeometry.ΓSpec.isIso_locallyRingedSpaceAdjunction_counit : CategoryTheory.IsIso locallyRingedSpaceAdjunction.counit

instance AlgebraicGeometry.ΓSpec.isIso_adjunction_counit : CategoryTheory.IsIso adjunction.counit

theorem AlgebraicGeometry.Scheme.toSpecΓ_apply (X : Scheme) (x : ↥X) : X.toSpecΓ x = (Spec.map (X.presheaf.Γgerm x)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))

@[deprecated AlgebraicGeometry.Scheme.toSpecΓ_apply (since := "2025-10-17")]

theorem AlgebraicGeometry.Scheme.toSpecΓ_base (X : Scheme) (x : ↥X) : X.toSpecΓ x = (Spec.map (X.presheaf.Γgerm x)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))

Alias of AlgebraicGeometry.Scheme.toSpecΓ_apply.

theorem AlgebraicGeometry.Scheme.toSpecΓ_naturality {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f Y.toSpecΓ = CategoryTheory.CategoryStruct.comp X.toSpecΓ (Spec.map (Hom.appTop f))

theorem AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (h : Spec (Y.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp Y.toSpecΓ h) = CategoryTheory.CategoryStruct.comp X.toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (Hom.appTop f)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.toSpecΓ_appTop (X : Scheme) : Hom.appTop X.toSpecΓ = (ΓSpecIso (X.presheaf.obj (Opposite.op ⊤))).hom

@[simp]

theorem AlgebraicGeometry.SpecMap_ΓSpecIso_hom (R : CommRingCat) : Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

@[simp]

theorem AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ (R : CommRingCat) : CategoryTheory.CategoryStruct.comp (Spec.map (Scheme.ΓSpecIso R).inv) (Spec R).toSpecΓ = CategoryTheory.CategoryStruct.id (Spec ((Spec R).presheaf.obj (Opposite.op ⊤)))

@[simp]

theorem AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc (R : CommRingCat) {Z : Scheme} (h : Spec ((Spec R).presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (Scheme.ΓSpecIso R).inv) (CategoryTheory.CategoryStruct.comp (Spec R).toSpecΓ h) = h

@[simp]

theorem AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv (R : CommRingCat) : CategoryTheory.CategoryStruct.comp (Spec R).toSpecΓ (Spec.map (Scheme.ΓSpecIso R).inv) = CategoryTheory.CategoryStruct.id (Spec R)

@[simp]

theorem AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc (R : CommRingCat) {Z : Scheme} (h : Spec R ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec R).toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (Scheme.ΓSpecIso R).inv) h) = h

theorem AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen (X : Scheme) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : (TopologicalSpace.Opens.map X.toSpecΓ.base).obj (PrimeSpectrum.basicOpen r) = X.basicOpen r

theorem AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv {X : Scheme} {B : CommRingCat} (φ : B ⟶ X.presheaf.obj (Opposite.op ⊤)) : CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso B).inv (Scheme.Hom.appTop ((ΓSpec.adjunction.homEquiv X (Opposite.op B)) φ.op)) = φ

theorem AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq {X : Scheme} {B : CommRingCat} (φ : B ⟶ X.presheaf.obj (Opposite.op ⊤)) : Scheme.Hom.appTop ((ΓSpec.adjunction.homEquiv X (Opposite.op B)) φ.op) = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso B).hom φ

theorem AlgebraicGeometry.ΓSpecIso_obj_hom {X : Scheme} (U : X.Opens) : (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom = CategoryTheory.CategoryStruct.comp (Scheme.Hom.appTop (Spec.map U.topIso.inv)) (CategoryTheory.CategoryStruct.comp (Scheme.Hom.appTop (↑U).toSpecΓ) U.topIso.hom)

Immediate consequences of the adjunction.

noncomputable def AlgebraicGeometry.Spec.fullyFaithfulToLocallyRingedSpace : toLocallyRingedSpace.FullyFaithful

The functor Spec.toLocallyRingedSpace : CommRingCatᵒᵖ ⥤ LocallyRingedSpace is fully faithful.

instance AlgebraicGeometry.instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace : Spec.toLocallyRingedSpace.Full

Spec is a full functor.

instance AlgebraicGeometry.instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace : Spec.toLocallyRingedSpace.Faithful

Spec is a faithful functor.

noncomputable def AlgebraicGeometry.Spec.fullyFaithful : Scheme.Spec.FullyFaithful

The functor Spec : CommRingCatᵒᵖ ⥤ Scheme is fully faithful.

instance AlgebraicGeometry.Spec.full : Scheme.Spec.Full

Spec is a full functor.

instance AlgebraicGeometry.Spec.faithful : Scheme.Spec.Faithful

Spec is a faithful functor.

theorem AlgebraicGeometry.Spec.map_inj {R S : CommRingCat} {φ ψ : R ⟶ S} : map φ = map ψ ↔ φ = ψ

theorem AlgebraicGeometry.Spec.map_injective {R S : CommRingCat} : Function.Injective map

@[simp]

theorem AlgebraicGeometry.Spec.map_eq_id {R : CommRingCat} {ϕ : R ⟶ R} : map ϕ = CategoryTheory.CategoryStruct.id (Spec R) ↔ ϕ = CategoryTheory.CategoryStruct.id R

noncomputable def AlgebraicGeometry.Spec.preimage {R S : CommRingCat} (f : Spec S ⟶ Spec R) : R ⟶ S

The preimage under Spec.

@[simp]

theorem AlgebraicGeometry.Spec.map_preimage {R S : CommRingCat} (f : Spec S ⟶ Spec R) : map (preimage f) = f

@[simp]

theorem AlgebraicGeometry.Spec.map_preimage_unop {R S : CommRingCat} (f : Spec R ⟶ Spec S) : map (fullyFaithful.preimage f).unop = f

@[simp]

theorem AlgebraicGeometry.Spec.preimage_map {R S : CommRingCat} (φ : R ⟶ S) : preimage (map φ) = φ

theorem AlgebraicGeometry.Spec.map_surjective {R S : CommRingCat} : Function.Surjective map

Useful for replacing f by Spec.map φ everywhere in proofs.

noncomputable def AlgebraicGeometry.Spec.homEquiv {R S : CommRingCat} : (Spec S ⟶ Spec R) ≃ (R ⟶ S)

Spec is fully faithful

@[simp]

theorem AlgebraicGeometry.Spec.homEquiv_apply {R S : CommRingCat} (f : Spec S ⟶ Spec R) : homEquiv f = preimage f

@[simp]

theorem AlgebraicGeometry.Spec.homEquiv_symm_apply {R S : CommRingCat} (f : R ⟶ S) : homEquiv.symm f = map f

@[simp]

theorem AlgebraicGeometry.Spec.preimage_id {R : CommRingCat} : preimage (CategoryTheory.CategoryStruct.id (Spec R)) = CategoryTheory.CategoryStruct.id R

@[simp]

theorem AlgebraicGeometry.Spec.preimage_comp {R S T : CommRingCat} (f : Spec R ⟶ Spec S) (g : Spec S ⟶ Spec T) : preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (preimage g) (preimage f)

theorem AlgebraicGeometry.Spec.preimage_comp_assoc {R S T : CommRingCat} (f : Spec R ⟶ Spec S) (g : Spec S ⟶ Spec T) {Z : CommRingCat} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (preimage (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (preimage g) (CategoryTheory.CategoryStruct.comp (preimage f) h)

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.instReflectiveLocallyRingedSpaceOppositeCommRingCatToLocallyRingedSpace : CategoryTheory.Reflective Spec.toLocallyRingedSpace

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Spec.reflective : CategoryTheory.Reflective Scheme.Spec

instance AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeLocallyRingedSpaceΓ : LocallyRingedSpace.Γ.IsRightAdjoint

instance AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeSchemeΓ : Scheme.Γ.IsRightAdjoint