A question about module

Stream: Is there code for X?

[Edison Xie]

I'm currently trying to prove the uniqueness of Wedderburn-Artin theorem and I'm stuck at a proposition as below:

import Mathlib.Tactic

local notation "M[" ι "," R "]" => Matrix ι ι R
variable (K : Type*) [Field K](B : Type*) [Field K] [Ring B] [Algebra K B] [FiniteDimensional K B]

instance (M : Type*) [AddCommGroup M] [Module B M]  :
  Algebra K (Module.End B M) where
    smul := fun k x =>
    { toFun := fun m => x $ (algebraMap K B k) • m
      map_add' := fun m1 m2 => by simp
      map_smul' := fun b m => by
        simp only [LinearMapClass.map_smul, RingHom.id_apply]
        rw [← MulAction.mul_smul, Algebra.commutes k b, MulAction.mul_smul] }
    toFun k :=
    { toFun := fun m => algebraMap K B k • m
      map_add' := fun m1 m2 => by simp
      map_smul' := fun m1 m2 => by
        simp only [RingHom.id_apply]
        rw [← MulAction.mul_smul, Algebra.commutes k m1, MulAction.mul_smul] }
    map_one' := by simp only [_root_.map_one, one_smul]; rfl
    map_mul' a b := by
      ext m
      simp only [_root_.map_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply,
        LinearMapClass.map_smul]
      rw [← MulAction.mul_smul, Algebra.commutes, MulAction.mul_smul]
    map_zero' := by simp only [map_zero, zero_smul]; rfl
    map_add' a b := by
      ext m
      simp only [map_add, add_smul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
    commutes' a x := by
      ext m
      simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, LinearMap.mul_apply,
        LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul]
    smul_def' a x := by
      ext m
      change x _ = _
      simp only [_root_.map_smul, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
        LinearMap.mul_apply, LinearMap.coe_mk, AddHom.coe_mk]

def test' (D : Type*) [DivisionRing D] [Algebra K D] (m : ℕ) (hm : m ≠ 0)
    (Wdb : B ≃ₐ[K] M[Fin m, D]) (M : Type*)
    [AddCommGroup M] [Module B M] [IsSimpleModule B M] :
    Module.End B M ≃ₐ[K] Dᵐᵒᵖ := by sorry

And the math proof is on stack project lemma 11.5.1 https://stacks.math.columbia.edu/tag/074J

[Edison Xie]

A little help on test' would be appreciated

[Kim Morrison]

Just noting that for your first instance you can generalize all the way to

variable (K : Type*) [CommSemiring K](B : Type*) [Semiring B] [Algebra K B]

instance (M : Type*) [AddCommMonoid M] [Module B M]  :
  Algebra K (Module.End B M) where

[Kim Morrison]

I'm very surprised this doesn't already exist!

[Kim Morrison]

The stacks link you gave isn't exactly the statement you're trying to prove. How about you write out an informal proof first?

[Edison Xie]

Kim Morrison said:

I'm very surprised this doesn't already exist!

Yes so do I

[Edison Xie]

Kim Morrison said:

The stacks link you gave isn't exactly the statement you're trying to prove. How about you write out an informal proof first?

sorry for the confusion the proof should be in https://stacks.math.columbia.edu/tag/074E here, lemma 11.4.6 (4)

[Kim Morrison]

Do you have the equivalence from 11.4.5 set up?

[Edison Xie]

[Quoting…]

Yes it's morita equivalence I have a file for that

[Edison Xie]

MoritaEquivalence.lean

[Eric Wieser]

Kim Morrison said:

I'm very surprised this doesn't already exist!

@loogle Algebra _ (Module.End _ _)

[loogle]

:search: Module.End.instAlgebra

[Eric Wieser]

Is that not sufficiently general here?

[Eric Wieser]

I think the issue here is that you should resist the urge to construct new actions via composition with algebraMap, and instead assume the action already exists, and enforce it is precisely this action via IsScalarTower

[Kim Morrison]

That is ... unintuitive but helpful!