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.
TODO #
- https://stacks.math.columbia.edu/tag/01S4 Show that this is equivalent to radicial morphisms (injective + purely inseparable residue field extensions)
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).
- universally_injective : (AlgebraicGeometry.topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) => Function.Injective x).universally f
Instances
theorem
AlgebraicGeometry.universallyInjective_iff
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
AlgebraicGeometry.UniversallyInjective f ↔ (AlgebraicGeometry.topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) =>
Function.Injective x).universally
f
theorem
AlgebraicGeometry.Scheme.Hom.injective
{X Y : AlgebraicGeometry.Scheme}
(f : X.Hom Y)
[AlgebraicGeometry.UniversallyInjective f]
:
Function.Injective ⇑f.base
theorem
AlgebraicGeometry.universallyInjective_eq :
@AlgebraicGeometry.UniversallyInjective = (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) =>
Function.Injective x).universally
@[instance 900]
instance
AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Equations
- ⋯ = ⋯