feat(AlgebraicGeometry): The Weil divisor associated to an element of the function field on a locally Noetherian integral scheme

[Raph-DG]

In this PR we define and provide some basic API for principal Weil divisors, i.e. the Weil divisor associated to an element of the function field of a locally noetherian, integral scheme.

• depends on: feat(AlgebraicGeometry): Order of vanishing of elements of the function field of locally noetherian, integral schemes #29774
• depends on: [Merged by Bors] - feat(Topology): intersections preserve Notherian-ness and Quasisober-ness #37985
• depends on: feat(AlgebraicGeometry): Define algebraic cycles #37901
• depends on: feat(Topology): Relating irreducible components of a space to codimension one points in non dense subsets #38002

---

[github-actions]

PR summary 978a56a406

Import changes exceeding 2%

%	File
+15.21%	Mathlib.Topology.Sober

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Sober	710	818	+108 (+15.21%)

Import changes for all files

Files	Import difference
Mathlib.Topology.KrullDimension	1
Mathlib.Topology.Spectral.ConstructibleTopology	7
Mathlib.Topology.Spectral.Basic	92
Mathlib.Topology.Sober	108
Mathlib.Topology.LocallyFinsupp.Pushforward (new file)	936
Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic (new file)	2337
Mathlib.AlgebraicGeometry.OrderOfVanishing (new file)	2642
Mathlib.AlgebraicGeometry.AlgebraicCycle.Principal (new file)	2650

---

Declarations diff

+ AlgebraicCycle
+ PreimageSupportFinite
+ QuasiSober.coheight_eq_zero_subset_of_coheight_eq_one
+ QuasiSober.val_lt_genericPoint_of_closure_ne_top
+ QuasiSober.withTopLift
+ QuasiSober.withTopLift_strictMono
+ Scheme.germToFunctionField_eq_algebraMap_germ
+ Scheme.germToFunctionField_map
+ Specializes.strictMono_val
+ TopologicalSpace.NoetherianSpace.finite_coheight_one_of_closure_ne_univ
+ _root_.AlgebraicGeometry.Scheme.Hom.degree
+ _root_.AlgebraicGeometry.Scheme.Hom.preimageSupportFinite
+ _root_.IsProperMap.preimageSupportFinite
+ coheightZeroSetOrderIsoIrreducibleComponents
+ coheight_zero_of_coheight_one_of_strictMono
+ div
+ div_eq_ord_of_coheight_eq_one
+ div_eq_zero_of_coheight_ne_one
+ div_eq_zero_of_isUnit
+ div_eq_zero_of_isUnit_top
+ div_locally_finite
+ div_mul
+ div_neg
+ div_support
+ exists_isUnit_germ_eq
+ homgeneous_ext
+ homogeneous_le_iff
+ inter_preimageSupport_nonempty_finite
+ krullDimLE_of_coheight
+ map
+ mapAux
+ map_homogeneous
+ map_id
+ map_locally_finite
+ minimal_true_iff_isMin
+ moduleResidueFieldExtension
+ not_mem_of_ord_neq_one
+ ord
+ ord_ne_zero
+ ord_of_isUnit
+ preimageSupport
+ preimageSupportFinite_id
+ pushforward
+ restrict
+ restrict_apply
+ restrict_eqOn
+ restrict_eqOn_compl
+ restrict_eq_of_mem
+ restrict_eq_zero_of_eq_zero
+ restrict_eq_zero_of_not_mem
+ restrict_support_of_subset
+ restrict_support_subset
+ restrict_support_subset_inter
+ restrict_support_subset_support
+ restrict_univ
+ subtypeUnivOrderIso

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): Order of vanishing of elements of the function field of locally noetherian, integral schemes #29774
• [Merged by Bors] - feat(Topology): intersections preserve Notherian-ness and Quasisober-ness #37985
• feat(AlgebraicGeometry): Define algebraic cycles #37901
• feat(Topology): Relating irreducible components of a space to codimension one points in non dense subsets #38002
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.