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
fromCommRingᵒᵖ
toLocallyRingedSpace
.AlgebraicGeometry.ΓSpec.adjunction
: The adjunctionΓ ⊣ Spec
fromCommRingᵒᵖ
toScheme
.
The canonical map from the underlying set to the prime spectrum of Γ(X)
.
Equations
- X.toΓSpecFun x = (PrimeSpectrum.comap (X.presheaf.Γgerm x)) (LocalRing.closedPoint ↑(X.presheaf.stalk x))
Instances For
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).
toΓSpecFun
is continuous.
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 := ⋯ }
Instances For
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)
Instances For
The preimage is the basic open in X
defined by the same element 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
Instances For
r
is a unit as a section on the basic open defined by r
.
Define the sheaf hom on individual basic opens for the unit.
Equations
- X.toΓSpecCApp r = IsLocalization.Away.lift r ⋯
Instances For
Characterization of the sheaf hom on basic opens, direction ← (next lemma) is used at various places, but → is not used in this file.
The sheaf hom on all basic opens, commuting with restrictions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
The map on stalks induced by the unit commutes with maps from Γ(X)
to
stalks (in Spec Γ(X)
and in X
).
The canonical morphism from X
to the spectrum of its global sections.
Equations
- X.toΓSpec = { val := X.toΓSpecSheafedSpace, prop := ⋯ }
Instances For
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
.
toSpecΓ _
is an isomorphism so these are mutually two-sided inverses.
SpecΓIdentity
is iso so these are mutually two-sided inverses.
The adjunction Γ ⊣ Spec
from CommRingᵒᵖ
to LocallyRingedSpace
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The adjunction Γ ⊣ Spec
from CommRingᵒᵖ
to Scheme
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical map X ⟶ Spec Γ(X, ⊤)
. This is the unit of the Γ-Spec
adjunction.
Equations
- X.toSpecΓ = AlgebraicGeometry.ΓSpec.adjunction.unit.app X
Instances For
Alias of AlgebraicGeometry.Scheme.toSpecΓ_app_top
.
Alias of AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
.
Immediate consequences of the adjunction.
Spec preserves limits.
Equations
Equations
- AlgebraicGeometry.Spec.preservesLimits = AlgebraicGeometry.ΓSpec.adjunction.rightAdjointPreservesLimits
The functor Spec.toLocallyRingedSpace : CommRingCatᵒᵖ ⥤ LocallyRingedSpace
is fully faithful.
Equations
- AlgebraicGeometry.Spec.fullyFaithfulToLocallyRingedSpace = AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.fullyFaithfulROfIsIsoCounit
Instances For
Spec is a faithful functor.
The functor Spec : CommRingCatᵒᵖ ⥤ Scheme
is fully faithful.
Equations
- AlgebraicGeometry.Spec.fullyFaithful = AlgebraicGeometry.ΓSpec.adjunction.fullyFaithfulROfIsIsoCounit
Instances For
Spec is a full functor.
Equations
Spec is a faithful functor.
Equations
The preimage under Spec.
Equations
- AlgebraicGeometry.Spec.preimage f = (AlgebraicGeometry.Scheme.Spec.preimage f).unop
Instances For
Spec is fully faithful
Equations
- AlgebraicGeometry.Spec.homEquiv = { toFun := AlgebraicGeometry.Spec.preimage, invFun := AlgebraicGeometry.Spec.map, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
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).