Theorems · Theorem · category theory

SheafOfModules.GeneratingSections.mk.inj

∀ {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} {I : Type u} {s : I → M.sections}
  {epi : autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s)) SheafOfModules.GeneratingSections.epi._autoParam}
  {I_1 : Type u} {s_1 : I_1 → M.sections}
  {epi_1 : autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s_1)) SheafOfModules.GeneratingSections.epi._autoParam},
  { I := I, s := s, epi := epi } = { I := I_1, s := s_1, epi := epi_1 } → I = I_1 ∧ s ≍ s_1

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Cited by

1 results in Mathlib

Foundations

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