Theorems · Theorem · algebraic geometry

AlgebraicGeometry.tfae_universallyInjective

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  [AlgebraicGeometry.UniversallyInjective f,
      ∀ (K : Type u) [inst : Field K], Function.Injective fun g => CategoryTheory.CategoryStruct.comp g f,
      Function.Injective ⇑f ∧
        ∀ (x : ↥X), (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable,
      AlgebraicGeometry.Surjective (CategoryTheory.Limits.pullback.diagonal f)].TFAE

[Stacks Tag 01S4](https://stacks.math.columbia.edu/tag/01S4)

Defined in

Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Cited by

0 results in Mathlib

Foundations

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