Matrix AlgHom implies dim divisibility

Stream: Is there code for X?

[张守信(Shouxin Zhang)]

Let $\varphi: M^{n \times n}(\mathbb{F}) \to M^{m \times m}(\mathbb{F})$ be a unital algebra homomorphism. Prove that $n ∣ m$.

This was the final question in the Advanced Algebra section of the graduate entrance exam for the Mathematics Department at the University of Chinese Academy of Sciences (UCAS). (In China, math majors at typical universities tend to be more interested in the basic calculus and linear algebra problems directly related to the graduate school entrance exam, rather than problems from more advanced courses. So, at one point last year, I spent some time formalizing simple linear algebra exercises, hoping to attract more fellow students to get involved with Lean4 for formalization out of interest. This is the direct motivation for me to formalize this question.)

Mathematically, proving this is straightforward using some results about simple modules. However, I recall that when I attempted to formalize this proof in Lean4 last year, the mathlib infrastructure seemed insufficient.

I'm wondering if the library's infrastructure is adequate now to complete this formalization.

[张守信(Shouxin Zhang)]

An MWE is here:

import Mathlib

example {F : Type*} [Field F] {n m : ℕ} (hn : 0 < n)
  (φ : Matrix (Fin n) (Fin n) F →ₐ[F] Matrix (Fin m) (Fin m) F) :
  n ∣ m := by

  sorry

And a math proof:
Consider $\mathbb{F}^m$ as a left $M^{m \times m}(\mathbb{F})$-module and endow it with an $M^{n \times n}(\mathbb{F})$-module structure via the unital homomorphism $\varphi$ by $A \cdot v = \varphi(A)v$. Since $M^{n \times n}(\mathbb{F})$ is a simple (hence semisimple) algebra whose unique (up to isomorphism) simple left module is $S = \mathbb{F}^n$ (of dimension $n$), $\mathbb{F}^m$ as an $M^{n \times n}(\mathbb{F})$-module must be isomorphic to a direct sum $S^{\oplus k}$ for some integer $k \ge 1$ (as $\varphi$ is unital and $m \ge 1$). Comparing dimensions as $\mathbb{F}$-vector spaces yields $m = \dim_{\mathbb{F}}(\mathbb{F}^m) = \dim_{\mathbb{F}}(S^{\oplus k}) = k \cdot \dim_{\mathbb{F}}(S) = k \cdot n$, thus $n \mid m$.

The most important part is that, according to the Wedderburn–Artin theorem, any module over a semisimple algebra can be decomposed into a direct sum of simple modules. Regarding the Wedderburn–Artin theorem, it was previously in a 'proof-wanted' state. This morning, while browsing posts, I saw that it seemed to be resolved. I was wondering if this is the case?

[Kevin Buzzard]

@Edison Xie ?

[张守信(Shouxin Zhang)]

Seems the result will be pushed in lib soon.
"#Is there code for X? > Matrices form a semisimple ring "

[张守信(Shouxin Zhang)]

I'm not sure if the remaining parts can be solved by the upcoming API, let me check it out...

import Mathlib
set_option maxHeartbeats 0
open Module Matrix

instance {F : Type*} [Field F] {m : ℕ} : Module (Matrix (Fin m) (Fin m) F) (Fin m → F) where
  smul := fun X v => X.mulVec v
  one_smul := by
    intro b
    show (1 : Matrix (Fin m) (Fin m) F).mulVec b = b
    simp only [Matrix.one_mulVec]
  mul_smul := by
    intro x y b
    show (x * y).mulVec b = x.mulVec (y.mulVec b)
    simp only [Matrix.mulVec_mulVec]
  smul_zero := by
    intro x
    show x.mulVec 0 = 0
    simp only [Matrix.mulVec_zero]
  smul_add := by
    intro x a b
    show x.mulVec (a + b) = x.mulVec a + x.mulVec b
    rw [@Matrix.mulVec_add]
  add_smul := by
    intro x y v
    show (x + y).mulVec v = x.mulVec v + y.mulVec v
    rw [@Matrix.add_mulVec]
  zero_smul := by
    intro v
    show (0 : Matrix (Fin m) (Fin m) F).mulVec v = 0
    simp only [Matrix.zero_mulVec]

example {F : Type*} [Field F] {n m : ℕ} (hn : 0 < n)
  (φ : Matrix (Fin n) (Fin n) F →ₐ[F] Matrix (Fin m) (Fin m) F) :
  n ∣ m := by
  let R := Matrix (Fin n) (Fin n) F
  let A := Matrix (Fin m) (Fin m) F
  let V := Fin m → F
  have fin_dim_V : FiniteDimensional F V := inferInstance
  have finrank_V : finrank F V = m := finrank_fin_fun F
  let mod_R_V : Module R V := Module.compHom V φ.toRingHom
  have hn_fact : Fact (0 < n) := ⟨hn⟩
  have is_simple_R : IsSimpleRing (Matrix (Fin n) (Fin n) F) := by
    refine' @IsSimpleRing.matrix ..
    . exact Fin.pos_iff_nonempty.mp hn
    exact DivisionRing.isSimpleRing F
  let S := Fin n → F
  letI : Module R S := by
    unfold R S
    exact {
      smul := by
        intro X v; exact X.mulVec v
      one_smul := by
        intro b
        show (1 : Matrix (Fin n) (Fin n) F).mulVec b = b
        simp only [Matrix.one_mulVec]
      mul_smul := by
        intro x y b
        show (x * y).mulVec b = x.mulVec (y.mulVec b)
        simp only [Matrix.mulVec_mulVec]
      smul_zero := by
        intro x
        show x.mulVec 0 = 0
        simp only [Matrix.mulVec_zero]
      smul_add := by
        intro x a b
        show x.mulVec (a + b) = x.mulVec a + x.mulVec b
        rw [@Matrix.mulVec_add]
      add_smul := by
        intro x y v
        show (x + y).mulVec v = x.mulVec v + y.mulVec v
        rw [@Matrix.add_mulVec]
      zero_smul := by
        intro v
        show (0 : Matrix (Fin n) (Fin n) F).mulVec v = 0
        simp only [Matrix.zero_mulVec]
    }
  letI : IsScalarTower F R V := by
    unfold R
    refine IsScalarTower.of_algebraMap_smul ?_
    intro r x
    rw [@Algebra.algebraMap_eq_smul_one]
    rw [show (r • (1 : R) : R) • (x : V) = (φ (r • (1 : R))) • x by rfl]
    rw [@AlgHom.map_smul_of_tower, map_one]
    rw [show (r • (1 : A)) • (x : V) = (r • (1 : A)).mulVec (x : V) by rfl]
    rw [@smul_mulVec_assoc, one_mulVec]
  letI : IsScalarTower F R (Fin n → F) := by
    unfold R
    refine IsScalarTower.of_algebraMap_smul ?_
    intro r x
    rw [@Algebra.algebraMap_eq_smul_one]
    show (r • (1 : Matrix (Fin n) (Fin n) F)).mulVec x = _
    rw [@smul_mulVec_assoc, one_mulVec]
  letI (k : ℕ) : Module R (Fin k → S) := by
    exact Pi.Function.module (Fin k) (Matrix (Fin n) (Fin n) F) S
  obtain ⟨k, ⟨iso⟩⟩ : ∃ k, Nonempty ((Fin m → F) ≃ₗ[Matrix (Fin n) (Fin n) F] (Fin k → Fin n → F)) := by

    sorry
  let iso_F : V ≃ₗ[F] (Fin k → S) := {
    iso.toAddEquiv with
    map_smul' := by
      intro c v
      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe, RingHom.id_apply]
      haveI : LinearMap.CompatibleSMul V (Fin k → S) F R := by
        unfold V R S
        refine { map_smul := ?_ }
        intro f c' v'
        have h_smul_compat_V : c' • v' = (algebraMap F R c') • v' := by
          rw [show c' • v' = (φ (algebraMap F R c')) *ᵥ v' by
            rw [@AlgHom.map_algebraMap]
            rw [@Algebra.algebraMap_eq_smul_one]
            rw [@smul_mulVec_assoc]
            simp only [one_mulVec]]
          rw [AlgHom.commutes φ c']
          rw [@Algebra.algebraMap_eq_smul_one, smul_mulVec_assoc, one_mulVec]
          rw [@Algebra.algebraMap_eq_smul_one, @smul_one_smul]
        rw [h_smul_compat_V]
        rw [@LinearMap.map_smul_of_tower]
        simp only [algebraMap_smul]
      exact LinearMap.map_smul_of_tower (M := V) (S := R) (M₂ := (Fin k → S)) (fₗ := iso) (R := F) c v
  }
  have finrank_eq := LinearEquiv.finrank_eq iso_F
  rw [show finrank F (Fin k → S) = k * finrank F S by
    rw [finrank_pi_fintype]
    simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul]] at finrank_eq
  rw [finrank_V, finrank_fin_fun F] at finrank_eq
  rw [finrank_eq]
  simp only [dvd_mul_left]

[Edison Xie]

张守信(Shouxin Zhang) said:

The most important part is that, according to the Wedderburn–Artin theorem, any module over a semisimple algebra can be decomposed into a direct sum of simple modules. Regarding the Wedderburn–Artin theorem, it was previously in a 'proof-wanted' state. This morning, while browsing posts, I saw that it seemed to be resolved. I was wondering if this is the case?

the version of wedderburn you want is in #24119 and the unique simple module is in #23963(I also have a version of this in my repo but if @Junyan Xu get his version into mathlib before I finish exam then I guess his way is the way to do)

[张守信(Shouxin Zhang)]

Edison Xie said:

张守信(Shouxin Zhang) said:

The most important part is that, according to the Wedderburn–Artin theorem, any module over a semisimple algebra can be decomposed into a direct sum of simple modules. Regarding the Wedderburn–Artin theorem, it was previously in a 'proof-wanted' state. This morning, while browsing posts, I saw that it seemed to be resolved. I was wondering if this is the case?

the version of wedderburn you want is in #24119 and the unique simple module is in #23963(I also have a version of this in my repo but if Junyan Xu get his version into mathlib before I finish exam then I guess his way is the way to do)

Great!

[Junyan Xu]

Food for thought: let $\varphi:M_n(D_1)\to M_m(D_2)$ be a unital ring homomorphism where $D_1$ and $D_2$ are division rings. Does it follow that $n\mid m$?

Follow-up: can we classify all such homomorphisms? Are they all obtained by composing $M_n(D_1)\to M_n(D_2)$ (induced by $D_1\to D_2$), $M_n(D_2)\to M_m(D_2)$ (induced by $n\mid m$, and an automorphism of $M_m(D_2)$ (which must be inner by Skolem--Noether)? (Update: this is wrong, see below.)

[Edison Xie]

I think so, all the ingredient @张守信(Shouxin Zhang) mentioned works for division rings as well and I have almost all ingredient in my repo (honestly I think it's in your PR as well)

[Junyan Xu]

Notice I'm not assuming $D_1$ and $D_2$ are (finite-dimensional) modules/algebras over some common base, or that the homomorphism is an AlgHom, so it's not clear over what you'd count the dimensions.

[Edison Xie]

ah okay well then if they are not some finite dimensional $k$-algebra then I have no idea

[Junyan Xu]

This is a proof that Gemini 2.5 Pro (experimental) gave me, and I think it's correct. If you don't know about "isomorphic idempotents", it may be easier to think them as conjugate idempotents (which they are in this case).

[Junyan Xu]

The other day I wondered whether every nonzero element in an isotypic semisimple module generates a simple submodule. It's true over a division ring but there are also obvious counterexamples. It's interesting that Gemini worked out a counterexample that is equivalent to a trivial one without realizing there are such trivial counterexamples.
(This was the conversation.)

[Ruben Van de Velde]

I'll believe it when you formalise it :)

[Junyan Xu]

Should I ask Gemini to formalize it? :) The result could also be formulated as saying that the existence of a ring homomorphism between simple Artinian rings A and B implies that that Module.length A A ∣ Module.length B B.

BTW Gemini also pointed out my follow-up question has a negative answer because there are examples like $\mathbb{C}\to M_2(\mathbb{R})$. The classification it gives says in general I need to take $M_n(D_1)\to M_m(D_2)$ induced by $D_1\to M_{m/n}(D_2)$ and compose it with a conjugation.

[Junyan Xu]

Okay, now there are only four sorries left, which are hopefully easy:

import Mathlib.LinearAlgebra.Basis.VectorSpace
import Mathlib.LinearAlgebra.Dimension.Constructions
import Mathlib.LinearAlgebra.Matrix.ToLin
import Mathlib.RingTheory.Idempotents

open Module (End)

variable (R M N ι : Type*) [Semiring R] [Fintype ι] [AddCommMonoid M] [AddCommMonoid N]
  [Module R M] [Module R N]

variable {R M} in
@[simps] def Module.unitsEnd : (End R M)ˣ ≃* (M ≃ₗ[R] M) where
  toFun u := .ofLinear u u.inv u.val_inv u.inv_val
  invFun e := .mk e e.symm (by ext; simp) (by ext; simp)
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl

variable {R ι} in
def matrixEquivEndVecMulOpposite [DecidableEq ι] :
    Matrix ι ι R ≃+* (End R (ι → R))ᵐᵒᵖ :=
  .trans (.opOp _) <| .op <| .trans (.symm .mopMatrix) <| .trans
    (.mapMatrix <| Module.moduleEndSelf _) <| .symm <| endVecRingEquivMatrixEnd ..

namespace LinearMap

variable [DecidableEq ι]

abbrev singleCompProj (i : ι) : End R (ι → R) := single R (fun _ ↦ R) i ∘ₗ proj i

lemma singleCompProj_conjugate (i j : ι) :
    ∃ e : (ι → R) ≃ₗ[R] ι → R, singleCompProj R ι j =
      e ∘ₗ singleCompProj R ι i ∘ₗ e.symm := by
  use LinearEquiv.piCongrLeft R (fun _ ↦ R) (Equiv.swap j i)
  ext k l
  simp only [singleCompProj, coe_comp, coe_single, coe_proj, Function.comp_apply, Function.eval,
    Pi.single_apply, LinearEquiv.piCongrLeft, Equiv.symm_swap, Module.val_unitsEnd_symm_apply,
    Units.inv_eq_val_inv, Module.val_inv_unitsEnd_symm_apply, LinearEquiv.symm_symm,
    LinearEquiv.coe_coe, LinearEquiv.piCongrLeft'_apply, Equiv.swap_apply_right,
    LinearEquiv.piCongrLeft'_symm_apply, Equiv.piCongrLeft'_symm, Equiv.piCongrLeft'_apply]
  split_ifs with h₁ h₂ h₃ h₄ h₅ h₆
  any_goals rfl
  · simp [h₁] at h₃
  · apply (h₁ _).elim; simpa [Equiv.swap_apply_eq_iff] using h₅

variable {R M N} in
def rangeConjEquiv (f : End R M) (e : M ≃ₗ[R] N):
    range (e.toLinearMap ∘ₗ f ∘ₗ e.symm.toLinearMap) ≃ₗ[R] range f :=
  .symm <| .trans (e.submoduleMap _) (.ofEq _ _ <| by simp [range_comp])

end LinearMap

namespace CompleteOrthogonalIdempotents

protected def singleCompProj [DecidableEq ι] :
    CompleteOrthogonalIdempotents (LinearMap.singleCompProj R ι) where
  idem i := by ext; simp
  ortho i j ne := by
    ext k l; simpa [Pi.single_apply] using fun _ h ↦ (ne h).elim
  complete := by ext; simp

variable {R M ι} {e : ι → End R M} (he : CompleteOrthogonalIdempotents e) {i j : ι}
include he

theorem apply_of_ne (ne : i ≠ j) (m : LinearMap.range (e j)) : e i m = 0 := by
  obtain ⟨_, m, rfl⟩ := m; exact congr($(he.ortho ne) m)

theorem apply_same (m : LinearMap.range (e i)) : e i m = m := by
  obtain ⟨_, m, rfl⟩ := m; exact congr($(he.idem i) m)

noncomputable def linearEquiv (he : CompleteOrthogonalIdempotents e) :
    M ≃ₗ[R] Π i, LinearMap.range (e i) := by
  classical
  refine .ofLinear (.pi fun _ ↦ .rangeRestrict _) (.lsum _ _ ℕ fun _ ↦ Submodule.subtype _)
    ?_ (by convert he.complete; ext; simp)
  ext i m j
  simp only [LinearMap.lsum_apply, LinearMap.coe_comp, LinearMap.coeFn_sum,
    Submodule.coe_subtype, LinearMap.coe_proj, LinearMap.coe_single, Function.comp_apply,
    Finset.sum_apply, Function.eval, LinearMap.pi_apply, map_sum, AddSubmonoidClass.coe_finset_sum,
    LinearMap.codRestrict_apply, LinearMap.id_comp]
  rw [Finset.sum_eq_single j, he.apply_same]
  · intro _ _ ne; apply he.apply_of_ne ne.symm
  · intro h; exact (h <| Finset.mem_univ _).elim

end CompleteOrthogonalIdempotents

variable {D E n m : Type*} [DivisionRing D] [DivisionRing E] [Fintype n] [Fintype m]

theorem dvd_of_end_ringHom_end (f : End D (n → D) →+* End E (m → E)) :
    Fintype.card n ∣ Fintype.card m := by
  classical
  have coi := (CompleteOrthogonalIdempotents.singleCompProj D n).map f
  set e := f ∘ LinearMap.singleCompProj D n
  have (i j : n) : ∃ e' : (m → E) ≃ₗ[E] m → E, e j = e' ∘ₗ e i ∘ₗ e'.symm := by
    have ⟨e', eq⟩ := LinearMap.singleCompProj_conjugate D n i j
    use Module.unitsEnd ((Module.unitsEnd.symm e').map f)
    convert congr(f $eq)
    simp_rw [← LinearMap.mul_eq_comp, map_mul]; rfl
  obtain _ | ⟨⟨i⟩⟩ := isEmpty_or_nonempty n
  · cases isEmpty_or_nonempty m; · simp
    exact (not_subsingleton _ f.codomain_trivial).elim
  choose e' eq using this i
  have := coi.linearEquiv.trans (.piCongrRight fun i ↦ .trans
    (.ofEq _ _ <| congr_arg LinearMap.range (eq i)) <|
      LinearMap.rangeConjEquiv _ _) |>.finrank_eq
  rw [Module.finrank_fintype_fun_eq_card, Module.finrank, rank_fun_eq_lift_mul,
    map_mul, Cardinal.toNat_natCast, Cardinal.toNat_lift] at this
  exact ⟨_, this⟩

theorem dvd_of_matrix_ringHom_matrix [DecidableEq n] [DecidableEq m]
    (f : Matrix n n D →+* Matrix m m E) :
    Fintype.card n ∣ Fintype.card m :=
  dvd_of_end_ringHom_end <| (matrixEquivEndVecMulOpposite.toRingHom.comp
    (f.comp matrixEquivEndVecMulOpposite.symm.toRingHom)).unop

[张守信(Shouxin Zhang)]

Thank you for the breakdown of 'sorry'! I'll give it a try at the end of the month! (I'll be free from coursework then >_<

[Junyan Xu]

Sorries are now gone :)

[Junyan Xu]

This is maybe one case of the "Original proof test" for mathematical AI as formulated by @Emily Riehl, though the proof is not formalized by the AI. I used my familiarity with mathlib API to choose Module.End as a substitute for Matrix to avoid defining the action of matrices on vectors, and chose to use conjugate idempotents rather than developing the theory for isomorphic idempotents.

[Emily Riehl]

This is very impressive. (I'll leave it for others who are closer to this area to comment on the "originality" of this argument.)

I feel a little awkward about that talk, which is something like an extended op-ed in the guise of a conference presentation, but the point I feel most strongly about is the one made on slide 18 because I'm worried that soon we'll be facing a flood of "vibe proving". Without formalization, will the human mathematical community be able to vet arguments fast enough to separate the solid proofs from the proofs by intimidation?

[Johan Commelin]

For an example of vibe formalization, see #maths > Lean Formalization of the Riemann Hypothesis – Open for Test
Luckily it is still very easy to find mistakes there. No adversarial exploits with elaborator magic, unicode homoglyphs, non-printing whitespace, etc...

[Junyan Xu]

Another recent success story of Gemini solving a conjecture in the negative: https://x.com/aryehazan/status/1915308472377237554

[张守信(Shouxin Zhang)]

Junyan Xu said:

Another recent success story of Gemini solving a conjecture in the negative: https://x.com/aryehazan/status/1915308472377237554

Given the rapid pace at which LLMs are advancing in mathematical capabilities, I believe that in the future, they will become akin to calculators—essentially serving as "simple conjecture verifiers." :horse: