feat(AlgebraicGeometry/Birational): dominant rational maps

[justus-springer]

Add a predicate RationalMap.IsDominant and add basic API. This is in preparation for defining composition of rational maps (see #39445). See also stacks#01RR.

• depends on: [Merged by Bors] - chore(AlgebraicGeometry/): create Birational subdirectory #39316
• depends on: feat(AlgebraicGeometry/Birational/RationalMap): add RationalMap.representative #39656

---

[github-actions]

PR summary 4a89d29c3f

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)	2456

---

Declarations diff

+ PartialMap.isDominant_toRationalMap
+ PartialMap.isDominant_toRationalMap_iff
+ PartialMap.representative_toRationalMap_equiv
+ RationalMap.IsDominant
+ RationalMap.isDominant_representative
+ RationalMap.representative
+ RationalMap.toRationalMap_representative
+ isDominant_hom_iff_isDominant_restrict_hom
+ isDominant_hom_iff_of_equiv
+ isDominant_hom_of_isDominant_restrict_hom
+ isDominant_restrict_hom

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:

• [Merged by Bors] - chore(AlgebraicGeometry/): create Birational subdirectory #39316
• feat(AlgebraicGeometry/Birational/RationalMap): add RationalMap.representative #39656
  By Dependent Issues (🤖). Happy coding!