Loogle!

Result

Found 423 declarations mentioning CategoryTheory.HasWeakSheafify. Of these, only the first 200 are shown.

• CategoryTheory.HasWeakSheafify 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] : Prop
• CategoryTheory.instHasWeakSheafifyOfHasSheafify 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {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
• CategoryTheory.HasSheafify.isRightAdjoint 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} A} [self : CategoryTheory.HasSheafify J A] : CategoryTheory.HasWeakSheafify J A
• CategoryTheory.sheafify 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Functor Cᵒᵖ D
• CategoryTheory.sheafification 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor Cᵒᵖ D)
• CategoryTheory.isoSheafify 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : P ≅ CategoryTheory.sheafify J P
• CategoryTheory.presheafToSheaf 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {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)
• CategoryTheory.isIso_toSheafify 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.IsIso (CategoryTheory.toSheafify J P)
• CategoryTheory.instReflectiveFunctorOppositeSheafSheafToPresheafOfHasWeakSheafify 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {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)
• CategoryTheory.toSheafify 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) : P ⟶ CategoryTheory.sheafify J P
• CategoryTheory.instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {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
• CategoryTheory.sheafificationAdjunction 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {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
• CategoryTheory.sheafification_obj 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.sheafification J D).obj P = CategoryTheory.sheafify J P
• CategoryTheory.isoSheafify_hom 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, 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
• CategoryTheory.sheafifyLift 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.sheafify J P ⟶ Q
• CategoryTheory.sheafifyMap 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : CategoryTheory.sheafify J P ⟶ CategoryTheory.sheafify J Q
• CategoryTheory.HasSheafify.mk 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (isRightAdjoint : CategoryTheory.HasWeakSheafify J A) (isLeftExact : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.sheafToPresheaf J A).leftAdjoint) : CategoryTheory.HasSheafify J A
• CategoryTheory.sheafificationIso 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) : P ≅ (CategoryTheory.presheafToSheaf J D).obj P.obj
• CategoryTheory.sheafifyMap_id 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, 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)
• CategoryTheory.isoSheafify_inv 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, 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
• CategoryTheory.toSheafify_sheafifyLift 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.sheafifyLift J η hQ) = η
• CategoryTheory.toSheafification 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] : CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ D) ⟶ CategoryTheory.sheafification J D
• CategoryTheory.sheafifyLift_id_toSheafify 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P) hP) (CategoryTheory.toSheafify J P) = CategoryTheory.CategoryStruct.id (CategoryTheory.sheafify J P)
• CategoryTheory.toSheafify_naturality 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.toSheafify J Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.sheafifyMap J η)
• CategoryTheory.toSheafification_app 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.toSheafification J D).app P = CategoryTheory.toSheafify J P
• CategoryTheory.instMonoFunctorOppositeHomFullSubcategoryIsSheafOfHasWeakSheafifyOfSheaf 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂) [CategoryTheory.Category.{v₂, u₂} A] {F G : CategoryTheory.Sheaf J A} [CategoryTheory.HasWeakSheafify J A] (f : F ⟶ G) [CategoryTheory.Mono f] : CategoryTheory.Mono f.hom
• CategoryTheory.sheafification_map 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) : (CategoryTheory.sheafification J D).map η = CategoryTheory.sheafifyMap J η
• CategoryTheory.sheafifyLift_id_toSheafify_assoc 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : CategoryTheory.sheafify J P ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P) hP) (CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) h) = h
• CategoryTheory.sheafificationNatIso 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] : CategoryTheory.Functor.id (CategoryTheory.Sheaf J D) ≅ (CategoryTheory.sheafToPresheaf J D).comp (CategoryTheory.presheafToSheaf J D)
• CategoryTheory.sheafifyLift_unique 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P 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
• CategoryTheory.sheafifyLift_comp 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {F P Q : CategoryTheory.Functor Cᵒᵖ D} (a : F ⟶ P) (hP : CategoryTheory.Presheaf.IsSheaf J P) (η : P ⟶ Q) (hQ : CategoryTheory.Presheaf.IsSheaf J Q) : CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.comp a η) hQ = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyLift J a hP) η
• CategoryTheory.sheafifyMap_sheafifyLift 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q 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
• CategoryTheory.sheafifyMap_comp 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q R : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q) (γ : Q ⟶ R) : CategoryTheory.sheafifyMap J (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) (CategoryTheory.sheafifyMap J γ)
• CategoryTheory.toSheafify_sheafifyLift_assoc 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P 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
• CategoryTheory.sheafify_hom_ext 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q : CategoryTheory.Functor Cᵒᵖ D} (η γ : 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) γ) : η = γ
• CategoryTheory.sheafification_reflective 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] : CategoryTheory.IsIso (CategoryTheory.sheafificationAdjunction J D).counit
• CategoryTheory.toSheafify_naturality_assoc 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P 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)
• CategoryTheory.sheafifyMap_sheafifyLift_assoc 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] {P Q 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
• CategoryTheory.sheafificationAdjunction_unit_app 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.sheafificationAdjunction J D).unit.app P = CategoryTheory.toSheafify J P
• CategoryTheory.sheafificationIso_hom_hom 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) : (CategoryTheory.sheafificationIso P).hom.hom = (CategoryTheory.isoSheafify J ⋯).hom
• CategoryTheory.sheafificationIso_inv_hom 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) : (CategoryTheory.sheafificationIso P).inv.hom = (CategoryTheory.isoSheafify J ⋯).inv
• CategoryTheory.isIso_sheafificationAdjunction_counit 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) : CategoryTheory.IsIso ((CategoryTheory.sheafificationAdjunction J D).counit.app P)
• CategoryTheory.sheafificationNatIso_hom_app_hom 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (X : CategoryTheory.Sheaf J D) : ((CategoryTheory.sheafificationNatIso J D).hom.app X).hom = CategoryTheory.toSheafify J X.obj
• CategoryTheory.instIsIsoFunctorOppositeHomFullSubcategoryIsSheafAppSheafCounitSheafificationAdjunction 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) : CategoryTheory.IsIso ((CategoryTheory.sheafificationAdjunction J D).counit.app P).hom
• CategoryTheory.sheafificationNatIso_inv_app_hom 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (X : CategoryTheory.Sheaf J D) : ((CategoryTheory.sheafificationNatIso J D).inv.app X).hom = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id X.obj) ⋯
• CategoryTheory.sheafificationAdjunction_counit_app_val 📋 Mathlib.CategoryTheory.Sites.Sheafification
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.HasWeakSheafify J D] (P : CategoryTheory.Sheaf J D) : ((CategoryTheory.sheafificationAdjunction J D).counit.app P).hom = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P.obj) ⋯
• CategoryTheory.Sheaf.instHasColimitsOfSize 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.Limits.HasColimitsOfSize.{u₁, u₂, w', w} D] : CategoryTheory.Limits.HasColimitsOfSize.{u₁, u₂, max u w', max (max (max w u) w') v} (CategoryTheory.Sheaf J D)
• CategoryTheory.Sheaf.instHasFiniteColimits 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.Limits.HasFiniteColimits D] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Sheaf J D)
• CategoryTheory.Sheaf.instHasFiniteCoproducts 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.Limits.HasFiniteCoproducts D] : CategoryTheory.Limits.HasFiniteCoproducts (CategoryTheory.Sheaf J D)
• CategoryTheory.Sheaf.instHasColimitsOfShape 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.Limits.HasColimitsOfShape K D] : CategoryTheory.Limits.HasColimitsOfShape K (CategoryTheory.Sheaf J D)
• CategoryTheory.Sheaf.sheafifyCocone 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D))) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Sheaf.isColimitSheafifyCocone 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D))) (hE : CategoryTheory.Limits.IsColimit E) : CategoryTheory.Limits.IsColimit (CategoryTheory.Sheaf.sheafifyCocone E)
• CategoryTheory.Sheaf.sheafifyCocone_ι_app_val 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D))) (k : K) : ((CategoryTheory.Sheaf.sheafifyCocone E).ι.app k).hom = CategoryTheory.CategoryStruct.comp (E.ι.app k) (CategoryTheory.toSheafify J E.pt)
• CategoryTheory.Sheaf.sheafifyCocone_ι_app_val_assoc 📋 Mathlib.CategoryTheory.Sites.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] [CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)} (E : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D))) (k : K) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : (((CategoryTheory.Functor.const K).obj (CategoryTheory.Sheaf.sheafifyCocone E).pt).obj k).obj ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Sheaf.sheafifyCocone E).ι.app k).hom h = CategoryTheory.CategoryStruct.comp (E.ι.app k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J E.pt) h)
• CategoryTheory.GrothendieckTopology.W_toSheafify 📋 Mathlib.CategoryTheory.Sites.Localization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.HasWeakSheafify J A] (P : CategoryTheory.Functor Cᵒᵖ A) : J.W (CategoryTheory.toSheafify J P)
• CategoryTheory.GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW 📋 Mathlib.CategoryTheory.Sites.Localization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.presheafToSheaf J A).IsLocalization J.W
• CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms 📋 Mathlib.CategoryTheory.Sites.Localization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.HasWeakSheafify J A] : J.W = (CategoryTheory.MorphismProperty.isomorphisms (CategoryTheory.Sheaf J A)).inverseImage (CategoryTheory.presheafToSheaf J A)
• CategoryTheory.GrothendieckTopology.W_iff 📋 Mathlib.CategoryTheory.Sites.Localization
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_2} [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.HasWeakSheafify J A] {P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A} (f : P₁ ⟶ P₂) : J.W f ↔ CategoryTheory.IsIso ((CategoryTheory.presheafToSheaf J A).map f)
• CategoryTheory.Sheaf.composeAndSheafify 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf J B)
• CategoryTheory.sheafifyComposeIso 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.sheafify J (P.comp F) ≅ (CategoryTheory.sheafify J P).comp F
• CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [J.PreservesSheafification F] [CategoryTheory.HasWeakSheafify J B] : J.W.IsInvertedBy (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B))
• CategoryTheory.instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] : CategoryTheory.Localization.Lifting (CategoryTheory.presheafToSheaf J A) J.W (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B)) (CategoryTheory.Sheaf.composeAndSheafify J F)
• CategoryTheory.sheafComposeIso_hom_fac 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) (CategoryTheory.sheafifyComposeIso J F P).hom = CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F
• CategoryTheory.sheafComposeIso_inv_fac 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F) (CategoryTheory.sheafifyComposeIso J F P).inv = CategoryTheory.toSheafify J (P.comp F)
• CategoryTheory.presheafToSheafCompComposeAndSheafifyIso 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] : (CategoryTheory.presheafToSheaf J A).comp (CategoryTheory.Sheaf.composeAndSheafify J F) ≅ ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B)
• CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] : CategoryTheory.IsIso (CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F)
• CategoryTheory.toPresheafToSheafCompComposeAndSheafify 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] : ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B) ⟶ (CategoryTheory.presheafToSheaf J A).comp (CategoryTheory.Sheaf.composeAndSheafify J F)
• CategoryTheory.sheafComposeIso_hom_fac_assoc 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) {Z : CategoryTheory.Functor Cᵒᵖ B} (h : (CategoryTheory.sheafify J P).comp F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J F P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F) h
• CategoryTheory.sheafComposeIso_inv_fac_assoc 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) {Z : CategoryTheory.Functor Cᵒᵖ B} (h : CategoryTheory.sheafify J (P.comp F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J F P).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) h
• CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] (X : CategoryTheory.Functor Cᵒᵖ A) : (CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F).app X = (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J X) F)
• CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app 📋 Mathlib.CategoryTheory.Sites.PreservesSheafification
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] (X : CategoryTheory.Functor Cᵒᵖ A) : (CategoryTheory.presheafToSheafCompComposeAndSheafifyIso J F).inv.app X = (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J X) F)
• CategoryTheory.Presheaf.isLocallyInjective_toSheafify' 📋 Mathlib.CategoryTheory.Sites.LocallyInjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {FD : D → D → Type u_1} (J : CategoryTheory.GrothendieckTopology C) {CD : D → Type (max u v)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] (P : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)] : CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)
• CategoryTheory.Presheaf.isLocallySurjective_toSheafify' 📋 Mathlib.CategoryTheory.Sites.LocallySurjective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_2} [CategoryTheory.Category.{v_1, u_2} D] {FD : D → D → Type u_3} {CD : D → Type (max u v)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] (P : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)] : CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)
• CategoryTheory.GrothendieckTopology.instIsLocallyInjectiveToSheafify 📋 Mathlib.CategoryTheory.Sites.LocallyBijective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [J.WEqualsLocallyBijective A] [CategoryTheory.HasWeakSheafify J A] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)
• CategoryTheory.GrothendieckTopology.instIsLocallySurjectiveToSheafify 📋 Mathlib.CategoryTheory.Sites.LocallyBijective
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [J.WEqualsLocallyBijective A] [CategoryTheory.HasWeakSheafify J A] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)
• CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget 📋 Mathlib.CategoryTheory.Sites.LocallyBijective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_2} {CD : D → Type (max u v)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [CategoryTheory.ConcreteCategory D FD] [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : J.WEqualsLocallyBijective D
• CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.mk' 📋 Mathlib.CategoryTheory.Sites.LocallyBijective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [J.HasSheafCompose (CategoryTheory.forget A)] [∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)] [∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)] : J.WEqualsLocallyBijective A
• CategoryTheory.Presheaf.isLocallyInjective_presheafToSheaf_map_iff 📋 Mathlib.CategoryTheory.Sites.LocallyBijective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.HasWeakSheafify J A] [J.WEqualsLocallyBijective A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (φ : P ⟶ Q) : CategoryTheory.Sheaf.IsLocallyInjective ((CategoryTheory.presheafToSheaf J A).map φ) ↔ CategoryTheory.Presheaf.IsLocallyInjective J φ
• CategoryTheory.Presheaf.isLocallySurjective_presheafToSheaf_map_iff 📋 Mathlib.CategoryTheory.Sites.LocallyBijective
  {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.HasWeakSheafify J A] [J.WEqualsLocallyBijective A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (φ : P ⟶ Q) : CategoryTheory.Sheaf.IsLocallySurjective ((CategoryTheory.presheafToSheaf J A).map φ) ↔ CategoryTheory.Presheaf.IsLocallySurjective J φ
• PresheafOfModules.sheafification 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : CategoryTheory.Functor (PresheafOfModules R₀) (SheafOfModules R)
• PresheafOfModules.instIsLeftAdjointSheafOfModulesSheafification 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : (PresheafOfModules.sheafification α).IsLeftAdjoint
• PresheafOfModules.instFaithfulSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : ((SheafOfModules.forget R).comp (PresheafOfModules.restrictScalars α)).Faithful
• PresheafOfModules.instFullSheafOfModulesCompObjFunctorOppositeRingCatIsSheafForgetRestrictScalars 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : ((SheafOfModules.forget R).comp (PresheafOfModules.restrictScalars α)).Full
• PresheafOfModules.sheafificationAdjunction 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : PresheafOfModules.sheafification α ⊣ (SheafOfModules.forget R).comp (PresheafOfModules.restrictScalars α)
• PresheafOfModules.sheafificationCompToSheaf 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : (PresheafOfModules.sheafification α).comp (SheafOfModules.toSheaf R) ≅ (PresheafOfModules.toPresheaf R₀).comp (CategoryTheory.presheafToSheaf J AddCommGrpCat)
• PresheafOfModules.sheafificationHomEquiv 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] {P : PresheafOfModules R₀} {F : SheafOfModules R} : ((PresheafOfModules.sheafification α).obj P ⟶ F) ≃ (P ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F))
• PresheafOfModules.sheafificationCompForgetCompToPresheaf 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : (PresheafOfModules.sheafification α).comp ((SheafOfModules.forget R).comp (PresheafOfModules.toPresheaf R.obj)) ≅ (PresheafOfModules.toPresheaf R₀).comp ((CategoryTheory.presheafToSheaf J AddCommGrpCat).comp (CategoryTheory.sheafToPresheaf J AddCommGrpCat))
• PresheafOfModules.instIsIsoFunctorSheafOfModulesCounitSheafificationAdjunction 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : CategoryTheory.IsIso (PresheafOfModules.sheafificationAdjunction α).counit
• PresheafOfModules.sheafification_map 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] {X✝ Y✝ : PresheafOfModules R₀} (f : X✝ ⟶ Y✝) : (PresheafOfModules.sheafification α).map f = PresheafOfModules.sheafifyMap α (CategoryTheory.toSheafify J X✝.presheaf) (CategoryTheory.toSheafify J Y✝.presheaf) f ((CategoryTheory.presheafToSheaf J AddCommGrpCat).map ((PresheafOfModules.toPresheaf R₀).map f)) ⋯
• PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] (M₀ : PresheafOfModules R₀) : (PresheafOfModules.toPresheaf R₀).map ((PresheafOfModules.sheafificationAdjunction α).unit.app M₀) = CategoryTheory.toSheafify J M₀.presheaf
• PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] (M : SheafOfModules R) : (SheafOfModules.toSheaf R).map ((PresheafOfModules.sheafificationAdjunction α).counit.app M) = (CategoryTheory.sheafificationAdjunction J AddCommGrpCat).counit.app ((SheafOfModules.toSheaf R).obj M)
• PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] {P : PresheafOfModules R₀} {F : SheafOfModules R} (f : (PresheafOfModules.sheafification α).obj P ⟶ F) : (PresheafOfModules.toPresheaf R₀).map ((PresheafOfModules.sheafificationHomEquiv α) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P.presheaf) ((PresheafOfModules.toPresheaf R.obj).map f.val)
• PresheafOfModules.sheafificationAdjunction_homEquiv_apply 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] {P : PresheafOfModules R₀} {F : SheafOfModules R} (f : (PresheafOfModules.sheafification α).obj P ⟶ F) : ((PresheafOfModules.sheafificationAdjunction α).homEquiv P F) f = (PresheafOfModules.sheafificationHomEquiv α) f
• PresheafOfModules.toPresheaf_map_sheafificationHomEquiv 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] {P : PresheafOfModules R₀} {F : SheafOfModules R} (f : (PresheafOfModules.sheafification α).obj P ⟶ F) : (PresheafOfModules.toPresheaf R₀).map ((PresheafOfModules.sheafificationHomEquiv α) f) = ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)) ((SheafOfModules.toSheaf R).map f)
• PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] {P : PresheafOfModules R₀} {F : SheafOfModules R} (g : P ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F)) : (SheafOfModules.toSheaf R).map ((PresheafOfModules.sheafificationHomEquiv α).symm g) = ((CategoryTheory.sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm ((PresheafOfModules.toPresheaf R₀).map g)
• SheafOfModules.instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasColimitsOfSize.{w', w, max u' v, max (max (max (v + 1) u) u') v'} (PresheafOfModules R.obj)] : CategoryTheory.Limits.HasColimitsOfSize.{w', w, max u' v, max (max (max (v + 1) u) u') v'} (SheafOfModules R)
• SheafOfModules.instHasColimitsOfShapeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (K : Type w) [CategoryTheory.Category.{w', w} K] [CategoryTheory.Limits.HasColimitsOfShape K (PresheafOfModules R.obj)] : CategoryTheory.Limits.HasColimitsOfShape K (SheafOfModules R)
• SheafOfModules.free 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I : Type u) : SheafOfModules R
• SheafOfModules.freeFunctor 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.Functor (Type u) (SheafOfModules R)
• SheafOfModules.freeSection 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I : Type u} (i : I) : (SheafOfModules.free I).sections
• SheafOfModules.freeCofan 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I : Type u) : CategoryTheory.Limits.Cofan fun x => SheafOfModules.unit R
• SheafOfModules.instPreservesColimitsOfSizeFreeFunctor 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.Limits.PreservesColimitsOfSize.{v₂, u₂, u, max u u₁, u + 1, max (max (u + 1) u₁) v₁} SheafOfModules.freeFunctor
• SheafOfModules.freeFunctor_obj 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (X : Type u) : SheafOfModules.freeFunctor.obj X = SheafOfModules.free X
• SheafOfModules.ιFree 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I : Type u} (i : I) : SheafOfModules.unit R ⟶ SheafOfModules.free I
• SheafOfModules.isColimitFreeCofan 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I : Type u) : CategoryTheory.Limits.IsColimit (SheafOfModules.freeCofan I)
• SheafOfModules.freeMap 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I J✝ : Type u} (f : I → J✝) : SheafOfModules.free I ⟶ SheafOfModules.free J✝
• SheafOfModules.freeHomEquiv 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) {I : Type u} : (SheafOfModules.free I ⟶ M) ≃ (I → M.sections)
• SheafOfModules.sectionMap_freeMap_freeSection 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I J✝ : Type u} (f : I → J✝) (i : I) : SheafOfModules.sectionsMap (SheafOfModules.freeMap f) (SheafOfModules.freeSection i) = SheafOfModules.freeSection (f i)
• SheafOfModules.freeFunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {X Y : Type u} (f : X ⟶ Y) : SheafOfModules.freeFunctor.map f = SheafOfModules.freeMap ⇑(CategoryTheory.ConcreteCategory.hom f)
• SheafOfModules.freeCofan_inj 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I : Type u} (i : I) : (SheafOfModules.freeCofan I).inj i = SheafOfModules.ιFree i
• SheafOfModules.ιFree_freeMap 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I J✝ : Type u} (f : I → J✝) (i : I) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (SheafOfModules.freeMap f) = SheafOfModules.ιFree (f i)
• SheafOfModules.freeSumIso 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I J✝ : Type u) : SheafOfModules.free I ⨿ SheafOfModules.free J✝ ≅ SheafOfModules.free (I ⊕ J✝)
• SheafOfModules.ιFree_freeMap_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I J✝ : Type u} (f : I → J✝) (i : I) {Z : SheafOfModules R} (h : SheafOfModules.free J✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap f) h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree (f i)) h
• SheafOfModules.mapFree 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) (η : SheafOfModules.unit S ⟶ F.obj (SheafOfModules.unit R)) : SheafOfModules.free I ⟶ F.obj (SheafOfModules.free I)
• SheafOfModules.mapFreeIso 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) : SheafOfModules.free I ≅ F.obj (SheafOfModules.free I)
• SheafOfModules.sectionsMap_freeHomEquiv_symm_freeSection 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I : Type u} {M : SheafOfModules R} (f : I → M.sections) (i : I) : SheafOfModules.sectionsMap (M.freeHomEquiv.symm f) (SheafOfModules.freeSection i) = f i
• SheafOfModules.freeHomEquiv_apply 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {I : Type u} (f : SheafOfModules.free I ⟶ M) (i : I) : M.freeHomEquiv f i = SheafOfModules.sectionsMap f (SheafOfModules.freeSection i)
• SheafOfModules.freeHomEquiv_freeMap 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I J✝ : Type u} (f : I → J✝) : (SheafOfModules.free J✝).freeHomEquiv (SheafOfModules.freeMap f) = SheafOfModules.freeSection ∘ f
• SheafOfModules.mapFreeIso_hom 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) : (SheafOfModules.mapFreeIso F I η).hom = SheafOfModules.mapFree F I η.hom
• SheafOfModules.ιFree_mapFree 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) (η : SheafOfModules.unit S ⟶ F.obj (SheafOfModules.unit R)) (i : I) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (SheafOfModules.mapFree F I η) = CategoryTheory.CategoryStruct.comp η (F.map (SheafOfModules.ιFree i))
• SheafOfModules.inl_freeSumIso_hom 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I J✝ : Type u) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (SheafOfModules.freeSumIso I J✝).hom = SheafOfModules.freeMap Sum.inl
• SheafOfModules.inr_freeSumIso_hom 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I J✝ : Type u) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (SheafOfModules.freeSumIso I J✝).hom = SheafOfModules.freeMap Sum.inr
• SheafOfModules.ιFree_mapFree_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) (η : SheafOfModules.unit S ⟶ F.obj (SheafOfModules.unit R)) (i : I) {Z : SheafOfModules S} (h : F.obj (SheafOfModules.free I) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFree F I η) h) = CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i)) h)
• SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {I : Type u} {M : SheafOfModules R} (f : SheafOfModules.free I ⟶ M) (i : I) : M.unitHomEquiv.symm (M.freeHomEquiv f i) = CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) f
• SheafOfModules.ιFree_mapFreeIso_hom 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (SheafOfModules.mapFreeIso F I η).hom = CategoryTheory.CategoryStruct.comp η.hom (F.map (SheafOfModules.ιFree i))
• SheafOfModules.ιFree_mapFree_inv 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (SheafOfModules.mapFreeIso F I η).hom = CategoryTheory.CategoryStruct.comp η.hom (F.map (SheafOfModules.ιFree i))
• SheafOfModules.map_ιFree_mapFreeIso_inv 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I) : CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i)) (SheafOfModules.mapFreeIso F I η).inv = CategoryTheory.CategoryStruct.comp η.inv (SheafOfModules.ιFree i)
• SheafOfModules.map_ιFree_mapFree_hom 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I) : CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i)) (SheafOfModules.mapFreeIso F I η).inv = CategoryTheory.CategoryStruct.comp η.inv (SheafOfModules.ιFree i)
• SheafOfModules.freeHomEquiv_comp_apply 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} {I : Type u} (f : SheafOfModules.free I ⟶ M) (p : M ⟶ N) (i : I) : N.freeHomEquiv (CategoryTheory.CategoryStruct.comp f p) i = SheafOfModules.sectionsMap p (M.freeHomEquiv f i)
• SheafOfModules.freeHomEquiv_symm_comp 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} {I : Type u} (s : I → M.sections) (p : M ⟶ N) : CategoryTheory.CategoryStruct.comp (M.freeHomEquiv.symm s) p = N.freeHomEquiv.symm fun i => SheafOfModules.sectionsMap p (s i)
• SheafOfModules.ιFree_mapFreeIso_hom_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I) {Z : SheafOfModules S} (h : F.obj (SheafOfModules.free I) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) (CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFreeIso F I η).hom h) = CategoryTheory.CategoryStruct.comp η.hom (CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i)) h)
• SheafOfModules.map_ιFree_mapFreeIso_inv_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) (I : Type u) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete I) F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (i : I) {Z : SheafOfModules S} (h : SheafOfModules.free I ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (SheafOfModules.ιFree i)) (CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFreeIso F I η).inv h) = CategoryTheory.CategoryStruct.comp η.inv (CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) h)
• SheafOfModules.inl_freeSumIso_hom_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I J✝ : Type u) {Z : SheafOfModules R} (h : SheafOfModules.free (I ⊕ J✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (SheafOfModules.freeSumIso I J✝).hom h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inl) h
• SheafOfModules.inr_freeSumIso_hom_assoc 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (I J✝ : Type u) {Z : SheafOfModules R} (h : SheafOfModules.free (I ⊕ J✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (SheafOfModules.freeSumIso I J✝).hom h) = CategoryTheory.CategoryStruct.comp (SheafOfModules.freeMap Sum.inr) h
• CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] : ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (CategoryTheory.presheafToSheaf J A) ≅ (CategoryTheory.presheafToSheaf K A).comp (G.sheafPushforwardContinuous A J K)
• CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] (F : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (G.op.comp F)) ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom = G.op.whiskerLeft (CategoryTheory.toSheafify K F)
• CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_hom 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] (F : CategoryTheory.Functor Dᵒᵖ A) : ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom = CategoryTheory.sheafifyLift J (G.op.whiskerLeft (CategoryTheory.toSheafify K F)) ⋯
• CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val 📋 Mathlib.CategoryTheory.Sites.CoverLifting
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsContinuous J K] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] (F : CategoryTheory.Functor Dᵒᵖ A) : ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).hom = CategoryTheory.sheafifyLift J (G.op.whiskerLeft (CategoryTheory.toSheafify K F)) ⋯
• CategoryTheory.Functor.IsDenseSubsite.hasWeakSheafify_of_isEquivalence 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] : CategoryTheory.HasWeakSheafify K A
• CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] : CategoryTheory.Functor (CategoryTheory.Functor Dᵒᵖ A) (CategoryTheory.Sheaf K A)
• CategoryTheory.Functor.IsDenseSubsite.sheafifyAdjunctionOfIsEquivalence 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] : CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A ⊣ CategoryTheory.sheafToPresheaf K A
• CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_3} [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] {P : CategoryTheory.Functor Dᵒᵖ A} {Q : CategoryTheory.Sheaf K A} : ((CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P ⟶ Q) ≃ (P ⟶ Q.obj)
• CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalenceCompIso 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).comp (G.sheafPushforwardContinuous A J K) ≅ ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (CategoryTheory.presheafToSheaf J A)
• CategoryTheory.Functor.IsDenseSubsite.sheafEquivSheafificationCompatibility 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) (A : Type u_3) [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] : ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).comp (CategoryTheory.presheafToSheaf J A) ≅ (CategoryTheory.presheafToSheaf K A).comp (CategoryTheory.Functor.IsDenseSubsite.sheafEquiv J K G A).inverse
• CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_3} [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] {P : CategoryTheory.Functor Dᵒᵖ A} {Q₁ Q₂ : CategoryTheory.Sheaf K A} (f : (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁) (g : Q₁ ⟶ Q₂) : (CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) f) g.hom
• CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_3} [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] {P₁ P₂ : CategoryTheory.Functor Dᵒᵖ A} (f : P₁ ⟶ P₂) {Q : CategoryTheory.Sheaf K A} (g : (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q) : (CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).map f) g) = CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) g)
• CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_right_assoc 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_3} [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] {P : CategoryTheory.Functor Dᵒᵖ A} {Q₁ Q₂ : CategoryTheory.Sheaf K A} (f : (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁) (g : Q₁ ⟶ Q₂) {Z : CategoryTheory.Functor Dᵒᵖ A} (h : Q₂.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) f) (CategoryTheory.CategoryStruct.comp g.hom h)
• CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left_assoc 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_3} [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Functor.IsDenseSubsite J K G] [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A] {P₁ P₂ : CategoryTheory.Functor Dᵒᵖ A} (f : P₁ ⟶ P₂) {Q : CategoryTheory.Sheaf K A} (g : (CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q) {Z : CategoryTheory.Functor Dᵒᵖ A} (h : Q.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence J K G A).map f) g)) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence J K G) g) h)
• SheafOfModules.GeneratingSections 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Type (max (u + 1) u')
• SheafOfModules.GeneratingSections.I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (self : M.GeneratingSections) : Type u
• SheafOfModules.GeneratingSections.IsFiniteType 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (σ : M.GeneratingSections) : Prop
• SheafOfModules.IsFiniteType 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Prop
• SheafOfModules.LocalGeneratorsData 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : Type (max (max (max (u + 1) u') v') (w + 1))
• SheafOfModules.GeneratingSections.s 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (self : M.GeneratingSections) : self.I → M.sections
• SheafOfModules.GeneratingSections.IsFiniteType.finite 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {inst✝¹ : CategoryTheory.HasWeakSheafify J AddCommGrpCat} {inst✝² : J.WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R} {σ : M.GeneratingSections} [self : σ.IsFiniteType] : Finite σ.I
• SheafOfModules.GeneratingSections.IsFiniteType.mk 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {σ : M.GeneratingSections} (finite : Finite σ.I := by infer_instance) : σ.IsFiniteType
• SheafOfModules.LocalGeneratorsData.I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (self : M.LocalGeneratorsData) : Type w
• SheafOfModules.LocalGeneratorsData.IsFiniteType 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (p : M.LocalGeneratorsData) : Prop
• SheafOfModules.GeneratingSections.equivOfIso 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (e : M ≅ N) : M.GeneratingSections ≃ N.GeneratingSections
• SheafOfModules.LocalGeneratorsData.shrink 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.LocalGeneratorsData) : M.LocalGeneratorsData
• SheafOfModules.LocalGeneratorsData.X 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (self : M.LocalGeneratorsData) : self.I → C
• SheafOfModules.GeneratingSections.π 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (σ : M.GeneratingSections) : SheafOfModules.free σ.I ⟶ M
• SheafOfModules.LocalGeneratorsData.coversTop 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (self : M.LocalGeneratorsData) : J.CoversTop self.X
• SheafOfModules.IsFiniteType.exists_localGeneratorsData 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {inst✝¹ : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat} {inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} (M : SheafOfModules R) [self : M.IsFiniteType] : ∃ σ, σ.IsFiniteType
• SheafOfModules.IsFiniteType.mk 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (exists_localGeneratorsData : ∃ σ, σ.IsFiniteType) : M.IsFiniteType
• SheafOfModules.GeneratingSections.opEpi_id 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (σ : M.GeneratingSections) : σ.ofEpi (CategoryTheory.CategoryStruct.id M) = σ
• SheafOfModules.GeneratingSections.ofEpi 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] : N.GeneratingSections
• SheafOfModules.LocalGeneratorsData.mk 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (I : Type w) (X : I → C) (coversTop : J.CoversTop X) (generators : (i : I) → (M.over (X i)).GeneratingSections) : M.LocalGeneratorsData
• SheafOfModules.GeneratingSections.instIsFiniteTypeOfEpi 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] [σ.IsFiniteType] : (σ.ofEpi p).IsFiniteType
• SheafOfModules.GeneratingSections.ofEpi_I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] : (σ.ofEpi p).I = σ.I
• SheafOfModules.GeneratingSections.ofEpi_s 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] (i : σ.I) : (σ.ofEpi p).s i = SheafOfModules.sectionsMap p (σ.s i)
• SheafOfModules.LocalGeneratorsData.generators 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (self : M.LocalGeneratorsData) (i : self.I) : (M.over (self.X i)).GeneratingSections
• SheafOfModules.LocalGeneratorsData.IsFiniteType.isFiniteType 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {inst✝¹ : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat} {inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} {p : M.LocalGeneratorsData} [self : p.IsFiniteType] (i : p.I) : (p.generators i).IsFiniteType
• SheafOfModules.LocalGeneratorsData.IsFiniteType.mk 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {p : M.LocalGeneratorsData} (isFiniteType : ∀ (i : p.I), (p.generators i).IsFiniteType := by infer_instance) : p.IsFiniteType
• SheafOfModules.GeneratingSections.localGeneratorsData 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) : M.LocalGeneratorsData
• SheafOfModules.GeneratingSections.ofEpi_π 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] : (σ.ofEpi p).π = CategoryTheory.CategoryStruct.comp σ.π p
• SheafOfModules.GeneratingSections.localGeneratorsData_I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) : G.localGeneratorsData.I = C
• SheafOfModules.GeneratingSections.localGeneratorsData_X 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (a : C) : G.localGeneratorsData.X a = id a
• SheafOfModules.GeneratingSections.opEpi_comp 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M N P : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) (q : N ⟶ P) [CategoryTheory.Epi p] [CategoryTheory.Epi q] : σ.ofEpi (CategoryTheory.CategoryStruct.comp p q) = (σ.ofEpi p).ofEpi q
• SheafOfModules.GeneratingSections.map 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [CategoryTheory.Category.{v₁, u₁} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) : (F.obj M).GeneratingSections
• SheafOfModules.instIsFiniteTypeMap 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [CategoryTheory.Category.{v₁, u₁} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) [G.IsFiniteType] : (G.map F η).IsFiniteType
• SheafOfModules.GeneratingSections.map_I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [CategoryTheory.Category.{v₁, u₁} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) : (G.map F η).I = G.I
• SheafOfModules.GeneratingSections.mapFreeHom 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [CategoryTheory.Category.{v₁, u₁} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) : SheafOfModules.free G.I ⟶ F.obj M
• SheafOfModules.GeneratingSections.mk 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (I : Type u) (s : I → M.sections) (epi : CategoryTheory.Epi (M.freeHomEquiv.symm s) := by infer_instance) : M.GeneratingSections
• SheafOfModules.instIsIsoπMap 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [CategoryTheory.Category.{v₁, u₁} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) [CategoryTheory.IsIso G.π] : CategoryTheory.IsIso (G.map F η).π
• SheafOfModules.GeneratingSections.epi 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (self : M.GeneratingSections) : CategoryTheory.Epi (M.freeHomEquiv.symm self.s)
• SheafOfModules.GeneratingSections.localGeneratorsData_generators 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (x : C) : G.localGeneratorsData.generators x = G.map (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over x))) (CategoryTheory.Iso.refl (SheafOfModules.unit (R.over x)))
• SheafOfModules.GeneratingSections.map_π_eq 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [CategoryTheory.Category.{v₁, u₁} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) : (G.map F η).π = CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFreeIso F G.I η).hom (F.map G.π)
• SheafOfModules.GeneratingSections.map_s 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [CategoryTheory.Category.{v₁, u₁} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) (a✝ : G.I) : (G.map F η).s a✝ = (F.obj M).freeHomEquiv (G.mapFreeHom F η) a✝
• PresheafOfModules.instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : (PresheafOfModules.sheafification α).IsLocalization (J.W.inverseImage (PresheafOfModules.toPresheaf R₀))
• PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
  {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj) [CategoryTheory.Presheaf.IsLocallyInjective J α] [CategoryTheory.Presheaf.IsLocallySurjective J α] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] : J.W.inverseImage (PresheafOfModules.toPresheaf R₀) = (CategoryTheory.MorphismProperty.isomorphisms (SheafOfModules R)).inverseImage (PresheafOfModules.sheafification α)
• SheafOfModules.Presentation 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Type (max (u + 1) u₁)
• SheafOfModules.Presentation.IsFinite 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (p : M.Presentation) : Prop
• SheafOfModules.Presentation.generators 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (self : M.Presentation) : M.GeneratingSections
• SheafOfModules.IsFinitePresentation 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Prop
• SheafOfModules.IsQuasicoherent 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Prop
• SheafOfModules.QuasicoherentData 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Type (max (max (max (u + 1) u₁) v₁) (w + 1))
• SheafOfModules.QuasicoherentData.I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (self : M.QuasicoherentData) : Type w
• SheafOfModules.QuasicoherentData.IsFinitePresentation 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) : Prop
• SheafOfModules.isFinitePresentation 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.ObjectProperty (SheafOfModules R)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c