End

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/End.lean

Statistics

Metric	Count
Definitions End, Cowedge, desc, ext, mk, HasCoend, HasEnd, Wedge, ext, mk, coend, desc, map, ι, coendFunctor, endFunctor, end_, map, π, multicospanIndexEnd, multicospanShapeEnd, multispanIndexCoend, multispanShapeCoend	23
Theorems hom_ext, π_desc, π_desc_assoc, condition, condition_assoc, ext_hom_hom, ext_inv_hom, mk_pt, mk_π, hom_ext, lift_ι, lift_ι_assoc, condition, condition_assoc, ext_hom_hom, ext_inv_hom, mk_pt, mk_ι, condition, condition_assoc, hom_ext, hom_ext_iff, map_comp, map_comp_assoc, map_id, ι_desc, ι_desc_assoc, ι_map, ι_map_assoc, coendFunctor_map, coendFunctor_obj, endFunctor_map, endFunctor_obj, condition, condition_assoc, hom_ext, hom_ext_iff, lift_π, lift_π_assoc, map_comp, map_comp_assoc, map_id, map_π, map_π_assoc, multicospanIndexEnd_fst, multicospanIndexEnd_left, multicospanIndexEnd_right, multicospanIndexEnd_snd, multicospanShapeEnd_L, multicospanShapeEnd_R, multicospanShapeEnd_fst, multicospanShapeEnd_snd, multispanIndexCoend_fst, multispanIndexCoend_left, multispanIndexCoend_right, multispanIndexCoend_snd, multispanShapeCoend_L, multispanShapeCoend_R, multispanShapeCoend_fst, multispanShapeCoend_snd	60
Total	83

CategoryTheory

Definitions

Name	Category	Theorems
End 📖	CompOp	138 math math: IsGrothendieckAbelian.GabrielPopescuAux.ι_d, preadditiveCoyonedaObj_map, Rep.coe_linearization_obj_ρ, additive_yonedaObj, Action.leftRegularTensorIso_inv_hom, Monoid.Foldl.ofFreeMonoid_apply, Action.ofMulAction_apply, InducedCategory.endEquiv_symm_apply_hom, InducedCategory.endEquiv_apply, FDRep.endRingEquiv_symm_comp_ρ, PreGaloisCategory.endEquivSectionsFibers_π, Preadditive.homSelfLinearEquivEndMulOpposite_apply, Iso.refl_conj, preadditiveYonedaObj_obj_carrier, Traversable.foldlm.ofFreeMonoid_comp_of, Action.rightDual_ρ, Rep.linearization_single, Iso.conj_pow, End.mul_def, ModuleCat.endRingEquiv_symm_apply_hom, IsGrothendieckAbelian.GabrielPopescu.full, IsFreeGroupoid.SpanningTree.endIsFree, End.smul_left, IsFreeGroupoid.SpanningTree.functorOfMonoidHom_map, Rep.ρ_hom, HomOrthogonal.matrixDecomposition_id, Action.FunctorCategoryEquivalence.functor_map_app, ModuleCat.smul_naturality, ContinuousCohomology.I_obj_ρ_apply, Aut.toEnd_apply, preadditiveYoneda_obj, preadditiveYonedaMap_app, isSeparator_iff_faithful_preadditiveCoyonedaObj, ContinuousCohomology.Iobj_ρ_apply, isUnit_iff_isIso, Functor.map_conj, IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d, Abelian.full_comp_preadditiveCoyonedaObj, preadditiveYonedaObj_obj_isModule, Action.tensorUnit_ρ, Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj', FDRep.hom_hom_action_ρ, Functor.mapAction_obj_ρ_apply, Action.FintypeCat.toEndHom_apply, IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects, SingleObj.functor_map, SingleObj.toEnd_def, HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, preservesFiniteColimits_preadditiveYonedaObj_of_injective, Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply, Functor.FullyFaithful.mulEquivEnd_symm_apply, Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj, HomOrthogonal.matrixDecompositionLinearEquiv_apply, ModuleCat.smulNatTrans_apply_app, preservesFiniteColimits_preadditiveCoyonedaObj_of_projective, Units.toAut_hom, Traversable.foldl.unop_ofFreeMonoid, Action.leftRegularTensorIso_hom_hom, preservesHomology_preadditiveCoyonedaObj_of_projective, HomOrthogonal.matrixDecomposition_comp, Action.FintypeCat.quotientToEndHom_mk, PreGaloisCategory.FibreFunctor.end_isUnit, Monoid.foldlM.ofFreeMonoid_apply, preservesLimits_preadditiveYonedaObj, Action.res_map_hom, Rep.linearization_obj_ρ, FGModuleCat.Iso.conj_eq_conj, ModuleCat.HasColimit.coconePointSMul_apply, Action.ρ_self_inv_apply, Rep.linearizationTrivialIso_inv_hom, Action.ρ_one, Action.ρAut_apply_hom, End.smul_right, Action.trivial_ρ, Action.Hom.comm_assoc, preservesHomology_preadditiveYonedaObj_of_injective, SemimoduleCat.Iso.conj_eq_conj, HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, ModuleCat.mkOfSMul_smul, preadditiveYonedaObj_obj_isAddCommGroup, IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d, Iso.symm_self_conj, PreGaloisCategory.endEquivAutGalois_mul, Functor.mapEnd_apply, Action.res_obj_ρ, Preadditive.homSelfLinearEquivEndMulOpposite_symm_apply, End.one_def, isCoseparator_iff_faithful_preadditiveYonedaObj, Rep.ofHom_ρ, Action.FunctorCategoryEquivalence.inverse_map_hom, Rep.Action_ρ_eq_ρ, Abelian.preadditiveCoyonedaObj_map_surjective, Iso.self_symm_conj, Units.toAut_inv, IsFreeGroupoid.endIsFreeOfConnectedFree, Iso.conjAut_hom, ModuleCat.Iso.conj_eq_conj, Traversable.foldl.ofFreeMonoid_comp_of, Iso.conj_id, ActionCategory.stabilizerIsoEnd_apply, Action.tensor_ρ, IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj, Iso.trans_conj, FDRep.of_ρ, PreGaloisCategory.endEquivAutGalois_π, Action.isContinuous_def, Functor.mapAction_map_hom, IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits, Functor.FullyFaithful.mulEquivEnd_apply, preadditiveCoyonedaObj_obj_carrier, Action.leftDual_ρ, HomOrthogonal.matrixDecompositionAddEquiv_apply, Iso.conj_comp, preadditiveCoyonedaObj_obj_isModule, Action.Iso.conj_ρ, preservesLimits_preadditiveCoyonedaObj, ModuleCat.endRingEquiv_apply, Rep.linearizationTrivialIso_hom_hom, additive_coyonedaObj, IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc, Rep.ihom_obj_ρ, instNontrivialEndOfSimple, FGModuleCat.Iso.conj_hom_eq_conj, Action.FunctorCategoryEquivalence.functor_obj_map, Action.ρAut_apply_inv, Action.Hom.comm, Action.ρ_inv_self_apply, preadditiveCoyoneda_obj, preadditiveCoyonedaObj_obj_isAddCommGroup, Iso.conj_apply, FDRep.hom_action_ρ, PreGaloisCategory.endMulEquivAutGalois_pi, ActionCategory.stabilizerIsoEnd_symm_apply, FDRep.endRingEquiv_comp_ρ, IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj, Action.FintypeCat.toEndHom_trivial_of_mem, Action.FintypeCat.ofMulAction_apply, preadditiveYonedaObj_map

CategoryTheory.Limits

Definitions

Name	Category	Theorems
Cowedge 📖	CompOp	2 math math: Cowedge.ext_hom_hom, Cowedge.ext_inv_hom
HasCoend 📖	MathDef	—
HasEnd 📖	MathDef	—
Wedge 📖	CompOp	2 math math: Wedge.ext_hom_hom, Wedge.ext_inv_hom
coend 📖	CompOp	11 math math: coend.map_id, coend.condition, coend.map_comp_assoc, coend.condition_assoc, coendFunctor_obj, coend.ι_desc, coend.map_comp, coend.ι_map, coend.hom_ext_iff, coend.ι_map_assoc, coend.ι_desc_assoc
coendFunctor 📖	CompOp	2 math math: coendFunctor_obj, coendFunctor_map
endFunctor 📖	CompOp	2 math math: endFunctor_obj, endFunctor_map
end_ 📖	CompOp	13 math math: end_.map_π, end_.condition, endFunctor_obj, CategoryTheory.Enriched.FunctorCategory.enrichedComp_π_assoc, end_.map_id, end_.hom_ext_iff, end_.map_comp, end_.lift_π, end_.map_comp_assoc, end_.map_π_assoc, CategoryTheory.Enriched.FunctorCategory.enrichedComp_π, end_.lift_π_assoc, end_.condition_assoc
multicospanIndexEnd 📖	CompOp	12 math math: multicospanIndexEnd_fst, Wedge.mk_pt, Wedge.mk_ι, multicospanIndexEnd_snd, multicospanIndexEnd_right, Wedge.IsLimit.lift_ι, Wedge.ext_hom_hom, Wedge.condition, Wedge.IsLimit.lift_ι_assoc, Wedge.ext_inv_hom, multicospanIndexEnd_left, Wedge.condition_assoc
multicospanShapeEnd 📖	CompOp	16 math math: multicospanShapeEnd_L, multicospanIndexEnd_fst, Wedge.mk_pt, Wedge.mk_ι, multicospanIndexEnd_snd, multicospanIndexEnd_right, multicospanShapeEnd_snd, Wedge.IsLimit.lift_ι, Wedge.ext_hom_hom, multicospanShapeEnd_fst, Wedge.condition, Wedge.IsLimit.lift_ι_assoc, multicospanShapeEnd_R, Wedge.ext_inv_hom, multicospanIndexEnd_left, Wedge.condition_assoc
multispanIndexCoend 📖	CompOp	12 math math: multispanIndexCoend_right, Cowedge.IsColimit.π_desc_assoc, Cowedge.IsColimit.π_desc, Cowedge.condition_assoc, multispanIndexCoend_snd, Cowedge.ext_hom_hom, Cowedge.mk_pt, multispanIndexCoend_left, Cowedge.mk_π, Cowedge.ext_inv_hom, multispanIndexCoend_fst, Cowedge.condition
multispanShapeCoend 📖	CompOp	16 math math: multispanIndexCoend_right, Cowedge.IsColimit.π_desc_assoc, multispanShapeCoend_snd, Cowedge.IsColimit.π_desc, Cowedge.condition_assoc, multispanIndexCoend_snd, Cowedge.ext_hom_hom, Cowedge.mk_pt, multispanIndexCoend_left, Cowedge.mk_π, multispanShapeCoend_fst, Cowedge.ext_inv_hom, multispanShapeCoend_L, multispanIndexCoend_fst, multispanShapeCoend_R, Cowedge.condition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coendFunctor_map 📖	mathematical	HasCoend	CategoryTheory.Functor.map CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category coendFunctor coend.map	—	—
coendFunctor_obj 📖	mathematical	HasCoend	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category coendFunctor coend	—	—
endFunctor_map 📖	mathematical	HasEnd	CategoryTheory.Functor.map CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category endFunctor end_.map	—	—
endFunctor_obj 📖	mathematical	HasEnd	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category endFunctor end_	—	—
multicospanIndexEnd_fst 📖	mathematical	—	MulticospanIndex.fst multicospanShapeEnd multicospanIndexEnd CategoryTheory.Functor.map CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.left CategoryTheory.Functor.id MulticospanShape.fst CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
multicospanIndexEnd_left 📖	mathematical	—	MulticospanIndex.left multicospanShapeEnd multicospanIndexEnd CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op	—	—
multicospanIndexEnd_right 📖	mathematical	—	MulticospanIndex.right multicospanShapeEnd multicospanIndexEnd CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right	—	—
multicospanIndexEnd_snd 📖	mathematical	—	MulticospanIndex.snd multicospanShapeEnd multicospanIndexEnd CategoryTheory.NatTrans.app CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom	—	—
multicospanShapeEnd_L 📖	mathematical	—	MulticospanShape.L multicospanShapeEnd	—	—
multicospanShapeEnd_R 📖	mathematical	—	MulticospanShape.R multicospanShapeEnd CategoryTheory.Arrow	—	—
multicospanShapeEnd_fst 📖	mathematical	—	MulticospanShape.fst multicospanShapeEnd CategoryTheory.Comma.left CategoryTheory.Functor.id	—	—
multicospanShapeEnd_snd 📖	mathematical	—	MulticospanShape.snd multicospanShapeEnd CategoryTheory.Comma.right CategoryTheory.Functor.id	—	—
multispanIndexCoend_fst 📖	mathematical	—	MultispanIndex.fst multispanShapeCoend multispanIndexCoend CategoryTheory.NatTrans.app CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.hom	—	—
multispanIndexCoend_left 📖	mathematical	—	MultispanIndex.left multispanShapeCoend multispanIndexCoend CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left	—	—
multispanIndexCoend_right 📖	mathematical	—	MultispanIndex.right multispanShapeCoend multispanIndexCoend CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op	—	—
multispanIndexCoend_snd 📖	mathematical	—	MultispanIndex.snd multispanShapeCoend multispanIndexCoend CategoryTheory.Functor.map CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left MultispanShape.snd CategoryTheory.Comma.hom	—	—
multispanShapeCoend_L 📖	mathematical	—	MultispanShape.L multispanShapeCoend CategoryTheory.Arrow	—	—
multispanShapeCoend_R 📖	mathematical	—	MultispanShape.R multispanShapeCoend	—	—
multispanShapeCoend_fst 📖	mathematical	—	MultispanShape.fst multispanShapeCoend CategoryTheory.Comma.left CategoryTheory.Functor.id	—	—
multispanShapeCoend_snd 📖	mathematical	—	MultispanShape.snd multispanShapeCoend CategoryTheory.Comma.right CategoryTheory.Functor.id	—	—

CategoryTheory.Limits.Cowedge

Definitions

Name	Category	Theorems
ext 📖	CompOp	2 math math: ext_hom_hom, ext_inv_hom
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.multispanShapeCoend CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.multispanIndexCoend CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.Multicofork.π	—	CategoryTheory.Limits.Multicofork.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.multispanShapeCoend CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.multispanIndexCoend CategoryTheory.Limits.Multicofork.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
ext_hom_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.multispanShapeCoend CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.multispanIndexCoend CategoryTheory.Iso.hom CategoryTheory.Limits.Cowedge CategoryTheory.Limits.Cocone.category ext CategoryTheory.Limits.Cocone.pt	—	—
ext_inv_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.multispanShapeCoend CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.multispanIndexCoend CategoryTheory.Iso.inv CategoryTheory.Limits.Cowedge CategoryTheory.Limits.Cocone.category ext CategoryTheory.Limits.Cocone.pt	—	—
mk_pt 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.multispanShapeCoend CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.multispanIndexCoend	—	—
mk_π 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.Multicofork.π CategoryTheory.Limits.multispanShapeCoend CategoryTheory.Limits.multispanIndexCoend	—	—

CategoryTheory.Limits.Cowedge.IsColimit

Definitions

Name	Category	Theorems
desc 📖	CompOp	2 math math: π_desc_assoc, π_desc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.multispanShapeCoend CategoryTheory.Limits.multispanIndexCoend CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.Multicofork.π	—	—	CategoryTheory.Limits.Multicofork.IsColimit.hom_ext
π_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.multispanShapeCoend CategoryTheory.Limits.multispanIndexCoend CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.Multicofork.π desc	—	CategoryTheory.Limits.IsColimit.fac
π_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.MultispanIndex.right CategoryTheory.Limits.multispanShapeCoend CategoryTheory.Limits.multispanIndexCoend CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingMultispan CategoryTheory.Limits.WalkingMultispan.instSmallCategory CategoryTheory.Limits.MultispanIndex.multispan CategoryTheory.Limits.Multicofork.π desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_desc

CategoryTheory.Limits.Wedge

Definitions

Name	Category	Theorems
ext 📖	CompOp	2 math math: ext_hom_hom, ext_inv_hom
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.multicospanShapeEnd CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.Limits.multicospanIndexEnd CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Limits.Multifork.ι CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Limits.Multifork.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.multicospanShapeEnd CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.Limits.multicospanIndexEnd CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.Limits.Multifork.ι CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
ext_hom_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.multicospanShapeEnd CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.Limits.multicospanIndexEnd CategoryTheory.Iso.hom CategoryTheory.Limits.Wedge CategoryTheory.Limits.Cone.category ext CategoryTheory.Limits.Cone.pt	—	—
ext_inv_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.multicospanShapeEnd CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.Limits.multicospanIndexEnd CategoryTheory.Iso.inv CategoryTheory.Limits.Wedge CategoryTheory.Limits.Cone.category ext CategoryTheory.Limits.Cone.pt	—	—
mk_pt 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.multicospanShapeEnd CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.Limits.multicospanIndexEnd	—	—
mk_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.Multifork.ι CategoryTheory.Limits.multicospanShapeEnd CategoryTheory.Limits.multicospanIndexEnd	—	—

CategoryTheory.Limits.Wedge.IsLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.multicospanShapeEnd CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.Limits.multicospanIndexEnd CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.Limits.Multifork.ι	—	—	CategoryTheory.Limits.Multifork.IsLimit.hom_ext
lift_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.multicospanShapeEnd CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.Limits.multicospanIndexEnd CategoryTheory.Limits.MulticospanIndex.left lift CategoryTheory.Limits.Multifork.ι	—	CategoryTheory.Limits.IsLimit.fac
lift_ι_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.multicospanShapeEnd CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.Limits.multicospanIndexEnd lift CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.Limits.Multifork.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_ι

CategoryTheory.Limits.coend

Definitions

Name	Category	Theorems
desc 📖	CompOp	2 math math: ι_desc, ι_desc_assoc
map 📖	CompOp	6 math math: map_id, map_comp_assoc, map_comp, ι_map, ι_map_assoc, CategoryTheory.Limits.coendFunctor_map
ι 📖	CompOp	7 math math: condition, condition_assoc, ι_desc, ι_map, hom_ext_iff, ι_map_assoc, ι_desc_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Limits.coend CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver ι	—	CategoryTheory.Limits.Cowedge.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.coend ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Limits.coend ι	—	—	CategoryTheory.Limits.Multicoequalizer.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Limits.coend ι	—	hom_ext
map_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coend map CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category	—	hom_ext ι_map_assoc ι_map CategoryTheory.Category.assoc
map_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coend map CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coend	—	hom_ext ι_map CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
ι_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.coend ι desc	—	CategoryTheory.Limits.IsColimit.fac
ι_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.coend ι desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_desc
ι_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Limits.coend ι map CategoryTheory.NatTrans.app	—	ι_desc
ι_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Limits.coend ι map CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_map

CategoryTheory.Limits.end_

Definitions

Name	Category	Theorems
map 📖	CompOp	6 math math: map_π, map_id, map_comp, map_comp_assoc, map_π_assoc, CategoryTheory.Limits.endFunctor_map
π 📖	CompOp	11 math math: map_π, CategoryTheory.Enriched.FunctorCategory.enrichedId_π_assoc, condition, CategoryTheory.Enriched.FunctorCategory.enrichedComp_π_assoc, hom_ext_iff, lift_π, map_π_assoc, CategoryTheory.Enriched.FunctorCategory.enrichedComp_π, CategoryTheory.Enriched.FunctorCategory.enrichedId_π, lift_π_assoc, condition_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.end_ CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op π CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Limits.Wedge.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.end_ CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op π CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.end_ CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op π	—	—	CategoryTheory.Limits.Multiequalizer.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.end_ CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op π	—	hom_ext
lift_π 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.end_ lift π	—	CategoryTheory.Limits.IsLimit.fac
lift_π_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op CategoryTheory.Functor.map CategoryTheory.NatTrans.app Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Limits.end_ lift π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_π
map_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.end_ map CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category	—	hom_ext CategoryTheory.Category.assoc map_π map_π_assoc
map_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.end_ map CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.end_	—	hom_ext map_π CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
map_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.end_ CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op map π CategoryTheory.NatTrans.app	—	lift_π
map_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.end_ map CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category Opposite.op π CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_π

---

← Back to Index