Objects which cover the terminal object

In this file, given a site (C, J), we introduce the notion of a family of objects Y : I → C which "cover the final object": this means that for all X : C, the sieve Sieve.ofObjects Y X is covering for J. When there is a terminal object X : C, then J.CoversTop Y holds iff Sieve.ofObjects Y X is covering for J.

We introduce a notion of compatible family of elements on objects Y and obtain Presheaf.FamilyOfElementsOnObjects.IsCompatible.exists_unique_section which asserts that if a presheaf of types is a sheaf, then any compatible family of elements on objects Y which cover the final object extends as a section of this presheaf.

def CategoryTheory.GrothendieckTopology.CoversTop {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {I : Type u_1} (Y : I → C) : Prop

A family of objects Y : I → C "covers the final object" if for all X : C, the sieve ofObjects Y X is a covering sieve.

Equations

• J.CoversTop Y = ∀ (X : C), CategoryTheory.Sieve.ofObjects Y X ∈ J.sieves X

theorem CategoryTheory.GrothendieckTopology.coversTop_iff_of_isTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) (hX : CategoryTheory.Limits.IsTerminal X) {I : Type u_1} (Y : I → C) : J.CoversTop Y ↔ CategoryTheory.Sieve.ofObjects Y X ∈ J.sieves X

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.CoversTop.cover {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {I : Type u_1} {Y : I → C} (hY : J.CoversTop Y) (W : C) : J.Cover W

The cover of any object W : C attached to a family of objects Y that satisfy J.CoversTop Y

Equations

• hY.cover W = ⟨CategoryTheory.Sieve.ofObjects Y W, ⋯⟩

theorem CategoryTheory.GrothendieckTopology.CoversTop.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {I : Type u_1} {Y : I → C} (hY : J.CoversTop Y) (F : CategoryTheory.Sheaf J A) {c : CategoryTheory.Limits.Cone F.val} (hc : CategoryTheory.Limits.IsLimit c) {X : A} {f : X ⟶ c.pt} {g : X ⟶ c.pt} (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp f (c.π.app (Opposite.op (Y i))) = CategoryTheory.CategoryStruct.comp g (c.π.app (Opposite.op (Y i)))) : f = g

theorem CategoryTheory.GrothendieckTopology.CoversTop.sections_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {I : Type u_1} {Y : I → C} (hY : J.CoversTop Y) (F : CategoryTheory.Sheaf J (Type u_2)) {x : ↑F.val.sections} {y : ↑F.val.sections} (h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))) : x = y

def CategoryTheory.Presheaf.FamilyOfElementsOnObjects {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) {I : Type u_1} (Y : I → C) : Type (max u_1 w)

A family of elements of a presheaf of types F indexed by a family of objects Y : I → C consists of the data of an element in F.obj (Opposite.op (Y i)) for all i.

Equations

• CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y = ((i : I) → F.obj (Opposite.op (Y i)))

def CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} (x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y) : Prop

x : FamilyOfElementsOnObjects F Y is compatible if for any object Z such that there exists a morphism f : Z → Y i, then the pullback of x i by f is independent of f and i.

Equations

• x.IsCompatible = ∀ (Z : C) (i j : I) (f : Z ⟶ Y i) (g : Z ⟶ Y j), F.map f.op (x i) = F.map g.op (x j)

noncomputable def CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} (x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y) (X : C) : CategoryTheory.Presieve.FamilyOfElements F (CategoryTheory.Sieve.ofObjects Y X).arrows

A family of elements indexed by Sieve.ofObjects Y X that is induced by x : FamilyOfElementsOnObjects F Y. See the equational lemma IsCompatible.familyOfElements_apply which holds under the assumption x.IsCompatible.

Equations

• x✝¹.familyOfElements X x hf = F.map ⋯.some.op (x✝¹ (Exists.choose hf))

theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) {X : C} {Z : C} (f : Z ⟶ X) (i : I) (φ : Z ⟶ Y i) : x.familyOfElements X f ⋯ = F.map φ.op (x i)

theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_isCompatible {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (X : C) : (x.familyOfElements X).Compatible

theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.exists_unique_section {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) : ∃! s : ↑F.sections, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i

noncomputable def CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_ {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) : ↑F.sections

The section of a sheaf of types which lifts a compatible family of elements indexed by objects which cover the terminal object.

Equations

• hx.section_ hY hF = Exists.choose ⋯

@[simp]

theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y} (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) (i : I) : ↑(hx.section_ hY hF) (Opposite.op (Y i)) = x i