[Merged by Bors] - feat(AlgebraicGeometry): basic properties of separated morphisms and schemes

[erdOne]

---

[github-actions]

PR summary c9c73b6ad9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Separated	1
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer	543

---

Declarations diff

+ IsAffineOpen.preimage
+ IsClosedImmersion.of_comp
+ IsSeparated
+ IsSeparated.comp_iff
+ IsSeparated.hasAffineProperty
+ IsSeparated.of_comp
+ inl_coprodIsoPushout_hom
+ inl_coprodIsoPushout_inv
+ inr_coprodIsoPushout_hom
+ inr_coprodIsoPushout_inv
+ instance (f g : X ⟶ Y) [Y.IsSeparated] : IsClosedImmersion (Limits.equalizer.ι f g)
+ instance (priority := 900) [X.IsSeparated] : IsSeparated f := by
+ instance (priority := 900) {X : Scheme.{u}} [IsAffine X] : X.IsSeparated := ⟨inferInstance⟩
+ instance [IsSeparated f] [IsSeparated g] : IsSeparated (f ≫ g)
+ instance [IsSeparated g] :
+ instance [X.IsSeparated] : IsClosedImmersion (prod.lift (𝟙 X) (𝟙 X)) := by
+ instance {S T : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T) [IsSeparated i] :
+ isPullback_equalizer_prod
+ isPushout_coequalizer_coprod
+ isSeparated_iff_isClosedImmersion_prod_lift
+ of_comp_isClosedImmersion
+ prodIsoPullback_hom_fst
+ prodIsoPullback_hom_snd
+ prodIsoPullback_inv_fst
+ prodIsoPullback_inv_snd
- instance {Z : Scheme.{u}} (g : Y ⟶ Z) [IsSeparated f] [IsSeparated g] : IsSeparated (f ≫ g)
- isAffineOpen.preimage
- of_comp

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.

[chrisflav]

Thanks, LGTM! I'll do a zulip-merge in a second :)

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style