Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc

∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] {x : ↥X} (f : X.presheaf.stalk x ⟶ R)
  [inst_1 : IsLocalHom (CommRingCat.Hom.hom f)] (U : X.Opens)
  (hU :
    (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x))
        (IsLocalRing.closedPoint ↑R) ∈
      U)
  {Z : CommRingCat} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (X.presheaf.germ U
        ((CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x))
          (IsLocalRing.closedPoint ↑R))
        hU)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.stalkClosedPointTo
          (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x)))
        h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x ⋯) (CategoryTheory.CategoryStruct.comp f h)

Defined in

Mathlib.AlgebraicGeometry.Stalk

Cited by

0 results in Mathlib

Foundations

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

Assumes

IsLocalRingIsLocalHom