OddAbsIrred.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

1 declarations, 0 contain sorry, 0 declared as axioms

Irreducible ↔ absolutely irreducible, given a one-dimensional fixed space

Let ρ be a finite-dimensional representation of a monoid G over a field k, and suppose that some g : G has a one-dimensional fixed subspace V^g = {v | ρ g v = v}, i.e. that the eigenspace of ρ g for the eigenvalue 1 is one-dimensional. The main result of this file, OddRep.isIrreducible_iff_isAbsolutelyIrreducible, asserts that ρ is irreducible if and only if it is absolutely irreducible, that is, irreducible after base change to an algebraic closure of k (OddRep.IsAbsolutelyIrreducible).

A typical application is to an odd two-dimensional Galois representation in characteristic ≠ 2, where complex conjugation has eigenvalues 1 and -1 and hence a one-dimensional fixed space.

The definitions OddRep.baseChange and OddRep.IsAbsolutelyIrreducible, together with the proof and all supporting lemmas, are in FLT.Slop.RepresentationTheory.OddAbsIrredSlop.

Imports (1)

FLT.Slop.RepresentationTheory.OddAbsIrredSlop

Imported by 1 file

FLT.lean

theorem OddRep.isIrreducible_iff_isAbsolutelyIrreducible Proposition 1.2 / Theorem 1.3 line 45 source
Source documentation
Proposition 1.2 / Theorem 1.3. Let V be a finite-dimensional vector space over k and ρ : G →* GL(V) a representation. If some g : G has a one-dimensional fixed subspace V^g, then V is irreducible if and only if it is absolutely irreducible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, FiniteDimensional, Eq, Nat, Module.finrank, Subtype, Membership.mem, Submodule, Module.End.eigenspace, LinearMap, RingHom.id, OfNat.ofNat, Iff, Representation.IsIrreducible, Slop.OddRep.IsAbsolutelyIrreducible
Proof uses: Slop.OddRep.isIrreducible_iff_isAbsolutelyIrreducible_slop
50 instances, coercions and auxiliary constants left out.
```
theorem isIrreducible_iff_isAbsolutelyIrreducible
    (ρ : Representation k G V) [FiniteDimensional k V]
    {g : G} (hg : finrank k (Module.End.eigenspace (ρ g) 1) = 1) :
    ρ.IsIrreducible ↔ Slop.OddRep.IsAbsolutelyIrreducible ρ :=
…
```
Mentions: Slop.OddRep.IsAbsolutelyIrreducible