From ca351a7474b506bb0f3461c775621b648a30bdf1 Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Fri, 10 Jan 2025 16:46:24 +0000 Subject: [PATCH 01/37] basic --- Mathlib/RingTheory/Morita/Basic.lean | 105 +++++++++++++++++++++++++++ 1 file changed, 105 insertions(+) create mode 100644 Mathlib/RingTheory/Morita/Basic.lean diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean new file mode 100644 index 0000000000000..bff0f79bded94 --- /dev/null +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -0,0 +1,105 @@ +/- +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.Basic +import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings + +/-! +# Morita equivalence + +We say that `R` and `S` are Morita equivalent if the categories of modules over `R` and `S` are +equivalent. In this file, we prove that Morita equivalence is an equivalence relation and that +isomorphic rings are Morita equivalent. + +# Main definitions + +- `MoritaEquivalent R S`: two rings `R` and `S` are Morita equivalent if their module categories + are equivalent. +- `IsMoritaEquivalent R S`: a predicate asserting that `R` and `S` are Morita equivalent. + +## TODO + +- For any ring `R`, `R` and `Matₙ(R)` are Morita equivalent. + +## References + +* [Nathan Jacobson, *Basic Algebra II*][jacobson1989] + +## Tags + +Morita Equivalence, Category Theory, Noncommutative Ring, Module Theory + +-/ + +universe v u₁ u₂ u₃ + +open CategoryTheory + +/-- +Two rings are Morita equivalent if their module categories are equivalent. +-/ +structure MoritaEquivalent (R : Type u₁) (S : Type u₂) [Ring R] [Ring S] where + /-- the underlying equivalence of category -/ + eqv : ModuleCat.{v} R ≌ ModuleCat.{v} S + +/-- +Two rings are Morita equivalent if their module categories are equivalent. +-/ +structure IsMoritaEquivalent (R : Type u₁) (S : Type u₂) [Ring R] [Ring S] : Prop where + cond : Nonempty <| MoritaEquivalent.{v} R S + +namespace MoritaEquivalent + +variable {R : Type u₁} [Ring R] {S : Type u₂} [Ring S] {T : Type u₃} [Ring T] + +/-- +Every ring is Morita equivalent to itself. +-/ +@[refl] +def refl : MoritaEquivalent R R where + eqv := CategoryTheory.Equivalence.refl (C := ModuleCat.{v} R) + +/-- +If `R` is Morita equivalent to `S`, then `S` is Morita equivalent to `R`. +-/ +@[symm] +def symm (e : MoritaEquivalent R S) : MoritaEquivalent S R where + eqv := e.eqv.symm + +/-- +If `R` is Morita equivalent to `S` and `S` is Morita equivalent to `T`, then `R` is Morita +equivalent to `T`. +-/ +@[trans] +def trans (e : MoritaEquivalent R S) (e' : MoritaEquivalent S T) : + MoritaEquivalent R T where + eqv := e.eqv.trans e'.eqv + +/-- +If `R` is isomorphic to `S` as rings, then `R` is Morita equivalent to `S`. +-/ +noncomputable def ofRingEquiv (f : R ≃+* S) : MoritaEquivalent R S where + eqv := ModuleCat.restrictScalarsEquivalenceOfRingEquiv f.symm + +end MoritaEquivalent + +namespace IsMoritaEquivalent + +variable {R : Type u₁} [Ring R] {S : Type u₂} [Ring S] {T : Type u₃} [Ring T] + +lemma refl : IsMoritaEquivalent R R where + cond := ⟨.refl⟩ + +lemma symm (h : IsMoritaEquivalent.{v} R S) : IsMoritaEquivalent.{v} S R where + cond := h.cond.map .symm + +lemma trans (h : IsMoritaEquivalent.{v} R S) (h' : IsMoritaEquivalent.{v} S T) : + IsMoritaEquivalent.{v} R T where + cond := Nonempty.map2 .trans h.cond h'.cond + +lemma of_ringEquiv (f : R ≃+* S) : IsMoritaEquivalent R S where + cond := ⟨.ofRingEquiv f⟩ + +end IsMoritaEquivalent From b5b09d20cd9bb82c0ffa950fa7cce5e24a69c02f Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Fri, 10 Jan 2025 19:13:43 +0000 Subject: [PATCH 02/37] fix build --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 7f0699745d63a..044bf8c7e25cc 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4552,6 +4552,7 @@ import Mathlib.RingTheory.Localization.NumDen import Mathlib.RingTheory.Localization.Submodule import Mathlib.RingTheory.MatrixAlgebra import Mathlib.RingTheory.MaximalSpectrum +import Mathlib.RingTheory.Morita.Basic import Mathlib.RingTheory.Multiplicity import Mathlib.RingTheory.MvPolynomial import Mathlib.RingTheory.MvPolynomial.Basic From 60c47ac5dec38cd4714f9adfe29467eaeaa95156 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Fri, 10 Jan 2025 22:05:12 +0000 Subject: [PATCH 03/37] apply suggestions --- Mathlib/RingTheory/Morita/Basic.lean | 43 ++++++++++++---------------- 1 file changed, 19 insertions(+), 24 deletions(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index bff0f79bded94..d132713c78523 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -15,7 +15,7 @@ isomorphic rings are Morita equivalent. # Main definitions -- `MoritaEquivalent R S`: two rings `R` and `S` are Morita equivalent if their module categories +- `MoritaEquivalence R S`: two rings `R` and `S` are Morita equivalent if their module categories are equivalent. - `IsMoritaEquivalent R S`: a predicate asserting that `R` and `S` are Morita equivalent. @@ -40,50 +40,45 @@ open CategoryTheory /-- Two rings are Morita equivalent if their module categories are equivalent. -/ -structure MoritaEquivalent (R : Type u₁) (S : Type u₂) [Ring R] [Ring S] where - /-- the underlying equivalence of category -/ - eqv : ModuleCat.{v} R ≌ ModuleCat.{v} S +def MoritaEquivalence (R : Type u₁) (S : Type u₂) [Ring R] [Ring S] := + ModuleCat.{v} R ≌ ModuleCat.{v} S /-- Two rings are Morita equivalent if their module categories are equivalent. -/ -structure IsMoritaEquivalent (R : Type u₁) (S : Type u₂) [Ring R] [Ring S] : Prop where - cond : Nonempty <| MoritaEquivalent.{v} R S +structure IsMoritaEquivalent (R : Type u₁) [Ring R] (S : Type u₂) [Ring S] : Prop where + cond : Nonempty <| MoritaEquivalence.{max u₁ u₂} R S -namespace MoritaEquivalent +namespace MoritaEquivalence variable {R : Type u₁} [Ring R] {S : Type u₂} [Ring S] {T : Type u₃} [Ring T] /-- Every ring is Morita equivalent to itself. -/ -@[refl] -def refl : MoritaEquivalent R R where - eqv := CategoryTheory.Equivalence.refl (C := ModuleCat.{v} R) +def refl : MoritaEquivalence R R := + CategoryTheory.Equivalence.refl (C := ModuleCat.{v} R) /-- If `R` is Morita equivalent to `S`, then `S` is Morita equivalent to `R`. -/ -@[symm] -def symm (e : MoritaEquivalent R S) : MoritaEquivalent S R where - eqv := e.eqv.symm +def symm (e : MoritaEquivalence R S) : MoritaEquivalence S R := + CategoryTheory.Equivalence.symm e /-- If `R` is Morita equivalent to `S` and `S` is Morita equivalent to `T`, then `R` is Morita equivalent to `T`. -/ -@[trans] -def trans (e : MoritaEquivalent R S) (e' : MoritaEquivalent S T) : - MoritaEquivalent R T where - eqv := e.eqv.trans e'.eqv +def trans (e : MoritaEquivalence R S) (e' : MoritaEquivalence S T) : MoritaEquivalence R T := + CategoryTheory.Equivalence.trans e e' /-- If `R` is isomorphic to `S` as rings, then `R` is Morita equivalent to `S`. -/ -noncomputable def ofRingEquiv (f : R ≃+* S) : MoritaEquivalent R S where - eqv := ModuleCat.restrictScalarsEquivalenceOfRingEquiv f.symm +noncomputable def ofRingEquiv (f : R ≃+* S) : MoritaEquivalence R S := + ModuleCat.restrictScalarsEquivalenceOfRingEquiv f.symm -end MoritaEquivalent +end MoritaEquivalence namespace IsMoritaEquivalent @@ -92,12 +87,12 @@ variable {R : Type u₁} [Ring R] {S : Type u₂} [Ring S] {T : Type u₃} [Ring lemma refl : IsMoritaEquivalent R R where cond := ⟨.refl⟩ -lemma symm (h : IsMoritaEquivalent.{v} R S) : IsMoritaEquivalent.{v} S R where +lemma symm (h : IsMoritaEquivalent R S) : IsMoritaEquivalent S R where cond := h.cond.map .symm -lemma trans (h : IsMoritaEquivalent.{v} R S) (h' : IsMoritaEquivalent.{v} S T) : - IsMoritaEquivalent.{v} R T where - cond := Nonempty.map2 .trans h.cond h'.cond +lemma trans (h : IsMoritaEquivalent R S) (h' : IsMoritaEquivalent S T) : + IsMoritaEquivalent R T where + cond := Nonempty.map2 (fun e e' ↦ MoritaEquivalence.trans e e') h.cond h'.cond lemma of_ringEquiv (f : R ≃+* S) : IsMoritaEquivalent R S where cond := ⟨.ofRingEquiv f⟩ From de693220aafd3349b027f9c364afb2b2ee58d9e5 Mon Sep 17 00:00:00 2001 From: zjj Date: Fri, 10 Jan 2025 22:38:13 +0000 Subject: [PATCH 04/37] inline --- Mathlib/RingTheory/Morita/Basic.lean | 50 ++++------------------------ 1 file changed, 6 insertions(+), 44 deletions(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index d132713c78523..a800d86f02d35 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -15,8 +15,6 @@ isomorphic rings are Morita equivalent. # Main definitions -- `MoritaEquivalence R S`: two rings `R` and `S` are Morita equivalent if their module categories - are equivalent. - `IsMoritaEquivalent R S`: a predicate asserting that `R` and `S` are Morita equivalent. ## TODO @@ -33,52 +31,15 @@ Morita Equivalence, Category Theory, Noncommutative Ring, Module Theory -/ -universe v u₁ u₂ u₃ +universe u₁ u₂ u₃ open CategoryTheory -/-- -Two rings are Morita equivalent if their module categories are equivalent. --/ -def MoritaEquivalence (R : Type u₁) (S : Type u₂) [Ring R] [Ring S] := - ModuleCat.{v} R ≌ ModuleCat.{v} S - /-- Two rings are Morita equivalent if their module categories are equivalent. -/ structure IsMoritaEquivalent (R : Type u₁) [Ring R] (S : Type u₂) [Ring S] : Prop where - cond : Nonempty <| MoritaEquivalence.{max u₁ u₂} R S - -namespace MoritaEquivalence - -variable {R : Type u₁} [Ring R] {S : Type u₂} [Ring S] {T : Type u₃} [Ring T] - -/-- -Every ring is Morita equivalent to itself. --/ -def refl : MoritaEquivalence R R := - CategoryTheory.Equivalence.refl (C := ModuleCat.{v} R) - -/-- -If `R` is Morita equivalent to `S`, then `S` is Morita equivalent to `R`. --/ -def symm (e : MoritaEquivalence R S) : MoritaEquivalence S R := - CategoryTheory.Equivalence.symm e - -/-- -If `R` is Morita equivalent to `S` and `S` is Morita equivalent to `T`, then `R` is Morita -equivalent to `T`. --/ -def trans (e : MoritaEquivalence R S) (e' : MoritaEquivalence S T) : MoritaEquivalence R T := - CategoryTheory.Equivalence.trans e e' - -/-- -If `R` is isomorphic to `S` as rings, then `R` is Morita equivalent to `S`. --/ -noncomputable def ofRingEquiv (f : R ≃+* S) : MoritaEquivalence R S := - ModuleCat.restrictScalarsEquivalenceOfRingEquiv f.symm - -end MoritaEquivalence + cond : Nonempty <| ModuleCat.{max u₁ u₂} R ≌ ModuleCat.{max u₁ u₂} S namespace IsMoritaEquivalent @@ -90,11 +51,12 @@ lemma refl : IsMoritaEquivalent R R where lemma symm (h : IsMoritaEquivalent R S) : IsMoritaEquivalent S R where cond := h.cond.map .symm -lemma trans (h : IsMoritaEquivalent R S) (h' : IsMoritaEquivalent S T) : +lemma trans {R S T : Type u₁} [Ring R] [Ring S] [Ring T] + (h : IsMoritaEquivalent R S) (h' : IsMoritaEquivalent S T) : IsMoritaEquivalent R T where - cond := Nonempty.map2 (fun e e' ↦ MoritaEquivalence.trans e e') h.cond h'.cond + cond := Nonempty.map2 .trans h.cond h'.cond lemma of_ringEquiv (f : R ≃+* S) : IsMoritaEquivalent R S where - cond := ⟨.ofRingEquiv f⟩ + cond := ⟨ModuleCat.restrictScalarsEquivalenceOfRingEquiv f.symm⟩ end IsMoritaEquivalent From 6af581cf53ac3f230074a6a16653b0b49ced4b34 Mon Sep 17 00:00:00 2001 From: zjj Date: Fri, 10 Jan 2025 22:48:32 +0000 Subject: [PATCH 05/37] add todo --- Mathlib/RingTheory/Morita/Basic.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index a800d86f02d35..7d9c070bc78b4 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -20,6 +20,9 @@ isomorphic rings 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. +- If `R ≈ S`, then `R` is simple iff `S` is simple. ## References @@ -51,6 +54,8 @@ lemma refl : IsMoritaEquivalent R R where lemma symm (h : IsMoritaEquivalent R S) : IsMoritaEquivalent S R where cond := h.cond.map .symm +-- TODO: We have restricted universe here, but if we have more Mortia Equivalence in terms full +-- idempotents, we could remove the restriction. lemma trans {R S T : Type u₁} [Ring R] [Ring S] [Ring T] (h : IsMoritaEquivalent R S) (h' : IsMoritaEquivalent S T) : IsMoritaEquivalent R T where From a66deb6a8a34a59ff9afc0ea55aaefc337f617d3 Mon Sep 17 00:00:00 2001 From: zjj Date: Mon, 13 Jan 2025 10:19:28 +0000 Subject: [PATCH 06/37] add 1 --- Mathlib/RingTheory/Morita/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 7d9c070bc78b4..721888574e63f 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -22,6 +22,7 @@ isomorphic rings are Morita equivalent. - 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 From ab44429b94e67d0691d066543838c6a80a9556e4 Mon Sep 17 00:00:00 2001 From: zjj Date: Mon, 13 Jan 2025 10:25:01 +0000 Subject: [PATCH 07/37] change --- Mathlib/RingTheory/Morita/Basic.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 721888574e63f..45df6633a761c 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -55,8 +55,13 @@ lemma refl : IsMoritaEquivalent R R where lemma symm (h : IsMoritaEquivalent R S) : IsMoritaEquivalent S R where cond := h.cond.map .symm --- TODO: We have restricted universe here, but if we have more Mortia Equivalence in terms full --- idempotents, we could remove the restriction. +-- 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 if we once we proved the definition of Mortia +-- equivalence is equivalent to the existence of a full idempotent element, we can remove this +-- restriction in the universe. +-- Or alternatively, @alreadyone has sketched an argument on how the universe restriction can be +-- removed via a categorical arguemnt, +-- see [here](https://github.com/leanprover-community/mathlib4/pull/20640#discussion_r1912189931) lemma trans {R S T : Type u₁} [Ring R] [Ring S] [Ring T] (h : IsMoritaEquivalent R S) (h' : IsMoritaEquivalent S T) : IsMoritaEquivalent R T where From 2e80c78294d1aa21fcbf79c676a71404c45c6f0b Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 13 Jan 2025 14:05:28 +0000 Subject: [PATCH 08/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/RingTheory/Morita/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 45df6633a761c..d31a2f458c4ef 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -56,11 +56,11 @@ lemma symm (h : IsMoritaEquivalent R S) : IsMoritaEquivalent S R where cond := h.cond.map .symm -- 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 if we once we proved the definition of Mortia --- equivalence is equivalent to the existence of a full idempotent element, we can remove this +-- `max u₁ u₂`, `max u₂ u₃` vs `max u₁ u₃`. But if we 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, @alreadyone has sketched an argument on how the universe restriction can be --- removed via a categorical arguemnt, +-- Or alternatively, @alreadydone one 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) lemma trans {R S T : Type u₁} [Ring R] [Ring S] [Ring T] (h : IsMoritaEquivalent R S) (h' : IsMoritaEquivalent S T) : From 90c9112a646d9c66da5446fc4257b6ae0c27f447 Mon Sep 17 00:00:00 2001 From: zjj Date: Wed, 15 Jan 2025 12:29:51 +0000 Subject: [PATCH 09/37] shorten line --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index d31a2f458c4ef..690d5cfdc4561 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -59,7 +59,7 @@ lemma symm (h : IsMoritaEquivalent R S) : IsMoritaEquivalent S R where -- `max u₁ u₂`, `max u₂ u₃` vs `max u₁ u₃`. But if we 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 one has sketched an argument on how the universe restriction can be +-- 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) lemma trans {R S T : Type u₁} [Ring R] [Ring S] [Ring T] From 273aaa7cc61273268e27d879a36bafb38b72f6dc Mon Sep 17 00:00:00 2001 From: zjj Date: Sat, 18 Jan 2025 16:27:18 +0000 Subject: [PATCH 10/37] generalize --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 28 ++++- .../Category/ModuleCat/ChangeOfRings.lean | 20 ++++ Mathlib/RingTheory/Morita/Basic.lean | 110 ++++++++++++++---- 3 files changed, 132 insertions(+), 26 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index 9d0fdd30373c1..77d6eed68e674 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -424,16 +424,36 @@ end Module section -variable {S : Type u} [CommRing S] +universe u₀ + +section + +variable {S₀ : Type u₀} [CommRing S₀] {S : Type u} [Ring S] [Algebra S₀ S] variable {M N : ModuleCat.{v} S} -instance : Linear S (ModuleCat.{v} S) where +instance : Module S₀ M := Module.compHom _ (algebraMap S₀ S) +instance : SMulCommClass S S₀ M := + { 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] } + +instance : Linear S₀ (ModuleCat.{v} S) where + smul_comp _ M N s₀ f g := by + ext + simp [show ∀ (m : M), s₀ • m = algebraMap S₀ S s₀ • m by intros; rfl, + show ∀ (n : N), s₀ • n = algebraMap S₀ S s₀ • n by intros; rfl] + +end + +section + +variable {S : Type u} [CommRing S] variable {X Y X' Y' : ModuleCat.{v} S} theorem Iso.homCongr_eq_arrowCongr (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y) : - Iso.homCongr i j f = ⟨LinearEquiv.arrowCongr i.toLinearEquiv j.toLinearEquiv f.hom⟩ := + Iso.homCongr i j f = ⟨LinearEquiv.arrowCongr (R := S) i.toLinearEquiv j.toLinearEquiv f.hom⟩ := rfl theorem Iso.conj_eq_conj (i : X ≅ X') (f : End X) : @@ -442,6 +462,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 monoids. -/ diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index b922ed2155138..55b05121cbb9a 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/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,25 @@ instance restrictScalars_isEquivalence_of_ringEquiv {R S} [Ring R] [Ring S] (e : (ModuleCat.restrictScalars e.toRingHom).IsEquivalence := (restrictScalarsEquivalenceOfRingEquiv e).isEquivalence_functor +instance restrictScalarsEquivalenceOfRingEquiv_additive {R S} [Ring R] [Ring S] (e : R ≃+* S) : + (restrictScalarsEquivalenceOfRingEquiv e).functor.Additive where + +instance restrictScalarsEquivalenceOfRingEquiv_linear + {R₀ R S} [CommRing R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S] + (e : R ≃ₐ[R₀] S) : + (restrictScalarsEquivalenceOfRingEquiv e.toRingEquiv).functor.Linear R₀ where + map_smul {M N} f r₀ := by + ext m + simp only [AlgEquiv.toRingEquiv_eq_coe, restrictScalarsEquivalenceOfRingEquiv, + RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, AddEquiv.toEquiv_eq_coe, + Equiv.toFun_as_coe, EquivLike.coe_coe, Equiv.invFun_as_coe, AddEquiv.coe_toEquiv_symm, + AddEquiv.coe_refl, AddEquiv.refl_symm, restrictScalars.map_apply, hom_smul, + LinearMap.smul_apply] + show algebraMap _ _ r₀ • _ = e (algebraMap _ _ r₀) • f.hom m + rw [AlgEquiv.commutes] + rfl + + open TensorProduct variable {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 690d5cfdc4561..9352580c63929 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -3,19 +3,23 @@ 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.Basic import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings +import Mathlib.CategoryTheory.Linear.LinearFunctor +import Mathlib.Algebra.Category.ModuleCat.Basic /-! # Morita equivalence -We say that `R` and `S` are Morita equivalent if the categories of modules over `R` and `S` are -equivalent. In this file, we prove that Morita equivalence is an equivalence relation and that -isomorphic rings are Morita equivalent. +For 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 -- `IsMoritaEquivalent R S`: a predicate asserting that `R` and `S` are Morita equivalent. +- `MoritaEquivalence R A B`: a structure containing a `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 @@ -35,25 +39,41 @@ Morita Equivalence, Category Theory, Noncommutative Ring, Module Theory -/ -universe u₁ u₂ u₃ +universe u₀ u₁ u₂ u₃ open CategoryTheory -/-- -Two rings are Morita equivalent if their module categories are equivalent. --/ -structure IsMoritaEquivalent (R : Type u₁) [Ring R] (S : Type u₂) [Ring S] : Prop where - cond : Nonempty <| ModuleCat.{max u₁ u₂} R ≌ ModuleCat.{max u₁ u₂} S +variable (R : Type u₀) [CommRing R] -namespace IsMoritaEquivalent +@[ext] +structure MoritaEquivalence + (A : Type u₁) [Ring A] [Algebra R A] + (B : Type u₂) [Ring B] [Algebra R B] where + eqv : ModuleCat.{max u₁ u₂} A ≌ ModuleCat.{max u₁ u₂} B + additive : eqv.functor.Additive := by infer_instance + linear : eqv.functor.Linear R := by infer_instance -variable {R : Type u₁} [Ring R] {S : Type u₂} [Ring S] {T : Type u₃} [Ring T] +namespace MoritaEquivalence -lemma refl : IsMoritaEquivalent R R where - cond := ⟨.refl⟩ +attribute [instance] MoritaEquivalence.additive MoritaEquivalence.linear -lemma symm (h : IsMoritaEquivalent R S) : IsMoritaEquivalent S R where - cond := h.cond.map .symm +/-- +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 + additive := CategoryTheory.Functor.instAdditiveId + linear := CategoryTheory.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 + additive := e.eqv.inverse_additive + 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 if we once we proved the definition of Morita @@ -62,12 +82,56 @@ lemma symm (h : IsMoritaEquivalent R S) : IsMoritaEquivalent S R where -- 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) -lemma trans {R S T : Type u₁} [Ring R] [Ring S] [Ring T] - (h : IsMoritaEquivalent R S) (h' : IsMoritaEquivalent S T) : - IsMoritaEquivalent R T where - cond := Nonempty.map2 .trans h.cond h'.cond +/-- +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 + additive := Functor.instAdditiveComp e.eqv.functor e'.eqv.functor + linear := Functor.instLinearComp e.eqv.functor e'.eqv.functor + +variable {R} in +/-- +Equivalence `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.restrictScalarsEquivalenceOfRingEquiv_linear f.symm + +end MoritaEquivalence + +/-- +Two rings are Morita equivalent if their module categories are equivalent. +-/ +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 + +-- variable {A : Type u₁} [Ring R] {B : Type u₂} [Ring B] {C : Type u₃} [Ring T] + +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_ringEquiv (f : R ≃+* S) : IsMoritaEquivalent R S where - cond := ⟨ModuleCat.restrictScalarsEquivalenceOfRingEquiv f.symm⟩ +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 From 13696f4fd348fc935bca2f20c45538ba60c39195 Mon Sep 17 00:00:00 2001 From: zjj Date: Sat, 18 Jan 2025 17:21:54 +0000 Subject: [PATCH 11/37] test --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index 77d6eed68e674..e081621b3a344 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -426,30 +426,33 @@ section universe u₀ -section +namespace Algebra variable {S₀ : Type u₀} [CommRing S₀] {S : Type u} [Ring S] [Algebra S₀ S] variable {M N : ModuleCat.{v} S} -instance : Module S₀ M := Module.compHom _ (algebraMap S₀ S) -instance : SMulCommClass S S₀ M := +scoped instance : Module S₀ M := Module.compHom _ (algebraMap S₀ S) + +scoped instance : SMulCommClass S S₀ M := { 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] } -instance : Linear S₀ (ModuleCat.{v} S) where +scoped instance instLinear : Linear S₀ (ModuleCat.{v} S) where smul_comp _ M N s₀ f g := by ext simp [show ∀ (m : M), s₀ • m = algebraMap S₀ S s₀ • m by intros; rfl, show ∀ (n : N), s₀ • n = algebraMap S₀ S s₀ • n by intros; rfl] -end +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} theorem Iso.homCongr_eq_arrowCongr (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y) : From 7d58c6634712bff28eb9db2e0de64b0ac5df770c Mon Sep 17 00:00:00 2001 From: zjj Date: Sat, 18 Jan 2025 22:58:29 +0000 Subject: [PATCH 12/37] fix? --- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean | 5 ++++- Mathlib/RingTheory/Morita/Basic.lean | 4 +++- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index 55b05121cbb9a..ceb71b0d05b44 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -268,7 +268,9 @@ instance restrictScalars_isEquivalence_of_ringEquiv {R S} [Ring R] [Ring S] (e : instance restrictScalarsEquivalenceOfRingEquiv_additive {R S} [Ring R] [Ring S] (e : R ≃+* S) : (restrictScalarsEquivalenceOfRingEquiv e).functor.Additive where -instance restrictScalarsEquivalenceOfRingEquiv_linear +namespace Algebra + +scoped instance restrictScalarsEquivalenceOfRingEquiv_linear {R₀ R S} [CommRing R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S] (e : R ≃ₐ[R₀] S) : (restrictScalarsEquivalenceOfRingEquiv e.toRingEquiv).functor.Linear R₀ where @@ -283,6 +285,7 @@ instance restrictScalarsEquivalenceOfRingEquiv_linear rw [AlgEquiv.commutes] rfl +end Algebra open TensorProduct diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 9352580c63929..84327c882c077 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -45,6 +45,8 @@ open CategoryTheory variable (R : Type u₀) [CommRing R] +open scoped ModuleCat.Algebra + @[ext] structure MoritaEquivalence (A : Type u₁) [Ring A] [Algebra R A] @@ -102,7 +104,7 @@ 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.restrictScalarsEquivalenceOfRingEquiv_linear f.symm + linear := ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear f.symm end MoritaEquivalence From f79a4f2be0884b43193229363ae124928a352b4e Mon Sep 17 00:00:00 2001 From: zjj Date: Sat, 18 Jan 2025 23:11:36 +0000 Subject: [PATCH 13/37] fix --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 6 ++++++ Mathlib/RingTheory/Morita/Basic.lean | 5 +++++ 2 files changed, 11 insertions(+) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index e081621b3a344..e8e7498158e0e 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -432,6 +432,9 @@ variable {S₀ : Type u₀} [CommRing S₀] {S : Type u} [Ring S] [Algebra S₀ variable {M N : ModuleCat.{v} S} +/-- +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 : SMulCommClass S S₀ M := @@ -439,6 +442,9 @@ scoped instance : SMulCommClass S S₀ M := 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 diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 84327c882c077..c647f7cbf2605 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -47,10 +47,15 @@ variable (R : Type u₀) [CommRing R] open scoped ModuleCat.Algebra +/-- +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 category. +-/ @[ext] structure MoritaEquivalence (A : Type u₁) [Ring A] [Algebra R A] (B : Type u₂) [Ring B] [Algebra R B] where + /--the underlying equivalence of category-/ eqv : ModuleCat.{max u₁ u₂} A ≌ ModuleCat.{max u₁ u₂} B additive : eqv.functor.Additive := by infer_instance linear : eqv.functor.Linear R := by infer_instance From d7d9043aede199777aafcb4a524b5b507a674e1d Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 22 Jan 2025 23:41:31 +0000 Subject: [PATCH 14/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Eric Wieser --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index c647f7cbf2605..48703558e9fb3 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -137,7 +137,7 @@ lemma trans {A B C : Type u₁} [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebr 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] +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⟩ From d1f7a09b4ba422af24b251bdb393928ddbb3de3a Mon Sep 17 00:00:00 2001 From: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Date: Fri, 24 Jan 2025 11:19:40 +0000 Subject: [PATCH 15/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 48703558e9fb3..bda659f93159a 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -49,7 +49,7 @@ open scoped ModuleCat.Algebra /-- 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 category. +`A`-modules and `B`-modules are equivalent as `R`-linear categories. -/ @[ext] structure MoritaEquivalence From 8a3322222f4fd5d4ca8bfdfed49354b2108034f1 Mon Sep 17 00:00:00 2001 From: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Date: Fri, 24 Jan 2025 11:19:48 +0000 Subject: [PATCH 16/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index bda659f93159a..9e49fe466be11 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -83,7 +83,7 @@ def symm {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebr 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 if we once we proved the definition of Morita +-- `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 From 68ba2a3567ea33515a5cb495f3ca1f841df1b2d9 Mon Sep 17 00:00:00 2001 From: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Date: Fri, 24 Jan 2025 11:19:55 +0000 Subject: [PATCH 17/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 9e49fe466be11..01e7502edc7d3 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -103,7 +103,7 @@ def trans {A B C : Type u₁} variable {R} in /-- -Equivalence `R`-algebras are Morita equivalent. +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) : From f0552fed0e376dfd0ad5f32e26cdb196da915061 Mon Sep 17 00:00:00 2001 From: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Date: Sat, 25 Jan 2025 19:58:39 +0000 Subject: [PATCH 18/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 01e7502edc7d3..165c8346a360b 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -55,7 +55,7 @@ Let `A` and `B` be `R`-algebras. We say that `A` and `B` are Morita equivalent i structure MoritaEquivalence (A : Type u₁) [Ring A] [Algebra R A] (B : Type u₂) [Ring B] [Algebra R B] where - /--the underlying equivalence of category-/ + /--the underlying equivalence of categories-/ eqv : ModuleCat.{max u₁ u₂} A ≌ ModuleCat.{max u₁ u₂} B additive : eqv.functor.Additive := by infer_instance linear : eqv.functor.Linear R := by infer_instance From 2344c2a415db701f55d3e769f5e6d6d158dca2f2 Mon Sep 17 00:00:00 2001 From: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Date: Sat, 25 Jan 2025 20:01:17 +0000 Subject: [PATCH 19/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 165c8346a360b..c48bbe6bff6d3 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -106,7 +106,7 @@ 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) : + [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 From d2f7b466f73a6a0f25e4f2b307b1805f0e242359 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Sat, 25 Jan 2025 23:46:10 +0000 Subject: [PATCH 20/37] Update Mathlib/Algebra/Category/ModuleCat/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index e8e7498158e0e..f4f59e532be42 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -428,7 +428,7 @@ universe u₀ namespace Algebra -variable {S₀ : Type u₀} [CommRing S₀] {S : Type u} [Ring S] [Algebra S₀ S] +variable {S₀ : Type u₀} [CommSemiring S₀] {S : Type u} [Ring S] [Algebra S₀ S] variable {M N : ModuleCat.{v} S} From 5ded14d87e781c36f67f7b3896e0b4c1b53fc321 Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Mon, 3 Feb 2025 02:16:04 +0000 Subject: [PATCH 21/37] junyan suggestion --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 8 ++++---- Mathlib/RingTheory/Morita/Basic.lean | 2 -- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index 68d9c1ce7cc81..bc67c5fd082d6 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -451,10 +451,10 @@ 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 : SMulCommClass S S₀ M := - { 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] } +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. diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index c48bbe6bff6d3..d55a9bbba4640 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -123,8 +123,6 @@ structure IsMoritaEquivalent namespace IsMoritaEquivalent --- variable {A : Type u₁} [Ring R] {B : Type u₂} [Ring B] {C : Type u₃} [Ring T] - lemma refl {A : Type u₁} [Ring A] [Algebra R A] : IsMoritaEquivalent R A A where cond := ⟨.refl R A⟩ From 99a4bf2527c39cb25bd89fda33b978e3e73a5754 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 3 Feb 2025 20:22:17 +0000 Subject: [PATCH 22/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index d55a9bbba4640..6a3d190eb45c3 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -43,7 +43,7 @@ universe u₀ u₁ u₂ u₃ open CategoryTheory -variable (R : Type u₀) [CommRing R] +variable (R : Type u₀) [CommSemiring R] open scoped ModuleCat.Algebra From 6c348321a6938478ec0984b6cf95d74ced412950 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 3 Feb 2025 20:22:26 +0000 Subject: [PATCH 23/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/RingTheory/Morita/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 6a3d190eb45c3..c86674cd9e21a 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -48,8 +48,8 @@ variable (R : Type u₀) [CommSemiring R] open scoped ModuleCat.Algebra /-- -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. +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. -/ @[ext] structure MoritaEquivalence From dffcf77b068ce32b4405d5e427ae1558661d542b Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Mon, 3 Feb 2025 20:22:35 +0000 Subject: [PATCH 24/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Junyan Xu --- Mathlib/RingTheory/Morita/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index c86674cd9e21a..4fd29bd1c3b4b 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -114,7 +114,8 @@ noncomputable def ofAlgEquiv {A : Type u₁} {B : Type u₂} end MoritaEquivalence /-- -Two rings are Morita equivalent if their module categories are equivalent. +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] From 54cac5f537c4896d7607192991af749feee93827 Mon Sep 17 00:00:00 2001 From: zjj Date: Mon, 3 Feb 2025 20:47:38 +0000 Subject: [PATCH 25/37] apply suggestions from @alreadydone --- .../Algebra/Category/ModuleCat/ChangeOfRings.lean | 2 +- Mathlib/RingTheory/Morita/Basic.lean | 13 +++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index 0a7d4fbb89cee..c70832211c50b 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -271,7 +271,7 @@ instance restrictScalarsEquivalenceOfRingEquiv_additive {R S} [Ring R] [Ring S] namespace Algebra scoped instance restrictScalarsEquivalenceOfRingEquiv_linear - {R₀ R S} [CommRing R₀] [Ring R] [Ring S] [Algebra R₀ R] [Algebra R₀ S] + {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₀ where map_smul {M N} f r₀ := by diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 4fd29bd1c3b4b..495a55c71ac03 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -6,6 +6,7 @@ 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 @@ -57,19 +58,21 @@ structure MoritaEquivalence (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 - additive : eqv.functor.Additive := by infer_instance - linear : eqv.functor.Linear R := by infer_instance + linear : + haveI := eqv.functor.additive_of_preserves_binary_products + eqv.functor.Linear R := by infer_instance namespace MoritaEquivalence -attribute [instance] MoritaEquivalence.additive MoritaEquivalence.linear +attribute [scoped instance] CategoryTheory.Functor.additive_of_preserves_binary_products + +attribute [instance] MoritaEquivalence.linear /-- 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 - additive := CategoryTheory.Functor.instAdditiveId linear := CategoryTheory.Functor.instLinearId /-- @@ -79,7 +82,6 @@ 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 - additive := e.eqv.inverse_additive linear := e.eqv.inverseLinear R -- TODO: We have restricted all the rings to the same universe here because of the complication @@ -98,7 +100,6 @@ def trans {A B C : Type u₁} (e : MoritaEquivalence R A B) (e' : MoritaEquivalence R B C) : MoritaEquivalence R A C where eqv := e.eqv.trans e'.eqv - additive := Functor.instAdditiveComp e.eqv.functor e'.eqv.functor linear := Functor.instLinearComp e.eqv.functor e'.eqv.functor variable {R} in From c7b5292b732e96c24e91e4970fb46f195561d0a6 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 3 Feb 2025 22:09:24 +0000 Subject: [PATCH 26/37] Remove Functor.Additive from def of Functor.Linear --- Mathlib/CategoryTheory/Linear/LinearFunctor.lean | 10 +++++----- Mathlib/RingTheory/Morita/Basic.lean | 14 +++++++------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Mathlib/CategoryTheory/Linear/LinearFunctor.lean b/Mathlib/CategoryTheory/Linear/LinearFunctor.lean index 0e58e65be5bae..bd49e0f79130c 100644 --- a/Mathlib/CategoryTheory/Linear/LinearFunctor.lean +++ b/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 diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 495a55c71ac03..fe781b6800245 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -58,22 +58,22 @@ structure MoritaEquivalence (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 : - haveI := eqv.functor.additive_of_preserves_binary_products - eqv.functor.Linear R := by infer_instance + linear : eqv.functor.Linear R := by infer_instance namespace MoritaEquivalence -attribute [scoped instance] CategoryTheory.Functor.additive_of_preserves_binary_products - 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 := CategoryTheory.Functor.instLinearId + linear := Functor.instLinearId /-- For any `R`-algebras `A` and `B`, if `A` is Morita equivalent to `B`, then `B` is Morita equivalent @@ -100,7 +100,7 @@ def trans {A B C : Type u₁} (e : MoritaEquivalence R A B) (e' : MoritaEquivalence R B C) : MoritaEquivalence R A C where eqv := e.eqv.trans e'.eqv - linear := Functor.instLinearComp e.eqv.functor e'.eqv.functor + linear := e.eqv.functor.instLinearComp e'.eqv.functor variable {R} in /-- From e5564036fd7f981355441bba60f6f8f82f426482 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 4 Feb 2025 00:13:07 +0000 Subject: [PATCH 27/37] unused arguments --- Mathlib/CategoryTheory/Action/Limits.lean | 2 +- Mathlib/CategoryTheory/Monoidal/Linear.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Action/Limits.lean b/Mathlib/CategoryTheory/Action/Limits.lean index 22a33887e6908..b355201ab7473 100644 --- a/Mathlib/CategoryTheory/Action/Limits.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Monoidal/Linear.lean b/Mathlib/CategoryTheory/Monoidal/Linear.lean index ca1021e4d0881..e1a028736ecd2 100644 --- a/Mathlib/CategoryTheory/Monoidal/Linear.lean +++ b/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 From 47ce0e000ea986137015bda9c45ecb3abe430ae8 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 4 Feb 2025 00:29:58 +0000 Subject: [PATCH 28/37] golf `restrictScalarsEquivalenceOfRingEquiv_linear` --- .../Category/ModuleCat/ChangeOfRings.lean | 24 ++++++++----------- 1 file changed, 10 insertions(+), 14 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index c70832211c50b..8d5a657b4b077 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -265,25 +265,21 @@ 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 -scoped 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₀ where - map_smul {M N} f r₀ := by - ext m - simp only [AlgEquiv.toRingEquiv_eq_coe, restrictScalarsEquivalenceOfRingEquiv, - RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, AddEquiv.toEquiv_eq_coe, - Equiv.toFun_as_coe, EquivLike.coe_coe, Equiv.invFun_as_coe, AddEquiv.coe_toEquiv_symm, - AddEquiv.coe_refl, AddEquiv.refl_symm, restrictScalars.map_apply, hom_smul, - LinearMap.smul_apply] - show algebraMap _ _ r₀ • _ = e (algebraMap _ _ r₀) • f.hom m - rw [AlgEquiv.commutes] - rfl +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 From 50cb794dea9a223cd632132dba2eabe73794de58 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 4 Feb 2025 15:51:00 +0000 Subject: [PATCH 29/37] Update Mathlib/RingTheory/Morita/Basic.lean --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index fe781b6800245..7108116feb851 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -17,7 +17,7 @@ relation and that isomorphic algebras are Morita equivalent. # Main definitions -- `MoritaEquivalence R A B`: a structure containing a `R`-linear equivalence of categories between +- `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. From bf8230e938f1e2cf2df59584b14833889569011e Mon Sep 17 00:00:00 2001 From: zjj Date: Tue, 4 Feb 2025 15:56:41 +0000 Subject: [PATCH 30/37] remove ext --- Mathlib/RingTheory/Morita/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index fe781b6800245..b08cfda2de307 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -52,7 +52,6 @@ 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. -/ -@[ext] structure MoritaEquivalence (A : Type u₁) [Ring A] [Algebra R A] (B : Type u₂) [Ring B] [Algebra R B] where From d046381c68f524aab163bc57afe9852a90a9e013 Mon Sep 17 00:00:00 2001 From: zjj Date: Tue, 4 Feb 2025 18:00:20 +0000 Subject: [PATCH 31/37] revert --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index bc67c5fd082d6..ace4f8d623b25 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -476,7 +476,7 @@ instance : Linear S (ModuleCat.{v} S) := ModuleCat.Algebra.instLinear variable {X Y X' Y' : ModuleCat.{v} S} theorem Iso.homCongr_eq_arrowCongr (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y) : - Iso.homCongr i j f = ⟨LinearEquiv.arrowCongr (R := S) i.toLinearEquiv j.toLinearEquiv f.hom⟩ := + Iso.homCongr i j f = ⟨LinearEquiv.arrowCongr i.toLinearEquiv j.toLinearEquiv f.hom⟩ := rfl theorem Iso.conj_eq_conj (i : X ≅ X') (f : End X) : From e914cb1b6dfc7b358d39fb4e9988dbb1f12fdec4 Mon Sep 17 00:00:00 2001 From: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Date: Wed, 5 Feb 2025 01:24:32 +0000 Subject: [PATCH 32/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Kim Morrison --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 553671fadfc6c..b6cb11aef1efe 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -55,7 +55,7 @@ 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-/ + /-- The underlying equivalence of categories -/ eqv : ModuleCat.{max u₁ u₂} A ≌ ModuleCat.{max u₁ u₂} B linear : eqv.functor.Linear R := by infer_instance From 8717ed548d89fa758f5bb54918bb0a83135dbfae Mon Sep 17 00:00:00 2001 From: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Date: Wed, 5 Feb 2025 15:35:08 +0000 Subject: [PATCH 33/37] Update Mathlib/RingTheory/Morita/Basic.lean Co-authored-by: Johan Commelin --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index b6cb11aef1efe..55dce91776b2b 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -11,7 +11,7 @@ import Mathlib.CategoryTheory.Adjunction.Limits /-! # Morita equivalence -For two `R`-algebras `A` and `B` are Morita equivalent if the categories of modules over `A` and +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. From d3807df73f542b520d1b365f969b3ac07486b697 Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Sat, 8 Feb 2025 17:24:18 +0000 Subject: [PATCH 34/37] apply kevin's suggestion --- Mathlib/RingTheory/Morita/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Morita/Basic.lean b/Mathlib/RingTheory/Morita/Basic.lean index 55dce91776b2b..a780af81b7546 100644 --- a/Mathlib/RingTheory/Morita/Basic.lean +++ b/Mathlib/RingTheory/Morita/Basic.lean @@ -124,7 +124,7 @@ structure IsMoritaEquivalent namespace IsMoritaEquivalent -lemma refl {A : Type u₁} [Ring A] [Algebra R A] : IsMoritaEquivalent R A A where +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] From eb6ad793249bb7a3645bd81283c6a83a2dc66aa2 Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Wed, 12 Feb 2025 21:12:40 +0000 Subject: [PATCH 35/37] apply andrew advice --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index bfdc7b5608d72..d3b3b8774451f 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -9,6 +9,7 @@ import Mathlib.Algebra.PUnitInstances.Module import Mathlib.CategoryTheory.Conj import Mathlib.CategoryTheory.Linear.Basic import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor +import Mathlib.Algebra.Algebra.Tower /-! # The category of `R`-modules @@ -445,19 +446,14 @@ 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 : 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] +scoped instance : IsScalarTower S₀ S M := by + exact IsScalarTower.of_algebraMap_smul <| fun _ _ ↦ rfl /-- 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 [show ∀ (m : M), s₀ • m = algebraMap S₀ S s₀ • m by intros; rfl, - show ∀ (n : N), s₀ • n = algebraMap S₀ S s₀ • n by intros; rfl] + smul_comp _ M N s₀ f g := by ext; simp end Algebra From fb514707f4ca782e8f4f4bda6208a3db19025d91 Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Wed, 12 Feb 2025 21:41:27 +0000 Subject: [PATCH 36/37] fix? --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index d3b3b8774451f..0f6e3452890ae 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -9,7 +9,7 @@ import Mathlib.Algebra.PUnitInstances.Module import Mathlib.CategoryTheory.Conj import Mathlib.CategoryTheory.Linear.Basic import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor -import Mathlib.Algebra.Algebra.Tower +import Mathlib.Algebra.Algebra.Basic /-! # The category of `R`-modules @@ -446,8 +446,8 @@ 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 := by - exact IsScalarTower.of_algebraMap_smul <| fun _ _ ↦ rfl +scoped instance : IsScalarTower S₀ S M where + smul_assoc _ _ _ := by rw [Algebra.smul_def, mul_smul]; rfl /-- Let `S` be an `S₀`-algebra. Then the category of `S`-modules is `S₀`-linear. From 84846a127308df8f9b78ebbb0da134a6f5067e21 Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Wed, 12 Feb 2025 22:58:27 +0000 Subject: [PATCH 37/37] fix large import --- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index 0f6e3452890ae..80e4f287e0321 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -9,7 +9,6 @@ import Mathlib.Algebra.PUnitInstances.Module import Mathlib.CategoryTheory.Conj import Mathlib.CategoryTheory.Linear.Basic import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor -import Mathlib.Algebra.Algebra.Basic /-! # The category of `R`-modules @@ -449,6 +448,11 @@ 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. -/