Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk_comp

∀ {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),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).hom sY =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).domain.ι sX

Defined in

Mathlib.AlgebraicGeometry.Birational.RationalMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

IrreducibleSpaceAlgebraicGeometry.LocallyOfFiniteTypeAlgebraicGeometry.Scheme.IsGermInjectiveAt