Basic

📁 Source: Mathlib/Algebra/Category/FGModuleCat/Basic.lean

Statistics

Metric	Count
Definitions FGModuleCat, FGModuleCatCoevaluation, FGModuleCatDual, FGModuleCatEvaluation, carrier, exactPairing, fullyFaithfulULift, instInhabited, isoToLinearEquiv, of, ofHom, rightDual, rightRigidCategory, ulift, toFGModuleCatIso, isFG, instAddCommGroupCarrier, instCoeSortFGModuleCatType, instModuleCarrier	19
Theorems FGModuleCatCoevaluation_apply_one, FGModuleCatDual_coe, FGModuleCatDual_obj, FGModuleCatEvaluation_apply, FGModuleCatEvaluation_apply', conj_eq_conj, conj_hom_eq_conj, hom_comp, hom_ext, hom_ext_iff, hom_hom_comp, hom_hom_id, hom_id, ihom_obj, instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, instFaithfulUlift, instFiniteCarrier, instFiniteHom, instFiniteHomModuleCatObjIsFG, instFullModuleCatForget₂LinearMapIdCarrierObjIsFG, instFullUlift, instIsMonoidalClosedModuleCatIsFG, instIsMonoidalModuleCatIsFG, instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, obj_carrier, of_carrier, tensorObj_obj, tensorUnit_obj, toFGModuleCatIso_hom, toFGModuleCatIso_inv, comp_id_fgModuleCat, id_fgModuleCat_comp, isFG_iff, instFiniteCarrier, instFiniteCarrierObjModuleCatIsFG	35
Total	54

FGModuleCat

Definitions

Name	Category	Theorems
FGModuleCatCoevaluation 📖	CompOp	1 math math: FGModuleCatCoevaluation_apply_one
FGModuleCatDual 📖	CompOp	5 math math: FGModuleCatEvaluation_apply, FGModuleCatDual_obj, FGModuleCatCoevaluation_apply_one, FGModuleCatDual_coe, FGModuleCatEvaluation_apply'
FGModuleCatEvaluation 📖	CompOp	2 math math: FGModuleCatEvaluation_apply, FGModuleCatEvaluation_apply'
carrier 📖	CompOp	26 math math: LinearMap.comp_id_fgModuleCat, FGModuleCatEvaluation_apply, TannakaDuality.FiniteGroup.sumSMulInv_apply, FDRep.instFiniteDimensionalCarrierVFGModuleCat, instFiniteCarrier, FDRep.average_char_eq_finrank_invariants, FDRep.hom_hom_action_ρ, FGModuleCatDual_obj, obj_carrier, FGModuleCatCoevaluation_apply_one, TannakaDuality.FiniteGroup.equivApp_inv, TannakaDuality.FiniteGroup.equivApp_hom, FDRep.char_linHom, of_carrier, Iso.conj_eq_conj, FDRep.char_one, TannakaDuality.FiniteGroup.sumSMulInv_single_id, FGModuleCatDual_coe, instFiniteCarrier, FDRep.instFiniteCarrierVFGModuleCat, FDRep.Iso.conj_ρ, FDRep.char_dual, FGModuleCatEvaluation_apply', Iso.conj_hom_eq_conj, FDRep.hom_action_ρ, FDRep.dualTensorIsoLinHom_hom_hom
exactPairing 📖	CompOp	—
fullyFaithfulULift 📖	CompOp	—
instInhabited 📖	CompOp	—
isoToLinearEquiv 📖	CompOp	2 math math: Iso.conj_eq_conj, Iso.conj_hom_eq_conj
of 📖	CompOp	5 math math: ihom_obj, of_carrier, LinearEquiv.toFGModuleCatIso_hom, FDRep.of_ρ, LinearEquiv.toFGModuleCatIso_inv
ofHom 📖	CompOp	1 math math: Iso.conj_eq_conj
rightDual 📖	CompOp	—
rightRigidCategory 📖	CompOp	—
ulift 📖	CompOp	3 math math: instIsEquivalenceFGModuleCatUlift, instFullUlift, instFaithfulUlift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
FGModuleCatCoevaluation_apply_one 📖	mathematical	—	DFunLike.coe CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat DivisionRing.toRing Field.toDivisionRing ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.MonoidalCategoryStruct.tensorUnit FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory ModuleCat.monoidalCategory EuclideanDomain.toCommRing Field.toEuclideanDomain instIsMonoidalModuleCatIsFG CategoryTheory.MonoidalCategoryStruct.tensorObj FGModuleCatDual ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory FGModuleCatCoevaluation AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Finset.sum Set.Elem carrier Module.Basis.ofVectorSpaceIndex instAddCommGroupCarrier instModuleCarrier TensorProduct Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module CommSemiring.toSemiring Algebra.to_smulCommClass Algebra.id TensorProduct.addCommMonoid Finset.univ FiniteDimensional.instFintypeElemOfVectorSpaceIndex instFiniteCarrier TensorProduct.tmul Module.Basis Module.Basis.instFunLike Module.Basis.ofVectorSpace Module.Basis.coord	—	coevaluation_apply_one instFiniteCarrier
FGModuleCatDual_coe 📖	mathematical	—	carrier DivisionRing.toRing Field.toDivisionRing FGModuleCatDual Module.Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid instAddCommGroupCarrier instModuleCarrier	—	—
FGModuleCatDual_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat DivisionRing.toRing Field.toDivisionRing ModuleCat.moduleCategory ModuleCat.isFG FGModuleCatDual ModuleCat.of Module.Dual carrier DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid instAddCommGroupCarrier instModuleCarrier LinearMap.addCommGroup Ring.toAddCommGroup Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Ring.toSemiring Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	—	—
FGModuleCatEvaluation_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat DivisionRing.toRing Field.toDivisionRing ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.MonoidalCategoryStruct.tensorObj FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory ModuleCat.monoidalCategory EuclideanDomain.toCommRing Field.toEuclideanDomain instIsMonoidalModuleCatIsFG FGModuleCatDual CategoryTheory.MonoidalCategoryStruct.tensorUnit ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory FGModuleCatEvaluation TensorProduct.tmul CommRing.toCommSemiring CommRing.toRing AddHom.toFun carrier AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommGroupCarrier NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield LinearMap.toAddHom instModuleCarrier Semiring.toModule	—	contractLeft_apply
FGModuleCatEvaluation_apply' 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier DivisionRing.toRing Field.toDivisionRing CategoryTheory.MonoidalCategoryStruct.tensorObj ModuleCat ModuleCat.moduleCategory CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain ModuleCat.MonoidalCategory.instMonoidalCategoryStruct ModuleCat.of Module.Dual carrier AddCommGroup.toAddCommMonoid instAddCommGroupCarrier instModuleCarrier LinearMap.addCommGroup Ring.toAddCommGroup Semiring.toModule LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Ring.toSemiring Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isFG CategoryTheory.MonoidalCategoryStruct.tensorUnit ModuleCat.isAddCommGroup NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ModuleCat.instCommRingCarrierTensorUnit ModuleCat.isModule TensorProduct CommRing.toCommSemiring FGModuleCatDual LinearMap.instFunLike ModuleCat.Hom.hom FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory ModuleCat.monoidalCategory instIsMonoidalModuleCatIsFG CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory FGModuleCatEvaluation TensorProduct.tmul AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.toAddHom	—	contractLeft_apply
hom_comp 📖	mathematical	—	ModuleCat.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.comp FGModuleCat CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category LinearMap.comp ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	hom_hom_comp
hom_ext 📖	—	ModuleCat.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—	CategoryTheory.ObjectProperty.hom_ext ModuleCat.hom_ext
hom_ext_iff 📖	mathematical	—	ModuleCat.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	hom_ext
hom_hom_comp 📖	mathematical	—	ModuleCat.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.comp FGModuleCat CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category LinearMap.comp ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
hom_hom_id 📖	mathematical	—	ModuleCat.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.id FGModuleCat CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category LinearMap.id ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule	—	—
hom_id 📖	mathematical	—	ModuleCat.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.id FGModuleCat CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category LinearMap.id ModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule	—	hom_hom_id
ihom_obj 📖	mathematical	—	CategoryTheory.Functor.obj FGModuleCat DivisionRing.toRing Field.toDivisionRing CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.ihom CategoryTheory.ObjectProperty.fullMonoidalSubcategory ModuleCat.monoidalCategory EuclideanDomain.toCommRing Field.toEuclideanDomain instIsMonoidalModuleCatIsFG CategoryTheory.MonoidalClosed.closed CategoryTheory.ObjectProperty.fullMonoidalClosedSubcategory ModuleCat.instMonoidalClosed instIsMonoidalClosedModuleCatIsFG of Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.instAddCommGroupHom ModuleCat.Hom.instModule Ring.toSemiring ModuleCat.isModule smulCommClass_self ModuleCat.carrier CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Module.toDistribMulAction CommRing.toRing instFiniteHomModuleCatObjIsFG	—	instIsMonoidalModuleCatIsFG instIsMonoidalClosedModuleCatIsFG
instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG 📖	mathematical	—	CategoryTheory.Functor.Additive FGModuleCat CommRing.toRing ModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.Preadditive.fullSubcategory ModuleCat.instPreadditive CategoryTheory.forget₂ 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 CategoryTheory.FullSubcategory.hasForget₂	—	—
instFaithfulUlift 📖	mathematical	—	CategoryTheory.Functor.Faithful FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG ulift	—	CategoryTheory.Functor.FullyFaithful.faithful
instFiniteCarrier 📖	mathematical	—	Module.Finite carrier Ring.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrier instModuleCarrier	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instFiniteHom 📖	mathematical	—	Module.Finite Quiver.Hom FGModuleCat DivisionRing.toRing Field.toDivisionRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Preadditive.fullSubcategory ModuleCat.instPreadditive CategoryTheory.Linear.homModule CategoryTheory.Linear.fullSubcategory ModuleCat.instLinear EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Module.Finite.equiv smulCommClass_self instFiniteHomModuleCatObjIsFG RingHomInvPair.ids
instFiniteHomModuleCatObjIsFG 📖	mathematical	—	Module.Finite Quiver.Hom ModuleCat DivisionRing.toRing Field.toDivisionRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isFG DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid ModuleCat.instAddCommGroupHom ModuleCat.Hom.instModule ModuleCat.isModule smulCommClass_self ModuleCat.carrier CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ModuleCat.isAddCommGroup Module.toDistribMulAction Ring.toSemiring CommRing.toRing	—	Module.Finite.equiv smulCommClass_self Module.Finite.linearMap Module.Free.of_divisionRing instFiniteCarrier RingHomInvPair.ids
instFullModuleCatForget₂LinearMapIdCarrierObjIsFG 📖	mathematical	—	CategoryTheory.Functor.Full FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.forget₂ 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 CategoryTheory.FullSubcategory.hasForget₂	—	instFiniteCarrierObjModuleCatIsFG
instFullUlift 📖	mathematical	—	CategoryTheory.Functor.Full FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG ulift	—	CategoryTheory.Functor.FullyFaithful.full
instIsMonoidalClosedModuleCatIsFG 📖	mathematical	—	CategoryTheory.ObjectProperty.IsMonoidalClosed ModuleCat DivisionRing.toRing Field.toDivisionRing ModuleCat.moduleCategory ModuleCat.monoidalCategory EuclideanDomain.toCommRing Field.toEuclideanDomain ModuleCat.isFG ModuleCat.instMonoidalClosed	—	Module.Finite.equiv smulCommClass_self Module.Finite.linearMap Module.Free.of_divisionRing RingHomInvPair.ids
instIsMonoidalModuleCatIsFG 📖	mathematical	—	CategoryTheory.ObjectProperty.IsMonoidal ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory ModuleCat.isFG	—	Module.Finite.self Module.Finite.tensorProduct
instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring CommRing.toCommSemiring FGModuleCat CommRing.toRing ModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.Preadditive.fullSubcategory ModuleCat.instPreadditive CategoryTheory.Linear.fullSubcategory ModuleCat.instLinear CategoryTheory.forget₂ 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 CategoryTheory.FullSubcategory.hasForget₂	—	—
obj_carrier 📖	mathematical	—	ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG carrier	—	—
of_carrier 📖	mathematical	—	carrier of	—	—
tensorObj_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.MonoidalCategoryStruct.tensorObj FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory ModuleCat.monoidalCategory instIsMonoidalModuleCatIsFG ModuleCat.MonoidalCategory.instMonoidalCategoryStruct	—	instIsMonoidalModuleCatIsFG
tensorUnit_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.MonoidalCategoryStruct.tensorUnit FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory ModuleCat.monoidalCategory instIsMonoidalModuleCatIsFG ModuleCat.MonoidalCategory.instMonoidalCategoryStruct	—	instIsMonoidalModuleCatIsFG

FGModuleCat.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_eq_conj 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End FGModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike CategoryTheory.Iso.conj FGModuleCat.ofHom FGModuleCat.carrier instAddCommGroupCarrier instModuleCarrier FGModuleCat.instFiniteCarrier LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring RingHomInvPair.ids Module.End AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction DFinsupp.instEquivLikeLinearEquiv LinearEquiv.conj FGModuleCat.isoToLinearEquiv ModuleCat.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—
conj_hom_eq_conj 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory DFunLike.coe MulEquiv CategoryTheory.End FGModuleCat CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike CategoryTheory.Iso.conj LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring RingHomInvPair.ids Module.End FGModuleCat.carrier AddCommGroup.toAddCommMonoid instAddCommGroupCarrier instModuleCarrier LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction DFinsupp.instEquivLikeLinearEquiv LinearEquiv.conj FGModuleCat.isoToLinearEquiv	—	—

LinearEquiv

Definitions

Name	Category	Theorems
toFGModuleCatIso 📖	CompOp	2 math math: toFGModuleCatIso_hom, toFGModuleCatIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFGModuleCatIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG FGModuleCat.of toFGModuleCatIso CategoryTheory.ConcreteCategory.ofHom 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 toLinearMap	—	RingHomInvPair.ids
toFGModuleCatIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG FGModuleCat.of toFGModuleCatIso CategoryTheory.ConcreteCategory.ofHom 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 toLinearMap symm	—	RingHomInvPair.ids

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_id_fgModuleCat 📖	mathematical	—	comp ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG FGModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup instAddCommGroupCarrier ModuleCat.isModule instModuleCarrier RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ModuleCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.id FGModuleCat CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category	—	ModuleCat.hom_ext_iff CategoryTheory.Category.id_comp
id_fgModuleCat_comp 📖	mathematical	—	comp ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ModuleCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.CategoryStruct.id FGModuleCat CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category	—	ModuleCat.hom_ext_iff CategoryTheory.Category.comp_id

ModuleCat

Definitions

Name	Category	Theorems
isFG 📖	CompOp	76 math math: instEssentiallySmallFGModuleCat, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, LinearMap.id_fgModuleCat_comp, FDRep.char_tensor, FGModuleCat.hom_hom_id, FDRep.endRingEquiv_symm_comp_ρ, FGModuleCat.instHasColimitsOfShapeOfFinCategory, TannakaDuality.FiniteGroup.forget_obj, FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, LinearMap.comp_id_fgModuleCat, instIsEquivalenceFGModuleCatUlift, FGModuleCat.instFiniteHomModuleCatObjIsFG, isFG_iff, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, FGModuleCat.hom_comp, FGModuleCat.FGModuleCatEvaluation_apply, FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, FGModuleCat.instIsMonoidalClosedModuleCatIsFG, TannakaDuality.FiniteGroup.sumSMulInv_apply, FDRep.instFiniteDimensionalCarrierVFGModuleCat, FGModuleCat.instFiniteHom, FDRep.average_char_eq_finrank_invariants, FGModuleCat.hom_id, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, FDRep.hom_hom_action_ρ, FGModuleCat.FGModuleCatDual_obj, FGModuleCat.obj_carrier, FGModuleCat.FGModuleCatCoevaluation_apply_one, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, TannakaDuality.FiniteGroup.equivApp_inv, TannakaDuality.FiniteGroup.forget_map, FGModuleCat.ihom_obj, TannakaDuality.FiniteGroup.equivApp_hom, FDRep.char_linHom, FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, FGModuleRepr.instIsEquivalenceFGModuleCatEmbed, FGModuleCat.instHasFiniteColimits, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, FDRep.instHasKernels, FGModuleCat.Iso.conj_eq_conj, FGModuleCat.hom_hom_comp, FDRep.char_one, FGModuleCat.hom_ext_iff, TannakaDuality.FiniteGroup.sumSMulInv_single_id, FDRep.simple_iff_end_is_rank_one, FGModuleCat.instHasLimitsOfShapeOfFinCategory, FGModuleCat.instFullUlift, LinearEquiv.toFGModuleCatIso_hom, FGModuleCat.tensorObj_obj, FGModuleCat.tensorUnit_obj, FGModuleCat.instHasFiniteLimits, instFiniteCarrierObjModuleCatIsFG, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, FDRep.forget₂_ρ, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, FDRep.instFiniteCarrierVFGModuleCat, FDRep.Iso.conj_ρ, FDRep.of_ρ, FDRep.char_dual, FGModuleCat.FGModuleCatEvaluation_apply', FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, FGModuleCat.instFaithfulUlift, TannakaDuality.FiniteGroup.ofRightFDRep_hom, FGModuleCat.Iso.conj_hom_eq_conj, LinearEquiv.toFGModuleCatIso_inv, TannakaDuality.FiniteGroup.equivHom_surjective, TannakaDuality.FiniteGroup.equivHom_injective, FDRep.hom_action_ρ, FDRep.dualTensorIsoLinHom_hom_hom, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, FDRep.endRingEquiv_comp_ρ, TannakaDuality.FiniteGroup.equivHom_apply, FDRep.simple_iff_char_is_norm_one, FGModuleCat.instIsMonoidalModuleCatIsFG, FGModuleCat.instIsIsoCoimageImageComparison

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFG_iff 📖	mathematical	—	isFG Module.Finite carrier Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule	—	—

(root)

Definitions

Name	Category	Theorems
FGModuleCat 📖	CompOp	68 math math: instEssentiallySmallFGModuleCat, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, LinearMap.id_fgModuleCat_comp, FDRep.char_tensor, FGModuleCat.hom_hom_id, FDRep.endRingEquiv_symm_comp_ρ, FGModuleCat.instHasColimitsOfShapeOfFinCategory, TannakaDuality.FiniteGroup.forget_obj, FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, LinearMap.comp_id_fgModuleCat, instIsEquivalenceFGModuleCatUlift, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, FGModuleCat.hom_comp, FGModuleCat.FGModuleCatEvaluation_apply, FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, TannakaDuality.FiniteGroup.sumSMulInv_apply, FDRep.instFiniteDimensionalCarrierVFGModuleCat, FGModuleCat.instFiniteHom, FDRep.average_char_eq_finrank_invariants, FGModuleCat.hom_id, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, FDRep.hom_hom_action_ρ, FGModuleCat.FGModuleCatCoevaluation_apply_one, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, TannakaDuality.FiniteGroup.equivApp_inv, TannakaDuality.FiniteGroup.forget_map, FGModuleCat.ihom_obj, TannakaDuality.FiniteGroup.equivApp_hom, FDRep.char_linHom, FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, FGModuleRepr.instIsEquivalenceFGModuleCatEmbed, FGModuleCat.instHasFiniteColimits, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, FDRep.instHasKernels, FGModuleCat.Iso.conj_eq_conj, FGModuleCat.hom_hom_comp, FDRep.char_one, TannakaDuality.FiniteGroup.sumSMulInv_single_id, FDRep.simple_iff_end_is_rank_one, FGModuleCat.instHasLimitsOfShapeOfFinCategory, FGModuleCat.instFullUlift, LinearEquiv.toFGModuleCatIso_hom, FGModuleCat.tensorObj_obj, FGModuleCat.tensorUnit_obj, FGModuleCat.instHasFiniteLimits, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, FDRep.forget₂_ρ, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, FDRep.instFiniteCarrierVFGModuleCat, FDRep.Iso.conj_ρ, FDRep.of_ρ, FDRep.char_dual, FGModuleCat.FGModuleCatEvaluation_apply', FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, FGModuleCat.instFaithfulUlift, TannakaDuality.FiniteGroup.ofRightFDRep_hom, FGModuleCat.Iso.conj_hom_eq_conj, LinearEquiv.toFGModuleCatIso_inv, TannakaDuality.FiniteGroup.equivHom_surjective, TannakaDuality.FiniteGroup.equivHom_injective, FDRep.hom_action_ρ, FDRep.dualTensorIsoLinHom_hom_hom, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, FDRep.endRingEquiv_comp_ρ, TannakaDuality.FiniteGroup.equivHom_apply, FDRep.simple_iff_char_is_norm_one, FGModuleCat.instIsIsoCoimageImageComparison
instAddCommGroupCarrier 📖	CompOp	10 math math: LinearMap.comp_id_fgModuleCat, FGModuleCat.FGModuleCatEvaluation_apply, instFiniteCarrier, FGModuleCat.FGModuleCatDual_obj, FGModuleCat.FGModuleCatCoevaluation_apply_one, FGModuleCat.Iso.conj_eq_conj, FGModuleCat.FGModuleCatDual_coe, FGModuleCat.instFiniteCarrier, FGModuleCat.FGModuleCatEvaluation_apply', FGModuleCat.Iso.conj_hom_eq_conj
instCoeSortFGModuleCatType 📖	CompOp	—
instModuleCarrier 📖	CompOp	10 math math: LinearMap.comp_id_fgModuleCat, FGModuleCat.FGModuleCatEvaluation_apply, instFiniteCarrier, FGModuleCat.FGModuleCatDual_obj, FGModuleCat.FGModuleCatCoevaluation_apply_one, FGModuleCat.Iso.conj_eq_conj, FGModuleCat.FGModuleCatDual_coe, FGModuleCat.instFiniteCarrier, FGModuleCat.FGModuleCatEvaluation_apply', FGModuleCat.Iso.conj_hom_eq_conj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteCarrier 📖	mathematical	—	Module.Finite FGModuleCat.carrier Ring.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupCarrier instModuleCarrier	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instFiniteCarrierObjModuleCatIsFG 📖	mathematical	—	Module.Finite ModuleCat.carrier CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule	—	CategoryTheory.ObjectProperty.FullSubcategory.property

---

← Back to Index