Documentation Verification Report

Quadruple

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

Statistics

Metric	Count
Definitions `Quadruple`, `adj₁`, `adj₂`, `adj₃`, `leftTriple`, `op`, `rightTriple`	7
Theorems `epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app`, `epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft`, `epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app`, `epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight`, `leftTriple_adj₁`, `leftTriple_adj₂`, `op_adj₁`, `op_adj₂`, `op_adj₃`, `op_leftTriple`, `op_rightTriple`, `rightTriple_adj₁`, `rightTriple_adj₂`	13
Total	20

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
`Quadruple` 📖	CompData	—

CategoryTheory.Adjunction.Quadruple

Definitions

Name	Category	Theorems
`adj₁` 📖	CompOp	3 math math: `leftTriple_adj₁`, `op_adj₁`, `op_adj₃`
`adj₂` 📖	CompOp	3 math math: `rightTriple_adj₁`, `op_adj₂`, `leftTriple_adj₂`
`adj₃` 📖	CompOp	3 math math: `rightTriple_adj₂`, `op_adj₁`, `op_adj₃`
`leftTriple` 📖	CompOp	8 math math: `leftTriple_adj₁`, `op_rightTriple`, `op_leftTriple`, `epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft`, `epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight`, `epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app`, `leftTriple_adj₂`, `epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app`
`op` 📖	CompOp	5 math math: `op_rightTriple`, `op_leftTriple`, `op_adj₁`, `op_adj₂`, `op_adj₃`
`rightTriple` 📖	CompOp	8 math math: `rightTriple_adj₂`, `op_rightTriple`, `op_leftTriple`, `epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft`, `epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight`, `epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app`, `rightTriple_adj₁`, `epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.Triple.leftToRight` `leftTriple` `CategoryTheory.Mono` `CategoryTheory.Adjunction.Triple.rightToLeft` `rightTriple`	—	`CategoryTheory.Functor.instFullOppositeOp` `CategoryTheory.Functor.instFaithfulOppositeOp` `epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app` `CategoryTheory.Adjunction.Triple.leftToRight_op` `CategoryTheory.Adjunction.Triple.op_rightToLeft` `Equiv.forall_congr_right`
`epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Adjunction.Triple.leftToRight` `leftTriple` `CategoryTheory.Mono` `CategoryTheory.Adjunction.Triple.rightToLeft` `rightTriple`	—	`CategoryTheory.NatTrans.epi_iff_epi_app` `CategoryTheory.NatTrans.mono_iff_mono_app` `epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app`
`epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.Triple.rightToLeft` `leftTriple` `CategoryTheory.Mono` `CategoryTheory.Adjunction.Triple.leftToRight` `rightTriple`	—	`CategoryTheory.Functor.isIso_whiskerLeft` `CategoryTheory.Adjunction.counit_isIso_of_R_fully_faithful` `CategoryTheory.Adjunction.Triple.rightToLeft_eq_counits` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.NatIso.isIso_inv_app` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.IsIso.inv_isIso` `Equiv.comp_injective` `CategoryTheory.Adjunction.homEquiv_naturality_left` `Equiv.injective_comp` `CategoryTheory.Adjunction.homEquiv_symm_id` `CategoryTheory.Adjunction.homEquiv_naturality_right_symm` `Equiv.apply_symm_apply` `CategoryTheory.Adjunction.homEquiv_id`
`epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Adjunction.Triple.rightToLeft` `leftTriple` `CategoryTheory.Mono` `CategoryTheory.Adjunction.Triple.leftToRight` `rightTriple`	—	`CategoryTheory.NatTrans.epi_iff_epi_app` `CategoryTheory.NatTrans.mono_iff_mono_app` `epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app`
`leftTriple_adj₁` 📖	mathematical	—	`CategoryTheory.Adjunction.Triple.adj₁` `leftTriple` `adj₁`	—	—
`leftTriple_adj₂` 📖	mathematical	—	`CategoryTheory.Adjunction.Triple.adj₂` `leftTriple` `adj₂`	—	—
`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`	—	—
`op_adj₃` 📖	mathematical	—	`adj₃` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `op` `CategoryTheory.Adjunction.op` `adj₁`	—	—
`op_leftTriple` 📖	mathematical	—	`leftTriple` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `op` `CategoryTheory.Adjunction.Triple.op` `rightTriple`	—	—
`op_rightTriple` 📖	mathematical	—	`rightTriple` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `op` `CategoryTheory.Adjunction.Triple.op` `leftTriple`	—	—
`rightTriple_adj₁` 📖	mathematical	—	`CategoryTheory.Adjunction.Triple.adj₁` `rightTriple` `adj₂`	—	—
`rightTriple_adj₂` 📖	mathematical	—	`CategoryTheory.Adjunction.Triple.adj₂` `rightTriple` `adj₃`	—	—

---

← Back to Index