Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.germ_stalkClosedPointTo

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

Defined in

Mathlib.AlgebraicGeometry.Stalk

Cited by

4 results in Mathlib

Foundations

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

Assumes

IsLocalRing