FDRep

📁 Source: Mathlib/RepresentationTheory/FDRep.lean

Statistics

Metric	Count
Definitions FDRep, dualTensorIsoLinHom, dualTensorIsoLinHomAux, forget₂HomLinearEquiv, instCoeSortType, instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRepIntertwiningMapVρ, isoToLinearEquiv, of, ρ	9
Theorems conj_ρ, dualTensorIsoLinHom_hom_hom, endRingEquiv_comp_ρ, endRingEquiv_symm_comp_ρ, finrank_hom_simple_simple, forget₂_ρ, hom_action_ρ, hom_hom_action_ρ, instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, instFiniteDimensionalHom, instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, instHasKernels, instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, of_ρ, of_ρ'	16
Total	25

FDRep

Definitions

Name	Category	Theorems
dualTensorIsoLinHom 📖	CompOp	1 math math: dualTensorIsoLinHom_hom_hom
dualTensorIsoLinHomAux 📖	CompOp	—
forget₂HomLinearEquiv 📖	CompOp	—
instCoeSortType 📖	CompOp	—
instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRepIntertwiningMapVρ 📖	CompOp	5 math math: instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, forget₂_ρ, instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ
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 Action.instCategory 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 ModuleCat.isAddCommGroup CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction FGModuleCat.instFiniteCarrier Representation.linHom ρ CategoryTheory.Iso.hom dualTensorIsoLinHom CategoryTheory.ConcreteCategory.ofHom Ring.toSemiring ModuleCat.carrier 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 FGModuleCat.instFiniteCarrier
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 Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive CategoryTheory.Preadditive.fullSubcategory ModuleCat.instPreadditive CategoryTheory.Linear.homModule Action.instLinear CategoryTheory.Linear.fullSubcategory ModuleCat.instLinear EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.Iso	—	CategoryTheory.finrank_hom_simple_simple instHasKernels instFiniteDimensionalHom
forget₂_ρ 📖	mathematical	—	Rep.ρ CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.obj FDRep CommRing.toRing Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Rep Rep.instCategory CategoryTheory.forget₂ Action.HomSubtype 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 Action.instConcreteCategoryHomSubtypeV Representation.IntertwiningMap Rep.V Rep.hV1 Rep.hV2 Representation.IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRepIntertwiningMapVρ ρ	—	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 ModuleCat.isAddCommGroup ModuleCat.isModule 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 ModuleCat.isAddCommGroup ModuleCat.isModule MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ	—	—
instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ 📖	mathematical	—	CategoryTheory.Functor.Faithful FDRep CommRing.toRing Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Rep CommSemiring.toSemiring CommRing.toCommSemiring Rep.instCategory CategoryTheory.forget₂ Action.HomSubtype 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 Action.instConcreteCategoryHomSubtypeV Representation.IntertwiningMap Rep.V Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRepIntertwiningMapVρ	—	CategoryTheory.Functor.Faithful.comp CategoryTheory.Functor.instFaithfulActionMapAction CategoryTheory.ObjectProperty.faithful_ι CategoryTheory.Functor.IsEquivalence.faithful Rep.instIsEquivalenceActionModuleCatActionToRep
instFiniteDimensionalHom 📖	mathematical	—	FiniteDimensional Quiver.Hom FDRep DivisionRing.toRing Field.toDivisionRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.Preadditive.homGroup Action.instPreadditive CategoryTheory.Preadditive.fullSubcategory ModuleCat.instPreadditive CategoryTheory.Linear.homModule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Action.instLinear CategoryTheory.Linear.fullSubcategory ModuleCat.instLinear EuclideanDomain.toCommRing Field.toEuclideanDomain	—	FiniteDimensional.of_injective Action.forget₂_linear Action.forget₂_additive CategoryTheory.Functor.map_injective CategoryTheory.forget₂_faithful FGModuleCat.instFiniteHom
instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ 📖	mathematical	—	CategoryTheory.Functor.Full FDRep CommRing.toRing Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Rep CommSemiring.toSemiring CommRing.toCommSemiring Rep.instCategory CategoryTheory.forget₂ Action.HomSubtype 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 Action.instConcreteCategoryHomSubtypeV Representation.IntertwiningMap Rep.V Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRepIntertwiningMapVρ	—	CategoryTheory.Functor.Full.comp CategoryTheory.Functor.instFullActionMapActionOfFaithful CategoryTheory.ObjectProperty.faithful_ι CategoryTheory.ObjectProperty.full_ι CategoryTheory.Functor.IsEquivalence.full Rep.instIsEquivalenceActionModuleCatActionToRep
instHasKernels 📖	mathematical	—	CategoryTheory.Limits.HasKernels FDRep DivisionRing.toRing Field.toDivisionRing Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Action.instHasZeroMorphisms CategoryTheory.ObjectProperty.instHasZeroMorphismsFullSubcategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive	—	CategoryTheory.Limits.hasKernels_of_hasEqualizers Action.hasLimitsOfShape FGModuleCat.instHasLimitsOfShapeOfFinCategory PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain
instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteColimits FDRep CommRing.toRing Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Rep CommSemiring.toSemiring CommRing.toCommSemiring Rep.instCategory CategoryTheory.forget₂ Action.HomSubtype 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 Action.instConcreteCategoryHomSubtypeV Representation.IntertwiningMap Rep.V Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRepIntertwiningMapVρ	—	CategoryTheory.Limits.comp_preservesFiniteColimits Action.Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG FGModuleCat.instHasFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence Rep.instIsEquivalenceActionModuleCatActionToRep
instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits FDRep CommRing.toRing Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Rep CommSemiring.toSemiring CommRing.toCommSemiring Rep.instCategory CategoryTheory.forget₂ Action.HomSubtype 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 Action.instConcreteCategoryHomSubtypeV Representation.IntertwiningMap Rep.V Rep.hV1 Rep.hV2 Rep.ρ Representation.IntertwiningMap.instFunLike Rep.instConcreteCategoryIntertwiningMapVρ instHasForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVRepIntertwiningMapVρ	—	CategoryTheory.Limits.comp_preservesFiniteLimits Action.Functor.instPreservesFiniteLimitsMapActionOfHasFiniteLimits FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG FGModuleCat.instHasFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence Rep.instIsEquivalenceActionModuleCatActionToRep
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 ModuleCat.isAddCommGroup CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isModule 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	23 math math: TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, FDRep.char_tensor, TannakaDuality.FiniteGroup.forget_obj, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FDRep.instFiniteDimensionalHom, TannakaDuality.FiniteGroup.forget_map, FDRep.instHasKernels, FDRep.instInjectiveOfNeZeroCastCard, FDRep.simple_iff_end_is_rank_one, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FDRep.forget₂_ρ, FDRep.char_orthonormal, FDRep.instProjectiveOfNeZeroCastCard, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, FDRep.scalar_product_char_eq_finrank_equivariant, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, TannakaDuality.FiniteGroup.equivHom_surjective, TannakaDuality.FiniteGroup.equivHom_injective, FDRep.dualTensorIsoLinHom_hom_hom, TannakaDuality.FiniteGroup.equivHom_apply, FDRep.simple_iff_char_is_norm_one, FDRep.finrank_hom_simple_simple

---

← Back to Index