Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Spec.sheafedSpaceMap

{R S : CommRingCat} → (R ⟶ S) → (AlgebraicGeometry.Spec.sheafedSpaceObj S ⟶ AlgebraicGeometry.Spec.sheafedSpaceObj R)

The induced map of a ring homomorphism on the ring spectra, as a morphism of sheafed spaces.

Defined in
Mathlib.AlgebraicGeometry.Spec
Cited by
16 results in Mathlib
Foundations
Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AlgebraicGeometry.Spec.toSheafedSpace · cited by 9Spec.toSheafedSpaceAlgebraicGeometry.Spec.locallyRingedSpaceMap · cited by 7Spec.locallyRingedSpaceMapAlgebraicGeometry.localRingHom_comp_stalkIso · cited by 3AlgebraicGeometry.localRi…AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app · cited by 2Spec.sheafedSpaceMap_hom_…AlgebraicGeometry.Spec.locallyRingedSpaceMap_toHom · cited by 2Spec.locallyRingedSpaceMa…AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp · cited by 1StructureSheaf.toPushforw…AlgebraicGeometry.Spec.sheafedSpaceMap_comp · cited by 1Spec.sheafedSpaceMap_compAlgebraicGeometry.stalkMap_toStalk · cited by 1AlgebraicGeometry.stalkMa…AlgebraicGeometry.stalkMap_toStalk_apply · cited by 1AlgebraicGeometry.stalkMa…AlgebraicGeometry.Spec.sheafedSpaceMap_id · cited by 1Spec.sheafedSpaceMap_idAlgebraicGeometry.Spec.locallyRingedSpaceMap_comp · cited by 1Spec.locallyRingedSpaceMa…AlgebraicGeometry.LocallyRingedSpace.comp_ring_hom_ext · cited by 1LocallyRingedSpace.comp_r…AlgebraicGeometry.localRingHom_comp_stalkIso_apply · cited by 0AlgebraicGeometry.localRi…AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc · cited by 0StructureSheaf.toPushforw…AlgebraicGeometry.Spec.sheafedSpaceMap_hom_base · cited by 0Spec.sheafedSpaceMap_hom_…Quiver.Hom · cited by 32603Quiver.HomCategoryTheory.Functor.obj · cited by 19642Functor.objOpposite · cited by 8081OppositeTopCat.carrier · cited by 3184TopCat.carrierCommRingCat · cited by 2333CommRingCatOpposite.unop · cited by 2231Opposite.unopTopologicalSpace.Opens · cited by 2040TopologicalSpace.OpensAlgebraicGeometry.PresheafedSpace.carrier · cited by 2020PresheafedSpace.carrierAlgebraicGeometry.SheafedSpace.toPresheafedSpace · cited by 1988SheafedSpace.toPresheafed…TopologicalSpace.Opens.map · cited by 645Opens.mapCommRingCat.Hom.hom · cited by 432Hom.homCommRingCat.ofHom · cited by 259CommRingCat.ofHomAlgebraicGeometry.SheafedSpace · cited by 142AlgebraicGeometry.Sheafed…AlgebraicGeometry.Spec.sheafedSpaceObj · cited by 24Spec.sheafedSpaceObjAlgebraicGeometry.StructureSheaf.comap · cited by 15StructureSheaf.comapSpec.sheafedSpaceMapCITED BYCITES

Cites16

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

Cited by18

Results whose statement or proof uses this declaration.