0-hypercovers #
Given a coverage J
on a category C
, we define the tyoe
of 0
-hypercovers of an object S : C
. They consists of a covering family
of morphisms X i ⟶ S
indexed by a type I₀
such that the induced presieve is in J
.
We define this with respect to a coverage and not to a Grothendieck topology, because this yields more control over the components of the cover.
The categorical data that is involved in a 0
-hypercover of an object S
. This
consists of a family of morphisms f i : X i ⟶ S
for i : I₀
.
- 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
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 presieve of S
that is generated by the morphisms f i : X i ⟶ S
.
Equations
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
The pre-0
-hypercover defined by a single morphism.
Equations
- CategoryTheory.PreZeroHypercover.singleton f = { I₀ := PUnit.{?u.11 + 1}, X := fun (x : PUnit.{?u.11 + 1}) => S, f := fun (x : PUnit.{?u.11 + 1}) => f }
Instances For
Pullback of a pre-0
-hypercover along a morphism. The components are pullback f (E.f i)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pullback of a pre-0
-hypercover along a morphism. The components are pullback (E.f i) f
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Refining each component of a pre-0
-hypercover yields a refined pre-0
-hypercover of the
base.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A morphism of pre-0
-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 refinement morphisms between objects in the coverings of
S
.
Instances For
The identity refinement of a pre-0
-hypercover.
Equations
- CategoryTheory.PreZeroHypercover.Hom.id E = { s₀ := id, h₀ := fun (x : E.I₀) => CategoryTheory.CategoryStruct.id (E.X x), w₀ := ⋯ }
Instances For
Composition of refinement morphisms of pre-0
-hypercovers.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
The type of 0
-hypercovers of an object S : C
in a category equipped with a
coverage J
. This can be constructed from a covering of S
.
Instances For
The 0
-hypercover defined by a single covering morphism.
Equations
- CategoryTheory.Coverage.ZeroHypercover.singleton J f hf = { toPreZeroHypercover := CategoryTheory.PreZeroHypercover.singleton f, mem₀ := ⋯ }
Instances For
Pullback of a 0
-hypercover along a morphism. The components are pullback f (E.f i)
.
Equations
- CategoryTheory.Coverage.ZeroHypercover.pullback₁ J f E = { toPreZeroHypercover := CategoryTheory.PreZeroHypercover.pullback₁ f E.toPreZeroHypercover, mem₀ := ⋯ }
Instances For
Pullback of a 0
-hypercover along a morphism. The components are pullback (E.f i) f
.
Equations
- CategoryTheory.Coverage.ZeroHypercover.pullback₂ J f E = { toPreZeroHypercover := CategoryTheory.PreZeroHypercover.pullback₂ f E.toPreZeroHypercover, mem₀ := ⋯ }
Instances For
Refining each component of a 0
-hypercover yields a refined 0
-hypercover of the base.
Equations
- CategoryTheory.Coverage.ZeroHypercover.bind J E F = { toPreZeroHypercover := E.bind fun (i : E.I₀) => (F i).toPreZeroHypercover, mem₀ := ⋯ }
Instances For
A morphism of 0
-hypercovers is a morphism of the underlying pre-0
-hypercovers.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.