Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Spec.structureSheaf

(R : Type u) → [inst : CommRing R] → TopCat.Sheaf CommRingCat (AlgebraicGeometry.PrimeSpectrum.Top R)

The structure sheaf on $Spec R$, valued in CommRingCat. This is provided as a bundled SheafedSpace as Spec.SheafedSpace R later.

Defined in
Mathlib.AlgebraicGeometry.StructureSheaf
Cited by
57 results in Mathlib
Foundations
Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.Spec.sheafedSpaceObj · cited by 24Spec.sheafedSpaceObjAlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen · cited by 18IsAffineOpen.isLocalizati…AlgebraicGeometry.StructureSheaf.comap · cited by 15StructureSheaf.comapAlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace · cited by 8LocallyRingedSpace.toΓSpe…AlgebraicGeometry.StructureSheaf.comap_apply · cited by 5StructureSheaf.comap_applyAlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp · cited by 4LocallyRingedSpace.toΓSpe…AlgebraicGeometry.StructureSheaf.toOpen_comp_comap · cited by 3StructureSheaf.toOpen_com…AlgebraicGeometry.StructureSheaf.toPushforwardStalk · cited by 3StructureSheaf.toPushforw…AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens · cited by 3LocallyRingedSpace.toΓSpe…AlgebraicGeometry.StructureSheaf.algebraMap_self_map · cited by 2StructureSheaf.algebraMap…AlgebraicGeometry.StructureSheaf.comap_id · cited by 2StructureSheaf.comap_idAlgebraicGeometry.StructureSheaf.globalSectionsIso · cited by 2StructureSheaf.globalSect…AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' · cited by 2IsAffineOpen.isLocalizati…AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc · cited by 2StructureSheaf.toOpen_com…AlgebraicGeometry.StructureSheaf.toPushforwardStalkAlgHom · cited by 2StructureSheaf.toPushforw…CommRing · cited by 17173CommRingCommRingCat · cited by 2333CommRingCatAlgebraicGeometry.PrimeSpectrum.Top · cited by 104PrimeSpectrum.TopTopCat.Sheaf · cited by 73TopCat.SheafAlgebraicGeometry.structurePresheafInCommRingCat · cited by 23AlgebraicGeometry.structu…Spec.structureSheafCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by67

Results whose statement or proof uses this declaration.