Theorems · Theorem · category theory

SheafOfModules.LocalGeneratorsData.mk.inj

∀ {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

1 results in Mathlib

Foundations

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