Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app

∀ {R S : CommRingCat} (f : R ⟶ S)
  (U : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace)ᵒᵖ),
  (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom.c.app U =
    CommRingCat.ofHom
      (AlgebraicGeometry.StructureSheaf.comap (CommRingCat.Hom.hom f) (Opposite.unop U)
        ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.topMap f)).obj (Opposite.unop U)) ⋯)

Defined in: Mathlib.AlgebraicGeometry.Spec
Cited by: 2 results in Mathlib
Foundations: Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites33

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

Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.Functor.objstatement · cited by 19,642
CategoryTheory.Functorstatement · cited by 16,252
Oppositestatement and proof · cited by 8,081
CategoryTheory.NatTrans.appstatement and proof · cited by 7,406
TopCat.carrierstatement and proof · cited by 3,184
CommRingCatstatement and proof · cited by 2,333
Opposite.unopstatement · cited by 2,231
TopologicalSpace.Opensstatement and proof · cited by 2,040
AlgebraicGeometry.PresheafedSpace.carrierstatement and proof · cited by 2,020
AlgebraicGeometry.SheafedSpace.toPresheafedSpacestatement and proof · cited by 1,988
CategoryTheory.ObjectProperty.FullSubcategory.objstatement · cited by 1,316

Cited by2

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Spec.sheafedSpaceMap_compproof · cited by 1
AlgebraicGeometry.stalkMap_toStalkproof · cited by 1