feat(AlgebraicGeometry/Birational): composition of rational maps

[justus-springer]

Define composition of partial and rational maps.

• depends on: feat(AlgebraicGeometry/Restrict): a few more restriction lemmas #39442
• depends on: feat(Data/Set/Image): nonempty_preimage_iff #39443
• depends on: feat(AlgebraicGeometry/Birational): dominant rational maps #39317

---

[github-actions]

PR summary 35ec727d8d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.Birational.Dominant (new file)	2455
Mathlib.AlgebraicGeometry.Birational.Composition (new file)	2456

---

Declarations diff

+ IsDominant
+ PartialMap.id_comp
+ PartialMap.isDominant_hom_iff_isDominant_toRationalMap
+ PartialMap.isDominant_hom_of_isDominant_toRationalMap
+ PartialMap.isDominant_hom_of_toRationalMap_eq
+ PartialMap.isDominant_toRationalMap
+ PartialMap.toRationalMap_dominantRep_equiv
+ RationalMap.id
+ RationalMap.id_comp
+ RationalMap.id_compHom
+ Scheme.Hom.isoImage_hom_homOfLE
+ Scheme.Hom.isoImage_inv_homOfLE
+ Scheme.Opens.ι_isoImage_inv_ι
+ _root_.AlgebraicGeometry.Scheme.Hom.toPartialMap_compHom
+ compHom_id
+ comp_def
+ comp_equiv_of_equiv
+ comp_equiv_of_equiv_left
+ comp_equiv_of_equiv_right
+ comp_restrict_left
+ comp_restrict_right
+ comp_toPartialMap
+ dominantRep
+ equiv.refl
+ equiv.symm
+ equiv.trans
+ equiv_of_restrict_eq
+ exists_dominant_rep
+ id
+ id_compHom
+ instance (f : X ⟶ Y) [IsDominant f] : IsDominant f.toPartialMap.hom := by
+ instance (f : X ⤏ Y) [f.IsDominant] (g : Y ⤏ Z) [g.IsDominant] : (f.comp g).IsDominant := by
+ instance (f : X ⤏ Y) [f.IsDominant] : IsDominant f.dominantRep.hom
+ inv_preimage
+ isDominant_comp_hom
+ isDominant_hom_iff_isDominant_restrict_hom
+ isDominant_hom_iff_of_equiv
+ isDominant_hom_of_isDominant_restrict_hom
+ isDominant_restrict_hom
+ morphismRestrictRestrict_ι_isoImage_hom
+ morphismRestrict_eq_isoImage_hom_homOfLE
+ morphismRestrict_homOfLE
+ morphismRestrict_homOfLE_ι_isoImage_hom
+ morphismRestrict_ι_image_ι_isoImage_inv
+ nonempty_preimage_iff
+ toRationalMap_comp
+ toRationalMap_dominantRep
+ ι_isoImage_inv_morphismRestrict_homOfLE
++ comp
++ comp_assoc
++ comp_id

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(AlgebraicGeometry/Restrict): a few more restriction lemmas #39442
• feat(Data/Set/Image): nonempty_preimage_iff #39443
• feat(AlgebraicGeometry/Birational): dominant rational maps #39317
  By Dependent Issues (🤖). Happy coding!