feat(Homology): Ext commute with flat base change

[Thmoas-Guan]

In this PR, using the linear map Ext(M,N) => Ext(F(M), F(N)) when F is exact functor, we prove that Ext commute with flat base change if the ring is noetherian and two modules are finitely generated, stated using IsBaseChange.

---

• depends on: feat(Homology) : compatibility of map between Ext #31046
• depends on: feat(Algebra): Hom commute with flat base change #31222
• depends on: feat(Homology/ModuleCat): Dimension Shifting tools in ModuleCat #32316

[github-actions]

PR summary 725c803ee9

Import changes exceeding 2%

%	File
+8.77%	Mathlib.Algebra.Module.FinitePresentation

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Module.FinitePresentation	1072	1166	+94 (+8.77%)
Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor	1077	1084	+7 (+0.65%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Smooth.Flat	2
23 files Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.Cyclotomic.Basic Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal Mathlib.NumberTheory.NumberField.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Cyclotomic.Three Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.NumberField.Ideal.Basic Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.LinearDisjoint Mathlib.RingTheory.Etale.Locus Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Unramified.LocalRing	3
11 files Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Polynomial.UniversalFactorizationRing Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Unramified.Locus	4
Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor	7
19 files Mathlib.Algebra.Module.Presentation.Differentials Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Etale.StandardEtale Mathlib.RingTheory.Extension.Cotangent.Basic Mathlib.RingTheory.Extension.Cotangent.Basis Mathlib.RingTheory.Extension.Cotangent.Free Mathlib.RingTheory.Extension.Cotangent.LocalizationAway Mathlib.RingTheory.Finiteness.ModuleFinitePresentation Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Smooth.AdicCompletion Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.NoetherianDescent Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmoothOfFree	16
Mathlib.Algebra.Module.FinitePresentation Mathlib.Algebra.Module.Presentation.Finite	94
Mathlib.RingTheory.Flat.IsBaseChange (new file)	1133
Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (new file)	1135
Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting (new file)	1722
Mathlib.Algebra.Category.ModuleCat.Ext.BaseChange (new file)	1861

---

Declarations diff

+ Abelian.Ext.mapExactFunctor
+ Abelian.Ext.mapExactFunctor_add
+ Abelian.Ext.mapExactFunctor_eq_shiftedHom_map
+ Abelian.Ext.mapExactFunctor_zero
+ CategoryTheory.Abelian.Ext.isBaseChange_aux
+ CategoryTheory.Functor.mapCochainComplexSingleFunctor
+ CategoryTheory.InjectivePresentation.shortComplex
+ CategoryTheory.InjectivePresentation.shortComplex_shortExact
+ CategoryTheory.isBaseChange_hom
+ Ext.isBaseChange
+ Ext.isBaseChange'
+ Ext.isBaseChangeMap
+ Ext.isBaseChangeMap'
+ Ext.isBaseChangeMap_aux
+ Ext.isBaseChangeMap_aux'
+ Ext.isLocalizedModule
+ Ext.isLocalizedModule'
+ Ext.isLocalizedModuleMap
+ Ext.isLocalizedModuleMap'
+ ExtendScalars'.map'
+ ExtendScalars'.map'_comp
+ ExtendScalars'.map'_id
+ ExtendScalars'.obj'
+ Functor.mapExactFunctor_smul
+ Functor.mapExtAddHom
+ Functor.mapExtAddHom_apply
+ Functor.mapExtAddHom_coe
+ Functor.mapExtLinearMap
+ Functor.mapExtLinearMap_apply
+ Functor.mapExtLinearMap_coe
+ Functor.mapExtLinearMap_toAddMonoidHom
+ Functor.mapHomologicalComplex_map_exact
+ Functor.mapShiftedHom_singleδ
+ Functor.mapTriangleOfSESδ
+ IsBaseChange.comp_equiv
+ IsBaseChange.of_equiv_left
+ IsBaseChange.of_equiv_right
+ IsBaseChange.of_left_exact
+ IsBaseChange.of_right_exact
+ LinearMap.shortComplexKer
+ LinearMap.shortExact_shortComplexKer
+ Module.FinitePresentation.exists_fin'
+ Module.FinitePresentation.isBaseChange_map
+ Module.exists_finite_presentation
+ Module.finite_shrink
+ Module.free_shrink
+ ModuleCat.extendScalars'.mapExtLinearMap
+ ModuleCat.extendScalars'.mapExtLinearMap_eq_mapExt
+ ModuleCat.extendScalars'_map_LinearMap
+ ModuleCat.extendScalars'_map_LinearMap_eq_mapAddHom
+ ModuleCat.iso_extendScalars'_of_isBaseChange
+ ModuleCat.iso_extendScalars'_of_isBaseChange'
+ ModuleCat.projective_shortComplex
+ ModuleCat.projective_shortComplex_shortExact
+ descShortComplex_hom
+ extClass_postcomp_surjective_of_projective_X₂
+ extClass_precomp_surjective_of_projective_X₂
+ extendScalars'
+ extendScalars'_map_exact
+ instance (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) :
+ instance (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) [Linear R V] [Linear R W] [F.Linear R] :
+ instance (M N : ModuleCat.{v'} S) : IsScalarTower R S (M ⟶ N)
+ instance (M N : ModuleCat.{v'} S) : Module R (M ⟶ N)
+ instance (M N : Type*) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
+ instance (n : ℕ) (M N : ModuleCat.{v'} S) : IsScalarTower R S (Ext M N n)
+ instance (n : ℕ) (M N : ModuleCat.{v'} S) : Module R (Ext M N n)
+ instance : (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism
+ instance : (extendScalars' R S).Additive
+ instance : NatTrans.CommShift F.mapDerivedCategoryFactors.symm.hom ℤ
+ instance [F.Linear R] : F.mapDerivedCategory.Linear R := by
+ instance [Linear R G] : Linear R (F ⋙ G)
+ instance [Module.Flat R S] : Limits.PreservesFiniteColimits (extendScalars' R S) := by
+ instance [Module.Flat R S] : Limits.PreservesFiniteLimits (extendScalars' R S) := by
+ instance [Small.{v} R] (M : ModuleCat.{v} R) : Module.Free R M.projective_shortComplex.X₂
+ instance [h : HasExt.{w'} D] (X Y : C) : HasSmallLocalizedShiftedHom.{w'}
+ instance {M : ModuleCat.{v} R} (ip : InjectivePresentation M) : Injective ip.shortComplex.X₂ := ip.2
+ instance {ι : Type*} (c : ComplexShape ι) :
+ instance {ι : Type*} (c : ComplexShape ι) : PreservesFiniteLimits (F.mapHomologicalComplex c) := by
+ linear_of_full_essSurj_comp
+ mapDerivedCategorySingleFunctor
+ mapExactFunctor₀
+ mapExt_comp_eq_comp_mapExt
+ mapExt_extClass_eq_extClass_map
+ mapExt_mk₀_eq_mk₀_map
+ subsingleton_of_injective
+ subsingleton_of_projective
+ triangleOfSESδ_hom
+ triangle_mor₃_hom
- instance {E : Type*} [Category* E] [Preadditive E] [CategoryTheory.Linear R E] (G : D ⥤ E)

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.

---

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

Current number	Change	Type
638	2	erw

Current commit e8f591a946
Reference commit 725c803ee9

You can run this locally as

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Homology) : compatibility of map between Ext #31046
• feat(Algebra): Hom commute with flat base change #31222
• feat(Homology/ModuleCat): Dimension Shifting tools in ModuleCat #32316
  By Dependent Issues (🤖). Happy coding!