Definitions/Def_RibetLevelLowering_ExchangeData.lean

The module defines, over a field k, a structure ExchangeData k packaging the numerical data of the exchange case of Ribet's level-lowering argument as a bundle of abstract finite-dimensional k-vector spaces. A term of ExchangeData k carries five types Xp, Yq, Lp, Yp, Lq, each equipped with an additive commutative group structure, a k-module structure and the assumption of being a finite k-module (these instance fields are registered as instances), together with two k-linear maps f : \mathrm{Yq} \to \mathrm{Lp} and g : \mathrm{Lp} \to \mathrm{Xp}, a proof that g is surjective, and a proof of the inclusion \ker g \le \operatorname{range} f — that is, right exactness of \mathrm{Yq} \to \mathrm{Lp} \to \mathrm{Xp} \to 0 recorded as an inclusion of submodules rather than an equality. Finally it carries two natural numbers lam and mu and five numerical constraints on dimensions, \operatorname{finrank}_k \mathrm{Yp} = 2\mu, \operatorname{finrank}_k \mathrm{Lp} = 2\lambda, \operatorname{finrank}_k \mathrm{Yq} \le \mu, \operatorname{finrank}_k \mathrm{Lq} \le \lambda, \operatorname{finrank}_k \mathrm{Xp} \le \mu, and the positivity 0 < \lambda. Thus the whole structure is a theorem-free data package: the geometric provenance of the five spaces (character groups of toric parts and Brandt-module analogues, reduced modulo a maximal ideal of a Hecke algebra) and of the maps is not part of the Lean type, which refers only to k.

The second declaration is the predicate SeqIso on ExchangeData k, defined to hold exactly when \operatorname{finrank}_k \mathrm{Yp} = \operatorname{finrank}_k \mathrm{Lq}. It is therefore an equality of dimensions, not the datum of a linear isomorphism between the two spaces.