Documentation Verification Report

VerticalComposition

📁 Source: Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean

Statistics

Metric	Count
Definitions `structuredArrowDownwardsComp`, `vComp'`, `whiskerVertical`	3
Theorems `instWhiskerVerticalOfIsIsoFunctor`, `vComp`, `vComp'`, `vComp'_iff_of_equivalences`, `vComp_iff_of_equivalences`, `whiskerVertical`, `whiskerVertical_iff`, `vComp'_app`, `whiskerVertical_app`	9
Total	12

CategoryTheory.TwoSquare

Definitions

Name	Category	Theorems
`structuredArrowDownwardsComp` 📖	CompOp	—
`vComp'` 📖	CompOp	3 math math: `GuitartExact.vComp'_iff_of_equivalences`, `vComp'_app`, `GuitartExact.vComp'`
`whiskerVertical` 📖	CompOp	4 math math: `whiskerVertical_app`, `GuitartExact.whiskerVertical_iff`, `GuitartExact.instWhiskerVerticalOfIsIsoFunctor`, `GuitartExact.whiskerVertical`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vComp'_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `vComp'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.map` `natTrans` `CategoryTheory.Iso.hom`	—	`vComp_app` `CategoryTheory.Category.assoc`
`whiskerVertical_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `whiskerVertical` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `natTrans` `CategoryTheory.Functor.map`	—	—

CategoryTheory.TwoSquare.GuitartExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instWhiskerVerticalOfIsIsoFunctor` 📖	mathematical	—	`CategoryTheory.TwoSquare.GuitartExact` `CategoryTheory.TwoSquare.whiskerVertical`	—	`whiskerVertical`
`vComp` 📖	mathematical	—	`CategoryTheory.TwoSquare.GuitartExact` `CategoryTheory.Functor.comp` `CategoryTheory.TwoSquare.vComp`	—	`CategoryTheory.Functor.initial_natIso_iff` `CategoryTheory.Functor.initial_comp` `CategoryTheory.TwoSquare.instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact`
`vComp'` 📖	mathematical	—	`CategoryTheory.TwoSquare.GuitartExact` `CategoryTheory.TwoSquare.vComp'`	—	`instWhiskerVerticalOfIsIsoFunctor` `vComp` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.isIso_inv`
`vComp'_iff_of_equivalences` 📖	mathematical	—	`CategoryTheory.TwoSquare.GuitartExact` `CategoryTheory.TwoSquare.vComp'` `CategoryTheory.Equivalence.functor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp`	—	`vComp_iff_of_equivalences` `CategoryTheory.TwoSquare.vComp'.eq_1` `whiskerVertical_iff`
`vComp_iff_of_equivalences` 📖	mathematical	—	`CategoryTheory.TwoSquare.GuitartExact` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.functor` `CategoryTheory.TwoSquare.vComp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	`CategoryTheory.TwoSquare.ext` `CategoryTheory.TwoSquare.vComp'_app` `CategoryTheory.Category.assoc` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.TwoSquare.vComp_app` `CategoryTheory.Functor.map_comp` `CategoryTheory.Equivalence.inv_fun_map` `CategoryTheory.CatCommSq.vInv_iso_hom_app` `CategoryTheory.Iso.hom_inv_id_app_assoc` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.Equivalence.counitInv_app_functor` `CategoryTheory.Functor.comp_map` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Functor.map_id` `vComp'` `CategoryTheory.TwoSquare.guitartExact_of_isEquivalence_of_isIso` `CategoryTheory.Equivalence.isEquivalence_inverse` `CategoryTheory.Iso.isIso_hom` `vComp` `CategoryTheory.Equivalence.isEquivalence_functor`
`whiskerVertical` 📖	mathematical	—	`CategoryTheory.TwoSquare.GuitartExact` `CategoryTheory.TwoSquare.whiskerVertical` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Iso.inv`	—	`CategoryTheory.TwoSquare.guitartExact_iff_initial` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Functor.initial_natIso_iff` `CategoryTheory.Functor.initial_comp` `CategoryTheory.TwoSquare.instInitialStructuredArrowObjStructuredArrowDownwardsOfGuitartExact` `CategoryTheory.Functor.initial_of_isLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Equivalence.isEquivalence_functor`
`whiskerVertical_iff` 📖	mathematical	—	`CategoryTheory.TwoSquare.GuitartExact` `CategoryTheory.TwoSquare.whiskerVertical` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Iso.inv`	—	`CategoryTheory.TwoSquare.ext` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.hom_inv_id_app_assoc` `whiskerVertical`

---

← Back to Index