feat(AlgebraicGeometry): The sheaf of modules associated to a Weil divisor

[Raph-DG]

In this PR, we construct the sheaf of modules associated to a Weil divisor. Funnily enough, the definition does not actually require that the cycle is a Weil divisor, so in fact we construct a sheaf of modules associated to an arbitrary algebraic cycle. This isn't a particularly interesting definition outside of the case where the cycle is a Weil divisor as far as I can tell, but still I thought that was interesting.

• depends on: feat(AlgebraicGeometry): The Weil divisor associated to an element of the function field on a locally Noetherian integral scheme #38472
• depends on: feat(Topology): add variant of the sheaf condition which assumes non triviality of the cover #35868

---

[mathlib-merge-conflicts]

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

[github-actions]

PR summary c5b4e3d6f3

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
Mathlib.AlgebraicGeometry.AlgebraicCycle.Sheaf (new file)	2733

---

Declarations diff

+ AlgebraicCycle
+ ConnectedByCover
+ IsIntegralInCodimensionOne
+ IsIntegralInCodimensionOne.stalk_domain
+ IsPreconnected.transGen_of_iUnion
+ IsRegularInCodimensionOne
+ IsRegularInCodimensionOne.stalk_dvr
+ IsSheafUniqueGluingNontrivial
+ 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_.AlgebraicCycle.presheaf
+ _root_.AlgebraicGeometry.Scheme.Hom.degree
+ _root_.AlgebraicGeometry.Scheme.Hom.preimageSupportFinite
+ _root_.IsProperMap.preimageSupportFinite
+ addSubgroup
+ add_mem'
+ algebra_restrict
+ carrier
+ coe_add
+ coe_neg
+ coe_nsmul
+ coe_smul
+ coe_sub
+ coe_zero
+ coe_zsmul
+ coheightZeroSetOrderIsoIrreducibleComponents
+ coheight_zero_of_coheight_one_of_strictMono
+ connectedByCover_of_connected
+ 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
+ instModuleCarrier
+ instSubsingleTonOfEmpty
+ instance : Add (carrier D U)
+ instance : AddCommGroup (carrier D U)
+ instance : Neg (carrier D U)
+ instance : SMul Γ(X, U) (carrier D U)
+ instance : SMul ℕ (carrier D U)
+ instance : SMul ℤ (carrier D U)
+ instance : Sub (carrier D U)
+ instance : Zero (carrier D U)
+ instance [IrreducibleSpace X] {U V : X.Opens} (k : V ≤ U) [Nonempty V] :
+ instance {X : Scheme.{u}} [IsIntegral X] : IsIntegralInCodimensionOne X := ⟨inferInstance⟩
+ inter_preimageSupport_nonempty_finite
+ isSheaf
+ isSheafUniqueGluing_iff_isSheafUniqueGluingNontrivial_types
+ isSheaf_iff_isSheafUniqueGluingNontrivial
+ krullDimLE_of_coheight
+ mapAux
+ mapFun
+ mapFunApplyNonempty
+ mapFunProof
+ map_comp
+ map_homogeneous
+ map_locally_finite
+ memAddSubgroup
+ minimal_true_iff_isMin
+ mk_of_mem_subgroup
+ moduleResidueFieldExtension
+ neg_mem'
+ not_mem_of_ord_neq_one
+ obj
+ ord
+ ord_ne_zero
+ ord_of_isUnit
+ preimageSupport
+ preimageSupportFinite_id
+ presheaf.map_eq
+ presheaf.obj_eq
+ presheaf.obj_eq'
+ 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_subset
+ restrict_support_of_subset
+ restrict_support_subset
+ restrict_support_subset_inter
+ restrict_support_subset_support
+ restrict_univ
+ sections_equal_of_connected_by_cover
+ sections_equal_of_nonempty_intersection
+ sheaf
+ smulVal
+ smulVal_mem_carrier
+ smul_mem_nonempty
+ subtypeUnivOrderIso
+ zero_mem'
++ map
++ map_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): The Weil divisor associated to an element of the function field on a locally Noetherian integral scheme #38472
• feat(Topology): add variant of the sheaf condition which assumes non triviality of the cover #35868
  By Dependent Issues (🤖). Happy coding!