Definitions/Def_ModularCurve_ComponentGroupOrder.lean

The ambient set-up is that of the character lattice of a graph of components: for a finite type \iota, X = characterLattice ι is the kernel of the degree map (D_x)_{x}\mapsto \sum_x D_x on \iota \to \mathbb{Z}, and for widths e : \iota \to \mathbb{N} the map gramMap e sends D \in X to the functional D' \mapsto \sum_x e(x)\,D_xD'_x on X, so its cokernel in \operatorname{Hom}_{\mathbb{Z}}(X,\mathbb{Z}) is the component group componentGroup e. Three items are introduced here. First, gramMatrixOf e v, for an arbitrary family v : \kappa \to X indexed by a finite type \kappa, is the \kappa \times \kappa integer matrix whose (i,j) entry is \sum_x e(x)\,(v_i)_x (v_j)_x, i.e. the value of the width pairing on v_i and v_j; the family is not required to be a basis, and a simp lemma records the entries. Second, under the hypothesis e(x) > 0 for all x, and given a \mathbb{Z}-basis c of X indexed by \kappa, gramRangeBasisOf is the basis of the submodule \operatorname{range}(\mathtt{gramMap } e) \subseteq \operatorname{Hom}_{\mathbb{Z}}(X,\mathbb{Z}) obtained by transporting c along the isomorphism of X onto the range induced by the injectivity of gramMap e (the cited theorem ModularCurve.gramMap_injective); its i-th vector is, as a functional on X, exactly \mathtt{gramMap } e\,(c_i). Third, toMatrix_dualBasis_gramRangeOf computes the coordinates of these vectors in the dual basis c^{\vee} of \operatorname{Hom}_{\mathbb{Z}}(X,\mathbb{Z}): the matrix c.dualBasis.toMatrix of the family i \mapsto \mathtt{gramMap } e\,(c_i) is the transpose of gramMatrixOf e c. Since the width pairing is symmetric, this matrix is the Gram matrix of c itself.