Documentation Verification Report

Reflection

📁 Source: Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean

Statistics

Metric	Count
Definitions `closed`, `monoidalClosed`	2
Theorems `instIsIsoAppUnitObjIhom`, `instIsIsoMapTensorHomAppUnit`, `isIso_tfae`	3
Total	5

CategoryTheory.Monoidal.Reflective

Definitions

Name	Category	Theorems
`closed` 📖	CompOp	—
`monoidalClosed` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoAppUnitObjIhom` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.ihom` `CategoryTheory.MonoidalClosed.closed` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit`	—	`List.TFAE.out` `isIso_tfae` `instIsIsoMapTensorHomAppUnit`
`instIsIsoMapTensorHomAppUnit` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit`	—	`CategoryTheory.whisker_eq` `CategoryTheory.Functor.LaxMonoidal.μ_natural` `CategoryTheory.Functor.Monoidal.δ_μ_assoc` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Functor.Monoidal.instIsIsoδ` `CategoryTheory.MonoidalCategory.tensor_isIso` `CategoryTheory.Adjunction.instIsIsoMapAppUnitOfFaithfulOfFull` `CategoryTheory.Functor.Monoidal.instIsIsoμ`
`isIso_tfae` 📖	mathematical	—	`List.TFAE`	—	`CategoryTheory.BraidedCategory.braiding_naturality` `CategoryTheory.MonoidalCategory.id_tensorHom` `CategoryTheory.Iso.eq_comp_inv` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.μ_iso_of_reflective` `CategoryTheory.Monad.isSplitMono_iff_isIso_unit` `CategoryTheory.isIso_iff_isIso_coyoneda_map` `CategoryTheory.types_ext` `CategoryTheory.Adjunction.homEquiv_unit` `CategoryTheory.Adjunction.homEquiv_counit` `CategoryTheory.Adjunction.counit_naturality` `CategoryTheory.Adjunction.left_triangle_components_assoc` `CategoryTheory.isIso_iff_bijective` `CategoryTheory.BraidedCategory.braiding_naturality_right_assoc` `CategoryTheory.SymmetricCategory.symmetry_assoc` `CategoryTheory.types_comp` `CategoryTheory.IsIso.comp_isIso'` `CategoryTheory.ihom.coev_naturality_assoc` `CategoryTheory.MonoidalCategory.whiskerLeft_comp` `CategoryTheory.ihom.ev_naturality` `CategoryTheory.ihom.ev_naturality_assoc` `CategoryTheory.ihom.ev_coev_assoc` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Functor.map_preimage` `CategoryTheory.Adjunction.unit_naturality_assoc` `CategoryTheory.Adjunction.right_triangle_components` `CategoryTheory.IsIso.of_isIso_comp_right` `CategoryTheory.isIso_iff_isIso_yoneda_map` `forall_swap` `Function.comp_assoc` `Equiv.eq_comp_symm` `CategoryTheory.MonoidalClosed.coev_app_comp_pre_app_assoc` `List.tfae_of_cycle`

---

← Back to Index