feat(RingTheory/Morita/Basic): Define Morita Equivalence (#20640)

Co-authored by: @jjaassoonn 



Co-authored-by: zjj <zjj@zjj>
Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>
Co-authored-by: Whysoserioushah <yx3021@ic.ac.uk>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib.lean

@@ -4752,6 +4752,7 @@ import Mathlib.RingTheory.Localization.NumDen
 import Mathlib.RingTheory.Localization.Pi
 import Mathlib.RingTheory.Localization.Submodule
 import Mathlib.RingTheory.MatrixAlgebra
+import Mathlib.RingTheory.Morita.Basic
 import Mathlib.RingTheory.Multiplicity
 import Mathlib.RingTheory.MvPolynomial
 import Mathlib.RingTheory.MvPolynomial.Basic

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -423,11 +423,40 @@ end Module
 
 section
 
-variable {S : Type u} [CommRing S]
+universe u₀
+
+namespace Algebra
+
+variable {S₀ : Type u₀} [CommSemiring S₀] {S : Type u} [Ring S] [Algebra S₀ S]
 
 variable {M N : ModuleCat.{v} S}
 
-instance : Linear S (ModuleCat.{v} S) where
+/--
+Let `S` be an `S₀`-algebra. Then `S`-modules are modules over `S₀`.
+-/
+scoped instance : Module S₀ M := Module.compHom _ (algebraMap S₀ S)
+
+scoped instance : IsScalarTower S₀ S M where
+  smul_assoc _ _ _ := by rw [Algebra.smul_def, mul_smul]; rfl
+
+scoped instance : SMulCommClass S S₀ M where
+  smul_comm s s₀ n :=
+    show s • algebraMap S₀ S s₀ • n = algebraMap S₀ S s₀ • s • n by
+    rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
+
+/--
+Let `S` be an `S₀`-algebra. Then the category of `S`-modules is `S₀`-linear.
+-/
+scoped instance instLinear : Linear S₀ (ModuleCat.{v} S) where
+  smul_comp _ M N s₀ f g := by ext; simp
+
+end Algebra
+
+section
+
+variable {S : Type u} [CommRing S]
+
+instance : Linear S (ModuleCat.{v} S) := ModuleCat.Algebra.instLinear
 
 variable {X Y X' Y' : ModuleCat.{v} S}
 
@@ -441,6 +470,8 @@ theorem Iso.conj_eq_conj (i : X ≅ X') (f : End X) :
 
 end
 
+end
+
 variable (M N : ModuleCat.{v} R)
 
 /-- `ModuleCat.Hom.hom` as an isomorphism of rings. -/

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.Limits
 import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.CategoryTheory.Adjunction.Mates
+import Mathlib.CategoryTheory.Linear.LinearFunctor
 
 /-!
 # Change Of Rings
@@ -264,6 +265,24 @@ instance restrictScalars_isEquivalence_of_ringEquiv {R S} [Ring R] [Ring S] (e :
     (ModuleCat.restrictScalars e.toRingHom).IsEquivalence :=
   (restrictScalarsEquivalenceOfRingEquiv e).isEquivalence_functor
 
+instance {R S} [Ring R] [Ring S] (f : R →+* S) : (restrictScalars f).Additive where
+
+instance restrictScalarsEquivalenceOfRingEquiv_additive {R S} [Ring R] [Ring S] (e : R ≃+* S) :
+    (restrictScalarsEquivalenceOfRingEquiv e).functor.Additive where
+
+namespace Algebra
+
+instance {R₀ R S} [CommSemiring R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S]
+    (f : R →ₐ[R₀] S) : (restrictScalars f.toRingHom).Linear R₀ where
+  map_smul {M N} g r₀ := by ext m; exact congr_arg (· • g.hom m) (f.commutes r₀).symm
+
+instance restrictScalarsEquivalenceOfRingEquiv_linear
+    {R₀ R S} [CommSemiring R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S] (e : R ≃ₐ[R₀] S) :
+    (restrictScalarsEquivalenceOfRingEquiv e.toRingEquiv).functor.Linear R₀ :=
+  inferInstanceAs ((restrictScalars e.toAlgHom.toRingHom).Linear R₀)
+
+end Algebra
+
 open TensorProduct
 
 variable {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S)

Mathlib/CategoryTheory/Action/Limits.lean

@@ -328,6 +328,6 @@ instance mapAction_preadditive [F.Additive] : (F.mapAction G).Additive where
 
 variable {R : Type*} [Semiring R] [CategoryTheory.Linear R V] [CategoryTheory.Linear R W]
 
-instance mapAction_linear [F.Additive] [F.Linear R] : (F.mapAction G).Linear R where
+instance mapAction_linear [F.Linear R] : (F.mapAction G).Linear R where
 
 end CategoryTheory.Functor

Mathlib/CategoryTheory/Linear/LinearFunctor.lean

@@ -28,7 +28,7 @@ variable (R : Type*) [Semiring R]
 
 /-- An additive functor `F` is `R`-linear provided `F.map` is an `R`-module morphism. -/
 class Functor.Linear {C D : Type*} [Category C] [Category D] [Preadditive C] [Preadditive D]
-  [Linear R C] [Linear R D] (F : C ⥤ D) [F.Additive] : Prop where
+  [Linear R C] [Linear R D] (F : C ⥤ D) : Prop where
   /-- the functor induces a linear map on morphisms -/
   map_smul : ∀ {X Y : C} (f : X ⟶ Y) (r : R), F.map (r • f) = r • F.map f := by aesop_cat
 
@@ -40,7 +40,7 @@ section
 
 variable {R}
 variable {C D : Type*} [Category C] [Category D] [Preadditive C] [Preadditive D]
-  [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : C ⥤ D) [Additive F] [Linear R F]
+  [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] (F : C ⥤ D) [Linear R F]
 
 @[simp]
 theorem map_smul {X Y : C} (r : R) (f : X ⟶ Y) : F.map (r • f) = r • F.map f :=
@@ -53,9 +53,9 @@ theorem map_units_smul {X Y : C} (r : Rˣ) (f : X ⟶ Y) : F.map (r • f) = r 
 instance : Linear R (𝟭 C) where
 
 instance {E : Type*} [Category E] [Preadditive E] [CategoryTheory.Linear R E] (G : D ⥤ E)
-    [Additive G] [Linear R G] : Linear R (F ⋙ G) where
+    [Linear R G] : Linear R (F ⋙ G) where
 
-variable (R)
+variable (R) [F.Additive]
 
 /-- `F.mapLinearMap` is an `R`-linear map whose underlying function is `F.map`. -/
 @[simps]
@@ -103,7 +103,7 @@ namespace Equivalence
 variable {C D : Type*} [Category C] [Category D] [Preadditive C] [Linear R C] [Preadditive D]
   [Linear R D]
 
-instance inverseLinear (e : C ≌ D) [e.functor.Additive] [e.functor.Linear R] :
+instance inverseLinear (e : C ≌ D) [e.functor.Linear R] :
   e.inverse.Linear R where
     map_smul r f := by
       apply e.functor.map_injective

Mathlib/CategoryTheory/Monoidal/Linear.lean

@@ -50,7 +50,7 @@ instance tensoringRight_linear (X : C) : ((tensoringRight C).obj X).Linear R whe
 ensures that the domain is linear monoidal. -/
 theorem monoidalLinearOfFaithful {D : Type*} [Category D] [Preadditive D] [Linear R D]
     [MonoidalCategory D] [MonoidalPreadditive D] (F : D ⥤ C) [F.Monoidal] [F.Faithful]
-    [F.Additive] [F.Linear R] : MonoidalLinear R D :=
+    [F.Linear R] : MonoidalLinear R D :=
   { whiskerLeft_smul := by
       intros X Y Z r f
       apply F.map_injective

Mathlib/RingTheory/Morita/Basic.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2025 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang, Yunzhou Xie
+-/
+import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
+import Mathlib.CategoryTheory.Linear.LinearFunctor
+import Mathlib.Algebra.Category.ModuleCat.Basic
+import Mathlib.CategoryTheory.Adjunction.Limits
+
+/-!
+# Morita equivalence
+
+Two `R`-algebras `A` and `B` are Morita equivalent if the categories of modules over `A` and
+`B` are `R`-linearly equivalent. In this file, we prove that Morita equivalence is an equivalence
+relation and that isomorphic algebras are Morita equivalent.
+
+# Main definitions
+
+- `MoritaEquivalence R A B`: a structure containing an `R`-linear equivalence of categories between
+  the module categories of `A` and `B`.
+- `IsMoritaEquivalent R A B`: a predicate asserting that `R`-algebras `A` and `B` are Morita
+  equivalent.
+
+## TODO
+
+- For any ring `R`, `R` and `Matₙ(R)` are Morita equivalent.
+- Morita equivalence in terms of projective generators.
+- Morita equivalence in terms of full idempotents.
+- Morita equivalence in terms of existence of an invertible bimodule.
+- If `R ≈ S`, then `R` is simple iff `S` is simple.
+
+## References
+
+* [Nathan Jacobson, *Basic Algebra II*][jacobson1989]
+
+## Tags
+
+Morita Equivalence, Category Theory, Noncommutative Ring, Module Theory
+
+-/
+
+universe u₀ u₁ u₂ u₃
+
+open CategoryTheory
+
+variable (R : Type u₀) [CommSemiring R]
+
+open scoped ModuleCat.Algebra
+
+/--
+Let `A` and `B` be `R`-algebras. A Morita equivalence between `A` and `B` is an `R`-linear
+equivalence between the categories of `A`-modules and `B`-modules.
+-/
+structure MoritaEquivalence
+    (A : Type u₁) [Ring A] [Algebra R A]
+    (B : Type u₂) [Ring B] [Algebra R B] where
+  /-- The underlying equivalence of categories -/
+  eqv : ModuleCat.{max u₁ u₂} A ≌ ModuleCat.{max u₁ u₂} B
+  linear : eqv.functor.Linear R := by infer_instance
+
+namespace MoritaEquivalence
+
+attribute [instance] MoritaEquivalence.linear
+
+instance {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B]
+    (e : MoritaEquivalence R A B) : e.eqv.functor.Additive :=
+  e.eqv.functor.additive_of_preserves_binary_products
+
+/--
+For any `R`-algebra `A`, `A` is Morita equivalent to itself.
+-/
+def refl (A : Type u₁) [Ring A] [Algebra R A] : MoritaEquivalence R A A where
+  eqv := CategoryTheory.Equivalence.refl
+  linear := Functor.instLinearId
+
+/--
+For any `R`-algebras `A` and `B`, if `A` is Morita equivalent to `B`, then `B` is Morita equivalent
+to `A`.
+-/
+def symm {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B]
+    (e : MoritaEquivalence R A B) : MoritaEquivalence R B A where
+  eqv := e.eqv.symm
+  linear := e.eqv.inverseLinear R
+
+-- TODO: We have restricted all the rings to the same universe here because of the complication
+-- `max u₁ u₂`, `max u₂ u₃` vs `max u₁ u₃`. But once we proved the definition of Morita
+-- equivalence is equivalent to the existence of a full idempotent element, we can remove this
+-- restriction in the universe.
+-- Or alternatively, @alreadydone has sketched an argument on how the universe restriction can be
+-- removed via a categorical argument,
+-- see [here](https://github.com/leanprover-community/mathlib4/pull/20640#discussion_r1912189931)
+/--
+For any `R`-algebras `A`, `B`, and `C`, if `A` is Morita equivalent to `B` and `B` is Morita
+equivalent to `C`, then `A` is Morita equivalent to `C`.
+-/
+def trans {A B C : Type u₁}
+    [Ring A] [Algebra R A] [Ring B] [Algebra R B] [Ring C] [Algebra R C]
+    (e : MoritaEquivalence R A B) (e' : MoritaEquivalence R B C) :
+    MoritaEquivalence R A C where
+  eqv := e.eqv.trans e'.eqv
+  linear := e.eqv.functor.instLinearComp e'.eqv.functor
+
+variable {R} in
+/--
+Isomorphic `R`-algebras are Morita equivalent.
+-/
+noncomputable def ofAlgEquiv {A : Type u₁} {B : Type u₂}
+    [Ring A] [Algebra R A] [Ring B] [Algebra R B] (f : A ≃ₐ[R] B) :
+    MoritaEquivalence R A B where
+  eqv := ModuleCat.restrictScalarsEquivalenceOfRingEquiv f.symm.toRingEquiv
+  linear := ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear f.symm
+
+end MoritaEquivalence
+
+/--
+Let `A` and `B` be `R`-algebras. We say that `A` and `B` are Morita equivalent if the categories of
+`A`-modules and `B`-modules are equivalent as `R`-linear categories.
+-/
+structure IsMoritaEquivalent
+    (A : Type u₁) [Ring A] [Algebra R A]
+    (B : Type u₂) [Ring B] [Algebra R B] : Prop where
+  cond : Nonempty <| MoritaEquivalence R A B
+
+namespace IsMoritaEquivalent
+
+lemma refl (A : Type u₁) [Ring A] [Algebra R A] : IsMoritaEquivalent R A A where
+  cond := ⟨.refl R A⟩
+
+lemma symm {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B]
+    (h : IsMoritaEquivalent R A B) : IsMoritaEquivalent R B A where
+  cond := h.cond.map <| .symm R
+
+lemma trans {A B C : Type u₁} [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C]
+    (h : IsMoritaEquivalent R A B) (h' : IsMoritaEquivalent R B C) :
+    IsMoritaEquivalent R A C where
+  cond := Nonempty.map2 (.trans R) h.cond h'.cond
+
+lemma of_algEquiv {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B]
+    (f : A ≃ₐ[R] B) : IsMoritaEquivalent R A B where
+  cond := ⟨.ofAlgEquiv f⟩
+
+end IsMoritaEquivalent