Theorem CategoryTheory.Adjunction.hasExactColimitsOfShape

Modification history

2026-10-30 15:08

Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean

chore(CategoryTheory): deprecate `leftExactFunctor` (#45418) …

Modified CategoryTheory.Adjunction.hasExactColimitsOfShape View on Github →

2025-01-02 12:06

Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean

feat(CategoryTheory/Sites): categories of sheaves are Grothendieck abelian (#19986) …

Added CategoryTheory.Adjunction.hasExactColimitsOfShape View on Github →