Theorems · Theorem · category theory

SheafOfModules.unitHomEquiv_symm_freeHomEquiv_apply

∀ {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] {I : Type u} {M : SheafOfModules R} (f : SheafOfModules.free I ⟶ M)
  (i : I), M.unitHomEquiv.symm (M.freeHomEquiv f i) = CategoryTheory.CategoryStruct.comp (SheafOfModules.ιFree i) f

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijective