def TwoSidedIdeal.mapMatrix (A : Type u_1) [Ring A] (ι : Type) [Fintype ι] (I : TwoSidedIdeal A) : TwoSidedIdeal (Matrix ι ι A)

If I is a two-sided-ideal of A, then Mₙ(I) := {(xᵢⱼ) | ∀ i j, xᵢⱼ ∈ I} is a two-sided-ideal of Mₙ(A).

Equations

• TwoSidedIdeal.mapMatrix A ι I = { ringCon := { r := fun (X Y : Matrix ι ι A) => ∀ (i j : ι), I.ringCon (X i j) (Y i j), iseqv := ⋯, mul' := ⋯, add' := ⋯ } }

@[simp]

theorem TwoSidedIdeal.mapMatrix_ringCon_r (A : Type u_1) [Ring A] (ι : Type) [Fintype ι] (I : TwoSidedIdeal A) (X Y : Matrix ι ι A) : (mapMatrix A ι I).ringCon.toSetoid X Y = ∀ (i j : ι), I.ringCon (X i j) (Y i j)

@[simp]

theorem TwoSidedIdeal.mem_mapMatrix (A : Type u_1) [Ring A] (ι : Type) [Fintype ι] (I : TwoSidedIdeal A) (x : Matrix ι ι A) : x ∈ mapMatrix A ι I ↔ ∀ (i j : ι), x i j ∈ I

def TwoSidedIdeal.equivRingConMatrix (A : Type u_1) [Ring A] (ι : Type) [Fintype ι] (oo : ι) : TwoSidedIdeal A ≃ TwoSidedIdeal (Matrix ι ι A)

The two-sided-ideals of A corresponds bijectively to that of Mₙ(A). Given an ideal I ≤ A, we send it to Mₙ(I). Given an ideal J ≤ Mₙ(A), we send it to {x₀₀ | x ∈ J}.

Equations

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

@[simp]

theorem TwoSidedIdeal.equivRingConMatrix_apply (A : Type u_1) [Ring A] (ι : Type) [Fintype ι] (oo : ι) (I : TwoSidedIdeal A) : (equivRingConMatrix A ι oo) I = mapMatrix A ι I

@[simp]

theorem TwoSidedIdeal.equivRingConMatrix_symm_apply (A : Type u_1) [Ring A] (ι : Type) [Fintype ι] (oo : ι) (J : TwoSidedIdeal (Matrix ι ι A)) : (equivRingConMatrix A ι oo).symm J = mk' ((fun (x : Matrix ι ι A) => x oo oo) '' ↑J) ⋯ ⋯ ⋯ ⋯ ⋯

def TwoSidedIdeal.equivRingConMatrix' (A : Type u_1) [Ring A] (ι : Type) [Fintype ι] (oo : ι) : TwoSidedIdeal A ≃o TwoSidedIdeal (Matrix ι ι A)

The two-sided-ideals of A corresponds bijectively to that of Mₙ(A). Given an ideal I ≤ A, we send it to Mₙ(I). Given an ideal J ≤ Mₙ(A), we send it to {x₀₀ | x ∈ J}.

Equations

• TwoSidedIdeal.equivRingConMatrix' A ι oo = { toEquiv := TwoSidedIdeal.equivRingConMatrix A ι oo, map_rel_iff' := ⋯ }

@[simp]

theorem TwoSidedIdeal.equivRingConMatrix'_apply_ringCon_r (A : Type u_1) [Ring A] (ι : Type) [Fintype ι] (oo : ι) (I : TwoSidedIdeal A) (X Y : Matrix ι ι A) : ((equivRingConMatrix' A ι oo) I).ringCon.toSetoid X Y = ∀ (i j : ι), I.ringCon (X i j) (Y i j)

@[simp]

theorem TwoSidedIdeal.equivRingConMatrix'_symm_apply_ringCon_r (A : Type u_1) [Ring A] (ι : Type) [Fintype ι] (oo : ι) (J : TwoSidedIdeal (Matrix ι ι A)) (x y : A) : ((RelIso.symm (equivRingConMatrix' A ι oo)) J).ringCon.toSetoid x y = ∃ x_1 ∈ J, x_1 oo oo = x - y

instance op_simple (A : Type u_1) [Ring A] [IsSimpleRing A] : IsSimpleRing Aᵐᵒᵖ

def mopToEnd (A : Type u_1) [Ring A] : Aᵐᵒᵖ →+* Module.End A A

The canonical map from Aᵒᵖ to Hom(A, A)

Equations

• mopToEnd A = { toFun := fun (a : Aᵐᵒᵖ) => { toFun := fun (x : A) => x * MulOpposite.unop a, map_add' := ⋯, map_smul' := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem mopToEnd_apply_apply (A : Type u_1) [Ring A] (a : Aᵐᵒᵖ) (x : A) : ((mopToEnd A) a) x = x * MulOpposite.unop a

def toEndMop (A : Type u_1) [Ring A] : A →+* (Module.End A A)ᵐᵒᵖ

The canonical map from A to Hom(A, A)ᵒᵖ

Equations

• toEndMop A = { toFun := fun (a : A) => MulOpposite.op { toFun := fun (x : A) => x * a, map_add' := ⋯, map_smul' := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem toEndMop_apply (A : Type u_1) [Ring A] (a : A) : (toEndMop A) a = MulOpposite.op { toFun := fun (x : A) => x * a, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def mopEquivEnd (A : Type u_1) [Ring A] : Aᵐᵒᵖ ≃+* Module.End A A

the map Aᵒᵖ → Hom(A, A) is bijective

Equations

• mopEquivEnd A = RingEquiv.ofBijective (mopToEnd A) ⋯

noncomputable def equivEndMop (A : Type u_1) [Ring A] : A ≃+* (Module.End A A)ᵐᵒᵖ

the map Aᵒᵖ → Hom(A, A) is bijective

Equations

• equivEndMop A = RingEquiv.ofBijective (toEndMop A) ⋯

@[simp]

theorem equivEndMop_symm_apply (A : Type u_1) [Ring A] (b : (Module.End A A)ᵐᵒᵖ) : (equivEndMop A).symm b = Function.surjInv ⋯ b

@[simp]

theorem equivEndMop_apply (A : Type u_1) [Ring A] (a : A) : (equivEndMop A) a = MulOpposite.op { toFun := fun (x : A) => x * a, map_add' := ⋯, map_smul' := ⋯ }

def matrixEquivMatrixMop (n : ℕ) (D : Type u_4) [Ring D] : Matrix (Fin n) (Fin n) Dᵐᵒᵖ ≃+* (Matrix (Fin n) (Fin n) D)ᵐᵒᵖ

For any ring D, Mₙ(D) ≅ Mₙ(D)ᵒᵖ.

Equations

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

@[simp]

theorem matrixEquivMatrixMop_apply (n : ℕ) (D : Type u_4) [Ring D] (M : Matrix (Fin n) (Fin n) Dᵐᵒᵖ) : (matrixEquivMatrixMop n D) M = MulOpposite.op (M.transpose.map fun (d : Dᵐᵒᵖ) => MulOpposite.unop d)

@[simp]

theorem matrixEquivMatrixMop_symm_apply (n : ℕ) (D : Type u_4) [Ring D] (M : (Matrix (Fin n) (Fin n) D)ᵐᵒᵖ) : (matrixEquivMatrixMop n D).symm M = (MulOpposite.unop M).transpose.map fun (d : D) => MulOpposite.op d

theorem Ideal.eq_of_le_of_isSimpleModule {A : Type u} [Ring A] (I : Ideal A) [simple : IsSimpleModule A ↥I] (J : Ideal A) (ineq : J ≤ I) (a : A) (ne_zero : a ≠ 0) (mem : a ∈ J) : J = I

theorem minimal_ideal_isSimpleModule {A : Type u} [Ring A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) (I_minimal : ∀ (J : Ideal A), J ≠ ⊥ → ¬J < I) : IsSimpleModule A ↥I

theorem Wedderburn_Artin.aux.one_eq {A : Type u} [Ring A] [simple : IsSimpleRing A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) : ∃ (n : ℕ) (x : Fin n → A) (i : Fin n → ↥I), ∑ j : Fin n, ↑(i j) * x j = 1

@[reducible, inline]

noncomputable abbrev Wedderburn_Artin.aux.n {A : Type u} [Ring A] [simple : IsSimpleRing A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) : ℕ

Equations

• Wedderburn_Artin.aux.n I I_nontrivial = Nat.find ⋯

@[reducible, inline]

noncomputable abbrev Wedderburn_Artin.aux.x {A : Type u} [Ring A] [simple : IsSimpleRing A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) : Fin (n I I_nontrivial) → A

Equations

• Wedderburn_Artin.aux.x I I_nontrivial = ⋯.choose

@[reducible, inline]

noncomputable abbrev Wedderburn_Artin.aux.i {A : Type u} [Ring A] [simple : IsSimpleRing A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) : Fin (n I I_nontrivial) → ↥I

Equations

• Wedderburn_Artin.aux.i I I_nontrivial = ⋯.choose

@[reducible, inline]

noncomputable abbrev Wedderburn_Artin.aux.nxi_spec {A : Type u} [Ring A] [simple : IsSimpleRing A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) : ∑ j : Fin (n I I_nontrivial), ↑(i I I_nontrivial j) * x I I_nontrivial j = 1

Equations

• ⋯ = ⋯

theorem Wedderburn_Artin.aux.n_ne_zero {A : Type u} [Ring A] [simple : IsSimpleRing A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) : NeZero (n I I_nontrivial)

@[reducible, inline]

noncomputable abbrev Wedderburn_Artin.aux.nxi_ne_zero {A : Type u} [Ring A] [simple : IsSimpleRing A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) (j : Fin (n I I_nontrivial)) : x I I_nontrivial j ≠ 0 ∧ i I I_nontrivial j ≠ 0

Equations

• ⋯ = ⋯

theorem Wedderburn_Artin.aux.equivIdeal {A : Type u} [Ring A] [simple : IsSimpleRing A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) (I_minimal : ∀ (J : Ideal A), J ≠ ⊥ → ¬J < I) : ∃ (n : ℕ) (_ : NeZero n), Nonempty ((Fin n → ↥I) ≃ₗ[A] A)

def endPowEquivMatrix (A : Type u_4) [Ring A] (M : Type u_5) [AddCommGroup M] [Module A M] (n : ℕ) : Module.End A (Fin n → M) ≃+* Matrix (Fin n) (Fin n) (Module.End A M)

Equations

• endPowEquivMatrix A M n = ↑(endVecAlgEquivMatrixEnd (Fin n) ℤ A M)

theorem Wedderburn_Artin_ideal_version (A : Type u) [Ring A] [IsArtinianRing A] [simple : IsSimpleRing A] : ∃ (n : ℕ) (_ : NeZero n) (I : Ideal A) (_ : IsSimpleModule A ↥I), Nonempty ((Fin n → ↥I) ≃ₗ[A] A)

theorem Wedderburn_Artin (A : Type u) [Ring A] [IsArtinianRing A] [simple : IsSimpleRing A] : ∃ (n : ℕ) (_ : NeZero n) (I : Ideal A) (_ : IsSimpleModule A ↥I), Nonempty (A ≃+* Matrix (Fin n) (Fin n) (Module.End A ↥I)ᵐᵒᵖ)

theorem Wedderburn_Artin' (A : Type u) [Ring A] [IsArtinianRing A] [simple : IsSimpleRing A] : ∃ (n : ℕ) (_ : NeZero n) (S : Type u) (x : DivisionRing S), Nonempty (A ≃+* Matrix (Fin n) (Fin n) S)

theorem Wedderburn_Artin_divisionRing_unique (D E : Type u) [DivisionRing D] [DivisionRing E] (m n : ℕ) [hm : NeZero m] [hn : NeZero n] (iso : Matrix (Fin m) (Fin m) D ≃+* Matrix (Fin n) (Fin n) E) : Nonempty (D ≃+* E)

theorem Matrix.mem_center_iff' (K : Type u_2) (R : Type u_3) [Field K] [Ring R] [Algebra K R] (n : ℕ) (M : Matrix (Fin n) (Fin n) R) : M ∈ Subalgebra.center K (Matrix (Fin n) (Fin n) R) ↔ ∃ (α : ↥(Subalgebra.center K R)), M = α • 1

theorem RingEquiv.mem_center_iff {R1 : Type u_2} {R2 : Type u_3} [Ring R1] [Ring R2] (e : R1 ≃+* R2) (x : R1) : x ∈ Subring.center R1 ↔ e x ∈ Subring.center R2

def algebraMapEndIdealMop (K : Type u) {B : Type v} [Field K] [Ring B] [Algebra K B] (I : Ideal B) : K →+* (Module.End B ↥I)ᵐᵒᵖ

For a K-algebra B, there is a map from I : Ideal B to End(I)ᵒᵖ defined by k ↦ x ↦ k • x.

Equations

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

@[simp]

theorem algebraMapEndIdealMop_apply (K : Type u) {B : Type v} [Field K] [Ring B] [Algebra K B] (I : Ideal B) (k : K) : (algebraMapEndIdealMop K I) k = MulOpposite.op { toFun := fun (x : ↥I) => k • x, map_add' := ⋯, map_smul' := ⋯ }

instance instAlgebraMulOppositeEndSubtypeMemIdeal_brauerGroup (K : Type u) (B : Type v) [Field K] [Ring B] [Algebra K B] (I : Ideal B) : Algebra K (Module.End B ↥I)ᵐᵒᵖ

Equations

• instAlgebraMulOppositeEndSubtypeMemIdeal_brauerGroup K B I = Algebra.mk (algebraMapEndIdealMop K I) ⋯ ⋯

theorem algebraEndIdealMop.algebraMap_eq (K : Type u) (B : Type v) [Field K] [Ring B] [Algebra K B] (I : Ideal B) : algebraMap K (Module.End B ↥I)ᵐᵒᵖ = algebraMapEndIdealMop K I

theorem Wedderburn_Artin_algebra_version (K : Type u) (B : Type v) [Field K] [Ring B] [Algebra K B] [FiniteDimensional K B] [sim : IsSimpleRing B] : ∃ (n : ℕ) (_ : NeZero n) (S : Type v) (x : DivisionRing S) (x_1 : Algebra K S), Nonempty (B ≃ₐ[K] Matrix (Fin n) (Fin n) S)

theorem is_central_of_wdb (K : Type u) (B : Type v) [Field K] [Ring B] [Algebra K B] [hctr : Algebra.IsCentral K B] (n : ℕ) (S : Type u_2) [NeZero n] [h : DivisionRing S] [Algebra K S] (Wdb : B ≃ₐ[K] Matrix (Fin n) (Fin n) S) : Algebra.IsCentral K S

theorem is_fin_dim_of_wdb (K : Type u) (B : Type v) [Field K] [Ring B] [Algebra K B] [FiniteDimensional K B] (n : ℕ) (S : Type u_2) [NeZero n] [h : DivisionRing S] [Algebra K S] (Wdb : B ≃ₐ[K] Matrix (Fin n) (Fin n) S) : FiniteDimensional K S

theorem bijective_algebraMap_of_finiteDimensional_divisionRing_over_algClosed (K : Type u_2) (D : Type u_3) [Field K] [IsAlgClosed K] [DivisionRing D] [alg : Algebra K D] [FiniteDimensional K D] : Function.Bijective ⇑(algebraMap K D)

theorem simple_eq_matrix_algClosed (K : Type u) (B : Type v) [Field K] [Ring B] [Algebra K B] [FiniteDimensional K B] [IsAlgClosed K] [IsSimpleRing B] : ∃ (n : ℕ) (_ : NeZero n), Nonempty (B ≃ₐ[K] Matrix (Fin n) (Fin n) K)