FDRep

📁 Source: Mathlib/RepresentationTheory/FDRep.lean

Statistics

Metric	Count
Definitions FDRep, dualTensorIsoLinHom, dualTensorIsoLinHomAux, forget₂HomLinearEquiv, instAddCommGroupCarrierVFGModuleCat, instCoeSortType, instConcreteCategoryHomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRep, instLargeCategory, instLinear, instModuleCarrierVFGModuleCat, instPreadditive, instRightRigidCategory, isoToLinearEquiv, of, ρ	16
Theorems conj_ρ, dualTensorIsoLinHom_hom_hom, endRingEquiv_comp_ρ, endRingEquiv_symm_comp_ρ, finrank_hom_simple_simple, forget₂_ρ, hom_action_ρ, hom_hom_action_ρ, instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, instFiniteCarrierVFGModuleCat, instFiniteDimensionalCarrierVFGModuleCat, instFiniteDimensionalHom, instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, instHasFiniteLimits, instHasKernels, instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, of_ρ, of_ρ'	19
Total	35

FDRep

Definitions

Name	Category	Theorems
dualTensorIsoLinHom 📖	CompOp	1 math math: dualTensorIsoLinHom_hom_hom
dualTensorIsoLinHomAux 📖	CompOp	—
forget₂HomLinearEquiv 📖	CompOp	—
instAddCommGroupCarrierVFGModuleCat 📖	CompOp	14 math math: TannakaDuality.FiniteGroup.sumSMulInv_apply, instFiniteDimensionalCarrierVFGModuleCat, average_char_eq_finrank_invariants, hom_hom_action_ρ, TannakaDuality.FiniteGroup.equivApp_inv, TannakaDuality.FiniteGroup.equivApp_hom, char_linHom, char_one, TannakaDuality.FiniteGroup.sumSMulInv_single_id, instFiniteCarrierVFGModuleCat, Iso.conj_ρ, char_dual, hom_action_ρ, dualTensorIsoLinHom_hom_hom
instCoeSortType 📖	CompOp	—
instConcreteCategoryHomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV 📖	CompOp	5 math math: instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, forget₂_ρ, instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV
instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRep 📖	CompOp	5 math math: instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, forget₂_ρ, instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV
instLargeCategory 📖	CompOp	24 math math: TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, char_tensor, TannakaDuality.FiniteGroup.forget_obj, instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, instFiniteDimensionalHom, instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, TannakaDuality.FiniteGroup.forget_map, instHasKernels, instInjectiveOfNeZeroCastCard, simple_iff_end_is_rank_one, forget₂_ρ, char_orthonormal, instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, instHasFiniteLimits, instProjectiveOfNeZeroCastCard, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, scalar_product_char_eq_finrank_equivariant, TannakaDuality.FiniteGroup.equivHom_surjective, TannakaDuality.FiniteGroup.equivHom_injective, dualTensorIsoLinHom_hom_hom, instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, TannakaDuality.FiniteGroup.equivHom_apply, simple_iff_char_is_norm_one, finrank_hom_simple_simple
instLinear 📖	CompOp	4 math math: instFiniteDimensionalHom, simple_iff_end_is_rank_one, scalar_product_char_eq_finrank_equivariant, finrank_hom_simple_simple
instModuleCarrierVFGModuleCat 📖	CompOp	14 math math: TannakaDuality.FiniteGroup.sumSMulInv_apply, instFiniteDimensionalCarrierVFGModuleCat, average_char_eq_finrank_invariants, hom_hom_action_ρ, TannakaDuality.FiniteGroup.equivApp_inv, TannakaDuality.FiniteGroup.equivApp_hom, char_linHom, char_one, TannakaDuality.FiniteGroup.sumSMulInv_single_id, instFiniteCarrierVFGModuleCat, Iso.conj_ρ, char_dual, hom_action_ρ, dualTensorIsoLinHom_hom_hom
instPreadditive 📖	CompOp	4 math math: instFiniteDimensionalHom, simple_iff_end_is_rank_one, scalar_product_char_eq_finrank_equivariant, finrank_hom_simple_simple
instRightRigidCategory 📖	CompOp	—
isoToLinearEquiv 📖	CompOp	1 math math: Iso.conj_ρ
of 📖	CompOp	5 math math: of_ρ', char_linHom, of_ρ, char_dual, dualTensorIsoLinHom_hom_hom
ρ 📖	CompOp	15 math math: endRingEquiv_symm_comp_ρ, of_ρ', TannakaDuality.FiniteGroup.sumSMulInv_apply, average_char_eq_finrank_invariants, hom_hom_action_ρ, TannakaDuality.FiniteGroup.equivApp_inv, TannakaDuality.FiniteGroup.equivApp_hom, char_linHom, TannakaDuality.FiniteGroup.sumSMulInv_single_id, forget₂_ρ, Iso.conj_ρ, char_dual, hom_action_ρ, dualTensorIsoLinHom_hom_hom, endRingEquiv_comp_ρ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dualTensorIsoLinHom_hom_hom 📖	mathematical	—	Action.Hom.hom FGModuleCat CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.MonoidalCategoryStruct.tensorObj FDRep instLargeCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory CategoryTheory.ObjectProperty.fullMonoidalSubcategory ModuleCat.monoidalCategory FGModuleCat.instIsMonoidalModuleCatIsFG of Module.Dual CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid LinearMap.addCommGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass Algebra.id Module.Finite.linearMap Module.Free.of_divisionRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self Representation.dual LinearMap FGModuleCat.carrier Action.V instAddCommGroupCarrierVFGModuleCat instModuleCarrierVFGModuleCat smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFiniteDimensionalCarrierVFGModuleCat Representation.linHom ρ CategoryTheory.Iso.hom dualTensorIsoLinHom CategoryTheory.ConcreteCategory.ofHom Ring.toSemiring ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.FullSubcategory.concreteCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier dualTensorHom	—	FGModuleCat.instIsMonoidalModuleCatIsFG Algebra.to_smulCommClass Module.Finite.linearMap Module.Free.of_divisionRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self smulCommClass_self instFiniteDimensionalCarrierVFGModuleCat
endRingEquiv_comp_ρ 📖	mathematical	—	MonoidHom.comp CategoryTheory.End ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isFG Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass CategoryTheory.Preadditive.instSemiringEnd ModuleCat.instPreadditive Module.End.instSemiring MonoidHomClass.toMonoidHom RingEquiv CategoryTheory.End.mul Module.End.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd LinearMap.instAdd EquivLike.toFunLike RingEquiv.instEquivLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass ModuleCat.endRingEquiv CategoryTheory.Preadditive.fullSubcategory MulEquiv.toMonoidHom CategoryTheory.InducedCategory.endEquiv CategoryTheory.ObjectProperty.FullSubcategory Action.ρ ρ	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
endRingEquiv_symm_comp_ρ 📖	mathematical	—	MonoidHom.comp LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring CategoryTheory.Preadditive.instSemiringEnd ModuleCat.instPreadditive MonoidHomClass.toMonoidHom RingEquiv Module.End.instMul CategoryTheory.End.mul LinearMap.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd EquivLike.toFunLike RingEquiv.instEquivLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm ModuleCat.endRingEquiv ρ CategoryTheory.Preadditive.fullSubcategory MulEquiv.toMonoidHom CategoryTheory.InducedCategory.endEquiv CategoryTheory.ObjectProperty.FullSubcategory Action.ρ	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
finrank_hom_simple_simple 📖	mathematical	—	Module.finrank Quiver.Hom FDRep DivisionRing.toRing Field.toDivisionRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instLargeCategory EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup instPreadditive CategoryTheory.Linear.homModule instLinear CategoryTheory.Iso	—	CategoryTheory.finrank_hom_simple_simple instHasKernels instFiniteDimensionalHom
forget₂_ρ 📖	mathematical	—	Rep.ρ CategoryTheory.Functor.obj FDRep CommRing.toRing instLargeCategory Rep Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Action.HomSubtype FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat.isFG LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.FullSubcategory.concreteCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV CommSemiring.toSemiring CommRing.toCommSemiring instConcreteCategoryHomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV Action.instConcreteCategoryHomSubtypeV instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRep ρ	—	MonoidHom.ext LinearMap.ext
hom_action_ρ 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring FGModuleCat.carrier AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVFGModuleCat instModuleCarrierVFGModuleCat MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	hom_hom_action_ρ
hom_hom_action_ρ 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring FGModuleCat.carrier AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVFGModuleCat instModuleCarrierVFGModuleCat MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	—
instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV 📖	mathematical	—	CategoryTheory.Functor.Faithful FDRep CommRing.toRing instLargeCategory Rep Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Action.HomSubtype FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat.isFG LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.FullSubcategory.concreteCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV CommSemiring.toSemiring CommRing.toCommSemiring instConcreteCategoryHomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV Action.instConcreteCategoryHomSubtypeV instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRep	—	CategoryTheory.Functor.instFaithfulActionMapAction CategoryTheory.ObjectProperty.faithful_ι
instFiniteCarrierVFGModuleCat 📖	mathematical	—	Module.Finite FGModuleCat.carrier CommRing.toRing Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVFGModuleCat instModuleCarrierVFGModuleCat	—	FGModuleCat.instFiniteCarrier
instFiniteDimensionalCarrierVFGModuleCat 📖	mathematical	—	FiniteDimensional FGModuleCat.carrier CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Field.toDivisionRing instAddCommGroupCarrierVFGModuleCat instModuleCarrierVFGModuleCat	—	instFiniteCarrierVFGModuleCat
instFiniteDimensionalHom 📖	mathematical	—	FiniteDimensional Quiver.Hom FDRep DivisionRing.toRing Field.toDivisionRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instLargeCategory EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.Preadditive.homGroup instPreadditive CategoryTheory.Linear.homModule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring instLinear	—	FiniteDimensional.of_injective Action.forget₂_linear Action.forget₂_additive CategoryTheory.Functor.map_injective CategoryTheory.forget₂_faithful FGModuleCat.instFiniteHom
instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV 📖	mathematical	—	CategoryTheory.Functor.Full FDRep CommRing.toRing instLargeCategory Rep Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Action.HomSubtype FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat.isFG LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.FullSubcategory.concreteCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV CommSemiring.toSemiring CommRing.toCommSemiring instConcreteCategoryHomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV Action.instConcreteCategoryHomSubtypeV instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRep	—	CategoryTheory.Functor.instFullActionMapActionOfFaithful CategoryTheory.ObjectProperty.faithful_ι CategoryTheory.ObjectProperty.full_ι
instHasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits FDRep DivisionRing.toRing Field.toDivisionRing instLargeCategory EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Action.instHasFiniteLimits FGModuleCat.instHasFiniteLimits PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain
instHasKernels 📖	mathematical	—	CategoryTheory.Limits.HasKernels FDRep DivisionRing.toRing Field.toDivisionRing instLargeCategory EuclideanDomain.toCommRing Field.toEuclideanDomain Action.instHasZeroMorphisms FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Preadditive.fullSubcategory ModuleCat.instPreadditive	—	CategoryTheory.Limits.hasKernels_of_hasEqualizers Action.hasLimitsOfShape FGModuleCat.instHasLimitsOfShapeOfFinCategory PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain
instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits FDRep CommRing.toRing instLargeCategory Rep Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Action.HomSubtype FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat.isFG LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.FullSubcategory.concreteCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV CommSemiring.toSemiring CommRing.toCommSemiring instConcreteCategoryHomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV Action.instConcreteCategoryHomSubtypeV instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRep	—	Action.Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG FGModuleCat.instHasFiniteColimits
instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits FDRep CommRing.toRing instLargeCategory Rep Action.instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ Action.HomSubtype FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat.isFG LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.FullSubcategory.concreteCategory ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.V Action.instFunLikeHomSubtypeV CommSemiring.toSemiring CommRing.toCommSemiring instConcreteCategoryHomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV Action.instConcreteCategoryHomSubtypeV instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRep	—	Action.Functor.instPreservesFiniteLimitsMapActionOfHasFiniteLimits FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG FGModuleCat.instHasFiniteLimits
of_ρ 📖	mathematical	—	Action.ρ FGModuleCat CommRing.toRing CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG of MonoidHom.comp CategoryTheory.End CategoryTheory.Category.toCategoryStruct ModuleCat.of FGModuleCat.of MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CategoryTheory.Preadditive.instSemiringEnd ModuleCat.instPreadditive CategoryTheory.Preadditive.fullSubcategory MulEquiv.toMonoidHom MulEquiv.symm MulOne.toMul CategoryTheory.InducedCategory.endEquiv CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj LinearMap Ring.toSemiring RingHom.id ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Module.End.instSemiring RingEquiv.toMonoidHom RingEquiv.symm CategoryTheory.End.mul Module.End.instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CategoryTheory.Preadditive.instRingEnd LinearMap.instAdd ModuleCat.endRingEquiv	—	—
of_ρ' 📖	mathematical	—	ρ of	—	—

FDRep.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_ρ 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring FGModuleCat.carrier CommRing.toRing Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG AddCommGroup.toAddCommMonoid FDRep.instAddCommGroupCarrierVFGModuleCat FDRep.instModuleCarrierVFGModuleCat MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike FDRep.ρ LinearEquiv RingHomInvPair.ids Module.End LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.conj FDRep.isoToLinearEquiv	—	RingHomInvPair.ids smulCommClass_self FDRep.isoToLinearEquiv.eq_1 FDRep.hom_hom_action_ρ FGModuleCat.Iso.conj_hom_eq_conj CategoryTheory.Iso.conj_apply ModuleCat.hom_ofHom ModuleCat.hom_ext_iff Action.Hom.comm Action.inv_hom_hom_assoc

(root)

Definitions

Name	Category	Theorems
FDRep 📖	CompOp	24 math math: TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, FDRep.char_tensor, TannakaDuality.FiniteGroup.forget_obj, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, FDRep.instFiniteDimensionalHom, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, TannakaDuality.FiniteGroup.forget_map, FDRep.instHasKernels, FDRep.instInjectiveOfNeZeroCastCard, FDRep.simple_iff_end_is_rank_one, FDRep.forget₂_ρ, FDRep.char_orthonormal, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, FDRep.instHasFiniteLimits, FDRep.instProjectiveOfNeZeroCastCard, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, FDRep.scalar_product_char_eq_finrank_equivariant, TannakaDuality.FiniteGroup.equivHom_surjective, TannakaDuality.FiniteGroup.equivHom_injective, FDRep.dualTensorIsoLinHom_hom_hom, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, TannakaDuality.FiniteGroup.equivHom_apply, FDRep.simple_iff_char_is_norm_one, FDRep.finrank_hom_simple_simple

---

← Back to Index