The category of 1-hypercovers up to homotopy

In this file we define the category of 1-hypercovers up to homotopy. This is the category of 1-hypercovers, but where morphisms are considered up to existence of a homotopy.

Main definitions

• CategoryTheory.PreOneHypercover.Homotopy: 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)}.
• CategoryTheory.GrothendieckTopology.HOneHypercover: The category of 1-hypercovers with respect to a Grothendieck topology and morphisms up to homotopy.

Main results

• CategoryTheory.GrothendieckTopology.HOneHypercover.isCofiltered_of_hasPullbacks: The category of 1-hypercovers up to homotopy is cofiltered if C has pullbacks.

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)}.

• H (i : E.I₀) : F.I₁ (f.s₀ i) (g.s₀ i)

  The index map sending i : E.I₀ to a above (f(i), g(i)).

• a (i : E.I₀) : E.X i ⟶ F.Y (self.H i)

  The morphism Xᵢ ⟶ Yₐ.

• wl (i : E.I₀) : CategoryStruct.comp (self.a i) (F.p₁ (self.H i)) = f.h₀ i
• wr (i : E.I₀) : CategoryStruct.comp (self.a i) (F.p₂ (self.H i)) = g.h₀ i

@[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) : CategoryStruct.comp (self.a i) (CategoryStruct.comp (F.p₁ (self.H i)) h) = CategoryStruct.comp (f.h₀ i) h

@[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) : CategoryStruct.comp (self.a i) (CategoryStruct.comp (F.p₂ (self.H i)) h) = CategoryStruct.comp (g.h₀ i) h

theorem CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq {C : Type u} [Category.{v, u} C] {S : C} {A : Type u_1} [Category.{v_1, u_1} A] {E F : PreOneHypercover S} {f g : E.Hom F} (H : Homotopy f g) (P : Functor Cᵒᵖ A) {c : Limits.Multifork (E.multicospanIndex P)} (hc : Limits.IsLimit c) (d : Limits.Multifork (F.multicospanIndex P)) : f.mapMultiforkOfIsLimit P hc d = g.mapMultiforkOfIsLimit P hc d

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.

@[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.

noncomputable def CategoryTheory.PreOneHypercover.cylinder {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : PreOneHypercover S

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 OneHypercover.cylinder).

@[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) (p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (cylinder f g).I₁ p q = ULift.{max w w', w} (E.I₁ p.fst q.fst)

@[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

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinder_p₂ {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)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (cylinder f g).p₂ k = CategoryStruct.comp (Limits.pullback.fst (Limits.pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)) (Limits.pullback.snd (cylinderf f g p.snd) (cylinderf f g q.snd))

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinder_p₁ {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)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (cylinder f g).p₁ k = CategoryStruct.comp (Limits.pullback.fst (Limits.pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)) (Limits.pullback.fst (cylinderf f g p.snd) (cylinderf f g q.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_Y {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)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (cylinder f g).Y k = Limits.pullback (Limits.pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)

theorem CategoryTheory.PreOneHypercover.toPullback_cylinder {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) : (cylinder f g).toPullback k = Limits.pullback.fst (Limits.pullback.map (cylinderf f g i.snd) (cylinderf f g j.snd) (E.f i.fst) (E.f j.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)

theorem CategoryTheory.PreOneHypercover.sieve₀_cylinder {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).sieve₀ = Sieve.generate (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) => (Sieve.pullback (Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)

theorem CategoryTheory.PreOneHypercover.sieve₁'_cylinder {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 : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (cylinder f g).sieve₁' i j = Sieve.pullback (Limits.pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (CategoryStruct.id S) ⋯ ⋯) (E.sieve₁' i.fst j.fst)

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.

@[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✝) : (cylinderHom f g).s₁ k = k.down

@[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) (p : (cylinder f g).I₀) : (cylinderHom f g).s₀ p = p.fst

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinderHom_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (p : (cylinder f g).I₀) : (cylinderHom f g).h₀ p = Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinderHom_h₁ {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 : (cylinder f g).I₀} (k : (cylinder f g).I₁ p q) : (cylinderHom f g).h₁ k = Limits.pullback.snd (Limits.pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)

noncomputable def CategoryTheory.PreOneHypercover.cylinderHomotopy {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : Homotopy ((cylinderHom f g).comp f) ((cylinderHom f g).comp g)

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

theorem CategoryTheory.PreOneHypercover.exists_nonempty_homotopy {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : ∃ (W : PreOneHypercover S) (h : W.Hom E), Nonempty (Homotopy (h.comp f) (h.comp g))

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

noncomputable def CategoryTheory.GrothendieckTopology.OneHypercover.cylinder {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : J.OneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : J.OneHypercover S

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.

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.cylinder_toPreOneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : J.OneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : (cylinder f g).toPreOneHypercover = PreOneHypercover.cylinder f g

theorem CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : J.OneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : ∃ (W : J.OneHypercover S) (h : W.Hom E), Nonempty (PreOneHypercover.Homotopy (PreOneHypercover.Hom.comp h f) (PreOneHypercover.Hom.comp h g))

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

def CategoryTheory.GrothendieckTopology.OneHypercover.homotopicRel {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (S : C) : HomRel (J.OneHypercover S)

Two refinement morphisms of 1-hypercovers are homotopic if there exists a homotopy between them. Note: This is not an equivalence relation, it is not even reflexive!

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.HOneHypercover {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (S : C) : Type (max (max u v) (u_1 + 1))

The category of 1-hypercovers with refinement morphisms up to homotopy.

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.OneHypercover.toHOneHypercover {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (S : C) : Functor (J.OneHypercover S) (J.HOneHypercover S)

The canonical projection from 1-hypercovers to 1-hypercovers up to homotopy.

theorem CategoryTheory.PreOneHypercover.Homotopy.map_eq_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {S : C} {E F : J.OneHypercover S} {f g : E ⟶ F} (H : Homotopy f g) : (GrothendieckTopology.OneHypercover.toHOneHypercover J S).map f = (GrothendieckTopology.OneHypercover.toHOneHypercover J S).map g

instance CategoryTheory.GrothendieckTopology.HOneHypercover.instNonempty {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {S : C} : Nonempty (J.HOneHypercover S)

instance CategoryTheory.GrothendieckTopology.HOneHypercover.isCofiltered_of_hasPullbacks {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {S : C} [Limits.HasPullbacks C] : IsCofiltered (J.HOneHypercover S)

If C has pullbacks, the category of 1-hypercovers up to homotopy is cofiltered.