Lean declarations

def Langlands.Tori.torusRank LanglandsLean @ main, LanglandsLean.AlgebraicGroups.Tori.Rank
```
noncomputable def torusRank : ℕ :=
  Module.finrank ℤ (CharLattice E (E ⊗[k] A))
```
def Langlands.Tori.torusSplitRank LanglandsLean @ main, LanglandsLean.AlgebraicGroups.Tori.Rank
```
noncomputable def torusSplitRank : ℕ :=
  Module.finrank ℤ (charRep k E A).invariants
```
theorem Langlands.Tori.torusSplitRank_le_torusRank LanglandsLean @ main, LanglandsLean.AlgebraicGroups.Tori.Rank
```
theorem torusSplitRank_le_torusRank [IsTorusAlgebra k E A] :
    torusSplitRank k E A ≤ torusRank k E A
```

theorem Langlands.Tori.torusSplitRank_eq_torusRank_iff LanglandsLean @ main, LanglandsLean.AlgebraicGroups.Tori.Rank sorry/admit

theorem torusSplitRank_eq_torusRank_iff
    [FiniteDimensional k E] [IsGalois k E] [IsTorusAlgebra k E A] :
    torusSplitRank k E A = torusRank k E A ↔ IsSplitTorusAlgebra k A

theorem Langlands.Tori.torusSplitRank_eq_zero_iff LanglandsLean @ main, LanglandsLean.AlgebraicGroups.Tori.Rank sorry/admit

theorem torusSplitRank_eq_zero_iff
    [FiniteDimensional k E] [IsGalois k E] [IsTorusAlgebra k E A] :
    torusSplitRank k E A = 0 ↔ IsAnisotropicAlgebra k E A

Modules: LanglandsLean.AlgebraicGroups.Tori.Rank

Rank and Split Rank of a Torus

Let \(T\) be a torus over \(k\), with character and cocharacter lattices \(X^*(T), X_*(T)\) and \(\Theta = \operatorname{Gal}(k_s/k)\) (Character and Cocharacter Lattices).

The rank of \(T\) is \[ \operatorname{rank} T \;:=\; \operatorname{rk}_{\mathbb{Z}} X^*(T) \;=\; \operatorname{rk}_{\mathbb{Z}} X_*(T), \] the \(n\) with \(T_{k_s} \cong \mathbb{G}_m^{\,n}\) (Algebraic Torus).
The split rank (or \(k\)-rank) of \(T\) is the rank of the maximal split subtorus \(T_d \subseteq T\) (Split-Anisotropic Decomposition of a Torus): \[ \operatorname{rank}_k T \;:=\; \operatorname{rank} T_d \;=\; \operatorname{rk}_{\mathbb{Z}} X_*(T)^{\Theta}. \] The second equality holds because cocharacters of \(T\) defined over \(k\) are exactly the \(\Theta\)-fixed cocharacters, and they all land in \(T_d\).
Equivalently on the character side: \[ \operatorname{rank}_k T \;=\; \operatorname{rk}_{\mathbb{Z}} X^*(T)^{\Theta}. \] Why the two invariant ranks agree. \(\Theta\) acts through a finite quotient \(Q\). Over \(\mathbb{Q}\), the perfect \(\Theta\)-invariant pairing \(X^*(T)_{\mathbb{Q}} \times X_*(T)_{\mathbb{Q}} \to \mathbb{Q}\) identifies \(X_*(T)_{\mathbb{Q}}\) with the dual representation of \(X^*(T)_{\mathbb{Q}}\), and for a finite group the invariants of a representation and of its dual have the same dimension (both equal the multiplicity of the trivial representation, by averaging / Maschke). Intersecting with the lattices does not change the rank of the invariants.

Basic facts

\(0 \leq \operatorname{rank}_k T \leq \operatorname{rank} T\).
\(\operatorname{rank}_k T = \operatorname{rank} T\) iff \(T\) is split (trivial action on a finite-index sublattice of \(X^*\) forces trivial action, since the action is by finite-order automorphisms of the lattice).
\(\operatorname{rank}_k T = 0\) iff \(T\) is anisotropic (Anisotropic Torus).
\(\operatorname{rank}_k T = \operatorname{rank} T_d\) and \(\operatorname{rank} T = \operatorname{rank}_k T + \operatorname{rank} T_a\) minus the rank of the finite intersection's contribution — precisely: the isogeny \(T_d \times T_a \to T\) of Split-Anisotropic Decomposition of a Torus gives \(\operatorname{rank} T = \operatorname{rank}_k T + \operatorname{rank} T_a\).

Downstream. The split rank of a maximal torus is the dimension of the corresponding apartment in the Bruhat–Tits building; the split rank of the connected center measures the non-compactness of the group of rational points.