Documentation

Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Universally injective morphism #

A morphism of schemes f : X ⟶ Y is universally injective if X ×[Y] Y' ⟶ Y' is injective for all base changes Y' ⟶ Y. This is equivalent to the diagonal morphism being surjective (AlgebraicGeometry.UniversallyInjective.iff_diagonal).

We show that being universally injective is local at the target, and is stable under compositions and base changes.

We also prove that universally injective is equivalent to being injective with purely inseparable residue field extensions (also known as a radical morphism), see AlgebraicGeometry.tfae_universallyInjective and Stacks tag 01S4.

source
class AlgebraicGeometry.UniversallyInjective {X Y : Scheme} (f : X ⟶ Y) :
Prop

A morphism of schemes f : X ⟶ Y is universally injective if the base change X ×[Y] Y' ⟶ Y' along any morphism Y' ⟶ Y is injective (on points).

Instances
    source
    theorem AlgebraicGeometry.universallyInjective_iff {X Y : Scheme} (f : X ⟶ Y) :
    UniversallyInjective f ↔ (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) => Function.Injective x).universally f
    source
    theorem AlgebraicGeometry.Scheme.Hom.injective {X Y : Scheme} (f : X ⟶ Y) [UniversallyInjective f] :
    Function.Injective ⇑f
    source
    theorem AlgebraicGeometry.universallyInjective_eq :
    @UniversallyInjective = (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) => Function.Injective x).universally
    source
    theorem AlgebraicGeometry.universallyInjective_eq_diagonal :
    @UniversallyInjective = CategoryTheory.MorphismProperty.diagonal @Surjective
    source
    theorem AlgebraicGeometry.UniversallyInjective.iff_diagonal {X Y : Scheme} (f : X ⟶ Y) :
    UniversallyInjective f ↔ Surjective (CategoryTheory.Limits.pullback.diagonal f)
    source
    @[instance 900]
    instance AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.Mono f] :
    UniversallyInjective f
    source
    theorem AlgebraicGeometry.UniversallyInjective.respectsIso :
    CategoryTheory.MorphismProperty.RespectsIso @UniversallyInjective
    source
    instance AlgebraicGeometry.UniversallyInjective.isStableUnderBaseChange :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @UniversallyInjective
    source
    instance AlgebraicGeometry.universallyInjective_isStableUnderComposition :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @UniversallyInjective
    source
    instance AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyInjective :
    CategoryTheory.MorphismProperty.IsMultiplicative @UniversallyInjective
    source
    instance AlgebraicGeometry.universallyInjective_isZariskiLocalAtTarget :
    IsZariskiLocalAtTarget @UniversallyInjective
    source
    theorem AlgebraicGeometry.tfae_universallyInjective {X Y : Scheme} (f : X ⟶ Y) :
    [UniversallyInjective f, ∀ (K : Type u) [inst : Field K], Function.Injective fun (g : Spec (CommRingCat.of K) ⟶ X) => CategoryTheory.CategoryStruct.comp g f, Function.Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable, Surjective (CategoryTheory.Limits.pullback.diagonal f)].TFAE

    Stacks Tag 01S4