Commit 2023-11-03 20:42 dfb12831

View on Github →

feat(CategoryTheory): inductive construction of composable arrows (#8146)

Estimated changes

Modified Mathlib/AlgebraicTopology/Nerve.lean

added theorem CategoryTheory.Nerve.δ₀_eq

Modified Mathlib/CategoryTheory/ComposableArrows.lean

added def CategoryTheory.ComposableArrows.Precomp.map

added theorem CategoryTheory.ComposableArrows.Precomp.map_comp

added theorem CategoryTheory.ComposableArrows.Precomp.map_id

added theorem CategoryTheory.ComposableArrows.Precomp.map_one_one

added theorem CategoryTheory.ComposableArrows.Precomp.map_one_succ

added theorem CategoryTheory.ComposableArrows.Precomp.map_succ_succ

added theorem CategoryTheory.ComposableArrows.Precomp.map_zero_one'

added theorem CategoryTheory.ComposableArrows.Precomp.map_zero_one

added theorem CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ

added theorem CategoryTheory.ComposableArrows.Precomp.map_zero_zero

added def CategoryTheory.ComposableArrows.Precomp.obj

added theorem CategoryTheory.ComposableArrows.Precomp.obj_one

added theorem CategoryTheory.ComposableArrows.Precomp.obj_succ

added theorem CategoryTheory.ComposableArrows.Precomp.obj_zero

added def CategoryTheory.ComposableArrows.mk₂

added def CategoryTheory.ComposableArrows.mk₃

added def CategoryTheory.ComposableArrows.precomp

added theorem CategoryTheory.ComposableArrows.precomp_δ₀

added def CategoryTheory.ComposableArrows.whiskerLeft

added def CategoryTheory.ComposableArrows.whiskerLeftFunctor

added def CategoryTheory.ComposableArrows.δ₀Functor

added def CategoryTheory.Functor.mapComposableArrows

deleted theorem CategoryTheory.nerve_obj_eq_composableArrows

added def Fin.succFunctor