Commit 2026-01-22 17:00 38c0fbc1

View on Github →

feat: definition of an intertwining map (#33221) Adds the definition of an intertwining map of representations, with an instance of an A-module structure. Proves that a multiplication by a central element is an intertwining map.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RepresentationTheory/Intertwining.lean

added def Representation.IntertwiningMap.centralMul

added def Representation.IntertwiningMap.coeFnAddMonoidHom

added theorem Representation.IntertwiningMap.coe_add

added theorem Representation.IntertwiningMap.coe_nsmul

added theorem Representation.IntertwiningMap.coe_smul

added theorem Representation.IntertwiningMap.coe_zero

added def Representation.IntertwiningMap.equivLinearMapAsModule

added theorem Representation.IntertwiningMap.id_apply

added theorem Representation.IntertwiningMap.isIntertwining

added theorem Representation.IntertwiningMap.isIntertwiningMap_of_mem_center

added theorem Representation.IntertwiningMap.toFun_injective

added theorem Representation.IntertwiningMap.toLinearMap_apply

added theorem Representation.IntertwiningMap.toLinearMap_injective

added structure Representation.IntertwiningMap

added structure Representation.IsIntertwiningMap

Modified Mathlib/RepresentationTheory/Subrepresentation.lean