ChosenPullback

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

Statistics

Metric	Count
Definitions ChosenPullback, LiftStruct, f, isLimit, p, pullback, p₁, p₂, ChosenPullback₃, chosenPullback, l, p, pullback, p₁, p₁₂, p₁₃, p₂, p₂₃, p₃	19
Theorems f_p, f_p_assoc, f_p₁, f_p₁_assoc, f_p₂, f_p₂_assoc, instSubsingleton, nonempty, w, w_assoc, condition, condition_assoc, hom_ext, hom_ext_iff, hp₁, hp₁_assoc, hp₂, hp₂_assoc, instNonemptyDiagonal, isPullback, exists_lift, hom_ext, hom_ext_iff, hp₁, hp₃, isPullback₁, isPullback₂, isPullback₃, p₁₂_eq_lift, p₁₂_p, p₁₂_p_assoc, p₁₂_p₁, p₁₂_p₁_assoc, p₁₂_p₂, p₁₂_p₂_assoc, p₁₃_eq_lift, p₁₃_p, p₁₃_p_assoc, p₁₃_p₁, p₁₃_p₁_assoc, p₁₃_p₃, p₁₃_p₃_assoc, p₂₃_eq_lift, p₂₃_p, p₂₃_p_assoc, p₂₃_p₂, p₂₃_p₂_assoc, p₂₃_p₃, p₂₃_p₃_assoc, w₁, w₁_assoc, w₂, w₂_assoc, w₃, w₃_assoc	55
Total	74

CategoryTheory.Limits

Definitions

Name	Category	Theorems
ChosenPullback 📖	CompData	—
ChosenPullback₃ 📖	CompData	—

CategoryTheory.Limits.ChosenPullback

Definitions

Name	Category	Theorems
LiftStruct 📖	CompData	2 math math: LiftStruct.nonempty, LiftStruct.instSubsingleton
isLimit 📖	CompOp	—
p 📖	CompOp	14 math math: CategoryTheory.Limits.ChosenPullback₃.p₂₃_p, LiftStruct.f_p_assoc, CategoryTheory.Pseudofunctor.DescentData'.ofDescentData_hom, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p_assoc, LiftStruct.f_p, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p, hp₁_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p, hp₁, hp₂, hp₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_p₁_p₂, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p_assoc
pullback 📖	CompOp	60 math math: CategoryTheory.Limits.ChosenPullback₃.p₂₃_p, LiftStruct.f_p₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom_assoc, CategoryTheory.Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₁_assoc, isPullback, LiftStruct.f_p_assoc, CategoryTheory.Limits.ChosenPullback₃.isPullback₂, CategoryTheory.Limits.ChosenPullback₃.hp₁, CategoryTheory.Pseudofunctor.DescentData'.ofDescentData_hom, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃_assoc, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p_assoc, CategoryTheory.Limits.ChosenPullback₃.isPullback₃, LiftStruct.f_p₁_assoc, LiftStruct.f_p, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p, condition, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₃, CategoryTheory.Limits.ChosenPullback₃.hp₃, hp₁_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p, CategoryTheory.Limits.ChosenPullback₃.p₂₃_eq_lift, CategoryTheory.Limits.ChosenPullback₃.w₁_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂, hom_ext_iff, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂, CategoryTheory.Limits.ChosenPullback₃.isPullback₁, hp₁, hp₂, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂_assoc, hp₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_p₁_p₂, CategoryTheory.Pseudofunctor.DescentData'.Hom.comm, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁, CategoryTheory.Pseudofunctor.DescentData'.Hom.comm_assoc, LiftStruct.f_p₂_assoc, LiftStruct.f_p₂, CategoryTheory.Limits.ChosenPullback₃.p₁₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_hom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂_assoc, CategoryTheory.Limits.ChosenPullback₃.w₁, condition_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Limits.ChosenPullback₃.w₃, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₂_eq_lift, CategoryTheory.Limits.ChosenPullback₃.w₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁_assoc
p₁ 📖	CompOp	41 math math: LiftStruct.f_p₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom_assoc, CategoryTheory.Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₁_assoc, isPullback, CategoryTheory.Limits.ChosenPullback₃.isPullback₂, CategoryTheory.Limits.ChosenPullback₃.hp₁, CategoryTheory.Pseudofunctor.DescentData'.ofDescentData_hom, LiftStruct.f_p₁_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, condition, CategoryTheory.Limits.ChosenPullback₃.hp₃, hp₁_assoc, CategoryTheory.Limits.ChosenPullback₃.p₂₃_eq_lift, CategoryTheory.Limits.ChosenPullback₃.w₁_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂, hom_ext_iff, CategoryTheory.Limits.ChosenPullback₃.isPullback₁, hp₁, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_p₁_p₂, CategoryTheory.Pseudofunctor.DescentData'.Hom.comm, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁, CategoryTheory.Pseudofunctor.DescentData'.Hom.comm_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_hom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp, CategoryTheory.Limits.ChosenPullback₃.w₁, condition_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Limits.ChosenPullback₃.w₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₂_eq_lift, CategoryTheory.Limits.ChosenPullback₃.w₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₁_assoc
p₂ 📖	CompOp	41 math math: CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom_assoc, CategoryTheory.Pseudofunctor.DescentData'.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpPullbackHom, isPullback, CategoryTheory.Limits.ChosenPullback₃.isPullback₂, CategoryTheory.Limits.ChosenPullback₃.hp₁, CategoryTheory.Pseudofunctor.DescentData'.ofDescentData_hom, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃, CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₃_assoc, CategoryTheory.Limits.ChosenPullback₃.isPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, condition, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₃, CategoryTheory.Limits.ChosenPullback₃.hp₃, CategoryTheory.Limits.ChosenPullback₃.p₂₃_eq_lift, CategoryTheory.Limits.ChosenPullback₃.w₁_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, hom_ext_iff, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂, hp₂, hp₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_pullHom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_p₁_p₂, CategoryTheory.Pseudofunctor.DescentData'.Hom.comm, CategoryTheory.Pseudofunctor.DescentData'.Hom.comm_assoc, LiftStruct.f_p₂_assoc, LiftStruct.f_p₂, CategoryTheory.Limits.ChosenPullback₃.p₁₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_eq_hom, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp, CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₂_assoc, CategoryTheory.Limits.ChosenPullback₃.w₁, condition_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Limits.ChosenPullback₃.w₃, CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Limits.ChosenPullback₃.p₁₂_eq_lift, CategoryTheory.Limits.ChosenPullback₃.w₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₁ p₂	—	—
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₁ p₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₁ p₂	—	—	CategoryTheory.IsPullback.hom_ext isPullback
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₁ p₂	—	hom_ext
hp₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₁ p	—	—
hp₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₁ p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hp₁
hp₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₂ p	—	condition hp₁
hp₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₂ p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hp₂
instNonemptyDiagonal 📖	mathematical	—	Diagonal	—	LiftStruct.nonempty CategoryTheory.Category.id_comp
isPullback 📖	mathematical	—	CategoryTheory.IsPullback pullback p₁ p₂	—	condition

CategoryTheory.Limits.ChosenPullback.LiftStruct

Definitions

Name	Category	Theorems
f 📖	CompOp	6 math math: f_p₁, f_p_assoc, f_p₁_assoc, f_p, f_p₂_assoc, f_p₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f_p 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback f CategoryTheory.Limits.ChosenPullback.p	—	—
f_p_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback f CategoryTheory.Limits.ChosenPullback.p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f_p
f_p₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback f CategoryTheory.Limits.ChosenPullback.p₁	—	—
f_p₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback f CategoryTheory.Limits.ChosenPullback.p₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f_p₁
f_p₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback f CategoryTheory.Limits.ChosenPullback.p₂	—	—
f_p₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback f CategoryTheory.Limits.ChosenPullback.p₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f_p₂
instSubsingleton 📖	mathematical	—	CategoryTheory.Limits.ChosenPullback.LiftStruct	—	CategoryTheory.Limits.ChosenPullback.hom_ext
nonempty 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Limits.ChosenPullback.LiftStruct	—	CategoryTheory.IsPullback.exists_lift CategoryTheory.Limits.ChosenPullback.isPullback CategoryTheory.Limits.ChosenPullback.hp₁ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	f_p₁ CategoryTheory.Category.assoc CategoryTheory.Limits.ChosenPullback.condition f_p₂
w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w

CategoryTheory.Limits.ChosenPullback₃

Definitions

Name	Category	Theorems
chosenPullback 📖	CompOp	16 math math: hp₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, hp₃, w₁_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, p₁₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp, w₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, w₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, p₁₂_eq_lift, w₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc
l 📖	CompOp	—
p 📖	CompOp	20 math math: p₂₃_p, w₂, p₂₃_p_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, p₁₂_p, p₁₃_p, w₁_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, w₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp, w₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, w₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, p₁₂_p_assoc, p₁₃_p_assoc, w₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc
pullback 📖	CompOp	32 math math: p₂₃_p, p₁₂_p₁_assoc, w₂, isPullback₂, p₂₃_p₃, p₂₃_p₃_assoc, p₂₃_p_assoc, isPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, p₁₂_p, p₁₃_p₃, p₁₃_p, p₂₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, p₁₂_p₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, p₂₃_p₂, w₂_assoc, p₁₂_p₂, isPullback₁, hom_ext_iff, p₂₃_p₂_assoc, p₁₃_p₁, p₁₂_p₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, p₁₃_p₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, p₁₂_p_assoc, p₁₃_p_assoc, exists_lift, p₁₃_p₁_assoc
p₁ 📖	CompOp	17 math math: p₁₂_p₁_assoc, hp₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, w₁_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, p₁₂_p₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, hom_ext_iff, p₁₃_p₁, p₁₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp, w₁, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, p₁₂_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc, exists_lift, p₁₃_p₁_assoc
p₁₂ 📖	CompOp	11 math math: p₁₂_p₁_assoc, isPullback₂, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, p₁₂_p, p₁₂_p₁, p₁₂_p₂, isPullback₁, p₁₂_p₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, p₁₂_p_assoc, p₁₂_eq_lift
p₁₃ 📖	CompOp	11 math math: isPullback₃, p₁₃_p₃, p₁₃_p, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, isPullback₁, p₁₃_p₁, p₁₃_eq_lift, p₁₃_p₃_assoc, p₁₃_p_assoc, p₁₃_p₁_assoc
p₂ 📖	CompOp	16 math math: w₂, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃, p₂₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, p₂₃_p₂, w₂_assoc, p₁₂_p₂, hom_ext_iff, p₂₃_p₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp, p₁₂_p₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, p₁₂_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc, exists_lift
p₂₃ 📖	CompOp	11 math math: p₂₃_p, isPullback₂, p₂₃_p₃, p₂₃_p₃_assoc, p₂₃_p_assoc, isPullback₃, p₂₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, p₂₃_p₂, p₂₃_p₂_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc
p₃ 📖	CompOp	17 math math: p₂₃_p₃, p₂₃_p₃_assoc, p₁₃_p₃, hp₃, p₂₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₃_eq_pullHom_of_chosenPullback₃, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃, hom_ext_iff, p₁₃_eq_lift, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp, w₃, p₁₃_p₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc, w₃_assoc, CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc, exists_lift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lift 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.CategoryStruct.comp p₁ p₂ p₃	—	CategoryTheory.IsPullback.exists_lift CategoryTheory.Limits.ChosenPullback.isPullback CategoryTheory.Category.assoc CategoryTheory.Limits.ChosenPullback.hp₂ CategoryTheory.Limits.ChosenPullback.hp₁ p₁₂.eq_1 p₁₂_p₁ p₁₂_p₂ p₂₃.eq_1 p₂₃_p₃
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₁ p₂ p₃	—	—	CategoryTheory.IsPullback.hom_ext isPullback₂ CategoryTheory.Limits.ChosenPullback.hom_ext CategoryTheory.Category.assoc p₁₂_p₁ p₁₂_p₂ p₂₃_p₂ p₂₃_p₃
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₁ p₂ p₃	—	hom_ext
hp₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ chosenPullback p₁	—	—
hp₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ chosenPullback p₃	—	—
isPullback₁ 📖	mathematical	—	CategoryTheory.IsPullback pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₂ p₁₃ CategoryTheory.Limits.ChosenPullback.p₁	—	CategoryTheory.IsPullback.mk' p₁₂_p₁ p₁₃_p₁ hom_ext CategoryTheory.Category.assoc CategoryTheory.eq_whisker p₁₂_p₂ p₁₃_p₃ exists_lift CategoryTheory.Limits.ChosenPullback.hp₂ CategoryTheory.Limits.ChosenPullback.hp₁ CategoryTheory.Limits.ChosenPullback.hom_ext
isPullback₂ 📖	mathematical	—	CategoryTheory.IsPullback pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₂ p₂₃ CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁	—	CategoryTheory.Limits.ChosenPullback.isPullback
isPullback₃ 📖	mathematical	—	CategoryTheory.IsPullback pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₃ p₂₃ CategoryTheory.Limits.ChosenPullback.p₂	—	CategoryTheory.IsPullback.mk' p₁₃_p₃ p₂₃_p₃ hom_ext CategoryTheory.Category.assoc p₁₃_p₁ CategoryTheory.eq_whisker p₂₃_p₂ exists_lift CategoryTheory.Limits.ChosenPullback.hp₁ CategoryTheory.Limits.ChosenPullback.hp₂ CategoryTheory.Limits.ChosenPullback.hom_ext
p₁₂_eq_lift 📖	mathematical	—	p₁₂ CategoryTheory.IsPullback.lift CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.isPullback chosenPullback p₁ p₂	—	CategoryTheory.Limits.ChosenPullback.hom_ext CategoryTheory.Limits.ChosenPullback.isPullback p₁₂_p₁ CategoryTheory.IsPullback.lift_fst p₁₂_p₂ CategoryTheory.IsPullback.lift_snd
p₁₂_p 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₂ CategoryTheory.Limits.ChosenPullback.p p	—	CategoryTheory.Limits.ChosenPullback.hp₂ p₁₂_p₂_assoc w₂
p₁₂_p_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₂ CategoryTheory.Limits.ChosenPullback.p p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₁₂_p
p₁₂_p₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₂ CategoryTheory.Limits.ChosenPullback.p₁ p₁	—	hp₁
p₁₂_p₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₂ CategoryTheory.Limits.ChosenPullback.p₁ p₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₁₂_p₁
p₁₂_p₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₂ CategoryTheory.Limits.ChosenPullback.p₂ p₂	—	CategoryTheory.Limits.ChosenPullback.hp₁
p₁₂_p₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₂ CategoryTheory.Limits.ChosenPullback.p₂ p₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₁₂_p₂
p₁₃_eq_lift 📖	mathematical	—	p₁₃ CategoryTheory.IsPullback.lift CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.isPullback chosenPullback p₁ p₃	—	CategoryTheory.Limits.ChosenPullback.hom_ext CategoryTheory.Limits.ChosenPullback.isPullback p₁₃_p₁ CategoryTheory.IsPullback.lift_fst p₁₃_p₃ CategoryTheory.IsPullback.lift_snd
p₁₃_p 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₃ CategoryTheory.Limits.ChosenPullback.p p	—	CategoryTheory.Limits.ChosenPullback.hp₁ p₁₃_p₁_assoc w₁
p₁₃_p_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₃ CategoryTheory.Limits.ChosenPullback.p p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₁₃_p
p₁₃_p₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₃ CategoryTheory.Limits.ChosenPullback.p₁ p₁	—	CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁
p₁₃_p₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₃ CategoryTheory.Limits.ChosenPullback.p₁ p₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₁₃_p₁
p₁₃_p₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₃ CategoryTheory.Limits.ChosenPullback.p₂ p₃	—	CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂
p₁₃_p₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₁₃ CategoryTheory.Limits.ChosenPullback.p₂ p₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₁₃_p₃
p₂₃_eq_lift 📖	mathematical	—	p₂₃ CategoryTheory.IsPullback.lift CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₁ CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.isPullback pullback p₂ p₃	—	CategoryTheory.Limits.ChosenPullback.hom_ext CategoryTheory.Limits.ChosenPullback.isPullback p₂₃_p₂ CategoryTheory.IsPullback.lift_fst p₂₃_p₃ CategoryTheory.IsPullback.lift_snd
p₂₃_p 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₂₃ CategoryTheory.Limits.ChosenPullback.p p	—	CategoryTheory.Limits.ChosenPullback.hp₂ p₂₃_p₃_assoc w₃
p₂₃_p_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₂₃ CategoryTheory.Limits.ChosenPullback.p p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₂₃_p
p₂₃_p₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₂₃ CategoryTheory.Limits.ChosenPullback.p₁ p₂	—	CategoryTheory.Limits.ChosenPullback.hp₂
p₂₃_p₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₂₃ CategoryTheory.Limits.ChosenPullback.p₁ p₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₂₃_p₂
p₂₃_p₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₂₃ CategoryTheory.Limits.ChosenPullback.p₂ p₃	—	hp₃
p₂₃_p₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback CategoryTheory.Limits.ChosenPullback.pullback p₂₃ CategoryTheory.Limits.ChosenPullback.p₂ p₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p₂₃_p₃
w₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ chosenPullback p₁ p	—	CategoryTheory.Category.assoc CategoryTheory.Limits.ChosenPullback.hp₁ CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p CategoryTheory.eq_whisker CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁
w₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ chosenPullback p₁ p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w₁
w₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₂ p	—	p₂₃_p₂_assoc CategoryTheory.Limits.ChosenPullback.condition w₃ p₂₃_p₃_assoc
w₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct pullback p₂ p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w₂
w₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ chosenPullback p₃ p	—	CategoryTheory.Category.assoc CategoryTheory.Limits.ChosenPullback.hp₂ CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p CategoryTheory.eq_whisker CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂
w₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.ChosenPullback.pullback CategoryTheory.Limits.ChosenPullback.p₂ CategoryTheory.Limits.ChosenPullback.p₁ chosenPullback p₃ p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w₃

---

← Back to Index