Commit 2024-02-13 09:59 b0057244

View on Github →

feat: computation of Over A for a presheaf A (#10245)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Comma/Presheaf.lean

added def CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow

added theorem CategoryTheory.OverPresheafAux.MakesOverArrow.map₁

added theorem CategoryTheory.OverPresheafAux.MakesOverArrow.map₂

added theorem CategoryTheory.OverPresheafAux.MakesOverArrow.of_arrow

added theorem CategoryTheory.OverPresheafAux.MakesOverArrow.of_yoneda_arrow

added structure CategoryTheory.OverPresheafAux.MakesOverArrow

added theorem CategoryTheory.OverPresheafAux.OverArrows.app_val

added def CategoryTheory.OverPresheafAux.OverArrows.costructuredArrowIso

added theorem CategoryTheory.OverPresheafAux.OverArrows.ext

added theorem CategoryTheory.OverPresheafAux.OverArrows.map_val

added def CategoryTheory.OverPresheafAux.OverArrows.map₁

added theorem CategoryTheory.OverPresheafAux.OverArrows.map₁_map₂

added theorem CategoryTheory.OverPresheafAux.OverArrows.map₁_val

added def CategoryTheory.OverPresheafAux.OverArrows.map₂

added theorem CategoryTheory.OverPresheafAux.OverArrows.map₂_val

added def CategoryTheory.OverPresheafAux.OverArrows.val

added theorem CategoryTheory.OverPresheafAux.OverArrows.val_mk

added def CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow

added theorem CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow_val

added theorem CategoryTheory.OverPresheafAux.OverArrows.yonedaCollectionPresheafToA_val_fst

added def CategoryTheory.OverPresheafAux.OverArrows

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.ext

added def CategoryTheory.OverPresheafAux.YonedaCollection.fst

added def CategoryTheory.OverPresheafAux.YonedaCollection.map₁

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_comp

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_fst

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_id

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_map₂

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_snd

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₁_yonedaEquivFst

added def CategoryTheory.OverPresheafAux.YonedaCollection.map₂

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_comp

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_fst

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_id

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_snd

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.map₂_yonedaEquivFst

added def CategoryTheory.OverPresheafAux.YonedaCollection.mk

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.mk_fst

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.mk_snd

added def CategoryTheory.OverPresheafAux.YonedaCollection.snd

added def CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst

added theorem CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst_eq

added def CategoryTheory.OverPresheafAux.YonedaCollection

added theorem CategoryTheory.OverPresheafAux.app_unitForward

added def CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver

added def CategoryTheory.OverPresheafAux.counit

added def CategoryTheory.OverPresheafAux.counitAux

added def CategoryTheory.OverPresheafAux.counitAuxAux

added def CategoryTheory.OverPresheafAux.counitBackward

added theorem CategoryTheory.OverPresheafAux.counitBackward_counitForward

added def CategoryTheory.OverPresheafAux.counitForward

added theorem CategoryTheory.OverPresheafAux.counitForward_counitBackward

added theorem CategoryTheory.OverPresheafAux.counitForward_naturality₁

added theorem CategoryTheory.OverPresheafAux.counitForward_naturality₂

added theorem CategoryTheory.OverPresheafAux.counitForward_val_fst

added theorem CategoryTheory.OverPresheafAux.counitForward_val_snd

added theorem CategoryTheory.OverPresheafAux.map_mkPrecomp_eqToHom

added def CategoryTheory.OverPresheafAux.restrictedYoneda

added def CategoryTheory.OverPresheafAux.restrictedYonedaObj

added def CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁

added def CategoryTheory.OverPresheafAux.toOverYonedaCompRestrictedYoneda

added def CategoryTheory.OverPresheafAux.unit

added def CategoryTheory.OverPresheafAux.unitAux

added def CategoryTheory.OverPresheafAux.unitAuxAux

added def CategoryTheory.OverPresheafAux.unitAuxAuxAux

added def CategoryTheory.OverPresheafAux.unitBackward

added theorem CategoryTheory.OverPresheafAux.unitBackward_unitForward

added def CategoryTheory.OverPresheafAux.unitForward

added theorem CategoryTheory.OverPresheafAux.unitForward_naturality₁

added theorem CategoryTheory.OverPresheafAux.unitForward_naturality₂

added theorem CategoryTheory.OverPresheafAux.unitForward_unitBackward

added def CategoryTheory.OverPresheafAux.yonedaCollectionFunctor

added def CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf

added def CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁

added def CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA

added def CategoryTheory.overEquivPresheafCostructuredArrow