theorem linearEquiv_of_isSimpleModule_over_simple_ring (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (M N : Type w) [AddCommGroup M] [AddCommGroup N] [Module A M] [Module A N] [IsSimpleModule A M] [IsSimpleModule A N] : Nonempty (M ≃ₗ[A] N)

Stacks Tag 074E ((1))

theorem directSum_simple_module_over_simple_ring (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (M : Type v) [AddCommGroup M] [Module A M] : ∃ (S : Type v) (x : AddCommGroup S) (x_1 : Module A S) (_ : IsSimpleModule A S) (ι : Type v), Nonempty (M ≃ₗ[A] ι →₀ S)

theorem directSum_simple_module_over_simple_ring' (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (M : Type v) [AddCommGroup M] [Module A M] (S : Type v) [AddCommGroup S] [Module A S] [IsSimpleModule A S] : ∃ (ι : Type v), Nonempty (M ≃ₗ[A] ι →₀ S)

theorem linearEquiv_iff_finrank_eq_over_simple_ring (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (M N : Type v) [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [Module k M] [Module k N] [IsScalarTower k A M] [IsScalarTower k A N] [Module.Finite A M] [Module.Finite A N] : Nonempty (M ≃ₗ[A] N) ↔ Module.finrank k M = Module.finrank k N

theorem simple_mod_of_wedderburn (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] {n : ℕ} (hn : n ≠ 0) (D : Type v) [DivisionRing D] [Algebra k D] (wdb : A ≃ₐ[k] Matrix (Fin n) (Fin n) D) : have x := Module.compHom (Fin n → D) wdb.toRingEquiv.toRingHom; IsSimpleModule A (Fin n → D)

Stacks Tag 074E ((3) first part)

@[reducible, inline]

abbrev endCatEquiv (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] (n : ℕ) (D : Type v) [DivisionRing D] [Algebra k D] (wdb : A ≃ₐ[k] Matrix (Fin n) (Fin n) D) [Module A (Fin n → D)] (smul_def : ∀ (a : A) (v : Fin n → D), a • v = wdb a • v) [IsScalarTower k (Matrix (Fin n) (Fin n) D) (Fin n → D)] [IsScalarTower k A (Fin n → D)] [SMulCommClass A k (Fin n → D)] : Module.End A (Fin n → D) ≃ₐ[k] Module.End (Matrix (Fin n) (Fin n) D) (Fin n → D)

Equations

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

noncomputable def matrixModuleEndAlgEquivMop (k : Type u) [Field k] {n : ℕ} [NeZero n] (D : Type v) [DivisionRing D] [Algebra k D] [IsScalarTower k (Matrix (Fin n) (Fin n) D) (Fin n → D)] [SMulCommClass (Matrix (Fin n) (Fin n) D) k (Fin n → D)] : Module.End (Matrix (Fin n) (Fin n) D) (Fin n → D) ≃ₐ[k] Dᵐᵒᵖ

Equations

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

noncomputable def end_simple_mod_of_wedderburn (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] (n : ℕ) (hn : n ≠ 0) (D : Type v) [DivisionRing D] [Algebra k D] (wdb : A ≃ₐ[k] Matrix (Fin n) (Fin n) D) : let x := Module.compHom (Fin n → D) wdb.toRingEquiv.toRingHom; have this := ⋯; Module.End A (Fin n → D) ≃ₐ[k] Dᵐᵒᵖ

Stacks Tag 074E ((3) first part)

Equations

• end_simple_mod_of_wedderburn k A n hn D wdb = (endCatEquiv k A n D wdb ⋯).trans (matrixModuleEndAlgEquivMop k D)

theorem end_simple_mod_of_wedderburn' (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (n : ℕ) (hn : n ≠ 0) (D : Type v) [DivisionRing D] [Algebra k D] (wdb : A ≃ₐ[k] Matrix (Fin n) (Fin n) D) (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] [Module k M] [IsScalarTower k A M] : Nonempty (Module.End A M ≃ₐ[k] Dᵐᵒᵖ)

instance end_simple_mod_finite (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] [Module k M] [IsScalarTower k A M] : FiniteDimensional k (Module.End A M)

@[implicit_reducible]

instance instAlgebraEndOfIsScalarTower_brauerGroup (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] (M : Type v) [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] : Algebra k (Module.End (Module.End A M) M)

Equations

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

theorem exists_gen (A : Type v) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] : ∃ (m : M), m ≠ 0 ∧ ∀ (m' : M), ∃ (a : A), m' = a • m

noncomputable def gen (A : Type v) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] : M

Equations

• gen A M = ⋯.choose

theorem gen_ne_zero (A : Type v) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] : gen A M ≠ 0

theorem gen_spec (A : Type v) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] (m' : M) : ∃ (a : A), m' = a • gen A M

def toEndEnd (A : Type v) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : A →ₗ[A] Module.End (Module.End A M) M

Equations

• toEndEnd A M = { toFun := fun (a : A) => DistribSMul.toLinearMap (Module.End A M) M a, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem toEndEnd_apply (A : Type v) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] (a : A) : (toEndEnd A M) a = DistribSMul.toLinearMap (Module.End A M) M a

def toEndEndAlgHom (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] (M : Type v) [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] : A →ₐ[k] Module.End (Module.End A M) M

Equations

• toEndEndAlgHom k A M = { toFun := (toEndEnd A M).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

instance instNontrivialEndOfIsSimpleModule_brauerGroup (A : Type v) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] : Nontrivial (Module.End (Module.End A M) M)

theorem toEndEnd_injective (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] [Module k M] [IsScalarTower k A M] : Function.Injective ⇑(toEndEnd A M)

class IsBalanced (A : Type v) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : Prop

• surj : Function.Surjective ⇑(toEndEnd A M)

instance instIsBalanced (A : Type v) [Ring A] : IsBalanced A A

theorem IsBalanced.congr_aux (A : Type v) [Ring A] (M N : Type v) [AddCommGroup M] [AddCommGroup N] [Module A M] [Module A N] (l : M ≃ₗ[A] N) (h : IsBalanced A M) : IsBalanced A N

theorem IsBalanced.congr (A : Type v) [Ring A] {M N : Type v} [AddCommGroup M] [AddCommGroup N] [Module A M] [Module A N] (l : M ≃ₗ[A] N) : IsBalanced A M ↔ IsBalanced A N

theorem isBalanced_of_simpleMod (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] [Module k M] [IsScalarTower k A M] : IsBalanced A M

noncomputable def end_end_iso (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (M : Type v) [AddCommGroup M] [Module A M] [IsSimpleModule A M] [Module k M] [IsScalarTower k A M] : A ≃ₐ[k] Module.End (Module.End A M) M

Equations

• end_end_iso k A M = AlgEquiv.ofBijective (toEndEndAlgHom k A M) ⋯

theorem Wedderburn_Artin_uniqueness₀ (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (n n' : ℕ) [NeZero n] [NeZero n'] (D : Type v) [DivisionRing D] [Algebra k D] (wdb : A ≃ₐ[k] Matrix (Fin n) (Fin n) D) (D' : Type v) [DivisionRing D'] [Algebra k D'] (wdb' : A ≃ₐ[k] Matrix (Fin n') (Fin n') D') : Nonempty (D ≃ₐ[k] D')

theorem Wedderburn_Artin_uniqueness₁ (k : Type u) (A : Type v) [Field k] [Ring A] [Algebra k A] [IsSimpleRing A] [FiniteDimensional k A] (n n' : ℕ) [NeZero n] [NeZero n'] (D : Type v) [DivisionRing D] [Algebra k D] (wdb : A ≃ₐ[k] Matrix (Fin n) (Fin n) D) (D' : Type v) [DivisionRing D'] [Algebra k D'] (wdb' : A ≃ₐ[k] Matrix (Fin n') (Fin n') D') : n = n'