# Documentation

Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

# 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} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : ) :
Type (max v u)

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

Equations
Instances For
theorem CategoryTheory.Equalizer.FirstObj.ext {C : Type u} {P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))} {X : C} {R : } (z₁ : ) (z₂ : ) (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)) { fst := Y, snd := { val := f, property := hf } } z₁ = CategoryTheory.Limits.Pi.π (fun (f : (Y : C) × { f : Y X // R f }) => P.obj (Opposite.op f.fst)) { fst := Y, snd := { val := f, property := hf } } z₂) :
z₁ = z₂
@[simp]
theorem CategoryTheory.Equalizer.firstObjEqFamily_hom {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : ) (t : ) (Y : C) (f : Y X) (hf : R f) :
.hom t f hf = CategoryTheory.Limits.Pi.π (fun (f : (Y : C) × { f : Y X // R f }) => P.obj (Opposite.op f.fst)) { fst := Y, snd := { val := f, property := hf } } t
@[simp]
theorem CategoryTheory.Equalizer.firstObjEqFamily_inv {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : ) :
∀ (a : ), .inv a = CategoryTheory.Limits.Pi.lift (fun (f : (Y : C) × { f : Y X // R f }) (x : ) => x f.snd (_ : R f.snd)) a

Show that FirstObj is isomorphic to FamilyOfElements.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Equalizer.forkMap {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : ) :
P.obj ()

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

Equations
Instances For

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} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (S : ) :
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
• = fun (f : (Y : C) × (Z : C) × (_ : Z Y) × { f' : Y X // S.arrows f' }) => P.obj (Opposite.op f.snd.fst)
Instances For
theorem CategoryTheory.Equalizer.Sieve.SecondObj.ext {C : Type u} {P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))} {X : C} {S : } (z₁ : ) (z₂ : ) (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)) { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := 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)) { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } z₂) :
z₁ = z₂
def CategoryTheory.Equalizer.Sieve.firstMap {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (S : ) :

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

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Equalizer.Sieve.w {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (S : ) :

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

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} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : ) :
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.
Instances For

The map pr₀* of .

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

The map pr₁* of .

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Equalizer.Presieve.w {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : ) :
theorem CategoryTheory.Equalizer.Presieve.compatible_iff {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C} (R : ) (x : ) :

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

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

def CategoryTheory.Equalizer.Presieve.Arrows.FirstObj {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {I : Type} (X : IC) :
Type (max v u)

The middle object of the fork diagram of . 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
Instances For
theorem CategoryTheory.Equalizer.Presieve.Arrows.FirstObj.ext {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {I : Type} (X : IC) (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} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {B : C} {I : Type} (X : IC) (π : (i : I) → X i B) :
Type (max v u)

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
Instances For
theorem CategoryTheory.Equalizer.Presieve.Arrows.SecondObj.ext {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {B : C} {I : Type} (X : IC) (π : (i : I) → X i B) (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} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {B : C} {I : Type} (X : IC) (π : (i : I) → X i B) :

The left morphism of the fork diagram.

Equations
Instances For
def CategoryTheory.Equalizer.Presieve.Arrows.firstMap {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {B : C} {I : Type} (X : IC) (π : (i : I) → X i B) :

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.
Instances For
def CategoryTheory.Equalizer.Presieve.Arrows.secondMap {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {B : C} {I : Type} (X : IC) (π : (i : I) → X i B) :

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.
Instances For
theorem CategoryTheory.Equalizer.Presieve.Arrows.w {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {B : C} {I : Type} (X : IC) (π : (i : I) → X i B) :
theorem CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff {C : Type u} (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {B : C} {I : Type} (X : IC) (π : (i : I) → X i B) :

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

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