DVRClosureGL2 axioms: the structural closure properties of a DVR context needed to
prove the Iwahori decomposition for $GL_2$. Beyond the basic DVRClosure, we require: units
are nonzero, the maximal ideal absorbs products with elements of $\mathfrak{o}$, units are
closed under inversion, and a unit minus a maximal-ideal element is still a unit.
- isInO_zero : C.isInO 0
- isInMaxIdeal_mul_isInO {x y : C.k} : C.isInMaxIdeal x → C.isInO y → C.isInMaxIdeal (x * y)
- isUnitInO_sub_isInMaxIdeal {x y : C.k} : C.isUnitInO x → C.isInMaxIdeal y → C.isUnitInO (x - y)
Instances
Construct an invertible $2\times 2$ matrix from a function: given a $2\times 2$ matrix
$f$ over the fraction field $k$ with nonzero determinant, produce the corresponding element
of $GL_2(k)$. The construction uses unitOfDetInvertible together with invertibleOfNonzero
to convert nonvanishing of the determinant into invertibility data.
Instances For
Entries of mkGL2 are the original entries: the matrix underlying the unit produced by
mkGL2 f hdet has the same entries as $f$.
The Iwahori subgroup of $GL_2$: elements of $GL_2(k)$ whose diagonal entries are units in $\mathfrak{o}$, whose upper-right entry lies in $\mathfrak{o}$, and whose lower-left entry lies in the maximal ideal $\mathfrak{m}$.
Instances For
Upper unipotent subgroup of $GL_2$: invertible matrices of the form $\begin{pmatrix} 1 & * \\ 0 & 1 \end{pmatrix}$.
Instances For
Lower unipotent subgroup of $GL_2$: invertible matrices of the form $\begin{pmatrix} 1 & 0 \\ * & 1 \end{pmatrix}$.
Instances For
Diagonal subgroup of $GL_2$: invertible matrices of the form $\begin{pmatrix} * & 0 \\ 0 & * \end{pmatrix}$.
Instances For
Generic-indexed formulation of the Iwahori subgroup: an element $g \in GL_2(k)$ belongs to the Iwahori subgroup iff its diagonal entries are units, its strictly-upper-triangular entries lie in $\mathfrak{o}$, and its strictly-lower-triangular entries lie in $\mathfrak{m}$. This form quantifies over indices and is convenient for later generalisations.
Instances For
Generic-indexed formulation of the lower unipotent subgroup: an element $g \in GL_2(k)$ is lower unipotent iff its diagonal entries are $1$ and its strictly-upper-triangular entries vanish.
Instances For
Generic-indexed formulation of the upper unipotent subgroup: an element $g \in GL_2(k)$ is upper unipotent iff its diagonal entries are $1$ and its strictly-lower-triangular entries vanish.
Instances For
Generic-indexed formulation of the diagonal subgroup: an element $g \in GL_2(k)$ is diagonal iff all its off-diagonal entries vanish.
Instances For
Generic and concrete Iwahori formulations agree: the index-quantified definition
IwahoriGL2Gen describes the same set as the explicit four-entry condition IwahoriGL2.
Generic and concrete lower-unipotent formulations agree: the index-quantified definition
LowerUnipGL2Gen describes the same set as the explicit three-entry condition
LowerUnipGL2.
Generic and concrete upper-unipotent formulations agree: the index-quantified definition
UpperUnipGL2Gen describes the same set as the explicit three-entry condition
UpperUnipGL2.
Generic and concrete diagonal formulations agree: the index-quantified definition
DiagGL2Gen describes the same set as the explicit two-entry condition DiagGL2.
$1$ is a unit in $\mathfrak{o}$: the multiplicative identity of $k$ comes from the unit $1$ in the local ring $\mathfrak{o}$.
$0$ lies in the maximal ideal: the zero of $k$ comes from $0 \in \mathfrak{m}$.
Entry formula for a unipotent--diagonal--unipotent product: when the middle factor $m$ is diagonal, the $(i,j)$ entry of the triple product $u' \cdot m \cdot u$ simplifies to $u'_{i0} m_{00} u_{0j} + u'_{i1} m_{11} u_{1j}$. This identity is the computational core of the explicit Iwahori decomposition for $GL_2$.
Existence of the Iwahori decomposition for $GL_2$: every Iwahori element $b$ factors as a product $b = u' \cdot m \cdot u$ where $u'$ is lower unipotent (inside the Iwahori), $m$ is diagonal (inside the Iwahori), and $u$ is upper unipotent (inside the Iwahori). Explicitly, $u' = \begin{pmatrix} 1 & 0 \\ c a^{-1} & 1 \end{pmatrix}$, $m = \mathrm{diag}(a, d - c a^{-1} \beta)$, and $u = \begin{pmatrix} 1 & a^{-1}\beta \\ 0 & 1 \end{pmatrix}$, where $a, \beta, c, d$ are the entries of $b$.
Uniqueness of the Iwahori decomposition for $GL_2$: any two factorisations $b = u'_i m_i u_i$ ($i = 1, 2$) of the same Iwahori element into lower-unipotent times diagonal times
upper-unipotent factors must coincide. The proof reads off the diagonal and off-diagonal
entries of $u'\,m\,u$ via gl2_triple_product_entry.
Iwahori decomposition for $GL_2$ (generic form): every element of the Iwahori subgroup $I$ of $GL_2$ factors uniquely as $b = u' \cdot m \cdot u$ with $u' \in U^- \cap I$, $m \in T \cap I$, and $u \in U^+ \cap I$, where $U^\pm$ are the (lower/upper) unipotent subgroups and $T$ is the diagonal torus. This is the abstract statement using the index-quantified group definitions.
Iwahori decomposition for $GL_2$ (concrete form): the same unique factorisation
$b = u' \cdot m \cdot u$ as IwahoriDecomposition, phrased using the explicit four-entry
membership conditions rather than the index-quantified ones.