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
Instances For
    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.
    Instances For
      @[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✝
      def CategoryTheory.Equalizer.forkMap {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max v u))) {X : C} (R : Presieve X) :

      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
      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} [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
        Instances For
          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.
          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

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

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

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

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