Theorem CategoryTheory.Presieve.FactorsThruAlong.pullbackArrows

Modification history

2025-08-30 20:46

Mathlib/CategoryTheory/Sites/Coverage.lean

refactor(CategoryTheory/Sites/Sieves): avoid `HasPullbacks C` in `Presieve.pullbackArrows` (#29085) …

Modified CategoryTheory.Presieve.FactorsThruAlong.pullbackArrows View on Github →

2025-07-08 19:42

Mathlib/CategoryTheory/Sites/Coverage.lean

feat(CategoryTheory/Sites): `0`-hypercovers (#26888) …

Added CategoryTheory.Presieve.FactorsThruAlong.pullbackArrows View on Github →