Theorems · Definition · category theory

SheafOfModules.GeneratingSections.mk.noConfusion

{C : Type u'} →
  {inst : CategoryTheory.Category.{v', u'} C} →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        {inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat} →
          {inst_2 : J.WEqualsLocallyBijective AddCommGrpCat} →
            {M : SheafOfModules R} →
              {P : Sort u_1} →
                {I : Type u} →
                  {s : I → M.sections} →
                    {epi :
                        autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s))
                          SheafOfModules.GeneratingSections.epi._autoParam} →
                      {I' : Type u} →
                        {s' : I' → M.sections} →
                          {epi' :
                              autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s'))
                                SheafOfModules.GeneratingSections.epi._autoParam} →
                            { I := I, s := s, epi := epi } = { I := I', s := s', epi := epi' } →
                              (I = I' → s ≍ s' → P) → P

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Cited by

1 results in Mathlib

Foundations

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