Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-11-03 09:34
ff8432d8
View on Github →
feat: categorical sheaf condition for presieves of arrows (
#7918
)
depends on:
#7855
Estimated changes
Modified
Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
added
theorem
CategoryTheory.Equalizer.Presieve.Arrows.FirstObj.ext
added
def
CategoryTheory.Equalizer.Presieve.Arrows.FirstObj
added
theorem
CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext
added
def
CategoryTheory.Equalizer.Presieve.Arrows.SecondObj
added
theorem
CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff
added
def
CategoryTheory.Equalizer.Presieve.Arrows.firstMap
added
def
CategoryTheory.Equalizer.Presieve.Arrows.forkMap
added
def
CategoryTheory.Equalizer.Presieve.Arrows.secondMap
added
theorem
CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition
added
theorem
CategoryTheory.Equalizer.Presieve.Arrows.w