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.

@[reducible, inline]

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

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

Equations

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

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

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.sheafToPresheaf J A).leftAdjoint)

theorem CategoryTheory.HasSheafify.isRightAdjoint {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} A} [self : CategoryTheory.HasSheafify J A], CategoryTheory.HasWeakSheafify J A

theorem CategoryTheory.HasSheafify.isLeftExact {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} A} [self : CategoryTheory.HasSheafify J A], Nonempty (CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.sheafToPresheaf J A).leftAdjoint)

instance CategoryTheory.instHasWeakSheafifyOfHasSheafify {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.instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf {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.sheafToPresheaf J A).leftAdjoint

Equations

• CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf J A = ⋯.some

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.sheafToPresheaf J A).leftAdjoint

instance CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf {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

• CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf J A = ⋯.some

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.Adjunction.ofIsRightAdjoint (CategoryTheory.sheafToPresheaf J A)

instance CategoryTheory.instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf {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).IsLeftAdjoint

Equations

• ⋯ = ⋯

instance CategoryTheory.instReflectiveFunctorOppositeSheafSheafToPresheafOfHasWeakSheafify {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.Reflective (CategoryTheory.sheafToPresheaf J A)

Equations

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

instance CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf {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.reflector (CategoryTheory.sheafToPresheaf J A))

Equations

• CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf J A = inferInstanceAs (CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.presheafToSheaf J A))

@[reducible, inline]

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

@[reducible, inline]

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

@[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

@[reducible, inline]

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

@[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 {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 η)

@[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)

@[reducible, inline]

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.presheafToSheaf J D).comp (CategoryTheory.sheafToPresheaf J D)

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 η

@[reducible, inline]

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

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)

@[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

@[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 {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) = η

@[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

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 {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.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

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 := ⋯ }

@[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

@[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

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

• ⋯ = ⋯

noncomputable def CategoryTheory.sheafificationNatIso {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.Sheaf J D) ≅ (CategoryTheory.sheafToPresheaf J D).comp (CategoryTheory.presheafToSheaf J D)

The natural isomorphism 𝟭 (Sheaf J D) ≅ sheafToPresheaf J D ⋙ presheafToSheaf J D.

Equations

• CategoryTheory.sheafificationNatIso J D = CategoryTheory.NatIso.ofComponents (fun (P : CategoryTheory.Sheaf J D) => CategoryTheory.sheafificationIso P) ⋯

@[simp]

theorem CategoryTheory.sheafificationNatIso_inv_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] (X : CategoryTheory.Sheaf J D) : ((CategoryTheory.sheafificationNatIso J D).inv.app X).val = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id X.val) ⋯

@[simp]

theorem CategoryTheory.sheafificationNatIso_hom_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] (X : CategoryTheory.Sheaf J D) : ((CategoryTheory.sheafificationNatIso J D).hom.app X).val = CategoryTheory.toSheafify J X.val