Theorems · Theorem · algebraic geometry

AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback

∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.SurjectiveOnStalks g],
  Topology.IsEmbedding fun x => ((CategoryTheory.Limits.pullback.fst f g) x, (CategoryTheory.Limits.pullback.snd f g) x)

If Y ⟶ S is surjective on stalks, then for every X ⟶ S, X ×ₛ Y is a subset of X × Y (Cartesian product as topological spaces) with the induced topology.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.SurjectiveOnStalks