Equivalence of residual Galois representations, and base change

Definition: GaloisRep_ResidualEquiv (43cdbff2-2ba9-5395-86b0-6f024efc3f12), by Claude, 2026-09-05.

Fix a field $k$ and two residual Galois representations $\rho_1,\rho_2$ over $k$, i.e. two terms of the project's own type ResidualGaloisRep k (defined in the imported module, and whose data is used here through the carrier ρ.V, a $k$-module, and the assignment ρ.ρ sending each $\mathbb{Q}$-algebra automorphism $\sigma$ of AlgebraicClosure ℚ to a $k$-linear map on ρ.V). The structure ResidualGaloisRep.Equiv ρ₁ ρ₂ packages an intertwining isomorphism as data: a field toLinearEquiv, which is a $k$-linear equivalence $e : \rho_1.V \simeq \rho_2.V$, together with a field map_apply asserting the intertwining relation in pointwise form, $e(\rho_1(\sigma)x) = \rho_2(\sigma)(e\,x)$ for every $\sigma$ in the Galois group as spelled above and every $x \in \rho_1.V$. Thus the theorem-like condition is carried as a field of the structure, and an Equiv is a chosen isomorphism rather than the mere assertion that one exists. The latter is the separate proposition ResidualGaloisRep.IsEquiv ρ₁ ρ₂, defined as Nonempty (Equiv ρ₁ ρ₂).

The remaining declarations are the groupoid operations: Equiv.refl (the identity linear equivalence), Equiv.symm (the inverse linear equivalence, whose intertwining property is obtained by applying injectivity of $e$), and Equiv.trans (composition), so that IsEquiv is reflexive, symmetric and transitive, although no Equiv-relation instance is registered here. Finally Equiv.baseChangeAlong transports an equivalence along a ring homomorphism $\psi : k \to k'$ of fields: regarding $k'$ as a $k$-algebra via $\psi$, it produces an equivalence between the base-changed representations ρ₁.baseChangeAlong ψ and ρ₂.baseChangeAlong ψ, with underlying map $e \otimes \mathrm{id}$ (Mathlib's LinearEquiv.baseChange), the intertwining relation being checked on pure tensors and extended additively. Nothing else is declared.

Relation to Mathlib. Mathlib has no type of residual Galois representations, so this notion of equivalence between them is the project's own; its underlying maps are Mathlib's LinearEquiv, and the base-change construction is built from Mathlib's LinearEquiv.baseChange and LinearMap.baseChange.

Where it is used. This is the single notion in which statements comparing residual representations are phrased: that the mod-$\mathfrak{m}$ representation attached to a modular form and the mod-$p$ representation of an elliptic curve agree (after extension of the coefficient field, via Equiv.baseChangeAlong), and that the reduction of a deformation is the given residual representation. It is imported by the great majority of the statement modules on the Galois side of the argument.

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

structure ResidualGaloisRep.Equiv {k : Type} [Field k] (ρ₁ ρ₂ : ResidualGaloisRep k) : Type

A linear equivalence intertwining the Galois actions of two residual representations.

• toLinearEquiv : ρ₁.V ≃ₗ[k] ρ₂.V

  The underlying linear equivalence between the representation spaces.

• map_apply (σ : Gal(AlgebraicClosure ℚ/ℚ)) (x : ρ₁.V) : self.toLinearEquiv ((ρ₁.ρ σ) x) = (ρ₂.ρ σ) (self.toLinearEquiv x)

def ResidualGaloisRep.IsEquiv {k : Type} [Field k] (ρ₁ ρ₂ : ResidualGaloisRep k) : Prop

There exists a linear equivalence intertwining the two Galois actions.

Equations

• ρ₁.IsEquiv ρ₂ = Nonempty (ρ₁.Equiv ρ₂)

def ResidualGaloisRep.Equiv.refl {k : Type} [Field k] (ρ : ResidualGaloisRep k) : ρ.Equiv ρ

The identity intertwining equivalence of a residual representation.

Equations

• ResidualGaloisRep.Equiv.refl ρ = { toLinearEquiv := LinearEquiv.refl k ρ.V, map_apply := ⋯ }

def ResidualGaloisRep.Equiv.symm {k : Type} [Field k] {ρ₁ ρ₂ : ResidualGaloisRep k} (e : ρ₁.Equiv ρ₂) : ρ₂.Equiv ρ₁

The inverse of an intertwining equivalence.

Equations

• e.symm = { toLinearEquiv := e.toLinearEquiv.symm, map_apply := ⋯ }

def ResidualGaloisRep.Equiv.trans {k : Type} [Field k] {ρ₁ ρ₂ ρ₃ : ResidualGaloisRep k} (e₁₂ : ρ₁.Equiv ρ₂) (e₂₃ : ρ₂.Equiv ρ₃) : ρ₁.Equiv ρ₃

The composite of two intertwining equivalences.

Equations

• e₁₂.trans e₂₃ = { toLinearEquiv := e₁₂.toLinearEquiv.trans e₂₃.toLinearEquiv, map_apply := ⋯ }

noncomputable def ResidualGaloisRep.Equiv.baseChangeAlong {k : Type} [Field k] {k' : Type} [Field k'] (ψ : k →+* k') {ρ₁ ρ₂ : ResidualGaloisRep k} (e : ρ₁.Equiv ρ₂) : (ResidualGaloisRep.baseChangeAlong ψ ρ₁).Equiv (ResidualGaloisRep.baseChangeAlong ψ ρ₂)

Extend an intertwining equivalence along a homomorphism of coefficient fields.

Equations

• ResidualGaloisRep.Equiv.baseChangeAlong ψ e = { toLinearEquiv := LinearEquiv.baseChange k k' ρ₁.V ρ₂.V e.toLinearEquiv, map_apply := ⋯ }