One

📁 Source: Mathlib/CategoryTheory/ComposableArrows/One.lean

Statistics

Metric	Count
Definitions functorArrows, mapFunctorArrows	2
Theorems functorArrows_map, functorArrows_obj, mapFunctorArrows_app	3
Total	5

CategoryTheory.ComposableArrows

Definitions

Name	Category	Theorems
functorArrows 📖	CompOp	10 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₃, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁, mapFunctorArrows_app, CategoryTheory.Triangulated.SpectralObject.distinguished', CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ', CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂, functorArrows_map, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃, functorArrows_obj
mapFunctorArrows 📖	CompOp	5 math math: CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁, mapFunctorArrows_app, CategoryTheory.Triangulated.SpectralObject.distinguished', CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorArrows_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder functorArrows homMk₁ mk₁ CategoryTheory.Functor.obj map' CategoryTheory.NatTrans.app	—	—
functorArrows_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder functorArrows mk₁ map'	—	—
mapFunctorArrows_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder functorArrows mapFunctorArrows homMk₁ CategoryTheory.Functor.obj map'	—	—

---

← Back to Index