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 structure_sheaf.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.

def AlgebraicGeometry.LocallyRingedSpace.ΓToStalk (X : AlgebraicGeometry.LocallyRingedSpace) (x : ↑X.toTopCat) : AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X) ⟶ X.presheaf.stalk x

The map from the global sections to a stalk.

Equations

• X.ΓToStalk x = X.presheaf.germ ⟨x, trivial⟩

theorem AlgebraicGeometry.LocallyRingedSpace.ΓToStalk_stalkMap {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : CategoryTheory.CategoryStruct.comp (Y.ΓToStalk (f.val.base x)) (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x) = CategoryTheory.CategoryStruct.comp (f.val.c.app (Opposite.op ⊤)) (X.ΓToStalk x)

theorem AlgebraicGeometry.LocallyRingedSpace.ΓToStalk_stalkMap_apply {X : AlgebraicGeometry.LocallyRingedSpace} {Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) (a : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (AlgebraicGeometry.PresheafedSpace.stalkMap f.val x) ((Y.ΓToStalk (f.val.base x)) a) = (X.ΓToStalk x) ((f.val.c.app (Opposite.op ⊤)) a)

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

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

Equations

• X.toΓSpecFun x = (PrimeSpectrum.comap (X.ΓToStalk x)) (LocalRing.closedPoint ↑(X.presheaf.stalk x))

theorem AlgebraicGeometry.LocallyRingedSpace.not_mem_prime_iff_unit_in_stalk (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (x : ↑X.toTopCat) : r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit ((X.ΓToStalk x) r)

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

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 : AlgebraicGeometry.LocallyRingedSpace) : Continuous X.toΓSpecFun

toΓSpecFun is continuous.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecBase_apply (X : AlgebraicGeometry.LocallyRingedSpace) : ∀ (a : ↑X.toTopCat), X.toΓSpecBase a = X.toΓSpecFun a

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

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

Equations

• X.toΓSpecBase = { toFun := X.toΓSpecFun, continuous_toFun := ⋯ }

@[reducible, inline]

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

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

Equations

• X.toΓSpecMapBasicOpen r = (TopologicalSpace.Opens.map X.toΓSpecBase).obj (PrimeSpectrum.basicOpen r)

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.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]

abbrev AlgebraicGeometry.LocallyRingedSpace.toToΓSpecMapBasicOpen (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.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.

Equations

• X.toToΓSpecMapBasicOpen r = X.presheaf.map (X.toΓSpecMapBasicOpen r).leTop.op

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

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

def AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) : (AlgebraicGeometry.Spec.structureSheaf ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).val.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.

Equations

• X.toΓSpecCApp r = IsLocalization.Away.lift r ⋯

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (f : (AlgebraicGeometry.Spec.structureSheaf ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).val.obj (Opposite.op (PrimeSpectrum.basicOpen r)) ⟶ X.presheaf.obj (Opposite.op (X.toΓSpecMapBasicOpen r))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (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 : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (PrimeSpectrum.basicOpen r)) (X.toΓSpecCApp r) = X.toToΓSpecMapBasicOpen r

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_base (X : AlgebraicGeometry.LocallyRingedSpace) : X.toΓSpecSheafedSpace.base = X.toΓSpecBase

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_c (X : AlgebraicGeometry.LocallyRingedSpace) : X.toΓSpecSheafedSpace.c = (TopCat.Sheaf.restrictHomEquivHom (AlgebraicGeometry.Spec.structureSheaf ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).val ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪) ⋯) X.toΓSpecCBasicOpens

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) (PrimeSpectrum.basicOpen r)) (X.toΓSpecSheafedSpace.c.app (Opposite.op (PrimeSpectrum.basicOpen r))) = X.toToΓSpecMapBasicOpen r

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

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

@[simp]

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

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

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

Equations

• X.toΓSpec = { val := X.toΓSpecSheafedSpace, prop := ⋯ }

theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq {X : AlgebraicGeometry.LocallyRingedSpace} (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))) : ⇑X.toΓSpec.val.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 : AlgebraicGeometry.LocallyRingedSpace} {R : CommRingCat} {f : R ⟶ AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)} {β : X ⟶ AlgebraicGeometry.Spec.locallyRingedSpaceObj R} (w : CategoryTheory.CategoryStruct.comp X.toΓSpec.val.base (AlgebraicGeometry.Spec.locallyRingedSpaceMap f).val.base = β.val.base) (h : ∀ (r : ↑R), CategoryTheory.CategoryStruct.comp f (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑R) (PrimeSpectrum.basicOpen r)) (β.val.c.app (Opposite.op (PrimeSpectrum.basicOpen r)))) : CategoryTheory.CategoryStruct.comp X.toΓSpec (AlgebraicGeometry.Spec.locallyRingedSpaceMap f) = β

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

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

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

The unit as a natural transformation.

Equations

• AlgebraicGeometry.identityToΓSpec = { app := AlgebraicGeometry.LocallyRingedSpace.toΓSpec, naturality := AlgebraicGeometry.identityToΓSpec.proof_1 }

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

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

@[simp]

theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app (R : CommRingCatᵒᵖ) : AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit.app R = (AlgebraicGeometry.StructureSheaf.toOpen ↑(Opposite.unop R) ⊤).op

@[simp]

theorem AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit_app' (R : Type u) [CommRing R] : AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit.app (Opposite.op (CommRingCat.of R)) = (AlgebraicGeometry.StructureSheaf.toOpen R ⊤).op

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

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

theorem AlgebraicGeometry.ΓSpec.adjunction_homEquiv (X : AlgebraicGeometry.Scheme) (R : CommRingCatᵒᵖ) : AlgebraicGeometry.ΓSpec.adjunction.homEquiv X R = AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R

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

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

@[simp]

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

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

@[simp]

theorem AlgebraicGeometry.ΓSpec.adjunction_unit_naturality_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Scheme.Spec.obj (AlgebraicGeometry.Scheme.Γ.rightOp.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ΓSpec.adjunction.unit.app Y) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ΓSpec.adjunction.unit.app X) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.app f ⊤)) h)

@[simp]

theorem AlgebraicGeometry.ΓSpec.adjunction_unit_naturality {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.ΓSpec.adjunction.unit.app Y) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ΓSpec.adjunction.unit.app X) (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.app f ⊤))

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

Equations

• AlgebraicGeometry.ΓSpec.isIso_locallyRingedSpaceAdjunction_counit = ⋯

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

Equations

• AlgebraicGeometry.ΓSpec.isIso_adjunction_counit = ⋯

@[simp]

theorem AlgebraicGeometry.ΓSpec.adjunction_unit_app_app_top (X : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.ΓSpec.adjunction.unit.app X) ⊤ = (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op ⊤))).hom

@[simp]

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

theorem AlgebraicGeometry.ΓSpec.adjunction_unit_map_basicOpen (X : AlgebraicGeometry.Scheme) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : (TopologicalSpace.Opens.map (AlgebraicGeometry.ΓSpec.adjunction.unit.app X).val.base).obj (PrimeSpectrum.basicOpen r) = X.basicOpen r

theorem AlgebraicGeometry.ΓSpec.toOpen_unit_app_val_c_app {X : AlgebraicGeometry.Scheme} (U : (TopologicalSpace.Opens ↑↑((AlgebraicGeometry.Scheme.Γ.rightOp.comp AlgebraicGeometry.Scheme.Spec).obj X).toPresheafedSpace)ᵒᵖ) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(Opposite.unop (AlgebraicGeometry.Scheme.Γ.rightOp.obj X))) (Opposite.unop U)) ((AlgebraicGeometry.ΓSpec.adjunction.unit.app X).val.c.app U) = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

@[simp]

theorem AlgebraicGeometry.ΓSpec.toOpen_unit_app_val_c_app'_assoc {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens (PrimeSpectrum ↑(X.presheaf.obj (Opposite.op ⊤)))) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (AlgebraicGeometry.ΓSpec.adjunction.unit.app X).val.base).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(X.presheaf.obj (Opposite.op ⊤))) U) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.ΓSpec.adjunction.unit.app X) U) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) h

@[simp]

theorem AlgebraicGeometry.ΓSpec.toOpen_unit_app_val_c_app' {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens (PrimeSpectrum ↑(X.presheaf.obj (Opposite.op ⊤)))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (↑(X.presheaf.obj (Opposite.op ⊤))) U) (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.ΓSpec.adjunction.unit.app X) U) = X.presheaf.map (CategoryTheory.homOfLE ⋯).op

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

Immediate consequences of the adjunction.

instance AlgebraicGeometry.instPreservesLimitsOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace : CategoryTheory.Limits.PreservesLimits AlgebraicGeometry.Spec.toLocallyRingedSpace

Spec preserves limits.

Equations

• AlgebraicGeometry.instPreservesLimitsOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace = AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.rightAdjointPreservesLimits

instance AlgebraicGeometry.Spec.preservesLimits : CategoryTheory.Limits.PreservesLimits AlgebraicGeometry.Scheme.Spec

Equations

• AlgebraicGeometry.Spec.preservesLimits = AlgebraicGeometry.ΓSpec.adjunction.rightAdjointPreservesLimits

def AlgebraicGeometry.Spec.fullyFaithfulToLocallyRingedSpace : AlgebraicGeometry.Spec.toLocallyRingedSpace.FullyFaithful

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

Equations

• AlgebraicGeometry.Spec.fullyFaithfulToLocallyRingedSpace = AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.fullyFaithfulROfIsIsoCounit

instance AlgebraicGeometry.instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace : AlgebraicGeometry.Spec.toLocallyRingedSpace.Full

Spec is a full functor.

Equations

• AlgebraicGeometry.instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace = ⋯

instance AlgebraicGeometry.instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace : AlgebraicGeometry.Spec.toLocallyRingedSpace.Faithful

Spec is a faithful functor.

Equations

• AlgebraicGeometry.instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace = ⋯

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

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

Equations

• AlgebraicGeometry.Spec.fullyFaithful = AlgebraicGeometry.ΓSpec.adjunction.fullyFaithfulROfIsIsoCounit

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

Spec is a full functor.

Equations

• AlgebraicGeometry.Spec.full = ⋯

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

Spec is a faithful functor.

Equations

• AlgebraicGeometry.Spec.faithful = ⋯

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

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

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

The preimage under Spec.

Equations

• AlgebraicGeometry.Spec.preimage f = (AlgebraicGeometry.Scheme.Spec.preimage f).unop

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Spec is fully faithful

Equations

• AlgebraicGeometry.Spec.homEquiv = { toFun := AlgebraicGeometry.Spec.preimage, invFun := AlgebraicGeometry.Spec.map, left_inv := ⋯, right_inv := ⋯ }

instance AlgebraicGeometry.instIsRightAdjointLocallyRingedSpaceOppositeCommRingCatToLocallyRingedSpace : AlgebraicGeometry.Spec.toLocallyRingedSpace.IsRightAdjoint

Equations

• AlgebraicGeometry.instIsRightAdjointLocallyRingedSpaceOppositeCommRingCatToLocallyRingedSpace = ⋯

instance AlgebraicGeometry.instIsRightAdjointSchemeOppositeCommRingCatSpec : AlgebraicGeometry.Scheme.Spec.IsRightAdjoint

Equations

• AlgebraicGeometry.instIsRightAdjointSchemeOppositeCommRingCatSpec = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• AlgebraicGeometry.Spec.reflective = CategoryTheory.Reflective.mk AlgebraicGeometry.Scheme.Γ.rightOp AlgebraicGeometry.ΓSpec.adjunction

@[deprecated AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq]

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

Alias of AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq.

---

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).