Reductive Groups Dependency graph

Algebraic Groups
Foundations

No matches

AlgebraicGroups.Forms
AlgebraicGroups.Tori
abv
additive-group
adeles
adjoint
adjoint-action
adjoint-group
adjunction
admissible-sets
affine-algebraic-groups
affine-group-scheme
affine-group-schemes
affine-root-systems
affine-schemes
affine-variety
affine-weyl-groups
algebra-hom
algebraic-fundamental-group
algebraic-group
algebraic-groups
anisotropic
antipode
apartments
automorphisms
b-g
bala-carter
base-change
based-root-data
basic-elements
bd-covers
bialgebra
bn-pairs
borel
borel-subgroup
borel-subgroups
bruhat-decomposition
bruhat-order
bruhat-tits
bruhat-tits-buildings
brylinski-deligne
buildings-and-parahorics
cartan-matrices
cartan-subgroup
center
centers
central-extensions
central-isogenies
centralizer
character
character-lattice
characters
chevalley
chevalley-basis
classical-and-exceptional-groups
classical-groups
classification
closed-subgroup
closed-subgroups
coalgebra
cocharacters
cocycle
cocycles
combinatorics
commutative-algebra
commutative-group
comodule
conjugacy
connected-component
connected-components
connected-group
construction
convolution
coordinate-ring
coordinate-rings
corollary
coroot
coroots
covers
coxeter-complexes
coxeter-groups
cuspidal
decomposition
definition
definitions
deligne-lusztig
derived-group
descent
descent-and-forms
determinant
diagonalizable
diagonalizable-group
diagonalizable-groups
dual-group
dual-groups
dual-root-data
dual-root-systems
duality
dynkin-diagrams
elliptic-elements
embedding-theorem
endoscopy
equivalence
equivariant-embedding
example
examples
exceptional-groups
existence-theorem
extended-groups
external-background
f-group
f-reductive-group
f-split
f-split-torus
f-torus
facets
field-of-definition
fields
finite-field
finite-groups-lie-type
finiteness
fixed-point
formal-deformation
forms
foundational-inputs
frobenius
functor
functor-of-points
fundamental-group
g-structure
galois-action
galois-cohomology
galois-descent
galois-lattice
galois-module
general-linear-group
generated-subgroup
geometric-conjugacy
gl-v
global-fields
group-action
group-like
group-scheme
group-schemes
harish-chandra
homogeneous-space
homomorphism
hopf-algebra
hopf-algebras
hopf-spec
identity-component
images
indexed-root-datum
induced
inner-forms
integral-form
isocrystals
isogeny
isogeny-type
isomorphism-theorem
jacobson-morozov
jordan-decomposition
jordan-zassenhaus
k-theory
k2
kaletha
kernels
kottwitz
kottwitz-homomorphism
kottwitz-map
kottwitz-structures
l-groups
l-morphisms
lang-theorem
langlands
langlands-dual-groups
lemma
levi-decomposition
levi-subgroups
lie-algebra
lie-algebras
lie-kolchin
linear-algebraic-groups
local-fields
locally-closed
lusztig-series
mathlib-aligned
maximal-tori
maximal-torus
metaplectic-covers
morphisms
moy-prasad-filtrations
multiplicative-group
multiplicative-type
newton-map
nilpotent-cone
nilpotent-elements
nilpotent-orbits
nonabelian-h1
norm-one
orbit
orbital-integrals
orthogonal
outer-forms
parabolic
parabolic-subgroups
parahoric-group-schemes
parahoric-subgroups
perverse-sheaves
pinned-dual-groups
pinnings
positive-roots
pure-inner-twists
quantum-groups
quasi-split
quasi-split-forms
quasi-trivial
quotient
quotients
radical
ramification
rank
rank-one
rank-one-subgroup
rational-forms
rational-nilpotent-orbits
rational-points
rational-representation
real-forms
reductive-group
reductive-groups
reductive-quotients
reductive-structure
reflection
regular-elements
regular-semisimple
regular-unipotent
relative-root-datum
relative-weyl-group
representation
resolution
rigid-inner-forms
rigid-inner-twists
root-data
root-data-and-duality
root-data-automorphisms
root-datum
root-lattice
root-pairing
root-subgroup
root-subgroups
root-system
root-systems
roots
roots-of-unity
schubert-variety
semilinear
semisimple
semisimple-elements
semisimple-groups
semisimple-lie-algebra
sigma-conjugacy
simple-roots
simply-connected
simply-connected-cover
sl2-embedding
sl2-triples
smoothness
solvable-group
solvable-groups
spec
special-linear
special-orthogonal
speiser
spherical-buildings
split
split-rank
split-reductive-group
split-reductive-groups
split-torus
splitting-field
splittings
springer
springer-correspondence
stabilizer
stable-conjugacy
strong-inner-forms
strong-real-forms
strongly-regular
structure-constants
subtorus
symplectic
tame
tangent-space
theorem
tits-buildings
tits-index
tits-systems
tori
torsors
torus
trace-formula
triangularization
twisted-conjugacy
twisted-form
twisting
type-B
type-C
type-D
unipotent
unipotent-elements
unipotent-groups
unipotent-orbits
unipotent-radical
unipotent-radicals
unipotent-variety
unramified
valuation-rings
valued-root-data
vogan-diagrams
weakly-induced
weight-lattice
weighted-dynkin-diagrams
weil-restriction
weyl-group
weyl-groups
yoneda

Reductive Linear Algebraic Groups Knowledge DAG

252 nodes across 13 topics.

Dependency graph

Algebraic Groups

Additive Group Scheme 𝔾_a Definition admitted
Adjoint Action Topic admitted
Admissible Sets Topic admitted
Affine Algebraic Groups Topic admitted
Affine Finite-Type Groups Have Faithful Finite-Dimensional Representations Theorem admitted
Affine G-Varieties Embed Equivariantly in Representations Theorem admitted
Affine Group Scheme over a Base Definition admitted
Affine Root Systems Topic admitted
Affine Weyl Groups Topic admitted
Algebra Homomorphisms Form a Group Under Convolution Theorem admitted
Algebraic Fundamental Group Topic admitted
Algebraic Group Actions, Orbits, and Stabilizers Definition admitted
Algebraic Group over a Base Definition admitted
Algebraic Groups Are Closed Subgroups of GL_n Theorem admitted
Algebraic Tori Topic admitted
Algebraic Torus Definition admitted
Anisotropic Torus Definition admitted
Antipode of a Commutative Hopf Algebra Is Multiplicative Theorem admitted
Antipode of a Hopf Algebra Is Anti-Multiplicative Theorem admitted
Automorphism Groups Topic admitted
Automorphisms of Root Data Topic admitted
B(G) Topic admitted
BN-Pairs and Tits Systems Topic admitted
Bala-Carter Classification Topic admitted
Base Change Topic admitted
Base Change Preserves Algebraic Group Structure Theorem admitted
Based Root Data Topic admitted
Basic Examples Topic admitted
Basic Sigma-Conjugacy Classes Topic admitted
Borel Fixed Point Theorem Theorem admitted
Borel Subgroups Topic admitted
Borel Subgroups Are Conjugate and Control Parabolics Theorem admitted
Bruhat Decomposition Theorem admitted
Bruhat Order Gives Schubert Closure Relations Theorem admitted
Bruhat-Tits Apartments Topic admitted
Bruhat-Tits Buildings Topic admitted
Brylinski-Deligne K2-Extensions Topic admitted
Cartan Matrices and Dynkin Diagrams Topic admitted
Cartan Subgroups from Maximal Tori Theorem admitted
Centers and Dual Centers Topic admitted
Central Extensions of Algebraic Groups Topic admitted
Central Isogenies Topic admitted
Central Isogenies and Duality Topic admitted
Character and Cocharacter Lattices Topic admitted
Characterization of Diagonalizable Groups Theorem admitted
Characters Are Group-Like Elements Theorem admitted
Chevalley Basis Definition admitted
Chevalley Existence Theorem Theorem admitted
Chevalley Group Construction from a Root Datum Definition admitted
Chevalley Isomorphism Theorem Theorem admitted
Chevalley Isomorphism Theorem for F-Split Groups Theorem admitted
Classical Groups Topic admitted
Classification of Irreducible Root Systems Theorem admitted
Classification of Rank-One Tori Theorem admitted
Classification of Real Tori Example admitted
Classification of Split Reductive Groups Topic admitted
Cocycles and Twisting Topic admitted
Commutative Algebraic Groups Split into Semisimple and Unipotent Parts Theorem admitted
Comodule over a Coalgebra Definition admitted
Composition with the Antipode Is an Algebra Hom for Commutative Hopf Algebras Theorem admitted
Conjugacy Classes Topic admitted
Conjugacy Classes in the Weyl Group Definition admitted
Connected Components Topic admitted
Connected Subgroups Generate a Closed Connected Subgroup Theorem admitted
Convolution Is Pointwise Multiplication Theorem admitted
Convolution of Algebra Homomorphisms Definition admitted
Convolution of Algebra Homomorphisms Is an Algebra Homomorphism Theorem admitted
Coordinate Hopf Algebra of an Affine Group Scheme Definition admitted
Coordinate Rings and Hopf Algebras Topic admitted
Coxeter Complexes Topic admitted
Coxeter Systems and Bruhat Order Topic admitted
Crystallographic and Reduced Root Systems Definition admitted
Definition of Linear Algebraic Groups Definition needs_definition_review
Derived Group, Center, Adjoint Group, and Simply Connected Cover Topic admitted
Diagonalizable Groups Topic admitted
Diagonalizable Groups Are Dual to Character Groups Theorem admitted
Dual Groups for Covers Topic admitted
Dual Reductive Groups Topic admitted
Dual Root Data Topic admitted
Dual Root Systems Topic admitted
Embedding Theorem for Algebraic Groups Theorem admitted
Essential Image of Spec Is Affine Group Schemes Theorem admitted
Exceptional Groups Topic admitted
Extended Groups for Real Forms Topic admitted
F-Tori Are Classified by Galois Modules Theorem admitted
Facets in Bruhat-Tits Buildings Topic admitted
Faithful Linear Representation Definition admitted
Field of Definition for Subgroups of F-Groups Theorem admitted
Finite-Dimensional Subspace in a Sub-Comodule Lemma admitted
Finiteness of Tori of Bounded Rank Theorem admitted
Fixed Point Theorem for F-Split Solvable Groups Theorem admitted
Forms of Algebraic Groups Topic admitted
Forms of Algebraic Objects Topic admitted
Functor of Points of a Group Scheme Definition admitted
Fundamental Group of a Root Datum Topic admitted
G-Representations Are A-Comodules Theorem admitted
Galois Action on Root Data Topic admitted
Galois Cohomology Topic admitted
Galois Descent for Hopf Algebras Theorem admitted
Galois Descent for Vector Spaces Theorem admitted
Galois Groups and Descent Data Topic admitted
General Linear Group Scheme GL(V) Definition formalized
General Linear Group Scheme GL_n Definition admitted
Geometric Conjugacy and Deligne–Lusztig Theory Definition admitted
Group Object Structure on Spec A via Yoneda Theorem admitted
Hom Into Spec via Global Sections (Spec ⊣ Γ Adjunction) Theorem admitted
Homomorphism of Affine Group Schemes Definition admitted
Homomorphisms of Tori Correspond to Lattice Maps Theorem admitted
Identity Component Is Closed Normal of Finite Index Theorem admitted
Image of an Algebraic Group Homomorphism Is Closed Theorem admitted
Indexed Root Datum of an F-Reductive Group Definition admitted
Induced Torus Definition admitted
Inner Forms Topic admitted
Isocrystals with G-Structure Topic admitted
Isogeny Types from the Root Datum Definition admitted
Jacobson-Morozov Theorem Topic admitted
Jordan Decomposition in Algebraic Groups Theorem admitted
Jordan Decomposition in a Linear Algebraic Group Theorem admitted
Kaletha Refined Inner Forms Topic admitted
Kernels, Images, and Quotients Topic admitted
Kottwitz Homomorphism Topic admitted
Kottwitz Map on B(G) Topic admitted
L-Groups Topic admitted
L-Groups for Covers Topic admitted
L-Morphisms Topic admitted
Lang Theorem for Connected Algebraic Groups over Finite Fields Theorem admitted
Langlands Dual Groups Topic admitted
Levi Decomposition for Parabolic F-Subgroups Theorem admitted
Levi Decomposition of Parabolic Subgroups Theorem admitted
Levi Subgroups and Unipotent Radicals Topic admitted
Lie Algebra of an Algebraic Group Definition admitted
Lie Algebras of Reductive Groups Topic admitted
Lie-Kolchin Theorem Theorem admitted
Linear Algebraic Groups Topic admitted
Local and Global Metaplectic Covers Topic admitted
Maximal F-Split Tori Are G(F)-Conjugate Theorem admitted
Maximal F-Tori Exist in Connected F-Groups Theorem admitted
Maximal Tori Topic admitted
Maximal Tori Are Conjugate Theorem admitted
Morphisms and Closed Subgroups Topic admitted
Moy-Prasad Filtrations Topic admitted
Multiplication of a Commutative Bialgebra Is a Coalgebra Hom Lemma admitted
Multiplicative Group Scheme 𝔾_m Definition admitted
Newton Map Topic admitted
Nilpotent Cone Topic admitted
Nilpotent Elements Topic admitted
Nilpotent Orbits Topic admitted
Nonabelian H1 Topic admitted
Norm-One Torus of a Separable Extension Example admitted
Orbits of Algebraic Group Actions Are Locally Closed Theorem admitted
Outer Forms Topic admitted
Parabolic Subgroups Topic admitted
Parahoric Group Schemes Topic admitted
Parahoric Subgroups Topic admitted
Pinned Dual Groups Topic admitted
Pinnings Topic admitted
Points of GL_n Are Invertible n×n Matrices over R Theorem admitted
Points of 𝔾_a Are the Additive Group of R Theorem admitted
Points of 𝔾_m Are the Units of R Theorem admitted
Pure Inner Twists Topic admitted
Quasi-Split Forms Topic admitted
Quasi-Split and Anisotropic Groups via the Indexed Root Datum Theorem admitted
Quotient by a Closed Subgroup Exists Theorem admitted
R-Points of a Group Scheme Form a Group Theorem admitted
Radical and Derived Group of a Reductive Group Theorem admitted
Rank and Split Rank of a Torus Definition admitted
Rank-One Subgroups and SL₂-Embeddings Definition admitted
Rational Bruhat Decomposition Theorem admitted
Rational Forms of Linear Algebraic Groups Topic admitted
Rational Forms of Reductive Groups Topic admitted
Rational Nilpotent Orbits Topic admitted
Real Forms Topic admitted
Reductive Groups Topic admitted
Reductive Groups over Local Fields Topic admitted
Reductive Quotients of Parahoric Group Schemes Topic admitted
Regular Elements Definition admitted
Regular Representation as a Comodule Example admitted
Relative Root Datum of an F-Reductive Group Theorem admitted
Relative Weyl Group Is Generated by Relative Reflections Theorem admitted
Resolution of a Torus by Induced Tori Theorem admitted
Rigid Inner Forms Topic admitted
Rigid Inner Twists Topic admitted
Root Chains and the String Property Theorem admitted
Root Data Definition admitted
Root Datum of a Reductive Group Definition admitted
Root Form and Positive Definiteness Theorem admitted
Root Pairings (Unified Framework) Definition admitted
Root Subgroups Generate a Reductive Group Theorem admitted
Root Systems Definition admitted
Roots of Unity Group Scheme μ_n Definition admitted
Roots, Coroots, and Root Subgroups Topic admitted
SL2-Triples Topic admitted
Semisimple Conjugacy Classes Definition admitted
Semisimple Groups Topic admitted
Sigma-Conjugacy Classes Topic admitted
Smooth Affine Group Schemes over Valuation Rings Topic admitted
Smoothness, Tangent Spaces, and Lie Algebras Topic admitted
Solvable Groups Topic admitted
Spec Functor on Hopf Algebras Definition admitted
Spec Functor on Hopf Algebras Is Fully Faithful Theorem admitted
Special Linear Group Scheme SL_n Definition admitted
Special Orthogonal Group Scheme SO_n Definition admitted
Spherical Buildings Topic admitted
Split Reductive Groups Definition admitted
Split Torus Definition admitted
Split-Anisotropic Decomposition of a Torus Theorem admitted
Splittings over Integral and Parahoric Subgroups Topic admitted
Springer Correspondence Theorem admitted
Stable Conjugacy Classes Definition admitted
Standard Parabolics Are Classified by Simple Roots Theorem admitted
Strong Inner Forms Topic admitted
Strong Real Forms Topic admitted
Strongly Regular Elements and Harish-Chandra Theory Definition admitted
Structure of Connected Solvable Algebraic Groups Theorem admitted
Subtori and Quotients via the Character Lattice Theorem admitted
Symplectic Group Scheme Sp_{2n} Definition admitted
Tamely Ramified Torus Definition admitted
The Diagonalizable Group Scheme D(M) Definition admitted
The Minimal Splitting Field of a Torus Theorem admitted
The Twisted Form of a Galois Lattice Definition admitted
Tits Buildings Topic admitted
Tori Are Classified by Cocycles in GL_n(Z) Theorem admitted
Tori among Groups of Multiplicative Type Theorem admitted
Tori over Finite Fields Example admitted
Tori up to Isogeny Are Rational Representations Theorem admitted
Torsors Topic admitted
Trivial Group Scheme over a Base Definition admitted
Trivial Representation as a Comodule Example admitted
Twisted Conjugacy Classes Topic admitted
Unipotent Elements and the Unipotent Variety Definition admitted
Unipotent Groups Topic admitted
Unipotent Orbits Definition admitted
Unipotent Radical of a Borel Subgroup and Positive Roots Theorem admitted
Unipotent Subgroups Are Triangularizable Theorem admitted
Unramified Torus Definition admitted
Valued Root Data Topic admitted
Vogan Diagrams Topic admitted
Weakly Induced Torus Definition admitted
Weighted Dynkin Diagrams Topic admitted
Weil Restriction of Tori Theorem admitted
Weyl Group Is Generated by Root Reflections Theorem admitted
Weyl Groups Topic admitted
Weyl Groups as Coxeter Groups Theorem admitted

Algebraic Groups.Affine Group Schemes

Additive Group Scheme 𝔾_a Definition admitted
Affine Algebraic Groups Topic admitted
Affine Group Scheme over a Base Definition admitted
Algebra Homomorphisms Form a Group Under Convolution Theorem admitted
Algebraic Group over a Base Definition admitted
Antipode of a Commutative Hopf Algebra Is Multiplicative Theorem admitted
Antipode of a Hopf Algebra Is Anti-Multiplicative Theorem admitted
Base Change Topic admitted
Base Change Preserves Algebraic Group Structure Theorem admitted
Characters Are Group-Like Elements Theorem admitted
Comodule over a Coalgebra Definition admitted
Composition with the Antipode Is an Algebra Hom for Commutative Hopf Algebras Theorem admitted
Convolution Is Pointwise Multiplication Theorem admitted
Convolution of Algebra Homomorphisms Definition admitted
Convolution of Algebra Homomorphisms Is an Algebra Homomorphism Theorem admitted
Coordinate Hopf Algebra of an Affine Group Scheme Definition admitted
Coordinate Rings and Hopf Algebras Topic admitted
Essential Image of Spec Is Affine Group Schemes Theorem admitted
Faithful Linear Representation Definition admitted
Finite-Dimensional Subspace in a Sub-Comodule Lemma admitted
Functor of Points of a Group Scheme Definition admitted
G-Representations Are A-Comodules Theorem admitted
General Linear Group Scheme GL_n Definition admitted
Group Object Structure on Spec A via Yoneda Theorem admitted
Hom Into Spec via Global Sections (Spec ⊣ Γ Adjunction) Theorem admitted
Homomorphism of Affine Group Schemes Definition admitted
Multiplication of a Commutative Bialgebra Is a Coalgebra Hom Lemma admitted
Multiplicative Group Scheme 𝔾_m Definition admitted
Points of GL_n Are Invertible n×n Matrices over R Theorem admitted
Points of 𝔾_a Are the Additive Group of R Theorem admitted
Points of 𝔾_m Are the Units of R Theorem admitted
R-Points of a Group Scheme Form a Group Theorem admitted
Regular Representation as a Comodule Example admitted
Roots of Unity Group Scheme μ_n Definition admitted
Spec Functor on Hopf Algebras Definition admitted
Spec Functor on Hopf Algebras Is Fully Faithful Theorem admitted
Special Linear Group Scheme SL_n Definition admitted
Special Orthogonal Group Scheme SO_n Definition admitted
Symplectic Group Scheme Sp_{2n} Definition admitted
The Diagonalizable Group Scheme D(M) Definition admitted
Trivial Group Scheme over a Base Definition admitted
Trivial Representation as a Comodule Example admitted

Algebraic Groups.Buildings

Affine Root Systems Topic admitted
Affine Weyl Groups Topic admitted
BN-Pairs and Tits Systems Topic admitted
Bruhat-Tits Apartments Topic admitted
Bruhat-Tits Buildings Topic admitted
Coxeter Complexes Topic admitted
Facets in Bruhat-Tits Buildings Topic admitted
Moy-Prasad Filtrations Topic admitted
Parahoric Group Schemes Topic admitted
Parahoric Subgroups Topic admitted
Reductive Groups over Local Fields Topic admitted
Reductive Quotients of Parahoric Group Schemes Topic admitted
Smooth Affine Group Schemes over Valuation Rings Topic admitted
Spherical Buildings Topic admitted
Tits Buildings Topic admitted
Valued Root Data Topic admitted

Algebraic Groups.Classical And Exceptional Groups

Classical Groups Topic admitted
Exceptional Groups Topic admitted
Special Linear Group Scheme SL_n Definition admitted
Special Orthogonal Group Scheme SO_n Definition admitted
Symplectic Group Scheme Sp_{2n} Definition admitted

Algebraic Groups.Conjugacy Classes

Adjoint Action Topic admitted
Bala-Carter Classification Topic admitted
Conjugacy Classes in the Weyl Group Definition admitted
Geometric Conjugacy and Deligne–Lusztig Theory Definition admitted
Jacobson-Morozov Theorem Topic admitted
Jordan Decomposition in Algebraic Groups Theorem admitted
Lie Algebras of Reductive Groups Topic admitted
Nilpotent Cone Topic admitted
Nilpotent Elements Topic admitted
Nilpotent Orbits Topic admitted
Rational Nilpotent Orbits Topic admitted
Regular Elements Definition admitted
SL2-Triples Topic admitted
Semisimple Conjugacy Classes Definition admitted
Springer Correspondence Theorem admitted
Stable Conjugacy Classes Definition admitted
Strongly Regular Elements and Harish-Chandra Theory Definition admitted
Unipotent Elements and the Unipotent Variety Definition admitted
Unipotent Orbits Definition admitted
Weighted Dynkin Diagrams Topic admitted

Algebraic Groups.Covers

Brylinski-Deligne K2-Extensions Topic admitted
Central Extensions of Algebraic Groups Topic admitted
Dual Groups for Covers Topic admitted
L-Groups for Covers Topic admitted
Local and Global Metaplectic Covers Topic admitted
Splittings over Integral and Parahoric Subgroups Topic admitted

Algebraic Groups.Forms

Cocycles and Twisting Topic admitted
Extended Groups for Real Forms Topic admitted
F-Tori Are Classified by Galois Modules Theorem admitted
Field of Definition for Subgroups of F-Groups Theorem admitted
Fixed Point Theorem for F-Split Solvable Groups Theorem admitted
Forms of Algebraic Groups Topic admitted
Forms of Algebraic Objects Topic admitted
Galois Cohomology Topic admitted
Galois Descent for Hopf Algebras Theorem admitted
Galois Descent for Vector Spaces Theorem admitted
Galois Groups and Descent Data Topic admitted
Homomorphisms of Tori Correspond to Lattice Maps Theorem admitted
Indexed Root Datum of an F-Reductive Group Definition admitted
Inner Forms Topic admitted
Kaletha Refined Inner Forms Topic admitted
Lang Theorem for Connected Algebraic Groups over Finite Fields Theorem admitted
Levi Decomposition for Parabolic F-Subgroups Theorem admitted
Maximal F-Split Tori Are G(F)-Conjugate Theorem admitted
Maximal F-Tori Exist in Connected F-Groups Theorem admitted
Nonabelian H1 Topic admitted
Outer Forms Topic admitted
Pure Inner Twists Topic admitted
Quasi-Split Forms Topic admitted
Quasi-Split and Anisotropic Groups via the Indexed Root Datum Theorem admitted
Rational Forms of Linear Algebraic Groups Topic admitted
Rational Forms of Reductive Groups Topic admitted
Real Forms Topic admitted
Rigid Inner Forms Topic admitted
Rigid Inner Twists Topic admitted
Stable Conjugacy Classes Definition admitted
Strong Inner Forms Topic admitted
Strong Real Forms Topic admitted
The Twisted Form of a Galois Lattice Definition admitted
Tori Are Classified by Cocycles in GL_n(Z) Theorem admitted
Torsors Topic admitted
Twisted Conjugacy Classes Topic admitted
Vogan Diagrams Topic admitted

Algebraic Groups.Kottwitz

Admissible Sets Topic admitted
Algebraic Fundamental Group Topic admitted
B(G) Topic admitted
Basic Sigma-Conjugacy Classes Topic admitted
Isocrystals with G-Structure Topic admitted
Kottwitz Homomorphism Topic admitted
Kottwitz Map on B(G) Topic admitted
Newton Map Topic admitted
Sigma-Conjugacy Classes Topic admitted

Algebraic Groups.Linear Algebraic Groups

Affine Finite-Type Groups Have Faithful Finite-Dimensional Representations Theorem admitted
Affine G-Varieties Embed Equivariantly in Representations Theorem admitted
Algebraic Group Actions, Orbits, and Stabilizers Definition admitted
Algebraic Groups Are Closed Subgroups of GL_n Theorem admitted
Automorphism Groups Topic admitted
Basic Examples Topic admitted
Commutative Algebraic Groups Split into Semisimple and Unipotent Parts Theorem admitted
Conjugacy Classes Topic admitted
Connected Components Topic admitted
Connected Subgroups Generate a Closed Connected Subgroup Theorem admitted
Definition of Linear Algebraic Groups Definition needs_definition_review
Embedding Theorem for Algebraic Groups Theorem admitted
Field of Definition for Subgroups of F-Groups Theorem admitted
General Linear Group Scheme GL(V) Definition formalized
Identity Component Is Closed Normal of Finite Index Theorem admitted
Image of an Algebraic Group Homomorphism Is Closed Theorem admitted
Jordan Decomposition in a Linear Algebraic Group Theorem admitted
Kernels, Images, and Quotients Topic admitted
Lang Theorem for Connected Algebraic Groups over Finite Fields Theorem admitted
Lie Algebra of an Algebraic Group Definition admitted
Lie-Kolchin Theorem Theorem admitted
Linear Algebraic Groups Topic admitted
Morphisms and Closed Subgroups Topic admitted
Orbits of Algebraic Group Actions Are Locally Closed Theorem admitted
Quotient by a Closed Subgroup Exists Theorem admitted
Smoothness, Tangent Spaces, and Lie Algebras Topic admitted
Unipotent Subgroups Are Triangularizable Theorem admitted

Algebraic Groups.Reductive Groups

Borel Fixed Point Theorem Theorem admitted
Borel Subgroups Topic admitted
Borel Subgroups Are Conjugate and Control Parabolics Theorem admitted
Bruhat Decomposition Theorem admitted
Bruhat Order Gives Schubert Closure Relations Theorem admitted
Cartan Subgroups from Maximal Tori Theorem admitted
Central Isogenies Topic admitted
Characterization of Diagonalizable Groups Theorem admitted
Chevalley Existence Theorem Theorem admitted
Chevalley Group Construction from a Root Datum Definition admitted
Chevalley Isomorphism Theorem Theorem admitted
Chevalley Isomorphism Theorem for F-Split Groups Theorem admitted
Commutative Algebraic Groups Split into Semisimple and Unipotent Parts Theorem admitted
Derived Group, Center, Adjoint Group, and Simply Connected Cover Topic admitted
Diagonalizable Groups Topic admitted
Diagonalizable Groups Are Dual to Character Groups Theorem admitted
Fixed Point Theorem for F-Split Solvable Groups Theorem admitted
Indexed Root Datum of an F-Reductive Group Definition admitted
Isogeny Types from the Root Datum Definition admitted
Jordan Decomposition in Algebraic Groups Theorem admitted
Levi Decomposition for Parabolic F-Subgroups Theorem admitted
Levi Decomposition of Parabolic Subgroups Theorem admitted
Levi Subgroups and Unipotent Radicals Topic admitted
Lie-Kolchin Theorem Theorem admitted
Maximal F-Split Tori Are G(F)-Conjugate Theorem admitted
Maximal F-Tori Exist in Connected F-Groups Theorem admitted
Maximal Tori Topic admitted
Maximal Tori Are Conjugate Theorem admitted
Parabolic Subgroups Topic admitted
Quasi-Split and Anisotropic Groups via the Indexed Root Datum Theorem admitted
Radical and Derived Group of a Reductive Group Theorem admitted
Rank-One Subgroups and SL₂-Embeddings Definition admitted
Rational Bruhat Decomposition Theorem admitted
Reductive Groups Topic admitted
Relative Root Datum of an F-Reductive Group Theorem admitted
Relative Weyl Group Is Generated by Relative Reflections Theorem admitted
Root Datum of a Reductive Group Definition admitted
Root Subgroups Generate a Reductive Group Theorem admitted
Semisimple Conjugacy Classes Definition admitted
Semisimple Groups Topic admitted
Solvable Groups Topic admitted
Split Reductive Groups Definition admitted
Standard Parabolics Are Classified by Simple Roots Theorem admitted
Structure of Connected Solvable Algebraic Groups Theorem admitted
Unipotent Elements and the Unipotent Variety Definition admitted
Unipotent Groups Topic admitted
Unipotent Radical of a Borel Subgroup and Positive Roots Theorem admitted
Unipotent Subgroups Are Triangularizable Theorem admitted
Weyl Group Is Generated by Root Reflections Theorem admitted

Algebraic Groups.Root Data

Automorphisms of Root Data Topic admitted
Based Root Data Topic admitted
Bruhat Decomposition Theorem admitted
Bruhat Order Gives Schubert Closure Relations Theorem admitted
Cartan Matrices and Dynkin Diagrams Topic admitted
Centers and Dual Centers Topic admitted
Central Isogenies and Duality Topic admitted
Chevalley Basis Definition admitted
Chevalley Existence Theorem Theorem admitted
Chevalley Group Construction from a Root Datum Definition admitted
Chevalley Isomorphism Theorem Theorem admitted
Chevalley Isomorphism Theorem for F-Split Groups Theorem admitted
Classification of Irreducible Root Systems Theorem admitted
Classification of Split Reductive Groups Topic admitted
Coxeter Systems and Bruhat Order Topic admitted
Crystallographic and Reduced Root Systems Definition admitted
Diagonalizable Groups Are Dual to Character Groups Theorem admitted
Dual Reductive Groups Topic admitted
Dual Root Data Topic admitted
Dual Root Systems Topic admitted
Fundamental Group of a Root Datum Topic admitted
Galois Action on Root Data Topic admitted
Indexed Root Datum of an F-Reductive Group Definition admitted
Isogeny Types from the Root Datum Definition admitted
L-Groups Topic admitted
L-Morphisms Topic admitted
Langlands Dual Groups Topic admitted
Levi Decomposition of Parabolic Subgroups Theorem admitted
Pinned Dual Groups Topic admitted
Pinnings Topic admitted
Quasi-Split and Anisotropic Groups via the Indexed Root Datum Theorem admitted
Rank-One Subgroups and SL₂-Embeddings Definition admitted
Rational Bruhat Decomposition Theorem admitted
Relative Root Datum of an F-Reductive Group Theorem admitted
Relative Weyl Group Is Generated by Relative Reflections Theorem admitted
Root Chains and the String Property Theorem admitted
Root Data Definition admitted
Root Datum of a Reductive Group Definition admitted
Root Form and Positive Definiteness Theorem admitted
Root Pairings (Unified Framework) Definition admitted
Root Subgroups Generate a Reductive Group Theorem admitted
Root Systems Definition admitted
Roots, Coroots, and Root Subgroups Topic admitted
Split Reductive Groups Definition admitted
Standard Parabolics Are Classified by Simple Roots Theorem admitted
Unipotent Radical of a Borel Subgroup and Positive Roots Theorem admitted
Weyl Group Is Generated by Root Reflections Theorem admitted
Weyl Groups Topic admitted
Weyl Groups as Coxeter Groups Theorem admitted

Algebraic Groups.Tori

Algebraic Tori Topic admitted
Algebraic Torus Definition admitted
Anisotropic Torus Definition admitted
Character and Cocharacter Lattices Topic admitted
Characters Are Group-Like Elements Theorem admitted
Classification of Rank-One Tori Theorem admitted
Classification of Real Tori Example admitted
Convolution Is Pointwise Multiplication Theorem admitted
F-Tori Are Classified by Galois Modules Theorem admitted
Finiteness of Tori of Bounded Rank Theorem admitted
Galois Descent for Hopf Algebras Theorem admitted
Galois Descent for Vector Spaces Theorem admitted
Homomorphisms of Tori Correspond to Lattice Maps Theorem admitted
Induced Torus Definition admitted
Norm-One Torus of a Separable Extension Example admitted
Rank and Split Rank of a Torus Definition admitted
Resolution of a Torus by Induced Tori Theorem admitted
Split Torus Definition admitted
Split-Anisotropic Decomposition of a Torus Theorem admitted
Subtori and Quotients via the Character Lattice Theorem admitted
Tamely Ramified Torus Definition admitted
The Diagonalizable Group Scheme D(M) Definition admitted
The Minimal Splitting Field of a Torus Theorem admitted
The Twisted Form of a Galois Lattice Definition admitted
Tori Are Classified by Cocycles in GL_n(Z) Theorem admitted
Tori among Groups of Multiplicative Type Theorem admitted
Tori over Finite Fields Example admitted
Tori up to Isogeny Are Rational Representations Theorem admitted
Unramified Torus Definition admitted
Weakly Induced Torus Definition admitted
Weil Restriction of Tori Theorem admitted

Foundations

Affine Schemes Topic admitted
Algebraic K-Theory and K2 Topic admitted
Basic Combinatorics Topic admitted
Commutative Algebra Topic admitted
Fields and Field Extensions Topic admitted
Global Fields, Adeles, and Reciprocity Symbols Topic admitted
Hopf Algebras Topic admitted
Local Fields Topic admitted
Quantum Group (Formal-Deformation Convention) Definition admitted