Documentation Verification Report

TwoSquare

📁 Source: Mathlib/CategoryTheory/Functor/TwoSquare.lean

Statistics

Metric	Count
Definitions `TwoSquare`, `equivNatTrans`, `hComp`, `hId`, `mk`, `natTrans`, `op`, `vComp`, `vId`, `whiskerBottom`, `whiskerLeft`, `whiskerRight`, `whiskerTop`, `«term_≫ᵥ_»`, `«term_≫ₕ_»`, `«term𝟙ᵥ»`, `«term𝟙ₕ»`	17
Theorems `equivNatTrans_apply`, `equivNatTrans_symm_apply`, `ext`, `ext_iff`, `hCompVCompHComp`, `hComp_app`, `hId_app`, `natTrans_op`, `vComp_app`, `vId_app`, `whiskerBottom_app`, `whiskerLeft_app`, `whiskerRight_app`, `whiskerTop_app`	14
Total	31

CategoryTheory

Definitions

Name	Category	Theorems
`TwoSquare` 📖	CompOp	16 math math: `TwoSquare.equivNatTrans_symm_apply`, `mateEquiv_counit_symm`, `iterated_mateEquiv_conjugateEquiv`, `iterated_mateEquiv_conjugateEquiv_symm`, `TwoSquare.equivNatTrans_apply`, `mateEquiv_hcomp`, `mateEquiv_symm_apply`, `conjugateEquiv_mateEquiv_vcomp`, `mateEquiv_conjugateEquiv_vcomp`, `Bicategory.toNatTrans_mateEquiv`, `unit_mateEquiv_symm`, `unit_mateEquiv`, `mateEquiv_vcomp`, `mateEquiv_counit`, `mateEquiv_square`, `mateEquiv_apply`

CategoryTheory.TwoSquare

Definitions

Name	Category	Theorems
`equivNatTrans` 📖	CompOp	3 math math: `equivNatTrans_symm_apply`, `CategoryTheory.iterated_mateEquiv_conjugateEquiv_symm`, `equivNatTrans_apply`
`hComp` 📖	CompOp	5 math math: `CategoryTheory.mateEquiv_hcomp`, `hComp_app`, `hCompVCompHComp`, `CategoryTheory.mateEquiv_vcomp`, `CategoryTheory.mateEquiv_square`
`hId` 📖	CompOp	1 math math: `hId_app`
`mk` 📖	CompOp	—
`natTrans` 📖	CompOp	26 math math: `structuredArrowRightwardsOpEquivalence.functor_obj_hom_right`, `CategoryTheory.iterated_mateEquiv_conjugateEquiv`, `structuredArrowRightwardsOpEquivalence.functor_obj_left_hom`, `structuredArrowRightwardsOpEquivalence.functor_obj_left_right`, `equivNatTrans_apply`, `CategoryTheory.coev_expComparison`, `CategoryTheory.frobeniusMorphism_mate`, `CategoryTheory.MonoidalClosedFunctor.comparison_iso`, `whiskerVertical_app`, `whiskerBottom_app`, `hComp_app`, `natTrans_op`, `CategoryTheory.frobeniusMorphism_iso_of_preserves_binary_products`, `CategoryTheory.mateEquiv_symm_apply`, `CategoryTheory.uncurry_expComparison`, `structuredArrowRightwardsOpEquivalence.functor_map_left_right`, `whiskerLeft_app`, `CategoryTheory.expComparison_ev`, `whiskerTop_app`, `CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso`, `whiskerRight_app`, `CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso`, `vComp_app`, `vComp'_app`, `ext_iff`, `CategoryTheory.mateEquiv_apply`
`op` 📖	CompOp	13 math math: `structuredArrowRightwardsOpEquivalence.functor_obj_hom_right`, `structuredArrowRightwardsOpEquivalence.functor_obj_left_hom`, `structuredArrowRightwardsOpEquivalence_inverse`, `structuredArrowRightwardsOpEquivalence.functor_obj_right_as`, `structuredArrowRightwardsOpEquivalence.functor_obj_left_right`, `structuredArrowRightwardsOpEquivalence_counitIso`, `guitartExact_op_iff`, `natTrans_op`, `structuredArrowRightwardsOpEquivalence.functor_map_left_right`, `structuredArrowRightwardsOpEquivalence_unitIso`, `instGuitartExactOppositeOp`, `structuredArrowRightwardsOpEquivalence_functor`, `structuredArrowRightwardsOpEquivalence.functor_obj_left_left_as`
`vComp` 📖	CompOp	7 math math: `GuitartExact.vComp_iff_of_equivalences`, `CategoryTheory.mateEquiv_hcomp`, `hCompVCompHComp`, `CategoryTheory.mateEquiv_vcomp`, `vComp_app`, `GuitartExact.vComp`, `CategoryTheory.mateEquiv_square`
`vId` 📖	CompOp	1 math math: `vId_app`
`whiskerBottom` 📖	CompOp	3 math math: `CategoryTheory.expComparison_whiskerLeft`, `whiskerBottom_app`, `CategoryTheory.mateEquiv_conjugateEquiv_vcomp`
`whiskerLeft` 📖	CompOp	2 math math: `CategoryTheory.conjugateEquiv_mateEquiv_vcomp`, `whiskerLeft_app`
`whiskerRight` 📖	CompOp	2 math math: `CategoryTheory.mateEquiv_conjugateEquiv_vcomp`, `whiskerRight_app`
`whiskerTop` 📖	CompOp	3 math math: `CategoryTheory.expComparison_whiskerLeft`, `CategoryTheory.conjugateEquiv_mateEquiv_vcomp`, `whiskerTop_app`
`«term_≫ᵥ_»` 📖	CompOp	—
`«term_≫ₕ_»` 📖	CompOp	—
`«term𝟙ᵥ»` 📖	CompOp	—
`«term𝟙ₕ»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivNatTrans_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.TwoSquare` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivNatTrans` `natTrans`	—	—
`equivNatTrans_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivNatTrans`	—	—
`ext` 📖	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `natTrans`	—	—	`CategoryTheory.NatTrans.ext`
`ext_iff` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `natTrans`	—	`ext`
`hCompVCompHComp` 📖	mathematical	—	`vComp` `CategoryTheory.Functor.comp` `hComp`	—	`ext` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.comp_map` `CategoryTheory.NatTrans.naturality`
`hComp_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `hComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `natTrans` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`hId_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `hId` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`natTrans_op` 📖	mathematical	—	`natTrans` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `op` `CategoryTheory.NatTrans.op` `CategoryTheory.Functor.comp`	—	—
`vComp_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `vComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `natTrans`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`vId_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `vId` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`whiskerBottom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `whiskerBottom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `natTrans`	—	—
`whiskerLeft_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `whiskerLeft` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `natTrans` `CategoryTheory.Functor.map`	—	—
`whiskerRight_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `whiskerRight` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `natTrans`	—	—
`whiskerTop_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `whiskerTop` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `natTrans`	—	—

---

← Back to Index