Associator

📁 Source: Mathlib/CategoryTheory/Sums/Associator.lean

Statistics

Metric	Count
Definitions `associativity`, `associator`, `inlCompAssociator`, `inlCompInlCompAssociator`, `inlCompInrCompInverseAssociator`, `inlCompInverseAssociator`, `inrCompAssociator`, `inrCompInlCompAssociator`, `inrCompInrCompInverseAssociator`, `inrCompInverseAssociator`, `inverseAssociator`	11
Theorems `associativity_functor`, `associativity_inverse`, `associatorIsEquivalence`, `associator_map_inl_inl`, `associator_map_inl_inr`, `associator_map_inr`, `associator_obj_inl_inl`, `associator_obj_inl_inr`, `associator_obj_inr`, `inlCompAssociator_hom_app`, `inlCompAssociator_inv_app`, `inlCompInlCompAssociator_hom_app_down`, `inlCompInlCompAssociator_inv_app_down`, `inlCompInrCompInverseAssociator_hom_app_down_down`, `inlCompInrCompInverseAssociator_inv_app_down_down`, `inlCompInverseAssociator_hom_app_down_down`, `inlCompInverseAssociator_inv_app_down_down`, `inrCompAssociator_hom_app_down_down`, `inrCompAssociator_inv_app_down_down`, `inrCompInlCompAssociator_hom_app_down_down`, `inrCompInlCompAssociator_inv_app_down_down`, `inrCompInrCompInverseAssociator_hom_app_down`, `inrCompInrCompInverseAssociator_inv_app_down`, `inrCompInverseAssociator_hom_app`, `inrCompInverseAssociator_inv_app`, `inverseAssociatorIsEquivalence`, `inverseAssociator_map_inl`, `inverseAssociator_map_inr_inl`, `inverseAssociator_map_inr_inr`, `inverseAssociator_obj_inl`, `inverseAssociator_obj_inr_inl`, `inverseAssociator_obj_inr_inr`	32
Total	43

CategoryTheory.sum

Definitions

Name	Category	Theorems
`associativity` 📖	CompOp	8 math math: `associativity_inverse`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd`, `associativity_functor`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst`
`associator` 📖	CompOp	16 math math: `associator_obj_inr`, `associator_map_inr`, `associatorIsEquivalence`, `associativity_functor`, `associator_obj_inl_inl`, `inlCompAssociator_hom_app`, `inrCompInlCompAssociator_inv_app_down_down`, `inlCompInlCompAssociator_inv_app_down`, `inrCompAssociator_hom_app_down_down`, `inrCompInlCompAssociator_hom_app_down_down`, `inrCompAssociator_inv_app_down_down`, `associator_map_inl_inr`, `associator_obj_inl_inr`, `inlCompInlCompAssociator_hom_app_down`, `associator_map_inl_inl`, `inlCompAssociator_inv_app`
`inlCompAssociator` 📖	CompOp	2 math math: `inlCompAssociator_hom_app`, `inlCompAssociator_inv_app`
`inlCompInlCompAssociator` 📖	CompOp	2 math math: `inlCompInlCompAssociator_inv_app_down`, `inlCompInlCompAssociator_hom_app_down`
`inlCompInrCompInverseAssociator` 📖	CompOp	4 math math: `inlCompInrCompInverseAssociator_hom_app_down_down`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst`, `inlCompInrCompInverseAssociator_inv_app_down_down`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst`
`inlCompInverseAssociator` 📖	CompOp	4 math math: `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst`, `inlCompInverseAssociator_inv_app_down_down`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst`, `inlCompInverseAssociator_hom_app_down_down`
`inrCompAssociator` 📖	CompOp	2 math math: `inrCompAssociator_hom_app_down_down`, `inrCompAssociator_inv_app_down_down`
`inrCompInlCompAssociator` 📖	CompOp	2 math math: `inrCompInlCompAssociator_inv_app_down_down`, `inrCompInlCompAssociator_hom_app_down_down`
`inrCompInrCompInverseAssociator` 📖	CompOp	4 math math: `inrCompInrCompInverseAssociator_hom_app_down`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd`, `inrCompInrCompInverseAssociator_inv_app_down`
`inrCompInverseAssociator` 📖	CompOp	2 math math: `inrCompInverseAssociator_hom_app`, `inrCompInverseAssociator_inv_app`
`inverseAssociator` 📖	CompOp	22 math math: `inrCompInverseAssociator_hom_app`, `associativity_inverse`, `inlCompInrCompInverseAssociator_hom_app_down_down`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_fst`, `inrCompInrCompInverseAssociator_hom_app_down`, `inlCompInrCompInverseAssociator_inv_app_down_down`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_snd`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_snd_snd`, `inverseAssociator_map_inr_inr`, `inverseAssociator_obj_inr_inl`, `inverseAssociatorIsEquivalence`, `inverseAssociator_map_inl`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst`, `inrCompInrCompInverseAssociator_inv_app_down`, `inverseAssociator_obj_inr_inr`, `inverseAssociator_obj_inl`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst`, `inlCompInverseAssociator_inv_app_down_down`, `CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_fst`, `inverseAssociator_map_inr_inl`, `inlCompInverseAssociator_hom_app_down_down`, `inrCompInverseAssociator_inv_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associativity_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CategoryTheory.sum` `associativity` `associator`	—	—
`associativity_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `CategoryTheory.sum` `associativity` `inverseAssociator`	—	—
`associatorIsEquivalence` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `CategoryTheory.sum` `associator`	—	`CategoryTheory.Equivalence.isEquivalence_functor`
`associator_map_inl_inl` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.sum` `associator` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inl_`	—	—
`associator_map_inl_inr` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.sum` `associator` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inl_` `CategoryTheory.Sum.inr_`	—	—
`associator_map_inr` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.sum` `associator` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inr_`	—	—
`associator_obj_inl_inl` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.sum` `associator`	—	—
`associator_obj_inl_inr` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.sum` `associator`	—	—
`associator_obj_inr` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.sum` `associator`	—	—
`inlCompAssociator_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.sum` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inl_` `CategoryTheory.Functor.sum'` `CategoryTheory.Sum.inr_` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `associator` `inlCompAssociator` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`inlCompAssociator_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.sum` `CategoryTheory.Functor.sum'` `CategoryTheory.Sum.inl_` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inr_` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `associator` `inlCompAssociator` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`inlCompInlCompAssociator_hom_app_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.sum` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inl_` `associator` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inlCompInlCompAssociator` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`inlCompInlCompAssociator_inv_app_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.sum` `CategoryTheory.Sum.inl_` `CategoryTheory.Functor.comp` `associator` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inlCompInlCompAssociator` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`inlCompInrCompInverseAssociator_hom_app_down_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.sum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inr_` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inl_` `inverseAssociator` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inlCompInrCompInverseAssociator` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`inlCompInrCompInverseAssociator_inv_app_down_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.sum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inr_` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inl_` `inverseAssociator` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inlCompInrCompInverseAssociator` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`inlCompInverseAssociator_hom_app_down_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.sum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inl_` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.sum'` `CategoryTheory.Sum.inr_` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inverseAssociator` `inlCompInverseAssociator` `CategoryTheory.CategoryStruct.id`	—	—
`inlCompInverseAssociator_inv_app_down_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.sum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inl_` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.sum'` `CategoryTheory.Sum.inr_` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inverseAssociator` `inlCompInverseAssociator` `CategoryTheory.CategoryStruct.id`	—	—
`inrCompAssociator_hom_app_down_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.sum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inr_` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.sum'` `CategoryTheory.Sum.inl_` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `associator` `inrCompAssociator` `CategoryTheory.CategoryStruct.id`	—	—
`inrCompAssociator_inv_app_down_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.sum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inr_` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.sum'` `CategoryTheory.Sum.inl_` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `associator` `inrCompAssociator` `CategoryTheory.CategoryStruct.id`	—	—
`inrCompInlCompAssociator_hom_app_down_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.sum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inl_` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inr_` `associator` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inrCompInlCompAssociator` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`inrCompInlCompAssociator_inv_app_down_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.sum` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inl_` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inr_` `associator` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inrCompInlCompAssociator` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`inrCompInrCompInverseAssociator_hom_app_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.sum` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inr_` `inverseAssociator` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inrCompInrCompInverseAssociator` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`inrCompInrCompInverseAssociator_inv_app_down` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.NatTrans.app` `CategoryTheory.sum` `CategoryTheory.Sum.inr_` `CategoryTheory.Functor.comp` `inverseAssociator` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inrCompInrCompInverseAssociator` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`inrCompInverseAssociator_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.sum` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inr_` `CategoryTheory.Functor.sum'` `CategoryTheory.Sum.inl_` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inverseAssociator` `inrCompInverseAssociator` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`inrCompInverseAssociator_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.sum` `CategoryTheory.Functor.sum'` `CategoryTheory.Functor.comp` `CategoryTheory.Sum.inr_` `CategoryTheory.Sum.inl_` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `inverseAssociator` `inrCompInverseAssociator` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`inverseAssociatorIsEquivalence` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `CategoryTheory.sum` `inverseAssociator`	—	`CategoryTheory.Equivalence.isEquivalence_inverse`
`inverseAssociator_map_inl` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.sum` `inverseAssociator` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inl_`	—	—
`inverseAssociator_map_inr_inl` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.sum` `inverseAssociator` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inr_` `CategoryTheory.Sum.inl_`	—	—
`inverseAssociator_map_inr_inr` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.sum` `inverseAssociator` `CategoryTheory.Functor.obj` `CategoryTheory.Sum.inr_`	—	—
`inverseAssociator_obj_inl` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.sum` `inverseAssociator`	—	—
`inverseAssociator_obj_inr_inl` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.sum` `inverseAssociator`	—	—
`inverseAssociator_obj_inr_inr` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.sum` `inverseAssociator`	—	—

---

← Back to Index