Triple

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

Statistics

Metric	Count
Definitions Triple, adj₁, adj₂, fullyFaithfulEquiv, leftToRight, op, rightToLeft	7
Theorems adj₁_counit_app_rightToLeft_app, adj₁_counit_app_rightToLeft_app_assoc, epi_rightToLeft_app_iff, epi_rightToLeft_app_iff_epi_map_adj₁_unit_app, epi_rightToLeft_app_iff_epi_map_adj₂_counit_app, isIso_unit_iff_isIso_counit, leftToRight_app, leftToRight_app_map_adj₁_unit_app, leftToRight_app_map_adj₁_unit_app_assoc, leftToRight_app_obj, leftToRight_app_obj_assoc, leftToRight_eq_counits, leftToRight_op, map_adj₂_counit_app_leftToRight_app, map_rightToLeft_app, map_rightToLeft_app_assoc, mono_leftToRight_app_iff, mono_leftToRight_app_iff_mono_adj₁_counit_app, mono_leftToRight_app_iff_mono_adj₂_unit_app, op_adj₁, op_adj₂, op_rightToLeft, rightToLeft_app_adj₂_unit_app, rightToLeft_app_adj₂_unit_app_assoc, rightToLeft_eq_counits, rightToLeft_eq_units, whiskerLeft_leftToRight, whiskerLeft_leftToRight_assoc, whiskerRight_rightToLeft, whiskerRight_rightToLeft_assoc	30
Total	37

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
Triple 📖	CompData	—

CategoryTheory.Adjunction.Triple

Definitions

Name	Category	Theorems
adj₁ 📖	CompOp	28 math math: isIso_unit_iff_isIso_counit, epi_rightToLeft_app_iff_epi_map_adj₁_unit_app, CategoryTheory.Adjunction.Quadruple.leftTriple_adj₁, rightToLeft_eq_units, adj₁_counit_app_rightToLeft_app, op_adj₁, mono_leftToRight_app_iff_mono_adj₁_counit_app, whiskerRight_rightToLeft_assoc, op_adj₂, leftToRight_app_obj, rightToLeft_eq_counits, adj₁_counit_app_rightToLeft_app_assoc, epi_rightToLeft_app_iff, leftToRight_app_map_adj₁_unit_app_assoc, leftToRight_eq_counits, CategoryTheory.Adjunction.Quadruple.rightTriple_adj₁, map_rightToLeft_app, whiskerRight_rightToLeft, whiskerLeft_leftToRight_assoc, map_adj₂_counit_app_leftToRight_app, map_rightToLeft_app_assoc, leftToRight_app, rightToLeft_app_adj₂_unit_app, leftToRight_app_obj_assoc, whiskerLeft_leftToRight, leftToRight_app_map_adj₁_unit_app, rightToLeft_app_adj₂_unit_app_assoc, mono_leftToRight_app_iff
adj₂ 📖	CompOp	28 math math: isIso_unit_iff_isIso_counit, CategoryTheory.Adjunction.Quadruple.rightTriple_adj₂, rightToLeft_eq_units, adj₁_counit_app_rightToLeft_app, op_adj₁, whiskerRight_rightToLeft_assoc, op_adj₂, leftToRight_app_obj, rightToLeft_eq_counits, adj₁_counit_app_rightToLeft_app_assoc, epi_rightToLeft_app_iff, leftToRight_app_map_adj₁_unit_app_assoc, leftToRight_eq_counits, map_rightToLeft_app, whiskerRight_rightToLeft, whiskerLeft_leftToRight_assoc, map_adj₂_counit_app_leftToRight_app, map_rightToLeft_app_assoc, leftToRight_app, mono_leftToRight_app_iff_mono_adj₂_unit_app, epi_rightToLeft_app_iff_epi_map_adj₂_counit_app, rightToLeft_app_adj₂_unit_app, leftToRight_app_obj_assoc, whiskerLeft_leftToRight, leftToRight_app_map_adj₁_unit_app, rightToLeft_app_adj₂_unit_app_assoc, mono_leftToRight_app_iff, CategoryTheory.Adjunction.Quadruple.leftTriple_adj₂
fullyFaithfulEquiv 📖	CompOp	—
leftToRight 📖	CompOp	17 math math: mono_leftToRight_app_iff_mono_adj₁_counit_app, CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft, leftToRight_app_obj, CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight, CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app, leftToRight_op, leftToRight_app_map_adj₁_unit_app_assoc, leftToRight_eq_counits, whiskerLeft_leftToRight_assoc, map_adj₂_counit_app_leftToRight_app, leftToRight_app, mono_leftToRight_app_iff_mono_adj₂_unit_app, leftToRight_app_obj_assoc, whiskerLeft_leftToRight, leftToRight_app_map_adj₁_unit_app, mono_leftToRight_app_iff, CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app
op 📖	CompOp	6 math math: op_adj₁, CategoryTheory.Adjunction.Quadruple.op_rightTriple, CategoryTheory.Adjunction.Quadruple.op_leftTriple, op_rightToLeft, op_adj₂, leftToRight_op
rightToLeft 📖	CompOp	18 math math: epi_rightToLeft_app_iff_epi_map_adj₁_unit_app, rightToLeft_eq_units, adj₁_counit_app_rightToLeft_app, whiskerRight_rightToLeft_assoc, CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft, op_rightToLeft, CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight, rightToLeft_eq_counits, CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app, adj₁_counit_app_rightToLeft_app_assoc, epi_rightToLeft_app_iff, map_rightToLeft_app, whiskerRight_rightToLeft, map_rightToLeft_app_assoc, epi_rightToLeft_app_iff_epi_map_adj₂_counit_app, rightToLeft_app_adj₂_unit_app, rightToLeft_app_adj₂_unit_app_assoc, CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adj₁_counit_app_rightToLeft_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit adj₁ rightToLeft CategoryTheory.Functor.map adj₂	—	CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp map_rightToLeft_app CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Adjunction.instIsIsoAppUnitObjOfFaithfulOfFull CategoryTheory.Adjunction.right_triangle_components_assoc CategoryTheory.Adjunction.unit_naturality
adj₁_counit_app_rightToLeft_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₁ rightToLeft CategoryTheory.Functor.map adj₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' adj₁_counit_app_rightToLeft_app
epi_rightToLeft_app_iff 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.NatTrans.app rightToLeft CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₂ CategoryTheory.Adjunction.unit adj₁	—	CategoryTheory.Adjunction.isLeftAdjoint map_rightToLeft_app CategoryTheory.Functor.map_epi CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint epi_rightToLeft_app_iff_epi_map_adj₁_unit_app CategoryTheory.Functor.map_comp CategoryTheory.Adjunction.right_triangle_components_assoc CategoryTheory.epi_comp CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful
epi_rightToLeft_app_iff_epi_map_adj₁_unit_app 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.NatTrans.app rightToLeft CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.Adjunction.unit adj₁	—	CategoryTheory.epi_comp_iff_of_isIso CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful rightToLeft_app_adj₂_unit_app
epi_rightToLeft_app_iff_epi_map_adj₂_counit_app 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.NatTrans.app rightToLeft CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.Adjunction.counit adj₂	—	CategoryTheory.epi_comp_iff_of_epi CategoryTheory.Adjunction.counit_epi_of_R_faithful adj₁_counit_app_rightToLeft_app
isIso_unit_iff_isIso_counit 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit adj₁ CategoryTheory.Adjunction.counit adj₂	—	CategoryTheory.Adjunction.isIso_counit_of_iso CategoryTheory.Adjunction.isIso_unit_of_iso
leftToRight_app 📖	mathematical	—	CategoryTheory.NatTrans.app leftToRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit adj₂ CategoryTheory.inv CategoryTheory.Functor.map adj₁ CategoryTheory.Functor.map_isIso CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful	—	CategoryTheory.Functor.map_isIso CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Adjunction.unit_isIso_of_L_fully_faithful CategoryTheory.Functor.inv_whiskerRight CategoryTheory.NatIso.isIso_inv_app CategoryTheory.Functor.map_inv CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
leftToRight_app_map_adj₁_unit_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.NatTrans.app leftToRight CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Adjunction.unit adj₁ adj₂	—	CategoryTheory.Functor.map_isIso CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful leftToRight_app CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.Category.comp_id
leftToRight_app_map_adj₁_unit_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app leftToRight CategoryTheory.Functor.map CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit adj₁ adj₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftToRight_app_map_adj₁_unit_app
leftToRight_app_obj 📖	mathematical	—	CategoryTheory.NatTrans.app leftToRight CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₁ CategoryTheory.Adjunction.unit adj₂	—	Equiv.apply_symm_apply CategoryTheory.Adjunction.homEquiv_symm_apply CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.Adjunction.left_triangle_components CategoryTheory.Adjunction.homEquiv_apply CategoryTheory.Functor.map_isIso CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful leftToRight_app CategoryTheory.Functor.map_inv CategoryTheory.Category.comp_id CategoryTheory.IsIso.eq_inv_of_hom_inv_id CategoryTheory.Adjunction.right_triangle_components
leftToRight_app_obj_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app leftToRight CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₁ CategoryTheory.Adjunction.unit adj₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftToRight_app_obj
leftToRight_eq_counits 📖	mathematical	—	leftToRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor.leftUnitor CategoryTheory.inv CategoryTheory.Functor.whiskerRight CategoryTheory.Adjunction.counit adj₂ CategoryTheory.Functor.isIso_whiskerRight CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerLeft adj₁ CategoryTheory.Functor.rightUnitor	—	CategoryTheory.NatTrans.ext' CategoryTheory.Functor.isIso_whiskerRight CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.NatIso.isIso_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.IsIso.comp_inv_eq CategoryTheory.Category.assoc CategoryTheory.IsIso.eq_inv_comp CategoryTheory.Functor.whiskerRight_app CategoryTheory.Adjunction.instIsIsoAppCounitOfFullOfFaithful CategoryTheory.Iso.eq_comp_inv CategoryTheory.Adjunction.counit_naturality CategoryTheory.Iso.comp_hom_eq_id CategoryTheory.Adjunction.left_triangle_components CategoryTheory.Functor.map_comp CategoryTheory.Adjunction.left_triangle_components_assoc
leftToRight_op 📖	mathematical	—	leftToRight Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op op CategoryTheory.Functor.instFullOppositeOp CategoryTheory.Functor.instFaithfulOppositeOp CategoryTheory.NatTrans.op	—	CategoryTheory.NatTrans.ext' CategoryTheory.Functor.instFullOppositeOp CategoryTheory.Functor.instFaithfulOppositeOp leftToRight.eq_1 CategoryTheory.Functor.isIso_whiskerRight CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful leftToRight_eq_counits CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.isIso_op CategoryTheory.Functor.map_isIso CategoryTheory.NatIso.isIso_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.inv_whiskerRight CategoryTheory.Category.assoc CategoryTheory.Functor.map_inv CategoryTheory.op_inv
map_adj₂_counit_app_leftToRight_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit adj₂ leftToRight adj₁	—	CategoryTheory.NatTrans.naturality leftToRight_app_obj CategoryTheory.Category.assoc CategoryTheory.Adjunction.right_triangle_components CategoryTheory.Category.comp_id
map_rightToLeft_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.NatTrans.app rightToLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₂ CategoryTheory.Adjunction.unit adj₁	—	CategoryTheory.congr_app whiskerRight_rightToLeft
map_rightToLeft_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app rightToLeft CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₂ CategoryTheory.Adjunction.unit adj₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_rightToLeft_app
mono_leftToRight_app_iff 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.NatTrans.app leftToRight CategoryTheory.Functor.comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₁ CategoryTheory.Adjunction.unit adj₂	—	leftToRight_app_obj mono_leftToRight_app_iff_mono_adj₂_unit_app CategoryTheory.Adjunction.instIsIsoAppCounitObjOfFaithfulOfFull
mono_leftToRight_app_iff_mono_adj₁_counit_app 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.NatTrans.app leftToRight CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₁	—	map_adj₂_counit_app_leftToRight_app CategoryTheory.mono_comp_iff_of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Adjunction.instIsIsoAppCounitOfFullOfFaithful
mono_leftToRight_app_iff_mono_adj₂_unit_app 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.NatTrans.app leftToRight CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit adj₂	—	leftToRight_app_map_adj₁_unit_app CategoryTheory.mono_comp_iff_of_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful
op_adj₁ 📖	mathematical	—	adj₁ Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op op CategoryTheory.Adjunction.op adj₂	—	—
op_adj₂ 📖	mathematical	—	adj₂ Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op op CategoryTheory.Adjunction.op adj₁	—	—
op_rightToLeft 📖	mathematical	—	rightToLeft Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op op CategoryTheory.Functor.instFullOppositeOp CategoryTheory.Functor.instFaithfulOppositeOp CategoryTheory.NatTrans.op	—	CategoryTheory.NatTrans.ext' CategoryTheory.Functor.instFullOppositeOp CategoryTheory.Functor.instFaithfulOppositeOp CategoryTheory.Functor.isIso_whiskerLeft CategoryTheory.Adjunction.unit_isIso_of_L_fully_faithful rightToLeft_eq_units CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful rightToLeft_eq_counits CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.isIso_op CategoryTheory.NatIso.isIso_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.inv_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.op_inv
rightToLeft_app_adj₂_unit_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.NatTrans.app rightToLeft CategoryTheory.Functor.id CategoryTheory.Adjunction.unit adj₂ CategoryTheory.Functor.map adj₁	—	CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp map_rightToLeft_app CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Adjunction.instIsIsoAppCounitObjOfFaithfulOfFull CategoryTheory.Adjunction.left_triangle_components CategoryTheory.Category.comp_id CategoryTheory.Adjunction.counit_naturality
rightToLeft_app_adj₂_unit_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.NatTrans.app rightToLeft CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Adjunction.unit adj₂ CategoryTheory.Functor.map adj₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightToLeft_app_adj₂_unit_app
rightToLeft_eq_counits 📖	mathematical	—	rightToLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor.rightUnitor CategoryTheory.inv CategoryTheory.Functor.whiskerLeft CategoryTheory.Adjunction.counit adj₁ CategoryTheory.Functor.isIso_whiskerLeft CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerRight adj₂ CategoryTheory.Iso.hom CategoryTheory.Functor.leftUnitor	—	CategoryTheory.NatTrans.ext' CategoryTheory.Functor.isIso_whiskerLeft CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful CategoryTheory.Functor.map_injective CategoryTheory.Functor.FullyFaithful.map_preimage CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Functor.inv_whiskerLeft CategoryTheory.NatIso.isIso_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.Adjunction.inv_counit_map CategoryTheory.Adjunction.instIsIsoAppCounitOfFullOfFaithful CategoryTheory.Adjunction.unit_naturality
rightToLeft_eq_units 📖	mathematical	—	rightToLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor.leftUnitor CategoryTheory.Functor.whiskerRight CategoryTheory.Adjunction.unit adj₁ CategoryTheory.Iso.hom CategoryTheory.Functor.associator CategoryTheory.inv CategoryTheory.Functor.whiskerLeft adj₂ CategoryTheory.Functor.isIso_whiskerLeft CategoryTheory.Adjunction.unit_isIso_of_L_fully_faithful CategoryTheory.Functor.rightUnitor	—	CategoryTheory.NatTrans.ext' CategoryTheory.Functor.isIso_whiskerLeft CategoryTheory.Adjunction.unit_isIso_of_L_fully_faithful CategoryTheory.Functor.map_injective CategoryTheory.Functor.FullyFaithful.map_preimage CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.Functor.inv_whiskerLeft CategoryTheory.NatIso.isIso_inv_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.Adjunction.inv_map_unit CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful CategoryTheory.Adjunction.counit_naturality
whiskerLeft_leftToRight 📖	mathematical	—	CategoryTheory.Functor.whiskerLeft leftToRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₁ CategoryTheory.Adjunction.unit adj₂	—	CategoryTheory.NatTrans.ext' leftToRight_app_obj
whiskerLeft_leftToRight_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerLeft leftToRight CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₁ CategoryTheory.Adjunction.unit adj₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_leftToRight
whiskerRight_rightToLeft 📖	mathematical	—	CategoryTheory.Functor.whiskerRight rightToLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₂ CategoryTheory.Adjunction.unit adj₁	—	CategoryTheory.Functor.FullyFaithful.map_preimage
whiskerRight_rightToLeft_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskerRight rightToLeft CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adj₂ CategoryTheory.Adjunction.unit adj₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_rightToLeft

---

← Back to Index