Induced

📁 Source: Mathlib/RepresentationTheory/Induced.lean

Statistics

Metric	Count
Definitions coinvariantsTensorIndHom, coinvariantsTensorIndInv, coinvariantsTensorIndIso, coinvariantsTensorIndNatIso, ind, indFunctor, indMap, indResAdjunction, indResHomEquiv, IndV, mk, ind	12
Theorems coinvariantsTensorIndHom_mk_tmul_indVMk, coinvariantsTensorIndInv_mk_tmul_indMk, coinvariantsTensorIndIso_hom, coinvariantsTensorIndIso_inv, coinvariantsTensorIndNatIso_hom_app, coinvariantsTensorIndNatIso_inv_app, indFunctor_map, indFunctor_obj, indResHomEquiv_apply, indResHomEquiv_symm_apply, instIsLeftAdjointIndFunctor, instIsRightAdjointResFunctor, hom_ext, hom_ext_iff, ind_apply, ind_mk	16
Total	28

Rep

Definitions

Name	Category	Theorems
coinvariantsTensorIndHom 📖	CompOp	3 math math: coinvariantsTensorIndIso_hom, coinvariantsTensorIndNatIso_hom_app, coinvariantsTensorIndHom_mk_tmul_indVMk
coinvariantsTensorIndInv 📖	CompOp	3 math math: coinvariantsTensorIndIso_inv, coinvariantsTensorIndNatIso_inv_app, coinvariantsTensorIndInv_mk_tmul_indMk
coinvariantsTensorIndIso 📖	CompOp	2 math math: coinvariantsTensorIndIso_inv, coinvariantsTensorIndIso_hom
coinvariantsTensorIndNatIso 📖	CompOp	2 math math: coinvariantsTensorIndNatIso_inv_app, coinvariantsTensorIndNatIso_hom_app
ind 📖	CompOp	25 math math: coindResAdjunction_counit_app, coindToInd_of_support_subset_orbit, indFunctor_obj, indCoindNatIso_hom_app, coindToInd_indToCoind, coinvariantsTensorIndIso_inv, coinvariantsTensorIndIso_hom, coinvariantsTensorIndNatIso_inv_app, coindResAdjunction_unit_app, coindToInd_apply, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, coindResAdjunction_homEquiv_apply, resIndAdjunction_counit_app, coinvariantsTensorIndNatIso_hom_app, indCoindNatIso_inv_app, coindResAdjunction_homEquiv_symm_apply, indCoindIso_hom_hom_toLinearMap, indResHomEquiv_apply, indCoindIso_inv_hom_toLinearMap, resIndAdjunction_unit_app, coinvariantsTensorIndHom_mk_tmul_indVMk, indToCoind_coindToInd, indResHomEquiv_symm_apply, coinvariantsTensorIndInv_mk_tmul_indMk
indFunctor 📖	CompOp	12 math math: coindResAdjunction_counit_app, indFunctor_obj, indCoindNatIso_hom_app, coindResAdjunction_unit_app, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, resIndAdjunction_counit_app, indCoindNatIso_inv_app, indFunctor_map, resIndAdjunction_unit_app, instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, instIsLeftAdjointIndFunctor
indMap 📖	CompOp	1 math math: indFunctor_map
indResAdjunction 📖	CompOp	2 math math: coindResAdjunction_counit_app, coindResAdjunction_unit_app
indResHomEquiv 📖	CompOp	4 math math: coindResAdjunction_homEquiv_apply, coindResAdjunction_homEquiv_symm_apply, indResHomEquiv_apply, indResHomEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinvariantsTensorIndHom_mk_tmul_indVMk 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind res ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier coinvariantsTensorIndHom V hV1 hV2 LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction coinvariantsTensorMk Representation.IndV ρ Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup TensorProduct.instModule Representation.tprod MonoidHom.comp NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Representation.Coinvariants.instModule Representation MonoidHom.instFunLike	—	smulCommClass_self RingHomCompTriple.ids Finsupp.sum_single_index zero_smul LinearMap.instSMulCommClass one_smul
coinvariantsTensorIndInv_mk_tmul_indMk 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor res ind ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier coinvariantsTensorIndInv TensorProduct V hV1 hV2 Representation.Coinvariants TensorProduct.addCommGroup TensorProduct.instModule Representation.tprod ρ Representation.Coinvariants.instAddCommGroup Representation.Coinvariants.instModule TensorProduct.tmul LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction coinvariantsTensorMk Representation.IndV Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Finsupp.instAddCommGroup Ring.toAddCommGroup MonoidHom.comp NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
coinvariantsTensorIndIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind res coinvariantsTensorIndIso coinvariantsTensorIndHom	—	—
coinvariantsTensorIndIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind res coinvariantsTensorIndIso coinvariantsTensorIndInv	—	—
coinvariantsTensorIndNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind CategoryTheory.Functor.comp resFunctor CategoryTheory.Iso.hom coinvariantsTensorIndNatIso coinvariantsTensorIndHom	—	—
coinvariantsTensorIndNatIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.comp resFunctor CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category coinvariantsTensor ind CategoryTheory.Iso.inv coinvariantsTensorIndNatIso coinvariantsTensorIndInv	—	—
indFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory indFunctor indMap	—	—
indFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory indFunctor ind	—	—
indResHomEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory ind res AddCommGroup.toAddCommMonoid instAddCommGroupHom instModuleHom EquivLike.toFunLike LinearEquiv.instEquivLike indResHomEquiv ofHom V hV1 hV2 ρ MonoidHom.comp LinearMap MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearMap.comp Representation.IntertwiningMap.toLinearMap Hom.hom InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	RingHomInvPair.ids
indResHomEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory res ind AddCommGroup.toAddCommMonoid instAddCommGroupHom instModuleHom EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm indResHomEquiv ofHom Representation.IndV V hV1 hV2 ρ Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule Representation.tprod MonoidHom.comp LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Representation.Coinvariants.instModule Representation.ind Representation.Coinvariants.lift TensorProduct.lift AddEquiv LinearMap.addCommMonoid LinearMap.module Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instAdd AddEquiv.instEquivLike Finsupp.lift LinearMap.comp Representation MonoidHom.instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Representation.IntertwiningMap.toLinearMap Hom.hom	—	RingHomInvPair.ids
instIsLeftAdjointIndFunctor 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory indFunctor	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointResFunctor 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory resFunctor	—	CategoryTheory.Adjunction.isRightAdjoint

Representation

Definitions

Name	Category	Theorems
IndV 📖	CompOp	10 math math: Rep.coindToInd_of_support_subset_orbit, Rep.coindToInd_apply, Rep.indCoindIso_hom_hom_toLinearMap, Rep.indCoindIso_inv_hom_toLinearMap, ind_mk, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Rep.indResHomEquiv_symm_apply, ind_apply, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, IndV.hom_ext_iff
ind 📖	CompOp	5 math math: Rep.indCoindIso_hom_hom_toLinearMap, Rep.indCoindIso_inv_hom_toLinearMap, ind_mk, Rep.indResHomEquiv_symm_apply, ind_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ind_apply 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring IndV AddCommGroup.toAddCommMonoid Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule tprod MonoidHom.comp NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring leftRegular Coinvariants.instModule MonoidHom.instFunLike ind Coinvariants.map LinearMap.rTensor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.lmapDomain MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
ind_mk 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring IndV AddCommGroup.toAddCommMonoid Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule tprod MonoidHom.comp NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring leftRegular Coinvariants.instModule LinearMap.instFunLike Representation MonoidHom.instFunLike ind MulOne.toMul InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Finsupp.mapDomain_single

Representation.IndV

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	LinearMap.comp Representation.IndV CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule Representation.tprod MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Representation.Coinvariants.instModule RingHomCompTriple.ids	—	—	RingHomCompTriple.ids Representation.Coinvariants.hom_ext TensorProduct.ext Finsupp.lhom_ext' smulCommClass_self LinearMap.ext_ring
hom_ext_iff 📖	mathematical	—	LinearMap.comp Representation.IndV CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Representation.Coinvariants.instAddCommGroup TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule DivInvMonoid.toMonoid Group.toDivInvMonoid TensorProduct.addCommGroup Finsupp.instAddCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.instModule Representation.tprod MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.leftRegular Representation.Coinvariants.instModule RingHomCompTriple.ids	—	RingHomCompTriple.ids hom_ext

---

← Back to Index