Commit 2021-10-25 22:55 c363ad63

View on Github →

feat(category_theory/sites/*): Cover preserving functors (#9691) Split from #9650

  • Defined cover_preserving functors as functors that push covering sieves to covering sieves.
  • Defined compatible_preserving functors as functors that push compatible families to compatible families.
  • Proved that functors that are both cover_preserving and compatible_preserving pulls sheaves to sheaves.

Estimated changes