[Merged by Bors] - feat: Schur's lemma for monoid representations

[stepan2698-cpu]

Adds an algebra instance on the set of intertwining maps. Proves various versions of Schur's lemma for monoid representations and proves that a finite-dimensional irreducible representation of a commutative monoid is one-dimensional.

---

• depends on: [Merged by Bors] - feat: definition of an irreducible representation #32856
• depends on: [Merged by Bors] - feat: definition of an intertwining map #33221

[github-actions]

PR summary c99f041082

Import changes exceeding 2%

%	File
+21.64%	Mathlib.RepresentationTheory.Irreducible

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RepresentationTheory.Irreducible	1400	1703	+303 (+21.64%)

Import changes for all files

Files	Import difference
Mathlib.RepresentationTheory.Irreducible	303

---

Declarations diff

+ algebraMap_apply
+ algebraMap_intertwiningMap_bijective_of_isAlgClosed
+ bijective_or_eq_zero
+ coe_mk
+ coe_mul
+ coe_one
+ comp
+ equivAlgEnd
+ finrank_eq_one_of_isMulCommutative
+ injective_or_eq_zero
+ instSemiring
+ instance (ρ : Representation k G V) [Module.Finite k V] : Module.Finite k ρ.asModule
+ instance : Algebra A (IntertwiningMap ρ ρ)
+ instance : IsSimpleModule k[G] ρ.asModule
+ instance : Monoid (IntertwiningMap ρ ρ)
+ instance : Mul (IntertwiningMap ρ ρ)
+ instance : NatCast (IntertwiningMap ρ ρ)
+ instance : One (IntertwiningMap ρ ρ) := ⟨id ρ⟩
+ instance : Pow (IntertwiningMap ρ ρ) ℕ := ⟨fun f n => npowRecAuto n f⟩
+ instance : Semigroup (IntertwiningMap ρ ρ)
+ llcomp
+ mul_apply
- id_apply

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[stepan2698-cpu]

in addition to the inline comment below, it looks like the PR description also needs updating.

I'm not sure why the Schur's lemma disappeared from this PR, I've added it back.

[stepan2698-cpu]

-awaiting-author

[ocfnash]

Thanks, this is nearly ready.

I have some concerns that we now have multiple spellings of Schur's Lemma, including FDRep.simple_iff_end_is_rank_one. This is partly a legacy of an interesting but more-or-less abandoned early attempt to develop representation theory in the language of category theory.

I'd be interested in any thoughts you might have about tidying this up, and I'll do some thinking but in the meantime I've left a few minor comments.

[stepan2698-cpu]

-awaiting-author

[stepan2698-cpu]

Thanks, this is nearly ready.

I have some concerns that we now have multiple spellings of Schur's Lemma, including FDRep.simple_iff_end_is_rank_one. This is partly a legacy of an interesting but more-or-less abandoned early attempt to develop representation theory in the language of category theory.

I'd be interested in any thoughts you might have about tidying this up, and I'll do some thinking but in the meantime I've left a few minor comments.

Ok I raised this question on Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Developing.20irreducible.20representations.20for.20mathlib/with/568481781
I was somewhat aware that there is older API for simple objects in the category of representations, and one reason I needed this version of Schur's lemma is because I wanted to give a proof of equivalence of the two definitions, and one direction (If rho is irreducible, then any monomorphism to rho is an isomorphism) is basically Schur's lemma in disguise.

[ocfnash]

I think this will be ready after my final nitpicks as follows:

[stepan2698-cpu]

-awaiting-author

[ocfnash]

Thanks, please apply my last two suggestions and then feel free to merge!

bors d+

[mathlib-bors]

✌️ stepan2698-cpu can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[stepan2698-cpu]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step