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