Documentation

Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

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 (TODO, Christian).

Main definitions #

source
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
    source
    @[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
    source
    @[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
    source
    theorem CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq {C : Type u} [Category.{v, u} C] {S : C} {A : Type u_1} [Category.{u_2, 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.

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[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
          source
          @[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))
          source
          @[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)
          source
          @[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))
          source
          @[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
          source
          @[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))
          source
          @[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) ⋯)
          source
          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) ⋯)
          source
          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)
          source
          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)
          source
          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
            source
            @[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
            source
            @[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
            source
            @[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)
            source
            @[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) ⋯)
            source
            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.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              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.

              source
              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.

              Equations
              Instances For
                source
                @[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
                source
                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.