Documentation

Mathlib.CategoryTheory.Sites.Hypercover.One

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) extends CategoryTheory.PreZeroHypercover S :
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.)

  • X (i : self.I₀) : C
  • f (i : self.I₀) : self.X i 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
    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

                  The trivial pre-1-hypercover of S with a single component S.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    @[simp]
                    noncomputable def CategoryTheory.PreOneHypercover.inter {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] :

                    Intersection of two pre-1-hypercovers.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem CategoryTheory.PreOneHypercover.inter_p₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2) :
                      @[simp]
                      theorem CategoryTheory.PreOneHypercover.inter_Y {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2) :
                      (E.inter F).Y k = Limits.pullback (CategoryStruct.comp (E.p₁ k.1) (E.f i.1)) (CategoryStruct.comp (F.p₁ k.2) (F.f i.2))
                      @[simp]
                      theorem CategoryTheory.PreOneHypercover.inter_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] :
                      @[simp]
                      theorem CategoryTheory.PreOneHypercover.inter_I₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) :
                      (E.inter F).I₁ i j = (E.I₁ i.1 j.1 × F.I₁ i.2 j.2)
                      @[simp]
                      theorem CategoryTheory.PreOneHypercover.inter_p₂ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2) :
                      theorem CategoryTheory.PreOneHypercover.sieve₁_inter {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] {i j : E.I₀ × F.I₀} {W : C} {p₁ : W Limits.pullback (E.f i.1) (F.f i.2)} {p₂ : W Limits.pullback (E.f j.1) (F.f j.2)} (w : CategoryStruct.comp p₁ (CategoryStruct.comp (Limits.pullback.fst (E.f i.1) (F.f i.2)) (E.f i.1)) = CategoryStruct.comp p₂ (CategoryStruct.comp (Limits.pullback.fst (E.f j.1) (F.f j.2)) (E.f j.1))) :
                      (E.inter F).sieve₁ p₁ p₂ = Sieve.bind (E.sieve₁ (CategoryStruct.comp p₁ (Limits.pullback.fst (E.f i.1) (F.f i.2))) (CategoryStruct.comp p₂ (Limits.pullback.fst (E.f j.1) (F.f j.2)))).arrows fun (x : C) (f : x W) (x_1 : (E.sieve₁ (CategoryStruct.comp p₁ (Limits.pullback.fst (E.f i.1) (F.f i.2))) (CategoryStruct.comp p₂ (Limits.pullback.fst (E.f j.1) (F.f j.2)))).arrows f) => Sieve.pullback f (F.sieve₁ (CategoryStruct.comp p₁ (Limits.pullback.snd (E.f i.1) (F.f i.2))) (CategoryStruct.comp p₂ (Limits.pullback.snd (E.f j.1) (F.f j.2))))
                      structure CategoryTheory.PreOneHypercover.Hom {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) extends E.Hom F.toPreZeroHypercover :
                      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₀ x.h₀ y.h₀ @s₁ C inst✝ S E F x @s₁ C inst✝ S E F y @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₀) (h₀ : x.h₀ y.h₀) (s₁ : @s₁ C inst✝ S E F x @s₁ C inst✝ S E F y) (h₁ : @h₁ C inst✝ S E F x @h₁ C inst✝ S E F y) :
                        x = y
                        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) (x✝ : E.I₀) :
                          (id E).h₀ x✝ = CategoryStruct.id (E.X 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 = a
                          @[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) (a : E.I₀) :
                          (id E).s₀ a = a
                          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 : 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) (a✝ : E.I₀) :
                            (f.comp g).s₀ a✝ = g.s₀ (f.s₀ a✝)
                            @[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_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✝)

                            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.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_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.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₀) :

                              The forgetful functor from pre-1-hypercovers to pre-0-hypercovers.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem CategoryTheory.PreOneHypercover.oneToZero_map {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ : PreOneHypercover S} (f : X✝ Y✝) :

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

                                Equations
                                Instances For
                                  noncomputable def CategoryTheory.PreOneHypercover.interFst {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] :
                                  (E.inter F).Hom E

                                  First projection from the intersection of two pre-1-hypercovers.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.PreOneHypercover.interFst_toHom {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] :
                                    @[simp]
                                    theorem CategoryTheory.PreOneHypercover.interFst_s₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] {i j : (E.inter F).I₀} (k : (E.inter F).I₁ i j) :
                                    (E.interFst F).s₁ k = k.1
                                    noncomputable def CategoryTheory.PreOneHypercover.interSnd {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] :
                                    (E.inter F).Hom F

                                    Second projection from the intersection of two pre-1-hypercovers.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.PreOneHypercover.interSnd_toHom {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] :
                                      @[simp]
                                      theorem CategoryTheory.PreOneHypercover.interSnd_s₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] {i j : (E.inter F).I₀} (k : (E.inter F).I₁ i j) :
                                      (E.interSnd F).s₁ k = k.2
                                      noncomputable def CategoryTheory.PreOneHypercover.interLift {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] {G : PreOneHypercover S} (f : G.Hom E) (g : G.Hom F) :
                                      G.Hom (E.inter F)

                                      Universal property of the intersection of two pre-1-hypercovers.

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

                                        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

                                              Forget the 1-components of a OneHypercover.

                                              Equations
                                              Instances For

                                                The trivial 1-hypercover of S where a single component S.

                                                Equations
                                                Instances For
                                                  noncomputable def CategoryTheory.GrothendieckTopology.OneHypercover.inter {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} [Limits.HasPullbacks C] (E : J.OneHypercover S) (F : J.OneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] :

                                                  Intersection of two 1-hypercovers.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.GrothendieckTopology.OneHypercover.inter_toPreOneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} [Limits.HasPullbacks C] (E : J.OneHypercover S) (F : J.OneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] :
                                                    @[reducible, inline]

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

                                                    Equations
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      @[simp]
                                                      theorem CategoryTheory.GrothendieckTopology.OneHypercover.id_h₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) {i✝ j✝ : E.I₀} (x✝ : E.I₁ i✝ j✝) :
                                                      @[simp]
                                                      theorem CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {X✝ Y✝ Z✝ : J.OneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {i✝ j✝ : X✝.I₀} (i : X✝.I₁ i✝ j✝) :
                                                      @[simp]
                                                      theorem CategoryTheory.GrothendieckTopology.OneHypercover.id_s₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) {i✝ j✝ : E.I₀} (a : E.I₁ i✝ j✝) :
                                                      @[simp]
                                                      theorem CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₀ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {X✝ Y✝ Z✝ : J.OneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (i : X✝.I₀) :
                                                      @[simp]
                                                      theorem CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₀ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {X✝ Y✝ Z✝ : J.OneHypercover 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.GrothendieckTopology.OneHypercover.comp_s₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {X✝ Y✝ Z✝ : J.OneHypercover 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✝)

                                                      An isomorphism of 1-hypercovers is an isomorphism of pre-1-hypercovers.

                                                      Equations
                                                      Instances For

                                                        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_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₂
                                                          @[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_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✝¹) :
                                                          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