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

Co-authored-by: Wang Jingting wangjt2020@163.com

---

• depends on: feat(Algebra/Homology): Ext modules #27416
• depends on: feat(Homology) : map between Ext induced by exact functor #30676

[github-actions]

PR summary a778305ec3

Import changes exceeding 2%

%	File
+7.03%	Mathlib.CategoryTheory.Shift.ShiftedHom

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Shift.ShiftedHom	740	792	+52 (+7.03%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Shift.ShiftedHomOpposite	35
Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Shift.ShiftedHom	52
Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear (new file)	1356
Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (new file)	1365
Mathlib.Algebra.Homology.DerivedCategory.Ext.BaseChange (new file)	1845

---

Declarations diff

+ CategoryTheory.Abelian.Ext.isBaseChange_aux
+ 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.mapExt
+ Functor.mapExtAddHom
+ Functor.mapExtAddHom_coe
+ Functor.mapExtLinearMap
+ Functor.mapExtLinearMap_coe
+ Functor.mapExtLinearMap_toAddMonoidHom
+ Functor.mapShiftedHom
+ Functor.mapShiftedHomAddHom
+ Functor.mapShiftedHomAddHom_linear
+ Functor.mapShiftedHomLinearMap
+ Functor.mapShiftedHom_add
+ Functor.mapShiftedHom_zero
+ IsBaseChange.of_exact
+ 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'
+ bilinearCompOfLinear
+ extendScalars'
+ extendScalars'_map_shortExact
+ hasExt_of_small1
+ hasExt_of_small2
+ homLinearEquiv
+ 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 (X Y : C) (n : M) : Module R (ShiftedHom X Y 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 : (extendScalars' R S).Additive
+ instance : Module R (Ext X Y n)
+ instance [F.Linear R] : Functor.Linear R (F.mapHomotopyCategory (ComplexShape.up ℤ))
+ instance [F.Linear R] [HasDerivedCategory.{w} C] [HasDerivedCategory.{w'} D] :
+ instance [Module.Flat R S] : Limits.PreservesFiniteColimits (extendScalars' R S) := by
+ instance [Module.Flat R S] : Limits.PreservesFiniteLimits (extendScalars' R S) := by
+ instance [Preadditive C] (X Y : C) (n : M) : AddCommGroup (ShiftedHom X Y n)
+ linearEquiv₀
+ mapDerivedCategorySingleFunctor
+ mapExt_comp_eq_comp_mapExt
+ mapExt_extClass_eq_extClass_map
+ mapExt_mk₀_eq_mk₀_map
+ mk₀_linearEquiv₀_apply
+ smul_eq_comp_mk₀
+ smul_hom
++ comp_smul
++ mk₀_smul
++ smul_comp
- instance [Preadditive C] (X Y : C) (n : M) : AddCommGroup (ShiftedHom X Y n) := by

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) = (1.00, 0.33)

Current number	Change	Type
762	1	erw
3	1	maxHeartBeats modifications

Current commit 4dfa50f898
Reference commit a778305ec3

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(Algebra/Homology): Ext modules #27416
• feat(Homology) : map between Ext induced by exact functor #30676
  By Dependent Issues (🤖). Happy coding!

[joelriou]

Could you try to add the compatibilities with the composition of Ext and with the bijection with Hom in degree 0?

[joelriou]

I believe there should be a "general" API for the interactions between ShiftedHom and a functor commuting with shifts (here, it would be F.mapDerivedCategory), then probably a similar API for SmallShiftedHom (applied to the localizer morphism consisting of the functor F.mapHomologicalComplex _ which preserves quasi-isomorphisms). Finally, using F.mapDerivedCategorySingleFunctor, we could get the expected maps. I think that it would be much easier to prove compatibilities by doing things in several (three!) steps as above.

[Thmoas-Guan]

For the first step, sorry I didn't see how to be general, isn't the current ShiftedHom.map enough? For the second step, do you mean by adding API for map of SmallShiftedHom under F.mapHomotopyCategory for exact functor F? Then what is the relation of the third step with the current map and the two previous steps? Sorry that I don't know what to add.

[joelriou]

The problem here is that we do not have an equational lemma expressing mapExt in terms of a general HasDerivedCategory instance. The definition is essentially correct, and it should be possible to prove certain compatibilities with it, but without a suitable equational lemma, this will become problematic at some point. I am afraid we very much need to follow sketch above about interactions between SmallShiftedHom and the application of functors which preserves suitable MorphismProperty and commute with shifts.

[Thmoas-Guan]

Sorry that I didn't get the point, so do you mean by adding some lemma to interact with Functor.mapShiftedHom? Furthermore do you mean by adding a version similar for SmallShiftedHom?