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

• CategoryTheory.GrothendieckTopology.CoversTop J 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) : CategoryTheory.GrothendieckTopology.CoversTop J Y ↔ CategoryTheory.Sieve.ofObjects Y X ∈ J.sieves X

@[inline, reducible]

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 : CategoryTheory.GrothendieckTopology.CoversTop J Y) (W : C) : CategoryTheory.GrothendieckTopology.Cover J W

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

Equations

• CategoryTheory.GrothendieckTopology.CoversTop.cover hY W = { val := CategoryTheory.Sieve.ofObjects Y W, property := (_ : CategoryTheory.Sieve.ofObjects Y W ∈ J.sieves 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 : CategoryTheory.GrothendieckTopology.CoversTop J 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 : CategoryTheory.GrothendieckTopology.CoversTop J Y) (F : CategoryTheory.Sheaf J (Type u_2)) {x : ↑(CategoryTheory.Functor.sections F.val)} {y : ↑(CategoryTheory.Functor.sections F.val)} (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.toPrefunctor.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

• CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible x = ∀ (Z : C) (i j : I) (f : Z ⟶ Y i) (g : Z ⟶ Y j), F.toPrefunctor.map f.op (x i) = F.toPrefunctor.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

• CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements x✝¹ X x hf = F.toPrefunctor.map (Nonempty.some (_ : Nonempty (x✝ ⟶ Y (Exists.choose hf)))).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 : CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible x) {X : C} {Z : C} (f : Z ⟶ X) (i : I) (φ : Z ⟶ Y i) : CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements x X f (_ : ∃ (i : I), Nonempty (Z ⟶ Y i)) = F.toPrefunctor.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 : CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible x) (X : C) : CategoryTheory.Presieve.FamilyOfElements.Compatible (CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements x X)

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 : CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible x) (hY : CategoryTheory.GrothendieckTopology.CoversTop J Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) : ∃! (s : ↑(CategoryTheory.Functor.sections F)), ∀ (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 : CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible x) (hY : CategoryTheory.GrothendieckTopology.CoversTop J Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) : ↑(CategoryTheory.Functor.sections F)

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

Equations

• CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_ hx hY hF = Exists.choose (_ : ∃! (s : ↑(CategoryTheory.Functor.sections F)), ∀ (i : I), ↑s (Opposite.op (Y i)) = x i)

@[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 : CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible x) (hY : CategoryTheory.GrothendieckTopology.CoversTop J Y) (hF : CategoryTheory.Presheaf.IsSheaf J F) (i : I) : ↑(CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_ hx hY hF) (Opposite.op (Y i)) = x i