Documentation Verification Report

Hom

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

Statistics

Metric	Count
Definitions `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`, `Hom`	66
Theorems `hom_map`, `hom_obj`	2
Total	68

CategoryTheory.Bicategory.Adj

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Bicategory.InducedBicategory

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	1 math math: `bicategory_Hom`

CategoryTheory.Cat

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	3 math math: `Hom₂.eqToHom_toNatTrans`, `CategoryTheory.Grothendieck.map_map_fiber`, `eqToHom_app`

CategoryTheory.CatEnrichedOrdinary

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Center

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Comon

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Dial

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.DifferentialObject

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Endofunctor.Algebra

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.EnrichedCategory

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	79 math math: `CategoryTheory.eHom_whisker_cancel`, `CategoryTheory.Iso.eHomCongr_refl`, `CategoryTheory.EnrichedOrdinaryCategory.homEquiv_comp`, `CategoryTheory.Iso.eHomCongr_inv_comp_assoc`, `CategoryTheory.e_comp_id`, `CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_homEquiv_symm`, `CategoryTheory.eHomEquiv_id`, `CategoryTheory.eHomWhiskerRight_comp`, `CategoryTheory.TransportEnrichment.eId_eq`, `CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition'`, `CategoryTheory.Iso.eHomCongr_hom`, `CategoryTheory.e_id_comp`, `CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition`, `CategoryTheory.ForgetEnrichment.equivFunctor_map`, `CategoryTheory.ForgetEnrichment.equivInverse_map`, `CategoryTheory.eHomWhiskerRight_comp_assoc`, `CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition_assoc`, `CategoryTheory.eHomWhiskerLeft_comp`, `CategoryTheory.Iso.eHomCongr_symm`, `CategoryTheory.eHomFunctor_obj_obj`, `CategoryTheory.eHom_whisker_exchange_assoc`, `CategoryTheory.Iso.eHomCongr_comp_assoc`, `CategoryTheory.EnrichedFunctor.forget_map`, `comp_id`, `CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π`, `CategoryTheory.e_comp_id_assoc`, `id_comp`, `CategoryTheory.EnrichedFunctor.id_map`, `CategoryTheory.eComp_eHomWhiskerRight`, `CategoryTheory.EnrichedFunctor.comp_map`, `CategoryTheory.e_assoc_assoc`, `CategoryTheory.eComp_eHomWhiskerLeft_assoc`, `CategoryTheory.e_assoc'`, `CategoryTheory.EnrichedOrdinaryCategory.homEquiv_id`, `CategoryTheory.Iso.eHomCongr_trans`, `CategoryTheory.eHomFunctor_map_app`, `CategoryTheory.EnrichedFunctor.map_id`, `CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_map`, `CategoryTheory.ForgetEnrichment.homOf_comp`, `CategoryTheory.eHom_whisker_cancel_assoc`, `CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_homEquiv`, `CategoryTheory.e_id_comp_assoc`, `CategoryTheory.ForgetEnrichment.homTo_comp`, `CategoryTheory.eComp_op_eq_assoc`, `CategoryTheory.eHomWhiskerLeft_id`, `CategoryTheory.TransportEnrichment.eComp_eq`, `CategoryTheory.eComp_eHomWhiskerRight_assoc`, `CategoryTheory.EnrichedFunctor.map_comp_assoc`, `CategoryTheory.tensorHom_eComp_op_eq_assoc`, `CategoryTheory.CatEnriched.comp_eq`, `CategoryTheory.eComp_eHomWhiskerLeft`, `CategoryTheory.tensorHom_eComp_op_eq`, `CategoryTheory.EnrichedFunctor.map_comp`, `CategoryTheory.eHomWhiskerRight_id`, `CategoryTheory.GradedNatTrans.naturality_assoc`, `CategoryTheory.Iso.eHomCongr_comp`, `CategoryTheory.eHom_whisker_cancel_inv_assoc`, `CategoryTheory.eHom_whisker_cancel_inv`, `CategoryTheory.CatEnriched.id_eq`, `CategoryTheory.eHomEquiv_comp`, `CategoryTheory.MonoidalClosed.enrichedCategorySelf_hom`, `CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π_assoc`, `CategoryTheory.Iso.eHomCongr_inv`, `CategoryTheory.EnrichedCat.whiskerRight_out_app`, `CategoryTheory.eHomEquiv_comp_assoc`, `CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition'_assoc`, `CategoryTheory.e_assoc'_assoc`, `CategoryTheory.Enriched.FunctorCategory.enrichedComp_π`, `CategoryTheory.Iso.eHomCongr_inv_comp`, `assoc`, `CategoryTheory.eHomWhiskerLeft_comp_assoc`, `CategoryTheory.EnrichedFunctor.map_id_assoc`, `CategoryTheory.eComp_op_eq`, `CategoryTheory.e_assoc`, `CategoryTheory.GradedNatTrans.naturality`, `CategoryTheory.enrichedNatTransYoneda_map_app`, `CategoryTheory.Enriched.FunctorCategory.diagram_obj_obj`, `CategoryTheory.eHom_whisker_exchange`, `CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_map`

CategoryTheory.Factorisation

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.FreeBicategory

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.FreeMonoidalCategory

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	11 math math: `mk_ρ_hom`, `mk_id`, `mk_whiskerRight`, `mk_comp`, `mk_l_inv`, `mk_l_hom`, `mk_α_hom`, `mk_ρ_inv`, `mk_whiskerLeft`, `mk_α_inv`, `mk_tensor`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	2 math math: `hom_map`, `hom_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_map` 📖	mathematical	—	`map` `Opposite` `CategoryTheory.uniformProd` `CategoryTheory.Category.opposite` `CategoryTheory.types` `hom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `Quiver.Hom`	—	—
`hom_obj` 📖	mathematical	—	`obj` `Opposite` `CategoryTheory.uniformProd` `CategoryTheory.Category.opposite` `CategoryTheory.types` `hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop`	—	—

CategoryTheory.Grothendieck

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.GrothendieckTopology.OneHypercover

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

CategoryTheory.GrothendieckTopology.Point

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Idempotents.Karoubi

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.InducedCategory

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.InjectiveResolution

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Join

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

CategoryTheory.LaxMonoidalFunctor

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.CategoricalPullback

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.CategoricalPullback.CatCommSqOver

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.ColimitPresentation.Total

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.FormalCoproduct

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.WalkingCospan

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

CategoryTheory.Limits.WalkingMulticospan

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.WalkingMultispan

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.WalkingParallelFamily

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.WalkingReflexivePair

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.WalkingSpan

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

CategoryTheory.Limits.WidePullbackShape

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Limits.WidePushoutShape

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.LocalizerMorphism.LeftResolution

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.LocalizerMorphism.RightResolution

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Mat_

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

CategoryTheory.Mod_

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Mon

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	1 math math: `hom_injective`

CategoryTheory.Monad.Algebra

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	1 math math: `CategoryTheory.Monad.adj_counit`

CategoryTheory.MonoidalCategory.DayFunctor

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.MorphismProperty.Comma

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.MorphismProperty.LeftFraction.Localization

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

CategoryTheory.Oplax.OplaxTrans

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Oplax.StrongTrans

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Pairwise

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.PreGaloisCategory.PointedGaloisObject

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.PreOneHypercover

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.PreZeroHypercover

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Precoverage.ZeroHypercover

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

CategoryTheory.ProjectiveResolution

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Pseudofunctor.CoGrothendieck

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Pseudofunctor.DescentData

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Pseudofunctor.Grothendieck

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Pseudofunctor.StrongTrans

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Quotient

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

CategoryTheory.RelCat

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.ShortComplex.SnakeInput

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.SimplicialThickening.SimplicialCategory

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	3 math math: `comp_id`, `assoc`, `id_comp`

CategoryTheory.SingleFunctors

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Square

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.Triangulated.SpectralObject

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CategoryTheory.WithInitial

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

CategoryTheory.WithTerminal

Definitions

Name	Category	Theorems
`Hom` 📖	CompOp	—

---

← Back to Index