LeanPool.BrauerGroupNew.Morita.TensorProduct

Imported Lean Pool material for LeanPool.BrauerGroupNew.Morita.TensorProduct.

@[simp]

theorem ModuleCat.ofHom_smul {R : Type u_1} {S : Type u_2} [Ring R] [Semiring S] {M N : ModuleCat R} [Module S ↑N] [SMulCommClass R S ↑N] (r : S) (f : ↑M →ₗ[R] ↑N) : ofHom (r • f) = r • ofHom f

Bundling a scaled linear map agrees with scaling the bundled morphism.

@[implicit_reducible]

noncomputable instance Morita.instModuleCarrierLeanPool (R : Type u) [CommRing R] (B : Type v) [Ring B] [Algebra R B] (N : ModuleCat B) : Module R ↑N

Equations

• Morita.instModuleCarrierLeanPool R B N = Module.compHom (↑N) (algebraMap R B)

instance Morita.instIsScalarTowerCarrier_leanPool (R : Type u) [CommRing R] (B : Type v) [Ring B] [Algebra R B] (N : ModuleCat B) : IsScalarTower R B ↑N

@[reducible, inline]

noncomputable abbrev Morita.aux0 (R : Type u) [CommRing R] (A B : Type v) [Ring A] [Ring B] [Algebra R A] [Algebra R B] (e1 : CategoryTheory.Functor (ModuleCat A) (ModuleCat B)) [e1.Additive] [CategoryTheory.Functor.Linear R e1] (N : ModuleCat A) : Module.End A ↑N →ₐ[R] Module.End B ↑(e1.obj N)

Transport endomorphisms across an R-linear additive functor between module categories.

Equations

• Morita.aux0 R A B e1 N = { toFun := fun (f : Module.End A ↑N) => ModuleCat.Hom.hom (e1.map (ModuleCat.ofHom f)), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[reducible, inline]

abbrev Module.End.restrictScalars (R : Type u_1) (S : Type u_2) (M : Type u_3) (R₁ : Type u_4) [Ring R] [Ring S] [CommRing R₁] [AddCommGroup M] [Module R M] [Module R₁ M] [Module S M] [Algebra R₁ R] [IsScalarTower R₁ R M] [Algebra R₁ S] [IsScalarTower R₁ S M] [LinearMap.CompatibleSMul M M R S] : End S M →ₐ[R₁] M →ₗ[R] M

Restrict scalars on an endomorphism algebra to a smaller scalar ring.

Equations

• Module.End.restrictScalars R S M R₁ = AlgHom.ofLinearMap (LinearMap.restrictScalarsₗ R S M M R₁) ⋯ ⋯

@[reducible, inline]

abbrev Morita.moduleMapAux (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M : ModuleCat (TensorProduct R A C)) : C →ₐ[R] Module.End A ↑((ModuleCat.restrictScalars Algebra.TensorProduct.includeLeftRingHom).obj M)

The right tensor factor acts on an A ⊗ C-module after restriction to an A-module.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Morita.moduleMap (R : Type u) [CommRing R] (A B C : Type v) [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (e1 : CategoryTheory.Functor (ModuleCat A) (ModuleCat B)) [e1.Additive] [CategoryTheory.Functor.Linear R e1] (M : ModuleCat (TensorProduct R A C)) : TensorProduct R B C →ₐ[R] Module.End R ↑(e1.obj ((ModuleCat.restrictScalars Algebra.TensorProduct.includeLeftRingHom).obj M))

The tensor-product algebra action obtained after applying a Morita equivalence to the left factor.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance Morita.modulefromtensor (R : Type u) [CommRing R] (A B C : Type v) [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (e1 : CategoryTheory.Functor (ModuleCat A) (ModuleCat B)) [e1.Additive] [CategoryTheory.Functor.Linear R e1] (M : ModuleCat (TensorProduct R A C)) : Module (TensorProduct R B C) ↑(e1.obj ((ModuleCat.restrictScalars Algebra.TensorProduct.includeLeftRingHom).obj M))

Equations

• Morita.modulefromtensor R A B C e1 M = Module.compHom (↑(e1.obj ((ModuleCat.restrictScalars Algebra.TensorProduct.includeLeftRingHom).obj M))) (Morita.moduleMap R A B C e1 M).toRingHom

structure TensorModule (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : Type (v + 1)

use Action instead once it's generalized to enriched categories.

• carrier : ModuleCat A

  The underlying module over the left tensor factor.

• morphism : C →ₐ[R] Module.End A ↑self.carrier

  The action of the right tensor factor by left-factor-linear endomorphisms.

@[implicit_reducible]

instance instCoeSortTensorModuleType (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CoeSort (TensorModule R A C) (Type v)

Equations

• instCoeSortTensorModuleType R A C = { coe := fun (M : TensorModule R A C) => ↑M.carrier }

structure TensorModule.Hom (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M N : TensorModule R A C) : Type v

Morphisms of tensor modules are maps that commute with the right tensor-factor action.

• hom : M.carrier ⟶ N.carrier

  The underlying map of modules over the left tensor factor.

• commutes (c : C) : CategoryTheory.CategoryStruct.comp self.hom (ModuleCat.ofHom (N.morphism c)) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.morphism c)) self.hom

  Compatibility with the right tensor-factor action.

theorem TensorModule.Hom.ext {R : Type u} {inst✝ : CommRing R} {A C : Type v} {inst✝¹ : Ring A} {inst✝² : Ring C} {inst✝³ : Algebra R A} {inst✝⁴ : Algebra R C} {M N : TensorModule R A C} {x y : Hom R A C M N} (hom : x.hom = y.hom) : x = y

theorem TensorModule.Hom.ext_iff {R : Type u} {inst✝ : CommRing R} {A C : Type v} {inst✝¹ : Ring A} {inst✝² : Ring C} {inst✝³ : Algebra R A} {inst✝⁴ : Algebra R C} {M N : TensorModule R A C} {x y : Hom R A C M N} : x = y ↔ x.hom = y.hom

@[simp]

theorem TensorModule.Hom.commutes_assoc {R : Type u} [CommRing R] {A C : Type v} [Ring A] [Ring C] [Algebra R A] [Algebra R C] {M N : TensorModule R A C} (self : Hom R A C M N) (c : C) {Z : ModuleCat A} (h : ModuleCat.of A ↑N.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (N.morphism c)) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.morphism c)) (CategoryTheory.CategoryStruct.comp self.hom h)

Compatibility with the right tensor-factor action.

@[simp]

theorem TensorModule.commutes_apply (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M N : TensorModule R A C) (f : Hom R A C M N) (c : C) (m : ↑M.carrier) : (ModuleCat.Hom.hom f.hom) ((M.morphism c) m) = (N.morphism c) ((ModuleCat.Hom.hom f.hom) m)

@[implicit_reducible]

instance instCategoryTensorModule (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CategoryTheory.Category.{v, v + 1} (TensorModule R A C)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TensorModule.hom_id (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M : TensorModule R A C) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.carrier

@[simp]

theorem TensorModule.hom_comp (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] {M N K : TensorModule R A C} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

theorem TensorModule.hom_ext (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] {M N : TensorModule R A C} (f g : M ⟶ N) (h : f.hom = g.hom) : f = g

theorem TensorModule.hom_ext_iff {R : Type u} [CommRing R] {A C : Type v} [Ring A] [Ring C] [Algebra R A] [Algebra R C] {M N : TensorModule R A C} {f g : M ⟶ N} : f = g ↔ f.hom = g.hom

def TensorModule.IsoMk (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] {M N : TensorModule R A C} (f : M.carrier ≅ N.carrier) (h : ∀ (c : C), CategoryTheory.CategoryStruct.comp f.hom (ModuleCat.ofHom (N.morphism c)) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.morphism c)) f.hom) : M ≅ N

Build an isomorphism of tensor modules from an isomorphism of the underlying modules.

Equations

• TensorModule.IsoMk R A C f h = { hom := { hom := f.hom, commutes := h }, inv := { hom := f.inv, commutes := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TensorModule.IsoMk_hom_hom (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] {M N : TensorModule R A C} (f : M.carrier ≅ N.carrier) (h : ∀ (c : C), CategoryTheory.CategoryStruct.comp f.hom (ModuleCat.ofHom (N.morphism c)) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.morphism c)) f.hom) : (IsoMk R A C f h).hom.hom = f.hom

@[simp]

theorem TensorModule.IsoMk_inv_hom (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] {M N : TensorModule R A C} (f : M.carrier ≅ N.carrier) (h : ∀ (c : C), CategoryTheory.CategoryStruct.comp f.hom (ModuleCat.ofHom (N.morphism c)) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.morphism c)) f.hom) : (IsoMk R A C f h).inv.hom = f.inv

@[implicit_reducible]

instance instCoeHomTensorModuleModuleCatCarrier (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M N : TensorModule R A C) : Coe (M ⟶ N) (M.carrier ⟶ N.carrier)

Equations

• instCoeHomTensorModuleModuleCatCarrier R A C M N = { coe := fun (f : M ⟶ N) => f.hom }

@[implicit_reducible]

instance instAddCommGroupHomTensorModule (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M N : TensorModule R A C) : AddCommGroup (M ⟶ N)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance instPreadditiveTensorModule (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CategoryTheory.Preadditive (TensorModule R A C)

Equations

• instPreadditiveTensorModule R A C = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

@[implicit_reducible]

noncomputable instance instModuleHomTensorModule (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M N : TensorModule R A C) : Module R (M ⟶ N)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance instLinearTensorModule (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CategoryTheory.Linear R (TensorModule R A C)

Equations

• instLinearTensorModule R A C = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

@[reducible, inline]

noncomputable abbrev moduleAux (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M : TensorModule R A C) : TensorProduct R A C →ₐ[R] Module.End R ↑M.carrier

The A ⊗ C action associated to a tensor module.

Equations

• moduleAux R A C M = Algebra.TensorProduct.lift (Algebra.lsmul R R ↑M.carrier) ((Module.End.restrictScalars R A (↑M.carrier) R).comp M.morphism) ⋯

theorem moduleAux_apply (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M : TensorModule R A C) (a : A) (c : C) (m : ↑M.carrier) : ((moduleAux R A C M) (a ⊗ₜ[R] c)) m = a • (M.morphism c) m

@[implicit_reducible]

noncomputable instance moduletotensor (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M : TensorModule R A C) : Module (TensorProduct R A C) ↑M.carrier

Equations

• moduletotensor R A C M = Module.compHom (↑M.carrier) (moduleAux R A C M).toRingHom

@[simp]

theorem smul_tensormod (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (x : TensorProduct R A C) (M : TensorModule R A C) (m : ↑M.carrier) : x • m = ((moduleAux R A C M) x) m

@[reducible, inline]

noncomputable abbrev toModuleOverTensor (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CategoryTheory.Functor (TensorModule R A C) (ModuleCat (TensorProduct R A C))

View a tensor module as a module over the tensor-product algebra.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev fromModuleOverTensor (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CategoryTheory.Functor (ModuleCat (TensorProduct R A C)) (TensorModule R A C)

Split an A ⊗ C-module into an A-module with a compatible C-action.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev e01 (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M : TensorModule R A C) : (CategoryTheory.Functor.id (TensorModule R A C)).obj M ≅ ((toModuleOverTensor R A C).comp (fromModuleOverTensor R A C)).obj M

The unit component comparing tensor modules with modules over the tensor-product algebra.

Equations

• One or more equations did not get rendered due to their size.

theorem e01_naturality (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] {X Y : TensorModule R A C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (TensorModule R A C)).map f) (e01 R A C Y).hom = CategoryTheory.CategoryStruct.comp (e01 R A C X).hom (((toModuleOverTensor R A C).comp (fromModuleOverTensor R A C)).map f)

Naturality of the tensor-module unit comparison.

@[reducible, inline]

noncomputable abbrev eModunitIso (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CategoryTheory.Functor.id (TensorModule R A C) ≅ (toModuleOverTensor R A C).comp (fromModuleOverTensor R A C)

The unit isomorphism for the equivalence between tensor modules and modules over A ⊗ C.

Equations

• eModunitIso R A C = CategoryTheory.NatIso.ofComponents (e01 R A C) ⋯

@[reducible, inline]

noncomputable abbrev e02 (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] (M : ModuleCat (TensorProduct R A C)) : ((fromModuleOverTensor R A C).comp (toModuleOverTensor R A C)).obj M ≅ (CategoryTheory.Functor.id (ModuleCat (TensorProduct R A C))).obj M

The counit component comparing modules over the tensor-product algebra with tensor modules.

Equations

• e02 R A C M = { toAddHom := AddHom.id ↑((fromModuleOverTensor R A C).obj M).carrier, map_smul' := ⋯, invFun := id, left_inv := ⋯, right_inv := ⋯ }.toModuleIso

@[reducible, inline]

noncomputable abbrev eModcounitIso (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : (fromModuleOverTensor R A C).comp (toModuleOverTensor R A C) ≅ CategoryTheory.Functor.id (ModuleCat (TensorProduct R A C))

The counit isomorphism for the equivalence between tensor modules and modules over A ⊗ C.

Equations

• eModcounitIso R A C = CategoryTheory.NatIso.ofComponents (e02 R A C) ⋯

@[reducible, inline]

noncomputable abbrev equivModuleOverTensor (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : TensorModule R A C ≌ ModuleCat (TensorProduct R A C)

Tensor modules are equivalent to modules over the tensor-product algebra.

Equations

• One or more equations did not get rendered due to their size.

instance instAdditiveTensorModuleModuleCatTensorProductFunctorEquivModuleOverTensor (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : (equivModuleOverTensor R A C).functor.Additive

instance instLinearTensorModuleModuleCatTensorProductFunctorEquivModuleOverTensor (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CategoryTheory.Functor.Linear R (equivModuleOverTensor R A C).functor

instance instLinearModuleCatTensorProductTensorModuleInverseEquivModuleOverTensor (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CategoryTheory.Functor.Linear R (equivModuleOverTensor R A C).inverse

@[reducible, inline]

noncomputable abbrev toBCfunctor (R : Type u) [CommRing R] (A B C : Type v) [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (F : CategoryTheory.Functor (ModuleCat A) (ModuleCat B)) [F.Additive] [CategoryTheory.Functor.Linear R F] : CategoryTheory.Functor (TensorModule R A C) (TensorModule R B C)

Apply an R-linear additive functor to the left factor of a tensor module.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev MoritaTensorAux0 (R : Type u) [CommRing R] (A B C : Type v) [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (e : ModuleCat A ≌ ModuleCat B) [e.functor.Additive] [CategoryTheory.Functor.Linear R e.functor] : TensorModule R A C ≌ TensorModule R B C

Tensor a Morita equivalence on the left with the identity on the right tensor factor.

Equations

• One or more equations did not get rendered due to their size.

instance instAdditiveTensorModuleFunctorMoritaTensorAux0 (R : Type u) [CommRing R] (A B C : Type v) [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (e : ModuleCat A ≌ ModuleCat B) [e.functor.Additive] [CategoryTheory.Functor.Linear R e.functor] : (MoritaTensorAux0 R A B C e).functor.Additive

instance instLinearTensorModuleFunctorMoritaTensorAux0 (R : Type u) [CommRing R] (A B C : Type v) [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (e : ModuleCat A ≌ ModuleCat B) [e.functor.Additive] [CategoryTheory.Functor.Linear R e.functor] : CategoryTheory.Functor.Linear R (MoritaTensorAux0 R A B C e).functor

@[reducible, inline]

noncomputable abbrev MoritaTensorAux1 (R : Type u) [CommRing R] (A B C : Type v) [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (e : ModuleCat A ≌ ModuleCat B) [e.functor.Additive] [CategoryTheory.Functor.Linear R e.functor] : ModuleCat (TensorProduct R A C) ≌ ModuleCat (TensorProduct R B C)

The induced equivalence of module categories over tensor-product algebras.

Equations

• MoritaTensorAux1 R A B C e = (equivModuleOverTensor R A C).symm.trans ((MoritaTensorAux0 R A B C e).trans (equivModuleOverTensor R B C))

instance instLinearModuleCatTensorProductRestrictScalarsIncludeLeftRingHom_leanPool (R : Type u) [CommRing R] (A C : Type v) [Ring A] [Ring C] [Algebra R A] [Algebra R C] : CategoryTheory.Functor.Linear R (ModuleCat.restrictScalars Algebra.TensorProduct.includeLeftRingHom)

instance MoritaTensorAux1_linear (R : Type u) [CommRing R] (A B C : Type v) [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (e : ModuleCat A ≌ ModuleCat B) [e.functor.Additive] [CategoryTheory.Functor.Linear R e.functor] : CategoryTheory.Functor.Linear R (MoritaTensorAux1 R A B C e).functor

theorem MoritaTensorLeft (R : Type u) [CommRing R] (A B C : Type v) [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (e : IsMoritaEquivalent R A B) : IsMoritaEquivalent R (TensorProduct R A C) (TensorProduct R B C)

Morita equivalence is preserved by tensoring on the right.

theorem MoritaTensor (R : Type u) [CommRing R] (A B C D : Type v) [Ring A] [Ring B] [Ring C] [Ring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (e1 : IsMoritaEquivalent R A B) (e2 : IsMoritaEquivalent R C D) : IsMoritaEquivalent R (TensorProduct R A C) (TensorProduct R B D)

Tensor products of Morita equivalent algebras are Morita equivalent.