Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_ofFromSpecStalk

∀ {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [inst : IrreducibleSpace ↥X]
  [inst_1 : AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↥X} [inst_2 : X.IsGermInjectiveAt x]
  (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y)
  (h : CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX),
  (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).fromSpecStalkOfMem ⋯ = φ

Defined in

Mathlib.AlgebraicGeometry.Birational.RationalMap

Cited by

1 results in Mathlib

Foundations

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

Assumes

IrreducibleSpaceAlgebraicGeometry.LocallyOfFiniteTypeAlgebraicGeometry.Scheme.IsGermInjectiveAt