Factoring through immersions after a schematic cover #
A morphism factors through an immersion if it does so after precomposition with a surjective, scheme-theoretically dominant morphism. Surjectivity detects containment in the open part of the immersion; schematic dominance detects the equations of its closed part. No flatness or reducedness is required.
This allows equivariant morphisms to restrict to locally closed scheme-theoretic images, including images with nonreduced scheme structure.
The construction uses Mathlib's Scheme.Hom.liftCoborder, IsOpenImmersion.lift,
IsClosedImmersion.lift, and the ideal-sheaf formula Scheme.Hom.ker_comp.
theorem
AlgebraicGeometry.Scheme.Hom.existsUnique_lift_of_surjective_of_isSchemeTheoreticallyDominant
{W X Y Z : Scheme}
(i : Z ⟶ Y)
[IsImmersion i]
(g : X ⟶ Y)
(p : W ⟶ X)
[Surjective p]
[IsSchemeTheoreticallyDominant p]
(a : W ⟶ Z)
(h : CategoryTheory.CategoryStruct.comp a i = CategoryTheory.CategoryStruct.comp p g)
:
A factorization through an immersion exists uniquely if it exists after a surjective, scheme-theoretically dominant morphism.