Theorems · Theorem · algebraic geometry

AlgebraicGeometry.stalkMap_injective_of_isAffine

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y] (x : ↥X),
  (∀ (g : ↑(Y.presheaf.obj (Opposite.op ⊤))),
      (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
            ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g) =
          0 →
        (CategoryTheory.ConcreteCategory.hom (Y.presheaf.Γgerm (f x))) g = 0) →
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsAffine