Theorems · Theorem · algebraic geometry

AlgebraicGeometry.stalkMap_injective_of_isOpenMap_of_injective

∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f : X ⟶ Y} [CompactSpace ↥X],
  IsOpenMap ⇑f →
    Function.Injective ⇑f →
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) →
        ∀ (x : ↥X),
          Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))

If f : X ⟶ Y is open, injective, X is quasi-compact and Y is affine, then f is stalkwise injective if it is injective on global sections.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsAffineCompactSpace