feat(RingTheory): Definition of complete intersection local ring

[Thmoas-Guan]

feat(RingTheory): Definition of Complete intersection ring

In this PR we give the definition of complete intersection local ring by epsilon_1(R)+ dim(R) equal to span rank of its maximal ideal.

We also proved for quotient of regular local ring, it is CI iff the ideal being quotient out is generated by regular sequence.

---

• depends on: feat(Algebra): cohen macaulay local ring is catenary #26245
• depends on: feat(Algebra): maximal Cohen Macaulay module #29533

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Algebra): cohen macaulay local ring is catenary #26245
• feat(Algebra): maximal Cohen Macaulay module #29533
  By Dependent Issues (🤖). Happy coding!

[github-actions]

PR summary 56e100aabd

Import changes exceeding 2%

%	File
+64.35%	Mathlib.RingTheory.AdicCompletion.LocalRing
+45.79%	Mathlib.RingTheory.AdicCompletion.Noetherian
+33.24%	Mathlib.RingTheory.Regular.Category
+25.10%	Mathlib.RingTheory.Regular.Depth

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.AdicCompletion.LocalRing	1209	1987	+778 (+64.35%)
Mathlib.RingTheory.AdicCompletion.Noetherian	1367	1993	+626 (+45.79%)
Mathlib.RingTheory.Regular.Category	1477	1968	+491 (+33.24%)
Mathlib.RingTheory.Regular.Depth	1809	2263	+454 (+25.10%)

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.ExteriorAlgebra.Basis Mathlib.LinearAlgebra.ExteriorPower.Basis	1
Mathlib.RingTheory.Regular.Depth	454
Mathlib.RingTheory.Regular.Category	491
Mathlib.RingTheory.AdicCompletion.Noetherian	626
Mathlib.RingTheory.AdicCompletion.LocalRing	778
Mathlib.RingTheory.Flat.Extension (new file)	1866
Mathlib.RingTheory.KoszulComplex.Cocomplex (new file)	1947
Mathlib.RingTheory.KoszulComplex.Complex (new file)	1949
Mathlib.RingTheory.KoszulComplex.Homotopy (new file)	1953
Mathlib.RingTheory.KoszulComplex.Dual (new file)	1975
Mathlib.RingTheory.RegularLocalRing.Defs (new file)	2148
Mathlib.RingTheory.RegularLocalRing.Basic (new file)	2159
Mathlib.RingTheory.RegularLocalRing.PowerSeries (new file)	2170
Mathlib.RingTheory.Smooth.Quotient (new file)	2175
Mathlib.RingTheory.Regular.Ischebeck (new file)	2303
Mathlib.RingTheory.CohenMacaulay.Basic (new file)	2407
Mathlib.RingTheory.CohenMacaulay.Catenary (new file)	2408
Mathlib.RingTheory.CohenMacaulay.Maximal (new file)	2418
Mathlib.RingTheory.CohenStructureTheorem (new file)	2426
Mathlib.RingTheory.CompleteIntersection.Basic (new file)	2717

---

Declarations diff

+ AdicCompletion.algebraMap_isLocalHom_of_fg
+ AdicCompletion.epsilon1_eq
+ AdicCompletion.isAdicComplete
+ AdicCompletion.isAdicComplete_of_fg
+ AdicCompletion.isAdicComplete_self
+ AdicCompletion.isLocalRing_of_fg
+ AdicCompletion.isMaximal_map
+ AdicCompletion.isNoetherianRing_of_fg
+ AdicCompletion.ker_eval
+ AdicCompletion.ker_eval_eq_range
+ AdicCompletion.le_ker_eval
+ 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.FormallySmooth.of_surjective_of_ker_eq_map_of_flat
+ CategoryTheory.Abelian.Ext.pow_mono_of_mono
+ CategoryTheory.Abelian.Ext.smul_id_postcomp_eq_zero_of_mem_ann
+ CategoryTheory.Functor.mapHomologicalComplex_sc
+ CochainComplex.linearYonedaObj
+ Epsilon1
+ FlatExtension
+ FormallySmooth.comp
+ GradedAlgebra.linearGMul
+ GradedAlgebra.linearGMul_eq_mul
+ Hom
+ Ideal.depth
+ Ideal.depth_eq_height
+ Ideal.depth_eq_of_iso
+ Ideal.depth_le_height
+ Ideal.depth_quotSMulTop_succ_eq_moduleDepth
+ Ideal.exist_regular_sequence_length_eq_height
+ Ideal.height_add_ringKrullDim_quotient_eq_ringKrullDim
+ Ideal.isLinearTopology
+ Ideal.ofList_height_eq_length_of_isWeaklyRegular
+ Ideal.ofList_height_eq_length_of_isWeaklyRegular'
+ Ideal.ofList_height_le_length
+ Ideal.ofList_spanFinrank_le_length
+ Ideal.primeHeight_add_ringKrullDim_quotient_eq_ringKrullDim
+ Ideal.primeHeight_eq_ringKrullDim_localization
+ Ideal.rTensor_mkQ_ker
+ Ideal.subtype_rTensor_range
+ IsBaseChange.of_eq_map
+ IsCohenMacaulayLocalRing
+ IsCohenMacaulayLocalRing.of_isLocalRing_of_isCohenMacaulayRing
+ IsCohenMacaulayRing
+ IsCohenMacaulayRing.of_isCohenMacaulayLocalRing
+ IsCohenRing
+ IsCompleteIntersectionLocalRing
+ IsDiscreteValuationRing.of_isRegularLocalRing_of_ringKrullDim_eq_one
+ IsLocalRing.Ideal.ofList_height_le_length'
+ IsLocalRing.ResidueField.map_bijective_of_surjective
+ IsLocalRing.ResidueField.map_injective
+ IsLocalRing.depth
+ IsLocalRing.depth_eq_of_algebraMap_surjective
+ IsLocalRing.depth_eq_of_iso
+ IsLocalRing.depth_eq_of_ringEquiv
+ IsLocalRing.depth_eq_sSup_length_regular
+ IsLocalRing.depth_quotSMulTop_succ_eq_moduleDepth
+ IsLocalRing.depth_quotient_regular_sequence_add_length_eq_depth
+ IsLocalRing.depth_quotient_regular_succ_eq_depth
+ IsLocalRing.depth_quotient_span_regular_succ_eq_depth
+ IsLocalRing.height_eq_height_maximalIdeal_of_maximalIdeal_mem_minimalPrimes
+ IsLocalRing.ideal_depth_eq_sSup_length_regular
+ IsLocalRing.ideal_depth_le_depth
+ IsRegularLocalRing
+ IsScalarTower.algebraMap_range_le
+ LinearEquiv.comap_smul_top
+ LinearMap.kerBaseChangeEquiv
+ LinearMap.ker_inf_smul_top_eq_smul_of_flat
+ LinearMap.lsum_smul_id_range
+ LinearMapOfSemiLinearMapAlgebraMap
+ ModuleCat.IsCohenMacaulay
+ ModuleCat.IsCohenMacaulay_of_iso
+ ModuleCat.IsMaximalCohenMacaulay
+ ModuleCat.depth_eq_supportDim_of_cohenMacaulay
+ ModuleCat.depth_eq_supportDim_unbot_of_cohenMacaulay
+ ModuleCat.exists_isRegular_of_exists_subsingleton_ext
+ ModuleCat.exists_isRegular_tfae
+ ModuleCat.isCohenMacaulay_iff
+ ModuleCat.subsingleton_ext_of_exists_isRegular
+ MvPowerSeries.isAdicComplete
+ MvPowerSeries.isRegularLocalRing_of_isRegularLocalRing
+ PowerSeries.isRegularLocalRing_of_isRegularLocalRing
+ PowerSeries.maximalIdeal_eq_sup
+ RingHom.FormallySmooth.of_flat_of_ker_eq_map_of_square_zero
+ SemiLinearMapAlgebraMapOfLinearMap
+ Submodule.comap_lt_top_of_lt_range
+ SuccStruct
+ WithIdeal.isTopologicallyNilpotent_of_mem
+ WithIdeal.uniformContinuous_of_map_le
+ XZeroLinearEquivRing
+ adicCompletion_isCompleteIntersectionLocalRing_iff
+ 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
+ adjoinTranscendentalAlgebraK
+ adjoinTranscendentalAlgebraK_apply_residue
+ adjoinTranscendentalIsScalarTower
+ adjoinTranscendentalToK
+ adjoinTranscendentalToK_ker
+ adjoinTranscendental_aeval_ker
+ adjoinTranscendental_maximalIdeal_eq_map
+ adjoinTranscendental_mem_range
+ algebraMap_range_lt_of_not_surjective
+ associatedPrimes_self_eq_minimalPrimes
+ associated_prime_eq_minimalPrimes_isCohenMacaulay
+ associated_prime_minimal_of_isCohenMacaulay
+ basis
+ coe_map
+ depth_eq_dim_quotient_associated_prime_of_isCohenMacaulay
+ depth_le_ringKrullDim
+ depth_le_ringKrullDim_associatedPrime
+ depth_le_supportDim
+ depth_ne_top
+ depth_quotient_regular_sequence_add_length_eq_depth
+ epsilon1_add_ringKrullDim_eq_spanFinrank_add_spanFinrank
+ epsilon1_add_ringKrullDim_eq_spanFinrank_add_spanFinrank_of_surjective
+ epsilon1_add_ringKrullDim_ge
+ epsilon1_eq_of_ringEquiv
+ epsilon1_eq_of_ringEquiv_aux
+ epsilon1_eq_spanFinrank
+ exactAt_of_isRegular
+ exactAt_of_lt_length_of_isRegular
+ exactAt_of_ne_length_of_isRegular
+ exist_isRegularLocalRing_surjective_adicCompletion
+ exist_isRegularLocalRing_surjective_adicCompletion_ker_le
+ exist_isRegularLocalRing_surjective_ker_le_of_isAdicComplete
+ exist_isRegularLocalRing_surjective_of_isAdicComplete
+ exist_nat_eq
+ exists_isCohenRing_of_not_charZero
+ exists_isCohenRing_residueField_map_bijective
+ exists_isLocalHom_flat
+ exists_mvPowerSeries_surjective_of_residueField_map_bijective
+ exists_section_of_charZero
+ ext_subsingleton_of_lt_moduleDepth
+ finite_generators_of_isNoetherian
+ free
+ free_of_isMaximalCohenMacaulay_of_isRegularLocalRing
+ free_of_quotSMulTop_free
+ ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth
+ iff_finrank_cotangentSpace
+ instance (priority := 100) [WithIdeal R] : IsLinearTopology R R := i.isLinearTopology
+ instance : Category.{w} (FlatExtension.{w} R K)
+ instance : IsLocalHom (algebraMap S (adjoinTranscendental S))
+ instance : Limits.HasIterationOfShape J (FlatExtension R K) := sorry
+ instance [IsCohenMacaulayLocalRing R] : (ModuleCat.of R R).IsCohenMacaulay
+ instance [IsDomain R] [IsDiscreteValuationRing R] : IsRegularLocalRing R := by
+ 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 [IsNoetherianRing R] [IsLocalRing R] [Small.{v} 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₂]
+ instance {k : Type*} [Field k] : IsRegularLocalRing k := by
+ isCohenMacaulayLocalRing_def
+ isCohenMacaulayLocalRing_iff
+ isCohenMacaulayLocalRing_localization_atPrime
+ isCohenMacaulayLocalRing_of_isRegularLocalRing
+ isCohenMacaulayLocalRing_of_ringEquiv
+ isCohenMacaulayLocalRing_of_ringKrullDim_le_depth
+ isCohenMacaulayRing_def
+ isCohenMacaulayRing_def'
+ isCohenMacaulayRing_iff
+ isCohenMacaulayRing_of_ringEquiv
+ isCohenMacaulay_of_isMaximalCohenMacaulay
+ isCompleteIntersectionLocalRing_def
+ isCompleteIntersectionLocalRing_iff
+ isCompleteIntersectionLocalRing_of_ringEquiv
+ isDomain_of_isRegularLocalRing
+ isField_of_isRegularLocalRing_of_dimension_zero
+ isLocalization_at_prime_prime_depth_le_depth
+ isLocalize_at_prime_depth_eq_of_isCohenMacaulay
+ isLocalize_at_prime_dim_eq_prime_depth_of_isCohenMacaulay
+ isLocalize_at_prime_isCohenMacaulay_of_isCohenMacaulay
+ isLocalizedModule_quotSMulTop_isLocalizedModule_map
+ isMaximalCohenMacaulay_def
+ isRegularLocalRing_def
+ isRegular_of_maximalIdeal_mem_ofList_minimalPrimes
+ isRegular_of_ofList_height_eq_length_of_isCohenMacaulayLocalRing
+ isRegular_of_span_eq_maximalIdeal
+ koszulAlgebra
+ koszulAlgebra.annihilator_homology
+ koszulCocomplex
+ koszulCocomplex.mem_annihilator_homology
+ koszulCocomplex.ofList_ideal_le_mem_annihilator_homology
+ koszulComplex
+ koszulComplex.mem_annihilator_homology
+ koszulComplex.ofList_ideal_annihilator_homology
+ koszulComplex.range_le_annihilator_homology
+ koszulComplex_aux
+ koszulComplex_aux_comp_eq_zero
+ localize_at_prime_depth_eq_of_isCohenMacaulay
+ localize_at_prime_isCohenMacaulay_of_isCohenMacaulay
+ map_comp
+ map_hom
+ map_id
+ map_id_refl
+ maximalIdeal_mem_minimalPrimes_of_surjective
+ maximalIdeal_mem_ofList_append_minimalPrimes_of_ofList_height_eq_length
+ minpolyLift
+ minpolyLift_spec
+ moduleDepth
+ moduleDepth_eq_depth_of_supp_eq
+ moduleDepth_eq_find
+ moduleDepth_eq_iff
+ moduleDepth_eq_moduleDepth_shrink
+ moduleDepth_eq_of_iso_fst
+ moduleDepth_eq_of_iso_snd
+ moduleDepth_eq_sSup_length_regular
+ moduleDepth_eq_sup_nat
+ moduleDepth_eq_top_iff
+ moduleDepth_eq_zero_of_hom_nontrivial
+ moduleDepth_ge_depth_sub_dim
+ moduleDepth_ge_min_of_shortExact_fst_fst
+ moduleDepth_ge_min_of_shortExact_fst_snd
+ moduleDepth_ge_min_of_shortExact_snd_fst
+ moduleDepth_ge_min_of_shortExact_snd_snd
+ moduleDepth_ge_min_of_shortExact_trd_fst
+ moduleDepth_ge_min_of_shortExact_trd_snd
+ moduleDepth_lt_top_iff
+ moduleDepth_quotSMulTop_succ_eq_moduleDepth
+ moduleDepth_quotient_regular_sequence_add_length_eq_moduleDepth
+ nonempty_linearEquiv_of_minimal_generators
+ nonempty_linearEquiv_of_minimal_generators'
+ of_ringEquiv
+ of_spanFinrank_maximalIdeal_le
+ padicIntOfCharP
+ padicIntOfCharP_flat_of_isCohenRing
+ padicIntToIntQuotient
+ padicIntToIntQuotient_ker
+ padicIntToIntQuotient_surjective
+ padicInt_to_int_quotient_comm
+ preservesHomology_of_flat
+ quotSMulTop_isCohenMacaulay_iff_isCohenMacaulay
+ quotSMulTop_isLocalizedModule_map
+ quotient_isCompleteIntersectionLocalRing
+ quotient_isCompleteIntersectionLocalRing_iff
+ quotient_isRegularLocalRing_tfae
+ quotient_power_char_formallySmooth
+ quotient_prime_ringKrullDim_ne_bot
+ quotient_regular_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_regular_sequence_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_regular_smul_top_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_span_regular_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_span_singleton
+ ringKrullDim_le_spanFinrank_maximalIdeal
+ ringKrullDim_quotient_eq_iSup_quotient_minimalPrimes
+ ring_depth_invariant
+ ring_depth_uLift
+ spanFinrank_comap
+ spanFinrank_eq_of_surjective_of_ker_le
+ span_ιMulti_orderEmbedding_of_span_eq_top
+ subsingleton_of_card_generators_le
+ subtype_comp_map_eq
+ toAdjoinAlgebraic
+ toAdjoinTranscendental
+ topHomologyLinearEquiv
+ topXLinearEquivOfBasis
+ topXLinearEquivOfBasisOfList
+ trivial
+ zeroHomologyLinearEquiv
++ X_isZero_of_card_generators_le
++ adjoinAlgebraic
++ adjoinTranscendental
++ baseChange_iso
++ instance (T : Type v) [CommRing T] (g : R →+* T) :
++ instance (x : K) (int : IsIntegral (ResidueField S) x) :
++ isoOfEquiv
++ map
++ nonempty_iso_of_minimal_generators
++ nonempty_iso_of_minimal_generators'
++ ofList
++ ofList_X_isZero_of_length_le
++++ instance [IsNoetherianRing R] [IsLocalRing R] (i : ℕ) :
- isUnit_iff_notMem_of_isAdicComplete_maximal

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) = (1.07, 0.11)

Current number	Change	Type
10	1	maxHeartBeats modifications
8787	60	backward.isDefEq

Current commit d4d6ccb52d
Reference commit 56e100aabd

You can run this locally as

./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-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.