English
A morphism is universally injective if and only if its diagonal morphism is surjective.
Русский
Морфизм является универсально инъективным тогда и только тогда, когда диагональная матрица (диагональная морфизм) сюрективна.
LaTeX
$$$\operatorname{UniversallyInjective}(f) \;\iff\; \text{diagonal}(f) \text{ surjective}. $$$
Lean4
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]
