16 Associative rings and algebras

TheoremFocal subgroup theorem#

The Focal Subgroup Theorem

For a Sylow p-subgroup P of a finite group G, P ∩ G' = P*, where P* is the focal subgroup of P.

Subgroup.commutator_inf_eq_focalSubgroup.{u_1} {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)]
  (P : Sylow p G) [(↑P).FiniteIndex] : commutator G ⊓ ↑P = (↑P).focalSubgroup
Sources
MathlibSubgroup.commutator_inf_eq_focalSubgroup
Uses 10
Statement usesIndex of a subgroup · Integer · Irreducible element · Subgroup generated by a subset
Proof usesCardinal · Euclid's' algorithm · Periodic points · Ring morphism · Ring structure \(\Z\) · Third Sylow theorem

TheoremWedderburn–Artin theorem#

Mathlib records this with 2 declarations.

IsSimpleRing.exists_algEquiv_matrix_divisionRing: The Wedderburn–Artin Theorem, algebra form: an Artinian simple algebra is isomorphic to a matrix algebra over a division algebra.

IsSimpleRing.exists_algEquiv_matrix_divisionRing.{u, u_1} (R₀ : Type u_1) (R : Type u)
  [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSimpleRing R] [IsArtinianRing R] :
  ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing: The Wedderburn–Artin Theorem, algebra form: a semisimple algebra is isomorphic to a product of matrix algebras over division algebras.

IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing.{u, u_1} (R₀ : Type u_1) (R : Type u)
  [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSemisimpleRing R] :
  ∃ n D d x x_1,
    (∀ (i : Fin n), NeZero (d i)) ∧
      Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
Sources
MathlibIsSimpleRing.exists_algEquiv_matrix_divisionRing · IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing
Uses 10
Statement usesAssociative algebra over a commutative ring · Finite set · Rational number · Ring-valued matrix · Sum of subspaces
Proof usesAlgebra of endomorphisms of a vector space · Cardinal · Ideal of a commutative ring · Noetherian module · Range of a linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.