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.

References #

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.)

Equations
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₂

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✝

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.)

Equations

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.

Equations
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₂

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

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

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

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

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} [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.)

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

The map pr₀* of the Stacks entry.

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

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

The map pr₁* of the Stacks entry.

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

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

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.

Stacks Tag 00VM

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.)

Equations
theorem CategoryTheory.Equalizer.Presieve.Arrows.FirstObj.ext {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type w)) {I : Type} (X : IC) (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 : IC) (π : (i : I) → X i B) [(Presieve.ofArrows X π).hasPullbacks] :

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.)

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

The left morphism of the fork diagram.

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

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 : IC) (π : (i : I) → X i B) [(Presieve.ofArrows X π).hasPullbacks] :

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

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

Stacks Tag 00VM