Condition for sheaf equivalence

Stream: maths

[Kenny Lau]

image.png

CategoryTheory.Functor.IsDenseSubsite.sheafEquiv contains the assumption [∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A], which I think might be too strong.

@Robin Carlier would you know about something like this?

[Kenny Lau]

basically, I think this hypothesis is not satisfied in the case where C = AffineScheme.{u}, D = Scheme.{u}, G = inclusion, and J, K are the Zariski topologies, and A = Type u

[Joël Riou]

A different approch to sheafification based on 1-hypercovers started by @Christian Merten #26326 should solve this issue.

[Kenny Lau]

thanks!

[Robin Carlier]

Joël answered in a much better way than I could have :sweat_smile: