Define n-fold direct sum of some module

Stream: general

[Ross Truscott]

Hi! Im very new to this so apologies for the basic question, but im struggling to understand how to write a function which takes in a module I have defined, $S$, and returns $S^n$ for some $n\in\N$.

From reading this, it seem that I need some $\iota$ of fintype, but I just dont understand how I actually implement this. So far I have

variable (R : Type u_2) [Ring R] (S : Type u_4) [AddCommGroup S] [Module R S] [IsSimpleModule R S]

and I want to define $M$ to be $\bigoplus^n S$, could anyone help guide me?

[Riccardo Brasca]

The easiest way is probably Fin n → S, you just consider functions from the "standard" set with n elements to S.

[Antoine Chambert-Loir]

If you insist on direct sum, you can also play with DirectSum (Fin n) fun _ => S.

[Wrenna Robson]

If for some reason you want it to be indexed by a general fintype, replace Fin n in the above by $\iota$ and you'll need a [Fintype $$\iota$$] typeclass.

[Eric Wieser]

Arguably the whole point of using DirectSum is for the case when the index type is _not_ finite

[Wrenna Robson]

Aye.

[Ross Truscott]

Im still having quite a lot of bother with this unfortunately. It seems that direct sum should still give me out an R-module, but this doesn't seem to be the case (at least as far as what I have written)

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Data.Matrix.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Algebra.DirectSum.Module
import Mathlib.RingTheory.SimpleModule.Basic

variable (R : Type u_2) [Ring R] (S : Type u_4) [AddCommGroup S] [Module R S] [IsSimpleModule R S]
variable (M : DirectSum (Fin n) fun _ => S)
theorem EndOfDirSumOfSimpleIsMatrixOverDiv (Fin n) (D : Module.End R S) M : (Module.End R M) ≃+* (Matrix n n D) := by
sorry

This throws up an error of "Failed to synthesise AddComMonoid M", but it seems that direct sum should still give me out an R module so this should work should it not? I think there's also likely a hundred other issues with what ive written (I seem to get a type mismatch with D as well..) but for now im confused about this

[Jireh Loreaux]

You have a stray M in there right before the colon.

[Jireh Loreaux]

(D : Module.End R S) M : (Module.End R M)

[Jireh Loreaux]

and M is a term in the direct sum, not a module.

[Jireh Loreaux]

I'm actually not sure what you're trying to write mathematically. Can you describe it in English?

[Ross Truscott]

Yeah sure. Let $S$ be a simple $R$-module, $D = \mathrm{End}_R(S)$ (this is a division ring by schurs lemma, hence the $D$) and $M = S^n$. Then $\mathrm{End}_R(M) = M_n(D)$ where $M_n$ is an $n\times n$ matrix with entries in $D$

[Jireh Loreaux]

are you looking for docs#endVecAlgEquivMatrixEnd ?

[Jireh Loreaux]

Okay, when you write (D : Module.End R S) this means, "let D be an R-endomorphism of S".

[Ross Truscott]

This does look like the result im trying to prove yeah. Im doing this as part of a class where im trying to prove Artin-Wedderburn so Im trying not to use much from Mathlib, but this does seem to be the result im trying to prove

Its possible, because Im just following the proof of AW I know, and dont really know any formalisation stuff that im just going about this very poorly though

[Jireh Loreaux]

By the way, I found that result like this: @loogle Module.End, Matrix

[loogle]

:search: algEquivMatrix, endVecRingEquivMatrixEnd, and 56 more

[Ross Truscott]

That is good to know! I am unfortunately more looking to prove it myself though, im trying to do this as part of a course on Lean, but im just really struggling to get to grips with how to actually set up my own theorems

[Jireh Loreaux]

Well, if that's the theorem you want to prove, you can still just use that statement, and provide your own proof / construction.

[Jireh Loreaux]

Note that when formalizing, we don't often write things like let D := Module.End R S or let M := n → S, at least not in the statement, as it generally just makes the statement more cluttered (and for some other technical reasons). If you would have made those substitutions instead of trying to introduce new names, your statement would have been fine.

[Ross Truscott]

Ok thank you! This is all good to know. Ill see if I can use this to get to a point where I finally have something to actually prove haha

[Kevin Buzzard]

@Ross Truscott have you not got a local Lean expert to help you? If not then you can ask here but usually such questions go in #new members .

Let me try and get you started here. I know you already pointed out that you want to do things yourself so just using docs#endVecRingEquivMatrixEnd (which is a closer fit for your question than the AlgEquiv version) is not an ideal solution for you.

Firstly, you want to think about the mathematics. What you write is true, but much more is true. In formalization it's always best to write down the most general statement. Simplicity of the module and the fact that $D$ is a division ring has nothing to do with the "theorem" that you're trying to "prove" as far as I can see. You want to state the natural result, not a result with superfluous hypotheses.

Secondly, I put "theorem" and "prove" in quotes because firstly your informal "theorem" is false. This is formal mathematics, not pen and paper mathematics. $End_R(M)$ is a collection of functions from $M$ to $M$ and $M_n(D)$ is a collection of $n$ by $n$ boxes (matrices) whose entries are functions, so they definitely not at all equal. What you mean of course is that they are "canonically isomorphic". But "canonical" has no formal meaning. In fact the thing which you are saying is a "theorem" is not a theorem at all, it is a definition, namely the definition of the actual isomorphism which mathematicians would deem to be "canonical". This is how formalization works -- the use of $=$ to denote canonical isomorphism is banned, and needs to be replaced by the actual function which mathematicians want to identify with the identity function.

OK with that rant out of the way, let's set up your definition. Mathematically we want this: $R$ is a ring, $S$ is an $R$-module, and then we want to write down a natural bijection between $End_R(S^n)$ and $M_n(End_R(S))$. What kind of a bijection? Well let's start with a bijection of sets (or types, as they're called here).

import Mathlib

-- note: not `theorem`
def endVecEquivMatrixEnd
    -- let n be a natural
    (n : ℕ)
    -- let R be a ring
    (R : Type) [Ring R]
    -- Let S be an R-module
    (S : Type) [AddCommGroup S] [Module R S]
    -- Then
    :
    -- we define a bijection between End_R(S^n) and M_n(End_R(S))
    Module.End R (Fin n → S) ≃ Matrix (Fin n) (Fin n) (Module.End R S) where
  -- We define it by giving maps in both directions
  -- Given the endomorphism F of S^n, the (i,j) coefficient of the matrix
  toFun F i j :=
    -- is the endomorphism of S which
    {
      -- as a function sends s to the i'th entry of the vector
      -- F(0,0,0,0,...0,s,0,0,0...) where s is in the j'th entry
      toFun s := F (Pi.single j s) i
      -- except that it might be the j'th entry of s in the i'th entry,
      -- so you'd better check the above line and swap i,j if necessary.
      -- This map preserves addition
      map_add' s t := by
        sorry
      -- and scalar multiplication
      map_smul' r s := by
        sorry
      -- and hence we've defined a linear map
      }
  -- The inverse function: given a matrix M
  invFun M :=
    -- we define a linear map S^n -> S^n
  { -- by sending a vector v to the vector whose i'th entry is
    toFun v i :=
      -- something like ∑_j, M_{ij}(v_j) or possibly ∑_j, M_{ji}V_j.
      ∑ j, M i j (v j)
      -- you had better check my algebra. I claim that this map is linear,
      -- indeed it preserves addition
    map_add' v w := by
      sorry
    -- and scalar multiplication
    map_smul' r v := by
      sorry
  }
  -- I claim that these two functions are inverses of each other
  -- in both directions.
  left_inv := by
    sorry
  right_inv := by
    sorry

I've filled in all the data, but this was a back of an envelope calculation so I might have got it wrong. So your job is to check that I defined your functions correctly, and if I did then to fill in all the sorrys. Then you'll have written down an explicit bijection between your sets.

[Ross Truscott]

@Kevin Buzzard This is incredibly helpful thank you! I am doing this as part of a "course" (although the course is mostly just pick a result and formalise it!), but I'm not sure the best way to be asking such specific questions in that context. I'll be sure to direct any future questions to #**new members> however, thanks for that!

So yes, of course when I wrote $=$ above, I certainly meant to write $\cong$. After this discussion yesterday I did notice that there is a difference between definitions and theorems in lean, but this seems to be some complicated type theoretic difference that I dont really understand. How should I think about theorems vs definitions? At least as far as, how should I know when my "informal" theorem is actually a definition as far as lean is concerned, as opposed to an honest to god theorem?

I also very much take your point about being sure to strip away any extra assumptions which are not needed. I was proving this as a lemma within context, but that adds both complexity to the code and removes generality so this is good to have pointed out!

This does now look like something I can actually work with, the actual mathematical content of the lemma is incredibly straight forward and I imagine shouldn't be too hard to write up (we shall see), but ive just not been able to work out how to actually state something I can begin to prove, or I guess, construct, so thank you for your help in that!

[Aaron Liu]

In Lean, proof irrelevance means that the proof of a theorem doesn't matter. So if you need to see the proof to use the "theorem", then it's not a theorem.

example: First Isomorphism "Theorem" says $G / \ker f \cong \operatorname{im} f$. But when you use it, you need to know that the isomorphism sends the equivalence class of $x$ to $f(x)$, so it's not a theorem.

[Kevin Buzzard]

Yes, the first isomorphism "theorem" is a great example of this. If it were just a theorem, saying "there happens to exist an isomorphism $G/ker(f)\cong Im(f)$" then you would never be able to do a diagram chase, because this theorem doesn't tell you what the map is. This has nothing to do with "complicated type-theoretic difference"s, this is simply about thinking precisely about mathematics. The useful form of the first isomorphism "theorem" is a definition of a map $G/ker(f)\to Im(f)$ and then a theorem about that definition, saying that that specific map is an isomorphism. This is what mathematicians use in practice. Similarly here you don't just want to know that $End_R(S^n)$ and $M_n(End_R(S))$ are in bijection, you want to know what the bijection is, so you should not just state a theorem saying they're isomorphic or in bijection or whatever, the package in a formal statement of what you need should include the data of the maps because this is what you'll use to do computations, and data is not theorems. The type theory part of things is that in Lean there are two universes, Type and Prop, and the types in the Type universe are data like the real numbers and groups and so on, and the types in the Prop universe are theorem statements. Terms in the Type universe are things like elements of groups, functions and so on; terms in the Prop universe are proofs. Formalizing makes you understand much better exactly where in Lean's world everything goes, in this way of organizing mathematics. But the fact that the first isomorphism theorem is more than a theorem isn't really anything to do with type theory, it's just something which mathematicians tend to sweep under the carpet but once someone explains it to you you're like "oh yeah I guess the actual definition of the map is sometimes important".

[metakuntyyy]

@Kevin Buzzard That are some wonderful explanations. I wonder if the explanations of your courses have changed since you started formalising in lean.

[Kevin Buzzard]

I guess the way I think about mathematics has changed since I started formalizing in the sense that I now understand the foundations much better, but nowadays I am mostly teaching Lean courses so that involves writing exactly the kind of code which I wrote above.