Mates

📁 Source: Mathlib/CategoryTheory/Adjunction/Mates.lean

Statistics

Metric	Count
Definitions `conjugateEquiv`, `conjugateIsoEquiv`, `mateEquiv`	3
Theorems `conjugateEquiv_adjunction_id`, `conjugateEquiv_adjunction_id_symm`, `conjugateEquiv_apply_app`, `conjugateEquiv_associator_hom`, `conjugateEquiv_comm`, `conjugateEquiv_comp`, `conjugateEquiv_comp_assoc`, `conjugateEquiv_counit`, `conjugateEquiv_counit_symm`, `conjugateEquiv_id`, `conjugateEquiv_iso`, `conjugateEquiv_leftUnitor_hom`, `conjugateEquiv_mateEquiv_vcomp`, `conjugateEquiv_of_iso`, `conjugateEquiv_rightUnitor_hom`, `conjugateEquiv_symm_apply_app`, `conjugateEquiv_symm_comm`, `conjugateEquiv_symm_comp`, `conjugateEquiv_symm_comp_assoc`, `conjugateEquiv_symm_id`, `conjugateEquiv_symm_iso`, `conjugateEquiv_symm_of_iso`, `conjugateEquiv_whiskerLeft`, `conjugateEquiv_whiskerRight`, `conjugateIsoEquiv_apply_hom`, `conjugateIsoEquiv_apply_inv`, `conjugateIsoEquiv_symm_apply_hom`, `conjugateIsoEquiv_symm_apply_inv`, `iterated_mateEquiv_conjugateEquiv`, `iterated_mateEquiv_conjugateEquiv_symm`, `mateEquiv_apply`, `mateEquiv_conjugateEquiv_vcomp`, `mateEquiv_counit`, `mateEquiv_counit_symm`, `mateEquiv_hcomp`, `mateEquiv_square`, `mateEquiv_symm_apply`, `mateEquiv_vcomp`, `unit_conjugateEquiv`, `unit_conjugateEquiv_symm`, `unit_mateEquiv`, `unit_mateEquiv_symm`	42
Total	45

CategoryTheory

Definitions

Name	Category	Theorems
`conjugateEquiv` 📖	CompOp	45 math math: `conjugateEquiv_iso`, `iterated_mateEquiv_conjugateEquiv`, `iterated_mateEquiv_conjugateEquiv_symm`, `conjugateEquiv_symm_id`, `conjugateEquiv_symm_comp_assoc`, `conjugateEquiv_symm_apply_app`, `conjugateEquiv_apply_app`, `frobeniusMorphism_mate`, `Adjunction.conjugateEquiv_leftAdjointCompIso_inv`, `Adjunction.leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm`, `conjugateEquiv_leftUnitor_hom`, `Equivalence.inverseFunctor_map`, `conjugateEquiv_counit_symm`, `conjugateEquiv_symm_iso`, `Equivalence.symmEquivFunctor_map`, `Adjunction.conjugateEquiv_leftAdjointIdIso_hom`, `conjugateEquiv_whiskerRight`, `unit_conjugateEquiv_symm`, `unit_conjugateEquiv`, `conjugateEquiv_symm_comp`, `SheafOfModules.conjugateEquiv_pullbackComp_inv`, `conjugateEquiv_counit`, `conjugateEquiv_rightUnitor_hom`, `conjugateEquiv_mateEquiv_vcomp`, `mateEquiv_conjugateEquiv_vcomp`, `conjugateEquiv_comm`, `Equivalence.congrLeftFunctor_map`, `conjugateEquiv_comp_assoc`, `conjugateEquiv_associator_hom`, `conjugateEquiv_symm_comm`, `conjugateEquiv_id`, `AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackId_hom`, `AlgebraicGeometry.Scheme.Modules.conjugateEquiv_pullbackComp_inv`, `conjugateIsoEquiv_apply_hom`, `conjugateIsoEquiv_apply_inv`, `conjugateEquiv_whiskerLeft`, `conjugateIsoEquiv_symm_apply_inv`, `Adjunction.leftAdjointCompNatTrans₀₂₃_eq_conjugateEquiv_symm`, `conjugateEquiv_adjunction_id_symm`, `SheafOfModules.conjugateEquiv_pullbackId_hom`, `conjugateEquiv_adjunction_id`, `conjugateIsoEquiv_symm_apply_hom`, `Bicategory.toNatTrans_conjugateEquiv`, `conjugateEquiv_comp`, `Equivalence.symmEquivInverse_map_app`
`conjugateIsoEquiv` 📖	CompOp	4 math math: `conjugateIsoEquiv_apply_hom`, `conjugateIsoEquiv_apply_inv`, `conjugateIsoEquiv_symm_apply_inv`, `conjugateIsoEquiv_symm_apply_hom`
`mateEquiv` 📖	CompOp	14 math math: `mateEquiv_counit_symm`, `iterated_mateEquiv_conjugateEquiv`, `iterated_mateEquiv_conjugateEquiv_symm`, `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`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjugateEquiv_adjunction_id` 📖	mathematical	—	`NatTrans.app` `Functor.id` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `Adjunction.id` `CategoryStruct.comp` `Functor.obj` `Functor.comp` `Adjunction.counit`	—	`Category.id_comp` `Functor.whiskerRight_comp` `Category.assoc` `Category.comp_id`
`conjugateEquiv_adjunction_id_symm` 📖	mathematical	—	`NatTrans.app` `Functor.id` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateEquiv` `Adjunction.id` `CategoryStruct.comp` `Functor.obj` `Functor.comp` `Adjunction.unit`	—	`Category.id_comp` `Functor.whiskerRight_comp` `Category.assoc` `Category.comp_id`
`conjugateEquiv_apply_app` 📖	mathematical	—	`NatTrans.app` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `CategoryStruct.comp` `Functor.obj` `Functor.id` `Functor.comp` `Adjunction.unit` `Functor.map` `Adjunction.counit`	—	`Category.comp_id` `Category.id_comp`
`conjugateEquiv_associator_hom` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `Adjunction.comp` `Iso.hom` `Functor.associator`	—	`NatTrans.ext'` `conjugateEquiv_apply_app` `Adjunction.comp_unit_app` `Category.assoc` `Functor.map_id` `Adjunction.comp_counit_app` `Category.id_comp` `Functor.map_comp` `Adjunction.unit_naturality_assoc` `Adjunction.right_triangle_components` `Category.comp_id`
`conjugateEquiv_comm` 📖	mathematical	`CategoryStruct.comp` `Functor` `Category.toCategoryStruct` `Functor.category` `CategoryStruct.id`	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv`	—	`conjugateEquiv_comp` `conjugateEquiv_id`
`conjugateEquiv_comp` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Category.toCategoryStruct` `Functor.category` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv`	—	`NatTrans.ext'` `mateEquiv_vcomp` `congr_app` `Category.comp_id` `Category.id_comp` `Category.assoc` `Functor.map_comp` `TwoSquare.hComp_app` `Functor.whiskerRight_comp` `TwoSquare.vComp_app` `Functor.map_id`
`conjugateEquiv_comp_assoc` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Category.toCategoryStruct` `Functor.category` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv`	—	`Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `conjugateEquiv_comp`
`conjugateEquiv_counit` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.id` `Functor.map` `NatTrans.app` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `Functor.comp` `Adjunction.counit`	—	`conjugateEquiv_apply_app` `Functor.map_comp` `Category.assoc` `Adjunction.counit_naturality` `Adjunction.counit_naturality_assoc` `Adjunction.left_triangle_components_assoc`
`conjugateEquiv_counit_symm` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.id` `Functor.map` `NatTrans.app` `Functor.comp` `Adjunction.counit` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateEquiv`	—	`Equiv.right_inv` `conjugateEquiv_counit`
`conjugateEquiv_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `CategoryStruct.id`	—	`NatTrans.ext'` `conjugateEquiv_apply_app` `Functor.map_id` `Category.id_comp` `Adjunction.right_triangle_components`
`conjugateEquiv_iso` 📖	mathematical	—	`IsIso` `Functor` `Functor.category` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv`	—	`conjugateEquiv_comm` `IsIso.inv_hom_id` `IsIso.hom_inv_id`
`conjugateEquiv_leftUnitor_hom` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `Functor.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `Adjunction.comp` `Adjunction.id` `Iso.hom` `Functor.leftUnitor` `Iso.inv` `Functor.rightUnitor`	—	`Iso.inv_ext'` `NatTrans.ext'` `conjugateEquiv_apply_app` `Adjunction.comp_unit_app` `Category.id_comp` `Functor.map_id` `Adjunction.right_triangle_components` `Category.comp_id`
`conjugateEquiv_mateEquiv_vcomp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `mateEquiv` `TwoSquare.whiskerLeft` `TwoSquare.whiskerTop` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `conjugateEquiv`	—	`TwoSquare.ext` `mateEquiv_vcomp` `congr_app` `Functor.map_comp` `Category.comp_id` `Category.id_comp` `Category.assoc` `conjugateEquiv_apply_app` `Functor.whiskerRight_comp` `Functor.whiskerRight_twice` `Iso.inv_hom_id_assoc` `Functor.map_id` `Functor.whiskerLeft_twice`
`conjugateEquiv_of_iso` 📖	mathematical	—	`IsIso` `Functor` `Functor.category`	—	`conjugateEquiv_symm_iso` `Equiv.symm_apply_apply`
`conjugateEquiv_rightUnitor_hom` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `Functor.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `Adjunction.comp` `Adjunction.id` `Iso.hom` `Functor.rightUnitor` `Iso.inv` `Functor.leftUnitor`	—	`Iso.inv_ext'` `NatTrans.ext'` `conjugateEquiv_apply_app` `Adjunction.comp_unit_app` `Functor.map_id` `Category.comp_id` `Category.id_comp` `Adjunction.right_triangle_components`
`conjugateEquiv_symm_apply_app` 📖	mathematical	—	`NatTrans.app` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateEquiv` `CategoryStruct.comp` `Functor.obj` `Functor.map` `Functor.id` `Functor.comp` `Adjunction.unit` `Adjunction.counit`	—	`Functor.map_id` `Category.comp_id` `Category.id_comp`
`conjugateEquiv_symm_comm` 📖	mathematical	`CategoryStruct.comp` `Functor` `Category.toCategoryStruct` `Functor.category` `CategoryStruct.id`	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateEquiv`	—	`conjugateEquiv_symm_comp` `conjugateEquiv_symm_id`
`conjugateEquiv_symm_comp` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Category.toCategoryStruct` `Functor.category` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateEquiv`	—	`Equiv.eq_symm_apply` `conjugateEquiv_comp` `Equiv.apply_symm_apply`
`conjugateEquiv_symm_comp_assoc` 📖	mathematical	—	`CategoryStruct.comp` `Functor` `Category.toCategoryStruct` `Functor.category` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateEquiv`	—	`Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `conjugateEquiv_symm_comp`
`conjugateEquiv_symm_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateEquiv` `CategoryStruct.id`	—	`Equiv.symm_apply_eq` `conjugateEquiv_id`
`conjugateEquiv_symm_iso` 📖	mathematical	—	`IsIso` `Functor` `Functor.category` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateEquiv`	—	`conjugateEquiv_symm_comm` `IsIso.inv_hom_id` `IsIso.hom_inv_id`
`conjugateEquiv_symm_of_iso` 📖	mathematical	—	`IsIso` `Functor` `Functor.category`	—	`conjugateEquiv_iso` `Equiv.apply_symm_apply`
`conjugateEquiv_whiskerLeft` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `Adjunction.comp` `Functor.whiskerLeft` `Functor.whiskerRight`	—	`NatTrans.ext'` `Functor.congr_map` `NatTrans.naturality` `Adjunction.unit_naturality` `conjugateEquiv_apply_app` `Adjunction.comp_unit_app` `Adjunction.comp_counit_app` `Functor.map_comp` `Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `Adjunction.right_triangle_components_assoc`
`conjugateEquiv_whiskerRight` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `Adjunction.comp` `Functor.whiskerRight` `Functor.whiskerLeft`	—	`NatTrans.ext'` `conjugateEquiv_apply_app` `Adjunction.comp_unit_app` `Adjunction.comp_counit_app` `Category.assoc` `Functor.map_comp` `Adjunction.unit_naturality_assoc` `Adjunction.right_triangle_components` `Category.comp_id`
`conjugateIsoEquiv_apply_hom` 📖	mathematical	—	`Iso.hom` `Functor` `Functor.category` `DFunLike.coe` `Equiv` `Iso` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateIsoEquiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `conjugateEquiv`	—	—
`conjugateIsoEquiv_apply_inv` 📖	mathematical	—	`Iso.inv` `Functor` `Functor.category` `DFunLike.coe` `Equiv` `Iso` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateIsoEquiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `conjugateEquiv`	—	—
`conjugateIsoEquiv_symm_apply_hom` 📖	mathematical	—	`Iso.hom` `Functor` `Functor.category` `DFunLike.coe` `Equiv` `Iso` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateIsoEquiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `conjugateEquiv`	—	—
`conjugateIsoEquiv_symm_apply_inv` 📖	mathematical	—	`Iso.inv` `Functor` `Functor.category` `DFunLike.coe` `Equiv` `Iso` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateIsoEquiv` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `conjugateEquiv`	—	—
`iterated_mateEquiv_conjugateEquiv` 📖	mathematical	—	`TwoSquare.natTrans` `DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `mateEquiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `conjugateEquiv` `Adjunction.comp`	—	`NatTrans.ext'` `Functor.whiskerRight_comp` `Functor.whiskerRight_twice` `Category.assoc` `Functor.map_id` `Category.comp_id` `Category.id_comp` `conjugateEquiv_apply_app` `Adjunction.comp_unit_app` `Adjunction.comp_counit_app` `Functor.map_comp`
`iterated_mateEquiv_conjugateEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mateEquiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `Equiv.trans` `conjugateEquiv` `Adjunction.comp` `TwoSquare.equivNatTrans`	—	`TwoSquare.ext` `Functor.whiskerLeft_twice` `Category.assoc` `Functor.whiskerRight_comp` `Functor.map_id` `Category.comp_id` `Category.id_comp` `conjugateEquiv_symm_apply_app` `Adjunction.comp_unit_app` `Functor.map_comp` `Adjunction.comp_counit_app`
`mateEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `mateEquiv` `CategoryStruct.comp` `Functor` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `Functor.id` `Iso.inv` `Functor.rightUnitor` `Functor.whiskerLeft` `Adjunction.unit` `Iso.hom` `Functor.associator` `Functor.whiskerRight` `TwoSquare.natTrans` `Adjunction.counit` `Functor.leftUnitor`	—	—
`mateEquiv_conjugateEquiv_vcomp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `mateEquiv` `TwoSquare.whiskerRight` `TwoSquare.whiskerBottom` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.category` `conjugateEquiv`	—	`TwoSquare.ext` `mateEquiv_vcomp` `congr_app` `Functor.map_comp` `Category.comp_id` `Category.id_comp` `Category.assoc` `conjugateEquiv_apply_app` `Functor.whiskerRight_comp` `Functor.whiskerRight_twice` `Functor.map_id` `Functor.whiskerLeft_twice` `Iso.hom_inv_id_assoc`
`mateEquiv_counit` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.comp` `Functor.id` `Functor.map` `NatTrans.app` `DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `mateEquiv` `Adjunction.counit`	—	`Category.comp_id` `Category.id_comp` `Functor.map_comp` `Category.assoc` `Adjunction.counit_naturality` `Adjunction.counit_naturality_assoc` `Adjunction.left_triangle_components_assoc`
`mateEquiv_counit_symm` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.comp` `Functor.id` `Functor.map` `NatTrans.app` `Adjunction.counit` `DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mateEquiv`	—	`Equiv.right_inv` `mateEquiv_counit`
`mateEquiv_hcomp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TwoSquare` `Functor.comp` `EquivLike.toFunLike` `Equiv.instEquivLike` `mateEquiv` `Adjunction.comp` `TwoSquare.vComp` `TwoSquare.hComp`	—	`TwoSquare.ext` `Functor.whiskerRight_comp` `Category.assoc` `Functor.whiskerRight_twice` `Iso.inv_hom_id_assoc` `Functor.map_id` `Category.comp_id` `Category.id_comp` `Functor.whiskerLeft_twice` `Iso.hom_inv_id_assoc` `Functor.map_comp` `Adjunction.unit_naturality` `Functor.comp_map` `NatTrans.naturality`
`mateEquiv_square` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TwoSquare` `Functor.comp` `EquivLike.toFunLike` `Equiv.instEquivLike` `mateEquiv` `Adjunction.comp` `TwoSquare.hComp` `TwoSquare.vComp`	—	`mateEquiv_vcomp` `mateEquiv_hcomp`
`mateEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mateEquiv` `CategoryStruct.comp` `Functor` `Category.toCategoryStruct` `Functor.category` `Functor.comp` `Functor.id` `Iso.inv` `Functor.leftUnitor` `Functor.whiskerRight` `Adjunction.unit` `Functor.associator` `Iso.hom` `Functor.whiskerLeft` `TwoSquare.natTrans` `Adjunction.counit` `Functor.rightUnitor`	—	—
`mateEquiv_vcomp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TwoSquare` `Functor.comp` `EquivLike.toFunLike` `Equiv.instEquivLike` `mateEquiv` `TwoSquare.hComp` `TwoSquare.vComp`	—	`TwoSquare.ext` `Functor.whiskerRight_comp` `Functor.whiskerRight_twice` `Category.assoc` `Functor.map_id` `Category.comp_id` `Category.id_comp` `Functor.whiskerLeft_twice` `Iso.hom_inv_id_assoc` `Adjunction.unit_naturality` `Functor.map_comp` `Functor.comp_map` `NatTrans.naturality` `Adjunction.left_triangle_components`
`unit_conjugateEquiv` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.id` `Functor.comp` `NatTrans.app` `Adjunction.unit` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `conjugateEquiv` `Functor.map`	—	`Category.id_comp` `Category.comp_id` `unit_mateEquiv`
`unit_conjugateEquiv_symm` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.id` `Functor.comp` `NatTrans.app` `Adjunction.unit` `Functor.map` `DFunLike.coe` `Equiv` `Quiver.Hom` `Functor` `CategoryStruct.toQuiver` `Functor.category` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `conjugateEquiv`	—	`Equiv.right_inv` `unit_conjugateEquiv`
`unit_mateEquiv` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.id` `Functor.comp` `Functor.map` `NatTrans.app` `Adjunction.unit` `DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `mateEquiv`	—	`Category.comp_id` `Category.id_comp` `Adjunction.unit_naturality_assoc` `Category.assoc` `Functor.map_comp` `Functor.comp_map` `NatTrans.naturality` `Adjunction.left_triangle_components` `Functor.map_id`
`unit_mateEquiv_symm` 📖	mathematical	—	`CategoryStruct.comp` `Category.toCategoryStruct` `Functor.obj` `Functor.id` `Functor.comp` `Functor.map` `NatTrans.app` `Adjunction.unit` `DFunLike.coe` `Equiv` `TwoSquare` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mateEquiv`	—	`Equiv.right_inv` `unit_mateEquiv`

---

← Back to Index