[Merged by Bors] - feat(AlgebraicGeometry): Define affine morphisms

[erdOne]

---

[github-actions]

PR summary 076dae1e7c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.Morphisms.Affine	1608

---

Declarations diff

+ IsAffineHom
+ affinePreimage
+ bijective
+ iSup_basicOpen_eq_top_iff
+ iSup_basicOpen_eq_top_iff'
+ iSup_basicOpen_of_span_eq_top
+ instance (priority := 100) isAffineHom_of_isAffine [IsAffine X] [IsAffine Y] : IsAffineHom f
+ instance (priority := 900) [IsAffineHom f] : QuasiCompact f
+ instance (priority := 900) [IsIso f] : IsAffineHom f
+ instance : HasAffineProperty @IsAffineHom fun X _ _ _ ↦ IsAffine X
+ instance : MorphismProperty.IsMultiplicative @IsAffineHom
+ instance [IsAffineHom f] [IsAffineHom g] : IsAffineHom (f ≫ g) := by
+ instance {X : Scheme} (r : Γ(X, ⊤)) :
+ isAffineHom_stableUnderBaseChange
+ isAffineOpen.preimage
+ isAffineOpen_of_isAffineOpen_basicOpen
+ isAffineOpen_of_isAffineOpen_basicOpen_aux
+ isAffine_of_isAffineHom
+ isAffine_of_isAffineOpen_basicOpen
+ isIso_ΓSpec_adjunction_unit_app_basicOpen

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>

[kbuzzard]

This looks great but it would be even better if we had a more detailed module docstring.

[joelriou]

Thanks!

bors merg

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style