Wedderburn-Artin Theorem

Stream: mathlib4

[Edison Xie]

I've commited a proof of wedderburn-artin as a draft #23583, I know there has been discussion towards TwoSidedIdeal and I'd like to know how people think about the current status and this PR :)

[Edison Xie]

cc @Junyan Xu

[Edison Xie]

#23583 is now ready-for-review!

[Junyan Xu]

I've built some minimal amount of isotypic component APIs in order to get more useful intermediate results from the proof. I haven't finished the proof of the WA theorem with this approach yet, but you can see my progress here. I'm sorry I didn't give detailed review on @Jiang Xu Wan's PR(s) (cc @Lior Silberman) but I'd appreciate suggestions to adapt our isotypic APIs to each other.

[Edison Xie]

Junyan Xu said:

I've built some minimal amount of isotypic component APIs in order to get more useful intermediate results from the proof.

Is there going to be a PR soon? :curious:

[Junyan Xu]

I'm currently adding and refining the isotypic API to make to proof flow more naturally and it will take some time.
I just introduce IsIsotypicOfType and one thing I have not coded is that if M is isotypic of type S, then it's isomorphic to a Finsupp over S (easy using finsuppEquivDFinsupp and isSemisimpleModule_iff_exists_linearEquiv_dfinsupp), and the number of copies of S must be Module.rank (DomMulAct <| Module.End R S) (S →ₗ[R] M) (this should be a separate Module.simpleLength definition, and if you take Cardinal.toENat you should get Module.length).

[Junyan Xu]

This is quite lovely:

import Mathlib
variable (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]

def Module.End.domMulActEquiv : letI E := Module.End R M
    E ≃ₗ[DomMulAct E] DomMulAct E where
  __ := DomMulAct.mk
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

combined with (ι →₀ M →ₗ[R] N) ≃ₗ[S] (M →ₗ[R] ι →₀ N) here (For M finite), this is enough to show the number of simple copies is invariant (it also follows from the theory of length if the number is finite), which is probably useful to prove the uniqueness part of Wedderburn--Artin.

[Edison Xie]

what's DomMulAct?

[Aaron Liu]

It lets the type act on the domain

[Yaël Dillies]

docs#DomMulAct

[Edison Xie]

wait so if it's a type synonym for MulOpposite, what's the difference?

[Aaron Liu]

Motivation

Right action can be represented in mathlib as an action of the opposite group Mᵐᵒᵖ. However,
this "domain shift" action cannot be an instance because this would create a "diamond"
(a.k.a. ambiguous notation): if M is a monoid, then how does Mᵐᵒᵖ act on M → M? On the one
hand, Mᵐᵒᵖ acts on M by c • a = a * c.unop, thus we have an action
(c • f) a = f a * c.unop. On the other hand, M acts on itself by multiplication on the left, so
with this new instance we would have (c • f) a = f (c.unop * a). Clearly, these are two different
actions, so both of them cannot be instances in the library.

To overcome this difficulty, we introduce a type synonym DomMulAct M := Mᵐᵒᵖ (notation:
Mᵈᵐᵃ). This new type carries the same algebraic structures as Mᵐᵒᵖ but acts on α → β by this
new action. So, e.g., Mᵈᵐᵃ acts on (M → M) → M by DomMulAct.mk c • F f = F (fun a ↦ c • f a)
while (Mᵈᵐᵃ)ᵈᵐᵃ (which is isomorphic to M) acts on (M → M) → M by
DomMulAct.mk (DomMulAct.mk c) • F f = F (fun a ↦ f (c • a)).

[Junyan Xu]

If MulOpposite is used in this case there will be a diamond for Module (MulOpposite E) E with Semiring.toOppositeModule. DomMulAct is the correct type synonym to use to obtain the right instances.

[Junyan Xu]

Sorry, it's not really a diamond, the actions are still defeq.

[Junyan Xu]

Opened #23963

[Edison Xie]

Junyan Xu said:

Opened #23963

So actually I am bit confused here, we both have the same results in two different PRs, how is it gonna work? If yours/my PR got merged do we delete the other one or do we adapt to each others?

[Junyan Xu]

I think my PR now includes all the end results from your PR. Since I adopted your statements I'm adding you as coauthors. If my PR gets merged, but you think some intermediate results in your PR is worth keeping, you might leave them there to get them reviewed.

[Ruben Van de Velde]

Please add a note to that effect on the PRs as well

[Junyan Xu]

I added "A replacement of #23583 with more meaningful intermediate results." in the description of #23963.

#23583 depends on another PR and still has "wip" in the title so I think it's unlikely that it gets merged first ...

[Edison Xie]

it's no longer a WIP I just forgot to change :((, the dependent PR is because @Eric Wieser wants to consult someone's opinion and that some one has yet replied in a week :((, however you have a point I should probly just close #23583 :smiling_face_with_tear:

[Edison Xie]

closed #23583

[Edison Xie]

I think #23963 also covers part of 074E by the use of IsIsotypic for simple rings? @Junyan Xu

[Eric Wieser]

I think some intermediate results from that PR like TwoSidedIdeal.span_eq_bot would still be good to have

[Edison Xie]

Eric Wieser said:

I think some intermediate results from that PR like TwoSidedIdeal.span_eq_bot would still be good to have

I will open a separate PR if necessary :)

[Junyan Xu]

Edison Xie said:

I think #23963 also covers part of 074E by the use of IsIsotypic for simple rings? Junyan Xu

I think the PR only covered parts (1) and (2) so far. (2) is equivalent to A being a semisimple A-module, i.e. A is a semisimple ring.

[Edison Xie]

Junyan Xu said:

Edison Xie said:

I think #23963 also covers part of 074E by the use of IsIsotypic for simple rings? Junyan Xu

I think the PR only covered parts (1) and (2) so far. (2) is equivalent to A being a semisimple A-module, i.e. A is a semisimple ring.

I have a whole file on 074E in our brauer project will PR after you get that merged :rolling_on_the_floor_laughing:

[Junyan Xu]

#24119 (+212 -116) is a preliminary PR with little mathematical content.
#23963 (+407 -20) is basic isotypic API + Wedderburn–Artin for Artinian simple rings.
#24192 (+484 -60) is more advanced isotypic API + Wedderburn–Artin for semisimple rings (module docstrings are added here).
Previous discussions:
#mathlib4 > two-sided ideals @ 💬
#mathlib4 > independent submodules @ 💬

[Edison Xie]

Junyan Xu said:

#24119 (+212 -116) is a preliminary PR with little mathematical content.

reviewed #24119!

[Junyan Xu]

Do we have this in the Brauer group repo? This is 28.F4 on Lorenz and I think it leads to a prove of the uniqueness part of Wedderburn--Artin (simple case) without talking about modules of the matrix algebra, using endomorphism algebras as substitutes.

import Mathlib

variable {ι R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι]

namespace Module.End

def ringHomEndFinsupp : End (End R M) M →+* End (End R (ι →₀ M)) (ι →₀ M) where
  toFun f :=
  { __ := Finsupp.mapRange.addMonoidHom f
    map_smul' g x := sorry }
  map_one' := _
  map_mul' := _
  map_zero' := _
  map_add' := _

def ringEquivEndFinsupp [Nonempty ι] :
    End (End R M) M ≃+* End (End R (ι →₀ M)) (ι →₀ M) where

end Module.End

[Edison Xie]

I have the uniqueness of Wedderburn using stack 074E

[Edison Xie]

Junyan Xu said:

Do we have this in the Brauer group repo? This is 28.F4 on Lorenz and I think it leads to a prove of the uniqueness part of Wedderburn--Artin (simple case) without talking about modules of the matrix algebra, using endomorphism algebras as substitutes.

import Mathlib

variable {ι R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι]

namespace Module.End

def ringHomEndFinsupp : End (End R M) M →+* End (End R (ι →₀ M)) (ι →₀ M) where
  toFun f :=
  { __ := Finsupp.mapRange.addMonoidHom f
    map_smul' g x := sorry }
  map_one' := _
  map_mul' := _
  map_zero' := _
  map_add' := _

def ringEquivEndFinsupp [Nonempty ι] :
    End (End R M) M ≃+* End (End R (ι →₀ M)) (ι →₀ M) where

end Module.End

and I have this for a different purpose, I can't remember what it exactly is but it's either for double centralizer theorem or skolem-noether

[Junyan Xu]

Turns out it's easy using a bit of induction (and no need of finiteness):

@[simps] noncomputable def ringHomEndFinsupp :
    End (End R M) M →+* End (End R (ι →₀ M)) (ι →₀ M) where
  toFun f :=
  { toFun := Finsupp.mapRange.addMonoidHom f
    map_add' := map_add _
    map_smul' g x := x.induction_linear (by simp)
      (fun _ _ h h' ↦ by rw [smul_add, map_add, h, h', map_add, smul_add]) fun i m ↦ by
        ext j
        show f (Finsupp.lapply j ∘ₗ g ∘ₗ Finsupp.lsingle i • m) = _
        rw [map_smul]
        simp }
  map_one' := by ext; simp
  map_mul' _ _ := by ext; simp
  map_zero' := by ext; simp
  map_add' _ _ := by ext; simp

@[simps!] noncomputable def ringEquivEndFinsupp (i : ι) :
    End (End R M) M ≃+* End (End R (ι →₀ M)) (ι →₀ M) where
  __ := ringHomEndFinsupp ι
  invFun f :=
  { toFun m := f (Finsupp.single i m) i
    map_add' _ _ := by simp
    map_smul' g m := let g := Finsupp.mapRange.linearMap g
      show _ = g _ i by rw [← g.smul_def, ← map_smul]; simp [g] }
  left_inv _ := by ext; simp
  right_inv f := by
    ext x j
    show f (Finsupp.lsingle (R := R) (M := M) i ∘ₗ Finsupp.lapply j • x) i = _
    rw [map_smul]
    simp

(Edit: added RingEquiv version)