Intertwining

📁 Source: Mathlib/RepresentationTheory/Intertwining.lean

Statistics

Metric	Count
Definitions IntertwiningMap, centralMul, coeFnAddMonoidHom, comp, equivAlgEnd, equivLinearMapAsModule, id, instAdd, instAddCommMonoid, instAlgebra, instFunLike, instModule, instMonoid, instMul, instNatCast, instOne, instPowNat, instSMul, instSMulNat, instSemigroup, instSemiring, instZero, llcomp, toLinearMap, IsIntertwiningMap	25
Theorems algebraMap_apply, coe_add, coe_mk, coe_mul, coe_nsmul, coe_one, coe_smul, coe_zero, ext, ext_iff, isIntertwining, isIntertwining', isIntertwiningMap_of_mem_center, mul_apply, toFun_injective, toLinearMap_apply, toLinearMap_injective, isIntertwining, isIntertwiningMap_iff	19
Total	44

Representation

Definitions

Name	Category	Theorems
IntertwiningMap 📖	CompData	16 math math: IntertwiningMap.mul_apply, IntertwiningMap.toLinearMap_injective, IntertwiningMap.coe_mul, IntertwiningMap.coe_zero, IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed, IsIrreducible.bijective_or_eq_zero, IntertwiningMap.algebraMap_apply, IsIrreducible.injective_or_eq_zero, IntertwiningMap.toLinearMap_apply, IntertwiningMap.toFun_injective, IntertwiningMap.coe_add, IntertwiningMap.isIntertwining, IntertwiningMap.coe_mk, IntertwiningMap.coe_nsmul, IntertwiningMap.coe_smul, IntertwiningMap.coe_one
IsIntertwiningMap 📖	CompData	2 math math: IntertwiningMap.isIntertwiningMap_of_mem_center, isIntertwiningMap_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntertwiningMap_iff 📖	mathematical	—	IsIntertwiningMap DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—

Representation.IntertwiningMap

Definitions

Name	Category	Theorems
centralMul 📖	CompOp	—
coeFnAddMonoidHom 📖	CompOp	—
comp 📖	CompOp	—
equivAlgEnd 📖	CompOp	—
equivLinearMapAsModule 📖	CompOp	—
id 📖	CompOp	—
instAdd 📖	CompOp	1 math math: coe_add
instAddCommMonoid 📖	CompOp	—
instAlgebra 📖	CompOp	2 math math: Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed, algebraMap_apply
instFunLike 📖	CompOp	11 math math: mul_apply, coe_zero, Representation.IsIrreducible.bijective_or_eq_zero, Representation.IsIrreducible.injective_or_eq_zero, toLinearMap_apply, coe_add, isIntertwining, coe_mk, coe_nsmul, coe_smul, coe_one
instModule 📖	CompOp	—
instMonoid 📖	CompOp	—
instMul 📖	CompOp	2 math math: mul_apply, coe_mul
instNatCast 📖	CompOp	—
instOne 📖	CompOp	2 math math: algebraMap_apply, coe_one
instPowNat 📖	CompOp	—
instSMul 📖	CompOp	2 math math: algebraMap_apply, coe_smul
instSMulNat 📖	CompOp	1 math math: coe_nsmul
instSemigroup 📖	CompOp	—
instSemiring 📖	CompOp	2 math math: Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed, algebraMap_apply
instZero 📖	CompOp	3 math math: coe_zero, Representation.IsIrreducible.bijective_or_eq_zero, Representation.IsIrreducible.injective_or_eq_zero
llcomp 📖	CompOp	—
toLinearMap 📖	CompOp	6 math math: toLinearMap_injective, coe_mul, ext_iff, toLinearMap_apply, toFun_injective, isIntertwining'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom Representation.IntertwiningMap Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instSemiring RingHom.instFunLike algebraMap instAlgebra instSMul instOne	—	—
coe_add 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap instFunLike instAdd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coe_mk 📖	mathematical	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe LinearMap LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	Representation.IntertwiningMap instFunLike	—	—
coe_mul 📖	mathematical	—	toLinearMap Representation.IntertwiningMap instMul LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.End.instMul	—	—
coe_nsmul 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap instFunLike instSMulNat AddMonoid.toNatSMul Pi.addMonoid AddCommMonoid.toAddMonoid	—	—
coe_one 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap instFunLike instOne	—	—
coe_smul 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap instFunLike instSMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction	—	—
coe_zero 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap instFunLike instZero Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
ext 📖	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring toLinearMap	—	—	—
ext_iff 📖	mathematical	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring toLinearMap	—	ext
isIntertwining 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap instFunLike LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	isIntertwining'
isIntertwining' 📖	mathematical	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring toLinearMap DFunLike.coe LinearMap LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—
isIntertwiningMap_of_mem_center 📖	mathematical	Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.center	Representation.IsIntertwiningMap DFunLike.coe Representation CommRing.toCommSemiring LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	Representation.isIntertwiningMap_iff Module.End.mul_apply MonoidHom.map_mul Submonoid.mem_center_iff
mul_apply 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap instFunLike instMul	—	—
toFun_injective 📖	mathematical	—	Representation.IntertwiningMap AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring toLinearMap	—	ext
toLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike toLinearMap Representation.IntertwiningMap instFunLike	—	—
toLinearMap_injective 📖	mathematical	—	Representation.IntertwiningMap LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring toLinearMap	—	ext

Representation.IsIntertwiningMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntertwining 📖	mathematical	Representation.IsIntertwiningMap	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—

---

← Back to Index