Documentation Verification Report

ParametrizedAdjunction

📁 Source: Mathlib/CategoryTheory/LiftingProperties/ParametrizedAdjunction.lean

Statistics

Metric	Count
Definitions `ParametrizedAdjunction`, `arrowHomEquiv`, `liftStructEquiv`	3
Theorems `arrowHomEquiv_apply_left`, `arrowHomEquiv_apply_right_fst`, `arrowHomEquiv_apply_right_fst_assoc`, `arrowHomEquiv_apply_right_snd`, `arrowHomEquiv_apply_right_snd_assoc`, `arrowHomEquiv_symm_apply_right`, `hasLiftingProperty_iff`, `inl_arrowHomEquiv_symm_apply_left`, `inl_arrowHomEquiv_symm_apply_left_assoc`, `inr_arrowHomEquiv_symm_apply_left`, `inr_arrowHomEquiv_symm_apply_left_assoc`	11
Total	14

CategoryTheory

Definitions

Name	Category	Theorems
`ParametrizedAdjunction` 📖	CompData	—

CategoryTheory.ParametrizedAdjunction

Definitions

Name	Category	Theorems
`arrowHomEquiv` 📖	CompOp	10 math math: `inr_arrowHomEquiv_symm_apply_left`, `inl_arrowHomEquiv_symm_apply_left`, `arrowHomEquiv_apply_left`, `arrowHomEquiv_apply_right_snd`, `arrowHomEquiv_symm_apply_right`, `inr_arrowHomEquiv_symm_apply_left_assoc`, `arrowHomEquiv_apply_right_fst_assoc`, `inl_arrowHomEquiv_symm_apply_left_assoc`, `arrowHomEquiv_apply_right_fst`, `arrowHomEquiv_apply_right_snd_assoc`
`liftStructEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrowHomEquiv_apply_left` 📖	mathematical	—	`CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.id` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategoryArrow` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Functor.PushoutObjObj.ι` `EquivLike.toFunLike` `Equiv.instEquivLike` `arrowHomEquiv` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.PushoutObjObj.inl`	—	—
`arrowHomEquiv_apply_right_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.right` `CategoryTheory.Functor.id` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `CategoryTheory.CommaMorphism.right` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.instCategoryArrow` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Functor.PushoutObjObj.ι` `EquivLike.toFunLike` `Equiv.instEquivLike` `arrowHomEquiv` `CategoryTheory.Functor.PullbackObjObj.fst` `CategoryTheory.Comma.left` `homEquiv` `CategoryTheory.Functor.PushoutObjObj.inr` `CategoryTheory.CommaMorphism.left`	—	`CategoryTheory.IsPullback.lift_fst` `CategoryTheory.Functor.PullbackObjObj.isPullback`
`arrowHomEquiv_apply_right_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.right` `CategoryTheory.Functor.id` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `CategoryTheory.CommaMorphism.right` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.instCategoryArrow` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Functor.PushoutObjObj.ι` `EquivLike.toFunLike` `Equiv.instEquivLike` `arrowHomEquiv` `CategoryTheory.Functor.PullbackObjObj.fst` `CategoryTheory.Comma.left` `homEquiv` `CategoryTheory.Functor.PushoutObjObj.inr` `CategoryTheory.CommaMorphism.left`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `arrowHomEquiv_apply_right_fst`
`arrowHomEquiv_apply_right_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.right` `CategoryTheory.Functor.id` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `CategoryTheory.CommaMorphism.right` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.instCategoryArrow` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Functor.PushoutObjObj.ι` `EquivLike.toFunLike` `Equiv.instEquivLike` `arrowHomEquiv` `CategoryTheory.Functor.PullbackObjObj.snd` `homEquiv`	—	`CategoryTheory.IsPullback.lift_snd` `CategoryTheory.Functor.PullbackObjObj.isPullback`
`arrowHomEquiv_apply_right_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comma.right` `CategoryTheory.Functor.id` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `CategoryTheory.CommaMorphism.right` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.instCategoryArrow` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Functor.PushoutObjObj.ι` `EquivLike.toFunLike` `Equiv.instEquivLike` `arrowHomEquiv` `CategoryTheory.Functor.PullbackObjObj.snd` `homEquiv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `arrowHomEquiv_apply_right_snd`
`arrowHomEquiv_symm_apply_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Functor.id` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.PushoutObjObj.ι` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.instCategoryArrow` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `arrowHomEquiv` `homEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.PullbackObjObj.snd`	—	—
`hasLiftingProperty_iff` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.PushoutObjObj.ι` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π`	—	`Equiv.surjective`
`inl_arrowHomEquiv_symm_apply_left` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.Functor.PushoutObjObj.inl` `CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.PushoutObjObj.ι` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.instCategoryArrow` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `arrowHomEquiv` `homEquiv`	—	`CategoryTheory.IsPushout.inl_desc` `CategoryTheory.Functor.PushoutObjObj.isPushout`
`inl_arrowHomEquiv_symm_apply_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Functor.PushoutObjObj.inl` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.PushoutObjObj.ι` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.instCategoryArrow` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `arrowHomEquiv` `homEquiv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_arrowHomEquiv_symm_apply_left`
`inr_arrowHomEquiv_symm_apply_left` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.Functor.PushoutObjObj.inr` `CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.PushoutObjObj.ι` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.instCategoryArrow` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `arrowHomEquiv` `CategoryTheory.Comma.right` `homEquiv` `CategoryTheory.CommaMorphism.right` `CategoryTheory.Functor.PullbackObjObj.fst`	—	`CategoryTheory.IsPushout.inr_desc` `CategoryTheory.Functor.PushoutObjObj.isPushout`
`inr_arrowHomEquiv_symm_apply_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.PushoutObjObj.pt` `CategoryTheory.Functor.PushoutObjObj.inr` `CategoryTheory.Comma.left` `CategoryTheory.Functor.id` `CategoryTheory.CommaMorphism.left` `CategoryTheory.Functor.PushoutObjObj.ι` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Arrow` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.instCategoryArrow` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `CategoryTheory.Functor.PullbackObjObj.pt` `CategoryTheory.Functor.PullbackObjObj.π` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `arrowHomEquiv` `CategoryTheory.Comma.right` `homEquiv` `CategoryTheory.CommaMorphism.right` `CategoryTheory.Functor.PullbackObjObj.fst`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_arrowHomEquiv_symm_apply_left`

---

← Back to Index