English
Formally, IsImmersion equals the infimum of IsPreimmersion and the topological IsLocallyClosed range property.
Русский
Формально IsImmersion равняется инфимному сочетанию IsPreimmersion и топологического свойства IsLocallyClosed на образ.
LaTeX
$$$\\text{IsImmersion} = \\big(\\text{IsPreimmersion} \\;\\land\\; \\text{IsLocallyClosed}(\\operatorname{range}(f))\\big)$$$
Lean4
/-- The diagonal morphism is always an immersion. -/
@[stacks 01KJ]
instance : IsImmersion (pullback.diagonal f) := by
let 𝒰 := Y.affineCover
let 𝒱 (i) := (pullback f (𝒰.f i)).affineCover
have H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤ :=
top_le_iff.mp fun _ _ ↦ range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ⟨_, rfl⟩
have := isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange f 𝒰 𝒱
have : IsImmersion ((pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱) ≫ Scheme.Opens.ι _) := inferInstance
rwa [morphismRestrict_ι, H, ← Scheme.topIso_hom,
MorphismProperty.cancel_left_of_respectsIso (P := @IsImmersion)] at this
