The equalizer diagram sheaf condition for a presieve

In Mathlib/CategoryTheory/Sites/IsSheafFor.lean it is defined what it means for a presheaf to be a sheaf for a particular presieve. In this file we provide equivalent conditions in terms of equalizer diagrams.

• In Equalizer.Presieve.sheaf_condition, the sheaf condition at a presieve is shown to be equivalent to that of https://stacks.math.columbia.edu/tag/00VM (and combined with isSheaf_pretopology, this shows the notions of IsSheaf are exactly equivalent.)

• In Equalizer.Sieve.equalizer_sheaf_condition, the sheaf condition at a sieve is shown to be equivalent to that of Equation (3) p. 122 in Maclane-Moerdijk [MM92].

References

• [MM92]: Sheaves in geometry and logic, Saunders MacLane, and Ieke Moerdijk: Chapter III, Section 4.
• https://stacks.math.columbia.edu/tag/00VL (sheaves on a pretopology or site)

def CategoryTheory.Equalizer.FirstObj {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) : Type (max v u)

The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of the Stacks entry.

Stacks Tag 00VM (This is the middle object of the fork diagram there.)

theorem CategoryTheory.Equalizer.FirstObj.ext {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type (max v u))} {X : C} {R : Presieve X} (z₁ z₂ : FirstObj P R) (h : ∀ (Y : C) (f : Y ⟶ X) (hf : R f), Limits.Pi.π (fun (f : (Y : C) × { f : Y ⟶ X // R f }) => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = Limits.Pi.π (fun (f : (Y : C) × { f : Y ⟶ X // R f }) => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂) : z₁ = z₂

theorem CategoryTheory.Equalizer.FirstObj.ext_iff {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type (max v u))} {X : C} {R : Presieve X} {z₁ z₂ : FirstObj P R} : z₁ = z₂ ↔ ∀ (Y : C) (f : Y ⟶ X) (hf : R f), Limits.Pi.π (fun (f : (Y : C) × { f : Y ⟶ X // R f }) => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = Limits.Pi.π (fun (f : (Y : C) × { f : Y ⟶ X // R f }) => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂

def CategoryTheory.Equalizer.firstObjEqFamily {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) : FirstObj P R ≅ Presieve.FamilyOfElements P R

Show that FirstObj is isomorphic to FamilyOfElements.

@[simp]

theorem CategoryTheory.Equalizer.firstObjEqFamily_inv {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) (a✝ : Presieve.FamilyOfElements P R) : (firstObjEqFamily P R).inv a✝ = Limits.Pi.lift (fun (f : (Y : C) × { f : Y ⟶ X // R f }) (x : Presieve.FamilyOfElements P R) => x ↑f.snd ⋯) a✝

@[simp]

theorem CategoryTheory.Equalizer.firstObjEqFamily_hom {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) (t : FirstObj P R) (x✝ : C) (x✝¹ : x✝ ⟶ X) (hf : R x✝¹) : (firstObjEqFamily P R).hom t x✝¹ hf = Limits.Pi.π (fun (f : (Y : C) × { f : Y ⟶ X // R f }) => P.obj (Opposite.op f.fst)) ⟨x✝, ⟨x✝¹, hf⟩⟩ t

instance CategoryTheory.Equalizer.instInhabitedFirstObjBotPresieve {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} : Inhabited (FirstObj P ⊥)

instance CategoryTheory.Equalizer.instInhabitedFirstObjArrowsBotSieve {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} : Inhabited (FirstObj P ⊥.arrows)

def CategoryTheory.Equalizer.forkMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) : P.obj (Opposite.op X) ⟶ FirstObj P R

The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of the Stacks entry.

Stacks Tag 00VM (This is the left morphism of the fork diagram there.)

This section establishes the equivalence between the sheaf condition of Equation (3) [MM92] and the definition of IsSheafFor.

def CategoryTheory.Equalizer.Sieve.SecondObj {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (S : Sieve X) : Type (max v u)

The rightmost object of the fork diagram of Equation (3) [MM92], which contains the data used to check a family is compatible.

theorem CategoryTheory.Equalizer.Sieve.SecondObj.ext {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type (max v u))} {X : C} {S : Sieve X} (z₁ z₂ : SecondObj P S) (h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f), Limits.Pi.π (fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ = Limits.Pi.π (fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂) : z₁ = z₂

theorem CategoryTheory.Equalizer.Sieve.SecondObj.ext_iff {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type (max v u))} {X : C} {S : Sieve X} {z₁ z₂ : SecondObj P S} : z₁ = z₂ ↔ ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f), Limits.Pi.π (fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ = Limits.Pi.π (fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂

def CategoryTheory.Equalizer.Sieve.firstMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (S : Sieve X) : FirstObj P S.arrows ⟶ SecondObj P S

The map p of Equations (3,4) [MM92].

instance CategoryTheory.Equalizer.Sieve.instInhabitedSecondObjBotSieve {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} : Inhabited (SecondObj P ⊥)

def CategoryTheory.Equalizer.Sieve.secondMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (S : Sieve X) : FirstObj P S.arrows ⟶ SecondObj P S

The map a of Equations (3,4) [MM92].

theorem CategoryTheory.Equalizer.Sieve.w {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (S : Sieve X) : CategoryStruct.comp (forkMap P S.arrows) (firstMap P S) = CategoryStruct.comp (forkMap P S.arrows) (secondMap P S)

theorem CategoryTheory.Equalizer.Sieve.compatible_iff {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (S : Sieve X) (x : FirstObj P S.arrows) : ((firstObjEqFamily P S.arrows).hom x).Compatible ↔ firstMap P S x = secondMap P S x

The family of elements given by x : FirstObj P S is compatible iff firstMap and secondMap map it to the same point.

theorem CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (S : Sieve X) : Presieve.IsSheafFor P S.arrows ↔ Nonempty (Limits.IsLimit (Limits.Fork.ofι (forkMap P S.arrows) ⋯))

P is a sheaf for S, iff the fork given by w is an equalizer.

This section establishes the equivalence between the sheaf condition of https://stacks.math.columbia.edu/tag/00VM and the definition of isSheafFor.

def CategoryTheory.Equalizer.Presieve.SecondObj {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) [R.hasPullbacks] : Type (max v u)

The rightmost object of the fork diagram of the Stacks entry, which contains the data used to check a family of elements for a presieve is compatible.

Stacks Tag 00VM (This is the rightmost object of the fork diagram there.)

def CategoryTheory.Equalizer.Presieve.firstMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) [R.hasPullbacks] : FirstObj P R ⟶ SecondObj P R

The map pr₀* of the Stacks entry.

Stacks Tag 00VM (This is the map pr₀* there.)

instance CategoryTheory.Equalizer.Presieve.instInhabitedSecondObjBotPresieve {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} [Limits.HasPullbacks C] : Inhabited (SecondObj P ⊥)

def CategoryTheory.Equalizer.Presieve.secondMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) [R.hasPullbacks] : FirstObj P R ⟶ SecondObj P R

The map pr₁* of the Stacks entry.

Stacks Tag 00VM (This is the map pr₁* there.)

theorem CategoryTheory.Equalizer.Presieve.w {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) [R.hasPullbacks] : CategoryStruct.comp (forkMap P R) (firstMap P R) = CategoryStruct.comp (forkMap P R) (secondMap P R)

theorem CategoryTheory.Equalizer.Presieve.compatible_iff {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) [R.hasPullbacks] (x : FirstObj P R) : ((firstObjEqFamily P R).hom x).Compatible ↔ firstMap P R x = secondMap P R x

The family of elements given by x : FirstObj P S is compatible iff firstMap and secondMap map it to the same point.

theorem CategoryTheory.Equalizer.Presieve.sheaf_condition {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) [R.hasPullbacks] : Presieve.IsSheafFor P R ↔ Nonempty (Limits.IsLimit (Limits.Fork.ofι (forkMap P R) ⋯))

P is a sheaf for R, iff the fork given by w is an equalizer.

Stacks Tag 00VM

def CategoryTheory.Equalizer.Presieve.Arrows.FirstObj {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {I : Type t} [Small.{w, t} I] (X : I → C) : Type w

The middle object of the fork diagram of the Stacks entry. The difference between this and Equalizer.FirstObj P (ofArrows X π) arises if the family of arrows π contains duplicates. The Presieve.ofArrows doesn't see those.

Stacks Tag 00VM (The middle object of the fork diagram there.)

theorem CategoryTheory.Equalizer.Presieve.Arrows.FirstObj.ext {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {I : Type t} [Small.{w, t} I] (X : I → C) (z₁ z₂ : FirstObj P X) (h : ∀ (i : I), Limits.Pi.π (fun (i : I) => P.obj (Opposite.op (X i))) i z₁ = Limits.Pi.π (fun (i : I) => P.obj (Opposite.op (X i))) i z₂) : z₁ = z₂

theorem CategoryTheory.Equalizer.Presieve.Arrows.FirstObj.ext_iff {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type w)} {I : Type t} [Small.{w, t} I] {X : I → C} {z₁ z₂ : FirstObj P X} : z₁ = z₂ ↔ ∀ (i : I), Limits.Pi.π (fun (i : I) => P.obj (Opposite.op (X i))) i z₁ = Limits.Pi.π (fun (i : I) => P.obj (Opposite.op (X i))) i z₂

def CategoryTheory.Equalizer.Presieve.Arrows.SecondObj {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) [(Presieve.ofArrows X π).hasPullbacks] : Type w

The rightmost object of the fork diagram of the Stacks entry. The difference between this and Equalizer.Presieve.SecondObj P (ofArrows X π) arises if the family of arrows π contains duplicates. The Presieve.ofArrows doesn't see those.

Stacks Tag 00VM (The rightmost object of the fork diagram there.)

theorem CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) [(Presieve.ofArrows X π).hasPullbacks] (z₁ z₂ : SecondObj P X π) (h : ∀ (ij : I × I), Limits.Pi.π (fun (ij : I × I) => P.obj (Opposite.op (Limits.pullback (π ij.1) (π ij.2)))) ij z₁ = Limits.Pi.π (fun (ij : I × I) => P.obj (Opposite.op (Limits.pullback (π ij.1) (π ij.2)))) ij z₂) : z₁ = z₂

theorem CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext_iff {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type w)} {B : C} {I : Type t} [Small.{w, t} I] {X : I → C} {π : (i : I) → X i ⟶ B} [(Presieve.ofArrows X π).hasPullbacks] {z₁ z₂ : SecondObj P X π} : z₁ = z₂ ↔ ∀ (ij : I × I), Limits.Pi.π (fun (ij : I × I) => P.obj (Opposite.op (Limits.pullback (π ij.1) (π ij.2)))) ij z₁ = Limits.Pi.π (fun (ij : I × I) => P.obj (Opposite.op (Limits.pullback (π ij.1) (π ij.2)))) ij z₂

def CategoryTheory.Equalizer.Presieve.Arrows.forkMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) : P.obj (Opposite.op B) ⟶ FirstObj P X

The left morphism of the fork diagram.

def CategoryTheory.Equalizer.Presieve.Arrows.firstMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) [(Presieve.ofArrows X π).hasPullbacks] : FirstObj P X ⟶ SecondObj P X π

The first of the two parallel morphisms of the fork diagram, induced by the first projection in each pullback.

def CategoryTheory.Equalizer.Presieve.Arrows.secondMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) [(Presieve.ofArrows X π).hasPullbacks] : FirstObj P X ⟶ SecondObj P X π

The second of the two parallel morphisms of the fork diagram, induced by the second projection in each pullback.

theorem CategoryTheory.Equalizer.Presieve.Arrows.w {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) [(Presieve.ofArrows X π).hasPullbacks] : CategoryStruct.comp (forkMap P X π) (firstMap P X π) = CategoryStruct.comp (forkMap P X π) (secondMap P X π)

theorem CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type w} (X : I → C) (π : (i : I) → X i ⟶ B) [(Presieve.ofArrows X π).hasPullbacks] (x : FirstObj P X) : Presieve.Arrows.Compatible P π ((Limits.Types.productIso fun (i : I) => P.obj (Opposite.op (X i))).hom x) ↔ firstMap P X π x = secondMap P X π x

The family of elements given by x : FirstObj P S is compatible iff firstMap and secondMap map it to the same point. See CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small for a version with less universe assumptions.

theorem CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) [(Presieve.ofArrows X π).hasPullbacks] (x : FirstObj P X) : Presieve.Arrows.Compatible P π ((equivShrink ((i : I) → P.obj (Opposite.op (X i)))).symm ((Limits.Types.Small.productIso fun (i : I) => P.obj (Opposite.op (X i))).hom x)) ↔ firstMap P X π x = secondMap P X π x

Version of CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff for a small indexing type.

theorem CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type t} [Small.{w, t} I] (X : I → C) (π : (i : I) → X i ⟶ B) [(Presieve.ofArrows X π).hasPullbacks] : Presieve.IsSheafFor P (Presieve.ofArrows X π) ↔ Nonempty (Limits.IsLimit (Limits.Fork.ofι (forkMap P X π) ⋯))

P is a sheaf for Presieve.ofArrows X π, iff the fork given by w is an equalizer.

Stacks Tag 00VM

theorem CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type u_1)} {X Y : C} {f : X ⟶ Y} (c : Limits.PullbackCone f f) (hc : Limits.IsLimit c) : Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (Limits.IsLimit (Limits.Fork.ofι (F.map f.op) ⋯))

The sheaf condition for a single morphism is the same as the canonical fork diagram being limiting.

theorem CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type u_1)} {X Y : C} {f : X ⟶ Y} [Limits.HasPullback f f] : Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (Limits.IsLimit (Limits.Fork.ofι (F.map f.op) ⋯))

Special case of isSheafFor_singleton_iff with c = pullback.cone f f.