Coinduced

📁 Source: Mathlib/RepresentationTheory/Coinduced.lean

Statistics

Metric	Count
Definitions coind, coind', coindFunctor, coindFunctor', coindFunctorIso, coindIso, coindMap, coindMap', coindVEquiv, resCoindAdjunction, resCoindHomEquiv, resCoindToHom, coind, coind', coindMap, coindV	16
Theorems coind'_ext, coind'_ext_iff, coindFunctor'_map, coindFunctor'_obj, coindFunctorIso_hom_app_hom_toFun_hom_toFun, coindFunctorIso_inv_app_hom_toFun_coe, coindFunctor_map, coindFunctor_obj, coindVEquiv_apply, coindVEquiv_symm_apply_coe, instIsLeftAdjointResFunctor, instIsRightAdjointCoindFunctor, instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, instPreservesProjectiveObjectsSubtypeMemSubgroupResFunctorSubtype, resCoindHomEquiv_apply, resCoindHomEquiv_symm_apply, resCoindToHom_hom_apply_coe, coe_coindV, coind'_apply_apply, coindMap_coe_apply, coindMap_coe_apply_apply, coind_apply, mem_coindV	23
Total	39

Rep

Definitions

Name	Category	Theorems
coind 📖	CompOp	20 math math: coindResAdjunction_counit_app, resCoindToHom_hom_apply_coe, coindToInd_of_support_subset_orbit, indCoindNatIso_hom_app, coindToInd_indToCoind, coindResAdjunction_unit_app, coindToInd_apply, resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, resCoindHomEquiv_symm_apply, coindResAdjunction_homEquiv_apply, resIndAdjunction_counit_app, indCoindNatIso_inv_app, coindResAdjunction_homEquiv_symm_apply, indCoindIso_hom_hom_toLinearMap, indCoindIso_inv_hom_toLinearMap, resCoindHomEquiv_apply, resIndAdjunction_unit_app, indToCoind_coindToInd, coindFunctor_obj
coind' 📖	CompOp	1 math math: coindFunctor'_obj
coindFunctor 📖	CompOp	15 math math: coindResAdjunction_counit_app, indCoindNatIso_hom_app, coindFunctor_map, instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, instIsRightAdjointCoindFunctor, coindFunctorIso_inv_app_hom_toFun_coe, coindResAdjunction_unit_app, coindResAdjunction_homEquiv_apply, resIndAdjunction_counit_app, indCoindNatIso_inv_app, coindResAdjunction_homEquiv_symm_apply, instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, resIndAdjunction_unit_app, coindFunctor_obj, coindFunctorIso_hom_app_hom_toFun_hom_toFun
coindFunctor' 📖	CompOp	4 math math: coindFunctorIso_inv_app_hom_toFun_coe, coindFunctor'_obj, coindFunctor'_map, coindFunctorIso_hom_app_hom_toFun_hom_toFun
coindFunctorIso 📖	CompOp	2 math math: coindFunctorIso_inv_app_hom_toFun_coe, coindFunctorIso_hom_app_hom_toFun_hom_toFun
coindIso 📖	CompOp	—
coindMap 📖	CompOp	1 math math: coindFunctor_map
coindMap' 📖	CompOp	1 math math: coindFunctor'_map
coindVEquiv 📖	CompOp	2 math math: coindVEquiv_symm_apply_coe, coindVEquiv_apply
resCoindAdjunction 📖	CompOp	2 math math: resIndAdjunction_counit_app, resIndAdjunction_unit_app
resCoindHomEquiv 📖	CompOp	4 math math: resIndAdjunction_homEquiv_symm_apply, resIndAdjunction_homEquiv_apply, resCoindHomEquiv_symm_apply, resCoindHomEquiv_apply
resCoindToHom 📖	CompOp	2 math math: resCoindToHom_hom_apply_coe, resCoindHomEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coind'_ext 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring V res leftRegular CommRing.toRing AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap.instFunLike Representation.IntertwiningMap.toLinearMap ρ Hom.hom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Ring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	hom_ext Representation.IntertwiningMap.ext Finsupp.lhom_ext' LinearMap.ext_ring RingHomCompTriple.ids
coind'_ext_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring V res leftRegular CommRing.toRing AddCommGroup.toAddCommMonoid hV1 hV2 LinearMap.instFunLike Representation.IntertwiningMap.toLinearMap ρ Hom.hom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Ring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	coind'_ext
coindFunctor'_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory coindFunctor' coindMap'	—	—
coindFunctor'_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory coindFunctor' coind'	—	—
coindFunctorIso_hom_app_hom_toFun_hom_toFun 📖	mathematical	—	DFunLike.coe Representation.IntertwiningMap V CommSemiring.toSemiring CommRing.toCommSemiring leftRegular CommRing.toRing AddCommGroup.toAddCommMonoid hV1 hV2 MonoidHom.comp LinearMap RingHom.id Semiring.toNonAssocSemiring MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ Representation.IntertwiningMap.instFunLike Hom.hom of Submodule Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike Representation.coindV Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory res Submodule.addCommGroup Pi.addCommGroup instAddCommGroupHom Submodule.module instModuleHom Representation.coind Representation.coind' CategoryTheory.Functor.obj coindFunctor coindFunctor' CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category coindFunctorIso Finsupp.sum AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
coindFunctorIso_inv_app_hom_toFun_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid V AddCommGroup.toAddCommMonoid hV1 Pi.Function.module hV2 SetLike.instMembership Submodule.setLike Representation.coindV ρ DFunLike.coe Representation.IntertwiningMap Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory res leftRegular CommRing.toRing instAddCommGroupHom Submodule.addCommGroup Pi.addCommGroup instModuleHom Submodule.module Representation.coind' Representation.coind Representation.IntertwiningMap.instFunLike Hom.hom CategoryTheory.Functor.obj coindFunctor' coindFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category coindFunctorIso Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring MonoidHom.comp LinearMap RingHom.id MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Representation.ofMulAction Monoid.toMulAction Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
coindFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory coindFunctor coindMap	—	—
coindFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory coindFunctor coind	—	—
coindVEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule Pi.addCommMonoid V AddCommGroup.toAddCommMonoid hV1 Pi.Function.module hV2 SetLike.instMembership Submodule.setLike Representation.coindV ρ Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory res leftRegular CommRing.toRing Submodule.addCommMonoid instAddCommGroupHom Submodule.module instModuleHom EquivLike.toFunLike LinearEquiv.instEquivLike coindVEquiv ofHom MonoidHom.comp LinearMap MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Finsupp.linearCombination	—	RingHomInvPair.ids
coindVEquiv_symm_apply_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid V AddCommGroup.toAddCommMonoid hV1 Pi.Function.module hV2 SetLike.instMembership Submodule.setLike Representation.coindV ρ DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory res leftRegular CommRing.toRing instAddCommGroupHom Submodule.addCommMonoid instModuleHom Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm coindVEquiv LinearMap LinearMap.instFunLike Representation.IntertwiningMap.toLinearMap Hom.hom Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Ring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomInvPair.ids
instIsLeftAdjointResFunctor 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory resFunctor	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointCoindFunctor 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint Rep CommSemiring.toSemiring CommRing.toCommSemiring instCategory coindFunctor	—	CategoryTheory.Adjunction.isRightAdjoint
instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms Rep Subgroup SetLike.instMembership Subgroup.instSetLike CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup instCategory 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
instPreservesProjectiveObjectsSubtypeMemSubgroupResFunctorSubtype 📖	mathematical	—	CategoryTheory.Functor.PreservesProjectiveObjects Rep CommSemiring.toSemiring CommRing.toCommSemiring DivInvMonoid.toMonoid Group.toDivInvMonoid instCategory Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup resFunctor Subgroup.subtype	—	CategoryTheory.Functor.preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype
resCoindHomEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory res coind AddCommGroup.toAddCommMonoid instAddCommGroupHom instModuleHom EquivLike.toFunLike LinearEquiv.instEquivLike resCoindHomEquiv resCoindToHom	—	RingHomInvPair.ids
resCoindHomEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory coind res AddCommGroup.toAddCommMonoid instAddCommGroupHom instModuleHom EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm resCoindHomEquiv ofHom V hV1 hV2 MonoidHom.comp LinearMap MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring ρ LinearMap.comp Pi.addCommMonoid Pi.Function.module LinearMap.proj MulOne.toOne Submodule SetLike.instMembership Submodule.setLike Representation.coindV Submodule.addCommMonoid Submodule.module Submodule.subtype Representation.IntertwiningMap.toLinearMap Hom.hom	—	RingHomInvPair.ids
resCoindToHom_hom_apply_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid V AddCommGroup.toAddCommMonoid hV1 Pi.Function.module hV2 SetLike.instMembership Submodule.setLike Representation.coindV ρ DFunLike.coe coind Representation.IntertwiningMap.instFunLike Hom.hom resCoindToHom Representation.IntertwiningMap res LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—

Representation

Definitions

Name	Category	Theorems
coind 📖	CompOp	7 math math: Rep.coindFunctorIso_inv_app_hom_toFun_coe, coindMap_coe_apply_apply, Rep.indCoindIso_hom_hom_toLinearMap, Rep.indCoindIso_inv_hom_toLinearMap, coind_apply, coindMap_coe_apply, Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun
coind' 📖	CompOp	3 math math: Rep.coindFunctorIso_inv_app_hom_toFun_coe, coind'_apply_apply, Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun
coindMap 📖	CompOp	2 math math: coindMap_coe_apply_apply, coindMap_coe_apply
coindV 📖	CompOp	17 math math: Rep.resCoindToHom_hom_apply_coe, Rep.coindToInd_of_support_subset_orbit, Rep.coindToInd_indToCoind, Rep.coindVEquiv_symm_apply_coe, Rep.coindFunctorIso_inv_app_hom_toFun_coe, coe_coindV, Rep.coindToInd_apply, Rep.resCoindHomEquiv_symm_apply, Rep.coindVEquiv_apply, coindMap_coe_apply_apply, Rep.indCoindIso_hom_hom_toLinearMap, Rep.indCoindIso_inv_hom_toLinearMap, mem_coindV, coind_apply, Rep.indToCoind_coindToInd, coindMap_coe_apply, Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_coindV 📖	mathematical	—	SetLike.coe Submodule 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 Rep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Rep.instCategory Rep.res Rep.leftRegular CommRing.toRing AddCommGroup.toAddCommMonoid Rep.instAddCommGroupHom Rep.instModuleHom LinearMap.instFunLike MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike coind' CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj Rep.resFunctor CategoryTheory.Functor.map Rep.V Ring.toSemiring Rep.hV1 Rep.hV2 LinearEquiv.toLinearMap LinearEquiv.symm Rep.leftRegularHomEquiv Finsupp.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
coindMap_coe_apply 📖	mathematical	—	Submodule Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike coindV DFunLike.coe IntertwiningMap Submodule.addCommMonoid Submodule.module coind IntertwiningMap.instFunLike coindMap LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.compLeft IntertwiningMap.toLinearMap	—	—
coindMap_coe_apply_apply 📖	mathematical	—	Submodule Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike coindV DFunLike.coe IntertwiningMap Submodule.addCommMonoid Submodule.module coind IntertwiningMap.instFunLike coindMap	—	—
coind_apply 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap 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	—	—
mem_coindV 📖	mathematical	—	Submodule Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike coindV MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DFunLike.coe MonoidHom MonoidHom.instFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	—

---

← Back to Index