Documentation

Mathlib.CategoryTheory.Sites.ZeroHypercover

0-hypercovers #

Given a coverage J on a category C, we define the tyoe of 0-hypercovers of an object S : C. They consists of a covering family of morphisms X i ⟶ S indexed by a type I₀ such that the induced presieve is in J.

We define this with respect to a coverage and not to a Grothendieck topology, because this yields more control over the components of the cover.

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

The categorical data that is involved in a 0-hypercover of an object S. This consists of a family of morphisms f i : X i ⟶ S for i : I₀.

  • 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

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 presieve of S that is generated by the morphisms f i : X i ⟶ S.

      Equations
      Instances For
        @[reducible, inline]

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

        Equations
        Instances For

          The pre-0-hypercover defined by a single morphism.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.PreZeroHypercover.singleton_f {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (x✝ : PUnit.{w + 1}) :
            (singleton f).f x✝ = f
            @[simp]
            theorem CategoryTheory.PreZeroHypercover.singleton_X {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (x✝ : PUnit.{w + 1}) :
            (singleton f).X x✝ = S
            noncomputable def CategoryTheory.PreZeroHypercover.pullback₁ {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] :

            Pullback of a pre-0-hypercover along a morphism. The components are pullback f (E.f i).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem CategoryTheory.PreZeroHypercover.pullback₁_I₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] :
              @[simp]
              theorem CategoryTheory.PreZeroHypercover.pullback₁_f {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] (x✝ : E.I₀) :
              (pullback₁ f E).f x✝ = Limits.pullback.fst f (E.f x✝)
              @[simp]
              theorem CategoryTheory.PreZeroHypercover.pullback₁_X {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] (i : E.I₀) :
              (pullback₁ f E).X i = Limits.pullback f (E.f i)
              noncomputable def CategoryTheory.PreZeroHypercover.pullback₂ {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] :

              Pullback of a pre-0-hypercover along a morphism. The components are pullback (E.f i) f.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.PreZeroHypercover.pullback₂_f {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] (x✝ : E.I₀) :
                (pullback₂ f E).f x✝ = Limits.pullback.snd (E.f x✝) f
                @[simp]
                theorem CategoryTheory.PreZeroHypercover.pullback₂_I₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] :
                @[simp]
                theorem CategoryTheory.PreZeroHypercover.pullback₂_X {C : Type u} [Category.{v, u} C] {S T : C} (f : S T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] (i : E.I₀) :
                (pullback₂ f E).X i = Limits.pullback (E.f i) f

                Refining each component of a pre-0-hypercover yields a refined pre-0-hypercover of the base.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.PreZeroHypercover.bind_I₀ {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : (i : E.I₀) → PreZeroHypercover (E.X i)) :
                  (E.bind F).I₀ = ((i : E.I₀) × (F i).I₀)
                  @[simp]
                  theorem CategoryTheory.PreZeroHypercover.bind_X {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : (i : E.I₀) → PreZeroHypercover (E.X i)) (x✝ : (i : E.I₀) × (F i).I₀) :
                  (E.bind F).X x✝ = match x✝ with | i, j => (F i).X j
                  @[simp]
                  theorem CategoryTheory.PreZeroHypercover.bind_f {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : (i : E.I₀) → PreZeroHypercover (E.X i)) (x✝ : (i : E.I₀) × (F i).I₀) :
                  (E.bind F).f x✝ = match x✝ with | i, j => CategoryStruct.comp ((F i).f j) (E.f i)
                  structure CategoryTheory.PreZeroHypercover.Hom {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) :
                  Type (max (max v w) w')

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

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

                    The identity refinement of a pre-0-hypercover.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.PreZeroHypercover.Hom.id_h₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (x✝ : E.I₀) :
                      (id E).h₀ x✝ = CategoryStruct.id (E.X x✝)
                      def CategoryTheory.PreZeroHypercover.Hom.comp {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover S} (f : E.Hom F) (g : F.Hom G) :
                      E.Hom G

                      Composition of refinement morphisms of pre-0-hypercovers.

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.PreZeroHypercover.Hom.comp_s₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover 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.PreZeroHypercover.Hom.comp_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover 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))
                        Equations
                        • One or more equations did not get rendered due to their size.
                        @[simp]
                        theorem CategoryTheory.PreZeroHypercover.comp_h₀ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreZeroHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (i : X✝.I₀) :
                        @[simp]
                        theorem CategoryTheory.PreZeroHypercover.comp_s₀ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreZeroHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (a✝ : X✝.I₀) :
                        (CategoryStruct.comp f g).s₀ a✝ = g.s₀ (f.s₀ a✝)
                        structure CategoryTheory.Coverage.ZeroHypercover {C : Type u} [Category.{v, u} C] (J : Coverage C) (S : C) extends CategoryTheory.PreZeroHypercover S :
                        Type (max (max u v) (w + 1))

                        The type of 0-hypercovers of an object S : C in a category equipped with a coverage J. This can be constructed from a covering of S.

                        Instances For

                          The 0-hypercover defined by a single covering morphism.

                          Equations
                          Instances For

                            Pullback of a 0-hypercover along a morphism. The components are pullback f (E.f i).

                            Equations
                            Instances For

                              Pullback of a 0-hypercover along a morphism. The components are pullback (E.f i) f.

                              Equations
                              Instances For

                                Refining each component of a 0-hypercover yields a refined 0-hypercover of the base.

                                Equations
                                Instances For
                                  @[reducible, inline]
                                  abbrev CategoryTheory.Coverage.ZeroHypercover.Hom {C : Type u} [Category.{v, u} C] (J : Coverage C) {S : C} (E : J.ZeroHypercover S) (F : J.ZeroHypercover S) :
                                  Type (max (max v w) w')

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

                                  Equations
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    @[simp]
                                    theorem CategoryTheory.Coverage.ZeroHypercover.id_h₀ {C : Type u} [Category.{v, u} C] (J : Coverage C) {S : C} (x✝ : J.ZeroHypercover S) (x✝¹ : x✝.I₀) :
                                    (CategoryStruct.id x✝).h₀ x✝¹ = CategoryStruct.id (x✝.X x✝¹)
                                    @[simp]
                                    theorem CategoryTheory.Coverage.ZeroHypercover.id_s₀ {C : Type u} [Category.{v, u} C] (J : Coverage C) {S : C} (x✝ : J.ZeroHypercover S) (a : x✝.I₀) :
                                    @[simp]
                                    theorem CategoryTheory.Coverage.ZeroHypercover.comp_s₀ {C : Type u} [Category.{v, u} C] (J : Coverage C) {S : C} {X✝ Y✝ Z✝ : J.ZeroHypercover S} (f : X✝.Hom Y✝.toPreZeroHypercover) (g : Y✝.Hom Z✝.toPreZeroHypercover) (a✝ : X✝.I₀) :
                                    (CategoryStruct.comp f g).s₀ a✝ = g.s₀ (f.s₀ a✝)
                                    @[simp]
                                    theorem CategoryTheory.Coverage.ZeroHypercover.comp_h₀ {C : Type u} [Category.{v, u} C] (J : Coverage C) {S : C} {X✝ Y✝ Z✝ : J.ZeroHypercover S} (f : X✝.Hom Y✝.toPreZeroHypercover) (g : Y✝.Hom Z✝.toPreZeroHypercover) (i : X✝.I₀) :