instance instModuleMatrixForall_brauerGroup (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module R M] : Module (Matrix ι ι R) (ι → M)

Equations

• instModuleMatrixForall_brauerGroup R ι M = Module.mk ⋯ ⋯

theorem matrix_smul_vec_def (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) : N • v = fun (i : ι) => ∑ j : ι, N i j • v j

theorem matrix_smul_vec_def' (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) : N • v = ∑ j : ι, fun (i : ι) => N i j • v j

theorem matrix_smul_vec_apply (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) (i : ι) : (N • v) i = ∑ j : ι, N i j • v j

def toModuleCatOverMatrix (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] : CategoryTheory.Functor (ModuleCat R) (ModuleCat (Matrix ι ι R))

Equations

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

@[simp]

theorem toModuleCatOverMatrix_obj_isModule (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] (M : ModuleCat R) : ((toModuleCatOverMatrix R ι).obj M).isModule = instModuleMatrixForall_brauerGroup R ι ↑M

@[simp]

theorem toModuleCatOverMatrix_obj_carrier (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] (M : ModuleCat R) : ↑((toModuleCatOverMatrix R ι).obj M) = (ι → ↑M)

@[simp]

theorem toModuleCatOverMatrix_map (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) : (toModuleCatOverMatrix R ι).map f = ModuleCat.ofHom { toFun := fun (v : ι → ↑X✝) (i : ι) => (CategoryTheory.ConcreteCategory.hom f) (v i), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem toModuleCatOverMatrix_obj_isAddCommGroup (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] (M : ModuleCat R) : ((toModuleCatOverMatrix R ι).obj M).isAddCommGroup = Pi.addCommGroup

def fromModuleCatOverMatrix.α (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] [Inhabited ι] (M : Type u_1) [AddCommGroup M] [Module (Matrix ι ι R) M] : AddSubgroup M

Equations

• fromModuleCatOverMatrix.α R ι M = { carrier := Set.range fun (x : M) => Matrix.stdBasisMatrix default default 1 • x, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem fromModuleCatOverMatrix.coe_α (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] [Inhabited ι] (M : Type u_1) [AddCommGroup M] [Module (Matrix ι ι R) M] : ↑(α R ι M) = Set.range fun (x : M) => Matrix.stdBasisMatrix default default 1 • x

instance fromModuleCatOverMatrix.module_α (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module (Matrix ι ι R) M] : Module R ↥(α R ι M)

Equations

• fromModuleCatOverMatrix.module_α R ι M = Module.mk ⋯ ⋯

@[simp]

theorem fromModuleCatOverMatrix.smul_α_coe (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module (Matrix ι ι R) M] (x : R) (y : ↥(α R ι M)) : ↑(x • y) = Matrix.stdBasisMatrix default default x • ↑y

def fromModuleCatOverMatrix (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : CategoryTheory.Functor (ModuleCat (Matrix ι ι R)) (ModuleCat R)

Equations

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

@[simp]

theorem fromModuleCatOverMatrix_map (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] {X✝ Y✝ : ModuleCat (Matrix ι ι R)} (f : X✝ ⟶ Y✝) : (fromModuleCatOverMatrix R ι).map f = ModuleCat.ofHom { toFun := fun (x : ↥(fromModuleCatOverMatrix.α R ι ↑X✝)) => ⟨(CategoryTheory.ConcreteCategory.hom f) ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem fromModuleCatOverMatrix_obj_isAddCommGroup (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : ((fromModuleCatOverMatrix R ι).obj M).isAddCommGroup = AddSubgroup.IsCommutative.addCommGroup (fromModuleCatOverMatrix.α R ι ↑M)

@[simp]

theorem fromModuleCatOverMatrix_obj_carrier (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : ↑((fromModuleCatOverMatrix R ι).obj M) = ↥(fromModuleCatOverMatrix.α R ι ↑M)

@[simp]

theorem fromModuleCatOverMatrix_obj_isModule (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : ((fromModuleCatOverMatrix R ι).obj M).isModule = fromModuleCatOverMatrix.module_α R ι ↑M

def matrix.unitIsoHom (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (toModuleCatOverMatrix R ι).comp (fromModuleCatOverMatrix R ι) ⟶ CategoryTheory.Functor.id (ModuleCat R)

Equations

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

@[simp]

theorem matrix.unitIsoHom_app (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (X : ModuleCat R) : (unitIsoHom R ι).app X = ModuleCat.ofHom { toFun := fun (x : ↥(fromModuleCatOverMatrix.α R ι ↑((toModuleCatOverMatrix R ι).obj X))) => ∑ i : ι, ↑x i, map_add' := ⋯, map_smul' := ⋯ }

def matrix.unitIsoInv (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : CategoryTheory.Functor.id (ModuleCat R) ⟶ (toModuleCatOverMatrix R ι).comp (fromModuleCatOverMatrix R ι)

Equations

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

@[simp]

theorem matrix.unitIsoInv_app (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (X : ModuleCat R) : (unitIsoInv R ι).app X = ModuleCat.ofHom { toFun := fun (x : ↑X) => ⟨Function.update 0 default x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

def matrix.unitIso (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (toModuleCatOverMatrix R ι).comp (fromModuleCatOverMatrix R ι) ≅ CategoryTheory.Functor.id (ModuleCat R)

Equations

• matrix.unitIso R ι = { hom := matrix.unitIsoHom R ι, inv := matrix.unitIsoInv R ι, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem matrix.unitIso_inv (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (unitIso R ι).inv = unitIsoInv R ι

@[simp]

theorem matrix.unitIso_hom (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (unitIso R ι).hom = unitIsoHom R ι

noncomputable def matrix.counitIsoHomMap (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : M ≅ ((fromModuleCatOverMatrix R ι).comp (toModuleCatOverMatrix R ι)).obj M

Equations

• matrix.counitIsoHomMap R ι M = (LinearEquiv.ofBijective { toFun := fun (m : ↑M) (i : ι) => ⟨Matrix.stdBasisMatrix default i 1 • m, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⋯).toModuleIso

@[simp]

theorem matrix.counitIsoHomMap_hom_hom_apply_coe (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) (a✝ : ↑M) (a✝¹ : ι) : ↑((ModuleCat.Hom.hom (counitIsoHomMap R ι M).hom) a✝ a✝¹) = Matrix.stdBasisMatrix default a✝¹ 1 • a✝

@[simp]

theorem matrix.counitIsoHomMap_inv_hom_apply (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) (a : ι → ↑((fromModuleCatOverMatrix R ι).obj M)) : (ModuleCat.Hom.hom (counitIsoHomMap R ι M).inv) a = ((↑(LinearEquiv.ofBijective { toFun := fun (m : ↑M) (i : ι) => ⟨Matrix.stdBasisMatrix default i 1 • m, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⋯)).inverse ⇑(LinearEquiv.ofBijective { toFun := fun (m : ↑M) (i : ι) => ⟨Matrix.stdBasisMatrix default i 1 • m, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⋯).symm ⋯ ⋯) a

noncomputable def matrix.counitIsoHom (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (fromModuleCatOverMatrix R ι).comp (toModuleCatOverMatrix R ι) ⟶ CategoryTheory.Functor.id (ModuleCat (Matrix ι ι R))

Equations

• matrix.counitIsoHom R ι = { app := fun (M : ModuleCat (Matrix ι ι R)) => (matrix.counitIsoHomMap R ι M).inv, naturality := ⋯ }

@[simp]

theorem matrix.counitIsoHom_app (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : (counitIsoHom R ι).app M = (counitIsoHomMap R ι M).inv

noncomputable def matrix.counitIsoInv (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : CategoryTheory.Functor.id (ModuleCat (Matrix ι ι R)) ⟶ (fromModuleCatOverMatrix R ι).comp (toModuleCatOverMatrix R ι)

Equations

• matrix.counitIsoInv R ι = { app := fun (M : ModuleCat (Matrix ι ι R)) => (matrix.counitIsoHomMap R ι M).hom, naturality := ⋯ }

@[simp]

theorem matrix.counitIsoInv_app (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : (counitIsoInv R ι).app M = (counitIsoHomMap R ι M).hom

noncomputable def matrix.counitIso (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (fromModuleCatOverMatrix R ι).comp (toModuleCatOverMatrix R ι) ≅ CategoryTheory.Functor.id (ModuleCat (Matrix ι ι R))

Equations

• matrix.counitIso R ι = { hom := matrix.counitIsoHom R ι, inv := matrix.counitIsoInv R ι, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem matrix.counitIso_inv (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (counitIso R ι).inv = counitIsoInv R ι

@[simp]

theorem matrix.counitIso_hom (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (counitIso R ι).hom = counitIsoHom R ι

noncomputable def moritaEquivalentToMatrix (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : ModuleCat R ≌ ModuleCat (Matrix ι ι R)

Equations

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

@[simp]

theorem moritaEquivalentToMatrix_inverse (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (moritaEquivalentToMatrix R ι).inverse = fromModuleCatOverMatrix R ι

@[simp]

theorem moritaEquivalentToMatrix_functor (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (moritaEquivalentToMatrix R ι).functor = toModuleCatOverMatrix R ι

@[simp]

theorem moritaEquivalentToMatrix_unitIso (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (moritaEquivalentToMatrix R ι).unitIso = (matrix.unitIso R ι).symm

@[simp]

theorem moritaEquivalentToMatrix_counitIso (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (moritaEquivalentToMatrix R ι).counitIso = matrix.counitIso R ι

class IsMoritaEquivalent (R : Type u) (S : Type u') [Ring R] [Ring S] : Prop

• out : Nonempty (ModuleCat R ≌ ModuleCat S)

noncomputable def IsMoritaEquivalent.equiv (R : Type u) (S : Type u') [Ring R] [Ring S] [IsMoritaEquivalent R S] : ModuleCat R ≌ ModuleCat S

Equations

• IsMoritaEquivalent.equiv R S = ⋯.some

instance IsMoritaEquivalent.instAdditiveModuleCatFunctorEquiv (R : Type u) (S : Type u') [Ring R] [Ring S] [IsMoritaEquivalent R S] : (equiv R S).functor.Additive

instance IsMoritaEquivalent.instAdditiveModuleCatInverseEquiv (R : Type u) (S : Type u') [Ring R] [Ring S] [IsMoritaEquivalent R S] : (equiv R S).inverse.Additive

theorem IsMoritaEquivalent.refl (R : Type u) [Ring R] : IsMoritaEquivalent R R

instance IsMoritaEquivalent.inst (R : Type u) [Ring R] : IsMoritaEquivalent R R

theorem IsMoritaEquivalent.symm (R : Type u) (S : Type u') [Ring R] [Ring S] [IsMoritaEquivalent R S] : IsMoritaEquivalent S R

theorem IsMoritaEquivalent.trans (R : Type u) (S : Type u') (T : Type u'') [Ring R] [Ring S] [Ring T] [IsMoritaEquivalent R S] [IsMoritaEquivalent S T] : IsMoritaEquivalent R T

instance IsMoritaEquivalent.matrix (R : Type u) [Ring R] (n : ℕ) : IsMoritaEquivalent R (Matrix (Fin (n + 1)) (Fin (n + 1)) R)

theorem IsMoritaEquivalent.matrix' (R : Type u) [Ring R] (n : ℕ) [hn : NeZero n] : IsMoritaEquivalent R (Matrix (Fin n) (Fin n) R)

@[reducible, inline]

abbrev IsMoritaEquivalent.ofIsoApp1 (R : Type u) (S : Type u') [Ring R] [Ring S] (e : R ≃+* S) (X : ModuleCat R) : X ⟶ ((ModuleCat.restrictScalars e.symm.toRingHom).comp (ModuleCat.restrictScalars e.toRingHom)).obj X

Equations

• IsMoritaEquivalent.ofIsoApp1 R S e X = ModuleCat.ofHom { toFun := ⇑LinearMap.id, map_add' := ⋯, map_smul' := ⋯ }

@[reducible, inline]

abbrev IsMoritaEquivalent.ofIsoApp2 (R : Type u) (S : Type u') [Ring R] [Ring S] (e : R ≃+* S) (X : ModuleCat R) : ((ModuleCat.restrictScalars e.symm.toRingHom).comp (ModuleCat.restrictScalars e.toRingHom)).obj X ⟶ X

Equations

• IsMoritaEquivalent.ofIsoApp2 R S e X = ModuleCat.ofHom { toFun := ⇑LinearMap.id, map_add' := ⋯, map_smul' := ⋯ }

theorem IsMoritaEquivalent.ofIso (R : Type u) (S : Type u') [Ring R] [Ring S] (e : R ≃+* S) : IsMoritaEquivalent R S

theorem IsMoritaEquivalent.division_ring.division_ring_exists_unique_isSimpleModule (S : Type u) [DivisionRing S] (N : Type u_1) [AddCommGroup N] [Module S N] [IsSimpleModule S N] : Nonempty (N ≃ₗ[S] S)

instance IsMoritaEquivalent.division_ring.instAdditiveModuleCatFunctor (R S : Type u) [DivisionRing R] [DivisionRing S] (e : ModuleCat R ≌ ModuleCat S) : e.functor.Additive

theorem IsMoritaEquivalent.division_ring.isSimpleModule_iff_injective_or_eq_zero (R : Type u) [Ring R] (M : ModuleCat R) : IsSimpleModule R ↑M ↔ Nontrivial ↑M ∧ ∀ (N : ModuleCat R) (f : M ⟶ N), f = 0 ∨ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)

instance CategoryTheory.Equivalence.nontrivial {R S : Type u} [Ring R] [Ring S] (e : ModuleCat R ≌ ModuleCat S) (M : ModuleCat R) [h : Nontrivial ↑M] : Nontrivial ↑(e.functor.obj M)

theorem IsMoritaEquivalent.division_ring.IsSimpleModule.functor (R S : Type u) [Ring R] [Ring S] (e : ModuleCat R ≌ ModuleCat S) (M : ModuleCat R) [simple_module : IsSimpleModule R ↑M] : IsSimpleModule S ↑(e.functor.obj M)

def IsMoritaEquivalent.division_ring.mopToEnd (R : Type u) [DivisionRing R] : Rᵐᵒᵖ →+* CategoryTheory.End (ModuleCat.of R R)

Equations

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

@[simp]

theorem IsMoritaEquivalent.division_ring.mopToEnd_apply (R : Type u) [DivisionRing R] (a : Rᵐᵒᵖ) : (mopToEnd R) a = ModuleCat.ofHom { toFun := fun (x : R) => x * MulOpposite.unop a, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def IsMoritaEquivalent.division_ring.mopEquivEnd (R : Type u) [DivisionRing R] : Rᵐᵒᵖ ≃+* CategoryTheory.End (ModuleCat.of R R)

Equations

• IsMoritaEquivalent.division_ring.mopEquivEnd R = RingEquiv.ofBijective (IsMoritaEquivalent.division_ring.mopToEnd R) ⋯

def IsMoritaEquivalent.division_ring.aux1 {R S : Type u} [DivisionRing R] [DivisionRing S] (e : ModuleCat R ≌ ModuleCat S) : CategoryTheory.End (ModuleCat.of R R) ≃+* CategoryTheory.End (e.functor.obj (ModuleCat.of R R))

Equations

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

noncomputable def IsMoritaEquivalent.division_ring.aux20 (R S : Type u) [DivisionRing R] [DivisionRing S] (e : ModuleCat R ≌ ModuleCat S) : e.functor.obj (ModuleCat.of R R) ≅ ModuleCat.of S S

Equations

• IsMoritaEquivalent.division_ring.aux20 R S e = ⋯.some.toModuleIso

def IsMoritaEquivalent.division_ring.aux2 (S : Type u) [DivisionRing S] (M N : ModuleCat S) (f : M ≅ N) : CategoryTheory.End M ≃+* CategoryTheory.End N

Equations

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

noncomputable def IsMoritaEquivalent.division_ring.toRingMopEquiv (R S : Type u) [DivisionRing R] [DivisionRing S] (e : ModuleCat R ≌ ModuleCat S) : Rᵐᵒᵖ ≃+* Sᵐᵒᵖ

Equations

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

noncomputable def IsMoritaEquivalent.division_ring.toRingEquiv (R S : Type u) [DivisionRing R] [DivisionRing S] (e : ModuleCat R ≌ ModuleCat S) : R ≃+* S

Equations

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

noncomputable def IsMoritaEquivalent.ringEquivOfDivisionRing (R S : Type u) [DivisionRing R] [DivisionRing S] [IsMoritaEquivalent R S] : R ≃+* S

Equations

• IsMoritaEquivalent.ringEquivOfDivisionRing R S = IsMoritaEquivalent.division_ring.toRingEquiv R S (IsMoritaEquivalent.equiv R S)