Theorems · Theorem · category theory

SheafOfModules.LocalGeneratorsData.mk.injEq

∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R}
  [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (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) (I_1 : Type w) (X_1 : I_1 → C)
  (coversTop_1 : J.CoversTop X_1) (generators_1 : (i : I_1) → (M.over (X_1 i)).GeneratingSections),
  ({ I := I, X := X, coversTop := coversTop, generators := generators } =
      { I := I_1, X := X_1, coversTop := coversTop_1, generators := generators_1 }) =
    (I = I_1 ∧ X ≍ X_1 ∧ generators ≍ generators_1)

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijective