Commit 2026-04-24 19:21 def28638

View on Github →

refactor(Algebra/Category/ModuleCat/Sheaf/Free): generalize SheafOfModules.mapFree (#38341)

  • Generalize mapFree to take in a hom η : unit S ⟶ F.obj (unit R) instead of an iso η : F.obj (unit R) ≅ unit S. Note that this direction does not require F to preserve coproducts, only the inverse does.
  • Rename what used to be mapFree to mapFreeIso
  • Simplify the proofs of ιFree_mapFree_inv and map_ιFree_mapFree_hom, rename them, and create deprecated aliases for the old versions. Motivation for this change: I want to apply mapFree to the existing morphism unitToPushforwardObjUnit : unit S ⟶ (pushforward.{u} φ).obj (unit R), which exactly fits the new type of η. Specializing to φ = 𝟙 (R.over X), this will yield the iso (free I).over X ≅ free (R := R.over X) I in a later PR.

Estimated changes