Documentation

Mathlib.CategoryTheory.Sites.Sheafification

Sheafification #

Given a site (C, J) we define a typeclass HasSheafify J A saying that the inclusion functor from A-valued sheaves on C to presheaves admits a left exact left adjoint (sheafification).

Note: to access the HasSheafify instance for suitable concrete categories, import the file Mathlib.CategoryTheory.Sites.LeftExact.

@[inline, reducible]

abbrev CategoryTheory.HasWeakSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] :

A proposition saying that the inclusion functor from sheaves to presheaves admits a left adjoint.

Equations

CategoryTheory.HasWeakSheafify J A = Nonempty (CategoryTheory.IsRightAdjoint (CategoryTheory.sheafToPresheaf J A))

Instances For

class CategoryTheory.HasSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] :

HasSheafify means that the inclusion functor from sheaves to presheaves admits a left exact left adjiont (sheafification).

Given a finite limit preserving functor F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A and an adjunction adj : F ⊣ sheafToPresheaf J A, use HasSheafify.mk' to construct a HasSheafify instance.

isRightAdjoint : CategoryTheory.HasWeakSheafify J A
isLeftExact : Nonempty (CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.leftAdjoint (CategoryTheory.sheafToPresheaf J A)))

Instances

instance CategoryTheory.instHasWeakSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasSheafify J A] :

CategoryTheory.HasWeakSheafify J A

Equations

⋯ = ⋯

instance CategoryTheory.instHasWeakSheafify_1 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.IsRightAdjoint (CategoryTheory.sheafToPresheaf J A)] :

CategoryTheory.HasWeakSheafify J A

Equations

⋯ = ⋯

instance CategoryTheory.instIsRightAdjointFunctorOppositeOppositeCategorySheafInstCategorySheafSheafToPresheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [h : CategoryTheory.HasWeakSheafify J A] :

CategoryTheory.IsRightAdjoint (CategoryTheory.sheafToPresheaf J A)

Equations

CategoryTheory.instIsRightAdjointFunctorOppositeOppositeCategorySheafInstCategorySheafSheafToPresheaf J A = Nonempty.some h

instance CategoryTheory.instPreservesFiniteLimitsFunctorOppositeOppositeCategorySheafInstCategorySheafLeftAdjointSheafToPresheafInstIsRightAdjointFunctorOppositeOppositeCategorySheafInstCategorySheafSheafToPresheafInstHasWeakSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasSheafify J A] :

CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.leftAdjoint (CategoryTheory.sheafToPresheaf J A))

Equations

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

theorem CategoryTheory.HasSheafify.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] {F : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj : F ⊣ CategoryTheory.sheafToPresheaf J A) [CategoryTheory.Limits.PreservesFiniteLimits F] :

CategoryTheory.HasSheafify J A

def CategoryTheory.presheafToSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasWeakSheafify J A] :

CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)

The sheafification functor, left adjoint to the inclusion.

Equations

CategoryTheory.presheafToSheaf J A = CategoryTheory.leftAdjoint (CategoryTheory.sheafToPresheaf J A)

Instances For

instance CategoryTheory.instPreservesFiniteLimitsFunctorOppositeOppositeCategorySheafInstCategorySheafPresheafToSheafInstHasWeakSheafify_1InstIsRightAdjointFunctorOppositeOppositeCategorySheafInstCategorySheafSheafToPresheafInstHasWeakSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasSheafify J A] :

CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.presheafToSheaf J A)

Equations

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

def CategoryTheory.sheafificationAdjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasWeakSheafify J A] :

CategoryTheory.presheafToSheaf J A ⊣ CategoryTheory.sheafToPresheaf J A

The sheafification-inclusion adjunction.

Equations

CategoryTheory.sheafificationAdjunction J A = CategoryTheory.IsRightAdjoint.adj

Instances For

instance CategoryTheory.instIsLeftAdjointFunctorOppositeOppositeCategorySheafInstCategorySheafPresheafToSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] [CategoryTheory.HasWeakSheafify J A] :

CategoryTheory.IsLeftAdjoint (CategoryTheory.presheafToSheaf J A)

Equations

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

@[inline, reducible]

noncomputable abbrev CategoryTheory.sheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) :

CategoryTheory.Functor Cᵒᵖ D

The sheafification of a presheaf P.

Equations

CategoryTheory.sheafify J P = ((CategoryTheory.presheafToSheaf J D).obj P).val

Instances For

@[inline, reducible]

noncomputable abbrev CategoryTheory.toSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) :

P ⟶ CategoryTheory.sheafify J P

The canonical map from P to its sheafification.

Equations

CategoryTheory.toSheafify J P = (CategoryTheory.sheafificationAdjunction J D).unit.app P

Instances For

@[simp]

theorem CategoryTheory.sheafificationAdjunction_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) :

(CategoryTheory.sheafificationAdjunction J D).unit.app P = CategoryTheory.toSheafify J P

@[inline, reducible]

noncomputable abbrev CategoryTheory.sheafifyMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) :

CategoryTheory.sheafify J P ⟶ CategoryTheory.sheafify J Q

The canonical map on sheafifications induced by a morphism.

Equations

CategoryTheory.sheafifyMap J η = ((CategoryTheory.presheafToSheaf J D).map η).val

Instances For

@[simp]

theorem CategoryTheory.sheafifyMap_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) :

CategoryTheory.sheafifyMap J (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (CategoryTheory.sheafify J P)

@[simp]

theorem CategoryTheory.sheafifyMap_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} {R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) :

CategoryTheory.sheafifyMap J (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) (CategoryTheory.sheafifyMap J γ)

@[simp]

theorem CategoryTheory.toSheafify_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : CategoryTheory.sheafify J Q ⟶ Z) :

CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J Q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) h)

@[simp]

theorem CategoryTheory.toSheafify_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) :

CategoryTheory.CategoryStruct.comp η (CategoryTheory.toSheafify J Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.sheafifyMap J η)

@[inline, reducible]

noncomputable abbrev CategoryTheory.sheafification {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] :

CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor Cᵒᵖ D)

The sheafification of a presheaf P, as a functor.

Equations

CategoryTheory.sheafification J D = CategoryTheory.Functor.comp (CategoryTheory.presheafToSheaf J D) (CategoryTheory.sheafToPresheaf J D)

Instances For

theorem CategoryTheory.sheafification_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) :

(CategoryTheory.sheafification J D).obj P = CategoryTheory.sheafify J P

theorem CategoryTheory.sheafification_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) :

(CategoryTheory.sheafification J D).map η = CategoryTheory.sheafifyMap J η

@[inline, reducible]

noncomputable abbrev CategoryTheory.toSheafification {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] :

CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ D) ⟶ CategoryTheory.sheafification J D

The canonical map from P to its sheafification, as a natural transformation.

Equations

CategoryTheory.toSheafification J D = (CategoryTheory.sheafificationAdjunction J D).unit

Instances For

theorem CategoryTheory.toSheafification_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) :

(CategoryTheory.toSheafification J D).app P = CategoryTheory.toSheafify J P

theorem CategoryTheory.isIso_toSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) :

CategoryTheory.IsIso (CategoryTheory.toSheafify J P)

noncomputable def CategoryTheory.isoSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) :

P ≅ CategoryTheory.sheafify J P

If P is a sheaf, then P is isomorphic to sheafify J P.

Equations

CategoryTheory.isoSheafify J hP = CategoryTheory.asIso (CategoryTheory.toSheafify J P)

Instances For

@[simp]

theorem CategoryTheory.isoSheafify_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) :

(CategoryTheory.isoSheafify J hP).hom = CategoryTheory.toSheafify J P

noncomputable def CategoryTheory.sheafifyLift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) :

CategoryTheory.sheafify J P ⟶ Q

Given a sheaf Q and a morphism P ⟶ Q, construct a morphism from sheafify J P to Q.

Equations

CategoryTheory.sheafifyLift J η hQ = (((CategoryTheory.sheafificationAdjunction J D).homEquiv P { val := Q, cond := hQ }).symm η).val

Instances For

@[simp]

theorem CategoryTheory.sheafificationAdjunction_counit_app_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) :

((CategoryTheory.sheafificationAdjunction J D).counit.app P).val = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P.val) ⋯

@[simp]

theorem CategoryTheory.toSheafify_sheafifyLift_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : Q ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J η hQ) h) = CategoryTheory.CategoryStruct.comp η h

@[simp]

theorem CategoryTheory.toSheafify_sheafifyLift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.sheafifyLift J η hQ) = η

theorem CategoryTheory.sheafifyLift_unique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (γ : CategoryTheory.sheafify J P ⟶ Q) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) γ = η → γ = CategoryTheory.sheafifyLift J η hQ

@[simp]

theorem CategoryTheory.isoSheafify_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) :

(CategoryTheory.isoSheafify J hP).inv = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P) hP

theorem CategoryTheory.sheafify_hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} (η : CategoryTheory.sheafify J P ⟶ Q) (γ : CategoryTheory.sheafify J P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) γ) :

η = γ

@[simp]

theorem CategoryTheory.sheafifyMap_sheafifyLift_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} {R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : R ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J γ hR) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.comp η γ) hR) h

@[simp]

theorem CategoryTheory.sheafifyMap_sheafifyLift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} {Q : CategoryTheory.Functor Cᵒᵖ D} {R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : CategoryTheory.Presheaf.IsSheaf J R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) (CategoryTheory.sheafifyLift J γ hR) = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.comp η γ) hR

@[simp]

theorem CategoryTheory.sheafificationIso_inv_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) :

(CategoryTheory.sheafificationIso P).inv.val = (CategoryTheory.isoSheafify J ⋯).inv

@[simp]

theorem CategoryTheory.sheafificationIso_hom_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) :

(CategoryTheory.sheafificationIso P).hom.val = (CategoryTheory.isoSheafify J ⋯).hom

noncomputable def CategoryTheory.sheafificationIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) :

P ≅ (CategoryTheory.presheafToSheaf J D).obj P.val

A sheaf P is isomorphic to its own sheafification.

Equations

CategoryTheory.sheafificationIso P = { hom := { val := (CategoryTheory.isoSheafify J ⋯).hom }, inv := { val := (CategoryTheory.isoSheafify J ⋯).inv }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

instance CategoryTheory.isIso_sheafificationAdjunction_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) :

CategoryTheory.IsIso ((CategoryTheory.sheafificationAdjunction J D).counit.app P)

Equations

⋯ = ⋯

instance CategoryTheory.sheafification_reflective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.HasWeakSheafify J D] :

CategoryTheory.IsIso (CategoryTheory.sheafificationAdjunction J D).counit

Equations

⋯ = ⋯