Diff — Representation theory

Revision #3286 → #4160 · back to history

modifiedRepresentation (via action)a300b7a2835c

Field	From #3286	To #4160
note	The action-style definition is `MulAction G V`, which is the standard Mathlib formulation of a group acting on a type.	Verified: `MulAction G V` in `Mathlib.Algebra.Group.Action.Defs` is the standard action-style formalization of a group acting on a type.

modifiedRepresentation (via homomorphism)e6d4711e831d

Field	From #3286	To #4160
note	`Representation k G V` is defined as the monoid hom `G →* (V →ₗ[k] V)`, exactly the homomorphism viewpoint.	Verified: `Representation k G V` in `Mathlib.RepresentationTheory.Basic` is defined as the monoid hom `G →* (V →ₗ[k] V)`.

modifiedRepresentation space and dimension94fb5fff8c56

Field	From #3286	To #4160
note	The underlying module of an object of `Rep k G` is the projection `Rep.V`; its dimension is `Module.finrank k V` (used e.g. in `FDRep.char_one`).	Verified: `Rep.V` returns the underlying module of a `Rep k G` object; dimension is expressed via `Module.finrank`.

modifiedFaithful representationfe793fad075d

Field	From #3286	To #4160
note	Mathlib has `FaithfulSMul` for actions, but there is no dedicated `Representation.IsFaithful` predicate spelling out injectivity of `ρ`.	Verified: `FaithfulSMul` exists in `Mathlib.Algebra.Group.Action.Faithful`; no dedicated `Representation.IsFaithful` predicate.

modifiedEquivariant map8775b7fa042f

Field	From #3286	To #4160
note	`IntertwiningMap ρ σ` bundles a linear map commuting with the group action, i.e. an equivariant/`G`-linear map.	Verified: `Representation.IntertwiningMap ρ σ` bundles a linear map commuting with the group action, i.e. a `G`-equivariant map.

modifiedIsomorphism of representationsfcf999572d42

Field	From #3286	To #4160
note	`Representation.Equiv ρ σ` is a linear equivalence that is also an intertwining map, i.e. an isomorphism of representations.	Verified: `Representation.Equiv ρ σ` is a linear equivalence that is also an intertwining map.

modifiedSubrepresentation168720ab99f5

Field	From #3286	To #4160
note	`Subrepresentation ρ` is a `Submodule` of `V` stable under every `ρ g`.	Verified: `Subrepresentation ρ` is a `Submodule` of `V` stable under every `ρ g`.

addedQuotient representation32c21f42c2b1

modifiedIrreducible and reducible representation7b17fad6762f

Field	From #3286	To #4160
note	`Representation.IsIrreducible ρ` is `IsSimpleOrder (Subrepresentation ρ)`, the standard formalization of irreducibility.	Verified: `Representation.IsIrreducible ρ` is defined via `IsSimpleOrder (Subrepresentation ρ)`.

modifiedSchur's lemma604c3bb9fb84

Field	From #3286	To #4160
note	Schur's lemma appears as `FDRep.finrank_hom_simple_simple` and `IsIrreducible.bijective_or_eq_zero` in `Mathlib.RepresentationTheory.Irreducible`.	Verified: Schur's lemma appears as `FDRep.finrank_hom_simple_simple` (finite-dimensional form) in `Mathlib.RepresentationTheory.FDRep`.

modifiedDirect sum of representations68ac6a1056ec

Field	From #3286	To #4160
note	`Representation.directSum` builds a representation on `⨁ i, V i` from a family of representations.	Verified: `Representation.directSum` builds a representation on `⨁ i, V i` from a family of representations.

modifiedDecomposable and indecomposable representationdc5569bcab26

Field	From #3286	To #4160
note	No `Indecomposable` predicate for representations exists in `Mathlib/RepresentationTheory`; the only `Indecomposable` files concern categories and monoids.	Grep of `Mathlib/RepresentationTheory` for `Indecomposable` returns no matches — no indecomposable-representation predicate exists.

modifiedSemisimple representation10fe0abbfb47

Field	From #3286	To #4160
note	`Representation.IsSemisimpleRepresentation ρ` is defined and shown equivalent to `IsSemisimpleModule k[G] ρ.asModule`.	Verified: `Representation.IsSemisimpleRepresentation` is defined in `Mathlib.RepresentationTheory.Semisimple` and shown equivalent to `IsSemisimpleModule k[G] ρ.asModule`.

modifiedTensor product of representationsb3b1fda4f216

Field	From #3286	To #4160
note	`Representation.tprod ρV ρW` is the representation on `V ⊗[k] W` via `TensorProduct.map (ρV g) (ρW g)`.	Verified: `Representation.tprod ρV ρW` builds the tensor-product representation on `V ⊗[k] W`.

modifiedClebsch–Gordan decomposition for SU(2)d40600f87e7f

Field	From #3286	To #4160
note	No Clebsch–Gordan decomposition or SU(2) representation theory appears anywhere under `Mathlib/`.	Grep across `Mathlib/` finds no Clebsch–Gordan or SU(2) representation theory.

modifiedMaschke's theorem28d01f0d1bbd

Field	From #3286	To #4160
note	Maschke's theorem is `MonoidAlgebra.Submodule.exists_isCompl` with the immediate instance `IsSemisimpleModule k[G] V` in `Mathlib.RepresentationTheory.Maschke`.	Verified: `MonoidAlgebra.Submodule.exists_isCompl` in `Mathlib.RepresentationTheory.Maschke` is Maschke's theorem.

modifiedCharacter of a representationb8d23e333ab3

Field	From #3286	To #4160
note	`FDRep.character V g = trace (ρ V g)` and `Representation.character` give the character of a finite-dimensional representation.	Verified: `FDRep.character V g = trace (ρ V g)` in `Mathlib.RepresentationTheory.Character`.

addedGroup algebra F[G]d97fd58fc0d4

modifiedModular representationcefcd3c6abec

Field	From #3286	To #4160
note	Mathlib's `Representation k G V` covers any field `k` including positive characteristic, but there is no dedicated `ModularRepresentation` notion or modular-representation-specific theory.	Grep finds no `ModularRepresentation`; `Representation k G V` supports positive characteristic but no modular-representation-specific theory is developed.

modifiedUnitary representation7e07e450bcd7

Field	From #3286	To #4160
note	No `UnitaryRepresentation` (or analogous Hilbert-space representation) is defined in `Mathlib/RepresentationTheory`.	Grep finds no `UnitaryRepresentation` anywhere in `Mathlib/`.

addedPeter–Weyl theorem664b514600c8

addedHaar measure7d2643b27f6e

modifiedLie groupe08b1e22a194

Field	From #3286	To #4160
note	`LieGroup I n G` requires a group structure on a manifold with `C^n` multiplication and inversion.	Verified: `LieGroup I n G` in `Mathlib.Geometry.Manifold.Algebra.LieGroup` requires a group on a manifold with `C^n` multiplication and inversion.

modifiedLie algebra5499dcf284b8

Field	From #3286	To #4160
note	`LieAlgebra R L` is the standard typeclass extending `LieRing L` with `Module R L` compatibility.	Verified: `LieAlgebra R L` extends `LieRing L` with `Module R L` compatibility.

addedCartan subalgebra2de094d4d6ca

modifiedLie superalgebra32713eb614d0

Field	From #3286	To #4160
note	Grep for `LieSuper`/`SuperLie` under `Mathlib/` returns no results; Lie superalgebras are not in Mathlib.	Grep for `LieSuper`/`SuperLie`/`LieSuperalgebra` under `Mathlib/` returns no results.

modifiedLinear algebraic group95e23949cf70

Field	From #3286	To #4160
note	No `LinearAlgebraicGroup` or `AffineGroupScheme` declaration exists in `Mathlib/`.	Grep for `LinearAlgebraicGroup`/`AffineGroupScheme` returns no matches in `Mathlib/`.

modifiedAutomorphic formcd5381ffd391

Field	From #3286	To #4160
note	Grep finds no `AutomorphicForm`/`automorphic` notion in Mathlib (modular forms exist, but automorphic forms do not).	Grep for `AutomorphicForm`/`Automorphic` in `Mathlib/` returns no matches.

addedUniversal enveloping algebrafe1f56368da5

addedHopf algebrae78a6659161a

modifiedSet-theoretic representatione9cc9590e0e0

Field	From #3286	To #4160
note	A set-theoretic / permutation representation is exactly a `MulAction G X` in Mathlib.	Verified: `MulAction G X` is exactly a set-theoretic / permutation representation.

modifiedRepresentation of a group in a category7090db2e1d47

Field	From #3286	To #4160
note	`Action V G` bundles an object of `V` with `ρ : G →* Aut(V)`, equivalent to the functor `SingleObj G ⥤ V` as documented in the file header.	Verified: `Action V G` bundles an object of `V` with `ρ : G →* Aut(V)`, equivalent to a functor `SingleObj G ⥤ V`.

addedQuiver0db61cc77547

addedMonoid action / monoid representationa3ccbf433aab