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 [MLM92].

References

• [MLM92]: 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 [MLM92], 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} [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₂

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.

Equations

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

@[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

@[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✝

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

Equations

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

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

Equations

• CategoryTheory.Equalizer.instInhabitedFirstObjArrowsBotSieve P = inferInstance

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 [MLM92], 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) [MLM92] 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) [MLM92], 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} [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₂

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) [MLM92].

Equations

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

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

Equations

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

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) [MLM92].

Equations

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

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

Equations

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

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 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} [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. See https://stacks.math.columbia.edu/tag/00VM.

def CategoryTheory.Equalizer.Presieve.Arrows.FirstObj {C : Type u} [Category.{v, u} C] (P : 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 π) arises 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} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {I : Type} (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₂

def CategoryTheory.Equalizer.Presieve.Arrows.SecondObj {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type} (X : I → C) (π : (i : I) → X i ⟶ B) [(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 π) arises 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} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type} (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₂

def CategoryTheory.Equalizer.Presieve.Arrows.forkMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type} (X : I → C) (π : (i : I) → X i ⟶ B) : P.obj (Opposite.op B) ⟶ 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} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type} (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.

Equations

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

def CategoryTheory.Equalizer.Presieve.Arrows.secondMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type} (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.

Equations

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

theorem CategoryTheory.Equalizer.Presieve.Arrows.w {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type} (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} (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.

theorem CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {B : C} {I : Type} (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. See https://stacks.math.columbia.edu/tag/00VM.