Coinduced

📁 Source: Mathlib/RepresentationTheory/Coinduced.lean

Statistics

Metric	Count
Definitions coind, coind', coindFunctor, coindFunctor', coindFunctorIso, coindIso, coindMap, coindMap', coindVEquiv, resCoindAdjunction, resCoindHomEquiv, coind, coind', coindV	14
Theorems coind'_ext, coind'_ext_iff, coindFunctor'_map, coindFunctor'_obj, coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, coindFunctorIso_inv_app_hom_hom_apply_coe, coindFunctor_map, coindFunctor_obj, coindIso_hom_hom_hom, coindIso_inv_hom_hom, coindMap'_hom, coindMap_hom, coindVEquiv_apply_hom, coindVEquiv_symm_apply_coe, instIsLeftAdjointActionModuleCatRes, instIsRightAdjointCoindFunctor, instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, instPreservesProjectiveObjectsActionModuleCatSubtypeMemSubgroupResSubtype, resCoindAdjunction_counit_app_hom_hom, resCoindAdjunction_unit_app_hom_hom, resCoindHomEquiv_apply_hom, resCoindHomEquiv_symm_apply_hom, coe_coindV, coind'_apply_apply, coind_apply	25
Total	39

Rep

Definitions

Name	Category	Theorems
coind 📖	CompOp	22 math math: resCoindHomEquiv_symm_apply_hom, resCoindHomEquiv_apply_hom, coindResAdjunction_counit_app, coindToInd_of_support_subset_orbit, indCoindNatIso_hom_app, coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, indCoindIso_inv_hom_hom, indCoindIso_hom_hom_hom, coindResAdjunction_unit_app, coindToInd_apply, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, coindFunctorIso_inv_app_hom_hom_apply_coe, coindResAdjunction_homEquiv_apply, resIndAdjunction_counit_app, coindIso_inv_hom_hom, indCoindNatIso_inv_app, coindResAdjunction_homEquiv_symm_apply, coindMap_hom, resIndAdjunction_unit_app, coindFunctor_obj, coindIso_hom_hom_hom
coind' 📖	CompOp	6 math math: coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, coindMap'_hom, coindFunctorIso_inv_app_hom_hom_apply_coe, coindIso_inv_hom_hom, coindFunctor'_obj, coindIso_hom_hom_hom
coindFunctor 📖	CompOp	17 math math: coindResAdjunction_counit_app, resCoindAdjunction_counit_app_hom_hom, indCoindNatIso_hom_app, coindFunctor_map, instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, instIsRightAdjointCoindFunctor, resCoindAdjunction_unit_app_hom_hom, coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, coindResAdjunction_unit_app, coindFunctorIso_inv_app_hom_hom_apply_coe, coindResAdjunction_homEquiv_apply, resIndAdjunction_counit_app, indCoindNatIso_inv_app, coindResAdjunction_homEquiv_symm_apply, instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, resIndAdjunction_unit_app, coindFunctor_obj
coindFunctor' 📖	CompOp	4 math math: coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, coindFunctorIso_inv_app_hom_hom_apply_coe, coindFunctor'_obj, coindFunctor'_map
coindFunctorIso 📖	CompOp	2 math math: coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, coindFunctorIso_inv_app_hom_hom_apply_coe
coindIso 📖	CompOp	2 math math: coindIso_inv_hom_hom, coindIso_hom_hom_hom
coindMap 📖	CompOp	2 math math: coindFunctor_map, coindMap_hom
coindMap' 📖	CompOp	2 math math: coindMap'_hom, coindFunctor'_map
coindVEquiv 📖	CompOp	4 math math: coindVEquiv_symm_apply_coe, coindIso_inv_hom_hom, coindVEquiv_apply_hom, coindIso_hom_hom_hom
resCoindAdjunction 📖	CompOp	4 math math: resCoindAdjunction_counit_app_hom_hom, resCoindAdjunction_unit_app_hom_hom, resIndAdjunction_counit_app, resIndAdjunction_unit_app
resCoindHomEquiv 📖	CompOp	4 math math: resCoindHomEquiv_symm_apply_hom, resCoindHomEquiv_apply_hom, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coind'_ext 📖	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.res leftRegular ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	Action.Hom.ext ModuleCat.hom_ext Finsupp.lhom_ext' LinearMap.ext_ring RingHomCompTriple.ids
coind'_ext_iff 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.res leftRegular ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	coind'_ext
coindFunctor'_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory coindFunctor' coindMap'	—	—
coindFunctor'_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory coindFunctor' coind'	—	—
coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring ModuleCat.carrier Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Finsupp.module Semiring.toModule ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommGroup Ring.toAddCommGroup Action.Hom.hom ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.res leftRegular Submodule Pi.addCommMonoid Action.V instAddCommGroupCarrierVModuleCat Pi.Function.module SetLike.instMembership Submodule.setLike Representation.coindV ρ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Submodule.addCommGroup Pi.addCommGroup CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Submodule.module CategoryTheory.Linear.homModule instLinearRep coind coind' Rep coindFunctor coindFunctor' CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category coindFunctorIso Finsupp.sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
coindFunctorIso_inv_app_hom_hom_apply_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.coindV ρ DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Quiver.Hom Action CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res leftRegular CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Submodule.addCommGroup Pi.addCommGroup CategoryTheory.Linear.homModule instLinearRep Submodule.module LinearMap.instFunLike ModuleCat.Hom.hom coind' coind Action.Hom.hom Rep coindFunctor' coindFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category coindFunctorIso Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommGroup Ring.toAddCommGroup ModuleCat.isAddCommGroup Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
coindFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory coindFunctor coindMap	—	—
coindFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory coindFunctor coind	—	—
coindIso_hom_hom_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory coind coind' Action.Hom.hom CategoryTheory.Iso.hom Rep Action.instCategory coindIso LinearEquiv.toLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.coindV ρ Quiver.Hom Action CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Action.res leftRegular Submodule.addCommGroup Pi.addCommGroup CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Submodule.module CategoryTheory.Linear.homModule instLinearRep coindVEquiv	—	—
coindIso_inv_hom_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory coind' coind Action.Hom.hom CategoryTheory.Iso.inv Rep Action.instCategory coindIso LinearEquiv.toLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Quiver.Hom Action CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Action.res leftRegular Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.coindV ρ CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Submodule.addCommGroup Pi.addCommGroup CategoryTheory.Linear.homModule instLinearRep Submodule.module LinearEquiv.symm coindVEquiv	—	—
coindMap'_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory coind' coindMap' ModuleCat.ofHom Quiver.Hom Action CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res leftRegular CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule CommSemiring.toSemiring CommRing.toCommSemiring instLinearRep CategoryTheory.Linear.rightComp	—	—
coindMap_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory coind coindMap ModuleCat.ofHom Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.coindV ρ Submodule.addCommGroup Pi.addCommGroup Submodule.module LinearMap.restrict Ring.toSemiring ModuleCat.isAddCommGroup LinearMap.compLeft ModuleCat.Hom.hom	—	—
coindVEquiv_apply_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.res leftRegular DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule Pi.addCommMonoid ModuleCat.carrier Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.coindV ρ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Submodule.addCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Submodule.module CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike LinearEquiv.instEquivLike coindVEquiv ModuleCat.ofHom Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule ModuleCat.isAddCommGroup Finsupp.linearCombination Ring.toSemiring	—	RingHomInvPair.ids
coindVEquiv_symm_apply_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.coindV ρ DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Action CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res leftRegular CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive Submodule.addCommMonoid CategoryTheory.Linear.homModule instLinearRep Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm coindVEquiv CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier Action.Hom.hom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomInvPair.ids
instIsLeftAdjointActionModuleCatRes 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Action ModuleCat CommRing.toRing ModuleCat.moduleCategory Action.instCategory Action.res	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointCoindFunctor 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Rep CommRing.toRing Action.instCategory ModuleCat ModuleCat.moduleCategory coindFunctor	—	CategoryTheory.Adjunction.isRightAdjoint
instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Action.instCategory ModuleCat ModuleCat.moduleCategory coindFunctor Subgroup.subtype	—	epi_iff_surjective QuotientGroup.rightRel_apply Quotient.eq' mul_inv_rev mul_inv_cancel_left SubgroupClass.toInvMemClass Subgroup.instSubgroupClass mul_assoc MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass hom_comm_apply inv_mul_cancel_right Quotient.mk'_surjective
instPreservesProjectiveObjectsActionModuleCatSubtypeMemSubgroupResSubtype 📖	mathematical	—	CategoryTheory.Functor.PreservesProjectiveObjects Action ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Action.res Subgroup.subtype	—	CategoryTheory.Functor.preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype
resCoindAdjunction_counit_app_hom_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule Action.Hom.hom ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.res coindFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Adjunction.counit resCoindAdjunction LinearMap.comp Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.Function.module SetLike.instMembership Submodule.setLike Representation.coindV ρ Ring.toSemiring Submodule.addCommGroup Pi.addCommGroup Submodule.module RingHom.id Semiring.toNonAssocSemiring LinearMap.proj MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Submodule.subtype	—	—
resCoindAdjunction_unit_app_hom_hom 📖	mathematical	—	ModuleCat.Hom.hom CommRing.toRing ModuleCat.of ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.res AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVModuleCat Pi.Function.module SetLike.instMembership Submodule.setLike Representation.coindV ρ Submodule.addCommGroup Pi.addCommGroup Submodule.module Action.Hom.hom coindFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit resCoindAdjunction LinearMap.codRestrict Ring.toSemiring Pi.module RingHom.id Semiring.toNonAssocSemiring MonoidHom.comp LinearMap MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearMap.pi DFunLike.coe Representation MonoidHom.instFunLike CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
resCoindHomEquiv_apply_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory coind DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Action CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res Rep AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike LinearEquiv.instEquivLike resCoindHomEquiv ModuleCat.ofHom ModuleCat.carrier Submodule Pi.addCommMonoid Action.V instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.coindV ρ ModuleCat.isAddCommGroup Submodule.addCommGroup Pi.addCommGroup Submodule.module LinearMap.codRestrict Ring.toSemiring Pi.module LinearMap.pi LinearMap.comp ModuleCat.Hom.hom Representation LinearMap MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	RingHomInvPair.ids
resCoindHomEquiv_symm_apply_hom 📖	mathematical	—	Action.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.obj Action Action.instCategory Action.res DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct coind AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm resCoindHomEquiv ModuleCat.ofHom ModuleCat.carrier ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.comp Ring.toSemiring Pi.addCommMonoid Action.V instAddCommGroupCarrierVModuleCat Pi.Function.module LinearMap.proj MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Submodule SetLike.instMembership Submodule.setLike Representation.coindV ρ Submodule.addCommMonoid Submodule.module Submodule.subtype ModuleCat.Hom.hom	—	RingHomInvPair.ids

Representation

Definitions

Name	Category	Theorems
coind 📖	CompOp	1 math math: coind_apply
coind' 📖	CompOp	1 math math: coind'_apply_apply
coindV 📖	CompOp	14 math math: Rep.resCoindHomEquiv_symm_apply_hom, Rep.resCoindHomEquiv_apply_hom, Rep.resCoindAdjunction_counit_app_hom_hom, Rep.resCoindAdjunction_unit_app_hom_hom, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, Rep.coindVEquiv_symm_apply_coe, coe_coindV, Rep.coindToInd_apply, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, Rep.coindIso_inv_hom_hom, Rep.coindVEquiv_apply_hom, Rep.coindMap_hom, coind_apply, Rep.coindIso_hom_hom_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_coindV 📖	mathematical	—	SetLike.coe Submodule CommSemiring.toSemiring Pi.addCommMonoid Pi.Function.module Submodule.setLike coindV setOf	—	—
coind'_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Quiver.Hom Action ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory CategoryTheory.Functor.obj Action.res Rep.leftRegular AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive ModuleCat.instPreadditive CategoryTheory.Linear.homModule instLinearRep LinearMap.instFunLike MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike coind' CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map LinearEquiv ModuleCat.carrier Action.V Rep Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm Rep.leftRegularHomEquiv Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
coind_apply 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Submodule Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike coindV Submodule.addCommMonoid Submodule.module MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike coind LinearMap.restrict LinearMap.funLeft MulOne.toMul	—	—

---

← Back to Index