feat(AlgebraicGeometry): universally injective morphisms (#18845)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

Mathlib.lean

@@ -933,6 +933,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.Separated
 import Mathlib.AlgebraicGeometry.Morphisms.Smooth
 import Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
 import Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
+import Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
 import Mathlib.AlgebraicGeometry.Noetherian
 import Mathlib.AlgebraicGeometry.OpenImmersion
 import Mathlib.AlgebraicGeometry.Over

Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean

@@ -42,4 +42,7 @@ instance : HasAffineProperty (isomorphisms Scheme) fun X _ f _ ↦ IsAffine X 
     (inferInstanceAs (IsIso (Spec.map (f.app ⊤)))),
     fun (_ : IsIso f) ↦ ⟨isAffine_of_isIso f, inferInstance⟩⟩
 
+instance : IsLocalAtTarget (monomorphisms Scheme) :=
+  diagonal_isomorphisms (C := Scheme).symm ▸ inferInstance
+
 end AlgebraicGeometry

Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

@@ -85,6 +85,14 @@ instance surjective_isLocalAtTarget : IsLocalAtTarget @Surjective := by
 
 end Surjective
 
+section Injective
+
+instance injective_isStableUnderComposition :
+    MorphismProperty.IsStableUnderComposition (topologically (Function.Injective ·)) where
+  comp_mem _ _ hf hg := hg.comp hf
+
+end Injective
+
 section IsOpenMap
 
 instance : (topologically IsOpenMap).RespectsIso :=

Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

@@ -67,6 +67,14 @@ instance universallyClosed_isStableUnderComposition :
   rw [universallyClosed_eq]
   infer_instance
 
+lemma UniversallyClosed.of_comp_surjective {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
+    [UniversallyClosed (f ≫ g)] [Surjective f] : UniversallyClosed g := by
+  constructor
+  intro X' Y' i₁ i₂ f' H
+  have := UniversallyClosed.out _ _ _ ((IsPullback.of_hasPullback i₁ f).paste_horiz H)
+  exact IsClosedMap.of_comp_surjective (MorphismProperty.pullback_fst (P := @Surjective) _ _ ‹_›).1
+    (Scheme.Hom.continuous _) this
+
 instance universallyClosedTypeComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
     [hf : UniversallyClosed f] [hg : UniversallyClosed g] : UniversallyClosed (f ≫ g) :=
   comp_mem _ _ _ hf hg

Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.AlgebraicGeometry.PullbackCarrier
+import Mathlib.Topology.LocalAtTarget
+
+/-!
+# 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)
+
+-/
+
+noncomputable section
+
+open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
+
+universe v u
+
+namespace AlgebraicGeometry
+
+variable {X Y : Scheme.{u}} (f : X ⟶ Y)
+
+open CategoryTheory.MorphismProperty Function
+
+/--
+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).
+-/
+@[mk_iff]
+class UniversallyInjective (f : X ⟶ Y) : Prop where
+  universally_injective : universally (topologically (Injective ·)) f
+
+theorem Scheme.Hom.injective (f : X.Hom Y) [UniversallyInjective f] :
+    Function.Injective f.base :=
+  UniversallyInjective.universally_injective _ _ _ .of_id_snd
+
+theorem universallyInjective_eq :
+    @UniversallyInjective = universally (topologically (Injective ·)) := by
+  ext X Y f; rw [universallyInjective_iff]
+
+theorem universallyInjective_eq_diagonal :
+    @UniversallyInjective = diagonal @Surjective := by
+  apply le_antisymm
+  · intro X Y f hf
+    refine ⟨fun x ↦ ⟨(pullback.fst f f).base x, hf.1 _ _ _ (IsPullback.of_hasPullback f f) ?_⟩⟩
+    rw [← Scheme.comp_base_apply, pullback.diagonal_fst]
+    rfl
+  · rw [← universally_eq_iff.mpr (inferInstanceAs (IsStableUnderBaseChange (diagonal @Surjective))),
+      universallyInjective_eq]
+    apply universally_mono
+    intro X Y f hf x₁ x₂ e
+    obtain ⟨t, ht₁, ht₂⟩ := Scheme.Pullback.exists_preimage_pullback _ _ e
+    obtain ⟨t, rfl⟩ := hf.1 t
+    rw [← ht₁, ← ht₂, ← Scheme.comp_base_apply, ← Scheme.comp_base_apply, pullback.diagonal_fst,
+      pullback.diagonal_snd]
+
+theorem UniversallyInjective.iff_diagonal :
+    UniversallyInjective f ↔ Surjective (pullback.diagonal f) := by
+  rw [universallyInjective_eq_diagonal]; rfl
+
+instance (priority := 900) [Mono f] : UniversallyInjective f :=
+  have := (pullback.isIso_diagonal_iff f).mpr inferInstance
+  (UniversallyInjective.iff_diagonal f).mpr inferInstance
+
+theorem UniversallyInjective.respectsIso : RespectsIso @UniversallyInjective :=
+  universallyInjective_eq_diagonal.symm ▸ inferInstance
+
+instance UniversallyInjective.isStableUnderBaseChange :
+    IsStableUnderBaseChange @UniversallyInjective :=
+  universallyInjective_eq_diagonal.symm ▸ inferInstance
+
+instance universallyInjective_isStableUnderComposition :
+    IsStableUnderComposition @UniversallyInjective :=
+  universallyInjective_eq ▸ inferInstance
+
+instance : MorphismProperty.IsMultiplicative @UniversallyInjective where
+  id_mem _ := inferInstance
+
+instance universallyInjective_isLocalAtTarget : IsLocalAtTarget @UniversallyInjective :=
+  universallyInjective_eq_diagonal.symm ▸ inferInstance
+
+end AlgebraicGeometry

Mathlib/AlgebraicGeometry/PullbackCarrier.lean

@@ -359,4 +359,10 @@ instance isJointlySurjectivePreserving (P : MorphismProperty Scheme.{u}) :
     obtain ⟨a, b, h⟩ := Pullback.exists_preimage_pullback x y hxy
     use a
 
+instance : MorphismProperty.IsStableUnderBaseChange @Surjective := by
+  refine .mk' ?_
+  introv hg
+  simp only [surjective_iff, ← Set.range_eq_univ, Pullback.range_fst] at hg ⊢
+  rw [hg, Set.preimage_univ]
+
 end AlgebraicGeometry.Scheme

Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean

@@ -60,6 +60,10 @@ instance [Mono f] : IsIso (diagonal f) := by
   rw [(IsIso.inv_eq_of_inv_hom_id (diagonal_fst f)).symm]
   infer_instance
 
+lemma isIso_diagonal_iff : IsIso (diagonal f) ↔ Mono f :=
+  ⟨fun H ↦ ⟨fun _ _ e ↦ by rw [← lift_fst _ _ e, (cancel_epi (g := fst f f) (h := snd f f)
+    (diagonal f)).mp (by simp), lift_snd]⟩, fun _ ↦ inferInstance⟩
+
 /-- The two projections `Δ_{X/Y} ⟶ X` form a kernel pair for `f : X ⟶ Y`. -/
 theorem diagonal_isKernelPair : IsKernelPair f (pullback.fst f f) (pullback.snd f f) :=
   IsPullback.of_hasPullback f f

Mathlib/CategoryTheory/MorphismProperty/Limits.lean

@@ -61,6 +61,13 @@ theorem IsStableUnderBaseChange.mk' {P : MorphismProperty C} [RespectsIso P]
     rw [← P.cancel_left_of_respectsIso e.inv, sq.flip.isoPullback_inv_fst]
     exact hP₂ _ _ _ f g hg
 
+instance IsStableUnderBaseChange.isomorphisms :
+    (isomorphisms C).IsStableUnderBaseChange where
+  of_isPullback {_ _ _ _ f g _ _} h hg :=
+    have : IsIso g := hg
+    have := hasPullback_of_left_iso g f
+    h.isoPullback_hom_snd ▸ inferInstanceAs (IsIso _)
+
 variable (C) in
 instance IsStableUnderBaseChange.monomorphisms :
     (monomorphisms C).IsStableUnderBaseChange where
@@ -296,6 +303,9 @@ instance IsStableUnderBaseChange.diagonal [IsStableUnderBaseChange P] [P.Respect
         P.cancel_right_of_respectsIso]
       exact P.baseChange_map f _ (by simpa))
 
+lemma diagonal_isomorphisms : (isomorphisms C).diagonal = monomorphisms C :=
+  ext _ _ fun _ _ _ ↦ pullback.isIso_diagonal_iff _
+
 end Diagonal
 
 section Universally

Mathlib/Topology/Maps/Basic.lean

@@ -461,6 +461,12 @@ protected theorem comp (hg : IsClosedMap g) (hf : IsClosedMap f) : IsClosedMap (
   rw [image_comp]
   exact hg _ (hf _ hs)
 
+protected theorem of_comp_surjective (hf : Surjective f) (hf' : Continuous f)
+    (hfg : IsClosedMap (g ∘ f)) : IsClosedMap g := by
+  intro K hK
+  rw [← image_preimage_eq K hf, ← image_comp]
+  exact hfg _ (hK.preimage hf')
+
 theorem closure_image_subset (hf : IsClosedMap f) (s : Set X) :
     closure (f '' s) ⊆ f '' closure s :=
   closure_minimal (image_subset _ subset_closure) (hf _ isClosed_closure)