Alternative constructor for points

Let J be a Grothendieck topology on a category C. We provide a constructor Point.ofIsCofiltered for points for J which takes as inputs:

• a functor p : N ⥤ C where N is cofiltered and initially small
• the assumption that for any covering sieve R of X, any morphism f : p.obj U ⟶ X, there exists a morphism g : Y ⟶ X in R, a morphism q : V ⟶ U in N and a morphism a : p.obj V ⟶ Y such that a ≫ g = p.map q ≫ f. We show that the fiber of a presheaf for the constructed point identifies to a colimit indexed by the category N.

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instHasColimitsOfShapeOppositeType {N : Type u'} [Category.{v', u'} N] [InitiallySmall N] : Limits.HasColimitsOfShape Nᵒᵖ (Type w)

noncomputable def CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] : Functor C (Type w)

Given a functor p : N ⥤ C, this is the functor C ⥤ Type w which sends X : C to the colimit of types of morphisms p.obj U ⟶ X for U : N.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] {p : Functor N C} [InitiallySmall N] {U : N} {X : C} (f : p.obj U ⟶ X) : (fiber p).obj X

Constructor for elements in fiber.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_jointly_surjective {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] {p : Functor N C} [InitiallySmall N] {X : C} (x : (fiber p).obj X) : ∃ (U : N) (f : p.obj U ⟶ X), fiberMk f = x

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.exists_of_fiberMk_eq_fiberMk {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] {p : Functor N C} [InitiallySmall N] [IsCofiltered N] {U : N} {X : C} {f₁ f₂ : p.obj U ⟶ X} (hf : fiberMk f₁ = fiberMk f₂) : ∃ (V : N) (g : V ⟶ U), CategoryStruct.comp (p.map g) f₁ = CategoryStruct.comp (p.map g) f₂

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_map_comp {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {U V : N} (g : V ⟶ U) {X : C} (f : p.obj U ⟶ X) : fiberMk (CategoryStruct.comp (p.map g) f) = fiberMk f

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {U V : N} (g : V ⟶ U) : fiberMk (p.map g) = fiberMk (CategoryStruct.id (p.obj U))

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiber_map_fiberMk {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {U : N} {X : C} (f : p.obj U ⟶ X) {Y : C} (g : X ⟶ Y) : (ConcreteCategory.hom ((fiber p).map g)) (fiberMk f) = fiberMk (CategoryStruct.comp f g)

noncomputable def CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] : Functor N (fiber p).Elements

A functor N ⥤ (fiber p).Elements which is initial when N is cofiltered and initially small.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_obj_snd {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] (U : N) : ((functor p).obj U).snd = fiberMk (CategoryStruct.id (p.obj U))

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_obj_fst {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] (U : N) : ((functor p).obj U).fst = p.obj U

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.functor_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {U V : N} (f : U ⟶ V) : (functor p).map f = CategoryOfElements.homMk ((fiber p).elementsMk (p.obj U) (fiberMk (CategoryStruct.id (p.obj U)))) ((fiber p).elementsMk (p.obj V) (fiberMk (CategoryStruct.id (p.obj V)))) (p.map f) ⋯

instance CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instInitialElementsFiberFunctorOfIsCofiltered {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] [IsCofiltered N] : (functor p).Initial

instance CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instInitiallySmallElementsFiberOfIsCofiltered {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] [IsCofiltered N] : InitiallySmall (fiber p).Elements

instance CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instIsCofilteredElementsFiber {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] [IsCofiltered N] : IsCofiltered (fiber p).Elements

noncomputable def CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) : J.Point

Constructor for points of Grothendieck topologies J : GrothendieckTopology C that are given by a functor p : N ⥤ C from a cofiltered and initially small category N.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered_fiber {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) : (ofIsCofiltered p hp).fiber = ofIsCofiltered.fiber p

noncomputable def CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (U : N) (P : Functor Cᵒᵖ A) : P.obj (Opposite.op (p.obj U)) ⟶ (ofIsCofiltered p hp).presheafFiber.obj P

The canonical maps P.obj (op (p.obj U)) ⟶ (ofIsCofiltered p hp).presheafFiber.obj P that are part of the colimit cocone presheafFiberOfIsCofilteredCocone.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] {V U : N} (f : V ⟶ U) (P : Functor Cᵒᵖ A) : CategoryStruct.comp (P.map (p.map f).op) (toPresheafFiberOfIsCofiltered p hp V P) = toPresheafFiberOfIsCofiltered p hp U P

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w_assoc {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] {V U : N} (f : V ⟶ U) (P : Functor Cᵒᵖ A) {Z : A} (h : (ofIsCofiltered p hp).presheafFiber.obj P ⟶ Z) : CategoryStruct.comp (P.map (p.map f).op) (CategoryStruct.comp (toPresheafFiberOfIsCofiltered p hp V P) h) = CategoryStruct.comp (toPresheafFiberOfIsCofiltered p hp U P) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_naturality {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : Functor Cᵒᵖ A} (g : P ⟶ Q) (U : N) : CategoryStruct.comp (toPresheafFiberOfIsCofiltered p hp U P) ((ofIsCofiltered p hp).presheafFiber.map g) = CategoryStruct.comp (g.app (Opposite.op (p.obj U))) (toPresheafFiberOfIsCofiltered p hp U Q)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_naturality_assoc {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : Functor Cᵒᵖ A} (g : P ⟶ Q) (U : N) {Z : A} (h : (ofIsCofiltered p hp).presheafFiber.obj Q ⟶ Z) : CategoryStruct.comp (toPresheafFiberOfIsCofiltered p hp U P) (CategoryStruct.comp ((ofIsCofiltered p hp).presheafFiber.map g) h) = CategoryStruct.comp (g.app (Opposite.op (p.obj U))) (CategoryStruct.comp (toPresheafFiberOfIsCofiltered p hp U Q) h)

noncomputable def CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Cᵒᵖ A) : Limits.Cocone (p.op.comp P)

The (colimit) cocone which, for a point constructed using Point.ofIsCofiltered and a functor p : N ⥤ C expresses the fiber of a presheaf as a colimit indexed indexed by N.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_pt {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Cᵒᵖ A) : (presheafFiberOfIsCofilteredCocone p hp P).pt = (ofIsCofiltered p hp).presheafFiber.obj P

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_ι_app {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Cᵒᵖ A) (U : Nᵒᵖ) : (presheafFiberOfIsCofilteredCocone p hp P).ι.app U = toPresheafFiberOfIsCofiltered p hp (Opposite.unop U) P

noncomputable def CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberOfIsCofilteredCocone {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {N : Type u'} [Category.{v', u'} N] (p : Functor N C) [InitiallySmall N] {J : GrothendieckTopology C} [IsCofiltered N] (hp : ∀ ⦃X : C⦄, ∀ R ∈ J X, ∀ ⦃U : N⦄ (f : p.obj U ⟶ X), ∃ (Y : C) (g : Y ⟶ X) (_ : R.arrows g) (V : N) (q : V ⟶ U) (a : p.obj V ⟶ Y), CategoryStruct.comp a g = CategoryStruct.comp (p.map q) f) {A : Type u''} [Category.{v'', u''} A] [Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : Functor Cᵒᵖ A) : Limits.IsColimit (presheafFiberOfIsCofilteredCocone p hp P)

For a point constructed using Point.ofIsCofiltered and a functor p : N ⥤ C, the fiber of a presheaf can be computed as a colimit indexed by N.

Equations

• One or more equations did not get rendered due to their size.