Assoc

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean

Statistics

Metric	Count
Definitions `pullbackAssoc`, `pullbackAssocIsPullback`, `pullbackAssocSymmIsPullback`, `pullbackPullbackLeftIsPullback`, `pullbackPullbackRightIsPullback`, `pushoutAssoc`, `pushoutAssocIsPushout`, `pushoutAssocSymmIsPushout`, `pushoutPushoutLeftIsPushout`, `pushoutPushoutRightIsPushout`	10
Theorems `hasPullback_assoc`, `hasPullback_assoc_symm`, `hasPushout_assoc`, `hasPushout_assoc_symm`, `inl_inl_pushoutAssoc_hom`, `inl_inl_pushoutAssoc_hom_assoc`, `inl_inr_pushoutAssoc_inv`, `inl_inr_pushoutAssoc_inv_assoc`, `inl_pushoutAssoc_inv`, `inl_pushoutAssoc_inv_assoc`, `inr_inl_pushoutAssoc_hom`, `inr_inl_pushoutAssoc_hom_assoc`, `inr_inr_pushoutAssoc_inv`, `inr_inr_pushoutAssoc_inv_assoc`, `inr_pushoutAssoc_hom`, `inr_pushoutAssoc_hom_assoc`, `pullbackAssoc_hom_fst`, `pullbackAssoc_hom_fst_assoc`, `pullbackAssoc_hom_snd_fst`, `pullbackAssoc_hom_snd_fst_assoc`, `pullbackAssoc_hom_snd_snd`, `pullbackAssoc_hom_snd_snd_assoc`, `pullbackAssoc_inv_fst_fst`, `pullbackAssoc_inv_fst_fst_assoc`, `pullbackAssoc_inv_fst_snd`, `pullbackAssoc_inv_fst_snd_assoc`, `pullbackAssoc_inv_snd`, `pullbackAssoc_inv_snd_assoc`	28
Total	38

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`pullbackAssoc` 📖	CompOp	12 math math: `pullbackAssoc_hom_snd_fst_assoc`, `pullbackAssoc_inv_fst_snd`, `pullbackAssoc_inv_fst_snd_assoc`, `pullbackAssoc_hom_snd_snd`, `pullbackAssoc_hom_snd_fst`, `pullbackAssoc_hom_snd_snd_assoc`, `pullbackAssoc_inv_snd_assoc`, `pullbackAssoc_hom_fst`, `pullbackAssoc_inv_snd`, `pullbackAssoc_inv_fst_fst_assoc`, `pullbackAssoc_hom_fst_assoc`, `pullbackAssoc_inv_fst_fst`
`pullbackAssocIsPullback` 📖	CompOp	—
`pullbackAssocSymmIsPullback` 📖	CompOp	—
`pullbackPullbackLeftIsPullback` 📖	CompOp	—
`pullbackPullbackRightIsPullback` 📖	CompOp	—
`pushoutAssoc` 📖	CompOp	12 math math: `inl_inr_pushoutAssoc_inv_assoc`, `inl_pushoutAssoc_inv_assoc`, `inr_pushoutAssoc_hom_assoc`, `inr_pushoutAssoc_hom`, `inl_inl_pushoutAssoc_hom`, `inl_inr_pushoutAssoc_inv`, `inr_inl_pushoutAssoc_hom`, `inl_pushoutAssoc_inv`, `inl_inl_pushoutAssoc_hom_assoc`, `inr_inr_pushoutAssoc_inv_assoc`, `inr_inl_pushoutAssoc_hom_assoc`, `inr_inr_pushoutAssoc_inv`
`pushoutAssocIsPushout` 📖	CompOp	—
`pushoutAssocSymmIsPushout` 📖	CompOp	—
`pushoutPushoutLeftIsPushout` 📖	CompOp	—
`pushoutPushoutRightIsPushout` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasPullback_assoc` 📖	mathematical	—	`HasPullback` `pullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback.fst`	—	`CategoryTheory.Category.assoc` `pullback.condition`
`hasPullback_assoc_symm` 📖	mathematical	—	`HasPullback` `pullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback.snd`	—	`pullback.condition` `CategoryTheory.Category.assoc`
`hasPushout_assoc` 📖	mathematical	—	`HasPushout` `pushout` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout.inl`	—	`CategoryTheory.Category.assoc` `pushout.condition`
`hasPushout_assoc_symm` 📖	mathematical	—	`HasPushout` `pushout` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout.inr`	—	`pushout.condition` `CategoryTheory.Category.assoc`
`inl_inl_pushoutAssoc_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.hom` `pushoutAssoc`	—	`pushout.condition` `CategoryTheory.Category.assoc` `IsColimit.comp_coconePointUniqueUpToIso_hom` `pushout.inl_desc`
`inl_inl_pushoutAssoc_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.hom` `pushoutAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_inl_pushoutAssoc_hom`
`inl_inr_pushoutAssoc_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.inv` `pushoutAssoc`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Iso.comp_inv_eq` `inr_inl_pushoutAssoc_hom`
`inl_inr_pushoutAssoc_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.inv` `pushoutAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_inr_pushoutAssoc_inv`
`inl_pushoutAssoc_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.inv` `pushoutAssoc`	—	`CategoryTheory.Iso.comp_inv_eq` `CategoryTheory.Category.assoc` `inl_inl_pushoutAssoc_hom`
`inl_pushoutAssoc_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.inv` `pushoutAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_pushoutAssoc_inv`
`inr_inl_pushoutAssoc_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.hom` `pushoutAssoc`	—	`pushout.condition` `CategoryTheory.Category.assoc` `IsColimit.comp_coconePointUniqueUpToIso_hom` `pushout.inl_desc` `pushout.inr_desc`
`inr_inl_pushoutAssoc_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.hom` `pushoutAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_inl_pushoutAssoc_hom`
`inr_inr_pushoutAssoc_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.inv` `pushoutAssoc`	—	`CategoryTheory.Category.assoc` `pushout.condition` `IsColimit.comp_coconePointUniqueUpToIso_inv` `pushout.inl_desc` `pushout.inr_desc`
`inr_inr_pushoutAssoc_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.inv` `pushoutAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_inr_pushoutAssoc_inv`
`inr_pushoutAssoc_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.hom` `pushoutAssoc`	—	`CategoryTheory.Iso.eq_comp_inv` `CategoryTheory.Category.assoc` `inr_inr_pushoutAssoc_inv`
`inr_pushoutAssoc_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.hom` `pushoutAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_pushoutAssoc_hom`
`pullbackAssoc_hom_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `pullback.fst` `CategoryTheory.Iso.hom` `pullbackAssoc`	—	`CategoryTheory.Iso.eq_inv_comp` `pullbackAssoc_inv_fst_fst`
`pullbackAssoc_hom_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `pullback.fst` `CategoryTheory.Iso.hom` `pullbackAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackAssoc_hom_fst`
`pullbackAssoc_hom_snd_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `pullback.fst` `CategoryTheory.Iso.hom` `pullbackAssoc`	—	`CategoryTheory.Category.assoc` `pullback.condition` `IsLimit.conePointUniqueUpToIso_hom_comp` `pullback.lift_fst`
`pullbackAssoc_hom_snd_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `pullback.fst` `CategoryTheory.Iso.hom` `pullbackAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackAssoc_hom_snd_fst`
`pullbackAssoc_hom_snd_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `pullback.fst` `CategoryTheory.Iso.hom` `pullbackAssoc`	—	`CategoryTheory.Category.assoc` `pullback.condition` `IsLimit.conePointUniqueUpToIso_hom_comp` `pullback.lift_snd`
`pullbackAssoc_hom_snd_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `pullback.fst` `CategoryTheory.Iso.hom` `pullbackAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackAssoc_hom_snd_snd`
`pullbackAssoc_inv_fst_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackAssoc`	—	`pullback.condition` `CategoryTheory.Category.assoc` `IsLimit.conePointUniqueUpToIso_inv_comp` `pullback.lift_fst`
`pullbackAssoc_inv_fst_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackAssoc_inv_fst_fst`
`pullbackAssoc_inv_fst_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackAssoc`	—	`CategoryTheory.Iso.inv_comp_eq` `pullbackAssoc_hom_snd_fst`
`pullbackAssoc_inv_fst_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackAssoc_inv_fst_snd`
`pullbackAssoc_inv_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackAssoc`	—	`CategoryTheory.Iso.inv_comp_eq` `pullbackAssoc_hom_snd_snd`
`pullbackAssoc_inv_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackAssoc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackAssoc_inv_snd`

---

← Back to Index