Skyscraper sheaves #

Let Φ be a point of a site (C, J). In this file, we construct the skyscraper sheaf functor skyscraperSheafFunctor : A ⥤ Sheaf J A and show that it is a right adjoint to Φ.sheafFiber : Sheaf J A ⥤ A.

source

noncomputable def CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] :

Functor A (Functor Cᵒᵖ A)

Given a point Φ on a site (C, J), this is the skyscraper presheaf functor A ⥤ Cᵒᵖ ⥤ A.

Equations

Φ.skyscraperPresheafFunctor = (Φ.fiber.op.comp CategoryTheory.Limits.piConst.flip).flip

Instances For

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_map_app {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) (j : Cᵒᵖ) :

(Φ.skyscraperPresheafFunctor.map f).app j = Limits.Pi.map fun (x : Φ.fiber.obj (Opposite.unop j)) => f

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_obj_obj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] (k : A) (j : Cᵒᵖ) :

(Φ.skyscraperPresheafFunctor.obj k).obj j = ∏ᶜ fun (x : Φ.fiber.obj (Opposite.unop j)) => k

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafFunctor_obj_map {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] (k : A) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) :

(Φ.skyscraperPresheafFunctor.obj k).map f = Limits.Pi.map' ⇑(ConcreteCategory.hom (Φ.fiber.map f.unop)) fun (x : Φ.fiber.obj (Opposite.unop Y✝)) => CategoryStruct.id k

source

@[reducible, inline]

noncomputable abbrev CategoryTheory.GrothendieckTopology.Point.skyscraperPresheaf {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] (M : A) :

Functor Cᵒᵖ A

Given a point Φ on a site (C, J), and an object M of a category A, this is the skyscraper presheaf with value M: it sends X : C to the product of copies of M indexed by Φ.fiber.obj X.

Equations

Φ.skyscraperPresheaf M = Φ.skyscraperPresheafFunctor.obj M

Instances For

source

noncomputable def CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] :

(Φ.presheafFiber.obj P ⟶ M) ≃ (P ⟶ Φ.skyscraperPresheaf M)

If Φ is a point of a site (C, J), P : Cᵒᵖ ⥤ A and M : A, this is the bijection (Φ.presheafFiber.obj P ⟶ M) ≃ (P ⟶ Φ.skyscraperPresheaf M) that is part of the adjunction skyscraperPresheafAdjunction.

Equations

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

Instances For

source

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_symm_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (g : P ⟶ Φ.skyscraperPresheaf M) :

Φ.skyscraperPresheafHomEquiv.symm g = Φ.presheafFiberDesc (fun (X : C) (x : Φ.fiber.obj X) => CategoryStruct.comp (g.app (Opposite.op X)) (Limits.Pi.π (fun (x : Opposite.unop (Φ.fiber.op.obj (Opposite.op X))) => M) x)) ⋯

source

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_apply_app {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (X : Cᵒᵖ) :

(Φ.skyscraperPresheafHomEquiv f).app X = Limits.Pi.lift fun (x : Opposite.unop (Φ.fiber.op.obj X)) => CategoryStruct.comp (Φ.toPresheafFiber (Opposite.unop X) x P) f

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_skyscraperPresheafHomEquiv_symm {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (g : P ⟶ Φ.skyscraperPresheaf M) (X : C) (x : Φ.fiber.obj X) :

CategoryStruct.comp (Φ.toPresheafFiber X x P) (Φ.skyscraperPresheafHomEquiv.symm g) = CategoryStruct.comp (g.app (Opposite.op X)) (Limits.Pi.π (fun (x : Opposite.unop (Φ.fiber.op.obj (Opposite.op X))) => M) x)

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_skyscraperPresheafHomEquiv_symm_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (g : P ⟶ Φ.skyscraperPresheaf M) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : M ⟶ Z) :

CategoryStruct.comp (Φ.toPresheafFiber X x P) (CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv.symm g) h) = CategoryStruct.comp (g.app (Opposite.op X)) (CategoryStruct.comp (Limits.Pi.π (fun (x : Opposite.unop (Φ.fiber.op.obj (Opposite.op X))) => M) x) h)

source

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_symm {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P Q : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : P ⟶ Q) (g : Q ⟶ Φ.skyscraperPresheaf M) :

Φ.skyscraperPresheafHomEquiv.symm (CategoryStruct.comp f g) = CategoryStruct.comp (Φ.presheafFiber.map f) (Φ.skyscraperPresheafHomEquiv.symm g)

source

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_symm_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P Q : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : P ⟶ Q) (g : Q ⟶ Φ.skyscraperPresheaf M) {Z : A} (h : M ⟶ Z) :

CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv.symm (CategoryStruct.comp f g)) h = CategoryStruct.comp (Φ.presheafFiber.map f) (CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv.symm g) h)

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_app_π {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (X : C) (x : Φ.fiber.obj X) :

CategoryStruct.comp ((Φ.skyscraperPresheafHomEquiv f).app (Opposite.op X)) (Limits.Pi.π (fun (x : Φ.fiber.obj X) => M) x) = CategoryStruct.comp (Φ.toPresheafFiber X x P) f

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_app_π_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (X : C) (x : Φ.fiber.obj X) {Z : A} (h : M ⟶ Z) :

CategoryStruct.comp ((Φ.skyscraperPresheafHomEquiv f).app (Opposite.op X)) (CategoryStruct.comp (Limits.Pi.π (fun (x : Φ.fiber.obj X) => M) x) h) = CategoryStruct.comp (Φ.toPresheafFiber X x P) (CategoryStruct.comp f h)

source

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_right {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P : Functor Cᵒᵖ A} {M N : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (g : M ⟶ N) :

Φ.skyscraperPresheafHomEquiv (CategoryStruct.comp f g) = CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv f) (Φ.skyscraperPresheafFunctor.map g)

source

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_right_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P : Functor Cᵒᵖ A} {M N : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : Φ.presheafFiber.obj P ⟶ M) (g : M ⟶ N) {Z : Functor Cᵒᵖ A} (h : Φ.skyscraperPresheaf N ⟶ Z) :

CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv (CategoryStruct.comp f g)) h = CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv f) (CategoryStruct.comp (Φ.skyscraperPresheafFunctor.map g) h)

source

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P Q : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : P ⟶ Q) (g : Φ.presheafFiber.obj Q ⟶ M) :

Φ.skyscraperPresheafHomEquiv (CategoryStruct.comp (Φ.presheafFiber.map f) g) = CategoryStruct.comp f (Φ.skyscraperPresheafHomEquiv g)

source

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {P Q : Functor Cᵒᵖ A} {M : A} [Limits.HasColimitsOfSize.{w, w, v', u'} A] (f : P ⟶ Q) (g : Φ.presheafFiber.obj Q ⟶ M) {Z : Functor Cᵒᵖ A} (h : Φ.skyscraperPresheaf M ⟶ Z) :

CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv (CategoryStruct.comp (Φ.presheafFiber.map f) g)) h = CategoryStruct.comp f (CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv g) h)

source

noncomputable def CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] :

Φ.presheafFiber ⊣ Φ.skyscraperPresheafFunctor

Given a point of a site, the skyscraper presheaf functor is right adjoint to the fiber functor on presheaves.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction_homEquiv_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : Functor Cᵒᵖ A} {M : A} (f : Φ.presheafFiber.obj P ⟶ M) :

(Φ.skyscraperPresheafAdjunction.homEquiv P M) f = Φ.skyscraperPresheafHomEquiv f

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction_homEquiv_symm_apply {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : Functor Cᵒᵖ A} {M : A} (f : P ⟶ Φ.skyscraperPresheaf M) :

(Φ.skyscraperPresheafAdjunction.homEquiv P M).symm f = Φ.skyscraperPresheafHomEquiv.symm f

source

theorem CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheaf {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] (M : A) :

Presheaf.IsSheaf J (Φ.skyscraperPresheaf M)

source

noncomputable def CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] :

Functor A (Sheaf J A)

Given a point Φ of a site (C, J), this is the skyscraper sheaf functor A ⥤ Sheaf J A.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_obj_obj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] (M : A) :

(Φ.skyscraperSheafFunctor.obj M).obj = Φ.skyscraperPresheaf M

source

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_map_hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] {X✝ Y✝ : A} (f : X✝ ⟶ Y✝) :

(Φ.skyscraperSheafFunctor.map f).hom = Φ.skyscraperPresheafFunctor.map f

source

@[reducible, inline]

noncomputable abbrev CategoryTheory.GrothendieckTopology.Point.skyscraperSheaf {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] (M : A) :

Sheaf J A

Given a point Φ on a site (C, J), and an object M of a category A, this is the skyscraper sheaf with value M: it sends X : C to the product of copies of M indexed by Φ.fiber.obj X.

Equations