Algebraic Groups.Linear Algebraic Groups

Theorem Affine Finite-Type Groups Have Faithful Finite-Dimensional Representations admitted

Theorem Affine G-Varieties Embed Equivariantly in Representations admitted

Definition Algebraic Group Actions, Orbits, and Stabilizers admitted

Theorem Algebraic Groups Are Closed Subgroups of GL_n admitted

Topic Automorphism Groups admitted

Topic Basic Examples admitted

Theorem Commutative Algebraic Groups Split into Semisimple and Unipotent Parts admitted

Topic Conjugacy Classes admitted

Topic Connected Components admitted

Theorem Connected Subgroups Generate a Closed Connected Subgroup admitted

Definition Definition of Linear Algebraic Groups needs_definition_review

Theorem Embedding Theorem for Algebraic Groups admitted

Theorem Field of Definition for Subgroups of F-Groups admitted

Definition General Linear Group Scheme GL(V) formalized

Theorem Identity Component Is Closed Normal of Finite Index admitted

Theorem Image of an Algebraic Group Homomorphism Is Closed admitted

Theorem Jordan Decomposition in a Linear Algebraic Group admitted

Topic Kernels, Images, and Quotients admitted

Theorem Lang Theorem for Connected Algebraic Groups over Finite Fields admitted

Definition Lie Algebra of an Algebraic Group admitted

Theorem Lie-Kolchin Theorem admitted

Topic Linear Algebraic Groups admitted

Topic Morphisms and Closed Subgroups admitted

Theorem Orbits of Algebraic Group Actions Are Locally Closed admitted

Theorem Quotient by a Closed Subgroup Exists admitted

Topic Smoothness, Tangent Spaces, and Lie Algebras admitted

Theorem Unipotent Subgroups Are Triangularizable admitted