[Merged by Bors] - feat(AlgebraicGeometry): define immersions

[erdOne]

---

[github-actions]

PR summary 6e583ac4ec

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.Morphisms.Immersion	1738

---

Declarations diff

+ IsImmersion
+ Scheme.Hom.coborderRange
+ Scheme.Hom.isClosedEmbedding
+ Scheme.Hom.isLocallyClosed_range
+ Scheme.Hom.liftCoborder
+ Scheme.Hom.liftCoborder_ι
+ comp
+ comp_iff
+ instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : IsImmersion f
+ instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : IsImmersion f
+ instance : IsLocalAtTarget @IsImmersion := by
+ instance : MorphismProperty.IsMultiplicative @IsImmersion
+ instance [IsImmersion f] : IsClosedImmersion f.liftCoborder := by
+ instance [IsImmersion f] : IsDominant f.coborderRange.ι := by
+ isImmersion_eq_inf
+ isImmersion_iff_exists
+ of_comp
+ stableUnderBaseChange

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[joelriou]

Otherwise, it looks very good to me!

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style