Commit 2025-09-11 17:39 b4ccfa4a

View on Github →

chore(CategoryTheory/Sites): move PreOneHypercover.Homotopy in new file (#29553) In preparation for more material. The module docstring is written in anticipation of #29551.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Hypercover/Homotopy.lean

added theorem CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy

added theorem CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq

added structure CategoryTheory.PreOneHypercover.Homotopy

added theorem CategoryTheory.PreOneHypercover.exists_nonempty_homotopy

added theorem CategoryTheory.PreOneHypercover.sieve₀_cylinder

added theorem CategoryTheory.PreOneHypercover.sieve₁'_cylinder

added theorem CategoryTheory.PreOneHypercover.toPullback_cylinder

Modified Mathlib/CategoryTheory/Sites/Hypercover/One.lean

deleted theorem CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy

deleted theorem CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq

deleted structure CategoryTheory.PreOneHypercover.Homotopy

deleted theorem CategoryTheory.PreOneHypercover.exists_nonempty_homotopy

deleted theorem CategoryTheory.PreOneHypercover.sieve₀_cylinder

deleted theorem CategoryTheory.PreOneHypercover.sieve₁'_cylinder

deleted theorem CategoryTheory.PreOneHypercover.toPullback_cylinder