Definitions/Def_ModularCurve_FullLevelSemistableCoveringInertiaIgusa.lean

Fix a prime q, an integer M' \neq 0, a valuation subring A of \overline{\mathbb{Q}} and a finite set W of places of the modular function field \mathrm{modularFunctionFieldC} over the residue field of A. For a semistable covering \mathcal{C} of type SemistableCovering q M' A W — whose data include, for each point \ell of \mathbb{P}^1(\mathbb{F}_q), an Igusa component chart \mathcal{C}.\mathrm{CIg}\,\ell on the field fieldBar q M' with residue field \mathcal{C}.\mathrm{FIg}\,\ell over \mathrm{ResidueField}\,A, consisting of a valuation subring integers with surjective residue map, a set dom of places of fieldBar q M' and a reduction map placeMap on those places — this module defines the predicate InertiaIgusaInftyClause on \mathcal{C}.

The predicate quantifies over all \tau in A.inertiaSubgroupIn ℚ, the inertia subgroup of A inside \mathrm{Aut}_{\mathbb{Q}}(\overline{\mathbb{Q}}), with no restriction on the tame character of \tau, and lets g be the semilinear automorphism ModularCurve.arithmeticGalois (xHFunctionField (q ^ 2 * M') (levelH q M')) τ, which acts on fieldBar q M' coefficientwise through \tau. For the chart at the point lineInfty q = [1:0] of \mathbb{P}^1(\mathbb{F}_q) it asserts four things: the valuation subring integers of that chart is g-stable, in the sense that f lies in it if and only if g \cdot f does; a place P lies in dom if and only if g \cdot P does; InducesOnChart (𝒞.CIg (lineInfty q)) g (RingEquiv.refl _) holds, i.e. the stability of integers is witnessed and the induced automorphism of \mathcal{C}.\mathrm{FIg}(\infty) is the identity, so residues are unchanged, \overline{g \cdot f} = \overline{f}; and the reduction map is g-invariant on its domain, \mathrm{placeMap}(g \cdot P) = \mathrm{placeMap}(P) for P \in \mathrm{dom}. The first clause duplicates the stability witness contained in InducesOnChart.

This is the analogue, for all of inertia and for the single Igusa chart at \infty with trivial induced map on the residue field, of the inertia clause in the naturality package (which allows a nontrivial induced automorphism and concerns the supersingular charts) and of InertiaClause (which treats all Igusa charts but only inertia elements of tame character 1).