feat(RingTheory): existence of coefficient ring

[Thmoas-Guan]

In this PR, we prove the existence of coefficient ring by the following two cases:
1: for residue field with char zero, there is a section of the residue field
2: for positive char, there exists a Cohen ring

---

• depends on: feat(RingTheory): regular local ring is domain #28683
• depends on: feat(RingTheory/AdicCompletion): AdicCompletion of Noetherian ring is Noetherian #38331
• depends on: feat(RingTheory): flat extension of local ring #36102
• depends on: feat(FieldTheory): basic theories about transcendental separable extension #37838
• depends on: feat(RingTheory/Smooth): transcendental separable extension is formally smooth #37953

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[github-actions]

PR summary c27c098f0d

Import changes exceeding 2%

%	File
+64.78%	Mathlib.RingTheory.AdicCompletion.LocalRing
+17.35%	Mathlib.RingTheory.AdicCompletion.Noetherian

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.AdicCompletion.LocalRing	1218	2007	+789 (+64.78%)
Mathlib.RingTheory.AdicCompletion.Noetherian	1839	2158	+319 (+17.35%)
Mathlib.RingTheory.Smooth.Field	2193	2200	+7 (+0.32%)

Import changes for all files

Files	Import difference
11 files Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.ZariskisMainTheorem	2
Mathlib.RingTheory.Smooth.Field	7
Mathlib.RingTheory.AdicCompletion.Noetherian	319
Mathlib.RingTheory.AdicCompletion.LocalRing	789
Mathlib.FieldTheory.TranscendentalSeparable (new file)	1998
Mathlib.RingTheory.Flat.Extension (new file)	2015
Mathlib.RingTheory.RegularLocalRing.Basic (new file)	2167
Mathlib.RingTheory.CohenStructureTheorem (new file)	2546

---

Declarations diff

+ AdicCompletion.algebraMap_isLocalHom_of_fg
+ AdicCompletion.isAdicComplete_of_fg
+ AdicCompletion.isAdicComplete_self
+ AdicCompletion.isLocalRing_of_fg
+ AdicCompletion.isMaximal_map_of_le
+ AdicCompletion.isNoetherianRing_of_fg
+ AdicCompletion.maximalIdeal_eq_map
+ AdicCompletion.maximalIdeal_eq_map_of_fg
+ AdicCompletion.mem_maximalIdeal_iff_eval_one_eq_zero
+ AdicCompletion.residueField_map_bijective
+ AdicCompletion.residueField_map_bijective_of_fg
+ AdicCompletion.ringKrullDim_eq
+ AdicCompletion.spanFinrank_maximalIdeal_eq
+ AlgHom.comp_toRingHom'
+ Algebra.Extension.ker_eq_comap_of_subalgebra
+ Algebra.FormallySmooth.of_isSeparablyGenerated
+ Algebra.FormallySmooth.of_isTranscendentalSeparable
+ Algebra.Generators.HomOfComm
+ Algebra.Generators.HomOfCommSelf
+ Algebra.Generators.homOfComm_cotangentSpace_map_eq
+ Algebra.Generators.homOfComm_cotangentSpace_map_injective_of_injective
+ Algebra.Generators.homOfComm_toAlgHom
+ Algebra.Generators.homOfComm_toExtensionHom_toAlgHom
+ Algebra.IsSeparablyGenerated
+ Algebra.IsTranscendentalSeparable
+ Algebra.h1Cotangent_eq_comap_of_algebraMap_injective
+ Algebra.h1Cotangent_subsingleton_of_subalgebra
+ Algebra.isSeparablyGenerated_of_charZero
+ Algebra.isSeparablyGenerated_of_equiv
+ Algebra.isTranscendentalSeparable_iff_isSeparablyGenerated_of_essFiniteType
+ Algebra.isTranscendentalSeparable_of_charZero
+ Algebra.isTranscendentalSeparable_of_isSeparablyGenerated
+ Algebra.isTranscendentalSeparable_of_perfectField
+ Algebra.isTranscendentalSeparable_tfae
+ FiniteRingKrullDim.ringKrullDim_eq_nat
+ FlatExtension
+ Hom
+ Hom.comp
+ Hom.hom
+ Hom.id
+ Ideal.height_add_one_le_of_lt_of_isPrime
+ Ideal.height_eq_ringKrullDim_iff
+ Ideal.height_eq_zero_iff
+ Ideal.height_strict_mono_of_isPrime
+ Ideal.height_strict_mono_of_isPrime_of_isPrime
+ Ideal.height_strict_mono_of_isPrime_of_is_prime
+ Ideal.isMaximal_of_height_eq_ringKrullDim
+ Ideal.le_minimalPrimes
+ Ideal.span_singleton_mul_eq_self_of_isPrime
+ Ideal.sup_height_isPrime_eq_ringKrullDim
+ Ideal.sup_height_of_maximal_eq_ringKrullDim
+ Ideal.toAssociatedGraded
+ IsBaseChange.of_eq_map
+ IsCohenRing
+ IsDiscreteValuationRing.of_isRegularLocalRing_of_ringKrullDim_eq_one
+ IsLocalRing.ResidueField.map_bijective_of_surjective
+ IsLocalRing.maximalIdeal_sq_lt_maximalIdeal
+ IsLocalRing.spanFinrank_maximalIdeal_quotient
+ IsReduced.tensorProduct_of_forall_fg_intermediateField
+ IsScalarTower.algebraMap_range_le
+ Polynomial.monomial_mem_reesAlgebra
+ SuccStruct
+ adjoinAlgebraicAlgebraK
+ adjoinAlgebraicIsScalarTower
+ adjoinAlgebraicResidueFieldEquiv
+ adjoinAlgebraicResidueFieldEquiv_apply_residue
+ adjoinAlgebraicResidueToK
+ adjoinAlgebraicToResidue
+ adjoinAlgebraicToResidueAux
+ adjoinAlgebraicToResidueAux_ker
+ adjoinAlgebraicToResidue_ker
+ adjoinAlgebraicToResidue_surjective
+ adjoinAlgebraic_algebraMap_isLocalHom
+ adjoinAlgebraic_isLocalRing
+ adjoinAlgebraic_maximalIdeal_eq_map
+ adjoinAlgebraic_maximalIdeal_map
+ adjoinAlgebraic_mem_range
+ adjoinPthRoots
+ adjoinPthRootsPthRoot
+ adjoinPthRootsPthRoot_bijective
+ adjoinPthRootsPthRoot_pow
+ adjoinPthRootsSelf
+ adjoinPthRootsSelf_algebraMap
+ adjoinPthRoots_pth_power_mem_bot
+ adjoinTranscendentalAlgebraK
+ adjoinTranscendentalAlgebraK_apply_residue
+ adjoinTranscendentalIsScalarTower
+ adjoinTranscendentalToK
+ adjoinTranscendentalToK_ker
+ adjoinTranscendental_aeval_ker
+ adjoinTranscendental_maximalIdeal_eq_map
+ adjoinTranscendental_mem_range
+ algebraMap_range_lt_of_not_surjective
+ coconeOfCoconeForget
+ exists_coeffs_sub_mem
+ exists_isCohenRing_of_not_charZero
+ exists_isCohenRing_residueField_map_bijective
+ exists_isLocalHom_flat
+ exists_monomial_span_of_fg
+ exists_section_of_charZero
+ instance (J : Type w) [LinearOrder J] [Nonempty J] (C : Type u) [Category.{v} C]
+ instance (J : Type w) [Preorder J] [Nonempty J] [IsDirectedOrder J] : IsFiltered J
+ instance (S S' : FlatExtension R K) :
+ instance : Algebra k (adjoinPthRoots k p) := (frobenius k p).toAlgebra
+ instance : Category.{w} (FlatExtension.{w} R K)
+ instance : CoeSort (FlatExtension.{w} R K) (Type w) := ⟨FlatExtension.Ring⟩
+ instance : ConcreteCategory (FlatExtension R K)
+ instance : ExpChar (AlgebraicClosure k) p := ExpChar.of_injective_algebraMap' k _
+ instance : Field (adjoinPthRoots k p) := inferInstanceAs (Field k)
+ instance : HasColimitsOfShape J (FlatExtension.{w} R K)
+ instance : HasFilteredColimitsOfSize.{w, w} (FlatExtension.{w} R K)
+ instance : HasForget₂ (FlatExtension.{w} R K) CommRingCat.{w}
+ instance : IsLocalHom (algebraMap S (adjoinTranscendental S))
+ instance [Fact (Nat.Prime p)] : Algebra.IsAlgebraic k (adjoinPthRoots k p)
+ instance [IsLocalRing R] [Small.{w} R] : IsLocalRing (Shrink R)
+ instance [IsNoetherianRing R] : IsNoetherianRing (AdicCompletion I R)
+ instance [IsNoetherianRing R] [IsLocalRing R] :
+ instance [IsNoetherianRing R] [IsLocalRing R] : IsAdicComplete
+ instance [IsNoetherianRing R] [IsLocalRing R] : IsLocalRing (AdicCompletion (maximalIdeal R) R)
+ instance [IsRegularLocalRing R] : IsDomain R := isDomain_of_isRegularLocalRing R
+ instance {S : Type*} [Semiring S] [Algebra R S] : IsLocalHom (AlgHom.id R S) := ⟨fun _ h ↦ h⟩
+ instance {S₁ S₂ S₃ : Type*} [Semiring S₁] [Semiring S₂] [Semiring S₃] [Algebra R S₁] [Algebra R S₂]
+ isColimit_coconeOfCoconeForget
+ isDomain_of_isRegularLocalRing
+ isNoetherianRing_of_isAdicComplete_of_fg
+ isReduced_injective_to_prod_localizations
+ isReduced_of_quotient_separable
+ isReduced_of_quotient_separable_of_field
+ isRegular_of_span_eq_maximalIdeal
+ linearIndepOn_pow_of_isReduced_tensorProduct
+ localization_minimal_isField
+ mem_map_algebraMap_reesAlgebra_iff
+ minimalPrimes_isPrime
+ minpolyLift
+ minpolyLift_spec
+ mk'
+ ofHom
+ padicIntOfCharP
+ padicIntOfCharP_flat_of_isCohenRing
+ padicIntToIntQuotient
+ padicIntToIntQuotient_ker
+ padicIntToIntQuotient_surjective
+ padicInt_to_int_quotient_comm
+ polynomialTensorProductEquiv
+ polynomialTensorProductEquiv_map_algebraMap
+ quotientPolynomialTensorProductEquiv
+ quotient_isRegularLocalRing_tfae
+ quotient_power_char_formallySmooth
+ quotient_span_singleton
+ reesAlgebraToAssociatedGraded
+ reesAlgebra_quotient_isNoetherian
+ spanFinrank_eq_one_iff
+ subset_iUnion_iff_mem_of_isMaximal_of_finite
+ tensorProduct_isReduced_of_isSeparablyGenerated_isDomain
+ tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced
+ tensorProduct_isReduced_of_isTranscendentalBasis_of_isDomain
+ tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced
+ tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced
+ tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType
+ tensorProduct_reesAlgebra_isNoetherian_of_fg
+ toAdjoinAlgebraic
+ toAdjoinTranscendental
+ toLocalizationMinimal
+ trivial
++ adjoinAlgebraic
++ adjoinTranscendental
++ instance (x : K) (int : IsIntegral (ResidueField S) x) :
- Ideal.height_strict_mono_of_is_prime

You can run this locally as follows

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

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

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

---

Increase in tech debt: (relative, absolute) = (12.00, 0.00)

Current number	Change	Type
6526	12	backward.isDefEq.respectTransparency

Current commit fc5df00508
Reference commit c27c098f0d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(RingTheory): regular local ring is domain #28683
• feat(RingTheory/AdicCompletion): AdicCompletion of Noetherian ring is Noetherian #38331
• feat(RingTheory): flat extension of local ring #36102
• feat(FieldTheory): basic theories about transcendental separable extension #37838
• feat(RingTheory/Smooth): transcendental separable extension is formally smooth #37953
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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

[mathlib-merge-conflicts]

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