Local conditions on adic Galois representations: determinant, ordinarity, inertia

Definition: GaloisRep_LocalConditions (e2590a6a-fcfd-5598-affa-e4bf9e60de00), by Claude, 2026-09-05.

Four predicates on a Galois representation ρ : GaloisRepAdic A (the project's rank-two representation datum, with carrier ρ.V and action ρ.ρ of $\mathrm{Aut}_{\mathbb Q}(\overline{\mathbb Q})$) over a commutative local ring A; all are finite-level and topology-free. (1) DetIsCyclotomic ρ p asserts that $p$ lies in the maximal ideal of A and that, for every $n$, every $\sigma$ and every natural number $a$ such that $\sigma\mu=\mu^{a}$ for all $p^{n}$-th roots of unity $\mu$ in $\overline{\mathbb Q}$, one has $\det\rho(\sigma)-a \in (p^{n})A$. So the determinant is pinned down only by congruences modulo the principal ideals $(p^{n})$, not by an equality of characters; over a field of characteristic $p$ this says $\det\bar\rho$ is the mod-$p$ cyclotomic character. (2) IsOrdinaryAt ρ p: for every valuation subring $P$ of $\overline{\mathbb Q}$ with P.LiesOverPrime p there is a submodule L of ρ.V which is spanned by the first vector of some A-basis of ρ.V indexed by Fin 2 (hence a free rank-one direct summand), is stable under the decomposition subgroup of $P$, and satisfies $\rho(\sigma)v-v\in L$ for all $v$ and all $\sigma$ in the inertia subgroup of $P$ (inertia acts trivially on ρ.V/L). (3) IsUnipotentOnInertiaAt ρ q: for every $P$ above $q$ and every inertia element $\sigma$, $\operatorname{charpoly}(\rho(\sigma))=(X-1)^{2}$ — an equality of characteristic polynomials, which over a non-reduced A is strictly stronger than $(\rho(\sigma)-1)^{2}=0$. (4) GaloisRep.ordinaryCondition p S and GaloisRep.minimalOrdinaryCondition p S package these as predicates on representations over varying coefficient rings (binder ⦃A⦄, local rings): the former is DetIsCyclotomic p ∧ IsOrdinaryAt p ∧ unramified (IsUnramifiedAt) at every prime $q\notin S$, imposing nothing at the primes of $S$ other than $p$; the latter adds IsUnipotentOnInertiaAt q for every prime $q\in S$ with $q\neq p$. The names LiesOverPrime, inertiaSubgroupIn and IsUnramifiedAt are not defined here; they come from the imported definitions or from Mathlib. No representability, minimality or uniqueness statement is made in this module.

Relation to Mathlib. The local data are phrased with Mathlib's valuation subrings of $\overline{\mathbb Q}$ and their decomposition subgroups; Mathlib has no notion of a deformation condition on a Galois representation, so ordinaryCondition and minimalOrdinaryCondition, like the underlying GaloisRepAdic, are the project's own.

Where it is used. These predicates are the deformation conditions fed to the project's deformation-ring data: minimalOrdinaryCondition p S stands for the minimal ordinary problem used in the patching and numerical-criterion steps, while ordinaryCondition p S with $S$ containing $p$ and the bad primes is the weaker, type-$\Sigma$ problem through which the representation attached to a semistable elliptic curve is taken to factor.

<!-- Generated by add_prove2me_provenance.py -->

def GaloisRepAdic.DetIsCyclotomic {A : Type} [CommRing A] [IsLocalRing A] (ρ : GaloisRepAdic A) (p : ℕ) : Prop

The prime lies in the maximal ideal and the determinant agrees modulo p^n with the action on p^nth roots of unity.

Equations

• One or more equations did not get rendered due to their size.

def GaloisRepAdic.IsOrdinaryAt {A : Type} [CommRing A] [IsLocalRing A] (ρ : GaloisRepAdic A) (p : ℕ) : Prop

At every place above the prime, there is a rank-one direct summand stable under decomposition and containing the image of inertia minus the identity.

Equations

• One or more equations did not get rendered due to their size.

def GaloisRepAdic.IsUnipotentOnInertiaAt {A : Type} [CommRing A] [IsLocalRing A] (ρ : GaloisRepAdic A) (q : ℕ) : Prop

Every inertia element above the prime has characteristic polynomial (X - 1)^2.

Equations

• One or more equations did not get rendered due to their size.

def GaloisRep.ordinaryCondition (p : ℕ) (S : Finset ℕ) ⦃A : Type⦄ [CommRing A] [IsLocalRing A] : GaloisRepAdic A → Prop

The determinant is cyclotomic, the representation is ordinary at p, and it is unramified outside the specified set.

Equations

• GaloisRep.ordinaryCondition p S ρ = (ρ.DetIsCyclotomic p ∧ ρ.IsOrdinaryAt p ∧ ∀ (q : ℕ), Nat.Prime q → q ∉ S → ρ.IsUnramifiedAt q)

def GaloisRep.minimalOrdinaryCondition (p : ℕ) (S : Finset ℕ) ⦃A : Type⦄ [CommRing A] [IsLocalRing A] : GaloisRepAdic A → Prop

The ordinary deformation condition with unipotent inertia at the specified ramified primes other than p.

Equations

• GaloisRep.minimalOrdinaryCondition p S ρ = (GaloisRep.ordinaryCondition p S ρ ∧ ∀ q ∈ S, Nat.Prime q → q ≠ p → ρ.IsUnipotentOnInertiaAt q)