Theorems · Definition · category theory

SheafOfModules.LocalGeneratorsData.mk.noConfusion

{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} →
              {P : Sort u_1} →
                {I : Type w} →
                  {X : I → C} →
                    {coversTop : J.CoversTop X} →
                      {generators : (i : I) → (M.over (X i)).GeneratingSections} →
                        {I' : Type w} →
                          {X' : I' → C} →
                            {coversTop' : J.CoversTop X'} →
                              {generators' : (i : I') → (M.over (X' i)).GeneratingSections} →
                                { I := I, X := X, coversTop := coversTop, generators := generators } =
                                    { I := I', X := X', coversTop := coversTop', generators := generators' } →
                                  (I = I' → X ≍ X' → generators ≍ generators' → P) → P

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Cited by

1 results in Mathlib

Foundations

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