Theorems · Theorem · category theory

CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_aux

∀ {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 →
    ∀ {X : C} (r : ↑(R.obj (Opposite.op X))) (m : ↑(A.obj (Opposite.op X))) {Y Z : C} (f : Y ⟶ X) (g : Z ⟶ Y)
      (r₀ : ↑(R₀.obj (Opposite.op Y))) (r₀' : ↑(R₀.obj (Opposite.op Z))) (m₀ : ↑(M₀.obj (Opposite.op Y)))
      (m₀' : ↑(M₀.obj (Opposite.op Z))),
      (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ =
          (CategoryTheory.ConcreteCategory.hom (R.map f.op)) r →
        (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' =
            (CategoryTheory.ConcreteCategory.hom (R.map (CategoryTheory.CategoryStruct.comp f.op g.op))) r →
          (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ =
              (CategoryTheory.ConcreteCategory.hom (A.map f.op)) m →
            (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' =
                (CategoryTheory.ConcreteCategory.hom (A.map (CategoryTheory.CategoryStruct.comp f.op g.op))) m →
              (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Z)))
                  ((CategoryTheory.ConcreteCategory.hom (M₀.map g.op)) (r₀ • m₀)) =
                (CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op Z))) (r₀' • m₀')

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Presheaf.IsLocallyInjectiveCategoryTheory.Presheaf.IsLocallyInjective