Theorems · Definition · category theory
SheafOfModules.unitHomEquiv
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
{J : CategoryTheory.GrothendieckTopology C} →
{R : CategoryTheory.Sheaf J RingCat} → (M : SheafOfModules R) → (SheafOfModules.unit R ⟶ M) ≃ M.sectionsThe bijection (unit R ⟶ M) ≃ M.sections for M : SheafOfModules R.
- Defined in
- Mathlib.Algebra.Category.ModuleCat.Sheaf
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement · cited by 32,603
- Equivstatement · cited by 8,337
- CategoryTheory.GrothendieckTopologystatement and proof · cited by 1,415
- CategoryTheory.Sheafstatement and proof · cited by 763
- RingCatstatement and proof · cited by 473
- Equiv.transproof · cited by 337
- SheafOfModulesstatement and proof · cited by 188
- SheafOfModules.valproof · cited by 55
- SheafOfModules.unitstatement · cited by 45
- CategoryTheory.Functor.FullyFaithful.homEquivproof · cited by 31
- SheafOfModules.sectionsstatement · cited by 28
Cited by7
Results whose statement or proof uses this declaration.
- SheafOfModules.freeHomEquivproof · cited by 20
- SheafOfModules.ιFree_freeMapproof · cited by 3
- SheafOfModules.unitHomEquiv_symm_freeHomEquiv_applystatement and proof · cited by 1
- SheafOfModules.unitHomEquiv_apply_coestatement · cited by 0
- SheafOfModules.unitHomEquiv_comp_applystatement · cited by 0
- SheafOfModules.pushforwardSections_unitHomEquivstatement and proof · cited by 0
- SheafOfModules.unitHomEquiv_symm_compstatement and proof · cited by 0