[Merged by Bors] - feat(RingTheory/Morita/Basic): Define Morita Equivalence

[Whysoserioushah]

Co-authored by: @jjaassoonn

---

[github-actions]

PR summary 84846a1273

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings	1189	1192	+3 (+0.25%)

Import changes for all files

Files	Import difference
6 files Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde	2
20 files Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf	3
Mathlib.RingTheory.Morita.Basic (new file)	1194

---

Declarations diff

+ IsMoritaEquivalent
+ MoritaEquivalence
+ instance : Linear S (ModuleCat.{v} S) := ModuleCat.Algebra.instLinear
+ instance {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B]
+ instance {R S} [Ring R] [Ring S] (f : R →+* S) : (restrictScalars f).Additive
+ instance {R₀ R S} [CommSemiring R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S]
+ ofAlgEquiv
+ of_algEquiv
+ restrictScalarsEquivalenceOfRingEquiv_additive
+ restrictScalarsEquivalenceOfRingEquiv_linear
++ refl
++ symm
++ trans
- instance : Linear S (ModuleCat.{v} S)

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.

---

No changes to technical debt.

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

[ADedecker]

I think it's quite important to add a base ring into the story: when A and B are algebras over a (commutative) ring R, you want to be able to say that their categories of modules are, not only equivalent or additively equivalent, but R-linearly equivalent (I'm not sure about the terminology, but I think you'll see what I mean).

Also, even in the general setup, I think it would be better to always assume a Morita equivalence to be additive, and add a constructor from a bare equivalence.

[jjaassoonn]

@ADedecker can you check the newest commit 273aaa7 to see if this is what you mean (modulo the factor a bunch of other stuff in mathlib is broken)

[erdOne]

You should give IsScalarTower instead. And use IsScalarTower.of_algebraMap_smul in the proof.

[Whysoserioushah]

changed!

[erdOne]

It still gives a large-import label. Perhaps add both IsScalarTower and SMulCommClass by hand?

[erdOne]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style