∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.IsImmersion f ↔
    ∃ Z g₁ g₂,
      AlgebraicGeometry.IsOpenImmersion g₁ ∧
        AlgebraicGeometry.IsClosedImmersion g₂ ∧ CategoryTheory.CategoryStruct.comp g₁ g₂ = f