LeanPool.BrauerGroupNew.Wedderburn

Imported Lean Pool material for LeanPool.BrauerGroupNew.Wedderburn.

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 = TwoSidedIdeal.mk' {X : Matrix ι ι A | ∀ (i j : ι), X i j ∈ I} ⋯ ⋯ ⋯ ⋯ ⋯

@[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_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) ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

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

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'_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

@[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 : ι), x i j - y i j ∈ I

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_apply (A : Type u_1) [Ring A] (a : A) : (equivEndMop A) a = MulOpposite.op { toFun := fun (x : A) => x * a, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

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

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) [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 WedderburnArtin.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 WedderburnArtin.aux.n {A : Type u} [Ring A] [simple : IsSimpleRing A] (I : Ideal A) (I_nontrivial : I ≠ ⊥) : ℕ

The minimal number of summands representing 1 from a nontrivial ideal in the Wedderburn-Artin proof.

Equations

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

@[reducible, inline]

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

The right factors in the chosen minimal representation of 1.

Equations

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

@[reducible, inline]

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

The ideal-valued left factors in the chosen minimal representation of 1.

Equations

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

theorem WedderburnArtin.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

The chosen representation of 1 by the auxiliary Wedderburn-Artin data.

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

theorem WedderburnArtin.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

theorem WedderburnArtin.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 : ℕ), n ≠ 0 ∧ 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)

Endomorphisms of a finite product are equivalent to matrices over endomorphisms of one factor.

Equations

• endPowEquivMatrix A M n = (endVecAlgEquivMatrixEnd (Fin n) ℤ A M).toRingEquiv

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

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

theorem WedderburnArtin' (A : Type u) [Ring A] [IsArtinianRing A] [simple : IsSimpleRing A] : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (S : Type u) (x : DivisionRing S), Nonempty (A ≃+* Matrix (Fin n) (Fin n) S)

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_reducible]

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

Equations

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

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 WedderburnArtin_algebra_version' (R : Type u) (A : Type v) [CommRing R] [Ring A] [sim : IsSimpleRing A] [Algebra R A] [hA : IsArtinianRing A] : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (S : Type v) (x : DivisionRing S) (x_1 : Algebra R S), Nonempty (A ≃ₐ[R] Matrix (Fin n) (Fin n) S)

theorem WedderburnArtin_algebra_version (K : Type u) (B : Type v) [Field K] [Ring B] [Algebra K B] [FiniteDimensional K B] [sim : IsSimpleRing B] : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (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) (hn : n ≠ 0) [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 : ℕ} (hn : n ≠ 0) (S : Type u_2) [h : DivisionRing S] [Algebra K S] (Wdb : B ≃ₐ[K] Matrix (Fin n) (Fin n) S) : FiniteDimensional K S

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 : ℕ), n ≠ 0 ∧ Nonempty (B ≃ₐ[K] Matrix (Fin n) (Fin n) K)