Documentation

Mathlib.CategoryTheory.Sites.OneHypercover

1-hypercovers #

Given a Grothendieck topology J on a category C, we define the type of 1-hypercovers of an object S : C. They consists of a covering family of morphisms X i ⟶ S indexed by a type I₀ and, for each tuple (i₁, i₂) of elements of I₀, a "covering Y j of the fibre product of X i₁ and X i₂ over S", a condition which is phrased here without assuming that the fibre product actually exist.

The definition OneHypercover.isLimitMultifork shows that if E is a 1-hypercover of S, and F is a sheaf, then F.obj (op S) identifies to the multiequalizer of suitable maps F.obj (op (E.X i)) ⟶ F.obj (op (E.Y j)).

structure CategoryTheory.PreOneHypercover {C : Type u} [Category.{v, u} C] (S : C) :
Type (max (max u v) (w + 1))

The categorical data that is involved in a 1-hypercover of an object S. This consists of a family of morphisms f i : X i ⟶ S for i : I₀, and for each tuple (i₁, i₂) of elements in I₀, a family of objects Y j indexed by a type I₁ i₁ i₂, which are equipped with a map to the fibre product of X i₁ and X i₂, which is phrased here as the data of the two projections p₁ : Y j ⟶ X i₁, p₂ : Y j ⟶ X i₂ and the relation p₁ j ≫ f i₁ = p₂ j ≫ f i₂. (See GrothendieckTopology.OneHypercover for the topological conditions.)

  • I₀ : Type w

    the index type of the covering of S

  • X (i : self.I₀) : C

    the objects in the covering of S

  • f (i : self.I₀) : self.X i S

    the morphisms in the covering of S

  • I₁ (i₁ i₂ : self.I₀) : Type w

    the index type of the coverings of the fibre products

  • Y i₁ i₂ : self.I₀ (j : self.I₁ i₁ i₂) : C

    the objects in the coverings of the fibre products

  • p₁ i₁ i₂ : self.I₀ (j : self.I₁ i₁ i₂) : self.Y j self.X i₁

    the first projection Y j ⟶ X i₁

  • p₂ i₁ i₂ : self.I₀ (j : self.I₁ i₁ i₂) : self.Y j self.X i₂

    the second projection Y j ⟶ X i₂

  • w i₁ i₂ : self.I₀ (j : self.I₁ i₁ i₂) : CategoryStruct.comp (self.p₁ j) (self.f i₁) = CategoryStruct.comp (self.p₂ j) (self.f i₂)
Instances For
    @[reducible, inline]

    The assumption that the pullback of X i₁ and X i₂ over S exists for any i₁ and i₂.

    Equations
    Instances For
      @[reducible, inline]

      The sieve of S that is generated by the morphisms f i : X i ⟶ S.

      Equations
      Instances For
        def CategoryTheory.PreOneHypercover.sieve₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i₁ i₂ : E.I₀} {W : C} (p₁ : W E.X i₁) (p₂ : W E.X i₂) :

        Given an object W equipped with morphisms p₁ : W ⟶ E.X i₁, p₂ : W ⟶ E.X i₂, this is the sieve of W which consists of morphisms g : Z ⟶ W such that there exists j and h : Z ⟶ E.Y j such that g ≫ p₁ = h ≫ E.p₁ j and g ≫ p₂ = h ≫ E.p₂ j. See lemmas sieve₁_eq_pullback_sieve₁' and sieve₁'_eq_sieve₁ for equational lemmas regarding this sieve.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.PreOneHypercover.sieve₁_apply {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i₁ i₂ : E.I₀} {W : C} (p₁ : W E.X i₁) (p₂ : W E.X i₂) (Z : C) (g : Z W) :
          (E.sieve₁ p₁ p₂).arrows g = ∃ (j : E.I₁ i₁ i₂) (h : Z E.Y j), CategoryStruct.comp g p₁ = CategoryStruct.comp h (E.p₁ j) CategoryStruct.comp g p₂ = CategoryStruct.comp h (E.p₂ j)
          @[reducible, inline]
          noncomputable abbrev CategoryTheory.PreOneHypercover.toPullback {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i₁ i₂ : E.I₀} (j : E.I₁ i₁ i₂) [Limits.HasPullback (E.f i₁) (E.f i₂)] :
          E.Y j Limits.pullback (E.f i₁) (E.f i₂)

          The obvious morphism E.Y j ⟶ pullback (E.f i₁) (E.f i₂) given by E : PreOneHypercover S.

          Equations
          Instances For
            noncomputable def CategoryTheory.PreOneHypercover.sieve₁' {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (i₁ i₂ : E.I₀) [Limits.HasPullback (E.f i₁) (E.f i₂)] :
            Sieve (Limits.pullback (E.f i₁) (E.f i₂))

            The sieve of pullback (E.f i₁) (E.f i₂) given by E : PreOneHypercover S.

            Equations
            Instances For
              theorem CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁' {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i₁ i₂ : E.I₀} [Limits.HasPullback (E.f i₁) (E.f i₂)] {W : C} (p₁ : W E.X i₁) (p₂ : W E.X i₂) (w : CategoryStruct.comp p₁ (E.f i₁) = CategoryStruct.comp p₂ (E.f i₂)) :
              E.sieve₁ p₁ p₂ = Sieve.pullback (Limits.pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)
              theorem CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (i₁ i₂ : E.I₀) [Limits.HasPullback (E.f i₁) (E.f i₂)] :
              E.sieve₁' i₁ i₂ = E.sieve₁ (Limits.pullback.fst (E.f i₁) (E.f i₂)) (Limits.pullback.snd (E.f i₁) (E.f i₂))
              @[reducible, inline]

              The sigma type of all E.I₁ i₁ i₂ for ⟨i₁, i₂⟩ : E.I₀ × E.I₀.

              Equations
              Instances For

                The shape of the multiforks attached to E : PreOneHypercover S.

                Equations
                Instances For

                  The diagram of the multifork attached to a presheaf F : Cᵒᵖ ⥤ A, S : C and E : PreOneHypercover S.

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

                    The multifork attached to a presheaf F : Cᵒᵖ ⥤ A, S : C and E : PreOneHypercover S.

                    Equations
                    Instances For
                      structure CategoryTheory.PreOneHypercover.Hom {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) :
                      Type (max (max u_2 u_3) v)

                      A morphism of pre-1-hypercovers of S is a family of refinement morphisms commuting with the structure morphisms of E and F.

                      Instances For
                        theorem CategoryTheory.PreOneHypercover.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {x y : E.Hom F} :
                        x = y x.s₀ = y.s₀ @s₁ C inst✝ S E F x @s₁ C inst✝ S E F y x.h₀ y.h₀ @h₁ C inst✝ S E F x @h₁ C inst✝ S E F y
                        theorem CategoryTheory.PreOneHypercover.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {x y : E.Hom F} (s₀ : x.s₀ = y.s₀) (s₁ : @s₁ C inst✝ S E F x @s₁ C inst✝ S E F y) (h₀ : x.h₀ y.h₀) (h₁ : @h₁ C inst✝ S E F x @h₁ C inst✝ S E F y) :
                        x = y
                        @[simp]
                        theorem CategoryTheory.PreOneHypercover.Hom.w₀_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (self : E.Hom F) (i : E.I₀) {Z : C} (h : S Z) :
                        theorem CategoryTheory.PreOneHypercover.Hom.w₁₂_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : F.X (self.s₀ j) Z) :
                        theorem CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : F.X (self.s₀ i) Z) :

                        The identity refinement of a pre-1-hypercover.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem CategoryTheory.PreOneHypercover.Hom.id_h₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i✝ j✝ : E.I₀} (x✝ : E.I₁ i✝ j✝) :
                          (id E).h₁ x✝ = CategoryStruct.id (E.Y x✝)
                          @[simp]
                          theorem CategoryTheory.PreOneHypercover.Hom.id_s₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i✝ j✝ : E.I₀} (a : E.I₁ i✝ j✝) :
                          (id E).s₁ a = _root_.id a
                          @[simp]
                          theorem CategoryTheory.PreOneHypercover.Hom.id_h₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (x✝ : E.I₀) :
                          (id E).h₀ x✝ = CategoryStruct.id (E.X x✝)
                          def CategoryTheory.PreOneHypercover.Hom.comp {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) :
                          E.Hom G

                          Composition of refinement morphisms of pre-1-hypercovers.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem CategoryTheory.PreOneHypercover.Hom.comp_h₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) {i✝ j✝ : E.I₀} (i : E.I₁ i✝ j✝) :
                            (f.comp g).h₁ i = CategoryStruct.comp (f.h₁ i) (g.h₁ (f.s₁ i))
                            @[simp]
                            theorem CategoryTheory.PreOneHypercover.Hom.comp_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) (i : E.I₀) :
                            (f.comp g).h₀ i = CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
                            @[simp]
                            theorem CategoryTheory.PreOneHypercover.Hom.comp_s₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) {i✝ j✝ : E.I₀} (a✝ : E.I₁ i✝ j✝) :
                            (f.comp g).s₁ a✝ = (g.s₁ f.s₁) a✝
                            @[simp]
                            theorem CategoryTheory.PreOneHypercover.Hom.comp_s₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) (a✝ : E.I₀) :
                            (f.comp g).s₀ a✝ = (g.s₀ f.s₀) a✝

                            The induced index map E.I₁' → F.I₁' from a refinement morphism E ⟶ F.

                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              @[simp]
                              theorem CategoryTheory.PreOneHypercover.id_s₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i✝ j✝ : E.I₀} (a : E.I₁ i✝ j✝) :
                              @[simp]
                              @[simp]
                              theorem CategoryTheory.PreOneHypercover.comp_h₁ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {i✝ j✝ : X✝.I₀} (i : X✝.I₁ i✝ j✝) :
                              @[simp]
                              theorem CategoryTheory.PreOneHypercover.id_h₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i✝ j✝ : E.I₀} (x✝ : E.I₁ i✝ j✝) :
                              @[simp]
                              theorem CategoryTheory.PreOneHypercover.comp_s₁ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {i✝ j✝ : X✝.I₀} (a✝ : X✝.I₁ i✝ j✝) :
                              (CategoryStruct.comp f g).s₁ a✝ = g.s₁ (f.s₁ a✝)
                              @[simp]
                              theorem CategoryTheory.PreOneHypercover.comp_s₀ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (a✝ : X✝.I₀) :
                              (CategoryStruct.comp f g).s₀ a✝ = g.s₀ (f.s₀ a✝)
                              @[simp]
                              theorem CategoryTheory.PreOneHypercover.comp_h₀ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (i : X✝.I₀) :
                              structure CategoryTheory.PreOneHypercover.Homotopy {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (f g : E.Hom F) :
                              Type (max (max v w) w')

                              A homotopy of refinements E ⟶ F is a family of morphisms Xᵢ ⟶ Yₐ where Yₐ is a component of the cover of X_{f(i)} ×[S] X_{g(i)}.

                              Instances For
                                @[simp]
                                theorem CategoryTheory.PreOneHypercover.Homotopy.wr_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {f g : E.Hom F} (self : Homotopy f g) (i : E.I₀) {Z : C} (h : F.X (g.s₀ i) Z) :
                                @[simp]
                                theorem CategoryTheory.PreOneHypercover.Homotopy.wl_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {f g : E.Hom F} (self : Homotopy f g) (i : E.I₀) {Z : C} (h : F.X (f.s₀ i) Z) :

                                A refinement morphism E ⟶ F induces a morphism on associated multiequalizers.

                                Equations
                                Instances For

                                  Homotopic refinements induce the same map on multiequalizers.

                                  @[reducible, inline]
                                  noncomputable abbrev CategoryTheory.PreOneHypercover.cylinderX {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {i : E.I₀} (k : F.I₁ (f.s₀ i) (g.s₀ i)) :
                                  C

                                  (Implementation): The covering object of cylinder f g.

                                  Equations
                                  Instances For
                                    @[reducible, inline]
                                    noncomputable abbrev CategoryTheory.PreOneHypercover.cylinderf {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {i : E.I₀} (k : F.I₁ (f.s₀ i) (g.s₀ i)) :
                                    cylinderX f g k S

                                    (Implementation): The structure morphisms of the covering objects of cylinder f g.

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

                                      Given two refinement morphisms f, g : E ⟶ F, this is a (pre-)1-hypercover W that admits a morphism h : W ⟶ E such that h ≫ f and h ≫ g are homotopic. Hence they become equal after quotienting out by homotopy. This is a 1-hypercover, if E and F are (see OneHpyercover.cylinder).

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.PreOneHypercover.cylinder_I₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) :
                                        @[simp]
                                        @[simp]
                                        theorem CategoryTheory.PreOneHypercover.cylinder_f {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (p : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) :
                                        (cylinder f g).f p = cylinderf f g p.snd
                                        @[simp]
                                        theorem CategoryTheory.PreOneHypercover.cylinder_I₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) :
                                        (cylinder f g).I₀ = ((i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i))
                                        @[simp]
                                        theorem CategoryTheory.PreOneHypercover.cylinder_X {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (p : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) :
                                        (cylinder f g).X p = cylinderX f g p.snd
                                        noncomputable def CategoryTheory.PreOneHypercover.cylinderHom {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) :
                                        (cylinder f g).Hom E

                                        (Implementation): The refinement morphism cylinder f g ⟶ E.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.PreOneHypercover.cylinderHom_s₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {i✝ j✝ : (cylinder f g).I₀} (k : (cylinder f g).I₁ i✝ j✝) :

                                          (Implementation): The homotopy of the morphisms cylinder f g ⟶ E ⟶ F.

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

                                            Up to homotopy, the category of (pre-)1-hypercovers is cofiltered.

                                            The type of 1-hypercovers of an object S : C in a category equipped with a Grothendieck topology J. This can be constructed from a covering of S and a covering of the fibre products of the objects in this covering (see OneHypercover.mk').

                                            Instances For
                                              theorem CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) (i₁ i₂ : E.I₀) [Limits.HasPullback (E.f i₁) (E.f i₂)] :
                                              E.sieve₁' i₁ i₂ J (Limits.pullback (E.f i₁) (E.f i₂))
                                              def CategoryTheory.GrothendieckTopology.OneHypercover.mk' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : PreOneHypercover S) [E.HasPullbacks] (mem₀ : E.sieve₀ J S) (mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ J (Limits.pullback (E.f i₁) (E.f i₂))) :

                                              In order to check that a certain data is a 1-hypercover of S, it suffices to check that the data provides a covering of S and of the fibre products.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.GrothendieckTopology.OneHypercover.mk'_toPreOneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : PreOneHypercover S) [E.HasPullbacks] (mem₀ : E.sieve₀ J S) (mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ J (Limits.pullback (E.f i₁) (E.f i₂))) :
                                                (mk' E mem₀ mem₁').toPreOneHypercover = E

                                                If E : J.OneHypercover S and F : Sheaf J A, then F.obj (op S) is a multiequalizer of suitable maps F.obj (op (E.X i)) ⟶ F.obj (op (E.Y j)) induced by E.p₁ j and E.p₂ j.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[reducible, inline]

                                                  A morphism of 1-hypercovers is a morphism of the underlying pre-1-hypercovers.

                                                  Equations
                                                  Instances For

                                                    Given two refinement morphism f, g : E ⟶ F, this is a 1-hypercover W that admits a morphism h : W ⟶ E such that h ≫ f and h ≫ g are homotopic. Hence they become equal after quotienting out by homotopy.

                                                    Equations
                                                    Instances For

                                                      Up to homotopy, the category of 1-hypercovers is cofiltered.

                                                      The tautological 1-pre-hypercover induced by S : J.Cover X. Its index type I₀ is given by S.Arrow (i.e. all the morphisms in the sieve S), while I₁ is given by all possible pullback cones.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₂ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (x✝ x✝¹ : S.Arrow) (r : x✝.Relation x✝¹) :
                                                        @[simp]
                                                        theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_Y {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (x✝ x✝¹ : S.Arrow) (r : x✝.Relation x✝¹) :
                                                        @[simp]
                                                        theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (x✝ x✝¹ : S.Arrow) (r : x✝.Relation x✝¹) :
                                                        @[simp]
                                                        theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (f₁ f₂ : S.Arrow) :
                                                        S.preOneHypercover.I₁ f₁ f₂ = f₁.Relation f₂
                                                        theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (f₁ f₂ : S.Arrow) {W : C} (p₁ : W f₁.Y) (p₂ : W f₂.Y) (w : CategoryStruct.comp p₁ f₁.f = CategoryStruct.comp p₂ f₂.f) :

                                                        The tautological 1-hypercover induced by S : J.Cover X. Its index type I₀ is given by S.Arrow (i.e. all the morphisms in the sieve S), while I₁ is given by all possible pullback cones.

                                                        Equations
                                                        Instances For