Documentation Verification Report

Tannaka

📁 Source: Mathlib/RepresentationTheory/Tannaka.lean

Statistics

Metric	Count
Definitions `algHomOfRightFDRepComp`, `equiv`, `equivApp`, `equivHom`, `forget`, `instMonoidalFDRepFGModuleCatForget₂HomSubtypeLinearMapIdCarrierObjModuleCatIsFGV`, `leftRegular`, `leftRegularFDRepHom`, `mulRepHom`, `ofRightFDRep`, `rightFDRep`, `rightRegular`, `sumSMulInv`	13
Theorems `equivApp_hom`, `equivApp_inv`, `equivHom_apply`, `equivHom_injective`, `equivHom_surjective`, `forget_map`, `forget_obj`, `leftRegular_apply`, `map_mul_toRightFDRepComp`, `ofRightFDRep_hom`, `rightRegular_apply`, `sumSMulInv_apply`, `sumSMulInv_single_id`, `toRightFDRepComp_in_rightRegular`, `toRightFDRepComp_injective`	15
Total	28

TannakaDuality.FiniteGroup

Definitions

Name	Category	Theorems
`algHomOfRightFDRepComp` 📖	CompOp	—
`equiv` 📖	CompOp	—
`equivApp` 📖	CompOp	3 math math: `equivApp_inv`, `equivApp_hom`, `equivHom_apply`
`equivHom` 📖	CompOp	3 math math: `equivHom_surjective`, `equivHom_injective`, `equivHom_apply`
`forget` 📖	CompOp	7 math math: `toRightFDRepComp_in_rightRegular`, `forget_obj`, `forget_map`, `map_mul_toRightFDRepComp`, `equivHom_surjective`, `equivHom_injective`, `equivHom_apply`
`instMonoidalFDRepFGModuleCatForget₂HomSubtypeLinearMapIdCarrierObjModuleCatIsFGV` 📖	CompOp	—
`leftRegular` 📖	CompOp	1 math math: `leftRegular_apply`
`leftRegularFDRepHom` 📖	CompOp	—
`mulRepHom` 📖	CompOp	—
`ofRightFDRep` 📖	CompOp	1 math math: `ofRightFDRep_hom`
`rightFDRep` 📖	CompOp	3 math math: `toRightFDRepComp_in_rightRegular`, `map_mul_toRightFDRepComp`, `ofRightFDRep_hom`
`rightRegular` 📖	CompOp	2 math math: `toRightFDRepComp_in_rightRegular`, `rightRegular_apply`
`sumSMulInv` 📖	CompOp	2 math math: `sumSMulInv_apply`, `ofRightFDRep_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivApp_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `FGModuleCat` `CommRing.toRing` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `Action.V` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `equivApp` `CategoryTheory.InducedCategory.homMk` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `ModuleCat.ofHom` `ModuleCat.carrier` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `DFunLike.coe` `MonoidHom` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `FGModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `FDRep.instAddCommGroupCarrierVFGModuleCat` `FDRep.instModuleCarrierVFGModuleCat` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `FDRep.ρ`	—	—
`equivApp_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `FGModuleCat` `CommRing.toRing` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `Action.V` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `equivApp` `CategoryTheory.InducedCategory.homMk` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `ModuleCat.ofHom` `ModuleCat.carrier` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `DFunLike.coe` `MonoidHom` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `FGModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `FDRep.instAddCommGroupCarrierVFGModuleCat` `FDRep.instModuleCarrierVFGModuleCat` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `FDRep.ρ` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`equivHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CategoryTheory.Aut` `CategoryTheory.LaxMonoidalFunctor` `FDRep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FDRep.instLargeCategory` `Action.instMonoidalCategory` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.ObjectProperty.fullMonoidalSubcategory` `ModuleCat.monoidalCategory` `FGModuleCat.instIsMonoidalModuleCatIsFG` `CategoryTheory.LaxMonoidalFunctor.instCategory` `forget` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `equivHom` `CategoryTheory.LaxMonoidalFunctor.isoOfComponents` `equivApp`	—	`FGModuleCat.instIsMonoidalModuleCatIsFG`
`equivHom_injective` 📖	mathematical	—	`CategoryTheory.Aut` `CategoryTheory.LaxMonoidalFunctor` `FDRep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FDRep.instLargeCategory` `Action.instMonoidalCategory` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.ObjectProperty.fullMonoidalSubcategory` `ModuleCat.monoidalCategory` `FGModuleCat.instIsMonoidalModuleCatIsFG` `CategoryTheory.LaxMonoidalFunctor.instCategory` `forget` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `equivHom`	—	`FGModuleCat.instIsMonoidalModuleCatIsFG` `Pi.single_apply` `one_mul` `NeZero.one`
`equivHom_surjective` 📖	mathematical	—	`CategoryTheory.Aut` `CategoryTheory.LaxMonoidalFunctor` `FDRep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FDRep.instLargeCategory` `Action.instMonoidalCategory` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.ObjectProperty.fullMonoidalSubcategory` `ModuleCat.monoidalCategory` `FGModuleCat.instIsMonoidalModuleCatIsFG` `CategoryTheory.LaxMonoidalFunctor.instCategory` `forget` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `equivHom`	—	`FGModuleCat.instIsMonoidalModuleCatIsFG` `toRightFDRepComp_in_rightRegular` `toRightFDRepComp_injective` `CategoryTheory.InducedCategory.hom_ext` `ModuleCat.hom_ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `FDRep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FDRep.instLargeCategory` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.LaxMonoidalFunctor.toFunctor` `Action.instMonoidalCategory` `CategoryTheory.ObjectProperty.fullMonoidalSubcategory` `ModuleCat.monoidalCategory` `FGModuleCat.instIsMonoidalModuleCatIsFG` `forget` `Action.Hom.hom`	—	`FGModuleCat.instIsMonoidalModuleCatIsFG`
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `FDRep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FDRep.instLargeCategory` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.LaxMonoidalFunctor.toFunctor` `Action.instMonoidalCategory` `CategoryTheory.ObjectProperty.fullMonoidalSubcategory` `ModuleCat.monoidalCategory` `FGModuleCat.instIsMonoidalModuleCatIsFG` `forget` `Action.V`	—	`FGModuleCat.instIsMonoidalModuleCatIsFG`
`leftRegular_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Representation` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `leftRegular` `MulOne.toMul` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`map_mul_toRightFDRepComp` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `ModuleCat.Hom.hom` `CommRing.toRing` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.Functor.obj` `FDRep` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FDRep.instLargeCategory` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.LaxMonoidalFunctor.toFunctor` `Action.instMonoidalCategory` `CategoryTheory.ObjectProperty.fullMonoidalSubcategory` `ModuleCat.monoidalCategory` `FGModuleCat.instIsMonoidalModuleCatIsFG` `forget` `rightFDRep` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.NatTrans.app` `CategoryTheory.LaxMonoidalFunctor.Hom.hom` `CategoryTheory.Iso.hom` `CategoryTheory.LaxMonoidalFunctor` `CategoryTheory.LaxMonoidalFunctor.instCategory` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`FGModuleCat.instIsMonoidalModuleCatIsFG` `CategoryTheory.NatTrans.naturality` `CategoryTheory.NatTrans.IsMonoidal.tensor` `CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal` `CategoryTheory.ConcreteCategory.congr_hom` `CategoryTheory.Functor.congr_map`
`ofRightFDRep_hom` 📖	mathematical	—	`Action.Hom.hom` `FGModuleCat` `CommRing.toRing` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `rightFDRep` `ofRightFDRep` `CategoryTheory.InducedCategory.homMk` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `Action.V` `ModuleCat.ofHom` `ModuleCat.carrier` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `sumSMulInv`	—	—
`rightRegular_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Representation` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `rightRegular` `MulOne.toMul`	—	—
`sumSMulInv_apply` 📖	mathematical	—	`DFunLike.coe` `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` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `FDRep.instAddCommGroupCarrierVFGModuleCat` `Pi.Function.module` `Semiring.toModule` `FDRep.instModuleCarrierVFGModuleCat` `LinearMap.instFunLike` `sumSMulInv` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `FDRep.ρ` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`sumSMulInv_single_id` 📖	mathematical	—	`Finset.sum` `FGModuleCat.carrier` `CommRing.toRing` `Action.V` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddCommGroup.toAddCommMonoid` `FDRep.instAddCommGroupCarrierVFGModuleCat` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `FDRep.instModuleCarrierVFGModuleCat` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `FDRep.ρ` `InvOneClass.toInv`	—	`Fintype.sum_single_smul` `inv_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `one_smul`
`toRightFDRepComp_in_rightRegular` 📖	mathematical	—	`ModuleCat.Hom.hom` `CommRing.toRing` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.Functor.obj` `FDRep` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FDRep.instLargeCategory` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.LaxMonoidalFunctor.toFunctor` `Action.instMonoidalCategory` `CategoryTheory.ObjectProperty.fullMonoidalSubcategory` `ModuleCat.monoidalCategory` `FGModuleCat.instIsMonoidalModuleCatIsFG` `forget` `rightFDRep` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.NatTrans.app` `CategoryTheory.LaxMonoidalFunctor.Hom.hom` `CategoryTheory.Iso.hom` `CategoryTheory.LaxMonoidalFunctor` `CategoryTheory.LaxMonoidalFunctor.instCategory` `DFunLike.coe` `Representation` `CommRing.toCommSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `CommSemiring.toSemiring` `Semiring.toModule` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `rightRegular`	—	`FGModuleCat.instIsMonoidalModuleCatIsFG` `AlgHom.eq_piEvalAlgHom` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial` `Module.Basis.ext` `CategoryTheory.NatTrans.naturality` `Pi.basisFun_apply` `inv_inv` `mul_one` `Pi.single_apply` `Pi.single_eq_same` `Pi.single_eq_of_ne'`
`toRightFDRepComp_injective` 📖	—	`CategoryTheory.NatTrans.app` `FDRep` `CommRing.toRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `FDRep.instLargeCategory` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.LaxMonoidalFunctor.toFunctor` `Action.instMonoidalCategory` `CategoryTheory.ObjectProperty.fullMonoidalSubcategory` `ModuleCat.monoidalCategory` `FGModuleCat.instIsMonoidalModuleCatIsFG` `forget` `CategoryTheory.LaxMonoidalFunctor.Hom.hom` `CategoryTheory.Iso.hom` `CategoryTheory.LaxMonoidalFunctor` `CategoryTheory.LaxMonoidalFunctor.instCategory` `rightFDRep`	—	—	`FGModuleCat.instIsMonoidalModuleCatIsFG` `CategoryTheory.Aut.ext` `CategoryTheory.LaxMonoidalFunctor.hom_ext` `CategoryTheory.NatTrans.ext'` `FGModuleCat.hom_ext` `LinearMap.ext` `CategoryTheory.NatTrans.naturality` `Fintype.sum_single_smul` `inv_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidHom.instMonoidHomClass` `one_smul`

---

← Back to Index