Definitions/Def_ModularCurve_DeligneRapoport.lean

Fix a group G, a commutative ring R, and an R-module J carrying a distributive multiplicative G-action; all five declarations are predicates on a chosen R-submodule \mathcal{T} \subseteq J (and, in two cases, on a subgroup I \le G or on a distinguished element of G). ToricStable G 𝒯 says that g \cdot x \in \mathcal{T} for every g \in G and every x \in \mathcal{T}, i.e. \mathcal{T} is a G-stable submodule. ToricInertiaFixed I 𝒯 says that every \sigma \in I acts as the identity on \mathcal{T}: \sigma \cdot x = x for all x \in \mathcal{T}. InertiaUnipotentTowards I 𝒯 says that (\sigma - 1)J \subseteq \mathcal{T}, spelled out as \sigma \cdot x - x \in \mathcal{T} for all \sigma \in I and all x \in J (note the quantifier is over all of J, not only over \mathcal{T}). IsInertiaFiltration I 𝒯 is the conjunction of four clauses: \mathcal{T} \neq \top (properness: \mathcal{T} is not all of J), ToricStable G 𝒯, ToricInertiaFixed I 𝒯 and InertiaUnipotentTowards I 𝒯. Together the last two clauses say exactly that I acts unipotently of level two through \mathcal{T}, i.e. (\sigma-1)(\tau-1) = 0 on J for \sigma, \tau \in I. Finally, ToricFrobeniusSq q φ 𝒯, for q : \mathbb{N} and \varphi \in G, asserts that \varphi acts on \mathcal{T} with square the scalar q^2: \varphi \cdot (\varphi \cdot x) = (q^2 : \mathbb{Z}) \cdot x for all x \in \mathcal{T}; it does not assert that \varphi itself acts by \pm q. No geometry is present here: nothing ties J to a Jacobian, G to a decomposition group, or \mathcal{T} to a toric part; the names record the intended instantiation only, and these predicates are hypotheses to be supplied by the consumer.