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.)
the index type of the coverings of the fibre products
the objects in the coverings of the fibre products
the first projection
Y j ⟶ X i₁the second projection
Y j ⟶ X i₂- 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
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
The trivial pre-1-hypercover of S with a single component S.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Intersection of two pre-1-hypercovers.
Equations
- One or more equations did not get rendered due to their size.
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 the fibre products over
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.
The forgetful functor from pre-1-hypercovers to pre-0-hypercovers.
Equations
- One or more equations did not get rendered due to their size.
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
First projection from the intersection of two pre-1-hypercovers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Second projection from the intersection of two pre-1-hypercovers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Universal property of the intersection of two pre-1-hypercovers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Forget the 1-components of a OneHypercover.
Equations
- E.toZeroHypercover = { toPreZeroHypercover := E.toPreZeroHypercover, mem₀ := ⋯ }
Instances For
The trivial 1-hypercover of S where a single component S.
Equations
- CategoryTheory.GrothendieckTopology.OneHypercover.trivial J S = { toPreOneHypercover := CategoryTheory.PreOneHypercover.trivial S, mem₀ := ⋯, mem₁ := ⋯ }
Instances For
Intersection of two 1-hypercovers.
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
Equations
- One or more equations did not get rendered due to their size.
An isomorphism of 1-hypercovers is an isomorphism of pre-1-hypercovers.
Equations
Instances For
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₁ := ⋯ }