Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc

∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X)
  (U : X.Opens) (hU : f (IsLocalRing.closedPoint ↑R) ∈ U) {Z : CommRingCat} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ U (f (IsLocalRing.closedPoint ↑R)) hU)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.stalkClosedPointTo f) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.mapIso (AlgebraicGeometry.Spec R).presheaf (CategoryTheory.eqToIso ⋯).op ≪≫
            AlgebraicGeometry.Scheme.ΓSpecIso R).hom
        h)

Defined in

Mathlib.AlgebraicGeometry.Stalk

Cited by

0 results in Mathlib

Foundations

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

Assumes

IsLocalRing