feat: Valuative criterion for properness.

[erdOne]

---

[github-actions]

PR summary e7c90832e6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.ValuativeCriterion.ValuationRing Mathlib.ValuativeCriterion.Lemmas	1
Mathlib.ValuativeCriterion.PullbackCarrier	1730
Mathlib.ValuativeCriterion.Fiber	1731
Mathlib.ValuativeCriterion.Immersion	1732
Mathlib.ValuativeCriterion.UniversallyClosed	1760
Mathlib.ValuativeCriterion.ValuativeCriterion	1769

---

Declarations diff

+ Algebra.mem_ideal_map_adjoin
+ CommRingCat.hom_inv_apply
+ CommRingCat.inv_hom_apply
+ IsSeparated.valuativeCriterion
+ IsSeparated_eq_valuativeCriterion
+ LocalSubring
+ LocalSubring.localRing
+ LocalSubring.map
+ LocalSubring.of
+ LocalSubring.range
+ LocalSubring.range_eq_range
+ LocalSubring.range_toLocalSubring
+ PrimeSpectrum.isClosed_image_of_stableUnderSpecialization'
+ PrimeSpectrum.isClosed_range_of_stableUnderSpecialization
+ Scheme.Hom.fiber
+ Scheme.Hom.fiberToResidueField
+ Scheme.Hom.fiber_isPullback
+ Scheme.Hom.fiberι
+ Scheme.Hom.range_fiberι
+ SpecOfPoint
+ SpecTensorTo
+ SpecTensorTo_SpecOfPoint
+ Spec_map_base
+ Spec_map_tensorInl_fromSpecResidueField
+ Spec_map_tensor_isPullback
+ Spec_mem_basicOpen
+ Triplet
+ Triplet.Spec_ofPointTensor_SpecTensorTo
+ Triplet.exists_preimage
+ ValuationSubring.toLocalSubring
+ ValuationSubring.toLocalSubring_injective
+ ValuativeCommSq
+ ValuativeCriterion
+ ValuativeCriterion.Existence
+ ValuativeCriterion.Uniqueness
+ _root_.AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_apply
+ _root_.AlgebraicGeometry.universallyClosed_eq_valuativeCriterion
+ _root_.AlgebraicGeometry.universallyClosed_of_valuativeCriterion
+ _root_.CommRingCat.of_apply
+ _root_.RingHom.injective_respectsIso
+ _root_.RingHom.injective_stableUnderComposition
+ _root_.SpecializingMap.comp
+ aeval_ite_mem_vars
+ bijective_rangeRestrict_comp_of_valuationRing
+ carrierEquiv
+ carrierEquiv_eq_iff
+ carrierEquiv_symm_fst
+ carrierEquiv_symm_snd
+ compactSpace_iff_exists
+ compactSpace_of_universallyClosed
+ default_asIdeal
+ diagonalCover
+ diagonalCoverDiagonal
+ diagonalCoverDiagonal_eq_top_of_injective
+ diagonalCover_map
+ diagonalRestrictIsoDiagonal
+ domination_preserved_by_range
+ eq
+ exists_factor_valuationRing
+ exists_factor_valuationRing'
+ exists_factor_valuationRing'_is_base
+ exists_preimage_pullback
+ exists_valuationSubring_le
+ ext
+ instance (T : Triplet f g) : Nontrivial T.tensor
+ instance (priority := 900) [UniversallyClosed f] : QuasiCompact f
+ instance : CoeSort (LocalSubring K) (Type u) := ⟨fun s ↦ s.1⟩
+ instance : IsImmersion (pullback.diagonal f) := sorry
+ instance : Membership K (LocalSubring K) := ⟨fun x k ↦ k ∈ x.1⟩
+ instance : PartialOrder (LocalSubring K)
+ instance {A : CommRingCat} [Nontrivial A] : Nonempty (Spec A)
+ instance {K : Type*} [Ring K] (_ : LocalSubring K) : SetLike (LocalSubring K) K
+ instance {K} [Field K] : Unique (Spec (.of K))
+ instance {R : Type*} {S : Type*} [CommRing R] [CommRing S]
+ instance {R M N : Type*} [Field R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
+ isClosedImmersion_diagonal_of_injective
+ isClosedImmersion_diagonal_restrict
+ isClosedImmersion_diagonal_restrict_aux
+ isClosedMap_iff_specializingMap
+ isClosedMap_of_comp
+ isClosed_image_of_stableUnderSpecialization_of_isAffine
+ isCompact_iff_exists
+ isProperMap_of_universallyClosed
+ isPullback_Spec_map_isPushout
+ isPullback_Spec_map_pushout
+ isSeparated_of_valuativeCriterion
+ map_maximalIdeal_eq_top_of_mem_maximalLocalSubrings
+ map_to_injective_range
+ map_to_injective_range_comm
+ map_to_injective_range_retract
+ maximalLocalSubrings
+ mem_of_mem_maximalLocalSubrings_of_isIntegral
+ mk'
+ nontrivial_of_isPushout_of_isField
+ obivious
+ ofPoint
+ ofPointTensor
+ ofPointTensor_SpecTensorTo
+ ofPoint_SpecTensorTo
+ of_specializingMap
+ proper_eq_ValuativeCriterion
+ range_diagonal_subset_diagonalCoverDiagonal
+ range_fst
+ range_fst_comp
+ range_map
+ range_of_local_ring_is_itself
+ range_of_val_ring_is_itself
+ range_snd
+ range_snd_comp
+ residueFieldCongr_inv_residueFieldMap_ofPoint
+ specTensorTo_base_fst
+ specTensorTo_base_snd
+ specTensorTo_fst
+ specTensorTo_snd
+ specializingMap
+ specializingMap_isLocalAtTarget
+ specializingMap_respectsIso
+ stableUnderBaseChange
+ tensor
+ tensorCongr
+ tensorCongr_SpecTensorTo
+ tensorCongr_inv
+ tensorCongr_refl
+ tensorCongr_symm
+ tensorCongr_trans
+ tensorCongr_trans_hom
+ tensorInl
+ tensorInr
+ tensorProduct_nontrivial_of_isField
+ topislocal
+ universallyClosed_eq_universallySpecializing
+ universallyClosed_iff_specializingMap
+ val_ring_is_max
+ val_subriing_from_val_ring
+ val_subriing_from_val_ring_eq_local_subring_inclusion
+ valuativeCriterion_eq

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

[github-actions]

[lint-style] _{reported by reviewdog 🐶}

Suggested change

	x ⤳ LocalRing.closedPoint R := Inseparable.specializes <| congrArg nhds hx.is_cls_pt
	x ⤳ LocalRing.closedPoint R := Inseparable.specializes <| congrArg nhds hx.is_cls_pt

[github-actions]

[lint-style] _{reported by reviewdog 🐶}

Suggested change

	LocalRing.closedPoint R ⤳ x := Inseparable.specializes <| congrArg nhds hx.is_cls_pt.symm
	LocalRing.closedPoint R ⤳ x := Inseparable.specializes <| congrArg nhds hx.is_cls_pt.symm

[github-actions]

[lint-style] _{reported by reviewdog 🐶}

Suggested change

	(f : R →+* S) : LocalSubring S := LocalSubring.map f (LocalSubring.of ⊤)
	(f : R →+* S) : LocalSubring S := LocalSubring.map f (LocalSubring.of ⊤)

[github-actions]

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

	(f : R →+* S) : LocalSubring S := LocalSubring.map f (LocalSubring.of ⊤)
	(f : R →+* S) : LocalSubring S := LocalSubring.map f (LocalSubring.of ⊤)