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 #

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
Instances For
    theorem CategoryTheory.Equalizer.FirstObj.ext_iff {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} :
    z₁ = z₂ ∀ (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₂
    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₂
    @[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) (Y : C) (f : Y X) (hf : R f) :
    (CategoryTheory.Equalizer.firstObjEqFamily P R).hom t f hf = CategoryTheory.Limits.Pi.π (fun (f : (Y : C) × { f : Y X // R f }) => P.obj (Opposite.op f.fst)) Y, f, hf t

    Show that FirstObj is isomorphic to FamilyOfElements.

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

      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
      Instances For

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

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

        Equations
        Instances For
          theorem CategoryTheory.Equalizer.Sieve.SecondObj.ext_iff {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} :
          z₁ = z₂ ∀ (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₂
          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₂

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

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

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

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

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

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

              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 https://stacks.math.columbia.edu/tag/00VL.

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

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

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

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

                      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_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {B : C} {I : Type} {X : IC} {π : (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 π} :
                        z₁ = z₂ ∀ (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₂
                        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 : IC) (π : (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₂

                        The left morphism of the fork diagram.

                        Equations
                        Instances For

                          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

                            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