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)).
structure
CategoryTheory.PreOneHypercover
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(S : C)
:
Type (max (max u v) (w + 1))
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 - f (i : self.I₀) : self.X i ⟶ S
the morphisms in the covering of
S - I₁ (i₁ i₂ : self.I₀) : Type w
the index type of the coverings of the fibre products
- Y ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : C
the objects in the coverings of the fibre products
- w ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : CategoryTheory.CategoryStruct.comp (self.p₁ j) (self.f i₁) = CategoryTheory.CategoryStruct.comp (self.p₂ j) (self.f i₂)
Instances For
@[reducible, inline]
abbrev
CategoryTheory.PreOneHypercover.HasPullbacks
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
:
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
@[reducible, inline]
abbrev
CategoryTheory.PreOneHypercover.sieve₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
:
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
def
CategoryTheory.PreOneHypercover.sieve₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
{i₁ i₂ : E.I₀}
{W : C}
(p₁ : W ⟶ E.X i₁)
(p₂ : W ⟶ E.X i₂)
:
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
@[simp]
theorem
CategoryTheory.PreOneHypercover.sieve₁_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
{i₁ i₂ : E.I₀}
{W : C}
(p₁ : W ⟶ E.X i₁)
(p₂ : W ⟶ E.X i₂)
(Z : C)
(g : Z ⟶ W)
:
(E.sieve₁ p₁ p₂).arrows g = ∃ (j : E.I₁ i₁ i₂) (h : Z ⟶ E.Y j),
CategoryTheory.CategoryStruct.comp g p₁ = CategoryTheory.CategoryStruct.comp h (E.p₁ j) ∧ CategoryTheory.CategoryStruct.comp g p₂ = CategoryTheory.CategoryStruct.comp h (E.p₂ j)
@[reducible, inline]
noncomputable abbrev
CategoryTheory.PreOneHypercover.toPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
{i₁ i₂ : E.I₀}
(j : E.I₁ i₁ i₂)
[CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)]
:
E.Y j ⟶ CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂)
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
def
CategoryTheory.PreOneHypercover.sieve₁'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(i₁ i₂ : E.I₀)
[CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)]
:
CategoryTheory.Sieve (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))
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
theorem
CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
{i₁ i₂ : E.I₀}
[CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)]
{W : C}
(p₁ : W ⟶ E.X i₁)
(p₂ : W ⟶ E.X i₂)
(w : CategoryTheory.CategoryStruct.comp p₁ (E.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (E.f i₂))
:
E.sieve₁ p₁ p₂ = CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)
theorem
CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(i₁ i₂ : E.I₀)
[CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)]
:
E.sieve₁' i₁ i₂ = E.sieve₁ (CategoryTheory.Limits.pullback.fst (E.f i₁) (E.f i₂)) (CategoryTheory.Limits.pullback.snd (E.f i₁) (E.f i₂))
@[reducible, inline]
abbrev
CategoryTheory.PreOneHypercover.I₁'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
:
Type w
The sigma type of all E.I₁ i₁ i₂ for ⟨i₁, i₂⟩ : E.I₀ × E.I₀.
Instances For
def
CategoryTheory.PreOneHypercover.multicospanIndex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
:
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
@[simp]
theorem
CategoryTheory.PreOneHypercover.multicospanIndex_sndTo
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
(j : E.I₁')
:
(E.multicospanIndex F).sndTo j = j.fst.2
@[simp]
theorem
CategoryTheory.PreOneHypercover.multicospanIndex_L
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
:
(E.multicospanIndex F).L = E.I₀
@[simp]
theorem
CategoryTheory.PreOneHypercover.multicospanIndex_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
(j : E.I₁')
:
(E.multicospanIndex F).fst j = F.map (E.p₁ j.snd).op
@[simp]
theorem
CategoryTheory.PreOneHypercover.multicospanIndex_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
(j : E.I₁')
:
(E.multicospanIndex F).right j = F.obj (Opposite.op (E.Y j.snd))
@[simp]
theorem
CategoryTheory.PreOneHypercover.multicospanIndex_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
(i : E.I₀)
:
(E.multicospanIndex F).left i = F.obj (Opposite.op (E.X i))
@[simp]
theorem
CategoryTheory.PreOneHypercover.multicospanIndex_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
(j : E.I₁')
:
(E.multicospanIndex F).snd j = F.map (E.p₂ j.snd).op
@[simp]
theorem
CategoryTheory.PreOneHypercover.multicospanIndex_fstTo
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
(j : E.I₁')
:
(E.multicospanIndex F).fstTo j = j.fst.1
@[simp]
theorem
CategoryTheory.PreOneHypercover.multicospanIndex_R
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
:
(E.multicospanIndex F).R = E.I₁'
def
CategoryTheory.PreOneHypercover.multifork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{S : C}
(E : CategoryTheory.PreOneHypercover S)
(F : CategoryTheory.Functor Cᵒᵖ A)
:
CategoryTheory.Limits.Multifork (E.multicospanIndex F)
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.multicospanIndex F).L) => F.map (E.f i₀).op) ⋯
Instances For
structure
CategoryTheory.GrothendieckTopology.OneHypercover
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(S : C)
extends CategoryTheory.PreOneHypercover S :
Type (max (max u v) (w + 1))
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₂) : CategoryTheory.CategoryStruct.comp (self.p₁ j) (self.f i₁) = CategoryTheory.CategoryStruct.comp (self.p₂ j) (self.f i₂)
- mem₀ : self.sieve₀ ∈ J S
- mem₁ (i₁ i₂ : self.I₀) ⦃W : C⦄ (p₁ : W ⟶ self.X i₁) (p₂ : W ⟶ self.X i₂) (w : CategoryTheory.CategoryStruct.comp p₁ (self.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (self.f i₂)) : self.sieve₁ p₁ p₂ ∈ J W
Instances For
theorem
CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{S : C}
(E : J.OneHypercover S)
(i₁ i₂ : E.I₀)
[CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)]
:
E.sieve₁' i₁ i₂ ∈ J (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))
def
CategoryTheory.GrothendieckTopology.OneHypercover.mk'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{S : C}
(E : CategoryTheory.PreOneHypercover S)
[E.HasPullbacks]
(mem₀ : E.sieve₀ ∈ J S)
(mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂)))
:
J.OneHypercover S
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
@[simp]
theorem
CategoryTheory.GrothendieckTopology.OneHypercover.mk'_toPreOneHypercover
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{S : C}
(E : CategoryTheory.PreOneHypercover S)
[E.HasPullbacks]
(mem₀ : E.sieve₀ ∈ J S)
(mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂)))
:
(CategoryTheory.GrothendieckTopology.OneHypercover.mk' E mem₀ mem₁').toPreOneHypercover = E
noncomputable def
CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{J : CategoryTheory.GrothendieckTopology C}
{S : C}
{E : J.OneHypercover S}
{F : CategoryTheory.Sheaf J A}
(c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.val))
:
c.pt ⟶ F.val.obj (Opposite.op S)
Auxiliary definition of isLimitMultifork.
Equations
- CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c = ⋯.amalgamateOfArrows E.f ⋯ c.ι ⋯
Instances For
theorem
CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_3, u_1} A]
{J : CategoryTheory.GrothendieckTopology C}
{S : C}
{E : J.OneHypercover S}
{F : CategoryTheory.Sheaf J A}
(c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.val))
(i₀ : E.I₀)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c)
(F.val.map (E.f i₀).op) = c.ι i₀
theorem
CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_3, u_1} A]
{J : CategoryTheory.GrothendieckTopology C}
{S : C}
{E : J.OneHypercover S}
{F : CategoryTheory.Sheaf J A}
(c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.val))
(i₀ : E.I₀)
{Z : A}
(h : F.val.obj (Opposite.op (E.X i₀)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c)
(CategoryTheory.CategoryStruct.comp (F.val.map (E.f i₀).op) h) = CategoryTheory.CategoryStruct.comp (c.ι i₀) h
noncomputable def
CategoryTheory.GrothendieckTopology.OneHypercover.isLimitMultifork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : Type u_1}
[CategoryTheory.Category.{u_2, u_1} A]
{J : CategoryTheory.GrothendieckTopology C}
{S : C}
(E : J.OneHypercover S)
(F : CategoryTheory.Sheaf J A)
:
CategoryTheory.Limits.IsLimit (E.multifork F.val)
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
def
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
:
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
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
:
S.preOneHypercover.I₀ = S.Arrow
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
(x✝ x✝¹ : S.Arrow)
(r : x✝.Relation x✝¹)
:
S.preOneHypercover.p₂ r = r.g₂
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_X
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
(f : S.Arrow)
:
S.preOneHypercover.X f = f.Y
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_Y
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
(x✝ x✝¹ : S.Arrow)
(r : x✝.Relation x✝¹)
:
S.preOneHypercover.Y r = r.Z
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
(x✝ x✝¹ : S.Arrow)
(r : x✝.Relation x✝¹)
:
S.preOneHypercover.p₁ r = r.g₁
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
(f : S.Arrow)
:
S.preOneHypercover.f f = f.f
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
(f₁ f₂ : S.Arrow)
:
S.preOneHypercover.I₁ f₁ f₂ = f₁.Relation f₂
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₀
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
:
S.preOneHypercover.sieve₀ = ↑S
theorem
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
(f₁ f₂ : S.Arrow)
{W : C}
(p₁ : W ⟶ f₁.Y)
(p₂ : W ⟶ f₂.Y)
(w : CategoryTheory.CategoryStruct.comp p₁ f₁.f = CategoryTheory.CategoryStruct.comp p₂ f₂.f)
:
def
CategoryTheory.GrothendieckTopology.Cover.oneHypercover
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
:
J.OneHypercover X
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₁ := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.GrothendieckTopology.Cover.oneHypercover_toPreOneHypercover
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{X : C}
(S : J.Cover X)
:
S.oneHypercover.toPreOneHypercover = S.preOneHypercover