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 refinementsE ⟶ Fis a family of morphismsXᵢ ⟶ YₐwhereYₐis a component of the cover ofX_{f(i)} ×[S] X_{g(i)}.CategoryTheory.GrothendieckTopology.HOneHypercover: The category of1-hypercovers with respect to a Grothendieck topology and morphisms up to homotopy.
Main results #
CategoryTheory.GrothendieckTopology.HOneHypercover.isCofiltered_of_hasPullbacks: The category of1-hypercovers up to homotopy is cofiltered ifChas 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)}.
The index map sending
i : E.I₀toaabove(f(i), g(i)).The morphism
Xᵢ ⟶ Yₐ.
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)
:
CategoryStruct.comp (self.a i) (CategoryStruct.comp (F.p₂ (self.H i)) h) = CategoryStruct.comp (g.h₀ i) h
@[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
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))
:
Homotopic refinements induce the same map on multiequalizers.
def
CategoryTheory.PreOneHypercover.Homotopy.isLimitMultifork
{C : Type u}
[Category.{v, u} C]
{S : C}
{E : PreOneHypercover S}
{F : PreOneHypercover S}
{A : Type u_1}
[Category.{v_1, u_1} A]
(f : E.Hom F)
(g : F.Hom E)
(hgf : Homotopy (g.comp f) (Hom.id F))
{G : Functor Cᵒᵖ A}
(hE : Limits.IsLimit (E.multifork G))
:
Limits.IsLimit (F.multifork G)
If f : E ⟶ F and g : F ⟶ E are refinement morphisms of pre-1-hypercovers such that
the composition g ≫ f is homotopic to the identity, then if the multifork associated
to E is exact also the multifork associated to F is exact.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.PreOneHypercover.Homotopy.isLimitMultiforkEquiv
{C : Type u}
[Category.{v, u} C]
{S : C}
{E : PreOneHypercover S}
{F : PreOneHypercover S}
{A : Type u_1}
[Category.{v_1, u_1} A]
(f : E.Hom F)
(g : F.Hom E)
(hfg : Homotopy (f.comp g) (Hom.id E))
(hgf : Homotopy (g.comp f) (Hom.id F))
{G : Functor Cᵒᵖ A}
:
E and F are homotopy equivalent, then the multifork associated
to E is exact if and only if the multifork associated to F is exact.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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
- CategoryTheory.PreOneHypercover.cylinderX f g k = CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.toPullback k)
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))
:
(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
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)
:
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
@[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))
:
@[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)
:
@[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))
:
@[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) ⋯)
@[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))
:
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)
:
(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✝)
:
@[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_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₀)
:
@[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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
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.
Equations
Instances For
@[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)
:
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!
Equations
Instances For
@[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.
Equations
Instances For
@[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.
Equations
Instances For
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)
:
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.