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} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : CategoryTheory.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 https://stacks.math.columbia.edu/tag/00VM.

Equations

• CategoryTheory.Equalizer.FirstObj P R = ∏ᶜ fun (f : (Y : C) × { f : Y ⟶ X // R f }) => P.obj (Opposite.op f.fst)

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

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

Show that FirstObj is isomorphic to FamilyOfElements.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Equalizer.instInhabitedFirstObjBotPresieve P = (CategoryTheory.Equalizer.firstObjEqFamily P ⊥).toEquiv.inhabited

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

Equations

• CategoryTheory.Equalizer.instInhabitedFirstObjArrowsBotSieve P = inferInstance

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

The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of https://stacks.math.columbia.edu/tag/00VM.

Equations

• CategoryTheory.Equalizer.forkMap P R = CategoryTheory.Limits.Pi.lift fun (f : (Y : C) × { f : Y ⟶ X // R f }) => P.map (↑f.snd).op

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} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (S : CategoryTheory.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.

Equations

• CategoryTheory.Equalizer.Sieve.SecondObj P S = ∏ᶜ fun (f : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' }) => P.obj (Opposite.op f.snd.fst)

theorem CategoryTheory.Equalizer.Sieve.SecondObj.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))} {X : C} {S : CategoryTheory.Sieve X} (z₁ : CategoryTheory.Equalizer.Sieve.SecondObj P S) (z₂ : CategoryTheory.Equalizer.Sieve.SecondObj P S) (h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f), CategoryTheory.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₁ = CategoryTheory.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₂

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Equalizer.Sieve.instInhabitedSecondObjBotSieve P = { default := CategoryTheory.Equalizer.Sieve.firstMap P ⊥ default }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

theorem CategoryTheory.Equalizer.Sieve.compatible_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (S : CategoryTheory.Sieve X) (x : CategoryTheory.Equalizer.FirstObj P S.arrows) : ((CategoryTheory.Equalizer.firstObjEqFamily P S.arrows).hom x).Compatible ↔ CategoryTheory.Equalizer.Sieve.firstMap P S x = CategoryTheory.Equalizer.Sieve.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} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Presieve.IsSheafFor P S.arrows ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.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} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : CategoryTheory.Presieve X) [R.hasPullbacks] : Type (max v u)

The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which contains the data used to check a family of elements for a presieve is compatible.

Equations

• One or more equations did not get rendered due to their size.

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

The map pr₀* of https://stacks.math.columbia.edu/tag/00VL.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Equalizer.Presieve.instInhabitedSecondObjBotPresieve P = { default := CategoryTheory.Equalizer.Presieve.firstMap P ⊥ default }

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

The map pr₁* of https://stacks.math.columbia.edu/tag/00VL.

Equations

• One or more equations did not get rendered due to their size.

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

theorem CategoryTheory.Equalizer.Presieve.compatible_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : CategoryTheory.Presieve X) [R.hasPullbacks] (x : CategoryTheory.Equalizer.FirstObj P R) : ((CategoryTheory.Equalizer.firstObjEqFamily P R).hom x).Compatible ↔ CategoryTheory.Equalizer.Presieve.firstMap P R x = CategoryTheory.Equalizer.Presieve.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} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : CategoryTheory.Presieve X) [R.hasPullbacks] : CategoryTheory.Presieve.IsSheafFor P R ↔ Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P R) ⋯))

P is a sheaf for R, iff the fork given by w is an equalizer. See https://stacks.math.columbia.edu/tag/00VM.

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

The middle object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM. The difference between this and Equalizer.FirstObj P (ofArrows X π) arrises if the family of arrows π contains duplicates. The Presieve.ofArrows doesn't see those.

Equations

• CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X = ∏ᶜ fun (i : I) => P.obj (Opposite.op (X i))

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

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

The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM. The difference between this and Equalizer.Presieve.SecondObj P (ofArrows X π) arrises if the family of arrows π contains duplicates. The Presieve.ofArrows doesn't see those.

Equations

• CategoryTheory.Equalizer.Presieve.Arrows.SecondObj P X π = ∏ᶜ fun (ij : I × I) => P.obj (Opposite.op (CategoryTheory.Limits.pullback (π ij.1) (π ij.2)))

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

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

The left morphism of the fork diagram.

Equations

• CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π = CategoryTheory.Limits.Pi.lift fun (i : I) => P.map (π i).op

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

P is a sheaf for Presieve.ofArrows X π, iff the fork given by w is an equalizer. See https://stacks.math.columbia.edu/tag/00VM.