OddAbsIrredSlop.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

12 declarations, 0 contain sorry, 0 declared as axioms

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

This file proves Proposition 1.2 / Theorem 1.3 of the blueprint "Odd_Rep_Irreducible": if ρ is a finite-dimensional representation of a monoid G over a field k and some g : G has a one-dimensional fixed subspace, then ρ is irreducible if and only if it is absolutely irreducible. The public-facing statement, OddRep.isIrreducible_iff_isAbsolutelyIrreducible, is in FLT.RepresentationTheory.OddAbsIrred and is proved by appeal to OddRep.isIrreducible_iff_isAbsolutelyIrreducible_slop from this file.

Main results

OddRep.smul_tmul_mem_range_iff: Fact 1.1 (l·e ∩ V = k·e inside V_l)
OddRep.exists_smul_eq_of_commute: Lemma 1.4 (End_G(V) = k)
OddRep.adjoinRange_eq_top: Lemma 1.5 (Jacobson density, A = End_k(V))
OddRep.adjoinRange_baseChange_eq_top: Lemma 1.6 (base change of A = End_k(V))
OddRep.isIrreducible_of_adjoinRange_eq_top: step (iv) of the blueprint
OddRep.isIrreducible_of_baseChange: descent of irreducibility (easy direction)
OddRep.isIrreducible_baseChange_of_finrank_eigenspace_eq_one: the hard direction, over an arbitrary field extension l/k
OddRep.isIrreducible_iff_isAbsolutelyIrreducible_slop: Proposition 1.2 / Theorem 1.3

Implementation notes

Representations are Representation k G V := G →* (V →ₗ[k] V) as in Mathlib.
Irreducibility is Mathlib's Representation.IsIrreducible, defined as IsSimpleOrder (Subrepresentation ρ). The notion of a "G-invariant subspace" is Mathlib's Subrepresentation structure: a Submodule together with the invariance field apply_mem_toSubmodule : ρ g v ∈ toSubmodule for v ∈ toSubmodule. The lemma OddRep.isIrreducible_iff_forall unpacks Representation.IsIrreducible into the elementary statement "V ≠ 0 and every invariant subspace is ⊥ or ⊤", which is what most proofs below use.
"Absolutely irreducible" (OddRep.IsAbsolutelyIrreducible) is defined here as: the base change to AlgebraicClosure k is irreducible. The blueprint's proof in fact shows irreducibility after base change to any field extension l/k; this is recorded separately as OddRep.isIrreducible_baseChange_of_finrank_eigenspace_eq_one.

Imports (11)

Imported by 3 files

def Slop.OddRep.baseChange Base change of a representation along a field extension l/k: G acts on l ⊗[k] V by 1 ⊗ ρ(g) line 78 source
Source documentation
Base change of a representation along a field extension l/k: G acts on l ⊗[k] V by 1 ⊗ ρ(g).

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Algebra, Representation, TensorProduct
Proof uses: MonoidHom.mk, LinearMap, RingHom.id, OneHom.mk, LinearMap.baseChange
31 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
noncomputable def baseChange (l : Type*) [Field l] [Algebra k l]
    (ρ : Representation k G V) : Representation l G (l ⊗[k] V) where
…
```
def Slop.OddRep.adjoinRange The k-subalgebra A ⊆ End_k(V) generated by the image of ρ line 93 source
Source documentation
The k-subalgebra A ⊆ End_k(V) generated by the image of ρ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Subalgebra, Module.End
Proof uses: Algebra.adjoin, Set.range, LinearMap, RingHom.id
36 instances, coercions and auxiliary constants left out.
```
def adjoinRange (ρ : Representation k G V) : Subalgebra k (Module.End k V) :=
…
```
def Slop.OddRep.IsAbsolutelyIrreducible A representation is absolutely irreducible if it remains irreducible after base change to an algebraic closure of k line 98 source
Source documentation
A representation is absolutely irreducible if it remains irreducible after base change to an algebraic closure of k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation
Proof uses: Representation.IsIrreducible, AlgebraicClosure, TensorProduct, Slop.OddRep.baseChange
20 instances, coercions and auxiliary constants left out.
```
def IsAbsolutelyIrreducible (ρ : Representation k G V) : Prop :=
…
```
lemma Slop.OddRep.isIrreducible_iff_forall line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Iff, Representation.IsIrreducible, And, Nontrivial, Submodule, Membership.mem, LinearMap, RingHom.id, Or, Eq, Bot.bot, Top.top
Proof uses: Iff.intro, And.intro, Iff.mp, Submodule.nontrivial_iff, nontrivial_of_ne, IsSimpleOrder.bot_ne_top, Subrepresentation, Subrepresentation.toSubmodule_injective, Subrepresentation.toSubmodule, Subrepresentation.mk, IsSimpleOrder.eq_bot_or_eq_top, Or.inl, congrArg, Or.inr, Iff.mpr, Nontrivial.mk, Exists.intro, Exists, Ne, bot_ne_top and 2 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
lemma Slop.OddRep.smul_tmul_mem_range_iff Fact 1.1 line 148 source
Source documentation
Fact 1.1. If e ≠ 0 in V, then for c : l, the element c ⊗ e of l ⊗[k] V lies in the image of the canonical map V → l ⊗[k] V, v ↦ 1 ⊗ v, if and only if c comes from k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, AddCommGroup, Module, Algebra, Ne, OfNat.ofNat, Iff, Membership.mem, TensorProduct, Submodule, LinearMap.range, RingHom.id, LinearMap, TensorProduct.mk, TensorProduct.tmul, Exists, Eq, RingHom, Algebra.algebraMap
Proof uses: Iff.intro, Module.Dual, Module.Projective.exists_dual_eq_one, LinearMap.comp, TensorProduct.rid, LinearMap.lTensor, rfl, Exists.intro, congrArg, Eq.mpr, HSMul.hSMul, id, Algebra.algebraMap_eq_smul_one, Eq.mp, one_smul, congr, congrFun', TensorProduct.mk_apply, TensorProduct.tmul_smul, TensorProduct.smul_tmul' and 1 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma smul_tmul_mem_range_iff (l : Type*) [Field l] [Algebra k l]
    {e : V} (he : e ≠ 0) (c : l) :
    c ⊗ₜ[k] e ∈ LinearMap.range (TensorProduct.mk k l V 1) ↔
      ∃ a : k, algebraMap k l a = c := by
…
```
lemma Slop.OddRep.exists_smul_eq_of_commute Lemma 1.4 line 179 source
Source documentation
Lemma 1.4. If ρ is irreducible and some g : G has a one-dimensional fixed subspace (the eigenspace of ρ g for the eigenvalue 1), then every G-equivariant endomorphism of V is scalar.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Representation.IsIrreducible, Eq, Nat, Module.finrank, Subtype, Membership.mem, Submodule, Module.End.eigenspace, LinearMap, RingHom.id, OfNat.ofNat, Module.End, Commute, Exists, HSMul.hSMul
Proof uses: Nontrivial, Or, Bot.bot, Top.top, And, Iff.mp, Slop.OddRep.isIrreducible_iff_forall, Iff, Eq.mpr, id, congrArg, propext, Module.End.mem_eigenspace_iff, one_smul, Iff.rfl, HMul.hMul, LinearMap.congr_fun, Eq.mp, Eq.refl, Ne and 18 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma exists_smul_eq_of_commute
    (hirr : ρ.IsIrreducible)
    {g : G} (hg : finrank k (Module.End.eigenspace (ρ g) 1) = 1)
    (T : Module.End k V) (hT : ∀ h : G, Commute (ρ h) T) :
    ∃ μ : k, T = μ • (1 : Module.End k V) := by
…
```
lemma Slop.OddRep.adjoinRange_eq_top Lemma 1.5 line 240 source
Source documentation
Lemma 1.5. Let A ⊆ End_k(V) be the k-algebra generated by ρ(G). If V is finite-dimensional, ρ is irreducible, and every G-equivariant endomorphism of V is scalar, then A = End_k(V).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, FiniteDimensional, Representation.IsIrreducible, Module.End, Commute, LinearMap, RingHom.id, Exists, Eq, HSMul.hSMul, OfNat.ofNat, Subalgebra, Slop.OddRep.adjoinRange, Top.top
Proof uses: Nontrivial, Submodule, Membership.mem, Or, Bot.bot, And, Iff.mp, Slop.OddRep.isIrreducible_iff_forall, Eq.mpr, id, congrArg, rfl, Algebra.subset_adjoin, Set.range, Exists.intro, IsScalarTower, Subtype, IsScalarTower.mk, IsSimpleModule, Iff.mpr and 35 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma adjoinRange_eq_top [FiniteDimensional k V]
    (hirr : ρ.IsIrreducible)
    (hEnd : ∀ T : Module.End k V, (∀ h : G, Commute (ρ h) T) →
      ∃ μ : k, T = μ • (1 : Module.End k V)) :
    adjoinRange ρ = ⊤ := by
…
```
Mentions: Slop.OddRep.adjoinRange
lemma Slop.OddRep.adjoinRange_baseChange_eq_top Lemma 1.6 line 296 source
Source documentation
Lemma 1.6. If the k-algebra generated by ρ(G) is all of End_k(V), then after base change along any field extension l/k, the l-algebra generated by (ρ.baseChange l)(G) is all of End_l(l ⊗[k] V).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, FiniteDimensional, Algebra, Eq, Subalgebra, Module.End, Slop.OddRep.adjoinRange, Top.top, TensorProduct, Slop.OddRep.baseChange
Proof uses: AlgHom, Module.End.baseChangeHom, rfl, LinearMap.baseChange, LinearMap, RingHom.id, Eq.mpr, id, congrArg, Eq.refl, Membership.mem, LE.le, Subalgebra.map, Subalgebra.restrictScalars, Algebra.adjoin, Set.range, Slop.OddRep.adjoinRange.eq_1, Set.image, Eq.symm, Algebra.adjoin_image and 31 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma adjoinRange_baseChange_eq_top [FiniteDimensional k V]
    (l : Type*) [Field l] [Algebra k l]
    (h : adjoinRange ρ = ⊤) :
    adjoinRange (baseChange l ρ) = ⊤ := by
…
```
Mentions: Slop.OddRep.adjoinRange, Slop.OddRep.baseChange
lemma Slop.OddRep.isIrreducible_of_adjoinRange_eq_top Documented declaration: isIrreducible_of_adjoinRange_eq_top line 349 source
Source documentation
If the algebra generated by ρ(G) is all of End_k(V) (and V ≠ 0), then ρ is irreducible: any nonzero invariant subspace W contains, for 0 ≠ w ∈ W and any v, an element T w = v with T ∈ A, hence W = ⊤.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Nontrivial, Eq, Subalgebra, Module.End, Slop.OddRep.adjoinRange, Top.top, Representation.IsIrreducible
Proof uses: Iff.mpr, And, Submodule, Membership.mem, LinearMap, RingHom.id, Or, Bot.bot, Slop.OddRep.isIrreducible_iff_forall, And.intro, inferInstance, Algebra.adjoin, Set.range, Algebra.adjoin_induction, Set, RingHom, Algebra.algebraMap, HSMul.hSMul, of_eq_true, eq_self and 35 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma isIrreducible_of_adjoinRange_eq_top [Nontrivial V]
    (h : adjoinRange ρ = ⊤) :
    ρ.IsIrreducible := by
…
```
Mentions: Slop.OddRep.adjoinRange
lemma Slop.OddRep.isIrreducible_of_baseChange Documented declaration: isIrreducible_of_baseChange line 405 source
Source documentation
If the base change of ρ along some field extension l/k is irreducible, then ρ itself is irreducible (an invariant subspace W ⊊ V gives rise to the invariant subspace l ⊗[k] W ⊊ l ⊗[k] V).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Algebra, Representation.IsIrreducible, TensorProduct, Slop.OddRep.baseChange
Proof uses: Nontrivial, Submodule, Membership.mem, LinearMap, RingHom.id, Or, Eq, Bot.bot, Top.top, And, Iff.mp, Slop.OddRep.isIrreducible_iff_forall, Iff.mpr, And.intro, Classical.byContradiction, Not, Subsingleton, Eq.mp, congrArg, propext and 37 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma isIrreducible_of_baseChange (l : Type*) [Field l] [Algebra k l]
    (h : (baseChange l ρ).IsIrreducible) :
    ρ.IsIrreducible := by
…
```
Mentions: Slop.OddRep.baseChange
theorem Slop.OddRep.isIrreducible_baseChange_of_finrank_eigenspace_eq_one The quantitative version of the hard direction: under the hypotheses of Theorem 1.3, the base change of ρ to any field extension l/k is irreducible line 447 source
Source documentation
The quantitative version of the hard direction: under the hypotheses of Theorem 1.3, the base change of ρ to any field extension l/k is irreducible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, FiniteDimensional, Algebra, Representation.IsIrreducible, Eq, Nat, Module.finrank, Subtype, Membership.mem, Submodule, Module.End.eigenspace, LinearMap, RingHom.id, OfNat.ofNat, TensorProduct, Slop.OddRep.baseChange
Proof uses: Module.End, Commute, Exists, HSMul.hSMul, Slop.OddRep.exists_smul_eq_of_commute, Subalgebra, Slop.OddRep.adjoinRange, Top.top, Slop.OddRep.adjoinRange_eq_top, Slop.OddRep.adjoinRange_baseChange_eq_top, Nontrivial, And.left, Or, Bot.bot, Iff.mp, And, Slop.OddRep.isIrreducible_iff_forall, Ne, exists_ne, Module.Dual and 14 more
135 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem isIrreducible_baseChange_of_finrank_eigenspace_eq_one
    [FiniteDimensional k V]
    (l : Type*) [Field l] [Algebra k l]
    (hirr : ρ.IsIrreducible)
    {g : G} (hg : finrank k (Module.End.eigenspace (ρ g) 1) = 1) :
    (baseChange l ρ).IsIrreducible := by
…
```
Mentions: Slop.OddRep.baseChange
theorem Slop.OddRep.isIrreducible_iff_isAbsolutelyIrreducible_slop Proposition 1.2 / Theorem 1.3 line 480 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: id, Iff.intro, AlgebraicClosure, TensorProduct, Slop.OddRep.baseChange, Slop.OddRep.isIrreducible_baseChange_of_finrank_eigenspace_eq_one, Slop.OddRep.isIrreducible_of_baseChange
60 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem isIrreducible_iff_isAbsolutelyIrreducible_slop
    [FiniteDimensional k V]
    {g : G} (hg : finrank k (Module.End.eigenspace (ρ g) 1) = 1) :
    ρ.IsIrreducible ↔ IsAbsolutelyIrreducible ρ := by
…
```
Mentions: Slop.OddRep.IsAbsolutelyIrreducible