Theorems · Theorem · category theory

PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ R : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R₀ ⟶ R) [CategoryTheory.Presheaf.IsLocallyInjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Functor Cᵒᵖ AddCommGrpCat} (φ : M₀.presheaf ⟶ A)
  [CategoryTheory.Presheaf.IsLocallyInjective J φ],
  CategoryTheory.Presheaf.IsSeparated J A →
    ∀ {Y : C} (r₀ r₀' : ↑(R₀.obj (Opposite.op Y))) (m₀ m₀' : ↑(M₀.obj (Opposite.op Y))),
      (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ =
          (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' →
        (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
            (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀' →
          (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀) =
            (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀' • m₀')

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Cited by

1 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Presheaf.IsLocallyInjectiveCategoryTheory.Presheaf.IsLocallyInjective