category_theory.sites.plus

@[simp]

theorem category_theory.grothendieck_topology.diagram_map {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) (X : C) (S T : (J.cover X)ᵒᵖ) (f : S ⟶ T) :

(J.diagram P X).map f = category_theory.limits.multiequalizer.lift ((opposite.unop T).index P) (category_theory.limits.multiequalizer ((opposite.unop S).index P)) (λ (I : ((opposite.unop T).index P).L), category_theory.limits.multiequalizer.ι ((opposite.unop S).index P) (category_theory.grothendieck_topology.cover.arrow.map I f.unop)) _

source

noncomputable def category_theory.grothendieck_topology.diagram {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) (X : C) :

(J.cover X)ᵒᵖ ⥤ D

The diagram whose colimit defines the values of plus.

Equations

J.diagram P X = {obj := λ (S : (J.cover X)ᵒᵖ), category_theory.limits.multiequalizer ((opposite.unop S).index P), map := λ (S T : (J.cover X)ᵒᵖ) (f : S ⟶ T), category_theory.limits.multiequalizer.lift ((opposite.unop T).index P) (category_theory.limits.multiequalizer ((opposite.unop S).index P)) (λ (I : ((opposite.unop T).index P).L), category_theory.limits.multiequalizer.ι ((opposite.unop S).index P) (category_theory.grothendieck_topology.cover.arrow.map I f.unop)) _, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.grothendieck_topology.diagram_obj {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) (X : C) (S : (J.cover X)ᵒᵖ) :

(J.diagram P X).obj S = category_theory.limits.multiequalizer ((opposite.unop S).index P)

source

noncomputable def category_theory.grothendieck_topology.diagram_pullback {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) {X Y : C} (f : X ⟶ Y) :

J.diagram P Y ⟶ (J.pullback f).op ⋙ J.diagram P X

A helper definition used to define the morphisms for plus.

Equations

J.diagram_pullback P f = {app := λ (S : (J.cover Y)ᵒᵖ), category_theory.limits.multiequalizer.lift ((opposite.unop ((J.pullback f).op.obj S)).index P) ((J.diagram P Y).obj S) (λ (I : ((opposite.unop ((J.pullback f).op.obj S)).index P).L), category_theory.limits.multiequalizer.ι ((opposite.unop S).index P) (category_theory.grothendieck_topology.cover.arrow.base I)) _, naturality' := _}

source

@[simp]

theorem category_theory.grothendieck_topology.diagram_pullback_app {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) {X Y : C} (f : X ⟶ Y) (S : (J.cover Y)ᵒᵖ) :

(J.diagram_pullback P f).app S = category_theory.limits.multiequalizer.lift ((opposite.unop ((J.pullback f).op.obj S)).index P) ((J.diagram P Y).obj S) (λ (I : ((opposite.unop ((J.pullback f).op.obj S)).index P).L), category_theory.limits.multiequalizer.ι ((opposite.unop S).index P) (category_theory.grothendieck_topology.cover.arrow.base I)) _

source

@[simp]

theorem category_theory.grothendieck_topology.diagram_nat_trans_app {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (X : C) (W : (J.cover X)ᵒᵖ) :

(J.diagram_nat_trans η X).app W = category_theory.limits.multiequalizer.lift ((opposite.unop W).index Q) ((J.diagram P X).obj W) (λ (i : ((opposite.unop W).index Q).L), category_theory.limits.multiequalizer.ι ((opposite.unop W).index P) i ≫ η.app (opposite.op i.Y)) _

source

noncomputable def category_theory.grothendieck_topology.diagram_nat_trans {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (X : C) :

J.diagram P X ⟶ J.diagram Q X

A natural transformation P ⟶ Q induces a natural transformation between diagrams whose colimits define the values of plus.

Equations

J.diagram_nat_trans η X = {app := λ (W : (J.cover X)ᵒᵖ), category_theory.limits.multiequalizer.lift ((opposite.unop W).index Q) ((J.diagram P X).obj W) (λ (i : ((opposite.unop W).index Q).L), category_theory.limits.multiequalizer.ι ((opposite.unop W).index P) i ≫ η.app (opposite.op i.Y)) _, naturality' := _}

source

@[simp]

theorem category_theory.grothendieck_topology.diagram_nat_trans_id {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) (P : Cᵒᵖ ⥤ D) :

J.diagram_nat_trans (𝟙 P) X = 𝟙 (J.diagram P X)

source

@[simp]

theorem category_theory.grothendieck_topology.diagram_nat_trans_zero {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [category_theory.preadditive D] (X : C) (P Q : Cᵒᵖ ⥤ D) :

J.diagram_nat_trans 0 X = 0

source

@[simp]

theorem category_theory.grothendieck_topology.diagram_nat_trans_comp {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) (X : C) :

J.diagram_nat_trans (η ≫ γ) X = J.diagram_nat_trans η X ≫ J.diagram_nat_trans γ X

source

@[simp]

theorem category_theory.grothendieck_topology.diagram_functor_map {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) (P Q : Cᵒᵖ ⥤ D) (η : P ⟶ Q) :

(J.diagram_functor D X).map η = J.diagram_nat_trans η X

source

@[simp]

theorem category_theory.grothendieck_topology.diagram_functor_obj {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) (P : Cᵒᵖ ⥤ D) :

(J.diagram_functor D X).obj P = J.diagram P X

source

noncomputable def category_theory.grothendieck_topology.diagram_functor {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (X : C) :

(Cᵒᵖ ⥤ D) ⥤ (J.cover X)ᵒᵖ ⥤ D

J.diagram P, as a functor in P.

Equations

J.diagram_functor D X = {obj := λ (P : Cᵒᵖ ⥤ D), J.diagram P X, map := λ (P Q : Cᵒᵖ ⥤ D) (η : P ⟶ Q), J.diagram_nat_trans η X, map_id' := _, map_comp' := _}

Instances for category_theory.grothendieck_topology.diagram_functor

source

noncomputable def category_theory.grothendieck_topology.plus_obj {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :

Cᵒᵖ ⥤ D

The plus construction, associating a presheaf to any presheaf. See plus_functor below for a functorial version.

Equations

J.plus_obj P = {obj := λ (X : Cᵒᵖ), category_theory.limits.colimit (J.diagram P (opposite.unop X)), map := λ (X Y : Cᵒᵖ) (f : X ⟶ Y), category_theory.limits.colim_map (J.diagram_pullback P f.unop) ≫ category_theory.limits.colimit.pre (J.diagram P (opposite.unop Y)) (J.pullback f.unop).op, map_id' := _, map_comp' := _}

source

noncomputable def category_theory.grothendieck_topology.plus_map {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :

J.plus_obj P ⟶ J.plus_obj Q

An auxiliary definition used in plus below.

Equations

J.plus_map η = {app := λ (X : Cᵒᵖ), category_theory.limits.colim_map (J.diagram_nat_trans η (opposite.unop X)), naturality' := _}

source

@[simp]

theorem category_theory.grothendieck_topology.plus_map_id {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (P : Cᵒᵖ ⥤ D) :

J.plus_map (𝟙 P) = 𝟙 (J.plus_obj P)

source

@[simp]

theorem category_theory.grothendieck_topology.plus_map_zero {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.preadditive D] (P Q : Cᵒᵖ ⥤ D) :

J.plus_map 0 = 0

source

@[simp]

theorem category_theory.grothendieck_topology.plus_map_comp {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) :

J.plus_map (η ≫ γ) = J.plus_map η ≫ J.plus_map γ

source

@[simp]

theorem category_theory.grothendieck_topology.plus_functor_obj {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (P : Cᵒᵖ ⥤ D) :

(J.plus_functor D).obj P = J.plus_obj P

source

noncomputable def category_theory.grothendieck_topology.plus_functor {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :

(Cᵒᵖ ⥤ D) ⥤ Cᵒᵖ ⥤ D

The plus construction, a functor sending P to J.plus_obj P.

Equations

J.plus_functor D = {obj := λ (P : Cᵒᵖ ⥤ D), J.plus_obj P, map := λ (P Q : Cᵒᵖ ⥤ D) (η : P ⟶ Q), J.plus_map η, map_id' := _, map_comp' := _}

Instances for category_theory.grothendieck_topology.plus_functor

source

@[simp]

theorem category_theory.grothendieck_topology.plus_functor_map {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (P Q : Cᵒᵖ ⥤ D) (η : P ⟶ Q) :

(J.plus_functor D).map η = J.plus_map η

source

noncomputable def category_theory.grothendieck_topology.to_plus {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :

P ⟶ J.plus_obj P

The canonical map from P to J.plus.obj P. See to_plus for a functorial version.

Equations

J.to_plus P = {app := λ (X : Cᵒᵖ), ⊤.to_multiequalizer P ≫ category_theory.limits.colimit.ι (J.diagram P (opposite.unop X)) (opposite.op ⊤), naturality' := _}

source

@[simp]

theorem category_theory.grothendieck_topology.to_plus_naturality {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :

η ≫ J.to_plus Q = J.to_plus P ≫ J.plus_map η

source

@[simp]

theorem category_theory.grothendieck_topology.to_plus_naturality_assoc {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) {X' : Cᵒᵖ ⥤ D} (f' : J.plus_obj Q ⟶ X') :

η ≫ J.to_plus Q ≫ f' = J.to_plus P ≫ J.plus_map η ≫ f'

source

@[simp]

theorem category_theory.grothendieck_topology.to_plus_nat_trans_app {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (P : Cᵒᵖ ⥤ D) :

(J.to_plus_nat_trans D).app P = J.to_plus P

source

noncomputable def category_theory.grothendieck_topology.to_plus_nat_trans {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (D : Type w) [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :

𝟭 (Cᵒᵖ ⥤ D) ⟶ J.plus_functor D

The natural transformation from the identity functor to plus.

Equations

J.to_plus_nat_trans D = {app := λ (P : Cᵒᵖ ⥤ D), J.to_plus P, naturality' := _}

source

@[simp]

theorem category_theory.grothendieck_topology.plus_map_to_plus {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] :

J.plus_map (J.to_plus P) = J.to_plus (J.plus_obj P)

(P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺

source

theorem category_theory.grothendieck_topology.is_iso_to_plus_of_is_sheaf {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (hP : category_theory.presheaf.is_sheaf J P) :

category_theory.is_iso (J.to_plus P)

source

noncomputable def category_theory.grothendieck_topology.iso_to_plus {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (hP : category_theory.presheaf.is_sheaf J P) :

P ≅ J.plus_obj P

The natural isomorphism between P and P⁺ when P is a sheaf.

Equations

J.iso_to_plus P hP = let _inst : category_theory.is_iso (J.to_plus P) := _ in category_theory.as_iso (J.to_plus P)

source

@[simp]

theorem category_theory.grothendieck_topology.iso_to_plus_hom {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (hP : category_theory.presheaf.is_sheaf J P) :

(J.iso_to_plus P hP).hom = J.to_plus P

source

noncomputable def category_theory.grothendieck_topology.plus_lift {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) :

J.plus_obj P ⟶ Q

Lift a morphism P ⟶ Q to P⁺ ⟶ Q when Q is a sheaf.

Equations

J.plus_lift η hQ = J.plus_map η ≫ (J.iso_to_plus Q hQ).inv

source

@[simp]

theorem category_theory.grothendieck_topology.to_plus_plus_lift_assoc {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) {X' : Cᵒᵖ ⥤ D} (f' : Q ⟶ X') :

J.to_plus P ≫ J.plus_lift η hQ ≫ f' = η ≫ f'

source

@[simp]

theorem category_theory.grothendieck_topology.to_plus_plus_lift {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) :

J.to_plus P ≫ J.plus_lift η hQ = η

source

theorem category_theory.grothendieck_topology.plus_lift_unique {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) (γ : J.plus_obj P ⟶ Q) (hγ : J.to_plus P ≫ γ = η) :

γ = J.plus_lift η hQ

source

theorem category_theory.grothendieck_topology.plus_hom_ext {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q : Cᵒᵖ ⥤ D} (η γ : J.plus_obj P ⟶ Q) (hQ : category_theory.presheaf.is_sheaf J Q) (h : J.to_plus P ≫ η = J.to_plus P ≫ γ) :

η = γ

source

@[simp]

theorem category_theory.grothendieck_topology.iso_to_plus_inv {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] (P : Cᵒᵖ ⥤ D) [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] (hP : category_theory.presheaf.is_sheaf J P) :

(J.iso_to_plus P hP).inv = J.plus_lift (𝟙 P) hP

source

@[simp]

theorem category_theory.grothendieck_topology.plus_map_plus_lift {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) (hR : category_theory.presheaf.is_sheaf J R) :

J.plus_map η ≫ J.plus_lift γ hR = J.plus_lift (η ≫ γ) hR

source

@[protected, instance]

def category_theory.grothendieck_topology.plus_functor_preserves_zero_morphisms {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) {D : Type w} [category_theory.category D] [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)] [∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D] [category_theory.preadditive D] :

(J.plus_functor D).preserves_zero_morphisms

mathlib3 documentation

The plus construction for presheaves. #