Theorems · Theorem · algebraic geometry

AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc

∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat) {Z : CommRingCat}
  (h : Y.presheaf.stalk y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom ((CategoryTheory.ConcreteCategory.hom e.inv.base) y))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv y) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) h

Defined in

Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Cited by

0 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound