Commit 2023-06-03 07:53 eb679e02

View on Github →

refactor: fixes to material on sheaves and stalks (#4571) Mostly this is installing the Opposite.rec' induction principle as the default @[eliminator], but also many other fixes and removing unnecessary steps from proofs.

Estimated changes

Modified Mathlib/AlgebraicGeometry/PresheafedSpace.lean

Modified Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

Modified Mathlib/AlgebraicGeometry/SheafedSpace.lean

Modified Mathlib/AlgebraicGeometry/Stalks.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

Modified Mathlib/CategoryTheory/Limits/Creates.lean

added theorem CategoryTheory.hasColimits_of_hasColimits_createsColimits

added theorem CategoryTheory.hasLimits_of_hasLimits_createsLimits

deleted theorem CategoryTheory.has_colimits_of_has_colimits_creates_colimits

deleted theorem CategoryTheory.has_limits_of_has_limits_creates_limits

Modified Mathlib/CategoryTheory/Monad/Limits.lean

added theorem CategoryTheory.hasColimits_of_reflective

added theorem CategoryTheory.hasLimits_of_reflective

deleted theorem CategoryTheory.has_colimits_of_reflective

deleted theorem CategoryTheory.has_limits_of_reflective

Modified Mathlib/CategoryTheory/Sites/Limits.lean

Modified Mathlib/Data/Opposite.lean

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Modified Mathlib/Topology/Sheaves/Limits.lean

Modified Mathlib/Topology/Sheaves/Presheaf.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean