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))
.
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.)
- I₀ : Type w
the index type of the covering of
S
- X (i : self.I₀) : C
the objects in the covering of
S
the morphisms in the covering of
S
the index type of the coverings of the fibre products
the objects in the coverings of the fibre products
- 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
The assumption that the pullback of X i₁
and X i₂
over S
exists
for any i₁
and i₂
.
Equations
- E.HasPullbacks = ∀ (i₁ i₂ : E.I₀), CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)
Instances For
The sieve of S
that is generated by the morphisms f i : X i ⟶ S
.
Equations
- E.sieve₀ = CategoryTheory.Sieve.ofArrows E.X E.f
Instances For
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
The obvious morphism E.Y j ⟶ pullback (E.f i₁) (E.f i₂)
given by E : PreOneHypercover S
.
Equations
- E.toPullback j = CategoryTheory.Limits.pullback.lift (E.p₁ j) (E.p₂ j) ⋯
Instances For
The sieve of pullback (E.f i₁) (E.f i₂)
given by E : PreOneHypercover S
.
Equations
- E.sieve₁' i₁ i₂ = CategoryTheory.Sieve.ofArrows E.Y fun (j : E.I₁ i₁ i₂) => E.toPullback j
Instances For
The sigma type of all E.I₁ i₁ i₂
for ⟨i₁, i₂⟩ : E.I₀ × E.I₀
.
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
- E.multifork F = CategoryTheory.Limits.Multifork.ofι (E.multicospanIndex F) (F.obj (Opposite.op S)) (fun (i₀ : E.multicospanShape.L) => F.map (E.f i₀).op) ⋯
Instances For
A morphism of pre-1
-hypercovers of S
is a family of refinement morphisms commuting
with the structure morphisms of E
and F
.
The map between indexing types of the coverings of
S
The map between indexing types of the coverings of the fibre products over
S
.The refinement morphisms between objects in the coverings of
S
.The refinement morphisms between objects in the coverings of the fibre products over
S
.- w₁₁ {i j : E.I₀} (k : E.I₁ i j) : CategoryStruct.comp (self.h₁ k) (F.p₁ (self.s₁ k)) = CategoryStruct.comp (E.p₁ k) (self.h₀ i)
- w₁₂ {i j : E.I₀} (k : E.I₁ i j) : CategoryStruct.comp (self.h₁ k) (F.p₂ (self.s₁ k)) = CategoryStruct.comp (E.p₂ k) (self.h₀ j)
Instances For
The identity refinement of a pre-1
-hypercover.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Composition of refinement morphisms of pre-1
-hypercovers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The induced index map E.I₁' → F.I₁'
from a refinement morphism E ⟶ F
.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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 morphism
Xᵢ ⟶ Yₐ
.
Instances For
A refinement morphism E ⟶ F
induces a morphism on associated multiequalizers.
Equations
- f.mapMultiforkOfIsLimit P hc d = CategoryTheory.Limits.Multifork.IsLimit.lift hc (fun (a : E.multicospanShape.L) => CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (P.map (f.h₀ a).op)) ⋯
Instances For
Homotopic refinements induce the same map on multiequalizers.
(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
(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
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 OneHpyercover.cylinder
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Implementation): The refinement morphism cylinder f g ⟶ E
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(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
Up to homotopy, the category of (pre-)1
-hypercovers is cofiltered.
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'
).
- 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
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
- CategoryTheory.GrothendieckTopology.OneHypercover.mk' E mem₀ mem₁' = { toPreOneHypercover := E, mem₀ := mem₀, mem₁ := ⋯ }
Instances For
Auxiliary definition of isLimitMultifork
.
Equations
Instances For
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
A morphism of 1
-hypercovers is a morphism of the underlying pre-1
-hypercovers.
Equations
- E.Hom F = E.Hom F.toPreOneHypercover
Instances For
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
Up to homotopy, the category of 1
-hypercovers is cofiltered.
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
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
- S.oneHypercover = { toPreOneHypercover := S.preOneHypercover, mem₀ := ⋯, mem₁ := ⋯ }